From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- interp/notation.ml | 199 ++++++++++++++++++++++++++++++----------------------- 1 file changed, 111 insertions(+), 88 deletions(-) (limited to 'interp/notation.ml') 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 -- cgit v1.2.3