unnecessary qualification of operators when used without arguments

[alleystoughton]

Consider the following example:

require import AllCore List.

theory T.

op [-] (x : int) = 2 * x.

print [-].
(*
* In [operators or predicates]:

op [-] (x : int) : int = 2 * x.
abbrev [-]  : xint -> xint = xopp.
abbrev [-]  : real -> real = opp.
abbrev [-]  : int -> int = CoreInt.opp.
*)

op u = [-] 4.

print u.
(*
* In [operators or predicates]:

op u : int = -4.
*)

op z = [-].

print z.
(*
* In [operators or predicates]:

op z : int -> int = T.[-].
*)

It seems that the redefined operator [-] is needlessly qualified when used with no argument. Because one can use [-] without qualification inside T, and because when it's used with an argument qualification is not used, it seems it should not be needed when used with no arguments.

[alleystoughton]

(I deleted a proposed fix, as it didn't work in general.)

[alleystoughton]

Actually, it seems the current pretty printing is flawed:

require import AllCore.

op a = 3 < 4.

op (<) (x y : int) = x = y.

print (<).
(*
* In [operators or predicates]:

op (<) (x y : int) : bool = x = y.
abbrev (<)  : real -> real -> bool = lt.
abbrev (<)  : int -> int -> bool = CoreInt.lt.
pred (<) ['a] (p q : 'a -> bool) = p <= q /\ ! q <= p.
*)

lemma foo : a = 3 < 4.
proof.
rewrite /a.
(*
Current goal

Type variables: <none>

------------------------------------------------------------------------
3 < 4 = 3 < 4

- - - -

of course this is really

CoreInt.lt 3 4 = (3 = 4)

and thus not provable, but it seems the first `3 < 4` shouldn't
be displayed this way. *)

[alleystoughton]

Also:

require import AllCore.

theory T.

op [!] (x : int) = -x.

op a = [!].

end T.

print T.a.
(*
* In [operators or predicates]:

op a : int -> int = T.[!].
*)

(* note that one can write *)

op b = T.([!]).

op b = T.[!].
(* parse error *)

(* so it seems qualifiction of
a unary operator isn't pretty
printing correctly *)