]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/declarative.ml
attributes now in the proof status: commit 2
[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 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 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 ~universe lhs rhs just last_step =
138  let aux ((proof,goal) as status) =
139   let (curi,metasenv,proofbo,proofty, attrs) = proof in
140   let _,context,gty = 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       `Auto params ->
152         let params =
153          if not (List.exists (fun (k,_) -> k = "paramodulation") params) then
154           ("paramodulation","1")::params
155          else params in
156         let params =
157          if not (List.exists (fun (k,_) -> k = "timeout") params) then
158           ("timeout","3")::params
159          else params
160         in
161          Tactics.auto ~dbd ~params ~universe
162     | `Term just -> Tactics.apply just 
163   in
164    let plhs,prhs,prepare =
165     match lhs with
166        None ->
167         let plhs,prhs =
168          match gty with 
169             Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
170           | _ -> assert false
171         in
172          plhs,prhs,
173           (fun continuation ->
174             ProofEngineTypes.apply_tactic continuation status)
175      | Some (None,lhs) ->
176         let plhs,prhs =
177          match gty with 
178             Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
179           | _ -> assert false
180         in
181          (*CSC: manca check plhs convertibile con lhs *)
182          plhs,prhs,
183           (fun continuation ->
184             ProofEngineTypes.apply_tactic continuation status)
185      | Some (Some name,lhs) ->
186         let newmeta = CicMkImplicit.new_meta metasenv [] in
187         let irl =
188          CicMkImplicit.identity_relocation_list_for_metavariable context in
189         let plhs = lhs in
190         let prhs = Cic.Meta(newmeta,irl) in
191          plhs,prhs,
192           (fun continuation ->
193             let metasenv = (newmeta, context, ty)::metasenv in
194             let mk_fresh_name_callback =
195              fun metasenv context _ ~typ ->
196               FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context
197                (Cic.Name name) ~typ
198             in
199             let proof = curi,metasenv,proofbo,proofty, attrs in
200             let proof,goals =
201              ProofEngineTypes.apply_tactic
202               (Tacticals.thens
203                 ~start:(Tactics.cut ~mk_fresh_name_callback
204                  (Cic.Appl [eq ; ty ; lhs ; prhs]))
205                 ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal)
206             in
207              let goals =
208               match goals with
209                  [g1;g2] -> [g2;newmeta;g1]
210                | _ -> assert false
211              in
212               proof,goals)
213    in
214     let continuation =
215      if last_step then
216       (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*)
217       just
218      else
219       Tacticals.thens
220        ~start:(Tactics.apply ~term:(Cic.Appl [trans;ty;plhs;rhs;prhs]))
221        ~continuations:[just ; Tacticals.id_tac]
222     in
223      prepare continuation
224  in
225   ProofEngineTypes.mk_tactic aux
226 ;;
227
228 let we_proceed_by_cases_on t pat =
229  (*BUG here: pat unused *)
230  Tactics.cases_intros t
231 ;;
232
233 let we_proceed_by_induction_on t pat =
234  (*BUG here: pat unused *)
235  Tactics.elim_intros ~depth:0 t
236 ;;
237
238 let case id ~params =
239  (*BUG here: id unused*)
240  (*BUG here: it does not verify that the previous branch is closed *)
241  (*BUG here: the params should be parsed telescopically*)
242  (*BUG here: the tactic_terms should be terms*)
243  let rec aux ~params ((proof,goal) as status) =
244   match params with
245      [] -> proof,[goal]
246    | (id,t)::tl ->
247       match ProofEngineTypes.apply_tactic (assume id t) status with
248          proof,[goal] -> aux tl (proof,goal)
249        | _ -> assert false
250  in
251   ProofEngineTypes.mk_tactic (aux ~params)
252 ;;
253
254 let thesisbecomes t =
255 let ty = None in
256  match ty with
257     None ->
258      Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
259       (fun _ metasenv ugraph -> t,metasenv,ugraph)
260   | Some ty ->
261      (*BUG here: missing check on t *)
262      Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
263       (fun _ metasenv ugraph -> ty,metasenv,ugraph)
264 ;;
265
266 let byinduction t id  = suppose t id None;;