summaryrefslogtreecommitdiff
path: root/interp/notation.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/notation.ml')
-rw-r--r--interp/notation.ml199
1 files changed, 111 insertions, 88 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index 5c10e0af..389a1c9d 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -7,13 +7,12 @@
(************************************************************************)
(*i*)
-open Errors
+open CErrors
open Util
open Pp
open Bigint
open Names
open Term
-open Nametab
open Libnames
open Globnames
open Constrexpr
@@ -45,8 +44,14 @@ type level = precedence * tolerability list
type delimiters = string
type notation_location = (DirPath.t * DirPath.t) * string
+type notation_data = {
+ not_interp : interpretation;
+ not_location : notation_location;
+ not_onlyprinting : bool;
+}
+
type scope = {
- notations: (interpretation * notation_location) String.Map.t;
+ notations: notation_data String.Map.t;
delimiters: delimiters option
}
@@ -65,11 +70,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 *)
@@ -187,7 +190,8 @@ let declare_delimiters scope key =
| None -> scope_map := String.Map.add scope newsc !scope_map
| Some oldkey when String.equal oldkey key -> ()
| Some oldkey ->
- msg_warning
+ (** FIXME: implement multikey scopes? *)
+ Flags.if_verbose Feedback.msg_info
(str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope);
scope_map := String.Map.add scope newsc !scope_map
end;
@@ -195,7 +199,7 @@ let declare_delimiters scope key =
let oldscope = String.Map.find key !delimiters_map in
if String.equal oldscope scope then ()
else begin
- msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope);
+ Flags.if_verbose Feedback.msg_info (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope);
delimiters_map := String.Map.add key scope !delimiters_map
end
with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map
@@ -204,7 +208,7 @@ let remove_delimiters scope =
let sc = find_scope scope in
let newsc = { sc with delimiters = None } in
match sc.delimiters with
- | None -> msg_warning (str "No bound key for scope " ++ str scope ++ str ".")
+ | None -> CErrors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".")
| Some key ->
scope_map := String.Map.add scope newsc !scope_map;
try
@@ -314,7 +318,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 +332,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 ()
@@ -381,17 +387,28 @@ let level_of_notation ntn =
(* The mapping between notations and their interpretation *)
-let declare_notation_interpretation ntn scopt pat df =
+let warn_notation_overridden =
+ CWarnings.create ~name:"notation-overridden" ~category:"parsing"
+ (fun (ntn,which_scope) ->
+ str "Notation" ++ spc () ++ str ntn ++ spc ()
+ ++ strbrk "was already used" ++ which_scope)
+
+let declare_notation_interpretation ntn scopt pat df ~onlyprint =
let scope = match scopt with Some s -> s | None -> default_scope in
let sc = find_scope scope in
let () =
if String.Map.mem ntn sc.notations then
let which_scope = match scopt with
| None -> mt ()
- | Some _ -> str " in scope " ++ str scope in
- msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope)
+ | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in
+ warn_notation_overridden (ntn,which_scope)
in
- let sc = { sc with notations = String.Map.add ntn (pat,df) sc.notations } in
+ let notdata = {
+ not_interp = pat;
+ not_location = df;
+ not_onlyprinting = onlyprint;
+ } in
+ let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in
let () = scope_map := String.Map.add scope sc !scope_map in
begin match scopt with
| None -> scope_stack := SingleNotation ntn :: !scope_stack
@@ -416,7 +433,9 @@ let rec find_interpretation ntn find = function
find_interpretation ntn find scopes
let find_notation ntn sc =
- String.Map.find ntn (find_scope sc).notations
+ let n = String.Map.find ntn (find_scope sc).notations in
+ let () = if n.not_onlyprinting then raise Not_found in
+ (n.not_interp, n.not_location)
let notation_of_prim_token = function
| Numeral n when is_pos_or_zero n -> to_string n
@@ -529,26 +548,25 @@ 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)) =
- Id.equal id1 id2 &&
+let var_attributes_eq (_, (sc1, tp1)) (_, (sc2, tp2)) =
pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
ntpe_eq tp1 tp2
let interpretation_eq (vars1, t1) (vars2, t2) =
- List.equal vars_eq vars1 vars2 &&
- Notation_ops.eq_notation_constr t1 t2
+ List.equal var_attributes_eq vars1 vars2 &&
+ Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2
let exists_notation_in_scope scopt ntn r =
let scope = match scopt with Some s -> s | None -> default_scope in
try
let sc = String.Map.find scope !scope_map in
- let (r',_) = String.Map.find ntn sc.notations in
- interpretation_eq r' r
+ let n = String.Map.find ntn sc.notations in
+ interpretation_eq n.not_interp r
with Not_found -> false
let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
@@ -556,23 +574,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 +594,7 @@ end
module ScopeClassMap = Map.Make(ScopeClassOrd)
let initial_scope_class_map : scope_name ScopeClassMap.t =
- ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty
+ ScopeClassMap.empty
let scope_class_map = ref initial_scope_class_map
@@ -617,8 +628,11 @@ 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 current_type_scope_name () =
+ find_scope_class_opt (Some CL_SORT)
+
+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
@@ -642,7 +656,7 @@ type arguments_scope_discharge_request =
| ArgsScopeManual
| ArgsScopeNoDischarge
-let load_arguments_scope _ (_,(_,r,scl,cls)) =
+let load_arguments_scope _ (_,(_,r,n,scl,cls)) =
List.iter (Option.iter check_scope) scl;
let initial_stamp = ScopeClassMap.empty in
arguments_scope := Refmap.add r (scl,cls,initial_stamp) !arguments_scope
@@ -650,14 +664,10 @@ 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 subst_arguments_scope (subst,(req,r,n,scl,cls)) =
let r' = fst (subst_global subst r) in
let subst_cl ocl = match ocl with
| None -> ocl
@@ -666,34 +676,42 @@ let subst_arguments_scope (subst,(req,r,scl,cls)) =
| Some cl' as ocl' when cl' != cl -> ocl'
| _ -> ocl in
let cls' = List.smartmap subst_cl cls in
- (ArgsScopeNoDischarge,r',scl,cls')
+ (ArgsScopeNoDischarge,r',n,scl,cls')
-let discharge_arguments_scope (_,(req,r,l,_)) =
+let discharge_arguments_scope (_,(req,r,n,l,_)) =
if req == ArgsScopeNoDischarge || (isVarRef r && Lib.is_in_section r) then None
- else Some (req,Lib.discharge_global r,l,[])
+ else
+ let n =
+ try
+ let vars = Lib.variable_section_segment_of_reference r in
+ List.length (List.filter (fun (_,_,b,_) -> b = None) vars)
+ with
+ Not_found (* Not a ref defined in this section *) -> 0 in
+ Some (req,Lib.discharge_global r,n,l,[])
-let classify_arguments_scope (req,_,_,_ as obj) =
+let classify_arguments_scope (req,_,_,_,_ as obj) =
if req == ArgsScopeNoDischarge then Dispose else Substitute obj
-let rebuild_arguments_scope (req,r,l,_) =
+let rebuild_arguments_scope (req,r,n,l,_) =
match req with
| ArgsScopeNoDischarge -> assert false
| ArgsScopeAuto ->
let scs,cls = compute_arguments_scope_full (fst(Universes.type_of_global r)(*FIXME?*)) in
- (req,r,scs,cls)
+ (req,r,List.length scs,scs,cls)
| ArgsScopeManual ->
(* Add to the manually given scopes the one found automatically
for the extra parameters of the section. Discard the classes
of the manually given scopes to avoid further re-computations. *)
- let l',cls = compute_arguments_scope_full (Global.type_of_global_unsafe r) in
- let nparams = List.length l' - List.length l in
- let l1 = List.firstn nparams l' in
- let cls1 = List.firstn nparams cls in
- (req,r,l1@l,cls1)
+ let l',cls = compute_arguments_scope_full (Global.type_of_global_unsafe r) in
+ let l1 = List.firstn n l' in
+ let cls1 = List.firstn n cls in
+ (req,r,0,l1@l,cls1)
type arguments_scope_obj =
arguments_scope_discharge_request * global_reference *
- scope_name option list * scope_class option list
+ (* Used to communicate information from discharge to rebuild *)
+ (* set to 0 otherwise *) int *
+ scope_name option list * scope_class option list
let inArgumentsScope : arguments_scope_obj -> obj =
declare_object {(default_object "ARGUMENTS-SCOPE") with
@@ -706,16 +724,15 @@ let inArgumentsScope : arguments_scope_obj -> obj =
let is_local local ref = local || isVarRef ref && Lib.is_in_section ref
-let declare_arguments_scope_gen req r (scl,cls) =
- Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl,cls))
+let declare_arguments_scope_gen req r n (scl,cls) =
+ Lib.add_anonymous_leaf (inArgumentsScope (req,r,n,scl,cls))
let declare_arguments_scope local r scl =
- let req = if is_local local r then ArgsScopeNoDischarge else ArgsScopeManual
- in
- (* We empty the list of argument classes to disable futher scope
+ let req = if is_local local r then ArgsScopeNoDischarge else ArgsScopeManual in
+ (* We empty the list of argument classes to disable further scope
re-computations and keep these manually given scopes. *)
- declare_arguments_scope_gen req r (scl,[])
-
+ declare_arguments_scope_gen req r 0 (scl,[])
+
let find_arguments_scope r =
try
let (scl,cls,stamp) = Refmap.find r !arguments_scope in
@@ -730,7 +747,8 @@ let find_arguments_scope r =
let declare_ref_arguments_scope ref =
let t = Global.type_of_global_unsafe ref in
- declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope_full t)
+ let (scs,cls as o) = compute_arguments_scope_full t in
+ declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o
(********************************)
@@ -788,9 +806,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
@@ -815,7 +831,7 @@ let pr_named_scope prglob scope sc =
++ fnl ()
++ pr_scope_classes scope
++ String.Map.fold
- (fun ntn ((_,r),(_,df)) strm ->
+ (fun ntn { not_interp = (_, r); not_location = (_, df) } strm ->
pr_notation_info prglob df r ++ fnl () ++ strm)
sc.notations (mt ())
@@ -859,7 +875,7 @@ let browse_notation strict ntn map =
let l =
String.Map.fold
(fun scope_name sc ->
- String.Map.fold (fun ntn ((_,r),df) l ->
+ String.Map.fold (fun ntn { not_interp = (_, r); not_location = df } l ->
if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
map [] in
List.sort (fun x y -> String.compare (fst x) (fst y)) l
@@ -925,7 +941,7 @@ let locate_notation prglob ntn scope =
let collect_notation_in_scope scope sc known =
assert (not (String.equal scope default_scope));
String.Map.fold
- (fun ntn ((_,r),(_,df)) (l,known as acc) ->
+ (fun ntn { not_interp = (_, r); not_location = (_, df) } (l,known as acc) ->
if String.List.mem ntn known then acc else ((df,r)::l,ntn::known))
sc.notations ([],known)
@@ -941,7 +957,7 @@ let collect_notations stack =
| SingleNotation ntn ->
if String.List.mem ntn knownntn then (all,knownntn)
else
- let ((_,r),(_,df)) =
+ let { not_interp = (_, r); not_location = (_, df) } =
String.Map.find ntn (find_scope default_scope).notations in
let all' = match all with
| (s,lonelyntn)::rest when String.equal s default_scope ->
@@ -977,23 +993,30 @@ let pr_visibility prglob = function
type unparsing_rule = unparsing list * precedence
type extra_unparsing_rules = (string * string) list
(* Concrete syntax for symbolic-extension table *)
-let printing_rules =
- ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules) String.Map.t)
+let notation_rules =
+ ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t)
-let declare_notation_printing_rule ntn ~extra unpl =
- printing_rules := String.Map.add ntn (unpl,extra) !printing_rules
+let declare_notation_rule ntn ~extra unpl gram =
+ notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules
let find_notation_printing_rule ntn =
- try fst (String.Map.find ntn !printing_rules)
+ try pi1 (String.Map.find ntn !notation_rules)
with Not_found -> anomaly (str "No printing rule found for " ++ str ntn)
let find_notation_extra_printing_rules ntn =
- try snd (String.Map.find ntn !printing_rules)
+ try pi2 (String.Map.find ntn !notation_rules)
with Not_found -> []
+let find_notation_parsing_rules ntn =
+ try pi3 (String.Map.find ntn !notation_rules)
+ with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn)
+
+let get_defined_notations () =
+ String.Set.elements @@ String.Map.domain !notation_rules
+
let add_notation_extra_printing_rule ntn k v =
try
- printing_rules :=
- let p, pp = String.Map.find ntn !printing_rules in
- String.Map.add ntn (p, (k,v) :: pp) !printing_rules
+ notation_rules :=
+ let p, pp, gr = String.Map.find ntn !notation_rules in
+ String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules
with Not_found ->
user_err_loc (Loc.ghost,"add_notation_extra_printing_rule",
str "No such Notation.")
@@ -1003,7 +1026,7 @@ let add_notation_extra_printing_rule ntn k v =
let freeze _ =
(!scope_map, !notation_level_map, !scope_stack, !arguments_scope,
- !delimiters_map, !notations_key_table, !printing_rules,
+ !delimiters_map, !notations_key_table, !notation_rules,
!scope_class_map)
let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
@@ -1013,7 +1036,7 @@ let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
delimiters_map := dlm;
arguments_scope := asc;
notations_key_table := fkm;
- printing_rules := pprules;
+ notation_rules := pprules;
scope_class_map := clsc
let init () =
@@ -1021,7 +1044,7 @@ let init () =
notation_level_map := String.Map.empty;
delimiters_map := String.Map.empty;
notations_key_table := KeyMap.empty;
- printing_rules := String.Map.empty;
+ notation_rules := String.Map.empty;
scope_class_map := initial_scope_class_map
let _ =
@@ -1034,6 +1057,6 @@ let with_notation_protection f x =
let fs = freeze false in
try let a = f x in unfreeze fs; a
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
let () = unfreeze fs in
iraise reraise
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 01:59:21 +0000