From 297b0cb44bbe8ec7304ca635c566815167266d4a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 Jun 2015 11:28:44 +0200 Subject: Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change in the semantics of arguments scopes: scopes can no longer be bound to Funclass or Sortclass (this does not seem to be useful)). It is useful to have function_scope for, e.g., function composition. This allows users to, e.g., automatically interpret ∘ as morphism composition when expecting a morphism of categories, as functor composition when expecting a functor, and as function composition when expecting a function. Additionally, it is nicer to have fewer special cases in the OCaml code, and give more things a uniform syntax. (The scope type_scope should not be special-cased; this change is coming up next.) Also explicitly define [function_scope] in theories/Init/Notations.v. This closes bug #3080, Build a [function_scope] like [type_scope], or allow [Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass] We now mention Funclass and Sortclass in the documentation of [Bind Scope] again. --- interp/notation.mli | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'interp/notation.mli') diff --git a/interp/notation.mli b/interp/notation.mli index 38bd5fc7b..85c4be4cc 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -153,7 +153,9 @@ val find_arguments_scope : global_reference -> scope_name option list type scope_class -val scope_class_of_reference : global_reference -> scope_class +(** Comparison of scope_class *) +val scope_class_compare : scope_class -> scope_class -> int + val subst_scope_class : Mod_subst.substitution -> scope_class -> scope_class option @@ -162,7 +164,8 @@ val declare_ref_arguments_scope : global_reference -> unit val compute_arguments_scope : Term.types -> scope_name option list val compute_type_scope : Term.types -> scope_name option -val compute_scope_of_global : global_reference -> scope_name option + +val scope_class_of_class : Classops.cl_typ -> scope_class (** Building notation key *) -- cgit v1.2.3 From 6aa58955515dff338ea85d59073dfc0d0c7648ab Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 Jun 2015 15:41:11 +0200 Subject: Move type_scope into user space, fix some output logs --- interp/constrextern.ml | 2 +- interp/constrintern.ml | 17 ++++++++++------- interp/notation.ml | 9 +++++---- interp/notation.mli | 4 +++- test-suite/bugs/closed/3080.v | 18 ++++++++++++++++++ test-suite/bugs/closed/3612.v | 2 ++ test-suite/bugs/closed/3649.v | 4 +++- theories/Init/Notations.v | 1 + 8 files changed, 43 insertions(+), 14 deletions(-) create mode 100644 test-suite/bugs/closed/3080.v (limited to 'interp/notation.mli') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f57772ecb..1c60d5c2f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -788,7 +788,7 @@ let rec extern inctx scopes vars r = Miscops.map_cast_type (extern_typ scopes vars) c') and extern_typ (_,scopes) = - extern true (Some Notation.type_scope,scopes) + extern true (Notation.current_type_scope_name (),scopes) and sub_extern inctx (_,scopes) = extern inctx (None,scopes) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8c56d0ccf..d572508a1 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -298,7 +298,7 @@ let set_var_scope loc id istermvar env ntnvars = (* Not in a notation *) () -let set_type_scope env = {env with tmp_scope = Some Notation.type_scope} +let set_type_scope env = {env with tmp_scope = Notation.current_type_scope_name ()} let reset_tmp_scope env = {env with tmp_scope = None} @@ -449,12 +449,15 @@ let intern_generalization intern env lvar loc bk ak c = | Some AbsPi -> true | Some _ -> false | None -> - let is_type_scope = match env.tmp_scope with + match Notation.current_type_scope_name () with + | Some type_scope -> + let is_type_scope = match env.tmp_scope with + | None -> false + | Some sc -> String.equal sc type_scope + in + is_type_scope || + String.List.mem type_scope env.scopes | None -> false - | Some sc -> String.equal sc Notation.type_scope - in - is_type_scope || - String.List.mem Notation.type_scope env.scopes in if pi then (fun (id, loc') acc -> @@ -1755,7 +1758,7 @@ let extract_ids env = Id.Set.empty let scope_of_type_kind = function - | IsType -> Some Notation.type_scope + | IsType -> Notation.current_type_scope_name () | OfType typ -> compute_type_scope typ | WithoutTypeConstraint -> None diff --git a/interp/notation.ml b/interp/notation.ml index 075e04cba..8395f7d9a 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -65,11 +65,9 @@ let empty_scope = { } let default_scope = "" (* empty name, not available from outside *) -let type_scope = "type_scope" (* special scope used for interpreting types *) let init_scope_map () = - scope_map := String.Map.add default_scope empty_scope !scope_map; - scope_map := String.Map.add type_scope empty_scope !scope_map + scope_map := String.Map.add default_scope empty_scope !scope_map (**********************************************************************) (* Operations on scopes *) @@ -576,7 +574,7 @@ end module ScopeClassMap = Map.Make(ScopeClassOrd) let initial_scope_class_map : scope_name ScopeClassMap.t = - ScopeClassMap.add CL_SORT type_scope ScopeClassMap.empty + ScopeClassMap.empty let scope_class_map = ref initial_scope_class_map @@ -610,6 +608,9 @@ let compute_arguments_scope t = fst (compute_arguments_scope_full t) let compute_type_scope t = find_scope_class_opt (try Some (compute_scope_class t) with Not_found -> None) +let current_type_scope_name () = + find_scope_class_opt (Some CL_SORT) + let scope_class_of_class (x : cl_typ) : scope_class = x diff --git a/interp/notation.mli b/interp/notation.mli index 85c4be4cc..2bfbb33c2 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -29,7 +29,6 @@ type scopes (** = [scope_name list] *) type local_scopes = tmp_scope_name option * scope_name list -val type_scope : scope_name val declare_scope : scope_name -> unit val current_scopes : unit -> scopes @@ -165,6 +164,9 @@ val declare_ref_arguments_scope : global_reference -> unit val compute_arguments_scope : Term.types -> scope_name option list val compute_type_scope : Term.types -> scope_name option +(** Get the current scope bound to Sortclass, if it exists *) +val current_type_scope_name : unit -> scope_name option + val scope_class_of_class : Classops.cl_typ -> scope_class (** Building notation key *) diff --git a/test-suite/bugs/closed/3080.v b/test-suite/bugs/closed/3080.v new file mode 100644 index 000000000..7d0dc090e --- /dev/null +++ b/test-suite/bugs/closed/3080.v @@ -0,0 +1,18 @@ +(* -*- coq-prog-args: ("-emacs" "-nois") -*- *) +Delimit Scope type_scope with type. +Delimit Scope function_scope with function. + +Bind Scope type_scope with Sortclass. +Bind Scope function_scope with Funclass. + +Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). +Notation "A -> B" := (forall (_ : A), B) : type_scope. + +Definition compose {A B C} (g : B -> C) (f : A -> B) := + fun x : A => g (f x). + +Notation " g ∘ f " := (compose g f) + (at level 40, left associativity) : function_scope. + +Fail Check (fun x => x) ∘ (fun x => x). (* this [Check] should fail, as [function_scope] is not opened *) +Check compose ((fun x => x) ∘ (fun x => x)) (fun x => x). (* this check should succeed, as [function_scope] should be automatically bound in the arugments to [compose] *) diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v index 9125ab16d..324c12525 100644 --- a/test-suite/bugs/closed/3612.v +++ b/test-suite/bugs/closed/3612.v @@ -6,6 +6,8 @@ lines, then from 421 lines to 428 lines, then from 444 lines to 429 lines, then Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Reserved Notation "x = y :> T" (at level 70, y at next level, no associativity). Reserved Notation "x = y" (at level 70, no associativity). +Delimit Scope type_scope with type. +Bind Scope type_scope with Sortclass. Open Scope type_scope. Global Set Universe Polymorphism. Notation "A -> B" := (forall (_ : A), B) : type_scope. diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v index 06188e7b1..fc60897d2 100644 --- a/test-suite/bugs/closed/3649.v +++ b/test-suite/bugs/closed/3649.v @@ -4,6 +4,8 @@ coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *) Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Reserved Notation "x = y" (at level 70, no associativity). +Delimit Scope type_scope with type. +Bind Scope type_scope with Sortclass. Open Scope type_scope. Axiom admit : forall {T}, T. Notation "A -> B" := (forall (_ : A), B) : type_scope. @@ -54,4 +56,4 @@ Goal forall (C D : PreCategory) (G G' : Functor C D) (** This [change] succeeded, but did not progress, in 07e4438bd758c2ced8caf09a6961ccd77d84e42b, because [T0 x o T1 x] was not found in the goal *) let T0 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T0) end in let T1 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T1) end in - progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)). \ No newline at end of file + progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)). diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 50728136b..ef6125e6f 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -79,6 +79,7 @@ Delimit Scope type_scope with type. Delimit Scope function_scope with function. Delimit Scope core_scope with core. +Bind Scope type_scope with Sortclass. Bind Scope function_scope with Funclass. Open Scope core_scope. -- cgit v1.2.3