X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcontent2cic.ml;fp=helm%2FgTopLevel%2Fcontent2cic.ml;h=17ba99ed8193797919c52f6981b2935b837670e6;hb=f7b2e35a7bdadb4fdf0e640428e694703ddf67a5;hp=0000000000000000000000000000000000000000;hpb=70f855932359e26ca89deb11c22f9c9d26154827;p=helm.git diff --git a/helm/gTopLevel/content2cic.ml b/helm/gTopLevel/content2cic.ml new file mode 100644 index 000000000..17ba99ed8 --- /dev/null +++ b/helm/gTopLevel/content2cic.ml @@ -0,0 +1,161 @@ +(* 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 term2cic p = + let rec proof2cic premise_env p = + let module C = Cic in + let module Con = Cic2content 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 = Cic2content in + match ce with + Con.Declaration d -> + (match d.Con.dec_name with + Some s -> + C.Lambda (C.Name s, term2cic d.Con.dec_type, target) + | None -> + C.Lambda (C.Anonymous, term2cic d.Con.dec_type, target)) + | Con.Hypothesis h -> + (match h.Con.dec_name with + Some s -> + C.Lambda (C.Name s, term2cic h.Con.dec_type, target) + | None -> + C.Lambda (C.Anonymous, term2cic h.Con.dec_type, target)) + | Con.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)) + | Con.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)) + | Con.Joint ho -> + raise TO_DO + + and conclude2cic premise_env conclude = + let module C = Cic in + let module Con = Cic2content 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: " ^ 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 + | _ -> 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, term2cic t)) exp_named_subst in + let cargs = args2cic premise_env args in + let cparams_and_IP = List.map term2cic 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 + 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 = "Apply") then + let cargs = (args2cic premise_env conclude.Con.conclude_args) in + C.Appl cargs + else (prerr_endline "7"; 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 = Cic2content in + function + Con.Aux n -> prerr_endline "8"; assert false + | Con.Premise prem -> + (match prem.Con.premise_n with + Some n -> + C.Rel n + | _ -> + (try List.assoc prem.Con.premise_xref premise_env + with Not_found -> + prerr_endline ("Not_found: " ^ prem.Con.premise_xref); + raise Not_found)) + | Con.Term t -> + term2cic t + | Con.ArgProof p -> + proof2cic [] p (* empty! *) + | Con.ArgMethod s -> raise TO_DO + +in proof2cic [] p +;; + + + + + +