Commit d4423e44 authored by Pietro Abate's avatar Pietro Abate

Add Types.is_squaresubtype

parent 3f1ff11d
......@@ -138,7 +138,7 @@ let test_squaresubtype =
let t1 = parse_typ s in
let t2 = parse_typ t in
let delta = List.fold_left (fun acc v -> Var.Set.add (Var.mk v) acc) Var.Set.empty delta in
assert_equal (snd(Types.squaresubtype delta t1 t2)) expected
assert_equal (Types.is_squaresubtype delta t1 t2) expected
)
) squaresubtype_tests
;;
......
......@@ -3356,6 +3356,8 @@ let squaresubtype delta s t =
in
loop 0
let is_squaresubtype delta s t = snd(squaresubtype delta s t)
exception FoundApply of t * int * int * Tallying.CS.sl
(** find two sets of type substitutions I,J such that
......@@ -3406,7 +3408,6 @@ let apply_raw delta s t =
let apply_full delta s t =
let _,_,_,res = apply_raw delta s t in
(* Format.printf "result: %a@\n@." Print.print res; *)
res
let squareapply delta s t = let s,_,_,res = apply_raw delta s t in (s,res)
......@@ -452,6 +452,7 @@ end
True if there exists a substitution such that s < t only
considering variables that are not in delta *)
val squaresubtype : Var.Set.t -> t -> t -> (Tallying.CS.sl * bool)
val is_squaresubtype : Var.Set.t -> t -> t -> bool
(** apply_raw s t returns the 4-tuple (subst,ss, tt, res) where
subst is the set of substitution that make the application succeed,
......
......@@ -822,7 +822,7 @@ let verify loc t s =
t
let squareverify loc delta t s =
if not (snd(Types.squaresubtype delta t s)) then
if not (Types.is_squaresubtype delta t s) then
raise_loc loc (Constraint (t, s));
t
......@@ -877,7 +877,7 @@ and type_check' loc env ed constr precise = match ed with
let t =
(* try Types.Arrow.check_strenghten a.fun_typ constr *)
try begin
if snd(Types.squaresubtype env.delta a.fun_typ constr) then a.fun_typ
if Types.is_squaresubtype env.delta a.fun_typ constr then a.fun_typ
else raise Not_found
end with Not_found ->
should_have loc constr
......
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