another bug corrected in explicit_polymorphism. slightly enhanced examples/list.why

examples/list.why

@@ -4,9 +4,9 @@ theory Induction2
 
   logic p ('a list, 'b list)
 
-  axiom Induction : 
-    p(Nil : 'a list, Nil : 'b list) -> 
-    (forall x1:'a, x2:'b, l1:'a list, l2:'b list. 
+  axiom Induction :
+    p(Nil : 'a list, Nil : 'b list) ->
+    (forall x1:'a, x2:'b, l1:'a list, l2:'b list.
        p(l1, l2) -> p(Cons(x1,l1), Cons(x2,l2))) ->
     forall l1:'a list, l2:'b list. length(l1)=length(l2) -> p(l1, l2)
 
@@ -31,12 +31,17 @@ theory Test1
 
   clone Induction2 with logic p = foo
 
-  goal G3 : forall l1: 'a list, l2 : 'b list. 
+  lemma G3 : forall l1: 'a list, l2 : 'b list.
     length(l1) = length(l2) ->
     length(zip(l1, l2)) = length(l1)
 
-  goal G4 : zip(Cons(1, Cons(2, Nil)), 
-                Cons(1., Cons(2., Nil))) = 
+  goal G4 : zip(Cons(1, Cons(2, Nil)),
+                Cons(1., Cons(2., Nil))) =
                 Cons ((1, 1.), Cons((2, 2.), Nil))
 
+  goal G5 : forall l1: 'a list, l2 : 'b list, l3: 'c list, l4: 'd list.
+    length(l1) = length(l2) and length(l2) = length(l3) and
+      length(l3) = length(l4) ->
+    length(zip(zip(l1,l2), zip(l3, l4))) = length(l3)
+
 end

src/transform/explicit_polymorphism.ml

@@ -141,13 +141,13 @@ module Utils = struct
   to types in [right]. [tv_to_ty] is a mapping given in argument.
   It must be compliant with the unification between [left] and [right] *)
   let rec find_matching_vars tv_to_ty left right =
-    (* Format.eprintf "matching @[%a@] with @[%a@]@."
+    (*Format.eprintf "matching @[%a@] with @[%a@]@."
       (Debug.print_list Pretty.print_ty) left
-      (Debug.print_list Pretty.print_ty) right; *)
+      (Debug.print_list Pretty.print_ty) right;*)
     assert (List.length left = List.length right);
     let tv_to_ty = List.fold_left2 ty_match tv_to_ty left right in
