]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/proofEngine.ml
draft version of locate_in_term
[helm.git] / helm / gTopLevel / proofEngine.ml
1 (* Copyright (C) 2000, 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 open ProofEngineHelpers
27 open ProofEngineTypes
28
29   (* proof assistant status *)
30
31 let proof = ref (None : proof option)
32 let goal = ref (None : goal option)
33
34 let get_proof () = !proof;;
35 let set_proof p = proof := p;;
36
37 let get_current_status_as_xml () =
38   match get_proof () with
39      None -> assert false
40    | Some (uri, metasenv, bo, ty) ->
41       let uri = match uri with Some uri -> uri | None -> assert false in
42       let currentproof =
43        (*CSC: Wrong: [] is just plainly wrong *)
44        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[])
45       in
46        let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
47         Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
48        in
49         let xml, bodyxml =
50          match
51           Cic2Xml.print_object uri ~ids_to_inner_sorts
52            ~ask_dtd_to_the_getter:true acurrentproof
53          with
54             xml,Some bodyxml -> xml,bodyxml
55           | _,None -> assert false
56         in
57          (xml, bodyxml)
58 ;;
59
60 let apply_tactic ~tactic =
61  let module PET = ProofEngineTypes in
62  match get_proof (),!goal with
63   | None,_
64   | _,None -> assert false
65   | Some proof', Some goal' ->
66      let (newproof, newgoals) = PET.apply_tactic tactic (proof', goal') in
67       set_proof (Some newproof);
68       goal :=
69        (match newgoals, newproof with
70            goal::_, _ -> Some goal
71          | [], (_,(goal,_,_)::_,_,_) ->
72          (* the tactic left no open goal ; let's choose the first open goal *)
73          (*CSC: here we could implement and use a proof-tree like notion... *)
74             Some goal
75          | _, _ -> None)
76 ;;
77
78 (* metas_in_term term                                                *)
79 (* Returns the ordered list of the metas that occur in [term].       *)
80 (* Duplicates are removed. The implementation is not very efficient. *)
81 let metas_in_term term =
82  let module C = Cic in
83   let rec aux =
84    function
85       C.Rel _ -> []
86     | C.Meta (n,_) -> [n]
87     | C.Sort _
88     | C.Implicit _ -> []
89     | C.Cast (te,ty) -> (aux te) @ (aux ty)
90     | C.Prod (_,s,t) -> (aux s) @ (aux t)
91     | C.Lambda (_,s,t) -> (aux s) @ (aux t)
92     | C.LetIn (_,s,t) -> (aux s) @ (aux t)
93     | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
94     | C.Var (_,exp_named_subst)
95     | C.Const (_,exp_named_subst)
96     | C.MutInd (_,_,exp_named_subst)
97     | C.MutConstruct (_,_,_,exp_named_subst) ->
98        List.fold_left (fun i (_,t) -> i @ (aux t)) [] exp_named_subst
99     | C.MutCase (_,_,outt,t,pl) ->
100        (aux outt) @ (aux t) @
101         (List.fold_left (fun i t -> i @ (aux t)) [] pl)
102     | C.Fix (_,fl) ->
103         List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
104     | C.CoFix (_,fl) ->
105         List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
106   in
107    let metas = aux term in
108     let rec elim_duplicates =
109      function
110         [] -> []
111       | he::tl ->
112          he::(elim_duplicates (List.filter (function el -> he <> el) tl))
113     in
114      elim_duplicates metas
115
116 (* perforate context term ty                                                 *)
117 (* replaces the term [term] in the proof with a new metavariable whose type  *)
118 (* is [ty]. [context] must be the context of [term] in the whole proof. This *)
119 (* could be easily computed; so the only reasons to have it as an argument   *)
120 (* are efficiency reasons.                                                   *)
121 let perforate context term ty =
122  let module C = Cic in
123   match get_proof () with
124      None -> assert false
125    | Some (uri,metasenv,bo,gty as proof') ->
126       let newmeta = new_meta_of_proof proof' in
127        (* We push the new meta at the end of the list for pretty-printing *)
128        (* purposes: in this way metas are ordered.                        *)
129        let metasenv' = metasenv@[newmeta,context,ty] in
130         let irl =
131           CicMkImplicit.identity_relocation_list_for_metavariable context
132         in
133 (*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
134         let bo' =
135          ProofEngineReduction.replace (==) [term] [C.Meta (newmeta,irl)] bo
136         in
137         (* It may be possible that some metavariables occurred only in *)
138         (* the term we are perforating and they now occurs no more. We *)
139         (* get rid of them, collecting the really useful metavariables *)
140         (* in metasenv''.                                              *)
141 (*CSC: Bug: una meta potrebbe non comparire in bo', ma comparire nel tipo *)
142 (*CSC: di una metavariabile che compare in bo'!!!!!!!                     *)
143          let newmetas = metas_in_term bo' in
144           let metasenv'' =
145            List.filter (function (n,_,_) -> List.mem n newmetas) metasenv'
146           in
147            set_proof (Some (uri,metasenv'',bo',gty)) ;
148            goal := Some newmeta
149
150
151 (************************************************************)
152 (*                  Some easy tactics.                      *)
153 (************************************************************)
154
155 (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
156 let reduction_tactic_in_scratch reduction_function terms ty =
157  let metasenv =
158   match get_proof () with
159      None -> []
160    | Some (_,metasenv,_,_) -> metasenv
161  in
162  let metano,context,_ =
163   match !goal with
164      None -> assert false
165    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
166  in
167   let terms' = List.map (reduction_function context) terms in
168    ProofEngineReduction.replace
169     ~equality:(==) ~what:terms ~with_what:terms' ~where:ty
170 ;;
171
172 let whd_in_scratch    = reduction_tactic_in_scratch CicReduction.whd
173 let reduce_in_scratch = reduction_tactic_in_scratch ProofEngineReduction.reduce
174 let simpl_in_scratch  = reduction_tactic_in_scratch ProofEngineReduction.simpl
175
176 (************************************************************)
177 (*              Tactics defined elsewhere                   *)
178 (************************************************************)
179
180   (* primitive tactics *)
181
182 let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
183 let intros ?mk_fresh_name_callback () =
184  apply_tactic (PrimitiveTactics.intros_tac ?mk_fresh_name_callback ())
185 let cut ?mk_fresh_name_callback term =
186  apply_tactic (PrimitiveTactics.cut_tac ?mk_fresh_name_callback ~term)
187 let letin ?mk_fresh_name_callback term =
188  apply_tactic (PrimitiveTactics.letin_tac ?mk_fresh_name_callback ~term)
189 let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)
190 let elim_intros_simpl term =
191   apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term)
192 let change ~goal_input:what ~input:with_what =
193   apply_tactic (PrimitiveTactics.change_tac ~what ~with_what)
194
195   (* structural tactics *)
196
197 let clearbody hyp = apply_tactic (ProofEngineStructuralRules.clearbody ~hyp)
198 let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp)
199
200   (* reduction tactics *)
201
202 let whd terms =
203  apply_tactic
204   (ReductionTactics.whd_tac ~also_in_hypotheses:true ~terms:(Some terms))
205 let reduce terms =
206  apply_tactic
207   (ReductionTactics.reduce_tac ~also_in_hypotheses:true ~terms:(Some terms))
208 let simpl terms =
209  apply_tactic
210   (ReductionTactics.simpl_tac ~also_in_hypotheses:true ~terms:(Some terms))
211
212 let fold_whd term =
213  apply_tactic
214   (ReductionTactics.fold_tac ~reduction:CicReduction.whd
215     ~also_in_hypotheses:true ~term)
216 let fold_reduce term =
217  apply_tactic
218   (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.reduce
219     ~also_in_hypotheses:true ~term)
220 let fold_simpl term =
221  apply_tactic
222   (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.simpl
223     ~also_in_hypotheses:true ~term)
224
225   (* other tactics *)
226
227 let elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term)
228 let ring () = apply_tactic Ring.ring_tac
229 let fourier () = apply_tactic FourierR.fourier_tac
230
231 (* let auto ~dbd () = apply_tactic (AutoTactic.auto_tac ~dbd) *)
232 let auto ~dbd () = apply_tactic (AutoTactic.auto_tac_new ~dbd)
233
234
235 let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term)
236 let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term)
237 let replace ~goal_input:what ~input:with_what = 
238   apply_tactic (EqualityTactics.replace_tac ~what ~with_what)
239
240 let reflexivity () = apply_tactic EqualityTactics.reflexivity_tac
241 let symmetry () = apply_tactic EqualityTactics.symmetry_tac
242 let transitivity term = apply_tactic (EqualityTactics.transitivity_tac ~term)
243
244 let exists () = apply_tactic IntroductionTactics.exists_tac
245 let split () = apply_tactic IntroductionTactics.split_tac 
246 let left () = apply_tactic IntroductionTactics.left_tac
247 let right () = apply_tactic IntroductionTactics.right_tac
248
249 let assumption () = apply_tactic VariousTactics.assumption_tac
250
251 let generalize ?mk_fresh_name_callback terms =
252  apply_tactic (VariousTactics.generalize_tac ?mk_fresh_name_callback terms)
253
254 let absurd term = apply_tactic (NegationTactics.absurd_tac ~term)
255 let contradiction () = apply_tactic NegationTactics.contradiction_tac
256
257 let decompose ~uris_choice_callback term =
258  apply_tactic (EliminationTactics.decompose_tac ~uris_choice_callback term)
259
260 let injection term = apply_tactic (DiscriminationTactics.injection_tac ~term)
261 let discriminate term = apply_tactic (DiscriminationTactics.discriminate_tac ~term)
262 let decide_equality () = apply_tactic DiscriminationTactics.decide_equality_tac
263 let compare term = apply_tactic (DiscriminationTactics.compare_tac ~term)
264
265 (*
266 let prova_tatticali () = apply_tactic Tacticals.prova_tac
267 *)
268