1 (* Copyright (C) 2002, 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/.
28 module PET = ProofEngineTypes
32 let clearbody (proof, goal) =
33 let curi,metasenv,_subst,pbo,pty, attrs = proof in
34 let metano,_,_ = CicUtil.lookup_meta goal metasenv in
43 (m,canonical_context,ty) when m = metano ->
44 let canonical_context' =
48 Some (C.Name hyp',C.Def (term,ty)) when hyp = hyp' ->
55 (CicTypeChecker.type_of_aux' metasenv context term
56 CicUniv.empty_ugraph) (* TASSI: FIXME *)
58 Some (C.Name hyp, Cic.Decl ty)
60 cleared_entry::context
61 | None -> None::context
63 | Some (n,C.Def (t,None)) ->
66 CicTypeChecker.type_of_aux' metasenv context t
67 CicUniv.empty_ugraph (* TASSI: FIXME *)
72 (lazy ("The correctness of hypothesis " ^
74 " relies on the body of " ^ hyp)
78 | Some (n,Cic.Def (te,Some ty)) ->
81 (CicTypeChecker.type_of_aux' metasenv context te
82 CicUniv.empty_ugraph (* TASSI: FIXME *));
84 (CicTypeChecker.type_of_aux' metasenv context ty
85 CicUniv.empty_ugraph (* TASSI: FIXME *));
90 (lazy ("The correctness of hypothesis " ^
92 " relies on the body of " ^ hyp)
95 ) canonical_context []
99 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
100 CicUniv.empty_ugraph (* TASSI: FIXME *)
105 (lazy ("The correctness of the goal relies on the body of " ^
108 m,canonical_context',ty
112 (curi,metasenv',_subst,pbo,pty, attrs), [goal]
114 PET.mk_tactic clearbody
117 let clear_one (proof, goal) =
118 let curi,metasenv,_subst,pbo,pty, attrs = proof in
119 let metano,context,ty =
120 CicUtil.lookup_meta goal metasenv
130 (m,canonical_context,ty) when m = metano ->
131 let context_changed, canonical_context' =
133 (fun entry (b, context) ->
135 Some (Cic.Name hyp',_) when hyp' = hyp ->
136 (true, None::context)
137 | None -> (b, None::context)
139 | Some (n,Cic.Def (t,Some _))
140 | Some (n,C.Def (t,None)) ->
144 CicTypeChecker.type_of_aux' metasenv context t
149 (lazy ("Hypothesis " ^ string_of_name n ^
150 " uses hypothesis " ^ hyp)))
155 ) canonical_context (false, [])
157 if not context_changed then
158 raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
161 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
164 raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
166 m,canonical_context',ty
170 (curi,metasenv',_subst,pbo,pty, attrs), [goal]
172 PET.mk_tactic clear_one
177 match PET.apply_tactic (clear_one ~hyp) status with
178 | proof, [g] -> proof, g
179 | _ -> raise (PET.Fail (lazy "clear: internal error"))
181 let proof, g = List.fold_left aux status hyps in
186 (* Warning: this tactic has no effect on the proof term.
187 It just changes the name of an hypothesis in the current sequent *)
188 let rename ~froms ~tos =
189 let rename (proof, goal) =
190 let error = "rename: lists of different length" in
192 try List.combine froms tos
193 with Invalid_argument _ -> raise (PET.Fail (lazy error))
195 let curi, metasenv, _subst, pbo, pty, attrs = proof in
196 let metano, _, _ = CicUtil.lookup_meta goal metasenv in
197 let rename_map = function
198 | Some (Cic.Name hyp, decl_or_def) as entry ->
199 begin try Some (Cic.Name (List.assoc hyp assocs), decl_or_def)
200 with Not_found -> entry end
204 | m, canonical_context, ty when m = metano ->
205 let canonical_context = List.map rename_map canonical_context in
206 m, canonical_context, ty
207 | conjecture -> conjecture
209 let metasenv = List.map map metasenv in
210 (curi, metasenv, _subst, pbo, pty, attrs), [goal]