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 deannotate p =
38 let rec proof2cic premise_env p =
40 let module Con = Content 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 = Content in
59 (match d.Con.dec_name with
61 C.Lambda (C.Name s, deannotate d.Con.dec_type, target)
63 C.Lambda (C.Anonymous, deannotate d.Con.dec_type, target))
65 (match h.Con.dec_name with
67 C.Lambda (C.Name s, deannotate h.Con.dec_type, target)
69 C.Lambda (C.Anonymous, deannotate 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))
82 | `Joint {Con.joint_kind = kind; Con.joint_defs = defs} ->
93 bo.Con.proof_conclude.Con.conclude_conclusion,
97 (name,n,deannotate ty,
98 proof2cic premise_env bo)
99 | _,_ -> assert false)
110 bo.Con.proof_conclude.Con.conclude_conclusion,
113 Some ty, Some name ->
115 proof2cic premise_env bo)
116 | _,_ -> assert false)
120 | _ -> (* no inductive types in local contexts *)
124 and conclude2cic premise_env conclude =
125 let module C = Cic in
126 let module Con = Content in
127 if conclude.Con.conclude_method = "TD_Conversion" then
128 (match conclude.Con.conclude_args with
129 [Con.ArgProof p] -> proof2cic [] p (* empty! *)
130 | _ -> prerr_endline "1"; assert false)
131 else if conclude.Con.conclude_method = "BU_Conversion" then
132 (match conclude.Con.conclude_args with
133 [Con.Premise prem] ->
134 (try List.assoc prem.Con.premise_xref premise_env
137 ("Not_found in BU_Conversion: " ^ prem.Con.premise_xref);
139 | _ -> prerr_endline "2"; assert false)
140 else if conclude.Con.conclude_method = "Exact" then
141 (match conclude.Con.conclude_args with
142 [Con.Term t] -> deannotate t
143 | [Con.Premise prem] ->
144 (match prem.Con.premise_n with
147 | _ -> prerr_endline "3"; assert false)
148 else if conclude.Con.conclude_method = "Intros+LetTac" then
149 (match conclude.Con.conclude_args with
150 [Con.ArgProof p] -> proof2cic [] p (* empty! *)
151 | _ -> prerr_endline "4"; assert false)
152 else if (conclude.Con.conclude_method = "ByInduction") then
153 (match (List.tl conclude.Con.conclude_args) with
155 id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args ->
157 List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
158 let cargs = args2cic premise_env args in
159 let cparams_and_IP = List.map deannotate params_and_IP in
160 C.Appl (C.Const(uri,subst)::cparams_and_IP@cargs)
161 | _ -> prerr_endline "5"; assert false)
162 else if (conclude.Con.conclude_method = "Rewrite") then
163 (match conclude.Con.conclude_args with
164 Con.Term (C.AConst (sid,uri,exp_named_subst))::args ->
166 List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
167 let cargs = args2cic premise_env args in
168 C.Appl (C.Const(uri,subst)::cargs)
169 | _ -> prerr_endline "6"; assert false)
170 else if (conclude.Con.conclude_method = "Apply") then
171 let cargs = (args2cic premise_env conclude.Con.conclude_args) in
173 else (prerr_endline "7"; assert false)
175 and args2cic premise_env l =
176 List.map (arg2cic premise_env) l
178 and arg2cic premise_env =
179 let module C = Cic in
180 let module Con = Content in
182 Con.Aux n -> prerr_endline "8"; assert false
183 | Con.Premise prem ->
184 (match prem.Con.premise_n with
187 (try List.assoc prem.Con.premise_xref premise_env
189 prerr_endline ("Not_found in arg2cic: premise " ^ (match prem.Con.premise_binder with None -> "previous" | Some p -> p) ^ ", xref=" ^ prem.Con.premise_xref);
194 proof2cic [] p (* empty! *)
195 | Con.ArgMethod s -> raise TO_DO
202 let cobj2obj deannotate (id,params,metasenv,obj) =
203 let module K = Content in
205 `Def (Content.Const,ty,`Proof bo) ->
209 (id, Some (proof2cic deannotate bo), deannotate ty, params)
213 (function (_,i,canonical_context,term) ->
214 let canonical_context' =
218 | _,Some (`Declaration d)
219 | _,Some (`Hypothesis d) ->
221 {K.dec_name = Some n ; K.dec_type = t} ->
222 Some (Cic.Name n, Cic.Decl (deannotate t))
224 | _,Some (`Definition d) ->
226 {K.def_name = Some n ; K.def_term = t} ->
227 Some (Cic.Name n, Cic.Def (deannotate t))
229 | _,Some (`Proof d) ->
231 {K.proof_name = Some n } ->
232 Some (Cic.Name n, Cic.Def (proof2cic deannotate d))
236 (i,canonical_context',deannotate term)
240 (id, metasenv'', proof2cic deannotate bo, deannotate ty, params))
244 let cobj2obj = cobj2obj Deannotate.deannotate_term;;