X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Fcic2acic.ml;h=c5bbfff78b34d658e347e817d84c0857d8b0aae5;hb=08e9d02504942642a917c0d3e4b4795e65172d89;hp=d8392f6206ab745e2647a75286e30745e481e18a;hpb=a5bbc4c69e8e8cd537a460a5f1899fd1c87b4c30;p=helm.git

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index d8392f620..c5bbfff78 100644
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -82,16 +82,16 @@ let fresh_id seed ids_to_terms ids_to_father_ids =
 
 let source_id_of_id id = "#source#" ^ id;;
 
-exception NotEnoughElements;;
+exception NotEnoughElements of string;;
 
 (*CSC: cut&paste da cicPp.ml *)
 (* get_nth l n   returns the nth element of the list l if it exists or *)
 (* raises NotEnoughElements if l has less than n elements             *)
-let rec get_nth l n =
+let rec get_nth msg l n =
  match (n,l) with
     (1, he::_) -> he
-  | (n, he::tail) when n > 1 -> get_nth tail (n-1)
-  | (_,_) -> raise NotEnoughElements
+  | (n, he::tail) when n > 1 -> get_nth msg tail (n-1)
+  | (_,_) -> raise (NotEnoughElements msg)
 ;;
 
 
@@ -224,7 +224,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
          match tt with
             C.Rel n ->
              let id =
-              match get_nth context n with
+              match get_nth "1" context n with
                  (Some (C.Name s,_)) -> s
                | _ -> "__" ^ string_of_int n
              in
