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 let new_meta_of_proof ~proof:(_, metasenv, _, _) =
27 CicMkImplicit.new_meta metasenv []
29 let subst_meta_in_proof proof meta term newmetasenv =
30 let uri,metasenv,bo,ty = proof in
31 (* empty context is ok for term since it wont be used by apply_subst *)
32 (* hack: since we do not know the context and the type of term, we
33 create a substitution with cc =[] and type = Implicit; they will be
34 in any case dropped by apply_subst, but it would be better to rewrite
35 the code. Cannot we just use apply_subst_metasenv, etc. ?? *)
36 let subst_in = CicMetaSubst.apply_subst [meta,([], term,Cic.Implicit None)] in
38 newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
42 (function i,canonical_context,ty ->
43 let canonical_context' =
46 Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
47 | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
49 | Some (_,Cic.Def (_,Some _)) -> assert false
52 i,canonical_context',(subst_in ty)
55 let bo' = subst_in bo in
56 (* Metavariables can appear also in the *statement* of the theorem
57 * since the parser does not reject as statements terms with
58 * metavariable therein *)
59 let ty' = subst_in ty in
60 let newproof = uri,metasenv'',bo',ty' in
61 (newproof, metasenv'')
63 (*CSC: commento vecchio *)
64 (* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv *)
65 (* This (heavy) function must be called when a tactic can instantiate old *)
66 (* metavariables (i.e. existential variables). It substitues the metasenv *)
67 (* of the proof with the result of removing [meta] from the domain of *)
68 (* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
69 (* in the current proof. Finally it applies [apply_subst_replacing] to *)
71 (*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
72 (*CSC: ci ripasso sopra apply_subst!!! *)
73 (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
74 (*CSC: [newmetasenv]. *)
75 let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
76 let (uri,_,bo,ty) = proof in
77 let bo' = subst_in bo in
78 (* Metavariables can appear also in the *statement* of the theorem
79 * since the parser does not reject as statements terms with
80 * metavariable therein *)
81 let ty' = subst_in ty in
84 (fun metasenv_entry i ->
85 match metasenv_entry with
86 (m,canonical_context,ty) when m <> meta ->
87 let canonical_context' =
91 | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
92 | Some (i,Cic.Def (t,None)) ->
93 Some (i,Cic.Def ((subst_in t),None))
94 | Some (_,Cic.Def (_,Some _)) -> assert false
97 (m,canonical_context',subst_in ty)::i
101 let newproof = uri,metasenv',bo',ty' in
102 (newproof, metasenv')
104 let compare_metasenvs ~oldmetasenv ~newmetasenv =
105 List.map (function (i,_,_) -> i)
108 not (List.exists (fun (j,_,_) -> i=j) oldmetasenv)) newmetasenv)
111 (** finds the _pointers_ to subterms that are alpha-equivalent to wanted in t *)
112 let find_subterms ~eq ~wanted t =
120 | Cic.Meta (_, ctx) ->
125 | Some t -> find w t @ acc
127 | Cic.Lambda (_, t1, t2)
128 | Cic.Prod (_, t1, t2)
129 | Cic.LetIn (_, t1, t2) ->
130 find w t1 @ find (CicSubstitution.lift 1 w) t2
132 List.fold_left (fun acc t -> find w t @ acc) [] l
133 | Cic.Cast (t, ty) -> find w t @ find w ty
134 | Cic.Implicit _ -> assert false
135 | Cic.Const (_, esubst)
136 | Cic.Var (_, esubst)
137 | Cic.MutInd (_, _, esubst)
138 | Cic.MutConstruct (_, _, _, esubst) ->
139 List.fold_left (fun acc (_, t) -> find w t @ acc) [] esubst
140 | Cic.MutCase (_, _, outty, indterm, patterns) ->
141 find w outty @ find w indterm @
142 List.fold_left (fun acc p -> find w p @ acc) [] patterns
143 | Cic.Fix (_, funl) ->
145 fun acc (_, _, ty, bo) -> find w ty @ find w bo @ acc
147 | Cic.CoFix (_, funl) ->
149 fun acc (_, ty, bo) -> find w ty @ find w bo @ acc