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