]> matita.cs.unibo.it Git - helm.git/blob - components/tactics/declarative.ml
Up to absolute value
[helm.git] / 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 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 t ty id ty' =
49  let just =
50   match t with
51      None -> Tactics.auto ~dbd ~params:[]
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 t =
81  let just =
82   match t with
83      None -> Tactics.auto ~dbd ~params:[]
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 t id1 t1 id2 t2 =
125 (*BUG: t1 and t2 not used *)
126 (*PARSING BUG: t2 is parsed in the current context, but it may
127   have occurrences of id1 in it *)
128  Tactics.elim_intros t
129   ~mk_fresh_name_callback:
130     (let i = ref 0 in
131       fun _ _ _  ~typ ->
132        incr i;
133        if !i = 1 then Cic.Name id1 else Cic.Name id2)
134
135 let andelim = existselim;;
136
137 let rewritingstep ~dbd lhs rhs just conclude =
138  let aux ((proof,goal) as status) =
139   let (curi,metasenv,proofbo,proofty) = proof in
140   let _,context,_ = CicUtil.lookup_meta goal metasenv in
141   let eq,trans =
142    match LibraryObjects.eq_URI () with
143       None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
144     | Some uri ->
145       Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
146   in
147   let ty,_ =
148    CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
149   let just =
150    match just with
151       None ->
152        Tactics.auto ~dbd
153         ~params:["paramodulation","1"; "timeout","3"]
154     | Some just -> Tactics.apply just
155   in
156    match lhs with
157       None ->
158        let plhs,prhs =
159         match 
160          fst
161           (CicTypeChecker.type_of_aux' metasenv context (Cic.Rel 1)
162             CicUniv.empty_ugraph)
163         with
164            Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
165          | _ -> assert false in
166        let last_hyp_name =
167         match context with
168            (Some (Cic.Name id,_))::_ -> id
169          | _ -> assert false
170        in
171         (match conclude with
172             None ->
173              ProofEngineTypes.apply_tactic
174               (Tacticals.thens
175                 ~start:(Tactics.apply ~term:trans)
176                 ~continuations:
177                   [ Tactics.apply prhs ;
178                     Tactics.apply (Cic.Rel 1) ;
179                     just]) status
180           | Some name ->
181              let mk_fresh_name_callback =
182               fun metasenv context _ ~typ ->
183                 FreshNamesGenerator.mk_fresh_name ~subst:[]
184                  metasenv context name ~typ
185              in
186               ProofEngineTypes.apply_tactic
187                (Tacticals.thens
188                  ~start:(Tactics.cut ~mk_fresh_name_callback
189                   (Cic.Appl [eq ; ty ; plhs ; rhs]))
190                  ~continuations:
191                    [ Tactics.clear ~hyps:[last_hyp_name] ;
192                      Tacticals.thens
193                       ~start:(Tactics.apply ~term:trans)
194                       ~continuations:
195                         [ Tactics.apply prhs ;
196                           Tactics.apply (Cic.Rel 1) ;
197                           just]
198                    ]) status)
199     | Some lhs ->
200        match conclude with
201           None -> ProofEngineTypes.apply_tactic just status
202         | Some name ->
203             let mk_fresh_name_callback =
204              fun metasenv context _ ~typ ->
205                FreshNamesGenerator.mk_fresh_name ~subst:[]
206                 metasenv context name ~typ
207             in
208              ProofEngineTypes.apply_tactic
209               (Tacticals.thens
210                 ~start:
211                   (Tactics.cut ~mk_fresh_name_callback
212                     (Cic.Appl [eq ; ty ; lhs ; rhs]))
213                 ~continuations:[ Tacticals.id_tac ; just ]) status
214  in
215   ProofEngineTypes.mk_tactic aux
216 ;;
217
218 let we_proceed_by_induction_on t pat =
219  (*BUG here: pat unused *)
220  Tactics.elim_intros ~depth:0 t
221 ;;
222
223 let case id ~params =
224  (*BUG here: id unused*)
225  (*BUG here: it does not verify that the previous branch is closed *)
226  (*BUG here: the params should be parsed telescopically*)
227  (*BUG here: the tactic_terms should be terms*)
228  let rec aux ~params ((proof,goal) as status) =
229   match params with
230      [] -> proof,[goal]
231    | (id,t)::tl ->
232       match ProofEngineTypes.apply_tactic (assume id t) status with
233          proof,[goal] -> aux tl (proof,goal)
234        | _ -> assert false
235  in
236   ProofEngineTypes.mk_tactic (aux ~params)
237 ;;
238
239 let thesisbecomes t =
240 let ty = None in
241  (*BUG here: missing check on t *)
242  match ty with
243     None -> Tacticals.id_tac
244   | Some ty ->
245      Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
246       (fun _ metasenv ugraph -> ty,metasenv,ugraph)
247 ;;
248
249 let byinduction t id  = suppose t id None;;