We do not longer generate inner-types and inner-sorts for XML files generated

[helm.git] / helm / ocaml / cic_omdoc / cic2acic.ml

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index 2c3b9fb629c294e6e9ab3658db3a400cb38c909b..69c91cdb3eb959d07fa1e8592ddf80adc518de02 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -585,3 +585,137 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
     aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
      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)
+;;