X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcontent2cic.ml;fp=helm%2Focaml%2Fcic_omdoc%2Fcontent2cic.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=644f55920bd76e72ebb9529ee62ba54a9e0b658e;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml deleted file mode 100644 index 644f55920..000000000 --- a/helm/ocaml/cic_omdoc/content2cic.ml +++ /dev/null @@ -1,268 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(***************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 17/06/2003 *) -(* *) -(***************************************************************************) - -exception TO_DO;; - -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 - [] -> current_env - | 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 - let body = conclude2cic new_premise_env p.Con.proof_conclude in - context2cic premise_env p.Con.proof_context body - - and context2cic premise_env context body = - List.fold_right (ce2cic premise_env) context body - - and ce2cic premise_env ce target = - let module C = Cic in - let module Con = Content in - match ce with - `Declaration d -> - (match d.Con.dec_name with - Some s -> - C.Lambda (C.Name s, deannotate d.Con.dec_type, target) - | None -> - 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, deannotate h.Con.dec_type, target) - | None -> - C.Lambda (C.Anonymous, deannotate h.Con.dec_type, target)) - | `Proof p -> - (match p.Con.proof_name with - Some s -> - C.LetIn (C.Name s, proof2cic premise_env p, target) - | None -> - C.LetIn (C.Anonymous, proof2cic premise_env p, target)) - | `Definition d -> - (match d.Con.def_name with - Some s -> - C.LetIn (C.Name s, proof2cic premise_env p, target) - | None -> - C.LetIn (C.Anonymous, proof2cic premise_env p, target)) - | `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 - let module Con = Content in - if conclude.Con.conclude_method = "TD_Conversion" then - (match conclude.Con.conclude_args with - [Con.ArgProof p] -> proof2cic [] p (* empty! *) - | _ -> prerr_endline "1"; assert false) - else if conclude.Con.conclude_method = "BU_Conversion" then - (match conclude.Con.conclude_args with - [Con.Premise prem] -> - (try List.assoc prem.Con.premise_xref premise_env - with Not_found -> - 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] -> 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 - (match (List.tl conclude.Con.conclude_args) with - Con.Term (C.AAppl - id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args -> - let subst = - 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 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, 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 "8"; assert false) - - and args2cic premise_env l = - List.map (arg2cic premise_env) l - - and arg2cic premise_env = - let module C = Cic in - let module Con = Content in - function - Con.Aux n -> prerr_endline "8"; assert false - | Con.Premise prem -> - (match prem.Con.premise_n with - Some n -> C.Rel n - | None -> - (try List.assoc prem.Con.premise_xref premise_env - with Not_found -> - 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.Lemma lemma -> - MQueryMisc.term_of_cic_textual_parser_uri - (MQueryMisc.cic_textual_parser_uri_of_string - (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' - 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)) - | _ -> 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;;