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 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.ml | 37 ++++++++++++------------------------- 1 file changed, 12 insertions(+), 25 deletions(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index d18b804bfd..075e04cba0 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -556,23 +556,16 @@ let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) (* Mapping classes to scopes *) -type scope_class = ScopeRef of global_reference | ScopeSort +open Classops -let scope_class_compare sc1 sc2 = match sc1, sc2 with -| ScopeRef gr1, ScopeRef gr2 -> RefOrdered.compare gr1 gr2 -| ScopeRef _, ScopeSort -> -1 -| ScopeSort, ScopeRef _ -> 1 -| ScopeSort, ScopeSort -> 0 +type scope_class = cl_typ -let scope_class_of_reference x = ScopeRef x +let scope_class_compare : scope_class -> scope_class -> int = + cl_typ_ord let compute_scope_class t = - let t', _ = decompose_appvect (Reductionops.whd_betaiotazeta Evd.empty t) in - match kind_of_term t' with - | Var _ | Const _ | Ind _ -> ScopeRef (global_of_constr t') - | Proj (p, c) -> ScopeRef (ConstRef (Projection.constant p)) - | Sort _ -> ScopeSort - | _ -> raise Not_found + let (cl,_,_) = find_class_type Evd.empty t in + cl module ScopeClassOrd = struct @@ -583,7 +576,7 @@ end module ScopeClassMap = Map.Make(ScopeClassOrd) let initial_scope_class_map : scope_name ScopeClassMap.t = - ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty + ScopeClassMap.add CL_SORT type_scope ScopeClassMap.empty let scope_class_map = ref initial_scope_class_map @@ -617,8 +610,8 @@ 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 compute_scope_of_global ref = - find_scope_class_opt (Some (ScopeRef ref)) +let scope_class_of_class (x : cl_typ) : scope_class = + x (** Updating a scope list, thanks to a list of argument classes and the current Bind Scope base. When some current scope @@ -650,12 +643,8 @@ let load_arguments_scope _ (_,(_,r,scl,cls)) = let cache_arguments_scope o = load_arguments_scope 1 o -let subst_scope_class subst cs = match cs with - | ScopeSort -> Some cs - | ScopeRef t -> - let (t',c) = subst_global subst t in - if t == t' then Some cs - else try Some (compute_scope_class c) with Not_found -> None +let subst_scope_class subst cs = + try Some (subst_cl_typ subst cs) with Not_found -> None let subst_arguments_scope (subst,(req,r,scl,cls)) = let r' = fst (subst_global subst r) in @@ -788,9 +777,7 @@ let pr_delimiters_info = function let classes_of_scope sc = ScopeClassMap.fold (fun cl sc' l -> if String.equal sc sc' then cl::l else l) !scope_class_map [] -let pr_scope_class = function - | ScopeSort -> str "Sort" - | ScopeRef t -> pr_global_env Id.Set.empty t +let pr_scope_class = pr_class let pr_scope_classes sc = let l = classes_of_scope sc in -- 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/notation.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index 075e04cba0..8395f7d9ad 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 -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- interp/notation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index d18b804bfd..5c10e0af71 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* P)" or `Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))') and those which are associated to at list one subterm (e.g. `Notation "x .+1" := (S x)' but also "Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))' as in #4592). The former have type NtnTypeOnlyBinder. - Thus avoiding in particular encoding too early Anonymous as GHole and "Name id" as "GVar id". There is a non-trivial alpha-conversion work to do to get #4592 working. See comments in Notation_ops.add_env. --- interp/notation.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index 5c10e0af71..04918bf7dd 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -529,9 +529,10 @@ let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true +| NtnTypeOnlyBinder, NtnTypeOnlyBinder -> true | NtnTypeConstrList, NtnTypeConstrList -> true | NtnTypeBinderList, NtnTypeBinderList -> true -| (NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList), _ -> false +| (NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList), _ -> false let vars_eq (id1, (sc1, tp1)) (id2, (sc2, tp2)) = -- cgit v1.2.3 From 508d5a99101097948b6de342295eec0d5c8cbe72 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 3 Mar 2016 18:59:51 +0100 Subject: Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop. Printing invalid UTF-8 string startled GTK too much, leading to CoqIDE dying improperly. We now check that all strings outputed by Coq are proper UTF-8. This is not perfect, as CoqIDE will sometimes truncate strings which contains the null character, but at least it should not crash. --- interp/notation.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index 5c10e0af71..c4addbf10f 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -314,7 +314,9 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) = patl let mkNumeral n = Numeral n -let mkString s = String s +let mkString = function +| None -> None +| Some s -> if Unicode.is_utf8 s then Some (String s) else None let delay dir int loc x = (dir, (fun () -> int loc x)) @@ -326,7 +328,7 @@ let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) = let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = declare_prim_token_interpreter sc (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p) - (patl, (fun r -> Option.map mkString (uninterp r)), inpat) + (patl, (fun r -> mkString (uninterp r)), inpat) let check_required_module loc sc (sp,d) = try let _ = Nametab.global_of_path sp in () -- cgit v1.2.3