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 (* Note: this code is almost identical to change_tac and
29 * it could be unified by making the change function a callback *)
30 let reduction_tac ~reduction ~pattern (proof,goal) =
31 let curi,metasenv,pbo,pty = proof in
32 let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
33 let change subst where terms =
34 if terms = [] then where
37 List.split (List.map (fun (context, t) -> t, reduction context t) terms)
40 ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
43 CicMetaSubst.apply_subst subst where' in
44 let (subst,metasenv,ugraph,selected_context,selected_ty) =
45 ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
46 ~conjecture ~pattern in
47 let ty' = change subst ty selected_ty in
50 (fun entry selected_entry context' ->
51 match entry,selected_entry with
52 None,None -> None::context'
53 | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
54 let ty' = change subst ty selected_ty in
55 Some (name,Cic.Decl ty')::context'
56 | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
57 let bo' = change subst bo selected_bo in
59 match ty,selected_ty with
61 | Some ty,Some selected_ty -> Some (change subst ty selected_ty)
64 Some (name,Cic.Def (bo',ty'))::context'
66 ) context selected_context [] in
69 | (n,_,_) when n = metano -> (metano,context',ty')
73 (curi,metasenv',pbo,pty), [metano]
76 let simpl_tac ~pattern =
77 mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);;
79 let reduce_tac ~pattern =
80 mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);;
82 let unfold_tac what ~pattern =
83 mk_tactic (reduction_tac ~reduction:(ProofEngineReduction.unfold ?what)
86 let whd_tac ~pattern =
87 mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);;
89 let normalize_tac ~pattern =
90 mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern);;
92 exception NotConvertible
94 (* Note: this code is almost identical to reduction_tac and
95 * it could be unified by making the change function a callback *)
96 (* CSC: with_what is parsed in the context of the goal, but it should replace
97 something that lives in a completely different context. Thus we
98 perform a delift + lift phase to move it in the right context. However,
99 in this way the tactic is less powerful than expected: with_what cannot
100 reference variables that are local to the term that is going to be
101 replaced. To fix this we should parse with_what in the context of the
102 term(s) to be replaced. *)
103 let change_tac ~pattern with_what =
104 let change_tac ~pattern ~with_what (proof, goal) =
105 let curi,metasenv,pbo,pty = proof in
106 let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
107 let context_len = List.length context in
108 let change subst context'_len where terms =
109 if terms = [] then where
114 (fun (context_of_t, t) ->
115 let context_of_t_len = List.length context_of_t in
116 let with_what_in_context' =
117 if context_len > context'_len then
119 let with_what,subst,metasenv' =
120 CicMetaSubst.delift_rels [] metasenv
121 (context_len - context'_len) with_what
124 assert (metasenv = metasenv');
129 let with_what_in_context_of_t =
130 if context_of_t_len > context'_len then
131 CicSubstitution.lift (context_of_t_len - context'_len)
132 with_what_in_context'
136 CicTypeChecker.type_of_aux' metasenv context_of_t with_what
137 CicUniv.empty_ugraph in
139 CicReduction.are_convertible ~metasenv context_of_t t with_what u in
141 t, with_what_in_context_of_t
143 raise NotConvertible) terms)
146 ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
149 CicMetaSubst.apply_subst subst where' in
150 let (subst,metasenv,ugraph,selected_context,selected_ty) =
151 ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture
153 let ty' = change subst context_len ty selected_ty in
156 (fun entry selected_entry context' ->
157 let context'_len = List.length context' in
158 match entry,selected_entry with
159 None,None -> None::context'
160 | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
161 let ty' = change subst context'_len ty selected_ty in
162 Some (name,Cic.Decl ty')::context'
163 | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
164 let bo' = change subst context'_len bo selected_bo in
166 match ty,selected_ty with
168 | Some ty,Some selected_ty ->
169 Some (change subst context'_len ty selected_ty)
170 | _,_ -> assert false
172 Some (name,Cic.Def (bo',ty'))::context'
173 | _,_ -> assert false
174 ) context selected_context [] in
177 | (n,_,_) when n = metano -> (metano,context',ty')
181 (curi,metasenv',pbo,pty), [metano]
183 mk_tactic (change_tac ~pattern ~with_what)
185 let fold_tac ~reduction ~term ~pattern =
186 let fold_tac ~reduction ~term ~pattern:(wanted,hyps_pat,concl_pat) status =
187 assert (wanted = None); (* this should be checked syntactically *)
188 let proof,goal = status in
189 let _,metasenv,_,_ = proof in
190 let _,context,_ = CicUtil.lookup_meta goal metasenv in
191 let reduced_term = reduction context term in
193 (change_tac ~pattern:(Some reduced_term,hyps_pat,concl_pat) term) status
195 mk_tactic (fold_tac ~reduction ~term ~pattern)