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 (* mk_fresh_name context name typ *)
27 (* returns an identifier which is fresh in the context *)
28 (* and that resembles [name] as much as possible. *)
29 (* [typ] will be the type of the variable *)
30 let mk_fresh_name context name ~typ =
35 (*CSC: great space for improvements here *)
37 (match CicTypeChecker.type_of_aux' [] context typ with
39 | C.Sort C.CProp -> "H"
43 with CicTypeChecker.TypeCheckerFailure _ -> "H"
46 Str.global_replace (Str.regexp "[0-9]*$") "" name
48 let already_used name =
49 List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context
51 if not (already_used basename) then
55 let name' = basename ^ string_of_int n in
56 if already_used name' then
64 let new_meta_of_proof ~proof:(_, metasenv, _, _) =
65 CicMkImplicit.new_meta metasenv
67 let subst_meta_in_proof proof meta term newmetasenv =
68 let uri,metasenv,bo,ty = proof in
69 let subst_in = CicMetaSubst.apply_subst [meta,term] in
71 newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
75 (function i,canonical_context,ty ->
76 let canonical_context' =
79 Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
80 | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
82 | Some (_,Cic.Def (_,Some _)) -> assert false
85 i,canonical_context',(subst_in ty)
88 let bo' = subst_in bo in
89 let newproof = uri,metasenv'',bo',ty in
90 (newproof, metasenv'')
92 (*CSC: commento vecchio *)
93 (* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv *)
94 (* This (heavy) function must be called when a tactic can instantiate old *)
95 (* metavariables (i.e. existential variables). It substitues the metasenv *)
96 (* of the proof with the result of removing [meta] from the domain of *)
97 (* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
98 (* in the current proof. Finally it applies [apply_subst_replacing] to *)
100 (*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
101 (*CSC: ci ripasso sopra apply_subst!!! *)
102 (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
103 (*CSC: [newmetasenv]. *)
104 let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
105 let (uri,_,bo,ty) = proof in
106 let bo' = subst_in bo in
109 (fun metasenv_entry i ->
110 match metasenv_entry with
111 (m,canonical_context,ty) when m <> meta ->
112 let canonical_context' =
116 | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
117 | Some (i,Cic.Def (t,None)) ->
118 Some (i,Cic.Def ((subst_in t),None))
119 | Some (_,Cic.Def (_,Some _)) -> assert false
122 (m,canonical_context',subst_in ty)::i
126 let newproof = uri,metasenv',bo',ty in
127 (newproof, metasenv')