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 whd_tac ~pattern =
83 mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);;
85 let normalize_tac ~pattern =
86 mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern);;
88 exception NotConvertible
90 (* Note: this code is almost identical to reduction_tac and
91 * it could be unified by making the change function a callback *)
92 (* CSC: with_what is parsed in the context of the goal, but it should replace
93 something that lives in a completely different context. Thus we
94 perform a delift + lift phase to move it in the right context. However,
95 in this way the tactic is less powerful than expected: with_what cannot
96 reference variables that are local to the term that is going to be
97 replaced. To fix this we should parse with_what in the context of the
98 term(s) to be replaced. *)
99 let change_tac ~pattern with_what =
100 let change_tac ~pattern ~with_what (proof, goal) =
101 let curi,metasenv,pbo,pty = proof in
102 let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
103 let context_len = List.length context in
104 let change subst context'_len where terms =
105 if terms = [] then where
110 (fun (context_of_t, t) ->
111 let context_of_t_len = List.length context_of_t in
112 let with_what_in_context' =
113 if context_len > context'_len then
115 let with_what,subst,metasenv' =
116 CicMetaSubst.delift_rels [] metasenv
117 (context_len - context'_len) with_what
120 assert (metasenv = metasenv');
125 let with_what_in_context_of_t =
126 if context_of_t_len > context'_len then
127 CicSubstitution.lift (context_of_t_len - context'_len)
128 with_what_in_context'
132 CicTypeChecker.type_of_aux' metasenv context_of_t with_what
133 CicUniv.empty_ugraph in
135 CicReduction.are_convertible ~metasenv context_of_t t with_what u in
137 t, with_what_in_context_of_t
139 raise NotConvertible) terms)
142 ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
145 CicMetaSubst.apply_subst subst where' in
146 let (subst,metasenv,ugraph,selected_context,selected_ty) =
147 ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture
149 let ty' = change subst context_len ty selected_ty in
152 (fun entry selected_entry context' ->
153 let context'_len = List.length context' in
154 match entry,selected_entry with
155 None,None -> None::context'
156 | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
157 let ty' = change subst context'_len ty selected_ty in
158 Some (name,Cic.Decl ty')::context'
159 | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
160 let bo' = change subst context'_len bo selected_bo in
162 match ty,selected_ty with
164 | Some ty,Some selected_ty ->
165 Some (change subst context'_len ty selected_ty)
166 | _,_ -> assert false
168 Some (name,Cic.Def (bo',ty'))::context'
169 | _,_ -> assert false
170 ) context selected_context [] in
173 | (n,_,_) when n = metano -> (metano,context',ty')
177 (curi,metasenv',pbo,pty), [metano]
179 mk_tactic (change_tac ~pattern ~with_what)
181 let fold_tac ~reduction ~term ~pattern =
182 let fold_tac ~reduction ~term ~pattern:(wanted,hyps_pat,concl_pat) status =
183 assert (wanted = None); (* this should be checked syntactically *)
184 let proof,goal = status in
185 let _,metasenv,_,_ = proof in
186 let _,context,_ = CicUtil.lookup_meta goal metasenv in
187 let reduced_term = reduction context term in
189 (change_tac ~pattern:(Some reduced_term,hyps_pat,concl_pat) term) status
191 mk_tactic (fold_tac ~reduction ~term ~pattern)