Commit 2ee30016 authored by Kim Nguyễn's avatar Kim Nguyễn

Do not add constraints of the form s <= 'a <= t, for monomorphic alpha's, just...

Do not add constraints of the form s <= 'a <= t, for monomorphic alpha's, just check that the constraint holds for all substitution and replace it with a universal Sat or Unsat. This prevent the algorithm from introducing dummy substitutions later on of the form 'a <- 'a which interact badly with type cleaning (replacing covariant/contra-variant occurences by Empty/Any).
parent a023197b
...@@ -215,12 +215,11 @@ let toplevel ...@@ -215,12 +215,11 @@ let toplevel
delta norm_rec mem lpos lneg delta norm_rec mem lpos lneg
= =
let singleton x ((t, s) as cst) = let singleton x ((t, s) as cst) =
(* constraints over monomorphic variables must be trivial, if Var.Set.mem delta x then
that is true for all substitutions let vx = var x in
*) if subtype t vx && subtype vx s then
let vx = var x in ConstrSet.sat
if Var.Set.mem delta x && (not (subtype t vx) || not (subtype vx s)) else ConstrSet.unsat
then ConstrSet.unsat
else ConstrSet.singleton x cst else ConstrSet.singleton x cst
in in
let var_compare v1 v2 = let var_compare v1 v2 =
...@@ -241,8 +240,6 @@ let toplevel ...@@ -241,8 +240,6 @@ let toplevel
singleton x (empty, t) singleton x (empty, t)
| (`Var x)::pos, (`Var y)::neg -> | (`Var x)::pos, (`Var y)::neg ->
DEBUG toplevel (Format.eprintf
"@[ - pos/neg case = %a, %a @]@\n" Var.print x Var.print y);
if var_compare x y < 0 then if var_compare x y < 0 then
let t = single (module V) true x pos lneg in let t = single (module V) true x pos lneg in
singleton x (empty, t) singleton x (empty, t)
......
...@@ -3241,9 +3241,14 @@ struct ...@@ -3241,9 +3241,14 @@ struct
let clean_type delta t = let clean_type delta t =
if no_var t then t else if no_var t then t else
let _tlv,pos, neg, all = Variable.collect_vars t in let _tlv,pos, neg, all = Variable.collect_vars t in
DEBUG clean_type (Format.eprintf " - for type %a pos: %a, neg: %a, all: %a, tlv: %a@\n" DEBUG clean_type (Format.eprintf " - for type %a pos: %a, neg: %a, all: %a, tlv: %a, delta: %a@\n"
Print.pp_type t Print.pp_type t
Var.Set.print pos Var.Set.print neg Var.Set.print all Var.Set.print _tlv); Var.Set.print pos
Var.Set.print neg
Var.Set.print all
Var.Set.print _tlv
Var.Set.print delta
);
let vars = Var.Set.diff all delta in let vars = Var.Set.diff all delta in
if Var.Set.is_empty vars then t else if Var.Set.is_empty vars then t else
let subst = Map.init let subst = Map.init
......
...@@ -41,7 +41,7 @@ module V = struct ...@@ -41,7 +41,7 @@ module V = struct
let is_internal x = x.kind == Internal let is_internal x = x.kind == Internal
let ident x = Ident.U.get_str x.name let ident x = Ident.U.get_str x.name
let print ppf x = Format.fprintf ppf "'%a" Ident.U.print x.name let print ppf x = Format.fprintf ppf "'%a_%i_%a" Ident.U.print x.name x.id print_kind x.kind
end end
......
...@@ -1253,6 +1253,17 @@ and type_check' loc env ed constr precise = match ed with ...@@ -1253,6 +1253,17 @@ and type_check' loc env ed constr precise = match ed with
end end
end end
in in
DEBUG typer_apply (Format.eprintf "@[<hov 2> Typing function application:@\n\
delta: %a@\n\
function: %a@\n\
argument: %a@\n\
result: %a@\n\
substtitution: %a @]@\n%!"
Var.Set.print env.delta
Types.Print.pp_type t1
Types.Print.pp_type t2
Types.Print.pp_type res
Type_tallying.pp_sl sl);
let e = exp' loc ed in let e = exp' loc ed in
e.exp_typ <- res; e.exp_typ <- res;
(Subst(e,sl),verify loc res constr) (Subst(e,sl),verify loc res 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