Interface change: only cobj2obj is exposed.

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index 815e0caaac8b65ba68f519a2181d238a95786c2a..1d4dcd1ee885bbaac4c9daa0be69f0f18e4a5220 100644 (file)
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -34,7 +34,7 @@
 
 exception TO_DO;;
 
-let proof2cic term2cic p =
+let proof2cic deannotate p =
   let rec proof2cic premise_env p =
     let module C = Cic in 
     let module Con = Content in
@@ -58,15 +58,15 @@ let proof2cic term2cic p =
         `Declaration d -> 
           (match d.Con.dec_name with
               Some s ->
-                C.Lambda (C.Name s, term2cic d.Con.dec_type, target)
+                C.Lambda (C.Name s, deannotate d.Con.dec_type, target)
             | None -> 
-                C.Lambda (C.Anonymous, term2cic d.Con.dec_type, target))
+                C.Lambda (C.Anonymous, deannotate d.Con.dec_type, target))
       | `Hypothesis h ->
           (match h.Con.dec_name with
               Some s ->
-                C.Lambda (C.Name s, term2cic h.Con.dec_type, target)
+                C.Lambda (C.Name s, deannotate h.Con.dec_type, target)
             | None -> 
-                C.Lambda (C.Anonymous, term2cic h.Con.dec_type, target))
+                C.Lambda (C.Anonymous, deannotate h.Con.dec_type, target))
       | `Proof p -> 
           (match p.Con.proof_name with
               Some s ->
@@ -94,7 +94,8 @@ let proof2cic term2cic p =
                                     bo.Con.proof_name
                                    with
                                       Some ty, Some name -> 
-                                       (name,n,term2cic ty,proof2cic premise_env bo)
+                                       (name,n,deannotate ty,
+                                         proof2cic premise_env bo)
                                     | _,_ -> assert false)
                              | _ -> assert false)
                           l defs in 
@@ -110,7 +111,8 @@ let proof2cic term2cic p =
                                     bo.Con.proof_name 
                                   with
                                      Some ty, Some name ->
-                                      (name,term2cic ty,proof2cic premise_env bo)
+                                      (name,deannotate ty,
+                                        proof2cic premise_env bo)
                                    | _,_ -> assert false)
                              | _ -> assert false)
                            defs in 
@@ -131,12 +133,13 @@ let proof2cic term2cic p =
          [Con.Premise prem] -> 
            (try List.assoc prem.Con.premise_xref premise_env
             with Not_found -> 
-              prerr_endline ("Not_found: " ^ prem.Con.premise_xref);
+              prerr_endline
+               ("Not_found in BU_Conversion: " ^ prem.Con.premise_xref);
               raise Not_found)
        | _ -> prerr_endline "2"; assert false)
     else if conclude.Con.conclude_method = "Exact" then
       (match conclude.Con.conclude_args with
-         [Con.Term t] -> term2cic t
+         [Con.Term t] -> deannotate t
        | [Con.Premise prem] -> 
            (match prem.Con.premise_n with
               None -> assert false
@@ -151,16 +154,16 @@ let proof2cic term2cic p =
          Con.Term (C.AAppl 
             id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args ->
            let subst =
-             List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in 
+             List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in 
            let cargs = args2cic premise_env args in
-           let cparams_and_IP = List.map term2cic params_and_IP in
+           let cparams_and_IP = List.map deannotate params_and_IP in
            C.Appl (C.Const(uri,subst)::cparams_and_IP@cargs)
        | _ -> prerr_endline "5"; assert false)
     else if (conclude.Con.conclude_method = "Rewrite") then
       (match conclude.Con.conclude_args with
          Con.Term (C.AConst (sid,uri,exp_named_subst))::args ->
            let subst =
-             List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in
+             List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
            let  cargs = args2cic premise_env args in
            C.Appl (C.Const(uri,subst)::cargs)
        | _ -> prerr_endline "6"; assert false)
@@ -179,15 +182,14 @@ let proof2cic term2cic p =
         Con.Aux n -> prerr_endline "8"; assert false
       | Con.Premise prem ->
           (match prem.Con.premise_n with
-            Some n -> 
-              C.Rel n
-            | _ ->
+              Some n -> C.Rel n
+            | None ->
               (try List.assoc prem.Con.premise_xref premise_env
                with Not_found -> 
-                  prerr_endline ("Not_found: " ^ prem.Con.premise_xref);
+                  prerr_endline ("Not_found in arg2cic: premise " ^ (match prem.Con.premise_binder with None -> "previous" | Some p -> p) ^ ", xref=" ^ prem.Con.premise_xref);
                   raise Not_found))
       | Con.Term t -> 
-          term2cic t
+          deannotate t
       | Con.ArgProof p ->
           proof2cic [] p (* empty! *)
       | Con.ArgMethod s -> raise TO_DO
@@ -195,4 +197,48 @@ let proof2cic term2cic p =
 in proof2cic [] p
 ;;
 
-let proof2cic = proof2cic Deannotate.deannotate_term;;
+exception ToDo;;
+
+let cobj2obj deannotate (id,params,metasenv,obj) =
+ let module K = Content in
+ match obj with
+    `Def (Content.Const,ty,`Proof bo) ->
+      (match metasenv with
+          None ->
+           Cic.Constant
+            (id, Some (proof2cic deannotate bo), deannotate ty, params)
+        | Some metasenv' ->
+           let metasenv'' =
+            List.map
+             (function (_,i,canonical_context,term) ->
+               let canonical_context' =
+                List.map
+                 (function
+                     _,None -> None
+                   | _,Some (`Declaration d) 
+                   | _,Some (`Hypothesis d) ->
+                     (match d with
+                        {K.dec_name = Some n ; K.dec_type = t} ->
+                          Some (Cic.Name n, Cic.Decl (deannotate t))
+                      | _ -> assert false)
+                   | _,Some (`Definition d) ->
+                      (match d with
+                          {K.def_name = Some n ; K.def_term = t} ->
+                            Some (Cic.Name n, Cic.Def (deannotate t))
+                        | _ -> assert false)
+                   | _,Some (`Proof d) ->
+                      (match d with
+                          {K.proof_name = Some n } ->
+                            Some (Cic.Name n, Cic.Def (proof2cic deannotate d))
+                        | _ -> assert false)
+                 ) canonical_context
+               in
+                (i,canonical_context',deannotate term)
+             ) metasenv'
+           in
+            Cic.CurrentProof
+             (id, metasenv'', proof2cic deannotate bo, deannotate ty, params))
+  | _ -> raise ToDo
+;;
+
+let cobj2obj = cobj2obj Deannotate.deannotate_term;;

diff --git a/helm/ocaml/cic_omdoc/content2cic.mli b/helm/ocaml/cic_omdoc/content2cic.mli
index a1c19fa578bcfb6c60ae19df4b6dcd0a07be43f5..9bb6509cc23da41c4e5fe7fd84495aeb4da8fd68 100644 (file)
--- a/helm/ocaml/cic_omdoc/content2cic.mli
+++ b/helm/ocaml/cic_omdoc/content2cic.mli
@@ -32,4 +32,4 @@
 (*                                                                        *)
 (**************************************************************************)
 
-val proof2cic : Cic.annterm Content.proof -> Cic.term
+val cobj2obj : Cic.annterm Content.cobj -> Cic.obj