let mk_fresh_name_callback context name ~typ =
let fresh_name =
- match ProofEngineHelpers.mk_fresh_name context name ~typ with
+ match FreshNamesGenerator.mk_fresh_name context name ~typ with
Cic.Name fresh_name -> fresh_name
| Cic.Anonymous -> assert false
in
-cicMkImplicit.cmo: cicMkImplicit.cmi
-cicMkImplicit.cmx: cicMkImplicit.cmi
cicUnification.cmi: cicMetaSubst.cmi
+freshNamesGenerator.cmo: freshNamesGenerator.cmi
+freshNamesGenerator.cmx: freshNamesGenerator.cmi
cicMkImplicit.cmo: cicMkImplicit.cmi
cicMkImplicit.cmx: cicMkImplicit.cmi
cicMetaSubst.cmo: cicMetaSubst.cmi
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* mk_fresh_name context name typ *)
+(* returns an identifier which is fresh in the context *)
+(* and that resembles [name] as much as possible. *)
+(* [typ] will be the type of the variable *)
+let mk_fresh_name context name ~typ =
+ let module C = Cic in
+ let basename =
+ match name with
+ C.Anonymous ->
+ (*CSC: great space for improvements here *)
+ (try
+ (match CicTypeChecker.type_of_aux' [] context typ with
+ C.Sort C.Prop
+ | C.Sort C.CProp -> "H"
+ | C.Sort C.Set -> "x"
+ | _ -> "H"
+ )
+ with CicTypeChecker.TypeCheckerFailure _ -> "H"
+ )
+ | C.Name name ->
+ Str.global_replace (Str.regexp "[0-9]*$") "" name
+ in
+ let already_used name =
+ List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context
+ in
+ if not (already_used basename) then
+ C.Name basename
+ else
+ let rec try_next n =
+ let name' = basename ^ string_of_int n in
+ if already_used name' then
+ try_next (n+1)
+ else
+ C.Name name'
+ in
+ try_next 1
+;;
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* mk_fresh_name context name typ *)
+(* returns an identifier which is fresh in the context *)
+(* and that resembles [name] as much as possible. *)
+(* [typ] will be the type of the variable *)
+val mk_fresh_name : Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
in
C.Lambda
- (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
+ (FreshNamesGenerator.mk_fresh_name context C.Anonymous ty, ty, gty'')
in
let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
in
C.Lambda
- (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
+ (FreshNamesGenerator.mk_fresh_name context C.Anonymous ty, ty, gty'')
in
let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
let irl =
T.type_of_aux' metasenv context arg
in
let fresh_name =
- ProofEngineHelpers.mk_fresh_name context (Cic.Name "Heta") ~typ:argty
+ FreshNamesGenerator.mk_fresh_name context (Cic.Name "Heta") ~typ:argty
in
(C.Appl [C.Lambda (fresh_name,argty,aux 0 t) ; arg])
raise (Fail (Printexc.to_string e))
let intros_tac
- ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name) ()
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()
~status:(proof, goal)
=
let module C = Cic in
(newproof, [newmeta])
let cut_tac
- ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name)
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
term ~status:(proof, goal)
=
let module C = Cic in
(newproof, [newmeta1 ; newmeta2])
let letin_tac
- ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name)
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
term ~status:(proof, goal)
=
let module C = Cic in
* http://cs.unibo.it/helm/.
*)
-(* mk_fresh_name context name typ *)
-(* returns an identifier which is fresh in the context *)
-(* and that resembles [name] as much as possible. *)
-(* [typ] will be the type of the variable *)
-let mk_fresh_name context name ~typ =
- let module C = Cic in
- let basename =
- match name with
- C.Anonymous ->
- (*CSC: great space for improvements here *)
- (try
- (match CicTypeChecker.type_of_aux' [] context typ with
- C.Sort C.Prop -> "H"
- | C.Sort C.CProp -> "H"
- | C.Sort C.Set -> "x"
- | _ -> "H"
- )
- with CicTypeChecker.TypeCheckerFailure _ -> "H"
- )
- | C.Name name ->
- Str.global_replace (Str.regexp "[0-9]*$") "" name
- in
- let already_used name =
- List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context
- in
- if not (already_used basename) then
- C.Name basename
- else
- let rec try_next n =
- let name' = basename ^ string_of_int n in
- if already_used name' then
- try_next (n+1)
- else
- C.Name name'
- in
- try_next 1
-;;
-
let new_meta_of_proof ~proof:(_, metasenv, _, _) =
CicMkImplicit.new_meta metasenv
* http://cs.unibo.it/helm/.
*)
-(* mk_fresh_name context name typ *)
-(* returns an identifier which is fresh in the context *)
-(* and that resembles [name] as much as possible. *)
-(* [typ] will be the type of the variable *)
-val mk_fresh_name : ProofEngineTypes.mk_fresh_name_type
-
(* Returns the first meta whose number is above the *)
(* number of the higher meta. *)
val new_meta_of_proof : proof:ProofEngineTypes.proof -> int
contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
let generalize_tac
- ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name)
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
terms ~status:((proof,goal) as status)
=
let module C = Cic in
projects / helm.git / commitdiff