Commit 3517a2b3 authored by Pietro Abate's avatar Pietro Abate
Browse files

Compte delta in abstr-inf

parent d8f4a2b7
......@@ -3395,7 +3395,7 @@ exception FoundSquareSub of Tallying.CS.sl * bool
let squaresubtype delta s t =
DescrHash.clear Tallying.memo_norm;
assert (Var.Set.is_empty (all_vars t));
assert (Var.Set.is_empty (Var.Set.diff (all_vars t) delta));
let ai = ref [| |] in
let tallying i =
try
......
......@@ -822,9 +822,7 @@ let require loc t s =
if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
let verify loc t s =
Format.printf "VERIFY %a < %a\n" Types.Print.print t Types.Print.print s;
require loc t s;
Format.printf "VERIFY TRUE \n";
t
let verify_noloc t s =
......@@ -887,6 +885,18 @@ and type_check' loc env ed constr precise = match ed with
in
(* update \delta with all variables in t1 -> t2 *)
let deltaintf =
let union (t1,t2) = Var.Set.union (Types.all_vars(t1)) (Types.all_vars(t2)) in
match a.fun_iface with
|[] -> Var.Set.empty
|head::tail ->
List.fold_left (fun acc inf ->
Var.Set.inter (union inf) acc
) (union head) tail
in
let env = {env with delta = Var.Set.union env.delta deltaintf } in
(* I check the body with all possible t1 -> t2 types *)
let sll =
List.fold_left (fun tacc (t1,t2) ->
......
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