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 where terms =
34 if terms = [] then where
37 List.split (List.map (fun (context, t) -> t, reduction context t) terms)
39 ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
41 let (selected_context,selected_ty) =
42 ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
43 let ty' = change ty selected_ty in
46 (fun entry selected_entry context' ->
47 match entry,selected_entry with
48 None,None -> None::context'
49 | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
50 let ty' = change ty selected_ty in
51 Some (name,Cic.Decl ty')::context'
52 | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
53 let bo' = change bo selected_bo in
55 match ty,selected_ty with
57 | Some ty,Some selected_ty -> Some (change ty selected_ty)
60 Some (name,Cic.Def (bo',ty'))::context'
62 ) context selected_context [] in
65 | (n,_,_) when n = metano -> (metano,context',ty')
69 (curi,metasenv',pbo,pty), [metano]
72 let simpl_tac ~pattern =
73 mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);;
75 let reduce_tac ~pattern =
76 mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);;
78 let whd_tac ~pattern =
79 mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);;
81 let normalize_tac ~pattern =
82 mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern);;
84 exception NotConvertible
86 (* Note: this code is almost identical to reduction_tac and
87 * it could be unified by making the change function a callback *)
88 (* CSC: with_what is parsed in the context of the goal, but it should replace
89 something that lives in a completely different context. Thus we
90 perform a delift + lift phase to move it in the right context. However,
91 in this way the tactic is less powerful than expected: with_what cannot
92 reference variables that are local to the term that is going to be
93 replaced. To fix this we should parse with_what in the context of the
94 term(s) to be replaced. *)
95 let change_tac ~pattern with_what =
96 let change_tac ~pattern ~with_what (proof, goal) =
97 let curi,metasenv,pbo,pty = proof in
98 let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
99 let context_len = List.length context in
100 let change context'_len where terms =
101 if terms = [] then where
106 (fun (context_of_t, t) ->
107 let context_of_t_len = List.length context_of_t in
108 let with_what_in_context' =
109 if context_len > context'_len then
111 let with_what,subst,metasenv' =
112 CicMetaSubst.delift_rels [] metasenv
113 (context_len - context'_len) with_what
116 assert (metasenv = metasenv');
121 let with_what_in_context_of_t =
122 if context_of_t_len > context'_len then
123 CicSubstitution.lift (context_of_t_len - context'_len)
124 with_what_in_context'
128 CicTypeChecker.type_of_aux' metasenv context_of_t with_what
129 CicUniv.empty_ugraph in
131 CicReduction.are_convertible ~metasenv context_of_t t with_what u in
133 t, with_what_in_context_of_t
135 raise NotConvertible) terms)
137 ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
139 let (selected_context,selected_ty) =
140 ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
141 let ty' = change context_len ty selected_ty in
144 (fun entry selected_entry context' ->
145 let context'_len = List.length context' in
146 match entry,selected_entry with
147 None,None -> None::context'
148 | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
149 let ty' = change context'_len ty selected_ty in
150 Some (name,Cic.Decl ty')::context'
151 | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
152 let bo' = change context'_len bo selected_bo in
154 match ty,selected_ty with
156 | Some ty,Some selected_ty ->
157 Some (change context'_len ty selected_ty)
158 | _,_ -> assert false
160 Some (name,Cic.Def (bo',ty'))::context'
161 | _,_ -> assert false
162 ) context selected_context [] in
165 | (n,_,_) when n = metano -> (metano,context',ty')
169 (curi,metasenv',pbo,pty), [metano]
171 mk_tactic (change_tac ~pattern ~with_what)
173 let fold_tac ~reduction ~term ~pattern =
174 let fold_tac ~reduction ~term ~pattern:(wanted,hyps_pat,concl_pat) status =
175 assert (wanted = None); (* this should be checked syntactically *)
176 let proof,goal = status in
177 let _,metasenv,_,_ = proof in
178 let _,context,_ = CicUtil.lookup_meta goal metasenv in
179 let reduced_term = reduction context term in
181 (change_tac ~pattern:(Some reduced_term,hyps_pat,concl_pat) term) status
183 mk_tactic (fold_tac ~reduction ~term ~pattern)