From 7b922ad1f9832c1edb3acea8f0c910fa2c0c20e5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 5 Feb 2004 11:33:09 +0000 Subject: [PATCH] mk_fresh_name moved to FreshNamesGenerator. --- helm/gTopLevel/gTopLevel.ml | 2 +- helm/ocaml/cic_unification/.depend | 4 +- .../cic_unification/freshNamesGenerator.ml | 62 +++++++++++++++++++ .../cic_unification/freshNamesGenerator.mli | 30 +++++++++ helm/ocaml/tactics/equalityTactics.ml | 4 +- helm/ocaml/tactics/primitiveTactics.ml | 8 +-- helm/ocaml/tactics/proofEngineHelpers.ml | 38 ------------ helm/ocaml/tactics/proofEngineHelpers.mli | 6 -- helm/ocaml/tactics/variousTactics.ml | 2 +- 9 files changed, 102 insertions(+), 54 deletions(-) create mode 100644 helm/ocaml/cic_unification/freshNamesGenerator.ml create mode 100644 helm/ocaml/cic_unification/freshNamesGenerator.mli diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 2b9e101ab..81f9acd66 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -558,7 +558,7 @@ let decompose_uris_choice_callback uris = 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 diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend index aaa723474..eb500c921 100644 --- a/helm/ocaml/cic_unification/.depend +++ b/helm/ocaml/cic_unification/.depend @@ -1,6 +1,6 @@ -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 diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml new file mode 100644 index 000000000..3f0006a39 --- /dev/null +++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml @@ -0,0 +1,62 @@ +(* 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 +;; diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.mli b/helm/ocaml/cic_unification/freshNamesGenerator.mli new file mode 100644 index 000000000..e350363e9 --- /dev/null +++ b/helm/ocaml/cic_unification/freshNamesGenerator.mli @@ -0,0 +1,30 @@ +(* 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 diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 48d5ea9a6..304f10450 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -59,7 +59,7 @@ let rewrite_tac ~term:equality ~status:(proof,goal) = ~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 @@ -120,7 +120,7 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) = ~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 = diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 5c187b053..2b505b79d 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -115,7 +115,7 @@ let eta_expand metasenv context t arg = 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]) @@ -312,7 +312,7 @@ let apply_tac ~term ~status = 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 @@ -329,7 +329,7 @@ let intros_tac (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 @@ -361,7 +361,7 @@ let cut_tac (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 diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index ccac132ef..aec43abc3 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -23,44 +23,6 @@ * 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 diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index 652776262..5a4f145f9 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -23,12 +23,6 @@ * 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 diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 04959e696..28acd57ec 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -59,7 +59,7 @@ e li aggiunga nel context, poi si conta la lunghezza di questo nuovo 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 -- 2.39.2