diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 961 |
1 files changed, 732 insertions, 229 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index bb58f00c..e2751865 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -20,7 +20,6 @@ open Constrexpr open Notation_term open Glob_term open Glob_ops -open Ppextend open Context.Named.Declaration (*i*) @@ -40,6 +39,30 @@ open Context.Named.Declaration expression, set this scope to be the current scope *) +let notation_entry_eq s1 s2 = match (s1,s2) with +| InConstrEntry, InConstrEntry -> true +| InCustomEntry s1, InCustomEntry s2 -> String.equal s1 s2 +| (InConstrEntry | InCustomEntry _), _ -> false + +let notation_entry_level_eq s1 s2 = match (s1,s2) with +| InConstrEntrySomeLevel, InConstrEntrySomeLevel -> true +| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2 +| (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false + +let notation_eq (from1,ntn1) (from2,ntn2) = + notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2 + +let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s + +module NotationOrd = + struct + type t = notation + let compare = Pervasives.compare + end + +module NotationSet = Set.Make(NotationOrd) +module NotationMap = CMap.Make(NotationOrd) + (**********************************************************************) (* Scope of symbols *) @@ -52,13 +75,10 @@ type notation_data = { } type scope = { - notations: notation_data String.Map.t; + notations: notation_data NotationMap.t; delimiters: delimiters option } -(* Uninterpreted notation map: notation -> level * DirPath.t *) -let notation_level_map = ref String.Map.empty - (* Scopes table: scope_name -> symbol_interpretation *) let scope_map = ref String.Map.empty @@ -66,7 +86,7 @@ let scope_map = ref String.Map.empty let delimiters_map = ref String.Map.empty let empty_scope = { - notations = String.Map.empty; + notations = NotationMap.empty; delimiters = None } @@ -78,41 +98,6 @@ let init_scope_map () = (**********************************************************************) (* Operations on scopes *) -let parenRelation_eq t1 t2 = match t1, t2 with -| L, L | E, E | Any, Any -> true -| Prec l1, Prec l2 -> Int.equal l1 l2 -| _ -> false - -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 () with Not_found -> @@ -143,12 +128,12 @@ let normalize_scope sc = (**********************************************************************) (* The global stack of scopes *) -type scope_elem = Scope of scope_name | SingleNotation of string +type scope_elem = Scope of scope_name | SingleNotation of notation type scopes = scope_elem list let scope_eq s1 s2 = match s1, s2 with -| Scope s1, Scope s2 -| SingleNotation s1, SingleNotation s2 -> String.equal s1 s2 +| Scope s1, Scope s2 -> String.equal s1 s2 +| SingleNotation s1, SingleNotation s2 -> notation_eq s1 s2 | Scope _, SingleNotation _ | SingleNotation _, Scope _ -> false @@ -200,8 +185,6 @@ let push_scope sc scopes = Scope sc :: scopes let push_scopes = List.fold_right push_scope -type local_scopes = tmp_scope_name option * scope_name list - let make_current_scopes (tmp_scope,scopes) = Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack) @@ -258,7 +241,7 @@ type interp_rule = according to the key of the pattern (adapted from Chet Murthy by HH) *) type key = - | RefKey of global_reference + | RefKey of GlobRef.t | Oth let key_compare k1 k2 = match k1, k2 with @@ -283,16 +266,14 @@ 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 : (string * (any_glob_constr -> prim_token option) * bool) KeyMap.t) - let glob_prim_constr_key c = match DAst.get c with - | GRef (ref, _) -> RefKey (canonical_gr ref) + | GRef (ref, _) -> Some (canonical_gr ref) | GApp (c, _) -> begin match DAst.get c with - | GRef (ref, _) -> RefKey (canonical_gr ref) - | _ -> Oth + | GRef (ref, _) -> Some (canonical_gr ref) + | _ -> None end - | _ -> Oth + | _ -> None let glob_constr_keys c = match DAst.get c with | GApp (c, _) -> @@ -320,77 +301,521 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) (* Interpreting numbers (not in summary because functional objects) *) type required_module = full_path * string list +type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign -type 'a prim_token_interpreter = - ?loc:Loc.t -> 'a -> glob_constr +type prim_token_uid = string -type cases_pattern_status = bool (* true = use prim token in patterns *) +type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr +type 'a prim_token_uninterpreter = any_glob_constr -> 'a option -type 'a prim_token_uninterpreter = - glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status +type 'a prim_token_interpretation = + 'a prim_token_interpreter * 'a prim_token_uninterpreter -type internal_prim_token_interpreter = - ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr) +module InnerPrimToken = struct -let prim_token_interpreter_tab = - (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t) + type interpreter = + | RawNumInterp of (?loc:Loc.t -> rawnum -> glob_constr) + | BigNumInterp of (?loc:Loc.t -> Bigint.bigint -> glob_constr) + | StringInterp of (?loc:Loc.t -> string -> glob_constr) -let add_prim_token_interpreter sc interp = - try - 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 - Hashtbl.add prim_token_interpreter_tab sc (interp cont) + let interp_eq f f' = match f,f' with + | RawNumInterp f, RawNumInterp f' -> f == f' + | BigNumInterp f, BigNumInterp f' -> f == f' + | StringInterp f, StringInterp f' -> f == f' + | _ -> false -let declare_prim_token_interpreter sc interp (patl,uninterp,b) = - declare_scope sc; - add_prim_token_interpreter sc interp; - List.iter (fun pat -> - prim_token_key_table := KeyMap.add - (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table) - patl + let ofNumeral n s = + if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) + + let do_interp ?loc interp primtok = + match primtok, interp with + | Numeral (n,s), RawNumInterp interp -> interp ?loc (n,s) + | Numeral (n,s), BigNumInterp interp -> interp ?loc (ofNumeral n s) + | String s, StringInterp interp -> interp ?loc s + | _ -> raise Not_found + + type uninterpreter = + | RawNumUninterp of (any_glob_constr -> rawnum option) + | BigNumUninterp of (any_glob_constr -> Bigint.bigint option) + | StringUninterp of (any_glob_constr -> string option) + + let uninterp_eq f f' = match f,f' with + | RawNumUninterp f, RawNumUninterp f' -> f == f' + | BigNumUninterp f, BigNumUninterp f' -> f == f' + | StringUninterp f, StringUninterp f' -> f == f' + | _ -> false + + 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 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 mkString = function + | None -> None + | Some s -> if Unicode.is_utf8 s then Some (String s) else None -let ofNumeral n s = + let do_uninterp uninterp g = match uninterp with + | RawNumUninterp u -> Option.map (fun (n,s) -> Numeral (n,s)) (u g) + | BigNumUninterp u -> Option.map mkNumeral (u g) + | StringUninterp u -> mkString (u g) + +end + +(* The following two tables of (un)interpreters will *not* be + synchronized. But their indexes will be checked to be unique. + These tables contain primitive token interpreters which are + registered in plugins, such as string and ascii syntax. It is + essential that only plugins add to these tables, and that + vernacular commands do not. See + https://github.com/coq/coq/issues/8401 for details of what goes + wrong when vernacular commands add to these tables. *) +let prim_token_interpreters = + (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.interpreter) Hashtbl.t) + +let prim_token_uninterpreters = + (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t) + +(*******************************************************) +(* Numeral notation interpretation *) +type numeral_notation_error = + | UnexpectedTerm of Constr.t + | UnexpectedNonOptionTerm of Constr.t + +exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error + +type numnot_option = + | Nop + | Warning of raw_natural_number + | Abstract of raw_natural_number + +type int_ty = + { uint : Names.inductive; + int : Names.inductive } + +type z_pos_ty = + { z_ty : Names.inductive; + pos_ty : Names.inductive } + +type target_kind = + | Int of int_ty (* Coq.Init.Decimal.int + uint *) + | UInt of Names.inductive (* Coq.Init.Decimal.uint *) + | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) + +type option_kind = Option | Direct +type conversion_kind = target_kind * option_kind + +type numeral_notation_obj = + { to_kind : conversion_kind; + to_ty : GlobRef.t; + of_kind : conversion_kind; + of_ty : GlobRef.t; + num_ty : Libnames.qualid; (* for warnings / error messages *) + warning : numnot_option } + +module Numeral = struct +(** * Numeral notation *) + +(** Reduction + + The constr [c] below isn't necessarily well-typed, since we + built it via an [mkApp] of a conversion function on a term + that starts with the right constructor but might be partially + applied. + + At least [c] is known to be evar-free, since it comes from + our own ad-hoc [constr_of_glob] or from conversions such + as [coqint_of_rawnum]. +*) + +let eval_constr env sigma (c : Constr.t) = + let c = EConstr.of_constr c in + let sigma,t = Typing.type_of env sigma c in + let c' = Vnorm.cbv_vm env sigma c t in + EConstr.Unsafe.to_constr c' + +(* For testing with "compute" instead of "vm_compute" : +let eval_constr env sigma (c : Constr.t) = + let c = EConstr.of_constr c in + let c' = Tacred.compute env sigma c in + EConstr.Unsafe.to_constr c' +*) + +let eval_constr_app env sigma c1 c2 = + eval_constr env sigma (mkApp (c1,[| c2 |])) + +exception NotANumber + +let warn_large_num = + CWarnings.create ~name:"large-number" ~category:"numbers" + (fun ty -> + strbrk "Stack overflow or segmentation fault happens when " ++ + strbrk "working with large numbers in " ++ pr_qualid ty ++ + strbrk " (threshold may vary depending" ++ + strbrk " on your system limits and on the command executed).") + +let warn_abstract_large_num = + CWarnings.create ~name:"abstract-large-number" ~category:"numbers" + (fun (ty,f) -> + strbrk "To avoid stack overflow, large numbers in " ++ + pr_qualid ty ++ strbrk " are interpreted as applications of " ++ + Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".") + +(** Comparing two raw numbers (base 10, big-endian, non-negative). + A bit nasty, but not critical: only used to decide when a + number is considered as large (see warnings above). *) + +exception Comp of int + +let rec rawnum_compare s s' = + let l = String.length s and l' = String.length s' in + if l < l' then - rawnum_compare s' s + else + let d = l-l' in + try + for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done; + for i = d to l-1 do + let c = Pervasives.compare s.[i] s'.[i-d] in + if c != 0 then raise (Comp c) + done; + 0 + with Comp c -> c + +(***********************************************************************) + +(** ** Conversion between Coq [Decimal.int] and internal raw string *) + +(** Decimal.Nil has index 1, then Decimal.D0 has index 2 .. Decimal.D9 is 11 *) + +let digit_of_char c = + assert ('0' <= c && c <= '9'); + Char.code c - Char.code '0' + 2 + +let char_of_digit n = + assert (2<=n && n<=11); + Char.chr (n-2 + Char.code '0') + +let coquint_of_rawnum uint str = + let nil = mkConstruct (uint,1) in + let rec do_chars s i acc = + if i < 0 then acc + else + let dg = mkConstruct (uint, digit_of_char s.[i]) in + do_chars s (i-1) (mkApp(dg,[|acc|])) + in + do_chars str (String.length str - 1) nil + +let coqint_of_rawnum inds (str,sign) = + let uint = coquint_of_rawnum inds.uint str in + mkApp (mkConstruct (inds.int, if sign then 1 else 2), [|uint|]) + +let rawnum_of_coquint c = + let rec of_uint_loop c buf = + match Constr.kind c with + | Construct ((_,1), _) (* Nil *) -> () + | App (c, [|a|]) -> + (match Constr.kind c with + | Construct ((_,n), _) (* D0 to D9 *) -> + let () = Buffer.add_char buf (char_of_digit n) in + of_uint_loop a buf + | _ -> raise NotANumber) + | _ -> raise NotANumber + in + let buf = Buffer.create 64 in + let () = of_uint_loop c buf in + if Int.equal (Buffer.length buf) 0 then + (* To avoid ambiguities between Nil and (D0 Nil), we choose + to not display Nil alone as "0" *) + raise NotANumber + else Buffer.contents buf + +let rawnum_of_coqint c = + match Constr.kind c with + | App (c,[|c'|]) -> + (match Constr.kind c with + | Construct ((_,1), _) (* Pos *) -> (rawnum_of_coquint c', true) + | Construct ((_,2), _) (* Neg *) -> (rawnum_of_coquint c', false) + | _ -> raise NotANumber) + | _ -> raise NotANumber + + +(***********************************************************************) + +(** ** Conversion between Coq [Z] and internal bigint *) + +(** First, [positive] from/to bigint *) + +let rec pos_of_bigint posty n = + match Bigint.div2_with_rest n with + | (q, false) -> + let c = mkConstruct (posty, 2) in (* xO *) + mkApp (c, [| pos_of_bigint posty q |]) + | (q, true) when not (Bigint.equal q Bigint.zero) -> + let c = mkConstruct (posty, 1) in (* xI *) + mkApp (c, [| pos_of_bigint posty q |]) + | (q, true) -> + mkConstruct (posty, 3) (* xH *) + +let rec bigint_of_pos c = match Constr.kind c with + | Construct ((_, 3), _) -> (* xH *) Bigint.one + | App (c, [| d |]) -> + begin match Constr.kind c with + | Construct ((_, n), _) -> + begin match n with + | 1 -> (* xI *) Bigint.add_1 (Bigint.mult_2 (bigint_of_pos d)) + | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d) + | n -> assert false (* no other constructor of type positive *) + end + | x -> raise NotANumber + end + | x -> raise NotANumber + +(** Now, [Z] from/to bigint *) + +let z_of_bigint { z_ty; pos_ty } n = + if Bigint.equal n Bigint.zero then + mkConstruct (z_ty, 1) (* Z0 *) + else + let (s, n) = + if Bigint.is_pos_or_zero n then (2, n) (* Zpos *) + else (3, Bigint.neg n) (* Zneg *) + in + let c = mkConstruct (z_ty, s) in + mkApp (c, [| pos_of_bigint pos_ty n |]) + +let bigint_of_z z = match Constr.kind z with + | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero + | App (c, [| d |]) -> + begin match Constr.kind c with + | Construct ((_, n), _) -> + begin match n with + | 2 -> (* Zpos *) bigint_of_pos d + | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d) + | n -> assert false (* no other constructor of type Z *) + end + | _ -> raise NotANumber + end + | _ -> raise NotANumber + +(** The uninterp function below work at the level of [glob_constr] + which is too low for us here. So here's a crude conversion back + to [constr] for the subset that concerns us. *) + +let rec constr_of_glob env sigma g = match DAst.get g with + | Glob_term.GRef (ConstructRef c, _) -> + let sigma,c = Evd.fresh_constructor_instance env sigma c in + sigma,mkConstructU c + | Glob_term.GApp (gc, gcl) -> + let sigma,c = constr_of_glob env sigma gc in + let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in + sigma,mkApp (c, Array.of_list cl) + | _ -> + raise NotANumber + +let rec glob_of_constr ?loc env sigma c = match Constr.kind c with + | App (c, ca) -> + let c = glob_of_constr ?loc env sigma c in + let cel = List.map (glob_of_constr ?loc env sigma) (Array.to_list ca) in + DAst.make ?loc (Glob_term.GApp (c, cel)) + | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None)) + | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None)) + | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None)) + | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None)) + | _ -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedTerm c)) + +let no_such_number ?loc ty = + CErrors.user_err ?loc + (str "Cannot interpret this number as a value of type " ++ + pr_qualid ty) + +let interp_option ty ?loc env sigma c = + match Constr.kind c with + | App (_Some, [| _; c |]) -> glob_of_constr ?loc env sigma c + | App (_None, [| _ |]) -> no_such_number ?loc ty + | x -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedNonOptionTerm c)) + +let uninterp_option c = + match Constr.kind c with + | App (_Some, [| _; x |]) -> x + | _ -> raise NotANumber + +let big2raw n = + if Bigint.is_pos_or_zero n then (Bigint.to_string n, true) + else (Bigint.to_string (Bigint.neg n), false) + +let raw2big (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 interp o ?loc n = + begin match o.warning with + | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 -> + warn_large_num o.num_ty + | _ -> () + end; + let c = match fst o.to_kind with + | Int int_ty -> coqint_of_rawnum int_ty n + | UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst n) + | UInt _ (* n <= 0 *) -> no_such_number ?loc o.num_ty + | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n) + in + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in + let to_ty = EConstr.Unsafe.to_constr to_ty in + match o.warning, snd o.to_kind with + | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 -> + warn_abstract_large_num (o.num_ty,o.to_ty); + glob_of_constr ?loc env sigma (mkApp (to_ty,[|c|])) + | _ -> + let res = eval_constr_app env sigma to_ty c in + match snd o.to_kind with + | Direct -> glob_of_constr ?loc env sigma res + | Option -> interp_option o.num_ty ?loc env sigma res + +let uninterp o (Glob_term.AnyGlobConstr n) = + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in + let of_ty = EConstr.Unsafe.to_constr of_ty in + try + let sigma,n = constr_of_glob env sigma n in + let c = eval_constr_app env sigma of_ty n in + let c = if snd o.of_kind == Direct then c else uninterp_option c in + match fst o.of_kind with + | Int _ -> Some (rawnum_of_coqint c) + | UInt _ -> Some (rawnum_of_coquint c, true) + | Z _ -> Some (big2raw (bigint_of_z c)) + with + | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *) + | NotANumber -> None (* all other functions except big2raw *) +end + +(* A [prim_token_infos], which is synchronized with the document + state, either contains a unique id pointing to an unsynchronized + prim token function, or a numeral notation object describing how to + interpret and uninterpret. We provide [prim_token_infos] because + we expect plugins to provide their own interpretation functions, + rather than going through numeral notations, which are available as + a vernacular. *) + +type prim_token_interp_info = + Uid of prim_token_uid + | NumeralNotation of numeral_notation_obj + +type prim_token_infos = { + pt_local : bool; (** Is this interpretation local? *) + pt_scope : scope_name; (** Concerned scope *) + pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *) + pt_required : required_module; (** Module that should be loaded first *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) + pt_in_match : bool (** Is this prim token legal in match patterns ? *) +} -let delay dir int ?loc x = (dir, (fun () -> int ?loc x)) +(* Table from scope_name to backtrack-able informations about interpreters + (in particular interpreter unique id). *) +let prim_token_interp_infos = + ref (String.Map.empty : (required_module * prim_token_interp_info) String.Map.t) + +(* Table from global_reference to backtrack-able informations about + prim_token uninterpretation (in particular uninterpreter unique id). *) +let prim_token_uninterp_infos = + ref (Refmap.empty : (scope_name * prim_token_interp_info * bool) Refmap.t) + +let hashtbl_check_and_set allow_overwrite uid f h eq = + match Hashtbl.find h uid with + | exception Not_found -> Hashtbl.add h uid f + | _ when allow_overwrite -> Hashtbl.add h uid f + | g when eq f g -> () + | _ -> + user_err ~hdr:"prim_token_interpreter" + (str "Unique identifier " ++ str uid ++ + str " already used to register a numeral or string (un)interpreter.") + +let register_gen_interpretation allow_overwrite uid (interp, uninterp) = + hashtbl_check_and_set + allow_overwrite uid interp prim_token_interpreters InnerPrimToken.interp_eq; + hashtbl_check_and_set + allow_overwrite uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq + +let register_rawnumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid + (InnerPrimToken.RawNumInterp interp, InnerPrimToken.RawNumUninterp uninterp) + +let register_bignumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid + (InnerPrimToken.BigNumInterp interp, InnerPrimToken.BigNumUninterp uninterp) + +let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid + (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp) + +let cache_prim_token_interpretation (_,infos) = + let ptii = infos.pt_interp_info in + let sc = infos.pt_scope in + declare_scope sc; + prim_token_interp_infos := + String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos; + List.iter (fun r -> prim_token_uninterp_infos := + Refmap.add r (sc,ptii,infos.pt_in_match) + !prim_token_uninterp_infos) + infos.pt_refs + +let subst_prim_token_interpretation (subs,infos) = + { infos with + pt_refs = List.map (subst_global_reference subs) infos.pt_refs } + +let classify_prim_token_interpretation infos = + if infos.pt_local then Dispose else Substitute infos + +let inPrimTokenInterp : prim_token_infos -> obj = + declare_object {(default_object "PRIM-TOKEN-INTERP") with + open_function = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o); + cache_function = cache_prim_token_interpretation; + subst_function = subst_prim_token_interpretation; + classify_function = classify_prim_token_interpretation} + +let enable_prim_token_interpretation infos = + Lib.add_anonymous_leaf (inPrimTokenInterp infos) + +(** Compatibility. + Avoid the next two functions, they will now store unnecessary + objects in the library segment. Instead, combine + [register_*_interpretation] and [enable_prim_token_interpretation] + (the latter inside a [Mltop.declare_cache_obj]). +*) -type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign +let fresh_string_of = + let count = ref 0 in + fun root -> count := !count+1; (string_of_int !count)^"_"^root + +let declare_numeral_interpreter ?(local=false) sc dir interp (patl,uninterp,b) = + let uid = fresh_string_of sc in + register_bignumeral_interpretation uid (interp,uninterp); + enable_prim_token_interpretation + { pt_local = local; + pt_scope = sc; + pt_interp_info = Uid uid; + pt_required = dir; + pt_refs = List.map_filter glob_prim_constr_key patl; + pt_in_match = b } +let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) = + let uid = fresh_string_of sc in + register_string_interpretation uid (interp,uninterp); + enable_prim_token_interpretation + { pt_local = local; + pt_scope = sc; + pt_interp_info = Uid uid; + pt_required = dir; + pt_refs = List.map_filter glob_prim_constr_key patl; + pt_in_match = b } -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,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) - (patl, (fun r -> mkString (uninterp r)), inpat) let check_required_module ?loc sc (sp,d) = try let _ = Nametab.global_of_path sp in () with Not_found -> - user_err ?loc ~hdr:"prim_token_interpreter" - (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") + match d with + | [] -> user_err ?loc ~hdr:"prim_token_interpreter" + (str "Cannot interpret in " ++ str sc ++ str " because " ++ pr_path sp ++ str " could not be found in the current environment.") + | _ -> 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 *) @@ -418,7 +843,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function end | SingleNotation ntn' :: scopes -> begin match ntn_scope, ntn with - | None, Some ntn when String.equal ntn ntn' -> + | None, Some ntn when notation_eq ntn ntn' -> Some (None, None) | _ -> find_without_delimiters find (ntn_scope,ntn) scopes @@ -427,24 +852,12 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function (* Can we switch to [scope]? Yes if it has defined delimiters *) find_with_delimiters ntn_scope -(* Uninterpreted notation levels *) - -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,onlyprint) !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 *) let warn_notation_overridden = CWarnings.create ~name:"notation-overridden" ~category:"parsing" (fun (ntn,which_scope) -> - str "Notation" ++ spc () ++ str ntn ++ spc () + str "Notation" ++ spc () ++ pr_notation ntn ++ spc () ++ strbrk "was already used" ++ which_scope ++ str ".") let declare_notation_interpretation ntn scopt pat df ~onlyprint = @@ -452,7 +865,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint = let sc = find_scope scope in if not onlyprint then begin let () = - if String.Map.mem ntn sc.notations then + if NotationMap.mem ntn sc.notations then let which_scope = match scopt with | None -> mt () | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in @@ -462,7 +875,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint = not_interp = pat; not_location = df; } in - let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in + let sc = { sc with notations = NotationMap.add ntn notdata sc.notations } in scope_map := String.Map.add scope sc !scope_map end; begin match scopt with @@ -479,7 +892,7 @@ let rec find_interpretation ntn find = function | Scope scope :: scopes -> (try let (pat,df) = find scope in pat,(df,Some scope) with Not_found -> find_interpretation ntn find scopes) - | SingleNotation ntn'::scopes when String.equal ntn' ntn -> + | SingleNotation ntn'::scopes when notation_eq ntn' ntn -> (try let (pat,df) = find default_scope in pat,(df,None) with Not_found -> (* e.g. because single notation only for constr, not cases_pattern *) @@ -488,12 +901,12 @@ let rec find_interpretation ntn find = function find_interpretation ntn find scopes let find_notation ntn sc = - let n = String.Map.find ntn (find_scope sc).notations in + let n = NotationMap.find ntn (find_scope sc).notations in (n.not_interp, n.not_location) let notation_of_prim_token = function - | Numeral (n,true) -> n - | Numeral (n,false) -> "- "^n + | Numeral (n,true) -> InConstrEntrySomeLevel, n + | Numeral (n,false) -> InConstrEntrySomeLevel, "- "^n | String _ -> raise Not_found let find_prim_token check_allowed ?loc p sc = @@ -505,21 +918,25 @@ let find_prim_token check_allowed ?loc p sc = pat, df with Not_found -> (* Try for a primitive numerical notation *) - let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc ?loc p in + let (spdir,info) = String.Map.find sc !prim_token_interp_infos in check_required_module ?loc sc spdir; - let pat = interp () in + let interp = match info with + | Uid uid -> Hashtbl.find prim_token_interpreters uid + | NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o) + in + let pat = InnerPrimToken.do_interp ?loc interp p in check_allowed pat; pat, ((dirpath (fst spdir),DirPath.empty),"") 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 + let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntrySomeLevel,"" in try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes with Not_found -> user_err ?loc ~hdr:"interp_prim_token" ((match p with | Numeral _ -> - str "No interpretation for numeral " ++ str (notation_of_prim_token p) + str "No interpretation for numeral " ++ pr_notation (notation_of_prim_token p) | String s -> str "No interpretation for string " ++ qs s) ++ str ".") let interp_prim_token ?loc = @@ -544,7 +961,7 @@ let interp_notation ?loc ntn local_scopes = try find_interpretation ntn (find_notation ntn) scopes with Not_found -> user_err ?loc - (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") + (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".") let uninterp_notations c = List.map_append (fun key -> keymap_find key !notations_key_table) @@ -558,47 +975,161 @@ let uninterp_ind_pattern_notations ind = let availability_of_notation (ntn_scope,ntn) scopes = let f scope = - String.Map.mem ntn (String.Map.find scope !scope_map).notations in + NotationMap.mem ntn (String.Map.find scope !scope_map).notations in find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes) -let uninterp_prim_token c = +(* We support coercions from a custom entry at some level to an entry + at some level (possibly the same), and from and to the constr entry. E.g.: + + Notation "[ expr ]" := expr (expr custom group at level 1). + Notation "( x )" := x (in custom group at level 0, x at level 1). + Notation "{ x }" := x (in custom group at level 0, x constr). + + Supporting any level is maybe overkill in that coercions are + commonly from the lowest level of the source entry to the highest + level of the target entry. *) + +type entry_coercion = notation list + +module EntryCoercionOrd = + struct + type t = notation_entry * notation_entry + let compare = Pervasives.compare + end + +module EntryCoercionMap = Map.Make(EntryCoercionOrd) + +let entry_coercion_map = ref EntryCoercionMap.empty + +let level_ord lev lev' = + match lev, lev' with + | None, _ -> true + | _, None -> true + | Some n, Some n' -> n <= n' + +let rec search nfrom nto = function + | [] -> raise Not_found + | ((pfrom,pto),coe)::l -> + if level_ord pfrom nfrom && level_ord nto pto then coe else search nfrom nto l + +let decompose_custom_entry = function + | InConstrEntrySomeLevel -> InConstrEntry, None + | InCustomEntryLevel (s,n) -> InCustomEntry s, Some n + +let availability_of_entry_coercion entry entry' = + let entry, lev = decompose_custom_entry entry in + let entry', lev' = decompose_custom_entry entry' in + if notation_entry_eq entry entry' && level_ord lev' lev then Some [] + else + try Some (search lev lev' (EntryCoercionMap.find (entry,entry') !entry_coercion_map)) + with Not_found -> None + +let better_path ((lev1,lev2),path) ((lev1',lev2'),path') = + (* better = shorter and lower source and higher target *) + level_ord lev1 lev1' && level_ord lev2' lev2 && List.length path <= List.length path' + +let shorter_path (_,path) (_,path') = + List.length path <= List.length path' + +let rec insert_coercion_path path = function + | [] -> [path] + | path'::paths as allpaths -> + (* If better or equal we keep the more recent one *) + if better_path path path' then path::paths + else if better_path path' path then allpaths + else if shorter_path path path' then path::allpaths + else path'::insert_coercion_path path paths + +let declare_entry_coercion (entry,_ as ntn) entry' = + let entry, lev = decompose_custom_entry entry in + let entry', lev' = decompose_custom_entry entry' in + (* Transitive closure *) + let toaddleft = + EntryCoercionMap.fold (fun (entry'',entry''') paths l -> + List.fold_right (fun ((lev'',lev'''),path) l -> + if notation_entry_eq entry entry''' && level_ord lev lev''' && + not (notation_entry_eq entry' entry'') + then ((entry'',entry'),((lev'',lev'),path@[ntn]))::l else l) paths l) + !entry_coercion_map [] in + let toaddright = + EntryCoercionMap.fold (fun (entry'',entry''') paths l -> + List.fold_right (fun ((lev'',lev'''),path) l -> + if entry' = entry'' && level_ord lev' lev'' && entry <> entry''' + then ((entry,entry'''),((lev,lev'''),path@[ntn]))::l else l) paths l) + !entry_coercion_map [] in + entry_coercion_map := + List.fold_right (fun (pair,path) -> + let olds = try EntryCoercionMap.find pair !entry_coercion_map with Not_found -> [] in + EntryCoercionMap.add pair (insert_coercion_path path olds)) + (((entry,entry'),((lev,lev'),[ntn]))::toaddright@toaddleft) + !entry_coercion_map + +let entry_has_global_map = ref String.Map.empty + +let declare_custom_entry_has_global s n = try - let (sc,numpr,_) = - KeyMap.find (glob_prim_constr_key c) !prim_token_key_table in - match numpr (AnyGlobConstr c) with - | None -> raise Notation_ops.No_match - | Some n -> (sc,n) - with Not_found -> raise Notation_ops.No_match - -let uninterp_prim_token_ind_pattern ind args = - let ref = IndRef ind in + let p = String.Map.find s !entry_has_global_map in + user_err (str "Custom entry " ++ str s ++ + str " has already a rule for global references at level " ++ int p ++ str ".") + with Not_found -> + entry_has_global_map := String.Map.add s n !entry_has_global_map + +let entry_has_global = function + | InConstrEntrySomeLevel -> true + | InCustomEntryLevel (s,n) -> + try String.Map.find s !entry_has_global_map <= n with Not_found -> false + +let entry_has_ident_map = ref String.Map.empty + +let declare_custom_entry_has_ident s n = try - let k = RefKey (canonical_gr ref) in - let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in - 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 = 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 + let p = String.Map.find s !entry_has_ident_map in + user_err (str "Custom entry " ++ str s ++ + str " has already a rule for global references at level " ++ int p ++ str ".") + with Not_found -> + entry_has_ident_map := String.Map.add s n !entry_has_ident_map + +let entry_has_ident = function + | InConstrEntrySomeLevel -> true + | InCustomEntryLevel (s,n) -> + try String.Map.find s !entry_has_ident_map <= n with Not_found -> false + +let uninterp_prim_token c = + match glob_prim_constr_key c with + | None -> raise Notation_ops.No_match + | Some r -> + try + let (sc,info,_) = Refmap.find r !prim_token_uninterp_infos in + let uninterp = match info with + | Uid uid -> Hashtbl.find prim_token_uninterpreters uid + | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o) + in + match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with + | None -> raise Notation_ops.No_match + | Some n -> (sc,n) + with Not_found -> raise Notation_ops.No_match let uninterp_prim_token_cases_pattern c = - try - let k = cases_pattern_key c in - 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 (AnyGlobConstr c) with - | None -> raise Notation_ops.No_match - | Some n -> (na,sc,n) - with Not_found -> raise Notation_ops.No_match + match glob_constr_of_closed_cases_pattern c with + | exception Not_found -> raise Notation_ops.No_match + | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n) let availability_of_prim_token n printer_scope local_scopes = let f scope = - try ignore ((Hashtbl.find prim_token_interpreter_tab scope) n); true - with Not_found -> false in + try + let uid = snd (String.Map.find scope !prim_token_interp_infos) in + let open InnerPrimToken in + match n, uid with + | Numeral _, NumeralNotation _ -> true + | _, NumeralNotation _ -> false + | _, Uid uid -> + let interp = Hashtbl.find prim_token_interpreters uid in + match n, interp with + | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true + | String _, StringInterp _ -> true + | _ -> false + 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) @@ -619,7 +1150,8 @@ let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeBinderList, NtnTypeBinderList -> true | (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false -let var_attributes_eq (_, (sc1, tp1)) (_, (sc2, tp2)) = +let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) = + notation_entry_level_eq entry1 entry2 && pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && ntpe_eq tp1 tp2 @@ -631,7 +1163,7 @@ 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 - let n = String.Map.find ntn sc.notations in + let n = NotationMap.find ntn sc.notations in interpretation_eq n.not_interp r with Not_found -> false @@ -741,7 +1273,7 @@ let subst_arguments_scope (subst,(req,r,n,scl,cls)) = match subst_scope_class subst cl with | Some cl' as ocl' when cl' != cl -> ocl' | _ -> ocl in - let cls' = List.smartmap subst_cl cls in + let cls' = List.Smart.map subst_cl cls in (ArgsScopeNoDischarge,r',n,scl,cls') let discharge_arguments_scope (_,(req,r,n,l,_)) = @@ -778,7 +1310,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) = (req,r,0,l1@l,cls1) type arguments_scope_obj = - arguments_scope_discharge_request * global_reference * + arguments_scope_discharge_request * GlobRef.t * (* Used to communicate information from discharge to rebuild *) (* set to 0 otherwise *) int * scope_name option list * scope_class option list @@ -847,10 +1379,10 @@ let rec string_of_symbol = function let l = List.flatten (List.map string_of_symbol l) in "_"::l@".."::l@["_"] | Break _ -> [] -let make_notation_key symbols = - String.concat " " (List.flatten (List.map string_of_symbol symbols)) +let make_notation_key from symbols = + (from,String.concat " " (List.flatten (List.map string_of_symbol symbols))) -let decompose_notation_key s = +let decompose_notation_key (from,s) = let len = String.length s in let rec decomp_ntn dirs n = if n>=len then List.rev dirs else @@ -865,7 +1397,7 @@ let decompose_notation_key s = | s -> Terminal (String.drop_simple_quotes s) in decomp_ntn (tok::dirs) (pos+1) in - decomp_ntn [] 0 + from, decomp_ntn [] 0 (************) (* Printing *) @@ -894,14 +1426,14 @@ let pr_notation_info prglob ntn c = let pr_named_scope prglob scope sc = (if String.equal scope default_scope then - match String.Map.cardinal sc.notations with + match NotationMap.cardinal sc.notations with | 0 -> str "No lonely notation" | n -> str "Lonely notation" ++ (if Int.equal n 1 then mt() else str"s") else str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters) ++ fnl () ++ pr_scope_classes scope - ++ String.Map.fold + ++ NotationMap.fold (fun ntn { not_interp = (_, r); not_location = (_, df) } strm -> pr_notation_info prglob df r ++ fnl () ++ strm) sc.notations (mt ()) @@ -916,11 +1448,11 @@ let pr_scopes prglob = let rec find_default ntn = function | [] -> None | Scope scope :: scopes -> - if String.Map.mem ntn (find_scope scope).notations then + if NotationMap.mem ntn (find_scope scope).notations then Some scope else find_default ntn scopes | SingleNotation ntn' :: scopes -> - if String.equal ntn ntn' then Some default_scope + if notation_eq ntn ntn' then Some default_scope else find_default ntn scopes let factorize_entries = function @@ -929,7 +1461,7 @@ let factorize_entries = function let (ntn,l_of_ntn,rest) = List.fold_left (fun (a',l,rest) (a,c) -> - if String.equal a a' then (a',c::l,rest) else (a,[c],(a',l)::rest)) + if notation_eq a a' then (a',c::l,rest) else (a,[c],(a',l)::rest)) (ntn,[c],[]) l in (ntn,l_of_ntn)::rest @@ -984,15 +1516,15 @@ let possible_notations ntn = (* Only "_ U _" format *) [ntn] else - let ntn' = make_notation_key (raw_analyze_notation_tokens toks) in + let _,ntn' = make_notation_key None (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 ntns = possible_notations ntn in - let find ntn' ntn = + let find (from,ntn' as fullntn') ntn = if String.contains ntn ' ' then String.equal ntn ntn' else - let toks = decompose_notation_key ntn' in + let _,toks = decompose_notation_key fullntn' in let get_terminals = function Terminal ntn -> Some ntn | _ -> None in let trms = List.map_filter get_terminals toks in if strict then String.List.equal [ntn] trms @@ -1001,10 +1533,10 @@ let browse_notation strict ntn map = let l = String.Map.fold (fun scope_name sc -> - String.Map.fold (fun ntn { not_interp = (_, r); not_location = df } l -> + NotationMap.fold (fun ntn { not_interp = (_, r); not_location = df } l -> 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 + List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l let global_reference_of_notation test (ntn,(sc,c,_)) = match c with @@ -1065,9 +1597,9 @@ let locate_notation prglob ntn scope = let collect_notation_in_scope scope sc known = assert (not (String.equal scope default_scope)); - String.Map.fold + NotationMap.fold (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)) + if List.mem_f notation_eq ntn known then acc else ((df,r)::l,ntn::known)) sc.notations ([],known) let collect_notations stack = @@ -1080,10 +1612,10 @@ let collect_notations stack = collect_notation_in_scope scope (find_scope scope) knownntn in ((scope,l)::all,knownntn) | SingleNotation ntn -> - if String.List.mem ntn knownntn then (all,knownntn) + if List.mem_f notation_eq ntn knownntn then (all,knownntn) else let { not_interp = (_, r); not_location = (_, df) } = - String.Map.find ntn (find_scope default_scope).notations in + NotationMap.find ntn (find_scope default_scope).notations in let all' = match all with | (s,lonelyntn)::rest when String.equal s default_scope -> (s,(df,r)::lonelyntn)::rest @@ -1113,64 +1645,35 @@ let pr_visibility prglob = function | None -> pr_scope_stack prglob !scope_stack (**********************************************************************) -(* Mapping notations to concrete syntax *) - -type unparsing_rule = unparsing list * precedence -type extra_unparsing_rules = (string * string) list -(* Concrete syntax for symbolic-extension table *) -let notation_rules = - ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t) - -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 pi1 (String.Map.find ntn !notation_rules) - 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 ++ str ".") - -let get_defined_notations () = - String.Set.elements @@ String.Map.domain !notation_rules - -let add_notation_extra_printing_rule ntn k v = - try - 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 ~hdr:"add_notation_extra_printing_rule" - (str "No such Notation.") - -(**********************************************************************) (* Synchronisation with reset *) let freeze _ = - (!scope_map, !notation_level_map, !scope_stack, !arguments_scope, - !delimiters_map, !notations_key_table, !notation_rules, - !scope_class_map) + (!scope_map, !scope_stack, !arguments_scope, + !delimiters_map, !notations_key_table, !scope_class_map, + !prim_token_interp_infos, !prim_token_uninterp_infos, + !entry_coercion_map, !entry_has_global_map, + !entry_has_ident_map) -let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) = +let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = scope_map := scm; - notation_level_map := nlm; scope_stack := scs; delimiters_map := dlm; arguments_scope := asc; notations_key_table := fkm; - notation_rules := pprules; - scope_class_map := clsc + scope_class_map := clsc; + prim_token_interp_infos := ptii; + prim_token_uninterp_infos := ptui; + entry_coercion_map := coe; + entry_has_global_map := globs; + entry_has_ident_map := ids let init () = init_scope_map (); - notation_level_map := String.Map.empty; delimiters_map := String.Map.empty; notations_key_table := KeyMap.empty; - notation_rules := String.Map.empty; - scope_class_map := initial_scope_class_map + scope_class_map := initial_scope_class_map; + prim_token_interp_infos := String.Map.empty; + prim_token_uninterp_infos := Refmap.empty let _ = Summary.declare_summary "symbols" |