1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (***************************************************************************)
30 (* Andrea Asperti <asperti@cs.unibo.it> *)
33 (***************************************************************************)
37 let proof2cic term2cic p =
38 let rec proof2cic premise_env p =
40 let module Con = Cic2content in
41 let rec extend_premise_env current_env =
46 ((p.Con.proof_id,(proof2cic current_env p))::current_env) atl in
47 let new_premise_env = extend_premise_env premise_env p.Con.proof_apply_context in
48 let body = conclude2cic new_premise_env p.Con.proof_conclude in
49 context2cic premise_env p.Con.proof_context body
51 and context2cic premise_env context body =
52 List.fold_right (ce2cic premise_env) context body
54 and ce2cic premise_env ce target =
56 let module Con = Cic2content in
59 (match d.Con.dec_name with
61 C.Lambda (C.Name s, term2cic d.Con.dec_type, target)
63 C.Lambda (C.Anonymous, term2cic d.Con.dec_type, target))
65 (match h.Con.dec_name with
67 C.Lambda (C.Name s, term2cic h.Con.dec_type, target)
69 C.Lambda (C.Anonymous, term2cic h.Con.dec_type, target))
71 (match p.Con.proof_name with
73 C.LetIn (C.Name s, proof2cic premise_env p, target)
75 C.LetIn (C.Anonymous, proof2cic premise_env p, target))
77 (match d.Con.def_name with
79 C.LetIn (C.Name s, proof2cic premise_env p, target)
81 C.LetIn (C.Anonymous, proof2cic premise_env p, target))
85 and conclude2cic premise_env conclude =
87 let module Con = Cic2content in
88 if conclude.Con.conclude_method = "TD_Conversion" then
89 (match conclude.Con.conclude_args with
90 [Con.ArgProof p] -> proof2cic [] p (* empty! *)
91 | _ -> prerr_endline "1"; assert false)
92 else if conclude.Con.conclude_method = "BU_Conversion" then
93 (match conclude.Con.conclude_args with
95 (try List.assoc prem.Con.premise_xref premise_env
97 prerr_endline ("Not_found: " ^ prem.Con.premise_xref);
99 | _ -> prerr_endline "2"; assert false)
100 else if conclude.Con.conclude_method = "Exact" then
101 (match conclude.Con.conclude_args with
102 [Con.Term t] -> term2cic t
103 | _ -> prerr_endline "3"; assert false)
104 else if conclude.Con.conclude_method = "Intros+LetTac" then
105 (match conclude.Con.conclude_args with
106 [Con.ArgProof p] -> proof2cic [] p (* empty! *)
107 | _ -> prerr_endline "4"; assert false)
108 else if (conclude.Con.conclude_method = "ByInduction") then
109 (match (List.tl conclude.Con.conclude_args) with
111 id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args ->
113 List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in
114 let cargs = args2cic premise_env args in
115 let cparams_and_IP = List.map term2cic params_and_IP in
116 C.Appl (C.Const(uri,subst)::cparams_and_IP@cargs)
117 | _ -> prerr_endline "5"; assert false)
118 else if (conclude.Con.conclude_method = "Rewrite") then
119 (match conclude.Con.conclude_args with
120 Con.Term (C.AConst (sid,uri,exp_named_subst))::args ->
122 List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in
123 let cargs = args2cic premise_env args in
124 C.Appl (C.Const(uri,subst)::cargs)
125 | _ -> prerr_endline "6"; assert false)
126 else if (conclude.Con.conclude_method = "Apply") then
127 let cargs = (args2cic premise_env conclude.Con.conclude_args) in
129 else (prerr_endline "7"; assert false)
131 and args2cic premise_env l =
132 List.map (arg2cic premise_env) l
134 and arg2cic premise_env =
135 let module C = Cic in
136 let module Con = Cic2content in
138 Con.Aux n -> prerr_endline "8"; assert false
139 | Con.Premise prem ->
140 (match prem.Con.premise_n with
144 (try List.assoc prem.Con.premise_xref premise_env
146 prerr_endline ("Not_found: " ^ prem.Con.premise_xref);
151 proof2cic [] p (* empty! *)
152 | Con.ArgMethod s -> raise TO_DO