Improve the debugging of the unify step of the tallying. Fix a bug where...

Improve the debugging of the unify step of the tallying. Fix a bug where substitutions were applied in the wrong order, yielding partially empty types.

compile/lambda.ml

@@ -26,7 +26,7 @@ type iface = (Types.descr * Types.descr) list
 
 type sigma = 
   | Identity (* this is basically as Types.Tallying.CS.sat *)
-  | List of Types.t Type_tallying.VarMap.map list
+  | List of Types.Subst.t list
   | Comp of (sigma * sigma)
   | Sel of (var_loc * iface * sigma) 
 

compile/lambda.mli

@@ -26,7 +26,7 @@ type iface = (Types.t * Types.t) list
 
 type sigma = 
   | Identity
-  | List of Types.t Type_tallying.VarMap.map list
+  | List of  Types.Subst.t list
   | Comp of (sigma * sigma)
   | Sel of (var_loc * iface * sigma) 
 

misc/utils.ml

@@ -4,11 +4,13 @@ let string_of_formatter pp t =
   Format.flush_str_formatter ()
 
 let pp_list ?(delim=("[","]")) ?(sep=",") f ppf l =
-  let rec aux ppf = function
-    |[] -> Format.fprintf ppf ""
-    |[h] -> Format.fprintf ppf "%a" f h
-    |h::t -> Format.fprintf ppf "%a%s%a" f h sep aux t
+  let od, cd = delim in
+  let rec aux ppf =
+    function
+  [] -> Format.fprintf ppf ""
+    | [ h ] -> Format.fprintf ppf "%a@ " f h
+    | h::t -> Format.fprintf ppf "%a%s@ %a" f h sep aux t
   in
   match l with
-    |[] -> Format.fprintf ppf "%s%s" (fst delim) (snd delim)
-    |_ -> Format.fprintf ppf "%s%a%s" (fst delim) aux l (snd delim)
+    [] -> Format.fprintf ppf "%s%s" od cd
+  |_ -> Format.fprintf ppf "%s@ %a%s" od aux l cd

runtime/value.ml

@@ -3,7 +3,7 @@ open Encodings
 
 type iface = (Types.t * Types.t) list
 type sigma =
-  | List of Types.t Type_tallying.VarMap.map list
+  | List of Types.Subst.t list
   | Comp of (sigma * sigma)
   | Sel of (int * iface * sigma)
   | Identity

runtime/value.mli

@@ -3,7 +3,7 @@ open Encodings
 
 type iface = (Types.t * Types.t) list
 type sigma =
-  | List of Types.t Type_tallying.VarMap.map list
+  | List of Types.Subst.t list
   | Comp of (sigma * sigma)
   | Sel of (int * iface * sigma)
   | Identity

types/patterns.ml

@@ -1399,6 +1399,6 @@ module Compile = struct
     try
       make_branches t b
     with
-    FindCode -> make_branches (Types.Substitution.hide_vars t) b
+    FindCode -> make_branches (Types.Subst.hide_vars t) b
 
 end

types/type_tallying.ml

@@ -10,16 +10,8 @@ let cap_product any_left any_right l =
 
 exception UnSatConstr of string
 
-module VarMap = Var.Set.Map
-
-let pp_s ppf s =
-  Utils.pp_list ~delim:("{","}") (fun ppf -> fun (v,t) ->
-    Format.fprintf ppf "%a = %a@," Var.print v Print.pp_type t
-  ) ppf (VarMap.get s)
-
 let pp_sl ppf l =
-  
-  Utils.pp_list ~delim:("{","}") pp_s ppf l
+  Utils.pp_list ~delim:("{","}") Subst.print ppf l
 
 type constr = Types.t * Types.t (* lower and
 				   upper bounds *)
@@ -44,11 +36,11 @@ let compare_type t1 t2 =
 (* A line is a conjunction of constraints *)
 module Line = struct
 
