Few modif in eta-fixing.

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 21b39fe65209372c21cd6078fe205ce33084d18b..0933dbc4b88a573f09a30f1060e3bc14dadc1859 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -257,10 +257,10 @@ let generate_conversion seed top_down id inner_proof ~ids_to_inner_types =
               };
           }
         else
-          { K.proof_name = None ;
+          { K.proof_name =  inner_proof.K.proof_name;
             K.proof_id   = gen_id seed;
             K.proof_context = [] ;
-            K.proof_apply_context = [inner_proof];
+            K.proof_apply_context = [{inner_proof with K.proof_name = None}];
             K.proof_conclude = 
               { K.conclude_id = gen_id seed; 
                 K.conclude_aref = id;
@@ -436,15 +436,27 @@ build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
  let module K = Content in
   try
    let sort = Hashtbl.find ids_to_inner_sorts id in
+   (match name_of n with
+     Some "w" -> prerr_endline ("build_def: " ^ sort );
+   | _ -> ());
    if sort = "Prop" then
-      `Proof (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
+       (prerr_endline ("entro");
+       let p = 
+        (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
+       in 
+        (match p.K.proof_name with
+           Some "w" -> prerr_endline ("TUTTO BENE:");
+         | Some s -> prerr_endline ("mi chiamo " ^ s);
+         | _ -> prerr_endline ("ho perso il nome"););
+      prerr_endline ("esco"); `Proof p;)
    else 
+      (prerr_endline ("siamo qui???");
       `Definition
         { K.def_name = name_of n;
           K.def_id = gen_id seed; 
           K.def_aref = id;
           K.def_term = t
-        }
+        })
   with
    Not_found -> assert false
 
@@ -500,7 +512,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
         else raise Not_a_proof 
     | C.ALetIn (id,n,s,t) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then 
+        if sort = "Prop" then
           let proof = aux t in
           let proof' = 
             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
@@ -686,6 +698,10 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                with Not_found -> -1) in
       if n<0 then raise NotApplicable
       else 
+        let method_name =
+          if uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" then
+            "Exists"
+          else "ByInduction" in
         let prefix = String.sub uri_str 0 n in
         let ind_str = (prefix ^ ".ind") in 
         let ind_uri = UriManager.uri_of_string ind_str in
@@ -700,7 +716,10 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
           if n = 0 then ([],l) else
           let p,a = split (n-1) (List.tl l) in
           ((List.hd l::p),a) in
-        let params_and_IP,tail_args = split (noparams+1) args in 
+        let params_and_IP,tail_args = split (noparams+1) args in
+        if method_name = "Exists" then
+          (prerr_endline ("+++++args++++:" ^ string_of_int (List.length args));
+           prerr_endline ("+++++tail++++:" ^ string_of_int (List.length tail_args)));
         let constructors = 
             (match inductive_types with
               [(_,_,_,l)] -> l
@@ -767,14 +786,14 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                   hdarg::(build_method_args (tlc,tla))
               | _ -> assert false in
           build_method_args (constructors1,args_for_cases) in
-          { K.proof_name = None;
+          { K.proof_name = name;
             K.proof_id   = gen_id seed;
             K.proof_context = []; 
             K.proof_apply_context = serialize seed subproofs;
             K.proof_conclude = 
               { K.conclude_id = gen_id seed; 
                 K.conclude_aref = id;
-                K.conclude_method = "ByInduction";
+                K.conclude_method = method_name;
                 K.conclude_args =
                   K.Aux (string_of_int no_constructors) 
                   ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))
@@ -819,7 +838,7 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                     else K.Term a in
                 hd::(ma_aux (n-1) tl) in
           (ma_aux 3 args) in 
-          { K.proof_name = None;
+          { K.proof_name = name;
             K.proof_id   = gen_id seed;
             K.proof_context = []; 
             K.proof_apply_context = serialize seed subproofs;

diff --git a/helm/ocaml/cic_omdoc/contentPp.ml b/helm/ocaml/cic_omdoc/contentPp.ml
index 58ba4873b627bbed8d3bd7aef47ff0a2e815c500..3967c621668818fbb68b8e48fcd3e2bbc96e0b32 100644 (file)
--- a/helm/ocaml/cic_omdoc/contentPp.ml
+++ b/helm/ocaml/cic_omdoc/contentPp.ml
@@ -139,7 +139,17 @@ and parg indent =
     | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!")
 ;;
  
-let print_proof p = pproof p 0;
+let print_proof p = pproof p 0;;
+
+let print_obj (_,_,_,obj) =
+  match obj with 
+    `Decl (_,decl) -> 
+       pcontext_element 0 (decl:> Cic.annterm Content.in_proof_context_element)
+  | `Def (_,_,def) -> 
+       pcontext_element 0 (def:> Cic.annterm Content.in_proof_context_element)
+  | `Joint _ as jo -> pcontext_element 0 jo 
+;;
+
 
 
 

diff --git a/helm/ocaml/cic_omdoc/contentPp.mli b/helm/ocaml/cic_omdoc/contentPp.mli
index 85ce238f39f42043febe8e161cd9b7e90f8fb54a..a160ab1ff3b7eb9e61ca06b017a67748e7d3b9cc 100644 (file)
--- a/helm/ocaml/cic_omdoc/contentPp.mli
+++ b/helm/ocaml/cic_omdoc/contentPp.mli
@@ -25,4 +25,6 @@
 
 val print_proof: Cic.annterm Content.proof -> unit
 
+val print_obj: Cic.annterm Content.cobj -> unit
 
+val parg: int -> Cic.annterm Content.arg ->unit

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index c3b84b60599cd280f68b6a154e72825fb3d09257..8407f8357e04d3f7f8603759cbeb7432060d58b3 100644 (file)
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ b/helm/ocaml/cic_omdoc/eta_fixing.ml
@@ -27,83 +27,138 @@ exception ReferenceToVariable;;
 exception RferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
+(* 
 let rec fix_lambdas_wrt_type ty te =
  let module C = Cic in
  let module S = CicSubstitution in
-(*  prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); 
-   flush stderr ; *)
-   (* cast e altra porcheria ???? *)
+(*  prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
+   match ty with
+     C.Prod (_,_,ty') ->
+       (match CicReduction.whd [] te with
+          C.Lambda (n,s,te') ->
+            C.Lambda (n,s,fix_lambdas_wrt_type ty' te')
+        | t ->
+            let rec get_sources =
+              function 
+                C.Prod (_,s,ty) -> s::(get_sources ty)
+              | _ -> [] in
+            let sources = get_sources ty in
+            let no_sources = List.length sources in
+            let rec mk_rels n shift =
+              if n = 0 then []
+            else (C.Rel (n + shift))::(mk_rels (n - 1) shift) in
+            let t' = S.lift no_sources t in
+            let t2 = 
+              match t' with
+                C.Appl l -> 
+                  C.LetIn 
+                     (C.Name "w",t',C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
+              | _ -> 
+                  C.Appl (t'::(mk_rels no_sources 0)) in
+                   List.fold_right
+                     (fun source t -> C.Lambda (C.Name "y",source,t)) 
+                      sources t2)
+   | _ -> te
+;; *)
+
+let rec fix_lambdas_wrt_type ty te =
+ let module C = Cic in
+ let module S = CicSubstitution in
+(*  prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
+   match ty,te with
+     C.Prod (_,_,ty'), C.Lambda (n,s,te') ->
+       C.Lambda (n,s,fix_lambdas_wrt_type ty' te')
+   | C.Prod (_,s,ty'), t -> 
+      let rec get_sources =
+        function 
+            C.Prod (_,s,ty) -> s::(get_sources ty)
+          | _ -> [] in
+      let sources = get_sources ty in
+      let no_sources = List.length sources in
+      let rec mk_rels n shift =
+        if n = 0 then []
+        else (C.Rel (n + shift))::(mk_rels (n - 1) shift) in
+      let t' = S.lift no_sources t in
+      let t2 = 
+         match t' with
+           C.Appl l -> 
+             C.LetIn (C.Name "w",t',C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
+         | _ -> C.Appl (t'::(mk_rels no_sources 0)) in
+      List.fold_right
+        (fun source t -> C.Lambda (C.Name "y",CicReduction.whd [] source,t)) sources t2
+   | _, _ -> te
+;;
+
+(*
+let rec fix_lambdas_wrt_type ty te =
+ let module C = Cic in
+ let module S = CicSubstitution in
+(*  prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
    match ty,te with
      C.Prod (_,_,ty'), C.Lambda (n,s,te') ->
        C.Lambda (n,s,fix_lambdas_wrt_type ty' te')
+   | C.Prod (_,s,ty'), ((C.Appl (C.Const _ ::_)) as t) -> 
+      (* const have a fixed arity *)
+      (* prerr_endline ("******** fl - eta expansion 0: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
+       let t' = S.lift 1 t in
+       C.Lambda (C.Name "x",s,
+         C.LetIn 
+          (C.Name "H", fix_lambdas_wrt_type ty' t', 
+            C.Appl [C.Rel 1;C.Rel 2])) 
    | C.Prod (_,s,ty'), C.Appl l ->
-       prerr_endline ("******** fl - eta expansion 1: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); 
-       flush stderr ;
+       (* prerr_endline ("******** fl - eta expansion 1: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
        let l' = List.map (S.lift 1) l in
         C.Lambda (C.Name "x",s,
          fix_lambdas_wrt_type ty' (C.Appl (l'@[C.Rel 1])))
    | C.Prod (_,s,ty'), _ ->
-       prerr_endline ("******** fl - eta expansion 2: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); 
+       (* prerr_endline ("******** fl - eta expansion 2: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
        flush stderr ;
        let te' = S.lift 1 te in
         C.Lambda (C.Name "x",s,
           fix_lambdas_wrt_type ty' (C.Appl [te';C.Rel 1]))
    | _, _ -> te
-;;
+;;*) 
 
 let fix_according_to_type ty hd tl =
  let module C = Cic in
  let module S = CicSubstitution in
-  let rec aux ty tl res =
-   (* prerr_endline ("entering aux_1 with type=" ^ CicPp.ppterm ty); 
-   flush stderr ; *)
-   match ty with
-      C.Rel _
-    | C.Var _
-    | C.Meta _ 
-    | C.Sort _ 
-    | C.Implicit -> 
+   let rec count_prods =
+     function
+       C.Prod (_,_,t) -> 1 + (count_prods t)
+       | _ -> 0 in
+  let expected_arity = count_prods ty in
+  let rec aux n ty tl res =
+    if n = 0 then
       (match tl with 
          [] -> C.Appl res
-       |  _ ->
-         prerr_endline ("******* fat - too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); 
-         flush stderr ;
-         C.LetIn 
-          (C.Name "H", C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
-    | C.Cast (v,t) -> aux v tl res
-    | C.Prod (n,s,t) -> 
-       (match tl with 
-          [] ->
-            prerr_endline ("******* fat - eta expansion: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); 
-         flush stderr ;
-           let res' = List.map (S.lift 1) res 
-           in 
+       | _ -> 
+          match res with
+            [] -> assert false
+          | [a] -> C.Appl (a::tl)
+          | _ ->
+              (* prerr_endline ("******* too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); *)
+              C.LetIn 
+                (C.Name "H", 
+                  C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
+    else 
+      let name,source,target =
+        (match ty with
+           C.Prod (C.Name _ as n,s,t) -> n,s,t
+         | C.Prod (C.Anonymous, s,t) -> C.Name "z",s,t
+         | _ -> (* prods number may only increase for substitution *) 
+           assert false) in
+      match tl with 
+         [] ->
+           (* prerr_endline ("******* too few args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); *)
+           let res' = List.map (S.lift 1) res in 
            C.Lambda 
-            (C.Name "x", (* Andrea: to do: generate a fresh name *)
-             s, 
-             aux t [] (res'@[C.Rel 1]))
+            (name, source, aux (n-1) target [] (res'@[C.Rel 1]))
         | hd::tl' -> 
-           let hd' = fix_lambdas_wrt_type s hd
-           in
-            aux (S.subst hd' t) tl' (res@[hd']))
-    | C.Lambda _ -> assert false
-    | C.LetIn (n,s,t) -> aux (S.subst s t) tl res
-    | C.Appl _
-    | C.Const _
-    | C.MutInd _ 
-    | C.MutConstruct _
-    | C.MutCase _
-    | C.Fix _
-    | C.CoFix _ -> (* ???? *)
-       (match tl with 
-         [] -> C.Appl res
-       |  _ -> (* Andrea: to do: generate a fresh name *)
-         C.LetIn 
-          (C.Name "H",
-           C.Appl res, 
-           C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
-  in
-  aux ty tl [hd]
+           let hd' = fix_lambdas_wrt_type source hd in
+            (*  (prerr_endline ("++++++prima :" ^(CicPp.ppterm hd)); 
+              prerr_endline ("++++++dopo :" ^(CicPp.ppterm hd'))); *)
+           aux (n-1) (S.subst hd' target) tl' (res@[hd']) in
+  aux expected_arity ty tl [hd]
 ;;
 
 let eta_fix metasenv t =
@@ -139,7 +194,7 @@ let eta_fix metasenv t =
    | C.Prod (n,s,t) -> C.Prod (n, eta_fix' s, eta_fix' t)
    | C.Lambda (n,s,t) -> C.Lambda (n, eta_fix' s, eta_fix' t)
    | C.LetIn (n,s,t) -> C.LetIn (n, eta_fix' s, eta_fix' t)
-   | C.Appl l -> 
+   | C.Appl l as appl -> 
        let l' =  List.map eta_fix' l 
        in 
        (match l' with
@@ -152,7 +207,11 @@ let eta_fix metasenv t =
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
              )
            in
-           fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l''
+           let result = fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' in
+           if not (CicReduction.are_convertible [] appl result) then 
+             (prerr_endline ("prima :" ^(CicPp.ppterm appl)); 
+              prerr_endline ("dopo :" ^(CicPp.ppterm result)));
+           result
         | _ -> C.Appl l' )
    | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' =
@@ -189,3 +248,5 @@ let eta_fix metasenv t =
    eta_fix' t
 ;;
 
+
+