Commit 1aa6a8b1 authored by Andrei Paskevich's avatar Andrei Paskevich

Mlw: overloaded symbols

This is a prototype version that requires no additional annotation.
In addition to the existing rules of scoping:

  - it is forbidden to declare two symbols with the same name
    in the same scope ("everything can be unambiguously named"),

  - it is allowed to shadow an earlier declaration with a newer one,
    if they belong to different scopes (e.g., via import),

we define one new rule:

  - when an rsymbol rs_new would normally shadow an rsymbol rs_old,
    but (1) both of them are either
      - binary relations: t -> t -> bool,
      - binary operators: t -> t -> t, or
      - unary operators:  t -> t
    and (2) their argument types are not the same,
    then rs_old remains visible in the current scope.
    Both symbols should take non-ghost arguments and
    return non-ghost results, but effects are allowed.
    The name itself is not taken into account, hence
    it is possible to overload "div", "mod", or "fact".

Clause (1) allows us to perform type inference for a family of rsymbols,
using an appropriate generalized signature.

Clause (2) removes guaranteed ambiguities: we treat this case as
the user's intention to redefine the symbol for a given type.

Type inference failures are still possible: either due to
polymorphism (['a -> 'a] combines with [int -> int] and
will fail with the "ambiguous notation" error), or due
to inability to infer the precise types of arguments.
Explicit type annotations and/or use of qualified names
for disambiguation should always allow to bypass the errors.

Binary operations on Booleans are treated as relations, not as
operators. Thus, (+) on bool will not combine with (+) on int.

This overloading only concerns programs: in logic, the added rule
does not apply, and the old symbols get shadowed by the new ones.

In this setting, modules never export families of overloaded symbols:
it is impossible to "use import" a single module, and have access to
several rsymbols for (=) or (+).

The new "overloading" rule prefers to silently discard the previous
binding when it cannot be combined with the new one. This allows us
to be mostly backward compatible with existing programs (except for
the cases where type inference fails, as discussed above).

This rule should be enough to have several equalities for different
program types or overloaded arithmetic operations for bounded integers.
These rsymbols should not be defined as let-functions: in fact, it is
forbidden now to redefine equality in logic, and the bounded integers
should be all coerced into mathematical integers anyway.

I would like to be able to overload mixfix operators too, but
there is no reasonable generalized signature for them: compare
"([]) : map 'a 'b -> 'a -> 'b" with "([]) : array 'a -> int -> 'a"
with "([]) : monomap -> key -> elt". If we restrict the overloading
to symbols with specific names, we might go with "'a -> 'b -> 'c" for
type inference (and even "'a -> 'b" for some prefix operators, such
as "!" or "?"). To discuss.
parent 025d36c7
...@@ -70,16 +70,35 @@ let overload_of_rs {rs_cty = cty} = ...@@ -70,16 +70,35 @@ let overload_of_rs {rs_cty = cty} =
exception IncompatibleNotation of string exception IncompatibleNotation of string
let merge_ps chk x vo vn = match vo, vn with let merge_ps chk x vo vn =
| OO s1, OO s2 -> let fsty rs = (List.hd rs.rs_cty.cty_args).pv_ity in
let o1 = overload_of_rs (Srs.choose s1) in if chk then match vo, vn with (* export namespace *)
let o2 = overload_of_rs (Srs.choose s2) in (* currently, we have no way to export notation *)
if o1 <> o2 then raise (IncompatibleNotation x); | _, OO _ | OO _, _ -> assert false
OO (Srs.union s1 s2) | PV v1, PV v2 when pv_equal v1 v2 -> vo
| _ when not chk -> vn | RS r1, RS r2 when rs_equal r1 r2 -> vo
| PV v1, PV v2 when pv_equal v1 v2 -> vo | _ -> raise (ClashSymbol x)
| RS r1, RS r2 when rs_equal r1 r2 -> vo else match vo, vn with (* import namespace *)
| _ -> raise (ClashSymbol x) (* once again, no way to export notation *)
| _, OO _ -> assert false
(* but we can merge two compatible symbols *)
| RS r1, RS r2 when not (rs_equal r1 r2) ->
let o1 = overload_of_rs r1 in
let o2 = overload_of_rs r2 in
if o1 <> o2 || o2 = NoOver then vn else
if fsty r1 == fsty r2 then vn else
OO (Srs.add r2 (Srs.singleton r1))
(* or add a compatible symbol to notation *)
| OO s1, RS r2 ->
let o1 = overload_of_rs (Srs.choose s1) in
let o2 = overload_of_rs r2 in
if o1 <> o2 || o2 = NoOver then vn else
let ty = fsty r2 in
let confl r = fsty r != ty in
let s1 = Srs.filter confl s1 in
if Srs.is_empty s1 then vn else
OO (Srs.add r2 s1)
| _ -> vn
let rec merge_ns chk _ no nn = let rec merge_ns chk _ no nn =
if no == nn then no else if no == nn then no else
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment