From: Claudio Sacerdoti Coen Date: Mon, 21 Jul 2003 14:06:17 +0000 (+0000) Subject: Interface change: only cobj2obj is exposed. X-Git-Tag: LucaOK~47 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a70ce8d5659ab5cd532317e206a30da878ff8a89;p=helm.git Interface change: only cobj2obj is exposed. --- diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml index 815e0caaa..1d4dcd1ee 100644 --- 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 a1c19fa57..9bb6509cc 100644 --- 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