From: Claudio Sacerdoti Coen Date: Thu, 5 Feb 2004 11:54:14 +0000 (+0000) Subject: fresh_name_generator has now also the metasenv parameter. X-Git-Tag: V_0_2_3~50 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=feb3c287997f7d35747c12e0db62e6194f5587a3;p=helm.git fresh_name_generator has now also the metasenv parameter. Before this patch it used the empty metasenv (and it worked, somehow!) --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 81f9acd66..b62f4b624 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -556,9 +556,9 @@ let decompose_uris_choice_callback uris = ) ;; -let mk_fresh_name_callback context name ~typ = +let mk_fresh_name_callback metasenv context name ~typ = let fresh_name = - match FreshNamesGenerator.mk_fresh_name context name ~typ with + match FreshNamesGenerator.mk_fresh_name metasenv context name ~typ with Cic.Name fresh_name -> fresh_name | Cic.Anonymous -> assert false in diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml index e4a9fa2e9..2b0e58d21 100644 --- a/helm/gTopLevel/invokeTactics.ml +++ b/helm/gTopLevel/invokeTactics.ml @@ -62,8 +62,7 @@ module type Callbacks = val decompose_uris_choice_callback : (UriManager.uri * int * 'a) list -> (UriManager.uri * int * 'b list) list - val mk_fresh_name_callback : - Cic.context -> Cic.name -> typ:Cic.term -> Cic.name + val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type end ;; diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli index 200e50a15..a304e7e3b 100644 --- a/helm/gTopLevel/invokeTactics.mli +++ b/helm/gTopLevel/invokeTactics.mli @@ -60,8 +60,7 @@ module type Callbacks = val decompose_uris_choice_callback : (UriManager.uri * int * 'a) list -> (UriManager.uri * int * 'b list) list - val mk_fresh_name_callback : - Cic.context -> Cic.name -> typ:Cic.term -> Cic.name + val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type end module type Tactics = diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend index eb500c921..8828b40df 100644 --- a/helm/ocaml/cic_unification/.depend +++ b/helm/ocaml/cic_unification/.depend @@ -8,6 +8,6 @@ cicMetaSubst.cmx: cicMetaSubst.cmi cicUnification.cmo: cicMetaSubst.cmi cicUnification.cmi cicUnification.cmx: cicMetaSubst.cmx cicUnification.cmi cicRefine.cmo: cicMetaSubst.cmi cicMkImplicit.cmi cicUnification.cmi \ - cicRefine.cmi + freshNamesGenerator.cmi cicRefine.cmi cicRefine.cmx: cicMetaSubst.cmx cicMkImplicit.cmx cicUnification.cmx \ - cicRefine.cmi + freshNamesGenerator.cmx cicRefine.cmi diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml index 3f0006a39..3f4d777c9 100644 --- a/helm/ocaml/cic_unification/freshNamesGenerator.ml +++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml @@ -27,14 +27,14 @@ (* 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 mk_fresh_name metasenv 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 + (match CicTypeChecker.type_of_aux' metasenv context typ with C.Sort C.Prop | C.Sort C.CProp -> "H" | C.Sort C.Set -> "x" diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.mli b/helm/ocaml/cic_unification/freshNamesGenerator.mli index e350363e9..371ca99fa 100644 --- a/helm/ocaml/cic_unification/freshNamesGenerator.mli +++ b/helm/ocaml/cic_unification/freshNamesGenerator.mli @@ -23,8 +23,9 @@ * http://cs.unibo.it/helm/. *) -(* mk_fresh_name context name typ *) +(* mk_fresh_name metasenv 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 +val mk_fresh_name : + Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 304f10450..ac28f9a28 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -59,7 +59,8 @@ let rewrite_tac ~term:equality ~status:(proof,goal) = ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty' in C.Lambda - (FreshNamesGenerator.mk_fresh_name context C.Anonymous ty, ty, gty'') + (FreshNamesGenerator.mk_fresh_name metasenv 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 +121,8 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) = ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty' in C.Lambda - (FreshNamesGenerator.mk_fresh_name context C.Anonymous ty, ty, gty'') + (FreshNamesGenerator.mk_fresh_name metasenv 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 2b505b79d..a518edaa6 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -37,13 +37,13 @@ exception WrongUriToVariable of string (* and [bo] = Lambda/LetIn [context].(Meta [newmeta]) *) (* So, lambda_abstract is the core of the implementation of *) (* the Intros tactic. *) -let lambda_abstract context newmeta ty mk_fresh_name = +let lambda_abstract metasenv context newmeta ty mk_fresh_name = let module C = Cic in let rec collect_context context = function C.Cast (te,_) -> collect_context context te | C.Prod (n,s,t) -> - let n' = mk_fresh_name context n ~typ:s in + let n' = mk_fresh_name metasenv context n ~typ:s in let (context',ty,bo) = collect_context ((Some (n',(C.Decl s)))::context) t in @@ -115,7 +115,8 @@ let eta_expand metasenv context t arg = T.type_of_aux' metasenv context arg in let fresh_name = - FreshNamesGenerator.mk_fresh_name context (Cic.Name "Heta") ~typ:argty + FreshNamesGenerator.mk_fresh_name + metasenv context (Cic.Name "Heta") ~typ:argty in (C.Appl [C.Lambda (fresh_name,argty,aux 0 t) ; arg]) @@ -321,7 +322,7 @@ let intros_tac let metano,context,ty = CicUtil.lookup_meta goal metasenv in let newmeta = new_meta_of_proof ~proof in let (context',ty',bo') = - lambda_abstract context newmeta ty mk_fresh_name_callback + lambda_abstract metasenv context newmeta ty mk_fresh_name_callback in let (newproof, _) = subst_meta_in_proof proof metano bo' [newmeta,context',ty'] @@ -338,7 +339,7 @@ let cut_tac let newmeta1 = new_meta_of_proof ~proof in let newmeta2 = newmeta1 + 1 in let fresh_name = - mk_fresh_name_callback context (Cic.Name "Hcut") ~typ:term in + mk_fresh_name_callback metasenv context (Cic.Name "Hcut") ~typ:term in let context_for_newmeta1 = (Some (fresh_name,C.Decl term))::context in let irl1 = @@ -370,7 +371,7 @@ let letin_tac let _ = CicTypeChecker.type_of_aux' metasenv context term in let newmeta = new_meta_of_proof ~proof in let fresh_name = - mk_fresh_name_callback context (Cic.Name "Hletin") ~typ:term in + mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in let context_for_newmeta = (Some (fresh_name,C.Def (term,None)))::context in let irl = diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml index 178be54d4..334c594da 100644 --- a/helm/ocaml/tactics/proofEngineTypes.ml +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -42,4 +42,4 @@ exception Fail of string (** constraint: the returned value will always be constructed by Cic.Name **) type mk_fresh_name_type = - Cic.context -> Cic.name -> typ:Cic.term -> Cic.name + Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 28acd57ec..64b9ff790 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -83,7 +83,7 @@ let generalize_tac ~start: (P.cut_tac (C.Prod( - (mk_fresh_name_callback context C.Anonymous typ), + (mk_fresh_name_callback metasenv context C.Anonymous typ), typ, (ProofEngineReduction.replace_lifting_csc 1 ~equality:(==)