-  type t = constr VarMap.map
+  type t = constr Var.Map.map
 
-  let singleton = VarMap.singleton
-  let is_empty = VarMap.is_empty
-  let length = VarMap.length
+  let singleton = Var.Map.singleton
+  let is_empty = Var.Map.is_empty
+  let length = Var.Map.length
 
     (* a set of constraints m1 subsumes a set of constraints m2,
        that is the solutions for m1 contains all the solutions for
@@ -58,18 +50,18 @@ module Line = struct
     *)
   let subsumes map1 map2 =
     List.for_all (fun (v,(i1, s1)) ->
-      try let i2, s2 = VarMap.assoc v map2 in
+      try let i2, s2 = Var.Map.assoc v map2 in
           subtype i1 i2 && subtype s2 s1
       with Not_found -> false
-    ) (VarMap.get map1)
+    ) (Var.Map.get map1)
 
   let print ppf map =
     Utils.pp_list ~delim:("{","}") (fun ppf (v, (i,s)) ->
       Format.fprintf ppf "%a <= %a <= %a" Print.pp_type i Var.print v Print.pp_type s
-    ) ppf (VarMap.get map)
+    ) ppf (Var.Map.get map)
 
   let compare map1 map2 =
-    VarMap.compare (fun (i1,s1) (i2,s2) ->
+    Var.Map.compare (fun (i1,s1) (i2,s2) ->
       let c = compare_type i1 i2 in
       if c == 0 then compare_type s1 s2
       else c) map1 map2
@@ -77,18 +69,18 @@ module Line = struct
   let add v (inf, sup) map =
     let new_i, new_s =
       try
-        let old_i, old_s = VarMap.assoc v map in
+        let old_i, old_s = Var.Map.assoc v map in
         cup old_i inf,
         cap old_s sup
       with
         Not_found -> inf, sup
     in
-    VarMap.replace v (new_i, new_s) map
+    Var.Map.replace v (new_i, new_s) map
 
-  let join map1 map2 = VarMap.fold add map1 map2
-  let fold = VarMap.fold
-  let empty = VarMap.empty
-  let for_all f m = List.for_all (fun (k,v) -> f k v) (VarMap.get m)
+  let join map1 map2 = Var.Map.fold add map1 map2
+  let fold = Var.Map.fold
+  let empty = Var.Map.empty
+  let for_all f m = List.for_all (fun (k,v) -> f k v) (Var.Map.get m)
 end
 
 module ConstrSet =
@@ -496,7 +488,7 @@ let solve delta s =
     let beta =
       var Var.(mk ~internal:true ("#" ^ (ident alpha)))
     in
-    VarMap.replace alpha (cap (cup s beta) t) acc
+    Var.Map.replace alpha (cap (cup s beta) t) acc
   in
   let extra_var t acc =
     if is_var t then
@@ -510,37 +502,55 @@ let solve delta s =
       let acc = extra_var t acc in
       let acc = extra_var s acc in
       add_eq alpha s t acc
-    ) m VarMap.empty
+    ) m Var.Map.empty
   in
   ConstrSet.fold (fun m acc -> (to_eq_set m) :: acc) s []
 
 let solve delta s =
   let res = solve delta s  in
