]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/declarative.ml
case tactic first tries with a simple outtype and then with a more sofisticated one
[helm.git] / helm / software / components / tactics / declarative.ml
1 (* Copyright (C) 2006, 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 type just = [ `Term of Cic.term | `Auto of Auto.auto_params ]
27
28 let mk_just ~dbd ~universe =
29  function
30     `Auto (l,params) -> 
31        Tactics.auto ~dbd 
32        ~params:(l,("skip_trie_filtering","1")::("skip_context","1")::params) ~universe
33   | `Term t -> Tactics.apply t
34 ;;
35
36 let assume id t =
37   Tacticals.then_
38      ~start:
39        (Tactics.intros ~howmany:1
40         ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
41      ~continuation:
42        (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
43          (fun _ metasenv ugraph -> t,metasenv,ugraph))
44 ;;
45
46 let suppose t id ty =
47 (*BUG: check on t missing *)
48  let ty = match ty with None -> t | Some ty -> ty in
49  Tacticals.then_
50    ~start:
51      (Tactics.intros ~howmany:1
52        ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
53    ~continuation:
54      (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)  
55       (fun _ metasenv ugraph -> ty,metasenv,ugraph))
56 ;;
57
58 let by_just_we_proved ~dbd ~universe just ty id ty' =
59  let just = mk_just ~dbd ~universe just in
60   match id with
61      None ->
62       (match ty' with
63           None -> assert false
64         | Some ty' ->
65            Tacticals.then_
66             ~start:(Tactics.change
67               ~pattern:(ProofEngineTypes.conclusion_pattern None)
68               (fun _ metasenv ugraph -> ty,metasenv,ugraph))
69             ~continuation:just
70       )
71    | Some id ->
72        let ty',continuation =
73         match ty' with
74            None -> ty,just
75          | Some ty' ->
76             ty',
77             Tacticals.then_
78              ~start:
79                (Tactics.change
80                  ~with_cast:true
81                  ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
82                  (fun _ metasenv ugraph -> ty,metasenv,ugraph))
83              ~continuation:just
84        in
85         Tacticals.thens
86         ~start:
87           (Tactics.cut ty'
88             ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
89         ~continuations:[ Tacticals.id_tac ; continuation ]
90 ;;
91
92 let bydone ~dbd ~universe just =
93  mk_just ~dbd ~universe just
94 ;;
95
96 let we_need_to_prove t id ty =
97  match id with
98     None ->
99      (match ty with
100          None -> Tacticals.id_tac (*BUG: check missing here *)
101        | Some ty ->
102           Tactics.change ~pattern:(ProofEngineTypes.conclusion_pattern None)
103            (fun _ metasenv ugraph -> ty,metasenv,ugraph))
104   | Some id ->
105      let aux status =
106       let cont,cutted =
107        match ty with
108           None -> Tacticals.id_tac,t
109         | Some ty ->
110            Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
111              (fun _ metasenv ugraph -> t,metasenv,ugraph), ty in
112       let proof,goals =
113        ProofEngineTypes.apply_tactic
114         (Tacticals.thens
115           ~start:
116            (Tactics.cut cutted
117              ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
118           ~continuations:[cont])
119         status
120       in
121        let goals' =
122         match goals with
123            [fst; snd] -> [snd; fst]
124          | _ -> assert false
125        in
126         proof,goals'
127      in
128       ProofEngineTypes.mk_tactic aux
129 ;;
130
131 let existselim ~dbd ~universe just id1 t1 id2 t2 =
132  let aux (proof, goal) = 
133   let (n,metasenv,_subst,bo,ty,attrs) = proof in
134   let metano,context,_ = CicUtil.lookup_meta goal metasenv in
135   let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
136   let proof' = (n,metasenv,_subst,bo,ty,attrs) in
137    ProofEngineTypes.apply_tactic (
138    Tacticals.thens
139     ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)]))
140     ~continuations:
141      [ Tactics.elim_intros (Cic.Rel 1)
142         ~mk_fresh_name_callback:
143           (let i = ref 0 in
144             fun _ _ _  ~typ ->
145              incr i;
146              if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
147        (mk_just ~dbd ~universe just)
148      ]) (proof', goal)
149  in
150   ProofEngineTypes.mk_tactic aux
151 ;;
152
153 let andelim ~dbd ~universe just id1 t1 id2 t2 = 
154    Tacticals.thens
155     ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/And.ind", 0, []); t1 ; t2]))
156     ~continuations:
157      [ Tactics.elim_intros (Cic.Rel 1)
158         ~mk_fresh_name_callback:
159           (let i = ref 0 in
160             fun _ _ _  ~typ ->
161              incr i;
162              if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
163        (mk_just ~dbd ~universe just) ]
164 ;;
165
166 let rewritingstep ~dbd ~universe lhs rhs just last_step =
167  let aux ((proof,goal) as status) =
168   let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in
169   let _,context,gty = CicUtil.lookup_meta goal metasenv in
170   let eq,trans =
171    match LibraryObjects.eq_URI () with
172       None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
173     | Some uri ->
174       Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
175   in
176   let ty,_ =
177    CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.oblivion_ugraph in
178   let just' =
179    match just with
180       `Auto (univ, params) ->
181         let params =
182          if not (List.exists (fun (k,_) -> k = "timeout") params) then
183           ("timeout","3")::params
184          else params
185         in
186         let params' =
187          if not (List.exists (fun (k,_) -> k = "paramodulation") params) then
188           ("paramodulation","1")::params
189          else params
190         in
191          if params = params' then
192           Tactics.auto ~dbd ~params:(univ, params) ~universe
193          else
194           Tacticals.first
195            [Tactics.auto ~dbd ~params:(univ, params) ~universe ;
196             Tactics.auto ~dbd ~params:(univ, params') ~universe]
197     | `Term just -> Tactics.apply just
198     | `SolveWith term -> 
199          Tactics.solve_rewrite ~universe ~params:([term],["steps","1"]) ()
200     | `Proof ->
201         Tacticals.id_tac
202   in
203    let plhs,prhs,prepare =
204     match lhs with
205        None ->
206         let plhs,prhs =
207          match gty with 
208             Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
209           | _ -> assert false
210         in
211          plhs,prhs,
212           (fun continuation ->
213             ProofEngineTypes.apply_tactic continuation status)
214      | Some (None,lhs) ->
215         let plhs,prhs =
216          match gty with 
217             Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
218           | _ -> assert false
219         in
220          (*CSC: manca check plhs convertibile con lhs *)
221          plhs,prhs,
222           (fun continuation ->
223             ProofEngineTypes.apply_tactic continuation status)
224      | Some (Some name,lhs) ->
225         let newmeta = CicMkImplicit.new_meta metasenv [] in
226         let irl =
227          CicMkImplicit.identity_relocation_list_for_metavariable context in
228         let plhs = lhs in
229         let prhs = Cic.Meta(newmeta,irl) in
230          plhs,prhs,
231           (fun continuation ->
232             let metasenv = (newmeta, context, ty)::metasenv in
233             let mk_fresh_name_callback =
234              fun metasenv context _ ~typ ->
235               FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context
236                (Cic.Name name) ~typ
237             in
238             let proof = curi,metasenv,_subst,proofbo,proofty, attrs in
239             let proof,goals =
240              ProofEngineTypes.apply_tactic
241               (Tacticals.thens
242                 ~start:(Tactics.cut ~mk_fresh_name_callback
243                  (Cic.Appl [eq ; ty ; lhs ; prhs]))
244                 ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal)
245             in
246              let goals =
247               match just,goals with
248                  `Proof, [g1;g2;g3] -> [g2;g3;newmeta;g1]
249                | _, [g1;g2] -> [g2;newmeta;g1]
250                | _, l -> 
251                  prerr_endline (String.concat "," (List.map string_of_int l));
252                  prerr_endline (CicMetaSubst.ppmetasenv [] metasenv);
253                  assert false
254              in
255               proof,goals)
256    in
257     let continuation =
258      if last_step then
259       (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
260       just'
261      else
262       Tacticals.thens
263        ~start:(Tactics.apply ~term:(Cic.Appl [trans;ty;plhs;rhs;prhs]))
264        ~continuations:[just' ; Tacticals.id_tac]
265     in
266      prepare continuation
267  in
268   ProofEngineTypes.mk_tactic aux
269 ;;
270
271 let we_proceed_by_cases_on t pat =
272  (*BUG here: pat unused *)
273  Tactics.cases_intros t
274 ;;
275
276 let we_proceed_by_induction_on t pat =
277  let pattern = None, [], Some pat in
278  Tactics.elim_intros ~depth:0 (*~pattern*) t
279 ;;
280
281 let case id ~params =
282  (*BUG here: id unused*)
283  (*BUG here: it does not verify that the previous branch is closed *)
284  (*BUG here: the params should be parsed telescopically*)
285  (*BUG here: the tactic_terms should be terms*)
286  let rec aux ~params ((proof,goal) as status) =
287   match params with
288      [] -> proof,[goal]
289    | (id,t)::tl ->
290       match ProofEngineTypes.apply_tactic (assume id t) status with
291          proof,[goal] -> aux tl (proof,goal)
292        | _ -> assert false
293  in
294   ProofEngineTypes.mk_tactic (aux ~params)
295 ;;
296
297 let thesisbecomes t =
298 let ty = None in
299  match ty with
300     None ->
301      Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
302       (fun _ metasenv ugraph -> t,metasenv,ugraph)
303   | Some ty ->
304      (*BUG here: missing check on t *)
305      Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
306       (fun _ metasenv ugraph -> ty,metasenv,ugraph)
307 ;;
308
309 let byinduction t id  = suppose t id None;;