@@ -300,20 +300,13 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
               C.ALambda
                (fresh_id'',n, aux' context idrefs s,
                 aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
-          | C.LetIn (n,s,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
+          | C.LetIn (n,s,ty,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,Some s_ty)))::context) (fresh_id''::idrefs) t)
+               (fresh_id'', n, aux' context idrefs s, aux' context idrefs ty,
+                aux' ((Some (n, C.Def(s,ty)))::context) (fresh_id''::idrefs) t)
           | C.Appl l ->
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = `Prop then
@@ -353,8 +346,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
@@ -370,8 +367,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
@@ -421,12 +422,21 @@ let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
            Hashtbl.add ids_to_hypotheses hid binding ;
            incr hypotheses_seed ;
            match binding with
-               Some (n,Cic.Def (t,_)) ->
-                 let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
-                 Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
-                  (Some hid);
-                 (binding::context),
-                   ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
+               Some (n,Cic.Def (t,ty)) ->
+                 let acic =
+                  acic_of_cic_context ~computeinnertypes context idrefs t
+                   None in
+                 let acic2 =
+                  acic_of_cic_context ~computeinnertypes context idrefs ty
+                   None
+                 in
+                  Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
+                   (Some hid);
+                  Hashtbl.replace ids_to_father_ids
+                   (CicUtil.id_of_annterm acic2) (Some hid);
+                  (binding::context),
+                    ((hid,Some (n,Cic.ADef (acic,acic2)))::acontext),
+                    (hid::idrefs)
              | Some (n,Cic.Decl t) ->
                  let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
                  Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
@@ -461,10 +471,8 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
               None -> None
             | Some (n, Cic.Decl t)->
                Some (n, Cic.Decl (Unshare.unshare t))
-            | Some (n, Cic.Def (t,None)) ->
-               Some (n, Cic.Def ((Unshare.unshare t),None))
-            | Some (n,Cic.Def (bo,Some ty)) ->
-               Some (n, Cic.Def (Unshare.unshare bo,Some (Unshare.unshare ty)))
+            | Some (n,Cic.Def (bo,ty)) ->
+               Some (n, Cic.Def (Unshare.unshare bo,Unshare.unshare ty))
           in
            d::canonical_context'
         ) canonical_context []
@@ -500,30 +508,30 @@ let acic_object_of_cic_object ?(eta_fix=false) obj =
   let aconjecture_of_conjecture' = aconjecture_of_conjecture seed 
     ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types 
     ids_to_hypotheses hypotheses_seed in 
-   let eta_fix metasenv context t =
+   let eta_fix_and_unshare metasenv context t =
     let t = if eta_fix then E.eta_fix metasenv context t else t in
      Unshare.unshare t in
    let aobj =
     match obj with
       C.Constant (id,Some bo,ty,params,attrs) ->
-       let bo' = (*eta_fix [] []*) bo in
-       let ty' = eta_fix [] [] ty in
+       let bo' = (*eta_fix_and_unshare[] [] bo*) Unshare.unshare bo in
+       let ty' = eta_fix_and_unshare [] [] 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
         C.AConstant
          ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
     | C.Constant (id,None,ty,params,attrs) ->
-       let ty' = eta_fix [] [] ty in
+       let ty' = eta_fix_and_unshare [] [] ty in
        let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
         C.AConstant
          ("mettereaposto",None,id,None,aty,params,attrs)
     | C.Variable (id,bo,ty,params,attrs) ->
-       let ty' = eta_fix [] [] ty in
+       let ty' = eta_fix_and_unshare [] [] ty in
        let abo =
         match bo with
            None -> None
          | Some bo ->
-            let bo' = eta_fix [] [] bo in
+            let bo' = eta_fix_and_unshare [] [] bo in
              Some (acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty'))
        in
        let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
@@ -540,16 +548,17 @@ let acic_object_of_cic_object ?(eta_fix=false) obj =
                 match d with
                    None -> None
                  | Some (n, C.Decl t)->
-                    Some (n, C.Decl (eta_fix conjectures canonical_context' t))
-                 | Some (n, C.Def (t,None)) ->
+                    Some (n, C.Decl (eta_fix_and_unshare conjectures canonical_context' t))
+                 | Some (n, C.Def (t,ty)) ->
                     Some (n,
-                     C.Def ((eta_fix conjectures canonical_context' t),None))
-                 | Some (_,C.Def (_,Some _)) -> assert false
+                     C.Def
+                      (eta_fix_and_unshare conjectures canonical_context' t,
+                       eta_fix_and_unshare conjectures canonical_context' ty))
                in
                 d::canonical_context'
              ) canonical_context []
            in
-           let term' = eta_fix conjectures canonical_context' term in
+           let term' = eta_fix_and_unshare conjectures canonical_context' term in
             (i,canonical_context',term')
          ) conjectures
        in
@@ -565,7 +574,7 @@ let acic_object_of_cic_object ?(eta_fix=false) obj =
           conjectures' in 
        (* let bo' = eta_fix conjectures' [] bo in *)
        let bo' = bo in
-       let ty' = eta_fix conjectures' [] ty in
+       let ty' = eta_fix_and_unshare conjectures' [] ty in
 (*
        let time2 = Sys.time () in
        prerr_endline
@@ -635,7 +644,7 @@ let plain_acic_term_of_cic_term =
   match t with
      C.Rel n ->
       let idref,id =
-       match get_nth context n with
+       match get_nth "2" context n with
           idref,(Some (C.Name s,_)) -> idref,s
         | idref,_ -> idref,"__" ^ string_of_int n
       in
@@ -659,10 +668,10 @@ let plain_acic_term_of_cic_term =
        C.ALambda
         (fresh_id,n, aux context s,
          aux ((fresh_id, Some (n, C.Decl s))::context) t)
-   | C.LetIn (n,s,t) ->
+   | C.LetIn (n,s,ty,t) ->
       C.ALetIn
-       (fresh_id, n, aux context s,
-        aux ((fresh_id, Some (n, C.Def(s,None)))::context) t)
+       (fresh_id, n, aux context s, aux context ty,
+        aux ((fresh_id, Some (n, C.Def(s,ty)))::context) t)
    | C.Appl l ->
       C.AAppl (fresh_id, List.map (aux context) l)
    | C.Const (uri,exp_named_subst) ->
@@ -687,9 +696,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
@@ -698,9 +710,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