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 (*CSC: generatore di nomi? Chiedere il nome? *)
28 let next_fresh_index = ref 0 in
31 incr next_fresh_index ;
32 "fresh_name" ^ string_of_int !next_fresh_index
34 incr next_fresh_index ;
35 name ^ string_of_int !next_fresh_index
37 (* identity_relocation_list_for_metavariable i canonical_context *)
38 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
39 (* where n = List.length [canonical_context] *)
40 (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
41 let identity_relocation_list_for_metavariable canonical_context =
42 let canonical_context_length = List.length canonical_context in
46 | (n,None::tl) -> None::(aux ((n+1),tl))
47 | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
49 aux (1,canonical_context)
51 (* Returns the first meta whose number is above the *)
52 (* number of the higher meta. *)
54 let (_,metasenv,_,_) = proof in
59 | None,(n,_,_)::tl -> aux (Some n,tl)
60 | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
62 1 + aux (None,metasenv)
64 let subst_meta_in_proof proof meta term newmetasenv =
65 let uri,metasenv,bo,ty = proof in
66 let subst_in = CicUnification.apply_subst [meta,term] in
68 newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
72 (function i,canonical_context,ty ->
73 let canonical_context' =
76 Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
77 | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s))
81 i,canonical_context',(subst_in ty)
84 let bo' = subst_in bo in
85 let newproof = uri,metasenv'',bo',ty in
86 (newproof, metasenv'')
88 (*CSC: commento vecchio *)
89 (* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv *)
90 (* This (heavy) function must be called when a tactic can instantiate old *)
91 (* metavariables (i.e. existential variables). It substitues the metasenv *)
92 (* of the proof with the result of removing [meta] from the domain of *)
93 (* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
94 (* in the current proof. Finally it applies [apply_subst_replacing] to *)
96 (*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
97 (*CSC: ci ripasso sopra apply_subst!!! *)
98 (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
99 (*CSC: [newmetasenv]. *)
100 let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
101 let (uri,_,bo,ty) = proof in
102 let bo' = subst_in bo in
105 (fun metasenv_entry i ->
106 match metasenv_entry with
107 (m,canonical_context,ty) when m <> meta ->
108 let canonical_context' =
112 | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
113 | Some (i,Cic.Def t) -> Some (i,Cic.Def (subst_in t))
116 (m,canonical_context',subst_in ty)::i
120 let newproof = uri,metasenv',bo',ty in
121 (newproof, metasenv')