diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 226 |
1 files changed, 99 insertions, 127 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 5dc1658824..6291a88bb0 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -21,6 +21,7 @@ open Notation_term open Glob_term open Glob_ops open Context.Named.Declaration +open NumTok (*i*) @@ -49,6 +50,11 @@ let notation_entry_level_eq s1 s2 = match (s1,s2) with | InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2 | (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false +let notation_with_optional_scope_eq inscope1 inscope2 = match (inscope1,inscope2) with + | LastLonelyNotation, LastLonelyNotation -> true + | NotationInScope s1, NotationInScope s2 -> String.equal s1 s2 + | (LastLonelyNotation | NotationInScope _), _ -> false + let notation_eq (from1,ntn1) (from2,ntn2) = notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2 @@ -63,6 +69,15 @@ module NotationOrd = module NotationSet = Set.Make(NotationOrd) module NotationMap = CMap.Make(NotationOrd) +module SpecificNotationOrd = + struct + type t = specific_notation + let compare = pervasives_compare + end + +module SpecificNotationSet = Set.Make(SpecificNotationOrd) +module SpecificNotationMap = CMap.Make(SpecificNotationOrd) + (**********************************************************************) (* Scope of symbols *) @@ -148,21 +163,21 @@ let normalize_scope sc = (**********************************************************************) (* The global stack of scopes *) -type scope_elem = Scope of scope_name | SingleNotation of notation -type scopes = scope_elem list +type scope_item = OpenScopeItem of scope_name | LonelyNotationItem of notation +type scopes = scope_item list let scope_eq s1 s2 = match s1, s2 with -| Scope s1, Scope s2 -> String.equal s1 s2 -| SingleNotation s1, SingleNotation s2 -> notation_eq s1 s2 -| Scope _, SingleNotation _ -| SingleNotation _, Scope _ -> false +| OpenScopeItem s1, OpenScopeItem s2 -> String.equal s1 s2 +| LonelyNotationItem s1, LonelyNotationItem s2 -> notation_eq s1 s2 +| OpenScopeItem _, LonelyNotationItem _ +| LonelyNotationItem _, OpenScopeItem _ -> false let scope_stack = ref [] let current_scopes () = !scope_stack let scope_is_open_in_scopes sc l = - List.exists (function Scope sc' -> String.equal sc sc' | _ -> false) l + List.exists (function OpenScopeItem sc' -> String.equal sc sc' | _ -> false) l let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack) @@ -188,7 +203,7 @@ let discharge_scope (_,(local,_,_ as o)) = let classify_scope (local,_,_ as o) = if local then Dispose else Substitute o -let inScope : bool * bool * scope_elem -> obj = +let inScope : bool * bool * scope_item -> obj = declare_object {(default_object "SCOPE") with cache_function = cache_scope; open_function = open_scope; @@ -197,11 +212,11 @@ let inScope : bool * bool * scope_elem -> obj = classify_function = classify_scope } let open_close_scope (local,opening,sc) = - Lib.add_anonymous_leaf (inScope (local,opening,Scope (normalize_scope sc))) + Lib.add_anonymous_leaf (inScope (local,opening,OpenScopeItem (normalize_scope sc))) let empty_scope_stack = [] -let push_scope sc scopes = Scope sc :: scopes +let push_scope sc scopes = OpenScopeItem sc :: scopes let push_scopes = List.fold_right push_scope @@ -254,7 +269,7 @@ let find_delimiters_scope ?loc key = (* Uninterpretation tables *) type interp_rule = - | NotationRule of scope_name option * notation + | NotationRule of specific_notation | SynDefRule of KerName.t (* We define keys for glob_constr and aconstr to split the syntax entries @@ -321,7 +336,7 @@ 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.sign * Constrexpr.raw_numeral +type rawnum = NumTok.Signed.t type prim_token_uid = string @@ -344,17 +359,13 @@ module InnerPrimToken = struct | StringInterp f, StringInterp f' -> f == f' | _ -> false - let ofNumeral s n = - let n = String.(concat "" (split_on_char '_' n)) in - match s with - | SPlus -> Bigint.of_string n - | SMinus -> Bigint.neg (Bigint.of_string n) - let do_interp ?loc interp primtok = match primtok, interp with - | Numeral (s,n), RawNumInterp interp -> interp ?loc (s,n) - | Numeral (s,{ NumTok.int = n; frac = ""; exp = "" }), - BigNumInterp interp -> interp ?loc (ofNumeral s n) + | Numeral n, RawNumInterp interp -> interp ?loc n + | Numeral n, BigNumInterp interp -> + (match NumTok.Signed.to_bigint n with + | Some n -> interp ?loc n + | None -> raise Not_found) | String s, StringInterp interp -> interp ?loc s | (Numeral _ | String _), (RawNumInterp _ | BigNumInterp _ | StringInterp _) -> raise Not_found @@ -371,10 +382,7 @@ module InnerPrimToken = struct | _ -> false let mkNumeral n = - if Bigint.is_pos_or_zero n then - Numeral (SPlus,NumTok.int (Bigint.to_string n)) - else - Numeral (SMinus,NumTok.int (Bigint.to_string (Bigint.neg n))) + Numeral (NumTok.Signed.of_bigint n) let mkString = function | None -> None @@ -411,8 +419,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t type numnot_option = | Nop - | Warning of string - | Abstract of string + | Warning of NumTok.UnsignedNat.t + | Abstract of NumTok.UnsignedNat.t type int_ty = { uint : Names.inductive; @@ -553,7 +561,7 @@ let uninterp to_raw o (Glob_term.AnyGlobConstr n) = Some (to_raw (fst o.of_kind, c)) with | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *) - | NotAValidPrimToken -> None (* all other functions except big2raw *) + | NotAValidPrimToken -> None (* all other functions except NumTok.Signed.of_bigint *) end @@ -586,26 +594,6 @@ let warn_abstract_large_num = 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 *) @@ -620,32 +608,31 @@ let char_of_digit n = assert (2<=n && n<=11); Char.chr (n-2 + Char.code '0') -let coquint_of_rawnum uint str = +let coquint_of_rawnum uint n = let nil = mkConstruct (uint,1) in + match n with None -> nil | Some n -> + let str = NumTok.UnsignedNat.to_string n in let rec do_chars s i acc = if i < 0 then acc - else if s.[i] == '_' then do_chars s (i-1) acc else + 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 sign str = - let uint = coquint_of_rawnum inds.uint str in +let coqint_of_rawnum inds (sign,n) = + let uint = coquint_of_rawnum inds.uint (Some n) in let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in mkApp (mkConstruct (inds.int, pos_neg), [|uint|]) -let coqdecimal_of_rawnum inds sign n = - let i, f, e = NumTok.(n.int, n.frac, n.exp) in - let i = coqint_of_rawnum inds.int sign i in +let coqdecimal_of_rawnum inds n = + let i, f, e = NumTok.Signed.to_decimal_and_exponent n in + let i = coqint_of_rawnum inds.int i in let f = coquint_of_rawnum inds.int.uint f in - if e = "" then mkApp (mkConstruct (inds.decimal, 1), [|i; f|]) (* Decimal *) - else - let sign, e = match e.[1] with - | '-' -> SMinus, String.sub e 2 (String.length e - 2) - | '+' -> SPlus, String.sub e 2 (String.length e - 2) - | _ -> SPlus, String.sub e 1 (String.length e - 1) in - let e = coqint_of_rawnum inds.int sign e in + match e with + | None -> mkApp (mkConstruct (inds.decimal, 1), [|i; f|]) (* Decimal *) + | Some e -> + let e = coqint_of_rawnum inds.int e in mkApp (mkConstruct (inds.decimal, 2), [|i; f; e|]) (* DecimalExp *) let rawnum_of_coquint c = @@ -666,26 +653,23 @@ let rawnum_of_coquint c = (* To avoid ambiguities between Nil and (D0 Nil), we choose to not display Nil alone as "0" *) raise NotAValidPrimToken - else NumTok.int (Buffer.contents buf) + else NumTok.UnsignedNat.of_string (Buffer.contents buf) let rawnum_of_coqint c = match Constr.kind c with | App (c,[|c'|]) -> (match Constr.kind c with - | Construct ((_,1), _) (* Pos *) -> (SPlus, rawnum_of_coquint c') - | Construct ((_,2), _) (* Neg *) -> (SMinus, rawnum_of_coquint c') + | Construct ((_,1), _) (* Pos *) -> (SPlus,rawnum_of_coquint c') + | Construct ((_,2), _) (* Neg *) -> (SMinus,rawnum_of_coquint c') | _ -> raise NotAValidPrimToken) | _ -> raise NotAValidPrimToken let rawnum_of_decimal c = let of_ife i f e = - let sign, n = rawnum_of_coqint i in - let f = - try (rawnum_of_coquint f).NumTok.int with NotAValidPrimToken -> "" in - let e = match e with None -> "" | Some e -> match rawnum_of_coqint e with - | SPlus, e -> "e+" ^ e.NumTok.int - | SMinus, e -> "e-" ^ e.NumTok.int in - sign,{ n with NumTok.frac = f; exp = e } in + let n = rawnum_of_coqint i in + let f = try Some (rawnum_of_coquint f) with NotAValidPrimToken -> None in + let e = match e with None -> None | Some e -> Some (rawnum_of_coqint e) in + NumTok.Signed.of_decimal_and_exponent n f e in match Constr.kind c with | App (_,[|i; f|]) -> of_ife i f None | App (_,[|i; f; e|]) -> of_ife i f (Some e) @@ -775,43 +759,31 @@ let bigint_of_int63 c = | Int i -> Bigint.of_string (Uint63.to_string i) | _ -> raise NotAValidPrimToken -let big2raw n = - if Bigint.is_pos_or_zero n then - (SPlus, NumTok.int (Bigint.to_string n)) - else - (SMinus, NumTok.int (Bigint.to_string (Bigint.neg n))) - -let raw2big s n = match s with - | SPlus -> Bigint.of_string n - | SMinus -> Bigint.neg (Bigint.of_string n) - let interp o ?loc n = begin match o.warning, n with - | Warning threshold, (SPlus, { NumTok.int = n; frac = ""; exp = "" }) - when rawnum_compare n threshold >= 0 -> + | Warning threshold, n when NumTok.Signed.is_bigger_int_than n threshold -> warn_large_num o.ty_name | _ -> () end; - let c = match fst o.to_kind, n with - | Int int_ty, (s, { NumTok.int = n; frac = ""; exp = "" }) -> - coqint_of_rawnum int_ty s n - | UInt uint_ty, (SPlus, { NumTok.int = n; frac = ""; exp = "" }) -> - coquint_of_rawnum uint_ty n - | Z z_pos_ty, (s, { NumTok.int = n; frac = ""; exp = "" }) -> - z_of_bigint z_pos_ty (raw2big s n) - | Int63, (s, { NumTok.int = n; frac = ""; exp = "" }) -> - interp_int63 ?loc (raw2big s n) + let c = match fst o.to_kind, NumTok.Signed.to_int n with + | Int int_ty, Some n -> + coqint_of_rawnum int_ty n + | UInt uint_ty, Some (SPlus, n) -> + coquint_of_rawnum uint_ty (Some n) + | Z z_pos_ty, Some n -> + z_of_bigint z_pos_ty (NumTok.SignedNat.to_bigint n) + | Int63, Some n -> + interp_int63 ?loc (NumTok.SignedNat.to_bigint n) | (Int _ | UInt _ | Z _ | Int63), _ -> no_such_prim_token "number" ?loc o.ty_name - | Decimal decimal_ty, (s,n) -> coqdecimal_of_rawnum decimal_ty s n + | Decimal decimal_ty, _ -> coqdecimal_of_rawnum decimal_ty 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 (snd n).NumTok.int threshold >= 0 -> + | Abstract threshold, Direct when NumTok.Signed.is_bigger_int_than n threshold -> warn_abstract_large_num (o.ty_name,o.to_ty); glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|])) | _ -> @@ -823,10 +795,10 @@ let interp o ?loc n = let uninterp o n = PrimTokenNotation.uninterp begin function - | (Int _, c) -> rawnum_of_coqint c - | (UInt _, c) -> (SPlus, rawnum_of_coquint c) - | (Z _, c) -> big2raw (bigint_of_z c) - | (Int63, c) -> big2raw (bigint_of_int63 c) + | (Int _, c) -> NumTok.Signed.of_int (rawnum_of_coqint c) + | (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c) + | (Z _, c) -> NumTok.Signed.of_bigint (bigint_of_z c) + | (Int63, c) -> NumTok.Signed.of_bigint (bigint_of_int63 c) | (Decimal _, c) -> rawnum_of_decimal c end o n end @@ -1064,17 +1036,17 @@ let check_required_module ?loc sc (sp,d) = the scope stack [scopes], and if yes, using delimiters or not *) let find_with_delimiters = function - | None -> None - | Some scope -> + | LastLonelyNotation -> None + | NotationInScope scope -> match (String.Map.find scope !scope_map).delimiters with | Some key -> Some (Some scope, Some key) | None -> None let rec find_without_delimiters find (ntn_scope,ntn) = function - | Scope scope :: scopes -> + | OpenScopeItem scope :: scopes -> (* Is the expected ntn/numpr attached to the most recently open scope? *) begin match ntn_scope with - | Some scope' when String.equal scope scope' -> + | NotationInScope scope' when String.equal scope scope' -> Some (None,None) | _ -> (* If the most recently open scope has a notation/numeral printer @@ -1084,9 +1056,9 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function else find_without_delimiters find (ntn_scope,ntn) scopes end - | SingleNotation ntn' :: scopes -> + | LonelyNotationItem ntn' :: scopes -> begin match ntn_scope, ntn with - | None, Some ntn when notation_eq ntn ntn' -> + | LastLonelyNotation, Some ntn when notation_eq ntn ntn' -> Some (None, None) | _ -> find_without_delimiters find (ntn_scope,ntn) scopes @@ -1123,7 +1095,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint deprecation = scope_map := String.Map.add scope sc !scope_map end; begin match scopt with - | None -> scope_stack := SingleNotation ntn :: !scope_stack + | None -> scope_stack := LonelyNotationItem ntn :: !scope_stack | Some _ -> () end @@ -1133,23 +1105,23 @@ let declare_uninterpretation rule (metas,c as pat) = let rec find_interpretation ntn find = function | [] -> raise Not_found - | Scope scope :: scopes -> + | OpenScopeItem scope :: scopes -> (try let n = find scope in (n,Some scope) with Not_found -> find_interpretation ntn find scopes) - | SingleNotation ntn'::scopes when notation_eq ntn' ntn -> + | LonelyNotationItem ntn'::scopes when notation_eq ntn' ntn -> (try let n = find default_scope in (n,None) with Not_found -> (* e.g. because single notation only for constr, not cases_pattern *) find_interpretation ntn find scopes) - | SingleNotation _::scopes -> + | LonelyNotationItem _::scopes -> find_interpretation ntn find scopes let find_notation ntn sc = NotationMap.find ntn (find_scope sc).notations let notation_of_prim_token = function - | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.to_string n - | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.to_string n + | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.Unsigned.sprint n + | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.Unsigned.sprint n | String _ -> raise Not_found let find_prim_token check_allowed ?loc p sc = @@ -1244,7 +1216,7 @@ let availability_of_notation (ntn_scope,ntn) scopes = commonly from the lowest level of the source entry to the highest level of the target entry. *) -type entry_coercion = notation list +type entry_coercion = (notation_with_optional_scope * notation) list module EntryCoercionOrd = struct @@ -1295,7 +1267,7 @@ let rec insert_coercion_path path = function 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 declare_entry_coercion (scope,(entry,_) as specific_ntn) entry' = let entry, lev = decompose_custom_entry entry in let entry', lev' = decompose_custom_entry entry' in (* Transitive closure *) @@ -1304,19 +1276,19 @@ let declare_entry_coercion (entry,_ as ntn) entry' = 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) + then ((entry'',entry'),((lev'',lev'),path@[specific_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) + then ((entry,entry'''),((lev,lev'''),path@[specific_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,entry'),((lev,lev'),[specific_ntn]))::toaddright@toaddleft) !entry_coercion_map let entry_has_global_map = ref String.Map.empty @@ -1389,7 +1361,7 @@ let availability_of_prim_token n printer_scope local_scopes = 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) + Option.map snd (find_without_delimiters f (NotationInScope printer_scope,None) scopes) (* Miscellaneous *) @@ -1430,7 +1402,7 @@ let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) (* Mapping classes to scopes *) -open Classops +open Coercionops type scope_class = cl_typ @@ -1705,11 +1677,11 @@ let pr_scopes prglob = let rec find_default ntn = function | [] -> None - | Scope scope :: scopes -> + | OpenScopeItem scope :: scopes -> if NotationMap.mem ntn (find_scope scope).notations then Some scope else find_default ntn scopes - | SingleNotation ntn' :: scopes -> + | LonelyNotationItem ntn' :: scopes -> if notation_eq ntn ntn' then Some default_scope else find_default ntn scopes @@ -1863,13 +1835,13 @@ let collect_notation_in_scope scope sc known = let collect_notations stack = fst (List.fold_left (fun (all,knownntn as acc) -> function - | Scope scope -> + | OpenScopeItem scope -> if String.List.mem_assoc scope all then acc else let (l,knownntn) = collect_notation_in_scope scope (find_scope scope) knownntn in ((scope,l)::all,knownntn) - | SingleNotation ntn -> + | LonelyNotationItem ntn -> if List.mem_f notation_eq ntn knownntn then (all,knownntn) else try @@ -1945,6 +1917,6 @@ let with_notation_protection f x = let fs = freeze ~marshallable:false in try let a = f x in unfreeze fs; a with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = unfreeze fs in - iraise reraise + Exninfo.iraise reraise |