1 (* Copyright (C) 2002, 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 exception Bad_pattern of string
28 let new_meta_of_proof ~proof:(_, metasenv, _, _) =
29 CicMkImplicit.new_meta metasenv []
31 let subst_meta_in_proof proof meta term newmetasenv =
32 let uri,metasenv,bo,ty = proof in
33 (* empty context is ok for term since it wont be used by apply_subst *)
34 (* hack: since we do not know the context and the type of term, we
35 create a substitution with cc =[] and type = Implicit; they will be
36 in any case dropped by apply_subst, but it would be better to rewrite
37 the code. Cannot we just use apply_subst_metasenv, etc. ?? *)
38 let subst_in = CicMetaSubst.apply_subst [meta,([], term,Cic.Implicit None)] in
40 newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
44 (function i,canonical_context,ty ->
45 let canonical_context' =
48 Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
49 | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
51 | Some (_,Cic.Def (_,Some _)) -> assert false
54 i,canonical_context',(subst_in ty)
57 let bo' = subst_in bo in
58 (* Metavariables can appear also in the *statement* of the theorem
59 * since the parser does not reject as statements terms with
60 * metavariable therein *)
61 let ty' = subst_in ty in
62 let newproof = uri,metasenv'',bo',ty' in
63 (newproof, metasenv'')
65 (*CSC: commento vecchio *)
66 (* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv *)
67 (* This (heavy) function must be called when a tactic can instantiate old *)
68 (* metavariables (i.e. existential variables). It substitues the metasenv *)
69 (* of the proof with the result of removing [meta] from the domain of *)
70 (* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
71 (* in the current proof. Finally it applies [apply_subst_replacing] to *)
73 (*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
74 (*CSC: ci ripasso sopra apply_subst!!! *)
75 (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
76 (*CSC: [newmetasenv]. *)
77 let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
78 let (uri,_,bo,ty) = proof in
79 let bo' = subst_in bo in
80 (* Metavariables can appear also in the *statement* of the theorem
81 * since the parser does not reject as statements terms with
82 * metavariable therein *)
83 let ty' = subst_in ty in
86 (fun metasenv_entry i ->
87 match metasenv_entry with
88 (m,canonical_context,ty) when m <> meta ->
89 let canonical_context' =
93 | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
94 | Some (i,Cic.Def (t,None)) ->
95 Some (i,Cic.Def ((subst_in t),None))
96 | Some (_,Cic.Def (_,Some _)) -> assert false
99 (m,canonical_context',subst_in ty)::i
103 let newproof = uri,metasenv',bo',ty' in
104 (newproof, metasenv')
106 let compare_metasenvs ~oldmetasenv ~newmetasenv =
107 List.map (function (i,_,_) -> i)
110 not (List.exists (fun (j,_,_) -> i=j) oldmetasenv)) newmetasenv)
113 (** finds the _pointers_ to subterms that are alpha-equivalent to wanted in t *)
114 let find_subterms ~wanted ~context t =
115 let rec find context w t =
116 if ProofEngineReduction.alpha_equivalence w t then
122 | Cic.Meta (_, ctx) ->
127 | Some t -> find context w t @ acc
129 | Cic.Lambda (name, t1, t2)
130 | Cic.Prod (name, t1, t2) ->
132 find (Some (name, Cic.Decl t1)::context)
133 (CicSubstitution.lift 1 w) t2
134 | Cic.LetIn (name, t1, t2) ->
136 find (Some (name, Cic.Def (t1,None))::context)
137 (CicSubstitution.lift 1 w) t2
139 List.fold_left (fun acc t -> find context w t @ acc) [] l
140 | Cic.Cast (t, ty) -> find context w t @ find context w ty
141 | Cic.Implicit _ -> assert false
142 | Cic.Const (_, esubst)
143 | Cic.Var (_, esubst)
144 | Cic.MutInd (_, _, esubst)
145 | Cic.MutConstruct (_, _, _, esubst) ->
146 List.fold_left (fun acc (_, t) -> find context w t @ acc) [] esubst
147 | Cic.MutCase (_, _, outty, indterm, patterns) ->
148 find context w outty @ find context w indterm @
149 List.fold_left (fun acc p -> find context w p @ acc) [] patterns
150 | Cic.Fix (_, funl) ->
152 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funl
155 fun acc (_, _, ty, bo) ->
156 find context w ty @ find (tys @ context) w bo @ acc
158 | Cic.CoFix (_, funl) ->
160 List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funl
163 fun acc (_, ty, bo) ->
164 find context w ty @ find (tys @ context) w bo @ acc
167 find context wanted t
169 let select_in_term ~context ~term ~pattern:(wanted,where) =
170 let add_ctx context name entry =
171 (Some (name, entry)) :: context
173 let rec aux context where term =
174 match (where, term) with
175 | Cic.Implicit (Some `Hole), t -> [context,t]
176 | Cic.Implicit (Some `Type), t -> []
177 | Cic.Implicit None,_ -> []
178 | Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) ->
183 Some t1, Some t2 -> aux context t1 t2
186 | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) ->
187 aux context te1 te2 @ aux context ty1 ty2
188 | Cic.Prod (Cic.Anonymous, s1, t1), Cic.Prod (name, s2, t2)
189 | Cic.Lambda (Cic.Anonymous, s1, t1), Cic.Lambda (name, s2, t2) ->
190 aux context s1 s2 @ aux (add_ctx context name (Cic.Decl s2)) t1 t2
191 | Cic.Prod (Cic.Name n1, s1, t1),
192 Cic.Prod ((Cic.Name n2) as name , s2, t2)
193 | Cic.Lambda (Cic.Name n1, s1, t1),
194 Cic.Lambda ((Cic.Name n2) as name, s2, t2) when n1 = n2->
195 aux context s1 s2 @ aux (add_ctx context name (Cic.Decl s2)) t1 t2
196 | Cic.Prod (name1, s1, t1), Cic.Prod (name2, s2, t2)
197 | Cic.Lambda (name1, s1, t1), Cic.Lambda (name2, s2, t2) -> []
198 | Cic.LetIn (Cic.Anonymous, s1, t1), Cic.LetIn (name, s2, t2) ->
199 aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
200 | Cic.LetIn (Cic.Name n1, s1, t1),
201 Cic.LetIn ((Cic.Name n2) as name, s2, t2) when n1 = n2->
202 aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
203 | Cic.LetIn (name1, s1, t1), Cic.LetIn (name2, s2, t2) -> []
204 | Cic.Appl terms1, Cic.Appl terms2 -> auxs context terms1 terms2
205 | Cic.Var (_, subst1), Cic.Var (_, subst2)
206 | Cic.Const (_, subst1), Cic.Const (_, subst2)
207 | Cic.MutInd (_, _, subst1), Cic.MutInd (_, _, subst2)
208 | Cic.MutConstruct (_, _, _, subst1), Cic.MutConstruct (_, _, _, subst2) ->
209 auxs context (List.map snd subst1) (List.map snd subst2)
210 | Cic.MutCase (_, _, out1, t1, pat1), Cic.MutCase (_ , _, out2, t2, pat2) ->
211 aux context out1 out2 @ aux context t1 t2 @ auxs context pat1 pat2
212 | Cic.Fix (_, funs1), Cic.Fix (_, funs2) ->
214 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
218 (fun (_, _, ty1, bo1) (_, _, ty2, bo2) ->
219 aux context ty1 ty2 @ aux (tys @ context) bo1 bo2)
221 | Cic.CoFix (_, funs1), Cic.CoFix (_, funs2) ->
223 List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
227 (fun (_, ty1, bo1) (_, ty2, bo2) ->
228 aux context ty1 ty2 @ aux (tys @ context) bo1 bo2)
232 (Printf.sprintf "Pattern %s versus term %s"
235 and auxs context terms1 terms2 = (* as aux for list of terms *)
236 List.concat (List.map2 (fun t1 t2 -> aux context t1 t2) terms1 terms2)
238 let context_len = List.length context in
239 let roots = aux context where term in
243 let rec find_in_roots =
246 | (context',where)::tl ->
247 let tl' = find_in_roots tl in
248 let context'_len = List.length context' in
251 CicSubstitution.lift (context'_len - context_len) wanted
253 find_subterms ~wanted ~context where
259 (** create a pattern from a term and a list of subterms.
260 * the pattern is granted to have a ? for every subterm that has no selected
262 * @param equality equality function used while walking the term. Defaults to
263 * physical equality (==) *)
264 let pattern_of ?(equality=(==)) ~term terms =
265 let (===) x y = equality x y in
266 let not_found = false, Cic.Implicit None in
269 | t when List.exists (fun t' -> t === t') terms ->
270 true,Cic.Implicit (Some `Hole)
271 | Cic.Var (uri, subst) ->
272 let b,subst = aux_subst subst in
274 true,Cic.Var (uri, subst)
277 | Cic.Meta (i, ctxt) ->
283 | Some t -> let bt,t = aux t in b||bt ,Some t::ctxt
287 true,Cic.Meta (i, ctxt)
290 | Cic.Cast (te, ty) ->
291 let b1,te = aux te in
292 let b2,ty = aux ty in
293 if b1||b2 then true,Cic.Cast (te, ty)
296 | Cic.Prod (name, s, t) ->
300 true, Cic.Prod (name, s, t)
303 | Cic.Lambda (name, s, t) ->
307 true, Cic.Lambda (name, s, t)
310 | Cic.LetIn (name, s, t) ->
314 true, Cic.LetIn (name, s, t)
329 | Cic.Const (uri, subst) ->
330 let b,subst = aux_subst subst in
332 true, Cic.Const (uri, subst)
335 | Cic.MutInd (uri, tyno, subst) ->
336 let b,subst = aux_subst subst in
338 true, Cic.MutInd (uri, tyno, subst)
341 | Cic.MutConstruct (uri, tyno, consno, subst) ->
342 let b,subst = aux_subst subst in
344 true, Cic.MutConstruct (uri, tyno, consno, subst)
347 | Cic.MutCase (uri, tyno, outty, t, pat) ->
348 let b1,outty = aux outty in
357 if b1 || b2 || b3 then
358 true, Cic.MutCase (uri, tyno, outty, t, pat)
361 | Cic.Fix (funno, funs) ->
364 (fun (name, i, ty, bo) (b,funs) ->
365 let b1,ty = aux ty in
366 let b2,bo = aux bo in
367 b||b1||b2, (name, i, ty, bo)::funs) funs (false,[])
370 true, Cic.Fix (funno, funs)
373 | Cic.CoFix (funno, funs) ->
376 (fun (name, ty, bo) (b,funs) ->
377 let b1,ty = aux ty in
378 let b2,bo = aux bo in
379 b||b1||b2, (name, ty, bo)::funs) funs (false,[])
382 true, Cic.CoFix (funno, funs)
387 | Cic.Implicit _ -> not_found
388 and aux_subst subst =
390 (fun (uri, t) (b,subst) ->
392 b||b1,(uri, t)::subst) subst (false,[])
396 exception Fail of string
398 (** select metasenv conjecture pattern
399 * select all subterms of [conjecture] matching [pattern].
400 * It returns the set of matched terms (that can be compared using physical
401 * equality to the subterms of [conjecture]) together with their contexts.
402 * The representation of the set mimics the ProofEngineTypes.pattern type:
403 * a list of hypothesis (names of) together with the list of its matched
404 * subterms (and their contexts) + the list of matched subterms of the
405 * with their context conclusion. Note: in the result the list of hypothesis
406 * has an entry for each entry in the context and in the same order.
407 * Of course the list of terms (with their context) associated to the
408 * hypothesis name may be empty. *)
409 let select ~metasenv ~conjecture:(_,context,ty) ~pattern:(what,hyp_patterns,goal_pattern) =
410 let find_pattern_for name =
411 try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns))
412 with Not_found -> None in
413 let ty_terms = select_in_term ~context ~term:ty ~pattern:(what,goal_pattern) in
414 let context_len = List.length context in
418 (fun entry (res,context) ->
420 None -> (None::res),(None::context)
421 | Some (name,Cic.Decl term) ->
422 (match find_pattern_for name with
423 | None -> ((Some (`Decl []))::res),(entry::context)
430 let what,subst',metasenv' =
431 CicMetaSubst.delift_rels [] metasenv
432 (context_len - List.length context) what
434 assert (subst' = []);
435 assert (metasenv' = metasenv);
437 let terms = select_in_term ~context ~term ~pattern:(what,pat) in
438 ((Some (`Decl terms))::res),(entry::context)
440 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
443 ("The term the user wants to convert is not closed " ^
444 "in the context of the position of the substitution.")))
445 | Some (name,Cic.Def (bo, ty)) ->
446 (match find_pattern_for name with
448 let selected_ty= match ty with None -> None | Some _ -> Some [] in
449 ((Some (`Def ([],selected_ty)))::res),(entry::context)
456 let what,subst',metasenv' =
457 CicMetaSubst.delift_rels [] metasenv
458 (context_len - List.length context) what
460 assert (subst' = []);
461 assert (metasenv' = metasenv);
464 select_in_term ~context ~term:bo ~pattern:(what,pat) in
469 Some (select_in_term ~context ~term:ty ~pattern:(what,pat))
471 ((Some (`Def (terms_bo,terms_ty)))::res),(entry::context)
473 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
476 ("The term the user wants to convert is not closed " ^
477 "in the context of the position of the substitution.")))
480 context_terms, ty_terms