-  DEBUG solve (Format.eprintf "Calling solve (%a, %a), got %a@\n%!" Var.Set.print delta ConstrSet.print s
+  DEBUG solve (Format.eprintf "Calling solve (%a, %a), got %a@\n%!"
+		 Var.Set.print delta ConstrSet.print s
 		 pp_sl res);
   res
 
-let unify (eq_set : Descr.t VarMap.map) =
+let () = Format.pp_set_margin Format.err_formatter 200
+
+let unify (eq_set : Descr.t Var.Map.map) =
   let rec loop eq_set accu =
-    if VarMap.is_empty eq_set then accu else
-      begin
-	let (alpha, t), eq_set' = VarMap.remove_min eq_set in
-	let x = Substitution.solve_rectype t alpha in
-	let eq_set' =
-          VarMap.map (fun s -> Substitution.single s (alpha,x)) eq_set'
-	in
-	let sigma = loop eq_set' (VarMap.replace alpha x accu) in
-	let t_alpha = Substitution.full x (VarMap.get sigma)  in
-	VarMap.replace alpha t_alpha sigma
-      end
+    DEBUG unify
+      (Format.eprintf "@[<hov 2>  Entering unify_loop @[(%a, %a)@]@\n"
+	 Subst.print eq_set Subst.print accu);
+    let res =
+      if Var.Map.is_empty eq_set then accu else
+	begin
+	  let (alpha, t), eq_set' = Var.Map.remove_min eq_set in
+	  DEBUG unify (Format.eprintf
+			 "@[<hov 2>- Choosing equation @[%a = %a@]@]@\n"
+			 Var.print alpha Types.Print.pp_type t);
+	  let x = Subst.solve_rectype t alpha in
+	  DEBUG unify (Format.eprintf
+			 "@[<hov 2>- Solving equation @[%a = %a@]@]@\n"
+			 Var.print alpha Types.Print.pp_type x);
+	  let eq_set' =
+            Var.Map.map (fun s -> Subst.single s (alpha,x)) eq_set'
+	  in
+	  let sigma = loop eq_set' (Var.Map.replace alpha x accu) in
+	  let t_alpha = Subst.full x sigma in
+	  DEBUG unify (Format.eprintf
+			 "@[<hov 2>- Applying substitution @[%a@] to @[%a@], @[<hov 4>got %a@]@]@\n"
+			 Subst.print sigma Print.pp_type x Print.pp_type t_alpha);
+	  Var.Map.replace alpha t_alpha sigma
+	end
+    in
+    DEBUG unify (Format.eprintf "Leaving unify_loop @[(%a, %a)@], @[<hov 4>got %a@]@]@\n"
+		   Subst.print eq_set Subst.print accu Subst.print res);
+    res
   in
-  loop VarMap.empty eq_set
-
-let unify eq_set =
-  let res = unify eq_set in
-  DEBUG unify (Format.eprintf "Calling unify (%a), got %a@\n%!" pp_s eq_set pp_s res);
+  let res = loop eq_set Var.Map.empty in
+  DEBUG unify (Format.(pp_print_flush err_formatter ()));
   res
 
+
 exception Step1Fail
 exception Step2Fail
 
@@ -566,12 +576,12 @@ let tallying delta l =
 
 
 type symsubst = I
-		| S of Descr.t VarMap.map
+		| S of Descr.t Var.Map.map
 		| A of (symsubst * symsubst)
 
 let rec dom = function
   |I -> Var.Set.empty
-  |S si -> VarMap.domain si
+  |S si -> Var.Map.domain si
   |A (si,sj) -> Var.Set.cup (dom si) (dom sj)
 
 (* composition of two symbolic substitution sets sigmaI, sigmaJ .Cartesian product *)
@@ -584,8 +594,8 @@ let (++) sI sJ =
   )
 
 let (>>) t s =
-  VarMap.fold (fun v t acc ->
-    Substitution.single acc (v, t)) s t
+  Var.Map.fold (fun v t acc ->
+    Subst.single acc (v, t)) s t
 
 (* apply a symbolic substitution si to a type t *)
 let (@@) t si =
@@ -610,23 +620,23 @@ let (@@) t si =
   aux t si
 
 let domain sl =