-    (* Format.eprintf "gives @[%a@]@."
-      (Debug.print_mtv Pretty.print_ty) tv_to_ty; flush stderr; *)
+    (*Format.eprintf "gives @[%a@]@."
+      (Debug.print_mtv Pretty.print_ty) tv_to_ty; flush stderr;*)
     tv_to_ty
 
   module Mint = Map.Make(struct
@@ -196,8 +196,8 @@ module Transform = struct
       let new_ty = List.map (const my_t) new_ty in
       let all_new_ty = new_ty @ lsymbol.ls_args in
       let new_lsymbol =
-	      Term.create_lsymbol (id_clone lsymbol.ls_name)
-	        all_new_ty lsymbol.ls_value in
+        Term.create_lsymbol (id_clone lsymbol.ls_name)
+          all_new_ty lsymbol.ls_value in
       new_lsymbol
 
   (** creates a lsymbol associated with the given tysymbol *)
@@ -240,7 +240,7 @@ module Transform = struct
 
 
   (** translation of terms *)
-  let rec term_transform tblT tblL varM tv_to_ty t = match t.t_node with
+  let rec term_transform tblT tblL varM t = match t.t_node with
     | Tapp(f, terms) ->
       let new_f = findL tblL f in
       (* first, remember an order for type vars of new_f *)
@@ -252,7 +252,7 @@ module Transform = struct
       let concrete_ty = List.map (fun x-> x.t_ty) terms in
       let result_to_match = fromSome new_f.ls_value in
       let result_ty = t.t_ty in
-      let tv_to_ty = find_matching_vars tv_to_ty
+      let tv_to_ty = find_matching_vars Mtv.empty
         (result_to_match :: args_to_match) (result_ty :: concrete_ty) in
       (* Debug.print_mtv Pretty.print_ty Format.err_formatter tv_to_ty; *)
       (* fresh terms to be added at the beginning of the list of arguments *)
@@ -260,14 +260,14 @@ module Transform = struct
       let new_ty = List.map (fun x -> Mint.find x int_to_tyvars) new_ty_int in
       let new_terms = List.map (ty_to_term tblT varM tv_to_ty) new_ty in
       let transformed_terms = List.map
-        (term_transform tblT tblL varM tv_to_ty) terms in
+        (term_transform tblT tblL varM) terms in
       let transformed_result = ty_to_ty tv_to_ty (fromSome new_f.ls_value) in
       t_app new_f (new_terms @ transformed_terms) transformed_result
       | _ -> (* default case : traverse *)
-        t_map (term_transform tblT tblL varM tv_to_ty)
-          (fmla_transform tblT tblL varM tv_to_ty) t
+        t_map (term_transform tblT tblL varM)
+          (fmla_transform tblT tblL varM) t
   (** (trivial) translation of formulae *)
-  and fmla_transform tblT tblL varM tv_to_ty f = match f.f_node with
+  and fmla_transform tblT tblL varM f = match f.f_node with
     | Fapp(p,terms) when (not (ls_equal p ps_equ)) && not(ls_equal p ps_neq) ->
       let new_p = findL tblL p in
       (* first, remember an order for type vars of new_f *)
@@ -277,7 +277,7 @@ module Transform = struct
       (* match types *)
       let args_to_match = drop (List.length type_vars) new_p.ls_args in
       let concrete_ty = List.map (fun x-> x.t_ty) terms in
-      let tv_to_ty = find_matching_vars tv_to_ty
+      let tv_to_ty = find_matching_vars Mtv.empty
          args_to_match concrete_ty in
       (* Debug.print_mtv Pretty.print_ty Format.err_formatter tv_to_ty; *)
       (* fresh terms to be added at the beginning of the list of arguments *)
@@ -285,11 +285,11 @@ module Transform = struct
       let new_ty = List.map (fun x -> Mint.find x int_to_tyvars) new_ty_int in
       let new_terms = List.map (ty_to_term tblT varM tv_to_ty) new_ty in
       let transformed_terms = List.map
-        (term_transform tblT tblL varM tv_to_ty) terms in
+        (term_transform tblT tblL varM) terms in
       f_app new_p (new_terms @ transformed_terms)
     | _ ->
-      f_map (term_transform tblT tblL varM tv_to_ty)
-        (fmla_transform tblT tblL varM tv_to_ty) f
+      f_map (term_transform tblT tblL varM)
+        (fmla_transform tblT tblL varM) f
   
 
 
@@ -334,7 +334,7 @@ module Transform = struct
     (* Debug.print_mty Pretty.print_vs Format.err_formatter varM;
     Format.eprintf "-----------@."; *)
     (*universal quantification over ty vars*)
-    let new_fmla = (fmla_transform tblT tblL varM Mtv.empty fmla) in
+    let new_fmla = (fmla_transform tblT tblL varM fmla) in
     let quantified_fmla = f_forall (map_values varM) [] new_fmla in
     [Decl.create_prop_decl prop_kind prop_name quantified_fmla]
 
@@ -346,14 +346,14 @@ end
 symbols) and a declaration, and returns the corresponding declaration in
 explicit polymorphism logic. *)
 let decl_transform tblT tblL d =
-  (*Format.eprintf "%a@." Pretty.print_decl d; *)
+  (*Format.eprintf "%a@." Pretty.print_decl d;*)
   let result = match d.d_node with
     | Dind _inds ->
     failwith "Dind : should not have inductives declarations at this point !"
     | Dtype tys -> Transform.type_transform tblT tys
     | Dlogic decls -> Transform.logic_transform tblL decls
     | Dprop prop -> Transform.prop_transform tblT tblL prop in
-  (* Format.eprintf "===@.%a@.@." (Debug.print_list Pretty.print_decl) result;*)
+  (*Format.eprintf "===@.%a@.@." (Debug.print_list Pretty.print_decl) result;*)
   result