Merge branch 'master' of https://git.cduce.org/cduce

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@." 

tests/libtest/typesTest.ml

@@ -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
 ;;

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 *)

types/types.ml

@@ -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)

types/types.mli

@@ -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,

typing/typer.ml

@@ -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
@@ -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 ->
@@ -951,8 +955,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 dom = Types.Arrow.domain(t1arrow) in
       let res = 
@@ -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