X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.ml;h=69c91cdb3eb959d07fa1e8592ddf80adc518de02;hb=73e63e535940a068e660d3688a3c8ebfa1930561;hp=608f6d7c3aa8af0faf616c448a2f693bb75de074;hpb=ff981d975589f8d21a364e7cfe875647f7483cd9;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index 608f6d7c3..69c91cdb3 100644
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -415,6 +415,26 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
     let ids_to_hypotheses = Hashtbl.create 23 in
     let hypotheses_seed = ref 0 in
     let seed = ref 1 in (* 'i0' is used for the whole sequent *)
+    let sequent =
+     let i,canonical_context,term = sequent in
+      let canonical_context' =
+       List.fold_right
+        (fun d canonical_context' ->
+          let d =
+           match d with
+              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 (_,Cic.Def (_,Some _)) -> assert false
+          in
+           d::canonical_context'
+        ) canonical_context []
+      in
+      let term' = Unshare.unshare term in
+       (i,canonical_context',term')
+    in
     let (metano,acontext,agoal) = 
       aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids 
       ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
@@ -443,8 +463,8 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
     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 =
-    if eta_fix then E.eta_fix metasenv context t else t
-   in
+    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) ->
@@ -478,7 +498,7 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
            let canonical_context' =
             List.fold_right
              (fun d canonical_context' ->
-               let d' =
+               let d =
                 match d with
                    None -> None
                  | Some (n, C.Decl t)->
@@ -489,7 +509,7 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
                  | Some (_,C.Def (_,Some _)) -> assert false
                in
                 d::canonical_context'
-             ) [] canonical_context
+             ) canonical_context []
            in
            let term' = eta_fix conjectures canonical_context' term in
             (i,canonical_context',term')
@@ -505,46 +525,6 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
              = aconjecture_of_conjecture' conjectures conjecture in
            (cid,i,acanonical_context,aterm))
           conjectures' in 
-(*           let idrefs',revacanonical_context =
-             let rec aux context idrefs =
-              function
-                 [] -> idrefs,[]
-               | hyp::tl ->
-                  let hid = "h" ^ string_of_int !hypotheses_seed in
-                  let new_idrefs = hid::idrefs in
-                   xxx_add ids_to_hypotheses hid hyp ;
-                   incr hypotheses_seed ;
-                   match hyp with
-                      (Some (n,C.Decl t)) ->
-                        let final_idrefs,atl =
-                         aux (hyp::context) new_idrefs tl in
-                        let at =
-                         acic_term_of_cic_term_context'
-                          conjectures context idrefs t None
-                        in
-                         final_idrefs,(hid,Some (n,C.ADecl at))::atl
-                    | (Some (n,C.Def (t,_))) ->
-                        let final_idrefs,atl =
-                         aux (hyp::context) new_idrefs tl in
-                        let at =
-                         acic_term_of_cic_term_context'
-                          conjectures context idrefs t None
-                        in
-                         final_idrefs,(hid,Some (n,C.ADef at))::atl
-                    | None ->
-                       let final_idrefs,atl =
-                        aux (hyp::context) new_idrefs tl
-                       in
-                        final_idrefs,(hid,None)::atl
-             in
-              aux [] [] (List.rev canonical_context) 
-            in
-             let aterm =
-              acic_term_of_cic_term_context' conjectures
-               canonical_context idrefs' term None 
-             in
-              (cid,i,(List.rev revacanonical_context),aterm) 
-         ) conjectures' in *)
 (*        let time1 = Sys.time () in *)
        let bo' = eta_fix conjectures' [] bo in
        let ty' = eta_fix conjectures' [] ty in
@@ -577,9 +557,15 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
         C.ACurrentProof
          ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params,attrs)
     | C.InductiveDefinition (tys,params,paramsno,attrs) ->
+       let tys =
+        List.map
+         (fun (name,i,arity,cl) ->
+           (name,i,Unshare.unshare arity,
+             List.map (fun (name,ty) -> name,Unshare.unshare ty) cl)) tys in
        let context =
         List.map
-         (fun (name,_,arity,_) -> Some (C.Name name, C.Decl arity)) tys in
+         (fun (name,_,arity,_) ->
+           Some (C.Name name, C.Decl (Unshare.unshare arity))) tys in
        let idrefs = List.map (function _ -> gen_id seed) tys in
        let atys =
         List.map2
@@ -600,4 +586,136 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
      ids_to_conjectures,ids_to_hypotheses
 ;;
 
