Commit 084211c1 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Mlw: slightly generalize the rules for overloading

A symbol is now considered overloadable if it satisfies
the following conditions:
  - it has at least one parameter
  - it is non-ghost and has fully visible result
  - all of its parameters are non-ghost and have the same type
  - its result is either of the same type as its parameters
    or it is a monomorphic immutable type.

An overloadable symbol can be combined with other symbols of the
same arity and overloading kind. Otherwise, the new symbol shadows
the previously defined ones.

This generalisation allows us to overload symbols such as "size"
or "length", and also symbols of arbitraty non-zero arity.

I am reluctant to generalize this any further, because then we
won't have reasonable destructible signatures for type inference.
parent 54190a07
......@@ -708,12 +708,13 @@ let dexpr ?loc node =
specialize_rs rs
| DEsym (OO ss) ->
let dt = dity_fresh () in
let ot = overload_of_rs (Srs.choose ss) in
begin match ot with
| UnOp -> [dt], dt
| BinOp -> [dt;dt], dt
| BinRel -> [dt;dt], dity_bool
| NoOver -> assert false end
let rs = Srs.choose ss in
let ot = overload_of_rs rs in
let res = match ot with
| SameType -> dt
| FixedRes ity -> dity_of_ity ity
| NoOver -> assert false (* impossible *) in
List.map (fun _ -> dt) rs.rs_cty.cty_args, res
| DEls_pure ls ->
specialize_ls ls
| DEpv_pure pv ->
......
......@@ -545,7 +545,7 @@ let create_let_decl ld =
let create_exn_decl xs =
if not (ity_closed xs.xs_ity) then Loc.errorm ?loc:xs.xs_name.id_loc
"Top-level exception %a has a polymorphic type" print_xs xs;
if not xs.xs_ity.ity_imm then Loc.errorm ?loc:xs.xs_name.id_loc
if not (ity_immutable xs.xs_ity) then Loc.errorm ?loc:xs.xs_name.id_loc
"The type of top-level exception %a has mutable components" print_xs xs;
mk_decl (PDexn xs) []
......
......@@ -49,25 +49,28 @@ let merge_ts = ns_replace its_equal
let merge_xs = ns_replace xs_equal
type overload =
| UnOp (* t -> t *)
| BinOp (* t -> t -> t *)
| BinRel (* t -> t -> bool *)
| NoOver (* none of the above *)
| FixedRes of ity (* t -> t -> ... -> T *)
| SameType (* t -> t -> ... -> t *)
| NoOver (* neither *)
let overload_of_rs {rs_cty = cty} =
if cty.cty_effect.eff_ghost then NoOver else
if cty.cty_mask <> MaskVisible then NoOver else
let same_type ity a = not a.pv_ghost && ity_equal a.pv_ity ity in
match cty.cty_args with
| [a;b] when ity_equal a.pv_ity b.pv_ity &&
ity_equal cty.cty_result ity_bool &&
not a.pv_ghost && not b.pv_ghost -> BinRel
| [a;b] when ity_equal a.pv_ity b.pv_ity &&
ity_equal cty.cty_result a.pv_ity &&
not a.pv_ghost && not b.pv_ghost -> BinOp
| [a] when ity_equal cty.cty_result a.pv_ity &&
not a.pv_ghost -> UnOp
| a::al when not a.pv_ghost && List.for_all (same_type a.pv_ity) al ->
let res = cty.cty_result in
if ity_equal res a.pv_ity then SameType else
if ity_closed res && ity_immutable res then FixedRes res else NoOver
| _ -> NoOver
let same_overload r1 r2 =
List.length r1.rs_cty.cty_args = List.length r2.rs_cty.cty_args &&
match overload_of_rs r1, overload_of_rs r2 with
| SameType, SameType -> true
| FixedRes t1, FixedRes t2 -> ity_equal t1 t2
| _ -> false (* two NoOver's are not the same *)
exception IncompatibleNotation of string
let merge_ps chk x vo vn =
......@@ -83,18 +86,14 @@ let merge_ps chk x vo vn =
| _, 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
if not (same_overload r1 r2) then vn else
if ity_equal (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 r1 = Srs.choose s1 and ty = fsty r2 in
if not (same_overload r1 r2) then vn else
let confl r = not (ity_equal (fsty r) ty) in
let s1 = Srs.filter confl s1 in
if Srs.is_empty s1 then vn else
OO (Srs.add r2 s1)
......
......@@ -42,10 +42,9 @@ val ns_find_xs : namespace -> string list -> xsymbol
val ns_find_ns : namespace -> string list -> namespace
type overload =
| UnOp (* t -> t *)
| BinOp (* t -> t -> t *)
| BinRel (* t -> t -> bool *)
| NoOver (* none of the above *)
| FixedRes of ity (* t -> t -> ... -> T *)
| SameType (* t -> t -> ... -> t *)
| NoOver (* neither *)
val overload_of_rs : rsymbol -> overload
......
......@@ -108,8 +108,17 @@ let find_xsymbol muc q = find_xsymbol_ns (get_namespace muc) q
let find_itysymbol muc q = find_itysymbol_ns (get_namespace muc) q
let find_prog_symbol muc q = find_prog_symbol_ns (get_namespace muc) q
let find_rsymbol muc q = match find_prog_symbol muc q with RS rs -> rs
| _ -> Loc.errorm ~loc:(qloc q) "program symbol expected"
let find_special muc test nm q =
match find_prog_symbol muc q with
| RS s when test s -> s
| OO ss ->
begin match Srs.elements (Srs.filter test ss) with
| [s] -> s
| _::_ -> Loc.errorm ~loc:(qloc q)
"Ambiguous %s notation: %a" nm print_qualid q
| [] -> Loc.errorm ~loc:(qloc q) "Not a %s: %a" nm print_qualid q
end
| _ -> Loc.errorm ~loc:(qloc q) "Not a %s: %a" nm print_qualid q
(** Parsing types *)
......@@ -397,8 +406,8 @@ open Dexpr
(* records *)
let find_record_field muc q =
match find_prog_symbol muc q with RS ({rs_field = Some _} as s) -> s
| _ -> Loc.errorm ~loc:(qloc q) "Not a record field: %a" print_qualid q
let test rs = rs.rs_field <> None in
find_special muc test "record field" q
let find_record_field2 muc (q,e) = find_record_field muc q, e
......@@ -434,12 +443,18 @@ let parse_record ~loc muc get_val fl =
(* patterns *)
let find_constructor muc q =
let test rs = match rs.rs_logic with
| RLls {ls_constr = c} -> c > 0
| _ -> false in
find_special muc test "constructor" q
let rec dpattern muc { pat_desc = desc; pat_loc = loc } =
Dexpr.dpattern ~loc (match desc with
| Ptree.Pwild -> DPwild
| Ptree.Pvar (x, gh) -> DPvar (create_user_id x, gh)
| Ptree.Papp (q, pl) ->
DPapp (find_rsymbol muc q, List.map (fun p -> dpattern muc p) pl)
DPapp (find_constructor muc q, List.map (dpattern muc) pl)
| Ptree.Prec fl ->
let get_val _ _ = function
| Some p -> dpattern muc p
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment