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

Better fix for variable ordering:

When computing the result type of a function application ((t→s) • u)  with tallying,
one first introduces a fresh variable 𝛾 and computes the tallying of
 (t → s) < (u → 𝛾)
When solving the tallying constraints generated (if that step succeeds),
variables are taken in some implementation defined order (variables created before
have a smaller internal id). It is important then that the variables in u
and 𝛾 are are all before the variables in t and s or all after.

Otherwise, when computing the substitution, variables in u will depend on variables
in t and s that will in turn depend on gamma (which gives unreadable types).
parent bd583e85
Pipeline #181 passed with stages
in 4 minutes and 17 seconds
......@@ -1332,8 +1332,6 @@ and type_check' loc env e constr precise =
let t2 = type_check env e2 dom true in
Types.Arrow.apply t1arrow t2
else
let t1 = Types.Subst.refresh env.mono_vars t1 in
let t2 = Types.Subst.refresh env.mono_vars t2 in
match Types.Tallying.squareapply env.mono_vars t1 t2 with
| None -> raise_loc loc (Constraint (t2, dom))
| Some (_, res) -> res
......
......@@ -8,7 +8,7 @@ let () = Format.set_margin 200
let parse_type str =
match Parse.pat (Stream.of_string str) with
| exception _ -> Types.empty
| p -> (Types.descr (Typer.typ Builtin.env p))
| p -> Types.descr (Typer.typ Builtin.env p)
let re1 = parse_type "{ .. }"
......@@ -161,6 +161,8 @@ let () =
let a = Var.mk "a" in
let b = Var.mk "b" in
let c = Var.mk "c" in
let d = Var.mk "d" in
let vtimes x y = Types.(times (cons (var x)) (cons (var y))) in
let delta = Var.Set.singleton a in
let s = Types.Sequence.star (Types.var b) in
let t = Types.Sequence.star Types.Int.any in
......@@ -178,12 +180,13 @@ let () =
let open Custom.Print in
printf "%a ~> %a@\n"
(pp_list (fun ppf (s, t) ->
fprintf ppf "%a <? %a"
Types.Print.print s Types.Print.print t))
l
Types.Subst.print_list
res)
fprintf ppf "%a <? %a" Types.Print.print s Types.Print.print t))
l Types.Subst.print_list res)
[
[ (vtimes a b, vtimes c d) ];
[ (vtimes a c, vtimes b d) ];
[ (vtimes c d, vtimes a b) ];
[ (vtimes a d, vtimes b c) ];
[ (s, t) ];
[ (s1, t1) ];
[ (s2, t2) ];
......@@ -191,30 +194,62 @@ let () =
[ (Types.Int.any, Types.any) ];
[ (Types.any, Types.empty) ];
];
Format.printf "@]@]\n%!"
Format.printf "@]@]\n%!"
(** Square apply *)
let () =
let t_map = parse_type "('a -> 'b) -> [ 'a * ] -> [ 'b * ]" in
let t_even = parse_type "(('c\\Int) -> ('c\\Int)) & (Int -> Bool)" in
let t_map = parse_type "('a -> 'b) -> [ 'a * ] -> [ 'b * ]" in
let f1 = parse_type "('a -> 'a)" in
let arg1 = Types.Int.any in
let open Format in
eprintf "@[SQUARE APPLY@[@\n";
List.iter (fun (f, arg) ->
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
Types.Print.print ff
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) ];
List.iter
(fun (f, arg) ->
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 Types.Print.print ff
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%!"
(** Debug the order of variables choosen during tallying. *)
let () =
let a = Types.var @@ Var.mk "a" in
let b = Types.var @@ Var.mk "b" in
let c = Types.var @@ Var.mk "c" in
let d = Types.var @@ Var.mk "d" in
let vtimes x y = Types.(times (cons x) (cons y)) in
let varrow x y = Types.(arrow (cons x) (cons y)) in
Format.printf "@[TALLYING@[@\n";
List.iter
(fun l ->
let res = Types.Tallying.tallying Var.Set.empty l in
let open Format in
let open Custom.Print in
printf "%a ~> %a@\n"
(pp_list (fun ppf (s, t) ->
fprintf ppf "%a <? %a" Types.Print.print s Types.Print.print t))
l Types.Subst.print_list res)
[
[ (vtimes a b, vtimes c d) ];
[ (vtimes a c, vtimes b d) ];
[ (vtimes c d, vtimes a b) ];
[ (vtimes a d, vtimes b c) ];
[ (varrow a b, varrow c d) ];
[ (varrow a c, varrow b d) ];
[ (varrow c d, varrow a b) ];
[ (varrow a d, varrow b c) ];
[ (varrow a Types.Int.any, varrow Types.Int.any d) ];
[ (varrow d Types.Int.any, varrow Types.Int.any a) ];
[ (varrow a b, varrow Types.Int.any c) ];
[ (varrow Types.Int.any c, varrow a b) ];
[ (varrow Types.Int.any c, varrow a d) ];
[ (varrow a d, varrow Types.Int.any c) ];
]
......@@ -448,15 +448,15 @@ and norm_record to_type delta mem line =
with Exit -> ConstrSet.unsat
let get_local delta =
try GlobalMemo.find global_memo delta with
Not_found ->
try GlobalMemo.find global_memo delta
with Not_found ->
let mem = LocalMemo.create 17 in
GlobalMemo.add global_memo delta mem;
mem
let norm delta t =
let mem = get_local delta in
norm delta mem t
norm delta mem t
(* Merging of constraints. *)
module TypeCache = struct
......@@ -617,22 +617,29 @@ exception FoundApply of t * int * int * Types.t Var.Map.map list
let apply_raw delta s t =
(*GlobalMemo.clear global_memo;*)
let vgamma = Var.mk "Gamma" in
let gamma = var vgamma in
let cgamma = cons gamma in
(* cell i of ai contains /\k<=i s_k, cell j of aj contains /\k<=j t_k *)
let ai = ref [||] and aj = ref [||] in
let tallying i j =
try
let s = get ai i in
let t = arrow (cons (get aj j)) cgamma in
let targ = get aj j in
let s = Subst.refresh delta s in
let targ = Subst.refresh delta targ in
let vgamma = Var.mk "Gamma" in
let gamma = var vgamma in
let cgamma = cons gamma in
let t = arrow (cons targ) cgamma in
let sl = tallying delta [ (s, t) ] in
let new_res =
List.fold_left
(fun tacc si -> cap tacc (Subst.apply_full si gamma))
(fun tacc si ->
let tres = Subst.apply_full si gamma in
let tres = Subst.refresh delta tres in
let tres = Subst.clean_type delta tres in
cap tacc tres)
any sl
in
let new_res = Subst.clean_type delta new_res in
(* let new_res = Subst.clean_type delta new_res in*)
raise (FoundApply (new_res, i, j, sl))
with
......@@ -659,7 +666,14 @@ let apply_raw delta s t =
done;
tallying i i;
loop (i + 1)
with FoundApply (res, i, j, sl) -> (sl, get ai i, get aj j, res)
with FoundApply (res, i, j, sl) ->
( sl,
get ai i,
get aj j,
let vars = Subst.vars res in
let vars = Var.Set.diff vars delta in
let mapping = Var.full_renaming vars in
Subst.apply_full (Var.Map.map Types.var mapping) res )
in
loop 0
......
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