From 9b05df26c99fcdddb41d9ef1e9dc3b0571b9395b Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 26 Oct 2009 15:50:20 +0000 Subject: Local/Global revision 12418 continued - Fixing non-export of newly created Local Argument Scope. - Fixing bad discharge of local variables in nested sections (bug still exists in v8.2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12420 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/notation.ml | 8 +++---- library/impargs.ml | 11 ++++----- test-suite/prerequisite/make_local.v | 2 +- test-suite/success/implicit.v | 43 ++++++++++++++++++++++++++++++++++++ 4 files changed, 53 insertions(+), 11 deletions(-) diff --git a/interp/notation.ml b/interp/notation.ml index 093d43934..6ae720fca 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -482,18 +482,16 @@ let classify_arguments_scope (req,_,_ as obj) = if req = ArgsScopeNoDischarge then Dispose else Substitute obj let rebuild_arguments_scope (req,r,l) = - let req' = - if isVarRef r && Lib.is_in_section r then ArgsScopeNoDischarge else req in match req with | ArgsScopeNoDischarge -> assert false | ArgsScopeAuto -> - (req',r,compute_arguments_scope (Global.type_of_global r)) + (req,r,compute_arguments_scope (Global.type_of_global r)) | ArgsScopeManual -> (* Add to the manually given scopes the one found automatically for the extra parameters of the section *) let l' = compute_arguments_scope (Global.type_of_global r) in let l1,_ = list_chop (List.length l' - List.length l) l' in - (req',r,l1@l) + (req,r,l1@l) let (inArgumentsScope,outArgumentsScope) = declare_object {(default_object "ARGUMENTS-SCOPE") with @@ -504,7 +502,7 @@ let (inArgumentsScope,outArgumentsScope) = discharge_function = discharge_arguments_scope; rebuild_function = rebuild_arguments_scope } -let is_local local ref = local || (isVarRef ref && not (Lib.is_in_section ref)) +let is_local local ref = local || isVarRef ref && Lib.is_in_section ref let declare_arguments_scope_gen req r scl = Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl)) diff --git a/library/impargs.ml b/library/impargs.ml index 89f34a38b..c434be70d 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -473,7 +473,7 @@ let discharge_implicits (_,(req,l)) = | ImplLocal -> None | ImplInteractive (ref,flags,exp) -> let vars = section_segment_of_reference ref in - let ref' = pop_global_reference ref in + let ref' = if isVarRef ref then ref else pop_global_reference ref in let l' = [ref', impls_of_context vars @ snd (List.hd l)] in Some (ImplInteractive (ref',flags,exp),l') | ImplConstant (con,flags) -> @@ -483,7 +483,8 @@ let discharge_implicits (_,(req,l)) = | ImplMutualInductive (kn,flags) -> let l' = List.map (fun (gr, l) -> let vars = section_segment_of_reference gr in - (pop_global_reference gr, impls_of_context vars @ l)) l + ((if isVarRef gr then gr else pop_global_reference gr), + impls_of_context vars @ l)) l in Some (ImplMutualInductive (pop_kn kn,flags),l') @@ -523,18 +524,18 @@ let rebuild_implicits (req,l) = [ref,l'] let classify_implicits (req,_ as obj) = - if req = ImplLocal then None else Some obj + if req = ImplLocal then Dispose else Substitute obj let (inImplicits, _) = declare_object {(default_object "IMPLICITS") with cache_function = cache_implicits; load_function = load_implicits; subst_function = subst_implicits; - classify_function = (fun x -> Substitute x); + classify_function = classify_implicits; discharge_function = discharge_implicits; rebuild_function = rebuild_implicits } -let is_local local ref = local || (isVarRef ref && not (is_in_section ref)) +let is_local local ref = local || isVarRef ref && is_in_section ref let declare_implicits_gen req flags ref = let imps = compute_global_implicits flags [] ref in diff --git a/test-suite/prerequisite/make_local.v b/test-suite/prerequisite/make_local.v index cdb7a2691..8700a6c4e 100644 --- a/test-suite/prerequisite/make_local.v +++ b/test-suite/prerequisite/make_local.v @@ -5,6 +5,6 @@ Definition f (A:Type) (a:A) := a. Local Arguments Scope f [type_scope type_scope]. Local Implicit Arguments f [A]. -(* Used in Import.v to test the locality flag *) +(* Used in ImportedCoercion.v to test the locality flag *) Local Coercion g (b:bool) := if b then 0 else 1. diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index aabb057a4..c6d0a6dd2 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -1,3 +1,5 @@ +(* Testing the behavior of implicit arguments *) + (* Implicit on section variables *) Set Implicit Arguments. @@ -19,8 +21,49 @@ Check (forall (type : Set) (elt : type) (empty : type -> bool), empty elt = true -> stack). +(* Nested sections and manual implicit arguments *) + +Variable op' : forall A : Set, A -> A -> Set. +Variable op'' : forall A : Set, A -> A -> Set. + +Section B. + +Definition eq1 := fun (A:Type) (x y:A) => x=y. +Definition eq2 := fun (A:Type) (x y:A) => x=y. +Definition eq3 := fun (A:Type) (x y:A) => x=y. + +Implicit Arguments op' []. +Global Implicit Arguments op'' []. + +Implicit Arguments eq2 []. +Global Implicit Arguments eq3 []. + +Check (op 0 0). +Check (op' nat 0 0). +Check (op'' nat 0 0). +Check (eq1 0 0). +Check (eq2 nat 0 0). +Check (eq3 nat 0 0). + +End B. + +Check (op 0 0). +Check (op' 0 0). +Check (op'' nat 0 0). +Check (eq1 0 0). +Check (eq2 0 0). +Check (eq3 nat 0 0). + End Spec. +Check (eq1 0 0). +Check (eq2 0 0). +Check (eq3 nat 0 0). + +(* Test discharge on automatic implicit arguments *) + +Check (op' 0 0). + (* Example submitted by Frédéric (interesting in v8 syntax) *) Parameter f : nat -> nat * nat. -- cgit v1.2.3