1 (* Copyright (C) 2000, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 open ProofEngineHelpers
29 (* proof assistant status *)
31 let proof = ref (None : proof)
32 let goal = ref (None : goal)
34 let apply_tactic ~tactic:tactic =
35 let (newproof, newgoal) = tactic ~status:(!proof, !goal) in
39 (* metas_in_term term *)
40 (* Returns the ordered list of the metas that occur in [term]. *)
41 (* Duplicates are removed. The implementation is not very efficient. *)
42 let metas_in_term term =
51 | C.Cast (te,ty) -> (aux te) @ (aux ty)
52 | C.Prod (_,s,t) -> (aux s) @ (aux t)
53 | C.Lambda (_,s,t) -> (aux s) @ (aux t)
54 | C.LetIn (_,s,t) -> (aux s) @ (aux t)
55 | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
58 | C.MutConstruct _ -> []
59 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
60 (aux outt) @ (aux t) @
61 (List.fold_left (fun i t -> i @ (aux t)) [] pl)
63 List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
65 List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
67 let metas = aux term in
68 let rec elim_duplicates =
72 he::(elim_duplicates (List.filter (function el -> he <> el) tl))
76 (* perforate context term ty *)
77 (* replaces the term [term] in the proof with a new metavariable whose type *)
78 (* is [ty]. [context] must be the context of [term] in the whole proof. This *)
79 (* could be easily computed; so the only reasons to have it as an argument *)
80 (* are efficiency reasons. *)
81 let perforate context term ty =
83 let newmeta = new_meta !proof in
86 | Some (uri,metasenv,bo,gty) ->
87 (* We push the new meta at the end of the list for pretty-printing *)
88 (* purposes: in this way metas are ordered. *)
89 let metasenv' = metasenv@[newmeta,context,ty] in
90 let irl = identity_relocation_list_for_metavariable context in
91 (*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
93 ProofEngineReduction.replace (==) term (C.Meta (newmeta,irl)) bo
95 (* It may be possible that some metavariables occurred only in *)
96 (* the term we are perforating and they now occurs no more. We *)
97 (* get rid of them, collecting the really useful metavariables *)
99 (*CSC: Bug: una meta potrebbe non comparire in bo', ma comparire nel tipo *)
100 (*CSC: di una metavariabile che compare in bo'!!!!!!! *)
101 let newmetas = metas_in_term bo' in
103 List.filter (function (n,_,_) -> List.mem n newmetas) metasenv'
105 proof := Some (uri,metasenv'',bo',gty) ;
109 (************************************************************)
110 (* Some easy tactics. *)
111 (************************************************************)
113 (*CSC: generatore di nomi? Chiedere il nome? *)
115 let next_fresh_index = ref 0
118 incr next_fresh_index ;
119 "fresh_name" ^ string_of_int !next_fresh_index
121 let reduction_tactic reduction_function term =
122 let curi,metasenv,pbo,pty =
125 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
127 let metano,context,ty =
130 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
132 (* We don't know if [term] is a subterm of [ty] or a subterm of *)
133 (* the type of one metavariable. So we replace it everywhere. *)
134 (*CSC: Il vero problema e' che non sapendo dove sia il term non *)
135 (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *)
136 (*CSC: e' meglio prima cercare il termine e scoprirne il *)
137 (*CSC: contesto, poi ridurre e infine rimpiazzare. *)
138 let replace context where=
139 (*CSC: Per il momento se la riduzione fallisce significa solamente che *)
140 (*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *)
141 (*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *)
143 let term' = reduction_function context term in
144 ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term'
149 let ty' = replace context ty in
152 (fun entry context ->
154 Some (name,Cic.Def t) ->
155 (Some (name,Cic.Def (replace context t)))::context
156 | Some (name,Cic.Decl t) ->
157 (Some (name,Cic.Decl (replace context t)))::context
158 | None -> None::context
164 (n,_,_) when n = metano -> (metano,context',ty')
168 proof := Some (curi,metasenv',pbo,pty) ;
171 (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
172 let reduction_tactic_in_scratch reduction_function term ty =
176 | Some (_,metasenv,_,_) -> metasenv
178 let metano,context,_ =
181 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
183 let term' = reduction_function context term in
184 ProofEngineReduction.replace
185 ~equality:(==) ~what:term ~with_what:term' ~where:ty
187 let whd = reduction_tactic CicReduction.whd
188 let reduce = reduction_tactic ProofEngineReduction.reduce
189 let simpl = reduction_tactic ProofEngineReduction.simpl
191 let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd
192 let reduce_in_scratch =
193 reduction_tactic_in_scratch ProofEngineReduction.reduce
194 let simpl_in_scratch =
195 reduction_tactic_in_scratch ProofEngineReduction.simpl
197 (* It is just the opposite of whd. The code should probably be merged. *)
199 let curi,metasenv,pbo,pty =
202 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
204 let metano,context,ty =
207 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
209 let term' = CicReduction.whd context term in
210 (* We don't know if [term] is a subterm of [ty] or a subterm of *)
211 (* the type of one metavariable. So we replace it everywhere. *)
212 (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
213 (*CSC: che si guadagni nulla in fatto di efficienza. *)
215 ProofEngineReduction.replace
216 ~equality:(ProofEngineReduction.syntactic_equality)
217 ~what:term' ~with_what:term
219 let ty' = replace ty in
223 Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
224 | Some (n,Cic.Def t) -> Some (n,Cic.Def (replace t))
231 (n,_,_) when n = metano -> (metano,context',ty')
235 proof := Some (curi,metasenv',pbo,pty) ;
238 exception NotConvertible
240 (*CSC: Bug (or feature?). [input] is parsed in the context of the goal, *)
241 (*CSC: while [goal_input] can have a richer context (because of binders) *)
242 (*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
243 (*CSC: Is that evident? Is that right? Or should it be changed? *)
244 let change ~goal_input ~input =
245 let curi,metasenv,pbo,pty =
248 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
250 let metano,context,ty =
253 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
255 (* are_convertible works only on well-typed terms *)
256 ignore (CicTypeChecker.type_of_aux' metasenv context input) ;
257 if CicReduction.are_convertible context goal_input input then
260 ProofEngineReduction.replace
261 ~equality:(==) ~what:goal_input ~with_what:input
263 let ty' = replace ty in
267 Some (name,Cic.Def t) -> Some (name,Cic.Def (replace t))
268 | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
275 (n,_,_) when n = metano -> (metano,context',ty')
279 proof := Some (curi,metasenv',pbo,pty) ;
285 (************************************************************)
286 (* Tactics defined elsewhere *)
287 (************************************************************)
289 (* primitive tactics *)
291 let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
293 apply_tactic (PrimitiveTactics.intros_tac ~name:(fresh_name ()))
294 let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term)
295 let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term)
296 let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)
297 let elim_intros_simpl term =
298 apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term)
300 (* structural tactics *)
302 let clearbody hyp = apply_tactic (ProofEngineStructuralRules.clearbody ~hyp)
303 let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp)
307 let elim_type term = apply_tactic (Ring.elim_type_tac ~term)
308 let ring () = apply_tactic Ring.ring_tac