]> matita.cs.unibo.it Git - helm.git/blob - components/tactics/reductionTactics.ml
Up to absolute value
[helm.git] / components / tactics / reductionTactics.ml
1 (* Copyright (C) 2002, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (* $Id$ *)
27
28 open ProofEngineTypes
29
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,pbo,pty = 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
37    else
38      let pairs, metasenv, ugraph =
39        List.fold_left
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)
44         terms
45      in
46      let terms, terms' = List.split pairs in
47      let where' =
48        ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
49         ~where:where
50      in
51      CicMetaSubst.apply_subst subst where', metasenv, ugraph
52   in
53   let (subst,metasenv,ugraph,selected_context,selected_ty) =
54     ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
55       ~conjecture ~pattern
56   in
57   let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
58   let context', metasenv, ugraph =
59    List.fold_right2
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
66           in
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
71           in
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
78                 in
79                 Some ty', metasenv, ugraph
80             | _,_ -> assert false
81           in
82            (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
83        | _,_ -> assert false
84     ) context selected_context ([], metasenv, ugraph) in
85   let metasenv' = 
86     List.map (function 
87       | (n,_,_) when n = metano -> (metano,context',ty')
88       | _ as t -> t
89     ) metasenv
90   in
91   (curi,metasenv',pbo,pty), [metano]
92 ;;
93
94 let simpl_tac ~pattern =
95  mk_tactic (reduction_tac
96   ~reduction:(const_lazy_reduction ProofEngineReduction.simpl) ~pattern)
97
98 let reduce_tac ~pattern =
99  mk_tactic (reduction_tac
100   ~reduction:(const_lazy_reduction ProofEngineReduction.reduce) ~pattern)
101
102 let unfold_tac what ~pattern =
103   let reduction =
104     match what with
105     | None -> const_lazy_reduction (ProofEngineReduction.unfold ?what:None)
106     | Some lazy_term ->
107         (fun context metasenv ugraph ->
108           let what, metasenv, ugraph = lazy_term context metasenv ugraph in
109           ProofEngineReduction.unfold ~what, metasenv, ugraph)
110   in
111   mk_tactic (reduction_tac ~reduction ~pattern)
112   
113 let whd_tac ~pattern =
114  mk_tactic (reduction_tac
115   ~reduction:(const_lazy_reduction CicReduction.whd) ~pattern)
116
117 let normalize_tac ~pattern =
118  mk_tactic (reduction_tac
119   ~reduction:(const_lazy_reduction CicReduction.normalize) ~pattern)
120
121 exception NotConvertible
122
123 (* Note: this code is almost identical to reduction_tac and
124 *  it could be unified by making the change function a callback *)
125 (* CSC: with_what is parsed in the context of the goal, but it should replace
126         something that lives in a completely different context. Thus we
127         perform a delift + lift phase to move it in the right context. However,
128         in this way the tactic is less powerful than expected: with_what cannot
129         reference variables that are local to the term that is going to be
130         replaced. To fix this we should parse with_what in the context of the
131         term(s) to be replaced. *)
132 let change_tac ~pattern with_what  =
133  let change_tac ~pattern ~with_what (proof, goal) =
134   let curi,metasenv,pbo,pty = proof in
135   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
136   let change subst where terms metasenv ugraph =
137    if terms = [] then where, metasenv, ugraph
138    else
139     let pairs, metasenv, ugraph =
140       List.fold_left
141         (fun (pairs, metasenv, ugraph) (context_of_t, t) ->
142           let with_what, metasenv, ugraph =
143             with_what context_of_t metasenv ugraph
144           in
145           let _,u =
146             CicTypeChecker.type_of_aux' metasenv context_of_t with_what ugraph
147           in
148           let b,_ =
149            CicReduction.are_convertible ~metasenv context_of_t t with_what u
150           in
151           if b then
152            ((t, with_what) :: pairs), metasenv, ugraph
153           else
154            raise NotConvertible)
155         ([], metasenv, ugraph)
156         terms
157     in
158     let terms, terms' = List.split pairs in
159      let where' =
160       ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
161        ~where:where
162      in
163       CicMetaSubst.apply_subst subst where', metasenv, ugraph
164   in
165   let (subst,metasenv,ugraph,selected_context,selected_ty) =
166    ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture
167     ~pattern in
168   let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
169   let context', metasenv, ugraph =
170    List.fold_right2
171     (fun entry selected_entry (context', metasenv, ugraph) ->
172      match entry,selected_entry with
173          None,None -> (None::context'), metasenv, ugraph
174        | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
175           let ty', metasenv, ugraph =
176             change subst ty selected_ty metasenv ugraph
177           in
178            (Some (name,Cic.Decl ty')::context'), metasenv, ugraph
179        | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
180           let bo', metasenv, ugraph =
181             change subst bo selected_bo metasenv ugraph
182           in
183           let ty', metasenv, ugraph =
184            match ty,selected_ty with
185               None,None -> None, metasenv, ugraph
186             | Some ty,Some selected_ty ->
187                 let ty', metasenv, ugraph =
188                   change subst ty selected_ty metasenv ugraph
189                 in
190                 Some ty', metasenv, ugraph
191             | _,_ -> assert false
192           in
193            (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
194        | _,_ -> assert false
195     ) context selected_context ([], metasenv, ugraph) in
196   let metasenv' = 
197     List.map
198       (function 
199         | (n,_,_) when n = metano -> (metano,context',ty')
200         | _ as t -> t)
201       metasenv
202   in
203   (curi,metasenv',pbo,pty), [metano]
204   in
205     mk_tactic (change_tac ~pattern ~with_what)
206
207 let fold_tac ~reduction ~term ~pattern =
208  let fold_tac ~reduction ~term ~pattern:(wanted,hyps_pat,concl_pat) status =
209   assert (wanted = None); (* this should be checked syntactically *)
210   let reduced_term =
211     (fun context metasenv ugraph ->
212       let term, metasenv, ugraph = term context metasenv ugraph in
213       let reduction, metasenv, ugraph = reduction context metasenv ugraph in
214       reduction context term, metasenv, ugraph)
215   in
216    apply_tactic
217     (change_tac ~pattern:(Some reduced_term,hyps_pat,concl_pat) term) status
218  in
219   mk_tactic (fold_tac ~reduction ~term ~pattern)
220