Several instances of the same bug fixed at once: when processing a Fix,

[helm.git] / helm / software / components / cic_acic / cic2acic.ml

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index e1c964c76073ac21388a1abf79ee9968c0c45e23..98b14298274542288534df848c3bedf4303fa78d 100644 (file)
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -135,7 +135,6 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
    prerr_endline
     ("++++++++++++ Tempi della double_type_of: "^ string_of_float (time2 -. time1)) ;
 *)
-    let time = ref 0. in
     let rec aux computeinnertypes father context idrefs tt =
      let fresh_id'' = fresh_id' father tt in
      (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
@@ -302,12 +301,19 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
                (fresh_id'',n, aux' context idrefs s,
                 aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
           | C.LetIn (n,s,t) ->
-             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
-             if innersort = `Prop then
-              add_inner_type fresh_id'' ;
-             C.ALetIn
-              (fresh_id'', n, aux' context idrefs s,
-               aux' ((Some (n, C.Def(s,None)))::context) (fresh_id''::idrefs) t)
+             let s_ty =
+              try
+               (cic_CicHash_find terms_to_types s).D.synthesized
+              with
+               Not_found ->
+                cicReduction_whd context (xxx_type_of_aux' metasenv context s);
+             in
+              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
+              if innersort = `Prop then
+               add_inner_type fresh_id'' ;
+              C.ALetIn
+               (fresh_id'', n, aux' context idrefs s,
+                aux' ((Some (n, C.Def(s,Some s_ty)))::context) (fresh_id''::idrefs) t)
           | C.Appl l ->
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = `Prop then
@@ -347,8 +353,12 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
              let fresh_idrefs =
               List.map (function _ -> gen_id seed) funs in
              let new_idrefs = List.rev fresh_idrefs @ idrefs in
-             let tys =
-              List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs
+             let tys,_ =
+               List.fold_left
+                 (fun (types,len) (n,_,ty,_) ->
+                    (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                     len+1)
+                ) ([],0) funs
              in
               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
               if innersort = `Prop then
@@ -364,8 +374,12 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
              let fresh_idrefs =
               List.map (function _ -> gen_id seed) funs in
              let new_idrefs = List.rev fresh_idrefs @ idrefs in
-             let tys =
-              List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs
+             let tys,_ =
+               List.fold_left
+                 (fun (types,len) (n,ty,_) ->
+                    (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                     len+1)
+                ) ([],0) funs
              in
               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
               if innersort = `Prop then
@@ -386,9 +400,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
            ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ;
           res
 *)
-  let res = aux global_computeinnertypes None context idrefs t in
-  prerr_endline (">>>> aux : " ^ string_of_float !time);
-  res
+  aux global_computeinnertypes None context idrefs t
 ;;
 
 let acic_of_cic_context ~computeinnertypes metasenv context idrefs t =
@@ -477,7 +489,7 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
       ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
 ;;
 
-let acic_object_of_cic_object ?(eta_fix=true) obj =
+let acic_object_of_cic_object ?(eta_fix=false) obj =
  let module C = Cic in
  let module E = Eta_fixing in
   let ids_to_terms = Hashtbl.create 503 in
@@ -502,7 +514,7 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
    let aobj =
     match obj with
       C.Constant (id,Some bo,ty,params,attrs) ->
-       let bo' = eta_fix [] [] bo in
+       let bo' = (*eta_fix [] []*) bo in
        let ty' = eta_fix [] [] ty in
        let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in
        let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
@@ -559,8 +571,8 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
              = aconjecture_of_conjecture' conjectures conjecture in
            (cid,i,acanonical_context,aterm))
           conjectures' in 
-(*        let time1 = Sys.time () in *)
-       let bo' = eta_fix conjectures' [] bo in
+       (* let bo' = eta_fix conjectures' [] bo in *)
+       let bo' = bo in
        let ty' = eta_fix conjectures' [] ty in
 (*
        let time2 = Sys.time () in
@@ -683,9 +695,12 @@ let plain_acic_term_of_cic_term =
       C.AMutCase (fresh_id, uri, tyno, aux context outty,
        aux context term, List.map (aux context) patterns)
    | C.Fix (funno, funs) ->
-      let tys =
-       List.map
-        (fun (name,_,ty,_) -> mk_fresh_id (), Some (C.Name name, C.Decl ty)) funs
+      let tys,_ =
+        List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+            (mk_fresh_id (),(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types,
+              len+1
+         ) ([],0) funs
       in
        C.AFix (fresh_id, funno,
         List.map2
@@ -694,9 +709,12 @@ let plain_acic_term_of_cic_term =
          ) tys funs
       )
    | C.CoFix (funno, funs) ->
-      let tys =
-       List.map (fun (name,ty,_) ->
-        mk_fresh_id (),Some (C.Name name, C.Decl ty)) funs
+      let tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+            (mk_fresh_id (),(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types,
+              len+1
+         ) ([],0) funs
       in
        C.ACoFix (fresh_id, funno,
         List.map2