X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcontent2cic.ml;h=339492d1985317911dad12a0890d5a89d62fea25;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=815e0caaac8b65ba68f519a2181d238a95786c2a;hpb=e23bc37c0a5e552395e499e7b8cee8d610b8e4f4;p=helm.git diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml index 815e0caaa..339492d19 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 @@ -146,28 +149,50 @@ let proof2cic term2cic p = (match conclude.Con.conclude_args with [Con.ArgProof p] -> proof2cic [] p (* empty! *) | _ -> prerr_endline "4"; assert false) - else if (conclude.Con.conclude_method = "ByInduction") then + else if (conclude.Con.conclude_method = "ByInduction" || + conclude.Con.conclude_method = "AndInd" || + conclude.Con.conclude_method = "Exists" || + conclude.Con.conclude_method = "FalseInd") then (match (List.tl conclude.Con.conclude_args) with - Con.Term (C.AAppl - id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args -> + 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) + else if (conclude.Con.conclude_method = "Case") then + (match conclude.Con.conclude_args with + Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Premise(prem)::patterns -> + C.MutCase + (UriManager.uri_of_string uri, + int_of_string notype, deannotate ty, + List.assoc prem.Con.premise_xref premise_env, + List.map + (function + Con.ArgProof p -> proof2cic [] p + | _ -> prerr_endline "7a"; assert false) patterns) + | Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns -> C.MutCase + (UriManager.uri_of_string uri, + int_of_string notype, deannotate ty, deannotate te, + List.map + (function + (Con.ArgProof p) -> proof2cic [] p + | _ -> prerr_endline "7a"; assert false) patterns) + | _ -> (prerr_endline "7"; assert false)) else if (conclude.Con.conclude_method = "Apply") then let cargs = (args2cic premise_env conclude.Con.conclude_args) in C.Appl cargs - else (prerr_endline "7"; assert false) + else (prerr_endline "8"; assert false) and args2cic premise_env l = List.map (arg2cic premise_env) l @@ -179,20 +204,65 @@ 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 - | Con.ArgProof p -> - proof2cic [] p (* empty! *) + | Con.Lemma lemma -> + CicUtil.term_of_uri (UriManager.uri_of_string lemma.Con.lemma_uri) + | Con.Term t -> deannotate t + | Con.ArgProof p -> proof2cic [] p (* empty! *) | Con.ArgMethod s -> raise TO_DO 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),None)) + | _ -> assert false) + | Some (`Proof d) -> + (match d with + {K.proof_name = Some n } -> + Some (Cic.Name n, + Cic.Def ((proof2cic deannotate d),None)) + | _ -> 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;;