-  List.fold_left (fun acc si -> Var.Set.cup acc (VarMap.domain si)) Var.Set.empty sl
+  List.fold_left (fun acc si -> Var.Set.cup acc (Var.Map.domain si)) Var.Set.empty sl
 
 let codomain ll =
   List.fold_left (fun acc e ->
-    VarMap.fold (fun _ v acc ->
+    Var.Map.fold (fun _ v acc ->
       Var.Set.cup (all_vars v) acc
     ) e acc
   ) Var.Set.empty ll
 
-let is_identity = List.for_all (VarMap.is_empty)
-let identity = [VarMap.empty]
+let is_identity = List.for_all (Var.Map.is_empty)
+let identity = [Var.Map.empty]
 
 let filter f sl =
   if is_identity sl then sl else
     List.fold_left (fun acc si ->
-      let e = VarMap.filter (fun v _ -> f v) si in
-      if VarMap.is_empty e then acc else e::acc
+      let e = Var.Map.filter (fun v _ -> f v) si in
+      if Var.Map.is_empty e then acc else e::acc
     ) [] sl
 
 
@@ -642,7 +652,7 @@ let set a i v =
   end
 let get a i = if i < 0 then any else (!a).(i)
 
-exception FoundSquareSub of Descr.t VarMap.map list
+exception FoundSquareSub of Descr.t Var.Map.map list
 
 let squaresubtype delta s t =
   NormMemoHash.clear memo_norm;
@@ -660,7 +670,7 @@ let squaresubtype delta s t =
     try
       let ss =
         if i = 0 then s
-        else (cap (Substitution.freshen delta s) (get ai (i-1)))
+        else (cap (Subst.freshen delta s) (get ai (i-1)))
       in
       set ai i ss;
       tallying i;
@@ -672,7 +682,7 @@ let squaresubtype delta s t =
 let is_squaresubtype delta s t =
   try ignore(squaresubtype delta s t);true with UnSatConstr _ -> false
 
-exception FoundApply of t * int * int * Descr.t VarMap.map list
+exception FoundApply of t * int * int * Descr.t Var.Map.map list
 
 (** find two sets of type substitutions I,J such that
     s @@ sigma_i < t @@ sigma_j for all i \in I, j \in J *)
@@ -697,9 +707,9 @@ let apply_raw delta s t =
       let t = arrow (cons (get aj j)) cgamma in
       let sl = tallying delta [ (s,t) ] in
       let new_res =
-        Substitution.clean_type delta (
+        Subst.clean_type delta (
           List.fold_left (fun tacc si ->
-            cap tacc (gamma >> si)
+            cap tacc (Subst.full gamma  si)
           ) any sl
         )
       in
@@ -713,8 +723,8 @@ let apply_raw delta s t =
       (* Format.printf "Starting expansion %i @\n@." i; *)
       let (ss,tt) =
         if i = 0 then (s,t) else
-          ((cap (Substitution.freshen delta s) (get ai (i-1))),
-           (cap (Substitution.freshen delta t) (get aj (i-1))))
+          ((cap (Subst.freshen delta s) (get ai (i-1))),
+           (cap (Subst.freshen delta t) (get aj (i-1))))
       in
       set ai i ss;
       set aj i tt;
@@ -741,4 +751,3 @@ let apply_full delta s t =
   res
 
 let squareapply delta s t = let s,_,_,res = apply_raw delta s t in (s,res)
-

types/type_tallying.mli

@@ -3,14 +3,12 @@ open Types
 
 exception UnSatConstr of string
 
-module VarMap : module type of Var.Set.Map
-
-val (>>) : t -> Descr.t VarMap.map -> t
+val (>>) : t -> Types.Subst.t -> t
 
   (** Symbolic Substitution Set *)
 type symsubst =
   |I (** Identity *)
-  |S of Descr.t VarMap.map (** Substitution *)
+  |S of Types.Subst.t (** Substitution *)
   |A of (symsubst * symsubst) (** Composition si (sj t) *)
 
   (** Cartesian Product of two symbolic substitution sets *)
@@ -19,19 +17,19 @@ val ( ++ ) : symsubst list -> symsubst list -> symsubst list
   (** Evaluation of a substitution *)
 val (@@) : t -> symsubst -> t
 
-val domain : Descr.t VarMap.map list -> Var.Set.t
-val codomain : Descr.t VarMap.map list -> Var.Set.t
-val is_identity : Descr.t VarMap.map list -> bool
-val identity : Descr.t VarMap.map list
-val filter : (Var.t -> bool) -> Descr.t VarMap.map list -> Descr.t VarMap.map list
+val domain : Types.Subst.t list -> Var.Set.t
+val codomain : Types.Subst.t list -> Var.Set.t
+val is_identity : Types.Subst.t list -> bool
+val identity : Types.Subst.t list
+val filter : (Var.t -> bool) -> Types.Subst.t list -> Types.Subst.t list
 
-val tallying : Var.Set.t -> (Types.t * Types.t) list ->
-  Types.t VarMap.map list
+val tallying : Var.Set.t -> (Types.t * Types.t) list -> Types.Subst.t list
+  
 
 (** Square Subtype relation. [squaresubtype delta s t] .
     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 -> Descr.t VarMap.map list
+val squaresubtype : Var.Set.t -> t -> t -> Types.Subst.t list
 val is_squaresubtype : Var.Set.t -> t -> t -> bool
 
 (** apply_raw s t returns the 4-tuple (subst,ss, tt, res) where
@@ -40,8 +38,8 @@ val is_squaresubtype : Var.Set.t -> t -> t -> bool
    and res is the type of the result of the application *)
 val apply_full : Var.Set.t -> t -> t -> t
 
-val apply_raw : Var.Set.t -> t -> t -> Descr.t VarMap.map list * t * t * t
+val apply_raw : Var.Set.t -> t -> t -> Types.Subst.t list * t * t * t
 
-val squareapply : Var.Set.t -> t -> t -> (Descr.t VarMap.map list * t)
+val squareapply : Var.Set.t -> t -> t -> (Types.Subst.t list * t)
 
-val pp_sl : Format.formatter -> Types.t VarMap.map list -> unit
+val pp_sl : Format.formatter -> Types.Subst.t list -> unit

types/types.ml

@@ -2727,7 +2727,7 @@ module Print = struct
       Format.pp_print_flush ppf ();
       Format.pp_set_formatter_output_functions ppf out_fun flush_fun
 
-
+  let wrap_formatter _ = fun () -> ()
   let pp_type ppf t =
     let reset = wrap_formatter ppf in
     pp_type ppf t;
@@ -3193,10 +3193,10 @@ module Positive = struct
 
 end
 
-module Substitution =
+module Subst =
 struct
-  module Map = Var.Set.Map
-  type t = Descr.t Map.map
+  type t = Descr.t Var.Map.map
+  module Map = Var.Map
 
   let identity = Map.empty
 
@@ -3212,8 +3212,9 @@ struct
     )
 
   let print ppf m =
-    Utils.pp_list (fun ppf (v, t) -> Format.fprintf ppf "%a:%a"
-                      Var.print v Print.pp_type t) ppf (Map.get m)
+    Utils.pp_list
+      ~delim:("{","}") (fun ppf (v, t) -> Format.fprintf ppf "%a←%a@,"
+	Var.print v Print.pp_type t) ppf (Map.get m)
 
   let add v t m =
     if is_var t && Var.(equal v (Set.choose (all_vars t))) then m
@@ -3296,10 +3297,14 @@ struct
 
 
   let full t l =
+    if no_var t then t else
+      app_subst t l
+
+  let full_list t l =
     if no_var t then t else
       app_subst t (of_list l)
 
-  let single t s = full t [s]
+  let single t s = full_list t [s]
 
   let freshen delta t =
     if no_var t then t else

types/types.mli

@@ -206,13 +206,17 @@ module Variable : sig
     val extract : t -> Var.t * bool
 end
 
-module Substitution : sig
-  val full : t -> (Var.t * t) list -> t
-  val single : t -> (Var.t * t) -> t
-  val freshen : Var.Set.t -> t -> t
-  val hide_vars : t -> t
-  val solve_rectype : t -> Var.t -> t
-  val clean_type : Var.Set.t -> t -> t
+module Subst : sig
+  type t = descr Var.Map.map
+  val identity : t
+  val print : Format.formatter -> t -> unit
+  val full : descr -> t -> descr
+  val full_list : descr -> (Var.t * descr) list -> descr
+  val single : descr -> (Var.t * descr) -> descr
+  val freshen : Var.Set.t -> descr -> descr
+  val hide_vars : descr -> descr
+  val solve_rectype : descr -> Var.t -> descr
+  val clean_type : Var.Set.t -> descr -> descr
 end
 
 

types/var.ml

@@ -52,6 +52,7 @@ module Set = struct
   let print ppf s = Utils.pp_list ~sep:";" ~delim:("{","}") V.print ppf (get s)
 end
 
+module Map = Set.Map
 
 include V
 let gen set =

types/var.mli

@@ -12,6 +12,8 @@ module Set : sig
   val dump : Format.formatter -> t -> unit
 end
 
+module Map : module type of Set.Map
+
 val gen : Set.t -> t
 
 type 'a var_or_atom = [ `Atm of 'a | `Var of t ]

typing/typed.ml

@@ -15,7 +15,7 @@ open Ident
 type tpat = Patterns.node
 type ttyp = Types.Node.t
 
-type sigma = Types.t Type_tallying.VarMap.map list
+type sigma = Types.Subst.t list
 
 type texpr  = 
     { exp_loc : loc; 

typing/typer.ml

@@ -548,7 +548,7 @@ module IType = struct
                 (Printf.sprintf "Wrong number of parameters for parametric type %s" (U.to_string id));
                  | Error s -> raise_loc_generic loc s
             in
-            mk_type (Types.Substitution.full t l)
+            mk_type (Types.Subst.full_list t l)
 	  with Not_found ->
             assert (rest == []);
             if args != [] then
@@ -623,7 +623,7 @@ module IType = struct
         in
         let sub_list = List.map (fun (v,vt) -> v, Types.var vt) vars_mapping in
         let t_rhs =
-          Types.Substitution.full t_rhs sub_list
+          Types.Subst.full_list t_rhs sub_list
         in
         let nargs = List.map2 (fun (_, v) (_, vt) -> v, vt) vars_mapping sub_list
         in
@@ -1140,8 +1140,8 @@ and type_check' loc env ed constr precise = match ed with
         (fun v ->
           let open Types in
           match v with
-          | Val t -> Val (Substitution.freshen env.delta t)
-          | EVal (a,b,t) ->  EVal (a,b,Substitution.freshen env.delta t)
+          | Val t -> Val (Subst.freshen env.delta t)
+          | EVal (a,b,t) ->  EVal (a,b,Subst.freshen env.delta t)
           | x -> x)
         env.ids }
     in
@@ -1217,7 +1217,7 @@ and type_check' loc env ed constr precise = match ed with
   | Apply (e1,e2) ->
     let t1 = type_check env e1 Types.Arrow.any true in
     let t1arrow = Types.Arrow.get t1 in
-    let t1 = Types.Substitution.freshen env.delta t1 in
+    let t1 = Types.Subst.freshen env.delta t1 in
       (* t [_delta 0 -> 1 *)
     begin try
             ignore(Type_tallying.tallying env.delta [(t1,Types.Arrow.any)])
@@ -1227,7 +1227,7 @@ and type_check' loc env ed constr precise = match ed with
 
     let dom = Types.Arrow.domain(t1arrow) in
     let t2 = type_check env e2 Types.any true in
-    let t2 = Types.Substitution.freshen env.delta t2 in
+    let t2 = Types.Subst.freshen env.delta t2 in
     let (sl,res) =
       if not (Types.no_var dom) ||
         not (Types.no_var t2) then