+let plain_acic_term_of_cic_term =
+ let module C = Cic in
+ let mk_fresh_id =
+  let id = ref 0 in
+   function () -> incr id; "i" ^ string_of_int !id in
+ let rec aux context t =
+  let fresh_id = mk_fresh_id () in
+  match t with
+     C.Rel n ->
+      let idref,id =
+       match get_nth context n with
+          idref,(Some (C.Name s,_)) -> idref,s
+        | idref,_ -> idref,"__" ^ string_of_int n
+      in
+       C.ARel (fresh_id, idref, n, id)
+   | C.Var (uri,exp_named_subst) ->
+      let exp_named_subst' =
+       List.map
+        (function i,t -> i, (aux context t)) exp_named_subst
+      in
+       C.AVar (fresh_id,uri,exp_named_subst')
+   | C.Implicit _
+   | C.Meta _ -> assert false
+   | C.Sort s -> C.ASort (fresh_id, s)
+   | C.Cast (v,t) ->
+      C.ACast (fresh_id, aux context v, aux context t)
+   | C.Prod (n,s,t) ->
+        C.AProd
+         (fresh_id, n, aux context s,
+          aux ((fresh_id, Some (n, C.Decl s))::context) t)
+   | C.Lambda (n,s,t) ->
+       C.ALambda
+        (fresh_id,n, aux context s,
+         aux ((fresh_id, Some (n, C.Decl s))::context) t)
+   | C.LetIn (n,s,t) ->
+      C.ALetIn
+       (fresh_id, n, aux context s,
+        aux ((fresh_id, Some (n, C.Def(s,None)))::context) t)
+   | C.Appl l ->
+      C.AAppl (fresh_id, List.map (aux context) l)
+   | C.Const (uri,exp_named_subst) ->
+      let exp_named_subst' =
+       List.map
+        (function i,t -> i, (aux context t)) exp_named_subst
+      in
+       C.AConst (fresh_id, uri, exp_named_subst')
+   | C.MutInd (uri,tyno,exp_named_subst) ->
+      let exp_named_subst' =
+       List.map
+        (function i,t -> i, (aux context t)) exp_named_subst
+      in
+       C.AMutInd (fresh_id, uri, tyno, exp_named_subst')
+   | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+      let exp_named_subst' =
+       List.map
+        (function i,t -> i, (aux context t)) exp_named_subst
+      in
+       C.AMutConstruct (fresh_id, uri, tyno, consno, exp_named_subst')
+   | C.MutCase (uri, tyno, outty, term, patterns) ->
+      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
+      in
+       C.AFix (fresh_id, funno,
+        List.map2
+         (fun (id,_) (name, indidx, ty, bo) ->
+           (id, name, indidx, aux context ty, aux (tys@context) bo)
+         ) tys funs
+      )
+   | C.CoFix (funno, funs) ->
+      let tys =
+       List.map (fun (name,ty,_) ->
+        mk_fresh_id (),Some (C.Name name, C.Decl ty)) funs
+      in
+       C.ACoFix (fresh_id, funno,
+        List.map2
+         (fun (id,_) (name, ty, bo) ->
+           (id, name, aux context ty, aux (tys@context) bo)
+         ) tys funs
+       )
+ in
+  aux
+;;
 
+let plain_acic_object_of_cic_object obj =
+ let module C = Cic in
+ let mk_fresh_id =
+  let id = ref 0 in
+   function () -> incr id; "it" ^ string_of_int !id
+ in
+  match obj with
+    C.Constant (id,Some bo,ty,params,attrs) ->
+     let abo = plain_acic_term_of_cic_term [] bo in
+     let aty = plain_acic_term_of_cic_term [] ty in
+      C.AConstant
+       ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
+  | C.Constant (id,None,ty,params,attrs) ->
+     let aty = plain_acic_term_of_cic_term [] ty in
+      C.AConstant
+       ("mettereaposto",None,id,None,aty,params,attrs)
+  | C.Variable (id,bo,ty,params,attrs) ->
+     let abo =
+      match bo with
+         None -> None
+       | Some bo -> Some (plain_acic_term_of_cic_term [] bo)
+     in
+     let aty = plain_acic_term_of_cic_term [] ty in
+      C.AVariable
+       ("mettereaposto",id,abo,aty,params,attrs)
+  | C.CurrentProof _ -> assert false
+  | C.InductiveDefinition (tys,params,paramsno,attrs) ->
+     let context =
+      List.map
+       (fun (name,_,arity,_) ->
+         mk_fresh_id (), Some (C.Name name, C.Decl arity)) tys in
+     let atys =
+      List.map2
+       (fun (id,_) (name,inductive,ty,cons) ->
+         let acons =
+          List.map
+           (function (name,ty) ->
+             (name,
+               plain_acic_term_of_cic_term context ty)
+           ) cons
+         in
+          (id,name,inductive,plain_acic_term_of_cic_term [] ty,acons)
+       ) context tys
+     in
+      C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
+;;