diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 425 |
1 files changed, 275 insertions, 150 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 389a1c9d..bb58f00c 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1,18 +1,19 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) open CErrors open Util open Pp -open Bigint open Names -open Term +open Constr open Libnames open Globnames open Constrexpr @@ -20,6 +21,8 @@ open Notation_term open Glob_term open Glob_ops open Ppextend +open Context.Named.Declaration + (*i*) (*s A scope is a set of notations; it includes @@ -40,14 +43,12 @@ open Ppextend (**********************************************************************) (* Scope of symbols *) -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 = { @@ -82,11 +83,35 @@ let parenRelation_eq t1 t2 = match t1, t2 with | Prec l1, Prec l2 -> Int.equal l1 l2 | _ -> false -let level_eq (l1, t1) (l2, t2) = - let tolerability_eq (i1, r1) (i2, r2) = - Int.equal i1 i2 && parenRelation_eq r1 r2 - in +open Extend + +let production_level_eq l1 l2 = true (* (l1 = l2) *) + +let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with +| NextLevel, NextLevel -> true +| NumLevel n1, NumLevel n2 -> Int.equal n1 n2 +| (NextLevel | NumLevel _), _ -> false *) + +let constr_entry_key_eq eq v1 v2 = match v1, v2 with +| ETName, ETName -> true +| ETReference, ETReference -> true +| ETBigint, ETBigint -> true +| ETBinder b1, ETBinder b2 -> b1 == b2 +| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2 +| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2 +| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2 +| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2' +| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false + +let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) = + let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in + let prod_eq (l1,pp1) (l2,pp2) = + if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2 + else production_level_eq l1 l2 in Int.equal l1 l2 && List.equal tolerability_eq t1 t2 + && List.equal (constr_entry_key_eq prod_eq) u1 u2 + +let level_eq = level_eq_gen false let declare_scope scope = try let _ = String.Map.find scope !scope_map in () @@ -95,7 +120,7 @@ let declare_scope scope = scope_map := String.Map.add scope empty_scope !scope_map let error_unknown_scope sc = - errorlabstrm "Notation" + user_err ~hdr:"Notation" (str "Scope " ++ str sc ++ str " is not declared.") let find_scope scope = @@ -208,7 +233,7 @@ let remove_delimiters scope = let sc = find_scope scope in let newsc = { sc with delimiters = None } in match sc.delimiters with - | None -> CErrors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".") + | None -> CErrors.user_err (str "No bound key for scope " ++ str scope ++ str ".") | Some key -> scope_map := String.Map.add scope newsc !scope_map; try @@ -217,17 +242,17 @@ let remove_delimiters scope = with Not_found -> assert false (* A delimiter for scope [scope] should exist *) -let find_delimiters_scope loc key = +let find_delimiters_scope ?loc key = try String.Map.find key !delimiters_map with Not_found -> - user_err_loc - (loc, "find_delimiters", str "Unknown scope delimiting key " ++ str key ++ str ".") + user_err ?loc ~hdr:"find_delimiters" + (str "Unknown scope delimiting key " ++ str key ++ str ".") (* Uninterpretation tables *) type interp_rule = | NotationRule of scope_name option * notation - | SynDefRule of kernel_name + | SynDefRule of KerName.t (* We define keys for glob_constr and aconstr to split the syntax entries according to the key of the pattern (adapted from Chet Murthy by HH) *) @@ -258,25 +283,34 @@ let keymap_find key map = (* Scopes table : interpretation -> scope_name *) let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) -let prim_token_key_table = ref KeyMap.empty +let prim_token_key_table = ref (KeyMap.empty : (string * (any_glob_constr -> prim_token option) * bool) KeyMap.t) -let glob_prim_constr_key = function - | GApp (_,GRef (_,ref,_),_) | GRef (_,ref,_) -> RefKey (canonical_gr ref) +let glob_prim_constr_key c = match DAst.get c with + | GRef (ref, _) -> RefKey (canonical_gr ref) + | GApp (c, _) -> + begin match DAst.get c with + | GRef (ref, _) -> RefKey (canonical_gr ref) + | _ -> Oth + end | _ -> Oth -let glob_constr_keys = function - | GApp (_,GRef (_,ref,_),_) -> [RefKey (canonical_gr ref); Oth] - | GRef (_,ref,_) -> [RefKey (canonical_gr ref)] +let glob_constr_keys c = match DAst.get c with + | GApp (c, _) -> + begin match DAst.get c with + | GRef (ref, _) -> [RefKey (canonical_gr ref); Oth] + | _ -> [Oth] + end + | GRef (ref,_) -> [RefKey (canonical_gr ref)] | _ -> [Oth] -let cases_pattern_key = function - | PatCstr (_,ref,_,_) -> RefKey (canonical_gr (ConstructRef ref)) +let cases_pattern_key c = match DAst.get c with + | PatCstr (ref,_,_) -> RefKey (canonical_gr (ConstructRef ref)) | _ -> Oth let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) | NList (_,_,NApp (NRef ref,args),_,_) - | NBinderList (_,_,NApp (NRef ref,args),_) -> + | NBinderList (_,_,NApp (NRef ref,args),_,_) -> RefKey (canonical_gr ref), Some (List.length args) | NRef ref -> RefKey(canonical_gr ref), None | NApp (_,args) -> Oth, Some (List.length args) @@ -288,15 +322,15 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) type required_module = full_path * string list type 'a prim_token_interpreter = - Loc.t -> 'a -> glob_constr + ?loc:Loc.t -> 'a -> glob_constr type cases_pattern_status = bool (* true = use prim token in patterns *) type 'a prim_token_uninterpreter = - glob_constr list * (glob_constr -> 'a option) * cases_pattern_status + glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status type internal_prim_token_interpreter = - Loc.t -> prim_token -> required_module * (unit -> glob_constr) + ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr) let prim_token_interpreter_tab = (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t) @@ -306,7 +340,7 @@ let add_prim_token_interpreter sc interp = let cont = Hashtbl.find prim_token_interpreter_tab sc in Hashtbl.replace prim_token_interpreter_tab sc (interp cont) with Not_found -> - let cont = (fun _loc _p -> raise Not_found) in + let cont = (fun ?loc _p -> raise Not_found) in Hashtbl.add prim_token_interpreter_tab sc (interp cont) let declare_prim_token_interpreter sc interp (patl,uninterp,b) = @@ -317,28 +351,46 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) = (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table) patl -let mkNumeral n = Numeral n +let mkNumeral n = + if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true) + else Numeral (Bigint.to_string (Bigint.neg n), false) + +let ofNumeral n s = + if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) + 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)) +let delay dir int ?loc x = (dir, (fun () -> int ?loc x)) + +type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign + +let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) = + declare_prim_token_interpreter sc + (fun cont ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s) + | p -> cont ?loc p) + (patl, (fun r -> match uninterp r with + | None -> None + | Some (n,s) -> Some (Numeral (n,s))), inpat) let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) = + let interp' ?loc (n,s) = interp ?loc (ofNumeral n s) in declare_prim_token_interpreter sc - (fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p) + (fun cont ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s) + | p -> cont ?loc p) (patl, (fun r -> Option.map mkNumeral (uninterp r)), 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) + (fun cont ?loc -> function String s -> delay dir interp ?loc s | p -> cont ?loc p) (patl, (fun r -> mkString (uninterp r)), inpat) -let check_required_module loc sc (sp,d) = +let check_required_module ?loc sc (sp,d) = try let _ = Nametab.global_of_path sp in () with Not_found -> - user_err_loc (loc,"prim_token_interpreter", - str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") + user_err ?loc ~hdr:"prim_token_interpreter" + (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") (* Look if some notation or numeral printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) @@ -377,13 +429,15 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function (* Uninterpreted notation levels *) -let declare_notation_level ntn level = +let declare_notation_level ?(onlyprint=false) ntn level = if String.Map.mem ntn !notation_level_map then - anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level"); - notation_level_map := String.Map.add ntn level !notation_level_map + anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level."); + notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map -let level_of_notation ntn = - String.Map.find ntn !notation_level_map +let level_of_notation ?(onlyprint=false) ntn = + let (level,onlyprint') = String.Map.find ntn !notation_level_map in + if onlyprint' && not onlyprint then raise Not_found; + level (* The mapping between notations and their interpretation *) @@ -391,25 +445,26 @@ 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) + ++ strbrk "was already used" ++ which_scope ++ str ".") 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 _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in - warn_notation_overridden (ntn,which_scope) - 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 + if not onlyprint then begin + let () = + if String.Map.mem ntn sc.notations then + let which_scope = match scopt with + | None -> mt () + | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in + warn_notation_overridden (ntn,which_scope) + in + let notdata = { + not_interp = pat; + not_location = df; + } in + let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in + scope_map := String.Map.add scope sc !scope_map + end; begin match scopt with | None -> scope_stack := SingleNotation ntn :: !scope_stack | Some _ -> () @@ -434,57 +489,62 @@ let rec find_interpretation ntn find = function let find_notation ntn sc = 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 - | Numeral n -> "- "^(to_string (neg n)) + | Numeral (n,true) -> n + | Numeral (n,false) -> "- "^n | String _ -> raise Not_found -let find_prim_token g loc p sc = +let find_prim_token check_allowed ?loc p sc = (* Try for a user-defined numerical notation *) try let (_,c),df = find_notation (notation_of_prim_token p) sc in - g (Notation_ops.glob_constr_of_notation_constr loc c),df + let pat = Notation_ops.glob_constr_of_notation_constr ?loc c in + check_allowed pat; + pat, df with Not_found -> (* Try for a primitive numerical notation *) - let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in - check_required_module loc sc spdir; - g (interp ()), ((dirpath (fst spdir),DirPath.empty),"") + let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc ?loc p in + check_required_module ?loc sc spdir; + let pat = interp () in + check_allowed pat; + pat, ((dirpath (fst spdir),DirPath.empty),"") -let interp_prim_token_gen g loc p local_scopes = +let interp_prim_token_gen ?loc g p local_scopes = let scopes = make_current_scopes local_scopes in let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in - try find_interpretation p_as_ntn (find_prim_token g loc p) scopes + try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes with Not_found -> - user_err_loc (loc,"interp_prim_token", - (match p with - | Numeral n -> str "No interpretation for numeral " ++ str (to_string n) + user_err ?loc ~hdr:"interp_prim_token" + ((match p with + | Numeral _ -> + str "No interpretation for numeral " ++ str (notation_of_prim_token p) | String s -> str "No interpretation for string " ++ qs s) ++ str ".") -let interp_prim_token = - interp_prim_token_gen (fun x -> x) - -(** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) - -let rec rcp_of_glob looked_for = function - | GVar (loc,id) -> RCPatAtom (loc,Some id) - | GHole (loc,_,_,_) -> RCPatAtom (loc,None) - | GRef (loc,g,_) -> looked_for g; RCPatCstr (loc, g,[],[]) - | GApp (loc,GRef (_,g,_),l) -> - looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[]) - | _ -> raise Not_found +let interp_prim_token ?loc = + interp_prim_token_gen ?loc (fun _ -> ()) + +let rec check_allowed_ref_in_pat looked_for = DAst.(with_val (function + | GVar _ | GHole _ -> () + | GRef (g,_) -> looked_for g + | GApp (f, l) -> + begin match DAst.get f with + | GRef (g, _) -> + looked_for g; List.iter (check_allowed_ref_in_pat looked_for) l + | _ -> raise Not_found + end + | _ -> raise Not_found)) -let interp_prim_token_cases_pattern_expr loc looked_for p = - interp_prim_token_gen (rcp_of_glob looked_for) loc p +let interp_prim_token_cases_pattern_expr ?loc looked_for p = + interp_prim_token_gen ?loc (check_allowed_ref_in_pat looked_for) p -let interp_notation loc ntn local_scopes = +let interp_notation ?loc ntn local_scopes = let scopes = make_current_scopes local_scopes in try find_interpretation ntn (find_notation ntn) scopes with Not_found -> - user_err_loc - (loc,"",str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") + user_err ?loc + (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") let uninterp_notations c = List.map_append (fun key -> keymap_find key !notations_key_table) @@ -505,7 +565,7 @@ let uninterp_prim_token c = try let (sc,numpr,_) = KeyMap.find (glob_prim_constr_key c) !prim_token_key_table in - match numpr c with + match numpr (AnyGlobConstr c) with | None -> raise Notation_ops.No_match | Some n -> (sc,n) with Not_found -> raise Notation_ops.No_match @@ -518,8 +578,8 @@ let uninterp_prim_token_ind_pattern ind args = if not b then raise Notation_ops.No_match; let args' = List.map (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in - let ref = GRef (Loc.ghost,ref,None) in - match numpr (GApp (Loc.ghost,ref,args')) with + let ref = DAst.make @@ GRef (ref,None) in + match numpr (AnyGlobConstr (DAst.make @@ GApp (ref,args'))) with | None -> raise Notation_ops.No_match | Some n -> (sc,n) with Not_found -> raise Notation_ops.No_match @@ -530,14 +590,14 @@ let uninterp_prim_token_cases_pattern c = let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in if not b then raise Notation_ops.No_match; let na,c = glob_constr_of_closed_cases_pattern c in - match numpr c with + match numpr (AnyGlobConstr c) with | None -> raise Notation_ops.No_match | Some n -> (na,sc,n) with Not_found -> raise Notation_ops.No_match let availability_of_prim_token n printer_scope local_scopes = let f scope = - try ignore (Hashtbl.find prim_token_interpreter_tab scope Loc.ghost n); true + try ignore ((Hashtbl.find prim_token_interpreter_tab scope) n); true with Not_found -> false in let scopes = make_current_scopes local_scopes in Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes) @@ -546,12 +606,18 @@ let availability_of_prim_token n printer_scope local_scopes = let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 +let notation_binder_source_eq s1 s2 = match s1, s2 with +| NtnParsedAsIdent, NtnParsedAsIdent -> true +| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 +| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2 +| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false + let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true -| NtnTypeOnlyBinder, NtnTypeOnlyBinder -> true +| NtnTypeBinder s1, NtnTypeBinder s2 -> notation_binder_source_eq s1 s2 | NtnTypeConstrList, NtnTypeConstrList -> true | NtnTypeBinderList, NtnTypeBinderList -> true -| (NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList), _ -> false +| (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false let var_attributes_eq (_, (sc1, tp1)) (_, (sc2, tp2)) = pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && @@ -561,7 +627,7 @@ let interpretation_eq (vars1, t1) (vars2, 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 exists_notation_in_scope scopt ntn onlyprint r = let scope = match scopt with Some s -> s | None -> default_scope in try let sc = String.Map.find scope !scope_map in @@ -581,8 +647,8 @@ type scope_class = cl_typ let scope_class_compare : scope_class -> scope_class -> int = cl_typ_ord -let compute_scope_class t = - let (cl,_,_) = find_class_type Evd.empty t in +let compute_scope_class sigma t = + let (cl,_,_) = find_class_type sigma t in cl module ScopeClassOrd = @@ -611,22 +677,22 @@ let find_scope_class_opt = function (**********************************************************************) (* Special scopes associated to arguments of a global reference *) -let rec compute_arguments_classes t = - match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty t) with +let rec compute_arguments_classes sigma t = + match EConstr.kind sigma (Reductionops.whd_betaiotazeta sigma t) with | Prod (_,t,u) -> - let cl = try Some (compute_scope_class t) with Not_found -> None in - cl :: compute_arguments_classes u + let cl = try Some (compute_scope_class sigma t) with Not_found -> None in + cl :: compute_arguments_classes sigma u | _ -> [] -let compute_arguments_scope_full t = - let cls = compute_arguments_classes t in +let compute_arguments_scope_full sigma t = + let cls = compute_arguments_classes sigma t in let scs = List.map find_scope_class_opt cls in scs, cls -let compute_arguments_scope t = fst (compute_arguments_scope_full t) +let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t) -let compute_type_scope t = - find_scope_class_opt (try Some (compute_scope_class t) with Not_found -> None) +let compute_type_scope sigma t = + find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None) let current_type_scope_name () = find_scope_class_opt (Some CL_SORT) @@ -684,7 +750,7 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) = let n = try let vars = Lib.variable_section_segment_of_reference r in - List.length (List.filter (fun (_,_,b,_) -> b = None) vars) + vars |> List.map fst |> List.filter is_local_assum |> List.length with Not_found (* Not a ref defined in this section *) -> 0 in Some (req,Lib.discharge_global r,n,l,[]) @@ -692,20 +758,24 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) = let classify_arguments_scope (req,_,_,_,_ as obj) = if req == ArgsScopeNoDischarge then Dispose else Substitute obj -let rebuild_arguments_scope (req,r,n,l,_) = +let rebuild_arguments_scope sigma (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,List.length scs,scs,cls) + let env = Global.env () in (*FIXME?*) + let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in + let scs,cls = compute_arguments_scope_full sigma typ in + (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 l1 = List.firstn n l' in - let cls1 = List.firstn n cls in - (req,r,0,l1@l,cls1) + (* 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 env = Global.env () in (*FIXME?*) + let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in + let l',cls = compute_arguments_scope_full sigma typ 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 * @@ -720,7 +790,8 @@ let inArgumentsScope : arguments_scope_obj -> obj = subst_function = subst_arguments_scope; classify_function = classify_arguments_scope; discharge_function = discharge_arguments_scope; - rebuild_function = rebuild_arguments_scope } + (* XXX: Should we pass the sigma here or not, see @herbelin's comment in 6511 *) + rebuild_function = rebuild_arguments_scope Evd.empty } let is_local local ref = local || isVarRef ref && Lib.is_in_section ref @@ -732,7 +803,7 @@ let declare_arguments_scope local r scl = (* 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 0 (scl,[]) - + let find_arguments_scope r = try let (scl,cls,stamp) = Refmap.find r !arguments_scope in @@ -745,12 +816,12 @@ let find_arguments_scope r = scl' with Not_found -> [] -let declare_ref_arguments_scope ref = - let t = Global.type_of_global_unsafe ref in - let (scs,cls as o) = compute_arguments_scope_full t in +let declare_ref_arguments_scope sigma ref = + let env = Global.env () in (* FIXME? *) + let typ = EConstr.of_constr @@ fst @@ Global.type_of_global_in_context env ref in + let (scs,cls as o) = compute_arguments_scope_full sigma typ in declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o - (********************************) (* Encoding notations as string *) @@ -819,7 +890,7 @@ let pr_scope_classes sc = let pr_notation_info prglob ntn c = str "\"" ++ str ntn ++ str "\" := " ++ - prglob (Notation_ops.glob_constr_of_notation_constr Loc.ghost c) + prglob (Notation_ops.glob_constr_of_notation_constr c) let pr_named_scope prglob scope sc = (if String.equal scope default_scope then @@ -862,8 +933,63 @@ let factorize_entries = function (ntn,[c],[]) l in (ntn,l_of_ntn)::rest +type symbol_token = WhiteSpace of int | String of string + +let split_notation_string str = + let push_token beg i l = + if Int.equal beg i then l else + let s = String.sub str beg (i - beg) in + String s :: l + in + let push_whitespace beg i l = + if Int.equal beg i then l else WhiteSpace (i-beg) :: l + in + let rec loop beg i = + if i < String.length str then + if str.[i] == ' ' then + push_token beg i (loop_on_whitespace (i+1) (i+1)) + else + loop beg (i+1) + else + push_token beg i [] + and loop_on_whitespace beg i = + if i < String.length str then + if str.[i] != ' ' then + push_whitespace beg i (loop i (i+1)) + else + loop_on_whitespace beg (i+1) + else + push_whitespace beg i [] + in + loop 0 0 + +let rec raw_analyze_notation_tokens = function + | [] -> [] + | String ".." :: sl -> NonTerminal Notation_ops.ldots_var :: raw_analyze_notation_tokens sl + | String "_" :: _ -> user_err Pp.(str "_ must be quoted.") + | String x :: sl when Id.is_valid x -> + NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl + | String s :: sl -> + Terminal (String.drop_simple_quotes s) :: raw_analyze_notation_tokens sl + | WhiteSpace n :: sl -> + Break n :: raw_analyze_notation_tokens sl + +let decompose_raw_notation ntn = raw_analyze_notation_tokens (split_notation_string ntn) + +let possible_notations ntn = + (* We collect the possible interpretations of a notation string depending on whether it is + in "x 'U' y" or "_ U _" format *) + let toks = split_notation_string ntn in + if List.exists (function String "_" -> true | _ -> false) toks then + (* Only "_ U _" format *) + [ntn] + else + let ntn' = make_notation_key (raw_analyze_notation_tokens toks) in + if String.equal ntn ntn' then (* Only symbols *) [ntn] else [ntn;ntn'] + let browse_notation strict ntn map = - let find ntn' = + let ntns = possible_notations ntn in + let find ntn' ntn = if String.contains ntn ' ' then String.equal ntn ntn' else let toks = decompose_notation_key ntn' in @@ -876,7 +1002,7 @@ let browse_notation strict ntn map = String.Map.fold (fun scope_name sc -> 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) + if List.exists (find ntn) ntns 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 @@ -887,25 +1013,25 @@ let global_reference_of_notation test (ntn,(sc,c,_)) = Some (ntn,sc,ref) | _ -> None -let error_ambiguous_notation loc _ntn = - user_err_loc (loc,"",str "Ambiguous notation.") +let error_ambiguous_notation ?loc _ntn = + user_err ?loc (str "Ambiguous notation.") -let error_notation_not_reference loc ntn = - user_err_loc (loc,"", - str "Unable to interpret " ++ quote (str ntn) ++ +let error_notation_not_reference ?loc ntn = + user_err ?loc + (str "Unable to interpret " ++ quote (str ntn) ++ str " as a reference.") -let interp_notation_as_global_reference loc test ntn sc = +let interp_notation_as_global_reference ?loc test ntn sc = let scopes = match sc with | Some sc -> - let scope = find_scope (find_delimiters_scope Loc.ghost sc) in + let scope = find_scope (find_delimiters_scope sc) in String.Map.add sc scope String.Map.empty | None -> !scope_map in let ntns = browse_notation true ntn scopes in let refs = List.map (global_reference_of_notation test) ntns in match Option.List.flatten refs with | [_,_,ref] -> ref - | [] -> error_notation_not_reference loc ntn + | [] -> error_notation_not_reference ?loc ntn | refs -> let f (ntn,sc,ref) = let def = find_default ntn !scope_stack in @@ -915,8 +1041,8 @@ let interp_notation_as_global_reference loc test ntn sc = in match List.filter f refs with | [_,_,ref] -> ref - | [] -> error_notation_not_reference loc ntn - | _ -> error_ambiguous_notation loc ntn + | [] -> error_notation_not_reference ?loc ntn + | _ -> error_ambiguous_notation ?loc ntn let locate_notation prglob ntn scope = let ntns = factorize_entries (browse_notation false ntn !scope_map) in @@ -924,19 +1050,18 @@ let locate_notation prglob ntn scope = match ntns with | [] -> str "Unknown notation" | _ -> - t (str "Notation " ++ - tab () ++ str "Scope " ++ tab () ++ fnl () ++ - prlist (fun (ntn,l) -> + str "Notation" ++ fnl () ++ + prlist_with_sep fnl (fun (ntn,l) -> let scope = find_default ntn scopes in prlist (fun (sc,r,(_,df)) -> hov 0 ( - pr_notation_info prglob df r ++ tbrk (1,2) ++ - (if String.equal sc default_scope then mt () else (str ": " ++ str sc)) ++ - tbrk (1,2) ++ - (if Option.equal String.equal (Some sc) scope then str "(default interpretation)" else mt ()) - ++ fnl ())) - l) ntns) + pr_notation_info prglob df r ++ + (if String.equal sc default_scope then mt () + else (spc () ++ str ": " ++ str sc)) ++ + (if Option.equal String.equal (Some sc) scope + then spc () ++ str "(default interpretation)" else mt ()))) + l) ntns let collect_notation_in_scope scope sc known = assert (not (String.equal scope default_scope)); @@ -1001,13 +1126,13 @@ let declare_notation_rule ntn ~extra unpl gram = let find_notation_printing_rule ntn = try pi1 (String.Map.find ntn !notation_rules) - with Not_found -> anomaly (str "No printing rule found for " ++ str ntn) + with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".") let find_notation_extra_printing_rules ntn = 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) + with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".") let get_defined_notations () = String.Set.elements @@ String.Map.domain !notation_rules @@ -1018,8 +1143,8 @@ let add_notation_extra_printing_rule ntn k v = 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.") + user_err ~hdr:"add_notation_extra_printing_rule" + (str "No such Notation.") (**********************************************************************) (* Synchronisation with reset *) |