Minor API change : Patterns.Print.print -> Patterns.Print.pp

compile/compile.ml

@@ -123,7 +123,7 @@ and compile_aux env = function
       let v = find x env in
       let ts = Types.all_vars (Types.descr (IdMap.assoc x env.gamma)) in
       let is_mono () =
-	let from_xi = try IdMap.assoc x env.xi with Not_found -> Var.Set.empty in
+	let from_xi = try IdMap.assoc x env.xi with Not_found -> assert false in
         let d = Var.Set.inter from_xi (domain(env.sigma)) in
         Var.Set.is_empty (Var.Set.inter ts d)
       in

driver/cduce.ml

@@ -200,7 +200,7 @@ let debug ppf tenv cenv = function
       and p = Typer.pat tenv p in
       Format.fprintf ppf "[DEBUG:filter t=%a p=%a]@."
 	Types.Print.pp_type (Types.descr t)
-	Patterns.Print.print (Patterns.descr p);
+	Patterns.Print.pp (Patterns.descr p);
       let f = Patterns.filter (Types.descr t) p in
       IdMap.iteri (fun x t ->
 		   Format.fprintf ppf " %a:%a@." 

types/patterns.ml

@@ -266,7 +266,7 @@ module Print = struct
 	Format.fprintf ppf "(%a:=%a)" Ident.print x Types.Print.pp_const c
     | Dummy -> assert false
       
-  let print ppf p =
+  let pp ppf p =
     mark S.empty p;
     print ppf p;
     let first = ref true in
@@ -284,7 +284,6 @@ module Print = struct
     names := M.empty;
     printed := S.empty
 
-
   let print_xs ppf xs =
     Format.fprintf ppf "{";
     let rec aux = function
@@ -294,6 +293,9 @@ module Print = struct
     in
     aux xs;
     Format.fprintf ppf "}"
+
+  let printf = pp Format.std_formatter
+  let string_of_pattern t = Utils.string_of_formatter pp t
 end
 
 let () = print_node := (fun ppf n -> Print.print ppf (descr n))

types/patterns.mli

@@ -31,7 +31,9 @@ val pp_node : Format.formatter -> node -> unit
 (* Pretty-printing *)
 
 module Print : sig
-  val print: Format.formatter -> descr -> unit
+  val pp: Format.formatter -> descr -> unit
+  val printf: descr -> unit
+  val string_of_pattern : descr -> string
 end
 
 (* Pattern matching: static semantics *)

typing/typer.ml

@@ -890,7 +890,11 @@ and type_check' loc env ed constr precise = match ed with
       (* 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
+        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 ->
@@ -950,8 +954,11 @@ and type_check' loc env ed constr precise = match ed with
       let t1 = Types.Positive.substitutefree t1 in
 
       (* t [_delta 0 -> 1 *)
-      begin try ignore(Types.Tallying.tallying ~delta:env.delta [(t1,Types.Arrow.any)])
-      with Types.Tallying.UnSatConstr _ -> raise_loc loc (Constraint (t1, Types.Arrow.any)) end;
+      begin try 
+        ignore(Types.Tallying.tallying ~delta:env.delta [(t1,Types.Arrow.any)])
+      with Types.Tallying.UnSatConstr _ ->
+        raise_loc loc (Constraint (t1, Types.Arrow.any))
+      end;
 
       let t1arrow = Types.Arrow.get t1 in
       let dom = Types.Arrow.domain(t1arrow) in
@@ -1147,12 +1154,15 @@ and branches_aux loc env targ tres constr precise = function
 
       let targ' = Types.cap targ acc in
       if Types.is_empty targ' then
+        (* this branch cannot be selected: we ignore it *)
         branches_aux loc env targ tres constr precise rem
       else begin
         b.br_used <- true;
 	  let res = Patterns.filter targ' p in (* t^i_j // p_j *)
         (* update gamma \Gamma, t^i_j // p_j*)
-        let env = { env with gamma = IdMap.merge (fun _ v2 -> v2) env.gamma res } in
+        let env = { env with 
+          gamma = IdMap.merge (fun _ v2 -> v2) env.gamma res } 
+        in
 	  let res = IdMap.map Types.descr res in
 	  
 	  b.br_vars_empty <-
@@ -1167,13 +1177,15 @@ and branches_aux loc env targ tres constr precise = function
         let xj =
           IdMap.fold (fun x t acc ->
             let s = Var.Set.diff (Types.all_vars t) env'.delta in
-            if not(Var.Set.is_empty s) then IdMap.add x s acc else acc
+            IdMap.add x s acc
           ) res IdMap.empty
         in
-        (* all poly variables associated with the pattern p_j that are not in \Delta *)
+        (* all polymorphic variables not in \Delta associated with a term 
+         * variable x in p_j*)
         b.br_vars_poly <- xj;
 
 	  let t = type_check env' b.br_body constr precise in (* s_i^j *)
+        Format.printf "patt %a // %a" Patterns.Print.pp (Patterns.descr p) Types.Print.pp_type t;
 	  let tres = if precise then Types.cup t tres else tres in
 	  let targ'' = Types.diff targ acc in
 	  if (Types.non_empty targ'') then