X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcontent2cic.ml;h=339492d1985317911dad12a0890d5a89d62fea25;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=e8a95fc892f7984afb25ede9f630279afe3fb859;hpb=264523336352a5241b747b7e04b33630f6010aeb;p=helm.git diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml index e8a95fc89..339492d19 100644 --- a/helm/ocaml/cic_omdoc/content2cic.ml +++ b/helm/ocaml/cic_omdoc/content2cic.ml @@ -34,14 +34,14 @@ 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 let rec extend_premise_env current_env = - function + function [] -> current_env - | p::atl -> + | p::atl -> extend_premise_env ((p.Con.proof_id,(proof2cic current_env p))::current_env) atl in let new_premise_env = extend_premise_env premise_env p.Con.proof_apply_context 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 -> @@ -79,8 +79,47 @@ let proof2cic term2cic p = C.LetIn (C.Name s, proof2cic premise_env p, target) | None -> C.LetIn (C.Anonymous, proof2cic premise_env p, target)) - | `Joint ho -> - raise TO_DO + | `Joint {Con.joint_kind = kind; Con.joint_defs = defs} -> + (match target with + C.Rel n -> + (match kind with + `Recursive l -> + let funs = + List.map2 + (fun n bo -> + match bo with + `Proof bo -> + (match + bo.Con.proof_conclude.Con.conclude_conclusion, + bo.Con.proof_name + with + Some ty, Some name -> + (name,n,deannotate ty, + proof2cic premise_env bo) + | _,_ -> assert false) + | _ -> assert false) + l defs in + C.Fix (n, funs) + | `CoRecursive -> + let funs = + List.map + (function bo -> + match bo with + `Proof bo -> + (match + bo.Con.proof_conclude.Con.conclude_conclusion, + bo.Con.proof_name + with + Some ty, Some name -> + (name,deannotate ty, + proof2cic premise_env bo) + | _,_ -> assert false) + | _ -> assert false) + defs in + C.CoFix (n, funs) + | _ -> (* no inductive types in local contexts *) + assert false) + | _ -> assert false) and conclude2cic premise_env conclude = let module C = Cic in @@ -94,39 +133,66 @@ 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 + | Some n -> C.Rel n) | _ -> prerr_endline "3"; assert false) else if conclude.Con.conclude_method = "Intros+LetTac" then (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 @@ -138,24 +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 ;; - - - +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;;