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/.
30 (* Note: this code is almost identical to change_tac and
31 * it could be unified by making the change function a callback *)
32 let reduction_tac ~reduction ~pattern (proof,goal) =
33 let curi,metasenv,_subst,pbo,pty, attrs = proof in
34 let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
35 let change subst where terms metasenv ugraph =
36 if terms = [] then where, metasenv, ugraph
38 let pairs, metasenv, ugraph =
40 (fun (pairs, metasenv, ugraph) (context, t) ->
41 let reduction, metasenv, ugraph = reduction context metasenv ugraph in
42 ((t, reduction context t) :: pairs), metasenv, ugraph)
43 ([], metasenv, ugraph)
46 let terms, terms' = List.split pairs in
48 ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
51 CicMetaSubst.apply_subst subst where', metasenv, ugraph
53 let (subst,metasenv,ugraph,selected_context,selected_ty) =
54 ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
57 let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
58 let context', metasenv, ugraph =
60 (fun entry selected_entry (context', metasenv, ugraph) ->
61 match entry,selected_entry with
62 None,None -> None::context', metasenv, ugraph
63 | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
64 let ty', metasenv, ugraph =
65 change subst ty selected_ty metasenv ugraph
67 Some (name,Cic.Decl ty')::context', metasenv, ugraph
68 | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
69 let bo', metasenv, ugraph =
70 change subst bo selected_bo metasenv ugraph
72 let ty', metasenv, ugraph =
73 match ty,selected_ty with
74 None,None -> None, metasenv, ugraph
75 | Some ty,Some selected_ty ->
76 let ty', metasenv, ugraph =
77 change subst ty selected_ty metasenv ugraph
79 Some ty', metasenv, ugraph
82 (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
84 ) context selected_context ([], metasenv, ugraph) in
87 | (n,_,_) when n = metano -> (metano,context',ty')
91 (curi,metasenv',_subst,pbo,pty, attrs), [metano]
94 let simpl_tac ~pattern =
95 mk_tactic (reduction_tac
96 ~reduction:(const_lazy_reduction ProofEngineReduction.simpl) ~pattern)
98 let reduce_tac ~pattern =
99 mk_tactic (reduction_tac
100 ~reduction:(const_lazy_reduction ProofEngineReduction.reduce) ~pattern)
102 let unfold_tac what ~pattern =
105 | None -> const_lazy_reduction (ProofEngineReduction.unfold ?what:None)
107 (fun context metasenv ugraph ->
108 let what, metasenv, ugraph = lazy_term context metasenv ugraph in
109 ProofEngineReduction.unfold ~what, metasenv, ugraph)
111 mk_tactic (reduction_tac ~reduction ~pattern)
113 let whd_tac ~pattern =
114 mk_tactic (reduction_tac
115 ~reduction:(const_lazy_reduction CicReduction.whd) ~pattern)
117 let normalize_tac ~pattern =
118 mk_tactic (reduction_tac
119 ~reduction:(const_lazy_reduction CicReduction.normalize) ~pattern)
121 let head_beta_reduce_tac ?delta ?upto ~pattern =
122 mk_tactic (reduction_tac
124 (const_lazy_reduction
125 (fun _context -> CicReduction.head_beta_reduce ?delta ?upto)) ~pattern)
127 exception NotConvertible
129 (* Note: this code is almost identical to reduction_tac and
130 * it could be unified by making the change function a callback *)
131 (* CSC: with_what is parsed in the context of the goal, but it should replace
132 something that lives in a completely different context. Thus we
133 perform a delift + lift phase to move it in the right context. However,
134 in this way the tactic is less powerful than expected: with_what cannot
135 reference variables that are local to the term that is going to be
136 replaced. To fix this we should parse with_what in the context of the
137 term(s) to be replaced. *)
138 let change_tac ~pattern with_what =
139 let change_tac ~pattern ~with_what (proof, goal) =
140 let curi,metasenv,_subst,pbo,pty, attrs = proof in
141 let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
142 let change subst where terms metasenv ugraph =
143 if terms = [] then where, metasenv, ugraph
145 let pairs, metasenv, ugraph =
147 (fun (pairs, metasenv, ugraph) (context_of_t, t) ->
148 let with_what, metasenv, ugraph =
149 with_what context_of_t metasenv ugraph
152 CicTypeChecker.type_of_aux' metasenv context_of_t with_what ugraph
155 CicReduction.are_convertible ~metasenv context_of_t t with_what u
158 ((t, with_what) :: pairs), metasenv, ugraph
160 raise NotConvertible)
161 ([], metasenv, ugraph)
164 let terms, terms' = List.split pairs in
166 ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
169 CicMetaSubst.apply_subst subst where', metasenv, ugraph
171 let (subst,metasenv,ugraph,selected_context,selected_ty) =
172 ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture
174 let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
175 let context', metasenv, ugraph =
177 (fun entry selected_entry (context', metasenv, ugraph) ->
178 match entry,selected_entry with
179 None,None -> (None::context'), metasenv, ugraph
180 | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
181 let ty', metasenv, ugraph =
182 change subst ty selected_ty metasenv ugraph
184 (Some (name,Cic.Decl ty')::context'), metasenv, ugraph
185 | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
186 let bo', metasenv, ugraph =
187 change subst bo selected_bo metasenv ugraph
189 let ty', metasenv, ugraph =
190 match ty,selected_ty with
191 None,None -> None, metasenv, ugraph
192 | Some ty,Some selected_ty ->
193 let ty', metasenv, ugraph =
194 change subst ty selected_ty metasenv ugraph
196 Some ty', metasenv, ugraph
197 | _,_ -> assert false
199 (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
200 | _,_ -> assert false
201 ) context selected_context ([], metasenv, ugraph) in
205 | (n,_,_) when n = metano -> (metano,context',ty')
209 (curi,metasenv',_subst,pbo,pty, attrs), [metano]
211 mk_tactic (change_tac ~pattern ~with_what)
213 let fold_tac ~reduction ~term ~pattern =
214 let fold_tac ~reduction ~term ~pattern:(wanted,hyps_pat,concl_pat) status =
215 assert (wanted = None); (* this should be checked syntactically *)
217 (fun context metasenv ugraph ->
218 let term, metasenv, ugraph = term context metasenv ugraph in
219 let reduction, metasenv, ugraph = reduction context metasenv ugraph in
220 reduction context term, metasenv, ugraph)
223 (change_tac ~pattern:(Some reduced_term,hyps_pat,concl_pat) term) status
225 mk_tactic (fold_tac ~reduction ~term ~pattern)