Commit d74eb9b6 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Preliminary implementation of simplified polymorphism:

 - polymorphic functions are explicitely annotated
 - runtime non-trivial checks of polymorphic functions raise a runtime exception
parent 74b0ff9b
......@@ -55,7 +55,7 @@ let mk name descr typing compile code ext_info depends =
status = `Unevaluated;
}
let magic = "CDUCE:compunit:00009"
let magic = "CDUCE:compunit:0000A"
let has_obj n =
let base = U.to_string n ^ ".cdo" in
......
......@@ -66,7 +66,8 @@ type t = {
ids : item Env.t;
ns : Ns.table;
keep_ns : bool;
mono : (U.t * Var.t) list;
poly_vars : (U.t * Var.t) list;
mono_vars : Var.Set.t
}
(* Namespaces *)
......@@ -115,7 +116,7 @@ let type_schema env loc name uri =
{ env with ids = Env.add x (ESchema sch) env.ids }
let empty_env =
{ ids = Env.empty; ns = Ns.def_table; keep_ns = false; mono = [] }
{ ids = Env.empty; ns = Ns.def_table; keep_ns = false; poly_vars = []; mono_vars = Var.Set.empty }
let enter_id x i env = { env with ids = Env.add x i env.ids }
......@@ -1001,19 +1002,19 @@ and abstraction env loc a =
USet.empty a.fun_iface
in
let vset = (* remove variables that are locally monomorphic *)
List.fold_left (fun acc (v, _) -> USet.remove v acc) vset env.mono
List.fold_left (fun acc (v, _) -> USet.remove v acc) vset env.poly_vars
in
let vset = List.fold_left (fun acc v -> USet.add v acc) vset a.fun_poly in
(* add those that are explicitely polymorphic. *)
let all_vars =
USet.fold (fun v acc -> (v, Var.mk (U.get_str v)) :: acc) vset env.mono
USet.fold (fun v acc -> (v, Var.mk (U.get_str v)) :: acc) vset env.poly_vars
in
let iface =
List.map
(fun (t1, t2) -> (var_typ all_vars env t1, var_typ all_vars env t2))
a.fun_iface
in
let env = { env with mono = all_vars } in
let env = { env with poly_vars = all_vars } in
let t =
List.fold_left
(fun accu (t1, t2) -> Types.cap accu (Types.arrow t1 t2))
......@@ -1231,6 +1232,7 @@ and type_check' loc env e constr precise =
Types.Print.print a.fun_typ
Types.Print.print constr)
in
let env = { env with mono_vars = Var.Set.cup env.mono_vars (Types.Subst.vars a.fun_typ) } in
let env =
match a.fun_name with
| None -> env
......@@ -1260,15 +1262,26 @@ and type_check' loc env e constr precise =
localize loc (flatten (type_map loc env true e b) constr) precise
| Apply (e1, e2) ->
let t1 = type_check env e1 Types.Function.any true in
let t1 = Types.Arrow.get t1 in
let dom = Types.Arrow.domain t1 in
let t1arrow = Types.Arrow.get t1 in
let dom = Types.Arrow.domain t1arrow in
let t2 = type_check env e2 Types.any true in
let res =
if Var.Set.is_empty (Types.Subst.vars t1) &&
Var.Set.is_empty (Types.Subst.vars t2) then
(* TODO don't retype e2 *)
let t2 = type_check env e2 dom true in
Types.Arrow.apply t1arrow t2
else
match Types.Tallying.squareapply env.mono_vars t1 t2 with
None -> raise_loc loc (Constraint(t2, dom))
| Some (_, res) -> res
(*
if Types.Arrow.need_arg t1 then
let t2 = type_check env e2 dom true in
Types.Arrow.apply t1 t2
else (
ignore (type_check env e2 dom false);
Types.Arrow.apply_noarg t1)
Types.Arrow.apply_noarg t1) *)
in
verify loc res constr
| Var s -> verify loc (find_value s env) constr
......
......@@ -202,7 +202,8 @@ let () =
let open Format in
eprintf "@[SQUARE APPLY@[@\n";
List.iter (fun (f, arg) ->
let subst,ff, aa, res = Types.Tallying.apply_raw Var.Set.empty f arg in
match Types.Tallying.apply_raw Var.Set.empty f arg with
Some ( subst,ff, aa, res ) ->
eprintf "@[(%a) • (%a)@] ~>@[fun=%a@\narg=%a@\nsubst=%a@\nres=%a@]@\n"
Types.Print.print f
Types.Print.print arg
......@@ -210,6 +211,10 @@ let () =
Types.Print.print aa
Types.Subst.print_list subst
Types.Print.print res
| None -> eprintf "@[(%a) • (%a)@] ~> Ill-typed"
Types.Print.print f
Types.Print.print arg
)
[ (f1, arg1); (t_map, t_even) ];
eprintf "@]@]\n%!"
......@@ -653,12 +653,22 @@ let apply_raw delta s t =
loop 0
let apply_full delta s t =
let _, _, _, res = apply_raw delta s t in
res
try
let _, _, _, res = apply_raw delta s t in
Some res
with UnsatConstr _ -> None
let squareapply delta s t =
try
let s, _, _, res = apply_raw delta s t in
(s, res)
Some (s, res)
with UnsatConstr _ -> None
let apply_raw delta s t =
try
Some (apply_raw delta s t)
with UnsatConstr _ -> None
let tallying delta types =
try tallying delta types with Step1Fail | Step2Fail -> []
......@@ -13,8 +13,8 @@ val is_squaresubtype : Var.Set.t -> Types.t -> Types.t -> bool
subst is the set of substitution that make the application succeed,
ss and tt are the expansions of s and t corresponding to that substitution
and res is the type of the result of the application *)
val apply_full : Var.Set.t -> Types.t -> Types.t -> Types.t
val apply_full : Var.Set.t -> Types.t -> Types.t -> Types.t option
val apply_raw : Var.Set.t -> Types.t -> Types.t -> Subst.t list * Types.t * Types.t * Types.t
val apply_raw : Var.Set.t -> Types.t -> Types.t -> (Subst.t list * Types.t * Types.t * Types.t) option
val squareapply : Var.Set.t -> Types.t -> Types.t -> (Subst.t list * Types.t)
val squareapply : Var.Set.t -> Types.t -> Types.t -> (Subst.t list * Types.t) option
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