From 64cb952f3fcf41c25a66a92bd124bba82e6db3f6 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 14 Mar 2018 10:23:51 +0100 Subject: Notation: no more chains of prim_token_interpreter This cleanup prepares for forthcoming synchronization of prim_token_interpreter wrt to Summary. These chains of prim_token_interpreter were anyway never used, only one interpreter was declared per numeral scope. After sync wrt Summary, we'll anyway be able to backtrack to a previous interpreter. --- interp/notation.ml | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) diff --git a/interp/notation.ml b/interp/notation.ml index 625d072b9f..36d4b0aa15 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -319,12 +319,7 @@ let prim_token_interpreter_tab = (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t) 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) + Hashtbl.replace prim_token_interpreter_tab sc interp let declare_prim_token_interpreter sc interp (patl,uninterp,b) = declare_scope sc; @@ -351,8 +346,8 @@ 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) + (fun ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s) + | _ -> raise Not_found) (patl, (fun r -> match uninterp r with | None -> None | Some (n,s) -> Some (Numeral (n,s))), inpat) @@ -360,13 +355,14 @@ let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,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) + (fun ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s) + | _ -> raise Not_found) (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 ?loc -> function String s -> delay dir interp ?loc s + | _ -> raise Not_found) (patl, (fun r -> mkString (uninterp r)), inpat) let check_required_module ?loc sc (sp,d) = -- cgit v1.2.3 From fa8e58f00b6774ac8669a7282d7863f8a605abd2 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 14 Mar 2018 11:17:50 +0100 Subject: Notation: avoid one intermediate (unit -> ...) --- interp/notation.ml | 47 ++++++++++++++++++++++++++--------------------- 1 file changed, 26 insertions(+), 21 deletions(-) diff --git a/interp/notation.ml b/interp/notation.ml index 36d4b0aa15..4b25146c50 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -304,6 +304,8 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) 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 @@ -313,17 +315,19 @@ type 'a prim_token_uninterpreter = glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status type internal_prim_token_interpreter = - ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr) + | ForNumeral of rawnum prim_token_interpreter + | ForString of string prim_token_interpreter let prim_token_interpreter_tab = - (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t) + (Hashtbl.create 7 : + (scope_name, required_module * internal_prim_token_interpreter) Hashtbl.t) -let add_prim_token_interpreter sc interp = - Hashtbl.replace prim_token_interpreter_tab sc interp +let add_prim_token_interpreter sc (dir,interp) = + Hashtbl.replace prim_token_interpreter_tab sc (dir,interp) -let declare_prim_token_interpreter sc interp (patl,uninterp,b) = +let declare_prim_token_interpreter sc (dir,interp) (patl,uninterp,b) = declare_scope sc; - add_prim_token_interpreter sc interp; + add_prim_token_interpreter sc (dir,interp); List.iter (fun pat -> prim_token_key_table := KeyMap.add (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table) @@ -340,29 +344,21 @@ 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)) - -type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign - let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) = declare_prim_token_interpreter sc - (fun ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s) - | _ -> raise Not_found) + (dir, ForNumeral interp) (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 ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s) - | _ -> raise Not_found) + (dir, ForNumeral (fun ?loc (n,s) -> interp ?loc (ofNumeral n s))) (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 ?loc -> function String s -> delay dir interp ?loc s - | _ -> raise Not_found) + (dir, ForString interp) (patl, (fun r -> mkString (uninterp r)), inpat) let check_required_module ?loc sc (sp,d) = @@ -472,9 +468,14 @@ 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,interp) = Hashtbl.find prim_token_interpreter_tab sc in check_required_module ?loc sc spdir; - let pat = interp () in + let pat = + match p, interp with + | Numeral (n,s), ForNumeral interp -> interp ?loc (n,s) + | String s, ForString interp -> interp ?loc s + | _ -> raise Not_found + in check_allowed pat; pat, ((dirpath (fst spdir),DirPath.empty),"") @@ -680,8 +681,12 @@ let uninterp_prim_token_cases_pattern c = 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 + match n, Hashtbl.find prim_token_interpreter_tab scope with + | exception Not_found -> false + | Numeral _, (_,ForNumeral _) -> true + | String _, (_,ForString _) -> true + | _ -> false + in let scopes = make_current_scopes local_scopes in Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes) -- cgit v1.2.3 From 3099be05553dab10b41d864f4981860eb105f145 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 4 Apr 2018 16:06:50 +0200 Subject: Notation: remove support for prim tokens denoting inductive types in "return" This is prim token notations for inductive *types*, not values. So we're speaking of a scope where 0 is the type nat, 1 is the type bool, etc. To my knowledge, this feature hasn't ever been used, and is very unlikely to be used ever, so let's clean the code a bit by removing it. --- interp/constrextern.ml | 13 +------------ interp/notation.ml | 14 -------------- interp/notation.mli | 2 -- 3 files changed, 1 insertion(+), 28 deletions(-) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 009894fddb..ddc0a5c000 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -531,18 +531,7 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = else try if !Flags.raw_print || !print_no_symbol then raise No_match; - let (sc,p) = uninterp_prim_token_ind_pattern ind args in - match availability_of_entry_coercion custom InConstrEntrySomeLevel with - | None -> raise No_match - | Some coercion -> - match availability_of_prim_token p sc scopes with - | None -> raise No_match - | Some key -> - insert_pat_coercion coercion (insert_pat_delimiters (CAst.make @@ CPatPrim p) key) - with No_match -> - try - if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation_ind_pattern allscopes vars ind args + extern_notation_ind_pattern allscopes vars ind args (uninterp_ind_pattern_notations ind) with No_match -> let c = extern_reference vars (IndRef ind) in diff --git a/interp/notation.ml b/interp/notation.ml index 4b25146c50..ebb734cb08 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -654,20 +654,6 @@ let uninterp_prim_token c = | 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 - 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 uninterp_prim_token_cases_pattern c = try let k = cases_pattern_key c in diff --git a/interp/notation.mli b/interp/notation.mli index c921606484..e8408330af 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -110,8 +110,6 @@ val uninterp_prim_token : 'a glob_constr_g -> scope_name * prim_token val uninterp_prim_token_cases_pattern : 'a cases_pattern_g -> Name.t * scope_name * prim_token -val uninterp_prim_token_ind_pattern : - inductive -> cases_pattern list -> scope_name * prim_token val availability_of_prim_token : prim_token -> scope_name -> subscopes -> delimiters option option -- cgit v1.2.3 From 5df8f2ed3d9cf8d7903568308d8ce2e8e6dd4720 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 6 Apr 2018 14:38:02 +0200 Subject: Tacenv: minor code cleanup --- plugins/ltac/tacenv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 0bb9ccb1d8..1f2c722b34 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -144,7 +144,7 @@ let add ~deprecation kn b t = mactab := KNmap.add kn entry !mactab let replace kn path t = - let (path, _, _) = KerName.repr path in + let path = KerName.modpath path in let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in mactab := KNmap.modify kn entry !mactab -- cgit v1.2.3 From 3c2331a4a9d8c5d5f27c90185c616fe3400d4f1f Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 6 Apr 2018 16:36:09 +0200 Subject: Extraargs: avoid two token declarations to appear in all .vo Without this, the library segment of all .vo except Notations.vo starts with two TOKEN objects (declaration of tokens "->" and "<-"). This is due to side effects creating these objects during the dynlink of ltac_plugin.cmxs, more precisely the two Metasyntax.add_token_obj in Extraargs. It's quite cleaner to register these two side effects via Mltop.declare_cache_obj, so that the two objects only live in Notations.vo, and are loaded from there. --- plugins/ltac/extraargs.ml4 | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index dbbdbfa396..d779951180 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -52,8 +52,11 @@ let () = (* Rewriting orientation *) -let _ = Metasyntax.add_token_obj "<-" -let _ = Metasyntax.add_token_obj "->" +let _ = + Mltop.declare_cache_obj + (fun () -> Metasyntax.add_token_obj "<-"; + Metasyntax.add_token_obj "->") + "ltac_plugin" let pr_orient _prc _prlc _prt = function | true -> Pp.mt () -- cgit v1.2.3 From 93119295d0dd81669b46f52032c1bfe8f36afca0 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 6 Apr 2018 16:37:47 +0200 Subject: Prelude : update the comment about ML plugins loaded by Init --- theories/Init/Prelude.v | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 802f18c0f2..390ff5e240 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -19,8 +19,11 @@ Require Export Peano. Require Export Coq.Init.Wf. Require Export Coq.Init.Tactics. Require Export Coq.Init.Tauto. -(* Initially available plugins - (+ nat_syntax_plugin loaded in Datatypes) *) +(* Some initially available plugins. See also: + - ltac_plugin (in Notations) + - nat_syntax_plugin (in Datatypes) + - tauto_plugin (in Tauto). +*) Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". (* Default substrings not considered by queries like SearchAbout *) -- cgit v1.2.3 From b3c75936a4912ca794cdcecfeb92044552336c63 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 4 Apr 2018 10:43:38 +0200 Subject: prim notations backtrackable, their declarations now in two parts (API change) The first part (e.g. register_bignumeral_interpretation) deals only with the interp/uninterp closures. It should typically be done as a side effect during a syntax plugin loading. No prim notation are active yet after this phase. The second part (enable_prim_token_interpretation) activates the prim notation. It is now correctly talking to Summary and to the LibStack. To avoid "phantom" objects in libstack after a mere Require, this second part should be done inside a Mltop.declare_cache_obj The link between the two parts is a prim_token_uid (a string), which should be unique for each primitive notation. When this primitive notation is specific to a scope, the scope_name could be used as uid. Btw, the list of "patterns" for detecting when an uninterpreter should be considered is now restricted to a list of global_reference (inductive constructors, or injection functions such as IZR). The earlier API was accepting a glob_constr list, but was actually only working well for global_reference. A minimal compatibility is provided (declare_numeral_interpreter), but is discouraged, since it is known to store uncessary objects in the libstack. --- interp/notation.ml | 272 +++++++++++++++++++++++----------- interp/notation.mli | 60 ++++++-- plugins/syntax/ascii_syntax.ml | 17 ++- plugins/syntax/int31_syntax.ml | 20 ++- plugins/syntax/n_syntax.ml | 21 ++- plugins/syntax/nat_syntax.ml | 18 ++- plugins/syntax/positive_syntax.ml | 22 ++- plugins/syntax/r_syntax.ml | 21 ++- plugins/syntax/string_syntax.ml | 19 ++- plugins/syntax/z_syntax.ml | 22 ++- test-suite/interactive/PrimNotation.v | 18 +++ 11 files changed, 365 insertions(+), 145 deletions(-) create mode 100644 test-suite/interactive/PrimNotation.v diff --git a/interp/notation.ml b/interp/notation.ml index ebb734cb08..f60ddcf909 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -266,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, _) -> @@ -303,63 +301,167 @@ 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 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr +type 'a prim_token_uninterpreter = any_glob_constr -> 'a option + +type 'a prim_token_interpretation = + 'a prim_token_interpreter * 'a prim_token_uninterpreter + +module InnerPrimToken = struct -type cases_pattern_status = bool (* true = use prim token in patterns *) + 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) -type 'a prim_token_uninterpreter = - glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status + 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 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 -type internal_prim_token_interpreter = - | ForNumeral of rawnum prim_token_interpreter - | ForString of string prim_token_interpreter + 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 prim_token_interpreter_tab = - (Hashtbl.create 7 : - (scope_name, required_module * internal_prim_token_interpreter) Hashtbl.t) + let mkString = function + | None -> None + | Some s -> if Unicode.is_utf8 s then Some (String s) else None -let add_prim_token_interpreter sc (dir,interp) = - Hashtbl.replace prim_token_interpreter_tab sc (dir,interp) + 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) -let declare_prim_token_interpreter sc (dir,interp) (patl,uninterp,b) = +end + +(* The following two tables of (un)interpreters will *not* be synchronized. + But their indexes will be checked to be unique *) +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) + +(* 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_uid) 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_uid * bool) Refmap.t) + +let hashtbl_check_and_set uid f h eq = + match Hashtbl.find h uid with + | exception Not_found -> 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 uid (interp, uninterp) = + hashtbl_check_and_set + uid interp prim_token_interpreters InnerPrimToken.interp_eq; + hashtbl_check_and_set + uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq + +let register_rawnumeral_interpretation uid (interp, uninterp) = + register_gen_interpretation uid + (InnerPrimToken.RawNumInterp interp, InnerPrimToken.RawNumUninterp uninterp) + +let register_bignumeral_interpretation uid (interp, uninterp) = + register_gen_interpretation uid + (InnerPrimToken.BigNumInterp interp, InnerPrimToken.BigNumUninterp uninterp) + +let register_string_interpretation uid (interp, uninterp) = + register_gen_interpretation uid + (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp) + +type prim_token_infos = { + pt_scope : scope_name; (** Concerned scope *) + pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) + pt_required : required_module; (** Module that should be loaded first *) + pt_refs : global_reference list; (** Entry points during uninterpretation *) + pt_in_match : bool (** Is this prim token legal in match patterns ? *) +} + +let cache_prim_token_interpretation (_,infos) = + let sc = infos.pt_scope in + let uid = infos.pt_uid in declare_scope sc; - add_prim_token_interpreter sc (dir,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 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 declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) = - declare_prim_token_interpreter sc - (dir, ForNumeral interp) - (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) = - declare_prim_token_interpreter sc - (dir, ForNumeral (fun ?loc (n,s) -> interp ?loc (ofNumeral n s))) - (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat) - -let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = - declare_prim_token_interpreter sc - (dir, ForString interp) - (patl, (fun r -> mkString (uninterp r)), inpat) + prim_token_interp_infos := + String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos; + List.iter (fun r -> prim_token_uninterp_infos := + Refmap.add r (sc,uid,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 inPrimTokenInterp : prim_token_infos -> obj = + declare_object {(default_object "PRIM-TOKEN-INTERP") with + cache_function = cache_prim_token_interpretation; + load_function = (fun _ -> cache_prim_token_interpretation); + subst_function = subst_prim_token_interpretation; + classify_function = (fun o -> Substitute o)} + +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]). +*) + +let declare_numeral_interpreter sc dir interp (patl,uninterp,b) = + register_bignumeral_interpretation sc (interp,uninterp); + enable_prim_token_interpretation + { pt_scope = sc; + pt_uid = sc; + pt_required = dir; + pt_refs = List.map_filter glob_prim_constr_key patl; + pt_in_match = b } +let declare_string_interpreter sc dir interp (patl,uninterp,b) = + register_string_interpretation sc (interp,uninterp); + enable_prim_token_interpretation + { pt_scope = sc; + pt_uid = sc; + pt_required = dir; + pt_refs = List.map_filter glob_prim_constr_key patl; + pt_in_match = b } + let check_required_module ?loc sc (sp,d) = try let _ = Nametab.global_of_path sp in () @@ -468,14 +570,10 @@ 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 in + let (spdir,uid) = String.Map.find sc !prim_token_interp_infos in check_required_module ?loc sc spdir; - let pat = - match p, interp with - | Numeral (n,s), ForNumeral interp -> interp ?loc (n,s) - | String s, ForString interp -> interp ?loc s - | _ -> raise Not_found - in + let interp = Hashtbl.find prim_token_interpreters uid in + let pat = InnerPrimToken.do_interp ?loc interp p in check_allowed pat; pat, ((dirpath (fst spdir),DirPath.empty),"") @@ -646,32 +744,33 @@ let entry_has_ident = function try String.Map.find s !entry_has_ident_map <= n with Not_found -> false let uninterp_prim_token c = - 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 + match glob_prim_constr_key c with + | None -> raise Notation_ops.No_match + | Some r -> + try + let (sc,uid,_) = Refmap.find r !prim_token_uninterp_infos in + let uninterp = Hashtbl.find prim_token_uninterpreters uid 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 = - match n, Hashtbl.find prim_token_interpreter_tab scope with - | exception Not_found -> false - | Numeral _, (_,ForNumeral _) -> true - | String _, (_,ForString _) -> true - | _ -> false + try + let uid = snd (String.Map.find scope !prim_token_interp_infos) in + let interp = Hashtbl.find prim_token_interpreters uid in + let open InnerPrimToken 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) @@ -1193,16 +1292,19 @@ let pr_visibility prglob = function let freeze _ = (!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,scs,asc,dlm,fkm,clsc,coe,globs,ids) = +let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = scope_map := scm; scope_stack := scs; delimiters_map := dlm; arguments_scope := asc; notations_key_table := fkm; 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 @@ -1211,7 +1313,9 @@ let init () = init_scope_map (); delimiters_map := String.Map.empty; notations_key_table := KeyMap.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" diff --git a/interp/notation.mli b/interp/notation.mli index e8408330af..2545e494ef 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Bigint open Names open Libnames open Constrexpr @@ -75,24 +74,61 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name type notation_location = (DirPath.t * DirPath.t) * string type required_module = full_path * string list -type cases_pattern_status = bool (** true = use prim token in patterns *) +type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign -type 'a prim_token_interpreter = - ?loc:Loc.t -> 'a -> glob_constr +(** The unique id string below will be used to refer to a particular + registered interpreter/uninterpreter of numeral or string notation. + Using the same uid for different (un)interpreters will fail. + If at most one interpretation of prim token is used per scope, + then the scope name could be used as unique id. *) -type 'a prim_token_uninterpreter = - glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status +type prim_token_uid = string -type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign +type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr +type 'a prim_token_uninterpreter = any_glob_constr -> 'a option -val declare_rawnumeral_interpreter : scope_name -> required_module -> - rawnum prim_token_interpreter -> rawnum prim_token_uninterpreter -> unit +type 'a prim_token_interpretation = + 'a prim_token_interpreter * 'a prim_token_uninterpreter -val declare_numeral_interpreter : scope_name -> required_module -> - bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit +val register_rawnumeral_interpretation : + prim_token_uid -> rawnum prim_token_interpretation -> unit + +val register_bignumeral_interpretation : + prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit + +val register_string_interpretation : + prim_token_uid -> string prim_token_interpretation -> unit + +type prim_token_infos = { + pt_scope : scope_name; (** Concerned scope *) + pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) + pt_required : required_module; (** Module that should be loaded first *) + pt_refs : global_reference list; (** Entry points during uninterpretation *) + pt_in_match : bool (** Is this prim token legal in match patterns ? *) +} +(** Note: most of the time, the [pt_refs] field above will contain + inductive constructors (e.g. O and S for nat). But it could also be + injection functions such as IZR for reals. *) + +(** Activate a prim token interpretation whose unique id and functions + have already been registered. *) + +val enable_prim_token_interpretation : prim_token_infos -> unit + +(** 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]). +*) + +val declare_numeral_interpreter : scope_name -> required_module -> + Bigint.bigint prim_token_interpreter -> + glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit val declare_string_interpreter : scope_name -> required_module -> - string prim_token_interpreter -> string prim_token_uninterpreter -> unit + string prim_token_interpreter -> + glob_constr list * string prim_token_uninterpreter * bool -> unit (** Return the [term]/[cases_pattern] bound to a primitive token in a given scope context*) diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 47a59ba631..9bf0b29b61 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -83,8 +83,17 @@ let make_ascii_string n = let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r) +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + let _ = - Notation.declare_string_interpreter "char_scope" - (ascii_path,ascii_module) - interp_ascii_string - ([DAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) + let sc = "char_scope" in + register_string_interpretation sc (interp_ascii_string,uninterp_ascii_string); + at_declare_ml_module enable_prim_token_interpretation + { pt_scope = sc; + pt_uid = sc; + pt_required = (ascii_path,ascii_module); + pt_refs = [static_glob_Ascii]; + pt_in_match = true } diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml index f10f98e23b..731eae349a 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -96,10 +96,18 @@ let uninterp_int31 (AnyGlobConstr i) = with Non_closed -> None +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + (* Actually declares the interpreter for int31 *) -let _ = Notation.declare_numeral_interpreter int31_scope - (int31_path, int31_module) - interp_int31 - ([DAst.make (GRef (int31_construct, None))], - uninterp_int31, - true) + +let _ = + register_bignumeral_interpretation int31_scope (interp_int31,uninterp_int31); + at_declare_ml_module enable_prim_token_interpretation + { pt_scope = int31_scope; + pt_uid = int31_scope; + pt_required = (int31_path,int31_module); + pt_refs = [int31_construct]; + pt_in_match = true } diff --git a/plugins/syntax/n_syntax.ml b/plugins/syntax/n_syntax.ml index 0e202be47f..29b88b1cb3 100644 --- a/plugins/syntax/n_syntax.ml +++ b/plugins/syntax/n_syntax.ml @@ -72,10 +72,17 @@ let uninterp_n (AnyGlobConstr p) = (************************************************************************) (* Declaring interpreters and uninterpreters for N *) -let _ = Notation.declare_numeral_interpreter "N_scope" - (n_path,binnums) - n_of_int - ([DAst.make @@ GRef (glob_N0, None); - DAst.make @@ GRef (glob_Npos, None)], - uninterp_n, - true) +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + +let _ = + let scope = "N_scope" in + register_bignumeral_interpretation scope (n_of_int,uninterp_n); + at_declare_ml_module enable_prim_token_interpretation + { pt_scope = scope; + pt_uid = scope; + pt_required = (n_path,binnums); + pt_refs = [glob_N0; glob_Npos]; + pt_in_match = true } diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index e158e0b516..85cb49586d 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -78,8 +78,18 @@ let uninterp_nat (AnyGlobConstr p) = (************************************************************************) (* Declare the primitive parsers and printers *) +open Notation + +let nat_scope = "nat_scope" + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + let _ = - Notation.declare_numeral_interpreter "nat_scope" - (nat_path,datatypes_module_name) - nat_of_int - ([DAst.make @@ GRef (glob_S,None); DAst.make @@ GRef (glob_O,None)], uninterp_nat, true) + register_bignumeral_interpretation nat_scope (nat_of_int,uninterp_nat); + at_declare_ml_module enable_prim_token_interpretation + { pt_scope = nat_scope; + pt_uid = nat_scope; + pt_required = (nat_path,datatypes_module_name); + pt_refs = [glob_S; glob_O]; + pt_in_match = true } diff --git a/plugins/syntax/positive_syntax.ml b/plugins/syntax/positive_syntax.ml index 0c82e47445..6fce4de9ef 100644 --- a/plugins/syntax/positive_syntax.ml +++ b/plugins/syntax/positive_syntax.ml @@ -91,11 +91,17 @@ let uninterp_positive (AnyGlobConstr p) = (* Declaring interpreters and uninterpreters for positive *) (************************************************************************) -let _ = Notation.declare_numeral_interpreter "positive_scope" - (positive_path,binnums) - interp_positive - ([DAst.make @@ GRef (glob_xI, None); - DAst.make @@ GRef (glob_xO, None); - DAst.make @@ GRef (glob_xH, None)], - uninterp_positive, - true) +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + +let _ = + let scope = "positive_scope" in + register_bignumeral_interpretation scope (interp_positive,uninterp_positive); + at_declare_ml_module enable_prim_token_interpretation + { pt_scope = scope; + pt_uid = scope; + pt_required = (positive_path,binnums); + pt_refs = [glob_xI; glob_xO; glob_xH]; + pt_in_match = true } diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 94aa143350..eccc544e41 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -131,9 +131,18 @@ let uninterp_r (AnyGlobConstr p) = with Non_closed_number -> None -let _ = Notation.declare_numeral_interpreter "R_scope" - (r_path,["Coq";"Reals";"Rdefinitions"]) - r_of_int - ([DAst.make @@ GRef (glob_IZR, None)], - uninterp_r, - false) +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + +let r_scope = "R_scope" + +let _ = + register_bignumeral_interpretation r_scope (r_of_int,uninterp_r); + at_declare_ml_module enable_prim_token_interpretation + { pt_scope = r_scope; + pt_uid = r_scope; + pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]); + pt_refs = [glob_IZR]; + pt_in_match = false } diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index c22869f4d6..ca1bf0df27 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -64,10 +64,17 @@ let uninterp_string (AnyGlobConstr r) = with Non_closed_string -> None +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + let _ = - Notation.declare_string_interpreter "string_scope" - (string_path,["Coq";"Strings";"String"]) - interp_string - ([DAst.make @@ GRef (static_glob_String,None); - DAst.make @@ GRef (static_glob_EmptyString,None)], - uninterp_string, true) + let sc = "string_scope" in + register_string_interpretation sc (interp_string,uninterp_string); + at_declare_ml_module enable_prim_token_interpretation + { pt_scope = sc; + pt_uid = sc; + pt_required = (string_path,["Coq";"Strings";"String"]); + pt_refs = [static_glob_String; static_glob_EmptyString]; + pt_in_match = true } diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 2534162e36..72e1321eab 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -68,11 +68,17 @@ let uninterp_z (AnyGlobConstr p) = (************************************************************************) (* Declaring interpreters and uninterpreters for Z *) -let _ = Notation.declare_numeral_interpreter "Z_scope" - (z_path,binnums) - z_of_int - ([DAst.make @@ GRef (glob_ZERO, None); - DAst.make @@ GRef (glob_POS, None); - DAst.make @@ GRef (glob_NEG, None)], - uninterp_z, - true) +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + +let _ = + let scope = "Z_scope" in + register_bignumeral_interpretation scope (z_of_int,uninterp_z); + at_declare_ml_module enable_prim_token_interpretation + { pt_scope = scope; + pt_uid = scope; + pt_required = (z_path,binnums); + pt_refs = [glob_ZERO; glob_POS; glob_NEG]; + pt_in_match = true } diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v new file mode 100644 index 0000000000..ca8cba67d5 --- /dev/null +++ b/test-suite/interactive/PrimNotation.v @@ -0,0 +1,18 @@ +(* Until recently, the Notation.declare_numeral_notation wasn't synchronized + w.r.t. backtracking. This should be ok now. + This test is pretty artificial (we must declare Z_scope for this to work). +*) + +Delimit Scope Z_scope with Z. +Open Scope Z_scope. +Check 0. +(* 0 : nat *) +Require BinNums. +Check 0. +(* 0 : BinNums.Z *) +Back 2. +Check 0. +(* Expected answer: 0 : nat *) +(* Used to fail with: +Error: Cannot interpret in Z_scope without requiring first module BinNums. +*) -- cgit v1.2.3 From b786723fe7aff0c58ac949d44a356e2df6805645 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 22 Feb 2017 23:15:24 +0100 Subject: Numeral Notation (for inductive types) This is a portion of roglo's PR#156 introducing a Numeral Notation command : we deal here with inductive types via conversion fonctions from/to Z written in Coq. For an example, see plugins/syntax/NatSyntaxViaZ.v This commit does not include the part about printing via some ltac. Using ltac was meant for dealing with real numbers, let's see first what become PR#415 about a compact representation for real literals. --- Makefile.common | 3 +- plugins/syntax/NatSyntaxViaZ.v | 56 +++++ plugins/syntax/g_numeral.ml4 | 283 ++++++++++++++++++++++++++ plugins/syntax/numeral_notation_plugin.mlpack | 1 + 4 files changed, 342 insertions(+), 1 deletion(-) create mode 100644 plugins/syntax/NatSyntaxViaZ.v create mode 100644 plugins/syntax/g_numeral.ml4 create mode 100644 plugins/syntax/numeral_notation_plugin.mlpack diff --git a/Makefile.common b/Makefile.common index 772561bd70..4f09fb376a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -146,7 +146,8 @@ OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \ z_syntax_plugin.cmo r_syntax_plugin.cmo \ int31_syntax_plugin.cmo \ ascii_syntax_plugin.cmo \ - string_syntax_plugin.cmo ) + string_syntax_plugin.cmo \ + numeral_notation_plugin.cmo) DERIVECMO:=plugins/derive/derive_plugin.cmo LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo diff --git a/plugins/syntax/NatSyntaxViaZ.v b/plugins/syntax/NatSyntaxViaZ.v new file mode 100644 index 0000000000..adee347d90 --- /dev/null +++ b/plugins/syntax/NatSyntaxViaZ.v @@ -0,0 +1,56 @@ +Declare ML Module "numeral_notation_plugin". +Require Import BinNums. + +(** ** Parsing and Printing digit strings as type nat *) + +Fixpoint pos_pred_double x := + match x with + | xI p => xI (xO p) + | xO p => xI (pos_pred_double p) + | xH => xH + end. + +Definition nat_of_Z x := + match x with + | Z0 => Some O + | Zpos p => + let fix iter p a := + match p with + | xI p0 => a + iter p0 (a + a) + | xO p0 => iter p0 (a + a) + | xH => a + end + in + Some (iter p (S O)) + | Zneg p => None + end. + +Fixpoint pos_succ x := + match x with + | xI p => xO (pos_succ p) + | xO p => xI p + | xH => xO xH + end. + +Definition Z_succ x := + match x with + | Z0 => Zpos xH + | Zpos x => Zpos (pos_succ x) + | Zneg x => + match x with + | xI p => Zneg (xO p) + | xO p => Zneg (pos_pred_double p) + | xH => Z0 + end + end. + +Fixpoint Z_of_nat_loop n := + match n with + | O => Z0 + | S p => Z_succ (Z_of_nat_loop p) + end. + +Definition Z_of_nat n := Some (Z_of_nat_loop n). + +Numeral Notation nat nat_of_Z Z_of_nat : nat_scope + (warning after 5000). diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 new file mode 100644 index 0000000000..b3f0591614 --- /dev/null +++ b/plugins/syntax/g_numeral.ml4 @@ -0,0 +1,283 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + 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 + end + | Const (c, _) -> anomaly (str "Const " ++ str (Constant.to_string c)) + | x -> anomaly (str "bigint_of_z App c " ++ str (obj_string x)) + end + | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero + | _ -> raise Not_found + +let constr_of_global_reference = function + | VarRef v -> mkVar v + | ConstRef cr -> mkConst cr + | IndRef ind -> mkInd ind + | ConstructRef c -> mkConstruct c + +let rec constr_of_glob_constr vl gc = + match DAst.get gc with + | Glob_term.GRef (gr, gllo) -> + constr_of_global_reference gr + | Glob_term.GVar (id) -> + constr_of_glob_constr vl (List.assoc id vl) + | Glob_term.GApp (gc, gcl) -> + let c = constr_of_glob_constr vl gc in + let cl = List.map (constr_of_glob_constr vl) gcl in + mkApp (c, Array.of_list cl) + | _ -> + raise Not_found + +let rec glob_constr_of_constr ?loc c = match Constr.kind c with + | Var id -> + DAst.make ?loc (Glob_term.GRef (VarRef id, None)) + | App (c, ca) -> + let c = glob_constr_of_constr ?loc c in + let cel = List.map (glob_constr_of_constr ?loc) (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)) + | x -> + anomaly (str "1 constr " ++ str (obj_string x)) + +let interp_big_int zposty ty thr f ?loc bi = + let t = + let c = mkApp (mkConst f, [| z_of_bigint zposty ty thr bi |]) in + eval_constr c + in + match Constr.kind t with + | App (_, [| _; c |]) -> glob_constr_of_constr ?loc c + | App (_, [| _ |]) -> + CErrors.user_err ?loc + (str "Cannot interpret this number as a value of type " ++ + str (string_of_reference ty)) + | x -> + anomaly (str "interp_big_int " ++ str (obj_string x)) + +let uninterp_big_int g (Glob_term.AnyGlobConstr c) = + match try Some (constr_of_glob_constr [] c) with Not_found -> None with + | Some c -> + begin match + try Some (eval_constr (mkApp (mkConst g, [| c |]))) + with Type_errors.TypeError _ -> None + with + | Some t -> + begin match Constr.kind t with + | App (c, [| _; x |]) -> Some (bigint_of_z x) + | x -> None + end + | None -> + None + end + | None -> + None + +let load_numeral_notation _ (_, (zposty, ty, f, g, sc, patl, thr, path)) = + Notation.declare_numeral_interpreter sc (path, []) + (interp_big_int zposty ty thr f) + (patl, uninterp_big_int g, true) + +let cache_numeral_notation o = load_numeral_notation 1 o + +type numeral_notation_obj = + (Names.inductive * Names.inductive) * + Libnames.reference * Names.Constant.t * + Names.Constant.t * + Notation_term.scope_name * Glob_term.glob_constr list * + Bigint.bigint * Libnames.full_path + +let inNumeralNotation : numeral_notation_obj -> Libobject.obj = + Libobject.declare_object { + (Libobject.default_object "NUMERAL NOTATION") with + Libobject.cache_function = cache_numeral_notation; + Libobject.load_function = load_numeral_notation } + +let vernac_numeral_notation ty f g sc waft = + let zposty = + let zty = + let c = qualid_of_ident (Id.of_string "Z") in + try match Nametab.locate c with IndRef i -> i | _ -> raise Not_found + with Not_found -> Nametab.error_global_not_found (CAst.make c) + in + let positivety = + let c = qualid_of_ident (Id.of_string "positive") in + try match Nametab.locate c with IndRef i -> i | _ -> raise Not_found + with Not_found -> Nametab.error_global_not_found (CAst.make c) + in + (zty, positivety) + in + let tyc = + let tyq = qualid_of_reference ty in + try Nametab.locate CAst.(tyq.v) with Not_found -> + Nametab.error_global_not_found tyq + in + let fc = + let fq = qualid_of_reference f in + try Nametab.locate_constant CAst.(fq.v) with Not_found -> + Nametab.error_global_not_found fq + in + let lqid = CAst.((qualid_of_reference ty).v) in + let crq = mkRefC (CAst.make (Qualid lqid)) in + let app x y = CAst.make (CApp ((None, x), [(y, None)])) in + let cref s = mkIdentC (Names.Id.of_string s) in + let arrow x y = + mkProdC ([CAst.make Anonymous], Default Decl_kinds.Explicit, x, y) + in + let _ = + (* checking "f" is of type "Z -> option ty" *) + let c = + mkCastC + (mkRefC f, + CastConv (arrow (cref "Z") (app (cref "option") crq))) + in + let (sigma, env) = Pfedit.get_current_context () in + Constrintern.intern_constr env sigma c + in + let thr = Bigint.of_int waft in + let path = Nametab.path_of_global tyc in + match tyc with + | IndRef (sp, spi) -> + let gc = + let gq = qualid_of_reference g in + try Nametab.locate_constant CAst.(gq.v) with Not_found -> + Nametab.error_global_not_found gq + in + let _ = + (* checking "g" is of type "ty -> option Z" *) + let c = + mkCastC + (mkRefC g, + CastConv (arrow crq (app (cref "option") (cref "Z")))) + in + let (sigma, env) = Pfedit.get_current_context () in + Constrintern.interp_open_constr env sigma c + in + let env = Global.env () in + let patl = + let mc = + let mib = Environ.lookup_mind sp env in + let inds = + List.init (Array.length mib.Declarations.mind_packets) + (fun x -> (sp, x)) + in + let ind = List.hd inds in + let mip = mib.Declarations.mind_packets.(snd ind) in + mip.Declarations.mind_consnames + in + Array.to_list + (Array.mapi + (fun i c -> + DAst.make + (Glob_term.GRef + (ConstructRef ((sp, spi), i + 1), None))) + mc) + in + Lib.add_anonymous_leaf + (inNumeralNotation + (zposty, ty, fc, gc, sc, patl, thr, path)) + | ConstRef _ | ConstructRef _ | VarRef _ -> + CErrors.user_err + (str (string_of_reference ty) ++ str " is not an inductive type") + +open Stdarg + +VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF + | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + ident(sc) ] -> + [ let waft = 0 in + vernac_numeral_notation ty f g (Id.to_string sc) waft ] + | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + ident(sc) "(" "warning" "after" int(waft) ")" ] -> + [ vernac_numeral_notation ty f g (Id.to_string sc) waft ] +END diff --git a/plugins/syntax/numeral_notation_plugin.mlpack b/plugins/syntax/numeral_notation_plugin.mlpack new file mode 100644 index 0000000000..643c148979 --- /dev/null +++ b/plugins/syntax/numeral_notation_plugin.mlpack @@ -0,0 +1 @@ +G_numeral -- cgit v1.2.3 From f3d18836471ced1244922430df4195f79b347a7c Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 27 Feb 2017 12:30:51 +0100 Subject: Numeral Notation: misc code improvements (records, subfunctions, exceptions ...) --- plugins/syntax/NatSyntaxViaZ.v | 7 +- plugins/syntax/g_numeral.ml4 | 369 +++++++++++++++++++++-------------------- 2 files changed, 191 insertions(+), 185 deletions(-) diff --git a/plugins/syntax/NatSyntaxViaZ.v b/plugins/syntax/NatSyntaxViaZ.v index adee347d90..8a4d8f236d 100644 --- a/plugins/syntax/NatSyntaxViaZ.v +++ b/plugins/syntax/NatSyntaxViaZ.v @@ -44,13 +44,14 @@ Definition Z_succ x := end end. -Fixpoint Z_of_nat_loop n := +Fixpoint Z_of_nat n := match n with | O => Z0 - | S p => Z_succ (Z_of_nat_loop p) + | S p => Z_succ (Z_of_nat p) end. -Definition Z_of_nat n := Some (Z_of_nat_loop n). +(** The 1st conversion must either have type [Z->nat] or [Z->option nat]. + The 2nd one must either have type [nat->Z] or [nat->option Z]. *) Numeral Notation nat nat_of_Z Z_of_nat : nat_scope (warning after 5000). diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index b3f0591614..b4c6a06ab0 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -9,7 +9,6 @@ DECLARE PLUGIN "numeral_notation_plugin" open Pp -open CErrors open Util open Names open Libnames @@ -19,12 +18,7 @@ open Constrexpr_ops open Constr open Misctypes -(* Numeral notation *) - -let obj_string x = - if Obj.is_block (Obj.repr x) then - "tag = " ^ string_of_int (Obj.tag (Obj.repr x)) - else "int_val = " ^ string_of_int (Obj.magic x) +(** * Numeral notation *) let eval_constr (c : Constr.t) = let env = Global.env () in @@ -35,6 +29,20 @@ let eval_constr (c : Constr.t) = (EConstr.of_constr j.Environ.uj_type) in EConstr.Unsafe.to_constr c' +exception NotANumber + +let warning_big_num ty = + strbrk "Stack overflow or segmentation fault happens when " ++ + strbrk "working with large numbers in " ++ pr_reference ty ++ + strbrk " (threshold may vary depending" ++ + strbrk " on your system limits and on the command executed)." + +type conversion_function = + | Direct of Constant.t + | Option of Constant.t + +(** Conversion between Coq's [Positive] and our internal bigint *) + let rec pos_of_bigint posty n = match Bigint.div2_with_rest n with | (q, false) -> @@ -47,135 +55,127 @@ let rec pos_of_bigint posty n = 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 + | n -> assert false (* no other constructor of type positive *) end - | x -> raise Not_found + | x -> raise NotANumber end - | Construct ((_, 3), _) -> (* xH *) Bigint.one - | x -> anomaly (str "bigint_of_pos" ++ str (obj_string x)) + | x -> raise NotANumber + +(** Conversion between Coq's [Z] and our internal bigint *) -let z_of_bigint (zty, posty) ty thr n = +type z_pos_ty = + { z_ty : Names.inductive; + pos_ty : Names.inductive } + +let maybe_warn (thr,msg) n = if Bigint.is_pos_or_zero n && not (Bigint.equal thr Bigint.zero) && Bigint.less_than thr n - then - Feedback.msg_warning - (strbrk "Stack overflow or segmentation fault happens when " ++ - strbrk "working with large numbers in " ++ - str (string_of_reference ty) ++ - strbrk " (threshold may vary depending" ++ - strbrk " on your system limits and on the command executed).") - else (); - if not (Bigint.equal n Bigint.zero) then + then Feedback.msg_warning msg + +let z_of_bigint { z_ty; pos_ty } warn n = + maybe_warn warn 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 (zty, s) in - mkApp (c, [| pos_of_bigint posty n |]) - else - mkConstruct (zty, 1) (* Z0 *) + 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 + | n -> assert false (* no other constructor of type Z *) end - | Const (c, _) -> anomaly (str "Const " ++ str (Constant.to_string c)) - | x -> anomaly (str "bigint_of_z App c " ++ str (obj_string x)) + | _ -> raise NotANumber end - | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero - | _ -> raise Not_found - -let constr_of_global_reference = function - | VarRef v -> mkVar v - | ConstRef cr -> mkConst cr - | IndRef ind -> mkInd ind - | ConstructRef c -> mkConstruct c - -let rec constr_of_glob_constr vl gc = - match DAst.get gc with - | Glob_term.GRef (gr, gllo) -> - constr_of_global_reference gr - | Glob_term.GVar (id) -> - constr_of_glob_constr vl (List.assoc id vl) + | _ -> raise NotANumber + +(** The uinterp 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 g = match DAst.get g with + | Glob_term.GRef (ConstructRef c, _) -> mkConstruct c | Glob_term.GApp (gc, gcl) -> - let c = constr_of_glob_constr vl gc in - let cl = List.map (constr_of_glob_constr vl) gcl in + let c = constr_of_glob gc in + let cl = List.map constr_of_glob gcl in mkApp (c, Array.of_list cl) | _ -> - raise Not_found + raise NotANumber -let rec glob_constr_of_constr ?loc c = match Constr.kind c with - | Var id -> - DAst.make ?loc (Glob_term.GRef (VarRef id, None)) +let rec glob_of_constr ?loc c = match Constr.kind c with | App (c, ca) -> - let c = glob_constr_of_constr ?loc c in - let cel = List.map (glob_constr_of_constr ?loc) (Array.to_list ca) in + let c = glob_of_constr ?loc c in + let cel = List.map (glob_of_constr ?loc) (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)) - | x -> - anomaly (str "1 constr " ++ str (obj_string x)) - -let interp_big_int zposty ty thr f ?loc bi = - let t = - let c = mkApp (mkConst f, [| z_of_bigint zposty ty thr bi |]) in - eval_constr c - in - match Constr.kind t with - | App (_, [| _; c |]) -> glob_constr_of_constr ?loc c - | App (_, [| _ |]) -> - CErrors.user_err ?loc - (str "Cannot interpret this number as a value of type " ++ - str (string_of_reference ty)) - | x -> - anomaly (str "interp_big_int " ++ str (obj_string x)) - -let uninterp_big_int g (Glob_term.AnyGlobConstr c) = - match try Some (constr_of_glob_constr [] c) with Not_found -> None with - | Some c -> - begin match - try Some (eval_constr (mkApp (mkConst g, [| c |]))) - with Type_errors.TypeError _ -> None - with - | Some t -> - begin match Constr.kind t with - | App (c, [| _; x |]) -> Some (bigint_of_z x) - | x -> None - end - | None -> - None - end - | None -> - None + | 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)) + | _ -> CErrors.anomaly (str "interp_big_int: unexpected constr") -let load_numeral_notation _ (_, (zposty, ty, f, g, sc, patl, thr, path)) = - Notation.declare_numeral_interpreter sc (path, []) - (interp_big_int zposty ty thr f) - (patl, uninterp_big_int g, true) +let interp_big_int zposty ty warn of_z ?loc bi = + match of_z with + | Direct f -> + let c = mkApp (mkConst f, [| z_of_bigint zposty warn bi |]) in + glob_of_constr ?loc (eval_constr c) + | Option f -> + let c = mkApp (mkConst f, [| z_of_bigint zposty warn bi |]) in + match Constr.kind (eval_constr c) with + | App (_Some, [| _; c |]) -> glob_of_constr ?loc c + | App (_None, [| _ |]) -> + CErrors.user_err ?loc + (str "Cannot interpret this number as a value of type " ++ + pr_reference ty) + | x -> CErrors.anomaly (str "interp_big_int: option expected") -let cache_numeral_notation o = load_numeral_notation 1 o +let uninterp_big_int to_z (Glob_term.AnyGlobConstr c) = + try + let t = constr_of_glob c in + match to_z with + | Direct g -> + let r = eval_constr (mkApp (mkConst g, [| t |])) in + Some (bigint_of_z r) + | Option g -> + let r = eval_constr (mkApp (mkConst g, [| t |])) in + match Constr.kind r with + | App (_Some, [| _; x |]) -> Some (bigint_of_z x) + | x -> None + with + | Type_errors.TypeError _ -> None (* cf. eval_constr *) + | NotANumber -> None (* cf constr_of_glob or bigint_of_z *) type numeral_notation_obj = - (Names.inductive * Names.inductive) * - Libnames.reference * Names.Constant.t * - Names.Constant.t * - Notation_term.scope_name * Glob_term.glob_constr list * - Bigint.bigint * Libnames.full_path + { num_ty : Libnames.reference; + z_pos_ty : z_pos_ty; + of_z : conversion_function; + to_z : conversion_function; + scope : Notation_term.scope_name; + constructors : Glob_term.glob_constr list; + warning : Bigint.bigint * Pp.t; + path : Libnames.full_path } + +let load_numeral_notation _ (_, o) = + Notation.declare_numeral_interpreter o.scope (o.path, []) + (interp_big_int o.z_pos_ty o.num_ty o.warning o.of_z) + (o.constructors, uninterp_big_int o.to_z, true) + +let cache_numeral_notation o = load_numeral_notation 1 o let inNumeralNotation : numeral_notation_obj -> Libobject.obj = Libobject.declare_object { @@ -183,92 +183,97 @@ let inNumeralNotation : numeral_notation_obj -> Libobject.obj = Libobject.cache_function = cache_numeral_notation; Libobject.load_function = load_numeral_notation } -let vernac_numeral_notation ty f g sc waft = - let zposty = - let zty = - let c = qualid_of_ident (Id.of_string "Z") in - try match Nametab.locate c with IndRef i -> i | _ -> raise Not_found - with Not_found -> Nametab.error_global_not_found (CAst.make c) - in - let positivety = - let c = qualid_of_ident (Id.of_string "positive") in - try match Nametab.locate c with IndRef i -> i | _ -> raise Not_found - with Not_found -> Nametab.error_global_not_found (CAst.make c) - in - (zty, positivety) - in - let tyc = - let tyq = qualid_of_reference ty in - try Nametab.locate CAst.(tyq.v) with Not_found -> - Nametab.error_global_not_found tyq - in - let fc = - let fq = qualid_of_reference f in - try Nametab.locate_constant CAst.(fq.v) with Not_found -> - Nametab.error_global_not_found fq +let get_constructors ind = + let mib,oib = Global.lookup_inductive ind in + let mc = oib.Declarations.mind_consnames in + Array.to_list + (Array.mapi + (fun j c -> + DAst.make + (Glob_term.GRef (ConstructRef (ind, j + 1), None))) + mc) + +let locate_ind s = + let q = qualid_of_string s in + try + match Nametab.locate q with + | IndRef i -> i + | _ -> raise Not_found + with Not_found -> Nametab.error_global_not_found (CAst.make q) + +(** TODO: we should ensure that BinNums is loaded (or autoload it ?) *) + +let locate_z () = + { z_ty = locate_ind "Coq.Numbers.BinNums.Z"; + pos_ty = locate_ind "Coq.Numbers.BinNums.positive"; } + +let locate_globref r = + let q = qualid_of_reference r in + try Nametab.locate CAst.(q.v) + with Not_found -> Nametab.error_global_not_found q + +let locate_constant r = + let q = qualid_of_reference r in + try Nametab.locate_constant CAst.(q.v) + with Not_found -> Nametab.error_global_not_found q + +let has_type f ty = + let (sigma, env) = Pfedit.get_current_context () in + let c = mkCastC (mkRefC f, CastConv ty) in + try let _ = Constrintern.interp_constr env sigma c in true + with Pretype_errors.PretypeError _ -> false + +let vernac_numeral_notation ty f g scope waft = + let z_pos_ty = locate_z () in + let tyc = locate_globref ty in + let fc = locate_constant f in + let gc = locate_constant g in + let cty = mkRefC (CAst.(make (Qualid (qualid_of_reference ty).v))) in - let lqid = CAst.((qualid_of_reference ty).v) in - let crq = mkRefC (CAst.make (Qualid lqid)) in - let app x y = CAst.make (CApp ((None, x), [(y, None)])) in - let cref s = mkIdentC (Names.Id.of_string s) in + let app x y = mkAppC (x,[y]) in + let cref s = mkIdentC (Id.of_string s) in let arrow x y = - mkProdC ([CAst.make Anonymous], Default Decl_kinds.Explicit, x, y) + mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) in - let _ = - (* checking "f" is of type "Z -> option ty" *) - let c = - mkCastC - (mkRefC f, - CastConv (arrow (cref "Z") (app (cref "option") crq))) - in - let (sigma, env) = Pfedit.get_current_context () in - Constrintern.intern_constr env sigma c + (* Check that [ty] is an inductive type *) + let constructors = match tyc with + | IndRef ind -> get_constructors ind + | ConstRef _ | ConstructRef _ | VarRef _ -> + CErrors.user_err + (pr_reference ty ++ str " is not an inductive type") in - let thr = Bigint.of_int waft in - let path = Nametab.path_of_global tyc in - match tyc with - | IndRef (sp, spi) -> - let gc = - let gq = qualid_of_reference g in - try Nametab.locate_constant CAst.(gq.v) with Not_found -> - Nametab.error_global_not_found gq - in - let _ = - (* checking "g" is of type "ty -> option Z" *) - let c = - mkCastC - (mkRefC g, - CastConv (arrow crq (app (cref "option") (cref "Z")))) - in - let (sigma, env) = Pfedit.get_current_context () in - Constrintern.interp_open_constr env sigma c - in - let env = Global.env () in - let patl = - let mc = - let mib = Environ.lookup_mind sp env in - let inds = - List.init (Array.length mib.Declarations.mind_packets) - (fun x -> (sp, x)) - in - let ind = List.hd inds in - let mip = mib.Declarations.mind_packets.(snd ind) in - mip.Declarations.mind_consnames - in - Array.to_list - (Array.mapi - (fun i c -> - DAst.make - (Glob_term.GRef - (ConstructRef ((sp, spi), i + 1), None))) - mc) - in - Lib.add_anonymous_leaf - (inNumeralNotation - (zposty, ty, fc, gc, sc, patl, thr, path)) - | ConstRef _ | ConstructRef _ | VarRef _ -> + (* Is "f" of type "Z -> ty" or "Z -> option ty" ? *) + let of_z = + if has_type f (arrow (cref "Z") cty) then + Direct fc + else if has_type f (arrow (cref "Z") (app (cref "option") cty)) then + Option fc + else + CErrors.user_err + (pr_reference f ++ str " should goes from Z to " ++ + pr_reference ty ++ str " or (option " ++ pr_reference ty ++ str ")") + in + (* Is "g" of type "ty -> Z" or "ty -> option Z" ? *) + let to_z = + if has_type g (arrow cty (cref "Z")) then + Direct gc + else if has_type g (arrow cty (app (cref "option") (cref "Z"))) then + Option gc + else CErrors.user_err - (str (string_of_reference ty) ++ str " is not an inductive type") + (pr_reference g ++ str " should goes from " ++ + pr_reference ty ++ str " to Z or (option Z)") + in + Lib.add_anonymous_leaf + (inNumeralNotation + { num_ty = ty; + z_pos_ty; + of_z; + to_z; + scope; + constructors; + warning = (Bigint.of_int waft, warning_big_num ty); + path = Nametab.path_of_global tyc }) open Stdarg -- cgit v1.2.3 From b344d8d3bf9a0685d31db51788aab817da85e5b8 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 21 Mar 2017 15:37:34 +0100 Subject: remove test file NatSyntaxViaZ.v --- plugins/syntax/NatSyntaxViaZ.v | 57 ------------------------------------------ 1 file changed, 57 deletions(-) delete mode 100644 plugins/syntax/NatSyntaxViaZ.v diff --git a/plugins/syntax/NatSyntaxViaZ.v b/plugins/syntax/NatSyntaxViaZ.v deleted file mode 100644 index 8a4d8f236d..0000000000 --- a/plugins/syntax/NatSyntaxViaZ.v +++ /dev/null @@ -1,57 +0,0 @@ -Declare ML Module "numeral_notation_plugin". -Require Import BinNums. - -(** ** Parsing and Printing digit strings as type nat *) - -Fixpoint pos_pred_double x := - match x with - | xI p => xI (xO p) - | xO p => xI (pos_pred_double p) - | xH => xH - end. - -Definition nat_of_Z x := - match x with - | Z0 => Some O - | Zpos p => - let fix iter p a := - match p with - | xI p0 => a + iter p0 (a + a) - | xO p0 => iter p0 (a + a) - | xH => a - end - in - Some (iter p (S O)) - | Zneg p => None - end. - -Fixpoint pos_succ x := - match x with - | xI p => xO (pos_succ p) - | xO p => xI p - | xH => xO xH - end. - -Definition Z_succ x := - match x with - | Z0 => Zpos xH - | Zpos x => Zpos (pos_succ x) - | Zneg x => - match x with - | xI p => Zneg (xO p) - | xO p => Zneg (pos_pred_double p) - | xH => Z0 - end - end. - -Fixpoint Z_of_nat n := - match n with - | O => Z0 - | S p => Z_succ (Z_of_nat p) - end. - -(** The 1st conversion must either have type [Z->nat] or [Z->option nat]. - The 2nd one must either have type [nat->Z] or [nat->option Z]. *) - -Numeral Notation nat nat_of_Z Z_of_nat : nat_scope - (warning after 5000). -- cgit v1.2.3 From 006d2cd8c25dbcd787168c49e0ebfdf5dfc89c12 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 28 Feb 2017 10:54:33 +0100 Subject: Numeral Notation: allow parsing from/to Decimal.int or Decimal.uint This way, we could fully bypass bigint.ml. The previous mechanism of parsing/printing Z is kept for now. Currently, the conversion functions accepted by Numeral Notation foo may have the following types. for parsing: int -> foo int -> option foo uint -> foo uint -> option foo Z -> foo Z -> option foo for printing: foo -> int foo -> option int foo -> uint foo -> option uint foo -> Z foo -> option Z Notes: - The Declare ML Module is directly done in Prelude - When doing a Numeral Notation, having the Z datatype around isn't mandatory anymore (but the error messages suggest that it can still be used). - An option (abstract after ...) allows to keep large numbers in an abstract form such as (Nat.of_uint 123456) instead of reducing to (S (S (S ...))) and ending immediately with Stack Overflow. - After checking with Matthieu, there is now a explicit check and an error message in case of polymorphic inductive types --- plugins/syntax/g_numeral.ml4 | 386 ++++++++++++++++++++++++++++++++----------- theories/Init/Decimal.v | 6 + theories/Init/Prelude.v | 10 ++ 3 files changed, 305 insertions(+), 97 deletions(-) diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index b4c6a06ab0..cb99904b6e 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -20,15 +20,35 @@ open Misctypes (** * 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 for + our own ad-hoc [constr_of_glob] or from conversions such + as [coqint_of_rawnum]. +*) + let eval_constr (c : Constr.t) = let env = Global.env () in - let j = Arguments_renaming.rename_typing env c in + let j = Typeops.infer env c in let c'= Vnorm.cbv_vm env (Evd.from_env env) (EConstr.of_constr j.Environ.uj_val) (EConstr.of_constr j.Environ.uj_type) in EConstr.Unsafe.to_constr c' +(* For testing with "compute" instead of "vm_compute" : +let eval_constr (c : constr) = + let (sigma, env) = Lemmas.get_current_context () in + Tacred.compute env sigma c +*) + +let eval_constr_app c1 c2 = eval_constr (mkApp (c1,[| c2 |])) + exception NotANumber let warning_big_num ty = @@ -37,11 +57,103 @@ let warning_big_num ty = strbrk " (threshold may vary depending" ++ strbrk " on your system limits and on the command executed)." -type conversion_function = - | Direct of Constant.t - | Option of Constant.t +let warning_abstract_num ty f = + let (sigma, env) = Pfedit.get_current_context () in + strbrk "To avoid stack overflow, large numbers in " ++ + pr_reference ty ++ strbrk " are interpreted as applications of " ++ + Printer.pr_constr_env env sigma f ++ strbrk "." + +(** Comparing two raw numbers (base 10, big-endian, non-negative). + A bit nasty, but not critical : only used to decide when a + nat number is considered as large. *) + +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 *) + +type int_ty = + { uint : Names.inductive; + int : Names.inductive } + +(** 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's [Positive] and our internal bigint *) +(** ** Conversion between Coq [Z] and internal bigint *) + +type z_pos_ty = + { z_ty : Names.inductive; + pos_ty : Names.inductive } + +(** First, [positive] from/to bigint *) let rec pos_of_bigint posty n = match Bigint.div2_with_rest n with @@ -68,19 +180,9 @@ let rec bigint_of_pos c = match Constr.kind c with end | x -> raise NotANumber -(** Conversion between Coq's [Z] and our internal bigint *) - -type z_pos_ty = - { z_ty : Names.inductive; - pos_ty : Names.inductive } +(** Now, [Z] from/to bigint *) -let maybe_warn (thr,msg) n = - if Bigint.is_pos_or_zero n && not (Bigint.equal thr Bigint.zero) && - Bigint.less_than thr n - then Feedback.msg_warning msg - -let z_of_bigint { z_ty; pos_ty } warn n = - maybe_warn warn n; +let z_of_bigint { z_ty; pos_ty } n = if Bigint.equal n Bigint.zero then mkConstruct (z_ty, 1) (* Z0 *) else @@ -105,7 +207,7 @@ let bigint_of_z z = match Constr.kind z with end | _ -> raise NotANumber -(** The uinterp function below work at the level of [glob_constr] +(** 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. *) @@ -127,53 +229,91 @@ let rec glob_of_constr ?loc c = match Constr.kind c with | 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)) - | _ -> CErrors.anomaly (str "interp_big_int: unexpected constr") - -let interp_big_int zposty ty warn of_z ?loc bi = - match of_z with - | Direct f -> - let c = mkApp (mkConst f, [| z_of_bigint zposty warn bi |]) in - glob_of_constr ?loc (eval_constr c) - | Option f -> - let c = mkApp (mkConst f, [| z_of_bigint zposty warn bi |]) in - match Constr.kind (eval_constr c) with - | App (_Some, [| _; c |]) -> glob_of_constr ?loc c - | App (_None, [| _ |]) -> - CErrors.user_err ?loc - (str "Cannot interpret this number as a value of type " ++ - pr_reference ty) - | x -> CErrors.anomaly (str "interp_big_int: option expected") - -let uninterp_big_int to_z (Glob_term.AnyGlobConstr c) = - try - let t = constr_of_glob c in - match to_z with - | Direct g -> - let r = eval_constr (mkApp (mkConst g, [| t |])) in - Some (bigint_of_z r) - | Option g -> - let r = eval_constr (mkApp (mkConst g, [| t |])) in - match Constr.kind r with - | App (_Some, [| _; x |]) -> Some (bigint_of_z x) - | x -> None - with - | Type_errors.TypeError _ -> None (* cf. eval_constr *) - | NotANumber -> None (* cf constr_of_glob or bigint_of_z *) + | _ -> CErrors.anomaly (str "Numeral.interp: unexpected constr") + +let no_such_number ?loc ty = + CErrors.user_err ?loc + (str "Cannot interpret this number as a value of type " ++ + pr_reference ty) + +let interp_option ty ?loc c = + match Constr.kind c with + | App (_Some, [| _; c |]) -> glob_of_constr ?loc c + | App (_None, [| _ |]) -> no_such_number ?loc ty + | x -> CErrors.anomaly (str "Numeral.interp: option expected") + +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) + +type target_kind = Int | UInt | Z +type option_kind = Option | Direct +type conversion_kind = target_kind * option_kind + +type numnot_option = + | Nop + | Warning of raw_natural_number + | Abstract of raw_natural_number type numeral_notation_obj = { num_ty : Libnames.reference; - z_pos_ty : z_pos_ty; - of_z : conversion_function; - to_z : conversion_function; + z_pos_ty : z_pos_ty option; + int_ty : int_ty; + to_kind : conversion_kind; + to_ty : constr; + of_kind : conversion_kind; + of_ty : constr; scope : Notation_term.scope_name; constructors : Glob_term.glob_constr list; - warning : Bigint.bigint * Pp.t; + warning : numnot_option; path : Libnames.full_path } +let interp o ?loc n = + begin match o.warning with + | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 -> + Feedback.msg_warning (warning_big_num o.num_ty) + | _ -> () + end; + let c = match fst o.to_kind with + | Int -> coqint_of_rawnum o.int_ty n + | UInt when snd n -> coquint_of_rawnum o.int_ty.uint (fst n) + | UInt (* n <= 0 *) -> no_such_number ?loc o.num_ty + | Z -> z_of_bigint (Option.get o.z_pos_ty) (raw2big n) + in + match o.warning, snd o.to_kind with + | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 -> + Feedback.msg_warning (warning_abstract_num o.num_ty o.to_ty); + glob_of_constr ?loc (mkApp (o.to_ty,[|c|])) + | _ -> + let res = eval_constr_app o.to_ty c in + match snd o.to_kind with + | Direct -> glob_of_constr ?loc res + | Option -> interp_option o.num_ty ?loc res + +let uninterp o (Glob_term.AnyGlobConstr n) = + try + let c = eval_constr_app o.of_ty (constr_of_glob 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 _ -> None (* cf. eval_constr_app *) + | NotANumber -> None (* all other functions except big2raw *) + let load_numeral_notation _ (_, o) = - Notation.declare_numeral_interpreter o.scope (o.path, []) - (interp_big_int o.z_pos_ty o.num_ty o.warning o.of_z) - (o.constructors, uninterp_big_int o.to_z, true) + Notation.declare_rawnumeral_interpreter o.scope (o.path, []) + (interp o) + (o.constructors, uninterp o, true) let cache_numeral_notation o = load_numeral_notation 1 o @@ -193,19 +333,30 @@ let get_constructors ind = (Glob_term.GRef (ConstructRef (ind, j + 1), None))) mc) -let locate_ind s = - let q = qualid_of_string s in - try - match Nametab.locate q with - | IndRef i -> i - | _ -> raise Not_found - with Not_found -> Nametab.error_global_not_found (CAst.make q) +let q_z = qualid_of_string "Coq.Numbers.BinNums.Z" +let q_positive = qualid_of_string "Coq.Numbers.BinNums.positive" +let q_int = qualid_of_string "Coq.Init.Decimal.int" +let q_uint = qualid_of_string "Coq.Init.Decimal.uint" +let q_option = qualid_of_string "Coq.Init.Datatypes.option" + +let unsafe_locate_ind q = + match Nametab.locate q with + | IndRef i -> i + | _ -> raise Not_found -(** TODO: we should ensure that BinNums is loaded (or autoload it ?) *) +let locate_ind q = + try unsafe_locate_ind q + with Not_found -> Nametab.error_global_not_found (CAst.make q) let locate_z () = - { z_ty = locate_ind "Coq.Numbers.BinNums.Z"; - pos_ty = locate_ind "Coq.Numbers.BinNums.positive"; } + try + Some { z_ty = unsafe_locate_ind q_z; + pos_ty = unsafe_locate_ind q_positive } + with Not_found -> None + +let locate_int () = + { uint = locate_ind q_uint; + int = locate_ind q_int } let locate_globref r = let q = qualid_of_reference r in @@ -223,66 +374,107 @@ let has_type f ty = try let _ = Constrintern.interp_constr env sigma c in true with Pretype_errors.PretypeError _ -> false -let vernac_numeral_notation ty f g scope waft = +let vernac_numeral_notation ty f g scope opts = + let int_ty = locate_int () in let z_pos_ty = locate_z () in let tyc = locate_globref ty in - let fc = locate_constant f in - let gc = locate_constant g in - let cty = mkRefC (CAst.(make (Qualid (qualid_of_reference ty).v))) - in + let to_ty = mkConst (locate_constant f) in + let of_ty = mkConst (locate_constant g) in + let cty = mkRefC ty in let app x y = mkAppC (x,[y]) in - let cref s = mkIdentC (Id.of_string s) in + let cref q = mkRefC (CAst.make (Qualid q)) in let arrow x y = mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) in + let cZ = cref q_z in + let cint = cref q_int in + let cuint = cref q_uint in + let coption = cref q_option in + let opt r = app coption r in (* Check that [ty] is an inductive type *) let constructors = match tyc with - | IndRef ind -> get_constructors ind + | IndRef ind when not (Global.is_polymorphic tyc) -> + get_constructors ind + | IndRef _ -> + CErrors.user_err + (str "The inductive type " ++ pr_reference ty ++ + str " cannot be polymorphic here for the moment") | ConstRef _ | ConstructRef _ | VarRef _ -> CErrors.user_err (pr_reference ty ++ str " is not an inductive type") in - (* Is "f" of type "Z -> ty" or "Z -> option ty" ? *) - let of_z = - if has_type f (arrow (cref "Z") cty) then - Direct fc - else if has_type f (arrow (cref "Z") (app (cref "option") cty)) then - Option fc + (* Check the type of f *) + let to_kind = + if has_type f (arrow cint cty) then Int, Direct + else if has_type f (arrow cint (opt cty)) then Int, Option + else if has_type f (arrow cuint cty) then UInt, Direct + else if has_type f (arrow cuint (opt cty)) then UInt, Option + else if Option.is_empty z_pos_ty then + CErrors.user_err + (pr_reference f ++ str " should goes from Decimal.int or uint to " ++ + pr_reference ty ++ str " or (option " ++ pr_reference ty ++ + str ")." ++ fnl () ++ + str "Instead of int, the type Z could also be used (load it first).") + else if has_type f (arrow cZ cty) then Z, Direct + else if has_type f (arrow cZ (opt cty)) then Z, Option else CErrors.user_err - (pr_reference f ++ str " should goes from Z to " ++ + (pr_reference f ++ str " should goes from Decimal.int or uint or Z to " + ++ pr_reference ty ++ str " or (option " ++ pr_reference ty ++ str ")") in - (* Is "g" of type "ty -> Z" or "ty -> option Z" ? *) - let to_z = - if has_type g (arrow cty (cref "Z")) then - Direct gc - else if has_type g (arrow cty (app (cref "option") (cref "Z"))) then - Option gc + (* Check the type of g *) + let of_kind = + if has_type g (arrow cty cint) then Int, Direct + else if has_type g (arrow cty (opt cint)) then Int, Option + else if has_type g (arrow cty cuint) then UInt, Direct + else if has_type g (arrow cty (opt cuint)) then UInt, Option + else if Option.is_empty z_pos_ty then + CErrors.user_err + (pr_reference g ++ str " should goes from " ++ + pr_reference ty ++ + str " to Decimal.int or (option int) or uint." ++ fnl () ++ + str "Instead of int, the type Z could also be used (load it first).") + else if has_type g (arrow cty cZ) then Z, Direct + else if has_type g (arrow cty (opt cZ)) then Z, Option else CErrors.user_err (pr_reference g ++ str " should goes from " ++ - pr_reference ty ++ str " to Z or (option Z)") + pr_reference ty ++ + str " to Decimal.int or (option int) or uint or Z or (option Z)") in Lib.add_anonymous_leaf (inNumeralNotation { num_ty = ty; z_pos_ty; - of_z; - to_z; + int_ty; + to_kind; + to_ty; + of_kind; + of_ty; scope; constructors; - warning = (Bigint.of_int waft, warning_big_num ty); + warning = opts; path = Nametab.path_of_global tyc }) +open Ltac_plugin open Stdarg +open Pcoq.Prim + +let pr_numnot_option _ _ _ = function + | Nop -> mt () + | Warning n -> str "(warning after " ++ str n ++ str ")" + | Abstract n -> str "(abstract after " ++ str n ++ str ")" + +ARGUMENT EXTEND numnotoption + PRINTED BY pr_numnot_option +| [ ] -> [ Nop ] +| [ "(" "warning" "after" bigint(waft) ")" ] -> [ Warning waft ] +| [ "(" "abstract" "after" bigint(n) ")" ] -> [ Abstract n ] +END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" - ident(sc) ] -> - [ let waft = 0 in - vernac_numeral_notation ty f g (Id.to_string sc) waft ] - | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" - ident(sc) "(" "warning" "after" int(waft) ")" ] -> - [ vernac_numeral_notation ty f g (Id.to_string sc) waft ] + ident(sc) numnotoption(o) ] -> + [ vernac_numeral_notation ty f g (Id.to_string sc) o ] END diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 57163b1b07..34b4e75814 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -161,3 +161,9 @@ with succ_double d := end. End Little. + +(** Pseudo-conversion functions used when declaring + Numeral Notations on [uint] and [int]. *) + +Definition uint_of_uint (i:uint) := i. +Definition int_of_int (i:int) := i. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 390ff5e240..f99a6a7c60 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -26,5 +26,15 @@ Require Export Coq.Init.Tauto. *) Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". +Declare ML Module "numeral_notation_plugin". + +(* Parsing / printing of decimal numbers *) +Arguments Nat.of_uint d%uint_scope. +Arguments Nat.of_int d%int_scope. +Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint + : uint_scope. +Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int + : int_scope. + (* Default substrings not considered by queries like SearchAbout *) Add Search Blacklist "_subproof" "_subterm" "Private_". -- cgit v1.2.3 From 24ccc118ccfb4c1223cd37bd43c9d26a77851176 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 15 Mar 2017 03:11:23 +0100 Subject: Numeral Notation for nat This parsing/printing method for nat should be just as fast as the previous dedicated code. Moreover, we could now parse large literals as nat numbers, by leaving them in a half-abstract form such as (Nat.of_uint 123456). This form is convertible to the closed (S (S (S ...))) form, so it shouldn't be a big deal for compatibility, except for if some Ltac stuff relies on (S ...) to be present after parsing. Of course, forcing the computation of a (Nat.of_uint ....) may take a while or raise a Stack Overflow. --- doc/stdlib/index-list.html.template | 1 + theories/Init/Datatypes.v | 1 - theories/Init/Nat.v | 4 +++ theories/Init/Peano.v | 1 + theories/Init/Prelude.v | 4 ++- theories/NArith/BinNatDef.v | 6 ++++ theories/Numbers/AltBinNotations.v | 68 +++++++++++++++++++++++++++++++++++++ theories/Numbers/BinNums.v | 16 ++++----- theories/PArith/BinPosDef.v | 10 ++++-- theories/ZArith/BinIntDef.v | 12 +++++-- 10 files changed, 105 insertions(+), 18 deletions(-) create mode 100644 theories/Numbers/AltBinNotations.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index f448248468..0fa42cadad 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -226,6 +226,7 @@ through the Require Import command.

theories/Numbers/BinNums.v theories/Numbers/NumPrelude.v theories/Numbers/NaryFunctions.v + theories/Numbers/AltBinNotations.v theories/Numbers/DecimalFacts.v theories/Numbers/DecimalNat.v theories/Numbers/DecimalPos.v diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 05b741f0ac..1e6843d511 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -12,7 +12,6 @@ Set Implicit Arguments. Require Import Notations. Require Import Logic. -Declare ML Module "nat_syntax_plugin". (********************************************************************) (** * Datatypes with zero and one element *) diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v index ad1bc717c4..eb4ba0e5e6 100644 --- a/theories/Init/Nat.v +++ b/theories/Init/Nat.v @@ -24,6 +24,10 @@ Definition t := nat. (** ** Constants *) +Local Notation "0" := O. +Local Notation "1" := (S O). +Local Notation "2" := (S (S O)). + Definition zero := 0. Definition one := 1. Definition two := 2. diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index d5322d0945..65e5e76a22 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -31,6 +31,7 @@ Require Import Logic. Require Coq.Init.Nat. Open Scope nat_scope. +Local Notation "0" := O. Definition eq_S := f_equal S. Definition f_equal_nat := f_equal (A:=nat). diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index f99a6a7c60..e8997d30b8 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -21,7 +21,6 @@ Require Export Coq.Init.Tactics. Require Export Coq.Init.Tauto. (* Some initially available plugins. See also: - ltac_plugin (in Notations) - - nat_syntax_plugin (in Datatypes) - tauto_plugin (in Tauto). *) Declare ML Module "cc_plugin". @@ -36,5 +35,8 @@ Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : int_scope. +(* Parsing / printing of [nat] numbers *) +Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000). + (* Default substrings not considered by queries like SearchAbout *) Add Search Blacklist "_subproof" "_subterm" "Private_". diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 5de75537cb..8bbecf9acb 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -13,6 +13,10 @@ Require Import BinPos. Local Open Scope N_scope. +Local Notation "0" := N0. +Local Notation "1" := (Npos 1). +Local Notation "2" := (Npos 2). + (**********************************************************************) (** * Binary natural numbers, definitions of operations *) (**********************************************************************) @@ -399,3 +403,5 @@ Definition to_uint n := Definition to_int n := Decimal.Pos (to_uint n). End N. + +Numeral Notation N N.of_uint N.to_uint : N_scope. diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v new file mode 100644 index 0000000000..595934ad89 --- /dev/null +++ b/theories/Numbers/AltBinNotations.v @@ -0,0 +1,68 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Some p + | _ => None + end. + +Definition pos_to_z p := Zpos p. + +Numeral Notation positive pos_of_z pos_to_z : positive_scope. + +(** [N] *) + +Definition n_of_z z := + match z with + | Z0 => Some N0 + | Zpos p => Some (Npos p) + | Zneg _ => None + end. + +Definition n_to_z n := + match n with + | N0 => Z0 + | Npos p => Zpos p + end. + +Numeral Notation N n_of_z n_to_z : N_scope. + +(** [Z] *) + +Definition z_of_z (z:Z) := z. + +Numeral Notation Z z_of_z z_of_z : Z_scope. diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index d5eb4f2681..3ba9d1f5ed 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -12,15 +12,11 @@ Set Implicit Arguments. -Declare ML Module "positive_syntax_plugin". -Declare ML Module "n_syntax_plugin". -Declare ML Module "z_syntax_plugin". - (** [positive] is a datatype representing the strictly positive integers in a binary way. Starting from 1 (represented by [xH]), one can add a new least significant digit via [xO] (digit 0) or [xI] (digit 1). - Numbers in [positive] can also be denoted using a decimal notation; - e.g. [6%positive] abbreviates [xO (xI xH)] *) + Numbers in [positive] will also be denoted using a decimal notation; + e.g. [6%positive] will abbreviate [xO (xI xH)] *) Inductive positive : Set := | xI : positive -> positive @@ -34,8 +30,8 @@ Arguments xI _%positive. (** [N] is a datatype representing natural numbers in a binary way, by extending the [positive] datatype with a zero. - Numbers in [N] can also be denoted using a decimal notation; - e.g. [6%N] abbreviates [Npos (xO (xI xH))] *) + Numbers in [N] will also be denoted using a decimal notation; + e.g. [6%N] will abbreviate [Npos (xO (xI xH))] *) Inductive N : Set := | N0 : N @@ -49,8 +45,8 @@ Arguments Npos _%positive. An integer is either zero or a strictly positive number (coded as a [positive]) or a strictly negative number (whose opposite is stored as a [positive] value). - Numbers in [Z] can also be denoted using a decimal notation; - e.g. [(-6)%Z] abbreviates [Zneg (xO (xI xH))] *) + Numbers in [Z] will also be denoted using a decimal notation; + e.g. [(-6)%Z] will abbreviate [Zneg (xO (xI xH))] *) Inductive Z : Set := | Z0 : Z diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 070314746a..39b609e9dd 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -26,6 +26,8 @@ Require Export BinNums. for the number 6 (which is 110 in binary notation). *) +Local Notation "1" := xH. + Notation "p ~ 1" := (xI p) (at level 7, left associativity, format "p '~' '1'") : positive_scope. Notation "p ~ 0" := (xO p) @@ -325,14 +327,14 @@ Definition sqrtrem_step (f g:positive->positive) p := let r' := g (f r) in if s' <=? r' then (s~1, sub_mask r' s') else (s~0, IsPos r') - | (s,_) => (s~0, sub_mask (g (f 1)) 4) + | (s,_) => (s~0, sub_mask (g (f 1)) 1~0~0) end. Fixpoint sqrtrem p : positive * mask := match p with | 1 => (1,IsNul) - | 2 => (1,IsPos 1) - | 3 => (1,IsPos 2) + | 1~0 => (1,IsPos 1) + | 1~1 => (1,IsPos 1~0) | p~0~0 => sqrtrem_step xO xO (sqrtrem p) | p~0~1 => sqrtrem_step xO xI (sqrtrem p) | p~1~0 => sqrtrem_step xI xO (sqrtrem p) @@ -615,3 +617,5 @@ Definition to_uint p := Decimal.rev (to_little_uint p). Definition to_int n := Decimal.Pos (to_uint n). End Pos. + +Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index db4de0b90c..8abcd15700 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -14,6 +14,10 @@ Require Import BinPos BinNat. Local Open Scope Z_scope. +Local Notation "0" := Z0. +Local Notation "1" := (Zpos 1). +Local Notation "2" := (Zpos 2). + (***********************************************************) (** * Binary Integers, Definitions of Operations *) (***********************************************************) @@ -53,7 +57,7 @@ Definition succ_double x := Definition pred_double x := match x with - | 0 => -1 + | 0 => neg 1 | neg p => neg p~1 | pos p => pos (Pos.pred_double p) end. @@ -104,7 +108,7 @@ Definition succ x := x + 1. (** ** Predecessor *) -Definition pred x := x + -1. +Definition pred x := x + neg 1. (** ** Subtraction *) @@ -171,7 +175,7 @@ Definition sgn z := match z with | 0 => 0 | pos p => 1 - | neg p => -1 + | neg p => neg 1 end. (** Boolean equality and comparisons *) @@ -636,3 +640,5 @@ Definition lxor a b := end. End Z. + +Numeral Notation Z Z.of_int Z.to_int : Z_scope. -- cgit v1.2.3 From ec0ad20de8daf2ad9f3237de92a745247db845f5 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 21 Mar 2017 16:13:24 +0100 Subject: remove legacy syntax plugins subsumed by Numeral Notation --- Makefile.common | 8 +- plugins/syntax/n_syntax.ml | 88 ---------------------- plugins/syntax/n_syntax_plugin.mlpack | 1 - plugins/syntax/nat_syntax.ml | 95 ------------------------ plugins/syntax/nat_syntax_plugin.mlpack | 1 - plugins/syntax/positive_syntax.ml | 107 --------------------------- plugins/syntax/positive_syntax_plugin.mlpack | 1 - plugins/syntax/z_syntax.ml | 84 --------------------- plugins/syntax/z_syntax_plugin.mlpack | 1 - 9 files changed, 3 insertions(+), 383 deletions(-) delete mode 100644 plugins/syntax/n_syntax.ml delete mode 100644 plugins/syntax/n_syntax_plugin.mlpack delete mode 100644 plugins/syntax/nat_syntax.ml delete mode 100644 plugins/syntax/nat_syntax_plugin.mlpack delete mode 100644 plugins/syntax/positive_syntax.ml delete mode 100644 plugins/syntax/positive_syntax_plugin.mlpack delete mode 100644 plugins/syntax/z_syntax.ml delete mode 100644 plugins/syntax/z_syntax_plugin.mlpack diff --git a/Makefile.common b/Makefile.common index 4f09fb376a..09457ced7b 100644 --- a/Makefile.common +++ b/Makefile.common @@ -140,10 +140,8 @@ FOCMO:=plugins/firstorder/ground_plugin.cmo CCCMO:=plugins/cc/cc_plugin.cmo BTAUTOCMO:=plugins/btauto/btauto_plugin.cmo RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo -NATSYNTAXCMO:=plugins/syntax/nat_syntax_plugin.cmo -OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \ - positive_syntax_plugin.cmo n_syntax_plugin.cmo \ - z_syntax_plugin.cmo r_syntax_plugin.cmo \ +SYNTAXCMO:=$(addprefix plugins/syntax/, \ + r_syntax_plugin.cmo \ int31_syntax_plugin.cmo \ ascii_syntax_plugin.cmo \ string_syntax_plugin.cmo \ @@ -157,7 +155,7 @@ PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \ $(QUOTECMO) $(RINGCMO) \ $(EXTRACTIONCMO) \ $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \ - $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \ + $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \ $(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) ifeq ($(HASNATDYNLINK)-$(BEST),false-opt) diff --git a/plugins/syntax/n_syntax.ml b/plugins/syntax/n_syntax.ml deleted file mode 100644 index 29b88b1cb3..0000000000 --- a/plugins/syntax/n_syntax.ml +++ /dev/null @@ -1,88 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* bignat_of_pos a - | GRef (a,_) when GlobRef.equal a glob_N0 -> Bigint.zero - | _ -> raise Non_closed_number - ) n - -let uninterp_n (AnyGlobConstr p) = - try Some (bignat_of_n p) - with Non_closed_number -> None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for N *) - -open Notation - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -let _ = - let scope = "N_scope" in - register_bignumeral_interpretation scope (n_of_int,uninterp_n); - at_declare_ml_module enable_prim_token_interpretation - { pt_scope = scope; - pt_uid = scope; - pt_required = (n_path,binnums); - pt_refs = [glob_N0; glob_Npos]; - pt_in_match = true } diff --git a/plugins/syntax/n_syntax_plugin.mlpack b/plugins/syntax/n_syntax_plugin.mlpack deleted file mode 100644 index 4c56645f07..0000000000 --- a/plugins/syntax/n_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -N_syntax diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml deleted file mode 100644 index 85cb49586d..0000000000 --- a/plugins/syntax/nat_syntax.ml +++ /dev/null @@ -1,95 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* > *) - -let threshold = of_int 5000 - -let warn_large_nat = - CWarnings.create ~name:"large-nat" ~category:"numbers" - (fun () -> strbrk "Stack overflow or segmentation fault happens when " ++ - strbrk "working with large numbers in nat (observed threshold " ++ - strbrk "may vary from 5000 to 70000 depending on your system " ++ - strbrk "limits and on the command executed).") - -let nat_of_int ?loc n = - if is_pos_or_zero n then begin - if less_than threshold n then warn_large_nat (); - let ref_O = DAst.make ?loc @@ GRef (glob_O, None) in - let ref_S = DAst.make ?loc @@ GRef (glob_S, None) in - let rec mk_nat acc n = - if n <> zero then - mk_nat (DAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) - else - acc - in - mk_nat ref_O n - end - else - user_err ?loc ~hdr:"nat_of_int" - (str "Cannot interpret a negative number as a number of type nat") - -(************************************************************************) -(* Printing via scopes *) - -exception Non_closed_number - -let rec int_of_nat x = DAst.with_val (function - | GApp (r, [a]) -> - begin match DAst.get r with - | GRef (s,_) when GlobRef.equal s glob_S -> add_1 (int_of_nat a) - | _ -> raise Non_closed_number - end - | GRef (z,_) when GlobRef.equal z glob_O -> zero - | _ -> raise Non_closed_number - ) x - -let uninterp_nat (AnyGlobConstr p) = - try - Some (int_of_nat p) - with - Non_closed_number -> None - -(************************************************************************) -(* Declare the primitive parsers and printers *) - -open Notation - -let nat_scope = "nat_scope" - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -let _ = - register_bignumeral_interpretation nat_scope (nat_of_int,uninterp_nat); - at_declare_ml_module enable_prim_token_interpretation - { pt_scope = nat_scope; - pt_uid = nat_scope; - pt_required = (nat_path,datatypes_module_name); - pt_refs = [glob_S; glob_O]; - pt_in_match = true } diff --git a/plugins/syntax/nat_syntax_plugin.mlpack b/plugins/syntax/nat_syntax_plugin.mlpack deleted file mode 100644 index 39bdd62f47..0000000000 --- a/plugins/syntax/nat_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Nat_syntax diff --git a/plugins/syntax/positive_syntax.ml b/plugins/syntax/positive_syntax.ml deleted file mode 100644 index 6fce4de9ef..0000000000 --- a/plugins/syntax/positive_syntax.ml +++ /dev/null @@ -1,107 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* DAst.make ?loc @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q]) - | (q,true) -> ref_xH - in - pos_of x - -let error_non_positive ?loc = - user_err ?loc ~hdr:"interp_positive" - (str "Only strictly positive numbers in type \"positive\".") - -let interp_positive ?loc n = - if is_strictly_pos n then pos_of_bignat ?loc n - else error_non_positive ?loc - -(**********************************************************************) -(* Printing positive via scopes *) -(**********************************************************************) - -let is_gr c gr = match DAst.get c with -| GRef (r, _) -> GlobRef.equal r gr -| _ -> false - -let rec bignat_of_pos x = DAst.with_val (function - | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) - | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) - | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one - | _ -> raise Non_closed_number - ) x - -let uninterp_positive (AnyGlobConstr p) = - try - Some (bignat_of_pos p) - with Non_closed_number -> - None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for positive *) -(************************************************************************) - -open Notation - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -let _ = - let scope = "positive_scope" in - register_bignumeral_interpretation scope (interp_positive,uninterp_positive); - at_declare_ml_module enable_prim_token_interpretation - { pt_scope = scope; - pt_uid = scope; - pt_required = (positive_path,binnums); - pt_refs = [glob_xI; glob_xO; glob_xH]; - pt_in_match = true } diff --git a/plugins/syntax/positive_syntax_plugin.mlpack b/plugins/syntax/positive_syntax_plugin.mlpack deleted file mode 100644 index ac8f3c425c..0000000000 --- a/plugins/syntax/positive_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Positive_syntax diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml deleted file mode 100644 index 72e1321eab..0000000000 --- a/plugins/syntax/z_syntax.ml +++ /dev/null @@ -1,84 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* bignat_of_pos a - | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) - | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero - | _ -> raise Non_closed_number - ) z - -let uninterp_z (AnyGlobConstr p) = - try - Some (bigint_of_z p) - with Non_closed_number -> None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for Z *) - -open Notation - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -let _ = - let scope = "Z_scope" in - register_bignumeral_interpretation scope (z_of_int,uninterp_z); - at_declare_ml_module enable_prim_token_interpretation - { pt_scope = scope; - pt_uid = scope; - pt_required = (z_path,binnums); - pt_refs = [glob_ZERO; glob_POS; glob_NEG]; - pt_in_match = true } diff --git a/plugins/syntax/z_syntax_plugin.mlpack b/plugins/syntax/z_syntax_plugin.mlpack deleted file mode 100644 index 411260c04c..0000000000 --- a/plugins/syntax/z_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Z_syntax -- cgit v1.2.3 From 1e49dad4c4ea721a0844d9553e84aed90777f46d Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 21 Mar 2017 18:56:18 +0100 Subject: Numeral Notation: some documentation in the refman --- doc/sphinx/user-extensions/syntax-extensions.rst | 44 ++++++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 5089a1b3e3..0293a92fbb 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1372,6 +1372,50 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. + +Numeral notations +----------------- + +Starting with version 8.9, the following command allows to customize +the way numeral literals are parsed and printed: + +.. cmd:: Numeral Notation @ty @pa @pr : @scope. + +In the previous line, `ty` should be the name of an inductive type, +while `pa` and `pr` should be the names of two parsing and printing +functions. +The parsing function `pa` should have one of the following types: + + * :g:`Decimal.int -> ty` + * :g:`Decimal.int -> option ty` + * :g:`Decimal.uint -> ty` + * :g:`Decimal.uint -> option ty` + * :g:`Z -> ty` + * :g:`Z -> option ty` + +And the printing function `pr` should have one of the following types: + + * :g:`ty -> Decimal.int` + * :g:`ty -> option Decimal.int` + * :g:`ty -> Decimal.uint` + * :g:`ty -> option Decimal.uint` + * :g:`ty -> Z` + * :g:`ty -> option Z` + +.. cmdv:: Numeral Notation @ty @pa @pr : @scope (warning after @n). + +When a literal larger than `n` is parsed, a warning message about +possible stack overflow will be displayed. + +.. cmdv:: Numeral Notation @ty @pa @pr : @scope (abstract after @n). + +When a literal `m` larger than `n` is parsed, the result will be +:g:`(pa m)`, without reduction of this application to a normal form. +Here `m` will be a ``Decimal.int`` or ``Decimal.uint`` or ``Z``, +depending on the type of the parsing function `pa`. This allows a more +compact representation of literals in types such as ``nat``, and +limits parse failures due to stack overflow. + .. _TacticNotation: Tactic Notations -- cgit v1.2.3 From 0ad2b76facd787f4b9b6f604f45199e549fe8f9c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 1 Jun 2017 17:45:01 -0400 Subject: Fix grammar ``` git grep --name-only 'should goes' | xargs sed s'/should goes/should go/g' -i ``` --- plugins/syntax/g_numeral.ml4 | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index cb99904b6e..78461fe87d 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -411,7 +411,7 @@ let vernac_numeral_notation ty f g scope opts = else if has_type f (arrow cuint (opt cty)) then UInt, Option else if Option.is_empty z_pos_ty then CErrors.user_err - (pr_reference f ++ str " should goes from Decimal.int or uint to " ++ + (pr_reference f ++ str " should go from Decimal.int or uint to " ++ pr_reference ty ++ str " or (option " ++ pr_reference ty ++ str ")." ++ fnl () ++ str "Instead of int, the type Z could also be used (load it first).") @@ -419,7 +419,7 @@ let vernac_numeral_notation ty f g scope opts = else if has_type f (arrow cZ (opt cty)) then Z, Option else CErrors.user_err - (pr_reference f ++ str " should goes from Decimal.int or uint or Z to " + (pr_reference f ++ str " should go from Decimal.int or uint or Z to " ++ pr_reference ty ++ str " or (option " ++ pr_reference ty ++ str ")") in @@ -431,7 +431,7 @@ let vernac_numeral_notation ty f g scope opts = else if has_type g (arrow cty (opt cuint)) then UInt, Option else if Option.is_empty z_pos_ty then CErrors.user_err - (pr_reference g ++ str " should goes from " ++ + (pr_reference g ++ str " should go from " ++ pr_reference ty ++ str " to Decimal.int or (option int) or uint." ++ fnl () ++ str "Instead of int, the type Z could also be used (load it first).") @@ -439,7 +439,7 @@ let vernac_numeral_notation ty f g scope opts = else if has_type g (arrow cty (opt cZ)) then Z, Option else CErrors.user_err - (pr_reference g ++ str " should goes from " ++ + (pr_reference g ++ str " should go from " ++ pr_reference ty ++ str " to Decimal.int or (option int) or uint or Z or (option Z)") in -- cgit v1.2.3 From 35916e2a3a9ccae1ece8ce64ddf55faa50ac88b6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 1 Jun 2017 18:21:29 -0400 Subject: Error on polymorphic conversions for numeral notations --- plugins/syntax/g_numeral.ml4 | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index 78461fe87d..9edb7c3351 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -405,7 +405,10 @@ let vernac_numeral_notation ty f g scope opts = in (* Check the type of f *) let to_kind = - if has_type f (arrow cint cty) then Int, Direct + if Global.is_polymorphic (Nametab.global f) then + CErrors.user_err + (pr_reference f ++ str " cannot be polymorphic for the moment") + else if has_type f (arrow cint cty) then Int, Direct else if has_type f (arrow cint (opt cty)) then Int, Option else if has_type f (arrow cuint cty) then UInt, Direct else if has_type f (arrow cuint (opt cty)) then UInt, Option @@ -425,7 +428,10 @@ let vernac_numeral_notation ty f g scope opts = in (* Check the type of g *) let of_kind = - if has_type g (arrow cty cint) then Int, Direct + if Global.is_polymorphic (Nametab.global g) then + CErrors.user_err + (pr_reference g ++ str " cannot be polymorphic for the moment") + else if has_type g (arrow cty cint) then Int, Direct else if has_type g (arrow cty (opt cint)) then Int, Option else if has_type g (arrow cty cuint) then UInt, Direct else if has_type g (arrow cty (opt cuint)) then UInt, Option -- cgit v1.2.3 From e539db48ab064dc0c10c5ebeb043372c840497c2 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 9 Mar 2018 15:23:17 +0100 Subject: Numeral Notation: minor text improvements suggested by J. Gross --- doc/sphinx/user-extensions/syntax-extensions.rst | 2 +- plugins/syntax/g_numeral.ml4 | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 0293a92fbb..e947fd891b 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1376,7 +1376,7 @@ Abbreviations Numeral notations ----------------- -Starting with version 8.9, the following command allows to customize +Starting with version 8.9, the following command allows the user to customize the way numeral literals are parsed and printed: .. cmd:: Numeral Notation @ty @pa @pr : @scope. diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index 9edb7c3351..41d02adbe1 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -27,7 +27,7 @@ open Misctypes that starts with the right constructor, but might be partially applied. - At least [c] is known to be evar-free, since it comes for + 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]. *) @@ -65,7 +65,7 @@ let warning_abstract_num ty f = (** Comparing two raw numbers (base 10, big-endian, non-negative). A bit nasty, but not critical : only used to decide when a - nat number is considered as large. *) + number is considered as large (see warnings above). *) exception Comp of int -- cgit v1.2.3 From 3ad9d3eea1fc090d5dd67e43b3f5ad472afc31d6 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 9 Mar 2018 15:50:59 +0100 Subject: Numeral Notation: use the modern warning infrastructure --- plugins/syntax/g_numeral.ml4 | 30 +++++++++++++++++------------- 1 file changed, 17 insertions(+), 13 deletions(-) diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index 41d02adbe1..0f34c73576 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -51,17 +51,21 @@ let eval_constr_app c1 c2 = eval_constr (mkApp (c1,[| c2 |])) exception NotANumber -let warning_big_num ty = - strbrk "Stack overflow or segmentation fault happens when " ++ - strbrk "working with large numbers in " ++ pr_reference ty ++ - strbrk " (threshold may vary depending" ++ - strbrk " on your system limits and on the command executed)." - -let warning_abstract_num ty f = - let (sigma, env) = Pfedit.get_current_context () in - strbrk "To avoid stack overflow, large numbers in " ++ - pr_reference ty ++ strbrk " are interpreted as applications of " ++ - Printer.pr_constr_env env sigma f ++ strbrk "." +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_reference 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) -> + let (sigma, env) = Pfedit.get_current_context () in + strbrk "To avoid stack overflow, large numbers in " ++ + pr_reference ty ++ strbrk " are interpreted as applications of " ++ + Printer.pr_constr_env env sigma f ++ strbrk ".") (** Comparing two raw numbers (base 10, big-endian, non-negative). A bit nasty, but not critical : only used to decide when a @@ -279,7 +283,7 @@ type numeral_notation_obj = let interp o ?loc n = begin match o.warning with | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 -> - Feedback.msg_warning (warning_big_num o.num_ty) + warn_large_num o.num_ty | _ -> () end; let c = match fst o.to_kind with @@ -290,7 +294,7 @@ let interp o ?loc n = in match o.warning, snd o.to_kind with | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 -> - Feedback.msg_warning (warning_abstract_num o.num_ty o.to_ty); + warn_abstract_large_num (o.num_ty,o.to_ty); glob_of_constr ?loc (mkApp (o.to_ty,[|c|])) | _ -> let res = eval_constr_app o.to_ty c in -- cgit v1.2.3 From 377188d7bfd27518e6ab47d5017907b1f527a7dd Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 12 Mar 2018 15:45:02 +0100 Subject: Numeral Notation + test-suite : fix 3 tests using Datatypes.v but not Prelude.v Earlier, the nat_syntax_plugin was loaded as soon as Datatypes.v. This would now implies to make Datatypes.v depends on Decimal.v. Instead, we postpone the Numeral Notation for nat until Prelude.v, and we adapt those three tests that happen to live strictly between Datatypes and Prelude. --- test-suite/bugs/closed/4527.v | 8 +++++--- test-suite/bugs/closed/4533.v | 11 +++++++---- test-suite/bugs/closed/4544.v | 3 ++- 3 files changed, 14 insertions(+), 8 deletions(-) diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index 117d6523a8..f8cedfff6e 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -23,7 +23,9 @@ Module Export Datatypes. Set Implicit Arguments. Notation nat := Coq.Init.Datatypes.nat. +Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. +Notation two := (S (S O)). Record prod (A B : Type) := pair { fst : A ; snd : B }. @@ -159,7 +161,7 @@ End Adjointify. (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), @@ -220,12 +222,12 @@ Section ORecursion. Definition O_indpaths {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o to O P == h o to O P) : g == h - := (fst (snd (extendable_to_O O 2) g h) p).1. + := (fst (snd (extendable_to_O O two) g h) p).1. Definition O_indpaths_beta {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P) : O_indpaths g h p (to O P x) = p x - := (fst (snd (extendable_to_O O 2) g h) p).2 x. + := (fst (snd (extendable_to_O O two) g h) p).2 x. End ORecursion. diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v index c3e0da1117..fd2380a070 100644 --- a/test-suite/bugs/closed/4533.v +++ b/test-suite/bugs/closed/4533.v @@ -17,7 +17,10 @@ Notation "A -> B" := (forall (_ : A), B) : type_scope. Module Export Datatypes. Set Implicit Arguments. Notation nat := Coq.Init.Datatypes.nat. + Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. + Notation one := (S O). + Notation two := (S one). Record prod (A B : Type) := pair { fst : A ; snd : B }. Notation "x * y" := (prod x y) : type_scope. Delimit Scope nat_scope with nat. @@ -109,7 +112,7 @@ Fixpoint ExtendableAlong@{i j k l} (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), @@ -160,17 +163,17 @@ Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses). Definition O_rec {P Q : Type} {Q_inO : In O Q} (f : P -> Q) : O P -> Q - := (fst (extendable_to_O O 1%nat) f).1. + := (fst (extendable_to_O O one) f).1. Definition O_rec_beta {P Q : Type} {Q_inO : In O Q} (f : P -> Q) (x : P) : O_rec f (to O P x) = f x - := (fst (extendable_to_O O 1%nat) f).2 x. + := (fst (extendable_to_O O one) f).2 x. Definition O_indpaths {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o to O P == h o to O P) : g == h - := (fst (snd (extendable_to_O O 2) g h) p).1. + := (fst (snd (extendable_to_O O two) g h) p).1. End ORecursion. diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index 4ad53bc629..13c47edc8f 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -19,6 +19,7 @@ Inductive sum (A B : Type) : Type := | inl : A -> sum A B | inr : B -> sum A B. Notation nat := Coq.Init.Datatypes.nat. +Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. Notation "x + y" := (sum x y) : type_scope. @@ -449,7 +450,7 @@ Section Extensions. (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), -- cgit v1.2.3 From 44638cda2f8f7461506a6e5a9a2edf860971f96c Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 12 Mar 2018 17:21:04 +0100 Subject: Decimal: scope name changed dec_(u)int_scope This avoid a clash with int_scope in ssreflect's ssrint.v --- theories/Init/Decimal.v | 8 ++++---- theories/Init/Prelude.v | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 34b4e75814..1ff00ec11c 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -42,10 +42,10 @@ Notation zero := (D0 Nil). Inductive int := Pos (d:uint) | Neg (d:uint). -Delimit Scope uint_scope with uint. -Bind Scope uint_scope with uint. -Delimit Scope int_scope with int. -Bind Scope int_scope with int. +Delimit Scope dec_uint_scope with uint. +Bind Scope dec_uint_scope with uint. +Delimit Scope dec_int_scope with int. +Bind Scope dec_int_scope with int. (** This representation favors simplicity over canonicity. For normalizing numbers, we need to remove head zero digits, diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index e8997d30b8..6d98bcb34a 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -28,12 +28,12 @@ Declare ML Module "ground_plugin". Declare ML Module "numeral_notation_plugin". (* Parsing / printing of decimal numbers *) -Arguments Nat.of_uint d%uint_scope. -Arguments Nat.of_int d%int_scope. +Arguments Nat.of_uint d%dec_uint_scope. +Arguments Nat.of_int d%dec_int_scope. Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint - : uint_scope. + : dec_uint_scope. Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int - : int_scope. + : dec_int_scope. (* Parsing / printing of [nat] numbers *) Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000). -- cgit v1.2.3 From 3c7c0bb08d406d4addfc0ac68dce45bf7c5cb7e9 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 11 Apr 2018 09:58:56 +0200 Subject: WIP: adapt Numeral Notation to synchronized prim notations --- plugins/syntax/g_numeral.ml4 | 57 ++++++++++++++++++----------------- test-suite/interactive/PrimNotation.v | 2 +- 2 files changed, 30 insertions(+), 29 deletions(-) diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index 0f34c73576..7977a76f94 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -268,17 +268,14 @@ type numnot_option = | Abstract of raw_natural_number type numeral_notation_obj = - { num_ty : Libnames.reference; - z_pos_ty : z_pos_ty option; - int_ty : int_ty; - to_kind : conversion_kind; - to_ty : constr; - of_kind : conversion_kind; - of_ty : constr; - scope : Notation_term.scope_name; - constructors : Glob_term.glob_constr list; - warning : numnot_option; - path : Libnames.full_path } + { num_ty : Libnames.reference; (* i *) + z_pos_ty : z_pos_ty option; (* i*) + int_ty : int_ty; (* i *) + to_kind : conversion_kind; (* i *) + to_ty : constr; (* i *) + of_kind : conversion_kind; (* u *) + of_ty : constr; (* u *) + warning : numnot_option; (* i *) } let interp o ?loc n = begin match o.warning with @@ -314,14 +311,17 @@ let uninterp o (Glob_term.AnyGlobConstr n) = | Type_errors.TypeError _ -> None (* cf. eval_constr_app *) | NotANumber -> None (* all other functions except big2raw *) -let load_numeral_notation _ (_, o) = - Notation.declare_rawnumeral_interpreter o.scope (o.path, []) - (interp o) - (o.constructors, uninterp o, true) +let load_numeral_notation _ (_, (opts,infos)) = + Notation.(register_rawnumeral_interpretation + infos.pt_uid (interp opts, uninterp opts)); + Notation.enable_prim_token_interpretation infos -let cache_numeral_notation o = load_numeral_notation 1 o +let cache_numeral_notation x = load_numeral_notation 1 x -let inNumeralNotation : numeral_notation_obj -> Libobject.obj = +(* TODO: substitution ? *) + +let inNumeralNotation : + numeral_notation_obj * Notation.prim_token_infos -> Libobject.obj = Libobject.declare_object { (Libobject.default_object "NUMERAL NOTATION") with Libobject.cache_function = cache_numeral_notation; @@ -331,11 +331,7 @@ let get_constructors ind = let mib,oib = Global.lookup_inductive ind in let mc = oib.Declarations.mind_consnames in Array.to_list - (Array.mapi - (fun j c -> - DAst.make - (Glob_term.GRef (ConstructRef (ind, j + 1), None))) - mc) + (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc) let q_z = qualid_of_string "Coq.Numbers.BinNums.Z" let q_positive = qualid_of_string "Coq.Numbers.BinNums.positive" @@ -453,8 +449,7 @@ let vernac_numeral_notation ty f g scope opts = pr_reference ty ++ str " to Decimal.int or (option int) or uint or Z or (option Z)") in - Lib.add_anonymous_leaf - (inNumeralNotation + let o = { num_ty = ty; z_pos_ty; int_ty; @@ -462,10 +457,16 @@ let vernac_numeral_notation ty f g scope opts = to_ty; of_kind; of_ty; - scope; - constructors; - warning = opts; - path = Nametab.path_of_global tyc }) + warning = opts } + in + let i = Notation.( + { pt_scope = scope; + pt_uid = Marshal.to_string o []; + pt_required = Nametab.path_of_global tyc,[]; + pt_refs = constructors; + pt_in_match = true }) + in + Lib.add_anonymous_leaf (inNumeralNotation (o,i)) open Ltac_plugin open Stdarg diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v index ca8cba67d5..4c81095c68 100644 --- a/test-suite/interactive/PrimNotation.v +++ b/test-suite/interactive/PrimNotation.v @@ -7,7 +7,7 @@ Delimit Scope Z_scope with Z. Open Scope Z_scope. Check 0. (* 0 : nat *) -Require BinNums. +Require BinInt. Check 0. (* 0 : BinNums.Z *) Back 2. -- cgit v1.2.3 From d4bfa3df0910ff3e69d4b162d2f8d68775ec69aa Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 11 Apr 2018 12:48:22 +0200 Subject: WIP: cleanup numeral_notation_obj + errors --- plugins/syntax/g_numeral.ml4 | 140 +++++++++++++++++++++++-------------------- 1 file changed, 74 insertions(+), 66 deletions(-) diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index 7977a76f94..caba4db4fc 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -258,7 +258,11 @@ let big2raw n = let raw2big (n,s) = if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) -type target_kind = Int | UInt | Z +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 @@ -268,14 +272,12 @@ type numnot_option = | Abstract of raw_natural_number type numeral_notation_obj = - { num_ty : Libnames.reference; (* i *) - z_pos_ty : z_pos_ty option; (* i*) - int_ty : int_ty; (* i *) - to_kind : conversion_kind; (* i *) - to_ty : constr; (* i *) - of_kind : conversion_kind; (* u *) - of_ty : constr; (* u *) - warning : numnot_option; (* i *) } + { to_kind : conversion_kind; + to_ty : constr; + of_kind : conversion_kind; + of_ty : constr; + num_ty : Libnames.reference; (* for warnings / error messages *) + warning : numnot_option } let interp o ?loc n = begin match o.warning with @@ -284,10 +286,10 @@ let interp o ?loc n = | _ -> () end; let c = match fst o.to_kind with - | Int -> coqint_of_rawnum o.int_ty n - | UInt when snd n -> coquint_of_rawnum o.int_ty.uint (fst n) - | UInt (* n <= 0 *) -> no_such_number ?loc o.num_ty - | Z -> z_of_bigint (Option.get o.z_pos_ty) (raw2big n) + | 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 match o.warning, snd o.to_kind with | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 -> @@ -304,24 +306,31 @@ let uninterp o (Glob_term.AnyGlobConstr n) = let c = eval_constr_app o.of_ty (constr_of_glob 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)) + | Int _ -> Some (rawnum_of_coqint c) + | UInt _ -> Some (rawnum_of_coquint c, true) + | Z _ -> Some (big2raw (bigint_of_z c)) with | Type_errors.TypeError _ -> None (* cf. eval_constr_app *) | NotANumber -> None (* all other functions except big2raw *) -let load_numeral_notation _ (_, (opts,infos)) = - Notation.(register_rawnumeral_interpretation - infos.pt_uid (interp opts, uninterp opts)); - Notation.enable_prim_token_interpretation infos +(* Here we only register the interp and uninterp functions + for a particular Numeral Notation (determined by a unique + string). The actual activation of the notation will be done + later (cf. Notation.enable_prim_token_interpretation). + This registration of interp/uninterp must be added in the + libstack, otherwise this won't work through a Require. *) + +let load_numeral_notation _ (_, (uid,opts)) = + Notation.register_rawnumeral_interpretation + uid (interp opts, uninterp opts) let cache_numeral_notation x = load_numeral_notation 1 x -(* TODO: substitution ? *) +(* TODO: substitution ? + TODO: uid pas stable par substitution dans opts + *) -let inNumeralNotation : - numeral_notation_obj * Notation.prim_token_infos -> Libobject.obj = +let inNumeralNotation : string * numeral_notation_obj -> Libobject.obj = Libobject.declare_object { (Libobject.default_object "NUMERAL NOTATION") with Libobject.cache_function = cache_numeral_notation; @@ -374,6 +383,20 @@ let has_type f ty = try let _ = Constrintern.interp_constr env sigma c in true with Pretype_errors.PretypeError _ -> false +let type_error_to f ty loadZ = + CErrors.user_err + (pr_reference f ++ str " should go from Decimal.int to " ++ + pr_reference ty ++ str " or (option " ++ pr_reference ty ++ str ")." ++ + fnl () ++ str "Instead of int, the types uint or Z could be used" ++ + (if loadZ then str " (load Z first)." else str ".")) + +let type_error_of g ty loadZ = + CErrors.user_err + (pr_reference g ++ str " should go from " ++ pr_reference ty ++ + str " to Decimal.int or (option int)." ++ fnl () ++ + str "Instead of int, the types uint or Z could be used" ++ + (if loadZ then str " (load Z first)." else str ".")) + let vernac_numeral_notation ty f g scope opts = let int_ty = locate_int () in let z_pos_ty = locate_z () in @@ -408,65 +431,50 @@ let vernac_numeral_notation ty f g scope opts = if Global.is_polymorphic (Nametab.global f) then CErrors.user_err (pr_reference f ++ str " cannot be polymorphic for the moment") - else if has_type f (arrow cint cty) then Int, Direct - else if has_type f (arrow cint (opt cty)) then Int, Option - else if has_type f (arrow cuint cty) then UInt, Direct - else if has_type f (arrow cuint (opt cty)) then UInt, Option - else if Option.is_empty z_pos_ty then - CErrors.user_err - (pr_reference f ++ str " should go from Decimal.int or uint to " ++ - pr_reference ty ++ str " or (option " ++ pr_reference ty ++ - str ")." ++ fnl () ++ - str "Instead of int, the type Z could also be used (load it first).") - else if has_type f (arrow cZ cty) then Z, Direct - else if has_type f (arrow cZ (opt cty)) then Z, Option + else if has_type f (arrow cint cty) then Int int_ty, Direct + else if has_type f (arrow cint (opt cty)) then Int int_ty, Option + else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct + else if has_type f (arrow cuint (opt cty)) then UInt int_ty.uint, Option else - CErrors.user_err - (pr_reference f ++ str " should go from Decimal.int or uint or Z to " - ++ - pr_reference ty ++ str " or (option " ++ pr_reference ty ++ str ")") + match z_pos_ty with + | Some z_pos_ty -> + if has_type f (arrow cZ cty) then Z z_pos_ty, Direct + else if has_type f (arrow cZ (opt cty)) then Z z_pos_ty, Option + else type_error_to f ty false + | None -> type_error_to f ty true in (* Check the type of g *) let of_kind = if Global.is_polymorphic (Nametab.global g) then CErrors.user_err (pr_reference g ++ str " cannot be polymorphic for the moment") - else if has_type g (arrow cty cint) then Int, Direct - else if has_type g (arrow cty (opt cint)) then Int, Option - else if has_type g (arrow cty cuint) then UInt, Direct - else if has_type g (arrow cty (opt cuint)) then UInt, Option - else if Option.is_empty z_pos_ty then - CErrors.user_err - (pr_reference g ++ str " should go from " ++ - pr_reference ty ++ - str " to Decimal.int or (option int) or uint." ++ fnl () ++ - str "Instead of int, the type Z could also be used (load it first).") - else if has_type g (arrow cty cZ) then Z, Direct - else if has_type g (arrow cty (opt cZ)) then Z, Option + else if has_type g (arrow cty cint) then Int int_ty, Direct + else if has_type g (arrow cty (opt cint)) then Int int_ty, Option + else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct + else if has_type g (arrow cty (opt cuint)) then UInt int_ty.uint, Option else - CErrors.user_err - (pr_reference g ++ str " should go from " ++ - pr_reference ty ++ - str " to Decimal.int or (option int) or uint or Z or (option Z)") + match z_pos_ty with + | Some z_pos_ty -> + if has_type g (arrow cty cZ) then Z z_pos_ty, Direct + else if has_type g (arrow cty (opt cZ)) then Z z_pos_ty, Option + else type_error_of g ty false + | None -> type_error_of g ty true in - let o = - { num_ty = ty; - z_pos_ty; - int_ty; - to_kind; - to_ty; - of_kind; - of_ty; - warning = opts } + let o = { to_kind; to_ty; of_kind; of_ty; + num_ty = ty; + warning = opts } in + (* TODO: un hash suffit-il ? *) + let uid = Marshal.to_string o [] in let i = Notation.( { pt_scope = scope; - pt_uid = Marshal.to_string o []; + pt_uid = uid; pt_required = Nametab.path_of_global tyc,[]; pt_refs = constructors; pt_in_match = true }) in - Lib.add_anonymous_leaf (inNumeralNotation (o,i)) + Lib.add_anonymous_leaf (inNumeralNotation (uid,o)); + Notation.enable_prim_token_interpretation i open Ltac_plugin open Stdarg -- cgit v1.2.3 From fa0f378c91286d9127777a06b1dc557f695c22ae Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 14 Jul 2018 06:25:22 -0400 Subject: Fix numeral notation for a rebase on top of master Some of this code is cargo-culted or kludged to work. As I understand it, the situation is as follows: There are two sorts of use-cases that need to be supported: 1. A plugin registers an OCaml function as a numeral interpreter. In this case, the function registration must be synchronized with the document state, but the functions should not be marshelled / stored in the .vo. 2. A vernacular registers a Gallina function as a numeral interpreter. In this case, the registration must be synchronized, and the function should be marshelled / stored in the .vo. In case (1), we can compare functions by pointer equality, and we should be able to rely on globally unique keys, even across backtracking. In case (2), we cannot compare functions by pointer equality (because they must be regenerated on unmarshelling when `Require`ing a .vo file), and we also cannot rely on any sort of unique key being both unique and persistent across files. The solution we use here is that we ask clients to provide "unique" keys, and that clients tell us whether or not to overwrite existing registered functions, i.e., to tell us whether or not we should expect interpreter functions to be globally unique under pointer equality. For plugins, a simple string suffices, as long as the string does not clash between different plugins. In the case of vernacular-registered functions, use marshell a description of all of the data used to generate the function, and use that string as a unique key which is expected to persist across files. Because we cannot rely on function-pointer uniqueness here, we tell the interpretation-registration to allow overwriting. ---- Some of this code is response to comments on the PR ---- Some code is to fix an issue that bignums revealed: Both Int31 and bignums registered numeral notations in int31_scope. We now prepend a globally unique identifier when registering numeral notations from OCaml plugins. This is permissible because we don't store the uid information for such notations in .vo files (assuming I'm understanding the code correctly). --- doc/sphinx/user-extensions/syntax-extensions.rst | 160 ++++++++++++++++++----- interp/notation.ml | 37 +++--- interp/notation.mli | 8 +- plugins/syntax/g_numeral.ml4 | 80 +++++++----- test-suite/success/NumeralNotations.v | 55 ++++++++ theories/Numbers/AltBinNotations.v | 45 +++---- 6 files changed, 272 insertions(+), 113 deletions(-) create mode 100644 test-suite/success/NumeralNotations.v diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index e947fd891b..ca588acf29 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1379,42 +1379,130 @@ Numeral notations Starting with version 8.9, the following command allows the user to customize the way numeral literals are parsed and printed: -.. cmd:: Numeral Notation @ty @pa @pr : @scope. - -In the previous line, `ty` should be the name of an inductive type, -while `pa` and `pr` should be the names of two parsing and printing -functions. -The parsing function `pa` should have one of the following types: - - * :g:`Decimal.int -> ty` - * :g:`Decimal.int -> option ty` - * :g:`Decimal.uint -> ty` - * :g:`Decimal.uint -> option ty` - * :g:`Z -> ty` - * :g:`Z -> option ty` - -And the printing function `pr` should have one of the following types: - - * :g:`ty -> Decimal.int` - * :g:`ty -> option Decimal.int` - * :g:`ty -> Decimal.uint` - * :g:`ty -> option Decimal.uint` - * :g:`ty -> Z` - * :g:`ty -> option Z` - -.. cmdv:: Numeral Notation @ty @pa @pr : @scope (warning after @n). - -When a literal larger than `n` is parsed, a warning message about -possible stack overflow will be displayed. - -.. cmdv:: Numeral Notation @ty @pa @pr : @scope (abstract after @n). - -When a literal `m` larger than `n` is parsed, the result will be -:g:`(pa m)`, without reduction of this application to a normal form. -Here `m` will be a ``Decimal.int`` or ``Decimal.uint`` or ``Z``, -depending on the type of the parsing function `pa`. This allows a more -compact representation of literals in types such as ``nat``, and -limits parse failures due to stack overflow. +.. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. + + In the previous line, :n:`@ident__1` should be the name of an + inductive type, while :n:`@ident__2` and :n:`@ident__3` should be + the names of the parsing and printing functions, respectively. The + parsing function :n:`@ident__2` should have one of the following + types: + + * :n:`Decimal.int -> @ident__1` + * :n:`Decimal.int -> option @ident__1` + * :n:`Decimal.uint -> @ident__1` + * :n:`Decimal.uint -> option @ident__1` + * :n:`Z -> @ident__1` + * :n:`Z -> option @ident__1` + + And the printing function :n:`@ident__3` should have one of the + following types: + + * :n:`@ident__1 -> Decimal.int` + * :n:`@ident__1 -> option Decimal.int` + * :n:`@ident__1 -> Decimal.uint` + * :n:`@ident__1 -> option Decimal.uint` + * :n:`@ident__1 -> Z` + * :n:`@ident__1 -> option Z` + + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). + + When a literal larger than :token:`num` is parsed, a warning + message about possible stack overflow, resulting from evaluating + :n:`@ident__2`, will be displayed. + + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num). + + When a literal :g:`m` larger than :token:`num` is parsed, the + result will be :n:`(@ident__2 m)`, without reduction of this + application to a normal form. Here :g:`m` will be a + :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the + type of the parsing function :n:`@ident__2`. This allows for a + more compact representation of literals in types such as :g:`nat`, + and limits parse failures due to stack overflow. Note that a + warning will be emitted when an integer larger than :token:`num` + is parsed. + + .. exn:: Cannot interpret this number as a value of type @type + + The numeral notation registered for :g:`ty` does not support the + given numeral. This error is given when the interpretation + function returns :g:`None`, or if the interpretation is registered + for only non-negative integers, and the given numeral is negative. + + .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + + The parsing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. + + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the the types Decimal.uint or Z could be used{? (require BinNums first)}. + + The printing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. + + .. exn:: @type is not an inductive type + + Numeral notations can only be declared for inductive types with no + arguments. + + .. exn:: The inductive type @type cannot be used in numeral notations because support for polymorphic inductive types is not yet implemented. + + Numeral notations do not currently support polymorphic inductive + types. Ensure that all types involved in numeral notations are + declared with :g:`Unset Universe Polymorphism`, or with the + :g:`Monomorphic` attribute. + + .. exn:: The function @ident cannot be used in numeral notations because support for polymorphic printing and parsing functions is not yet implemented. + + Numeral notations do not currently support polymorphic functions + for printing and parsing. Ensure that both functions passed to + :cmd:`Numeral Notation` are defined with :g:`Unset Universe + Polymorphism`, or with the :g:`Monomorphic` attribute. + + .. exn:: Unexpected term while parsing a numeral notation + + Parsing functions must always return ground terms, made up of + applications of constructors and inductive types. Parsing + functions may not return terms containing axioms, bare + (co)fixpoints, lambdas, etc. + + .. exn:: Unexpected non-option term while parsing a numeral notation + + Parsing functions expected to return an :g:`option` must always + return a concrete :g:`Some` or :g:`None` when applied to a + concrete numeral expressed as a decimal. They may not return + opaque constants. + + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). + + The type passed to :cmd:`Numeral Notation` must be a single + identifier. + + .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). + + Both functions passed to :cmd:`Numeral Notation` must be single + identifiers. + + .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). + + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(warning after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + + .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2. + + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(abstract after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + Typically, this indicates that the fully computed representation + of numerals can be so large that non-tail-recursive OCaml + functions run out of stack space when trying to walk them. + + For example + + .. coqtop:: all + + Check 90000. + .. _TacticNotation: diff --git a/interp/notation.ml b/interp/notation.ml index f60ddcf909..56d6acbdae 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -378,38 +378,39 @@ let prim_token_interp_infos = let prim_token_uninterp_infos = ref (Refmap.empty : (scope_name * prim_token_uid * bool) Refmap.t) -let hashtbl_check_and_set uid f h eq = +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 uid (interp, uninterp) = +let register_gen_interpretation allow_overwrite uid (interp, uninterp) = hashtbl_check_and_set - uid interp prim_token_interpreters InnerPrimToken.interp_eq; + allow_overwrite uid interp prim_token_interpreters InnerPrimToken.interp_eq; hashtbl_check_and_set - uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq + allow_overwrite uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq -let register_rawnumeral_interpretation uid (interp, uninterp) = - register_gen_interpretation uid +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 uid (interp, uninterp) = - register_gen_interpretation uid +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 uid (interp, uninterp) = - register_gen_interpretation uid +let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp) type prim_token_infos = { pt_scope : scope_name; (** Concerned scope *) pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) pt_required : required_module; (** Module that should be loaded first *) - pt_refs : global_reference list; (** Entry points during uninterpretation *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) pt_in_match : bool (** Is this prim token legal in match patterns ? *) } @@ -445,19 +446,25 @@ let enable_prim_token_interpretation infos = (the latter inside a [Mltop.declare_cache_obj]). *) +let fresh_string_of = + let count = ref 0 in + fun root -> count := !count+1; (string_of_int !count)^"_"^root + let declare_numeral_interpreter sc dir interp (patl,uninterp,b) = - register_bignumeral_interpretation sc (interp,uninterp); + let uid = fresh_string_of sc in + register_bignumeral_interpretation uid (interp,uninterp); enable_prim_token_interpretation { pt_scope = sc; - pt_uid = sc; + pt_uid = uid; pt_required = dir; pt_refs = List.map_filter glob_prim_constr_key patl; pt_in_match = b } let declare_string_interpreter sc dir interp (patl,uninterp,b) = - register_string_interpretation sc (interp,uninterp); + let uid = fresh_string_of sc in + register_string_interpretation uid (interp,uninterp); enable_prim_token_interpretation { pt_scope = sc; - pt_uid = sc; + pt_uid = uid; pt_required = dir; pt_refs = List.map_filter glob_prim_constr_key patl; pt_in_match = b } diff --git a/interp/notation.mli b/interp/notation.mli index 2545e494ef..1d01d75c82 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -91,19 +91,19 @@ type 'a prim_token_interpretation = 'a prim_token_interpreter * 'a prim_token_uninterpreter val register_rawnumeral_interpretation : - prim_token_uid -> rawnum prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit val register_bignumeral_interpretation : - prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit val register_string_interpretation : - prim_token_uid -> string prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit type prim_token_infos = { pt_scope : scope_name; (** Concerned scope *) pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) pt_required : required_module; (** Module that should be loaded first *) - pt_refs : global_reference list; (** Entry points during uninterpretation *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) pt_in_match : bool (** Is this prim token legal in match patterns ? *) } diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index caba4db4fc..19a15fd1df 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* strbrk "Stack overflow or segmentation fault happens when " ++ - strbrk "working with large numbers in " ++ pr_reference ty ++ + strbrk "working with large numbers in " ++ pr_qualid ty ++ strbrk " (threshold may vary depending" ++ strbrk " on your system limits and on the command executed).") @@ -64,11 +65,11 @@ let warn_abstract_large_num = (fun (ty,f) -> let (sigma, env) = Pfedit.get_current_context () in strbrk "To avoid stack overflow, large numbers in " ++ - pr_reference ty ++ strbrk " are interpreted as applications of " ++ + pr_qualid ty ++ strbrk " are interpreted as applications of " ++ Printer.pr_constr_env env sigma f ++ strbrk ".") (** Comparing two raw numbers (base 10, big-endian, non-negative). - A bit nasty, but not critical : only used to decide when a + A bit nasty, but not critical: only used to decide when a number is considered as large (see warnings above). *) exception Comp of int @@ -233,18 +234,24 @@ let rec glob_of_constr ?loc c = match Constr.kind c with | 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)) - | _ -> CErrors.anomaly (str "Numeral.interp: unexpected constr") + | _ -> let (sigma, env) = Pfedit.get_current_context () in + CErrors.user_err ?loc + (str "Unexpected term while parsing a numeral notation:" ++ fnl () ++ + Printer.pr_constr_env env sigma c) let no_such_number ?loc ty = CErrors.user_err ?loc (str "Cannot interpret this number as a value of type " ++ - pr_reference ty) + pr_qualid ty) let interp_option ty ?loc c = match Constr.kind c with | App (_Some, [| _; c |]) -> glob_of_constr ?loc c | App (_None, [| _ |]) -> no_such_number ?loc ty - | x -> CErrors.anomaly (str "Numeral.interp: option expected") + | x -> let (sigma, env) = Pfedit.get_current_context () in + CErrors.user_err ?loc + (str "Unexpected non-option term while parsing a numeral notation:" ++ fnl () ++ + Printer.pr_constr_env env sigma c) let uninterp_option c = match Constr.kind c with @@ -276,7 +283,7 @@ type numeral_notation_obj = to_ty : constr; of_kind : conversion_kind; of_ty : constr; - num_ty : Libnames.reference; (* for warnings / error messages *) + num_ty : Libnames.qualid; (* for warnings / error messages *) warning : numnot_option } let interp o ?loc n = @@ -322,7 +329,7 @@ let uninterp o (Glob_term.AnyGlobConstr n) = let load_numeral_notation _ (_, (uid,opts)) = Notation.register_rawnumeral_interpretation - uid (interp opts, uninterp opts) + ~allow_overwrite:true uid (interp opts, uninterp opts) let cache_numeral_notation x = load_numeral_notation 1 x @@ -355,7 +362,7 @@ let unsafe_locate_ind q = let locate_ind q = try unsafe_locate_ind q - with Not_found -> Nametab.error_global_not_found (CAst.make q) + with Not_found -> Nametab.error_global_not_found q let locate_z () = try @@ -367,35 +374,33 @@ let locate_int () = { uint = locate_ind q_uint; int = locate_ind q_int } -let locate_globref r = - let q = qualid_of_reference r in - try Nametab.locate CAst.(q.v) +let locate_globref q = + try Nametab.locate q with Not_found -> Nametab.error_global_not_found q -let locate_constant r = - let q = qualid_of_reference r in - try Nametab.locate_constant CAst.(q.v) +let locate_constant q = + try Nametab.locate_constant q with Not_found -> Nametab.error_global_not_found q let has_type f ty = let (sigma, env) = Pfedit.get_current_context () in - let c = mkCastC (mkRefC f, CastConv ty) in + let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in try let _ = Constrintern.interp_constr env sigma c in true with Pretype_errors.PretypeError _ -> false let type_error_to f ty loadZ = CErrors.user_err - (pr_reference f ++ str " should go from Decimal.int to " ++ - pr_reference ty ++ str " or (option " ++ pr_reference ty ++ str ")." ++ - fnl () ++ str "Instead of int, the types uint or Z could be used" ++ - (if loadZ then str " (load Z first)." else str ".")) + (pr_qualid f ++ str " should go from Decimal.int to " ++ + pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ + fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ + (if loadZ then str " (require BinNums first)." else str ".")) let type_error_of g ty loadZ = CErrors.user_err - (pr_reference g ++ str " should go from " ++ pr_reference ty ++ - str " to Decimal.int or (option int)." ++ fnl () ++ - str "Instead of int, the types uint or Z could be used" ++ - (if loadZ then str " (load Z first)." else str ".")) + (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ + str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ + str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ + (if loadZ then str " (require BinNums first)." else str ".")) let vernac_numeral_notation ty f g scope opts = let int_ty = locate_int () in @@ -405,7 +410,7 @@ let vernac_numeral_notation ty f g scope opts = let of_ty = mkConst (locate_constant g) in let cty = mkRefC ty in let app x y = mkAppC (x,[y]) in - let cref q = mkRefC (CAst.make (Qualid q)) in + let cref q = mkRefC q in let arrow x y = mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) in @@ -420,17 +425,20 @@ let vernac_numeral_notation ty f g scope opts = get_constructors ind | IndRef _ -> CErrors.user_err - (str "The inductive type " ++ pr_reference ty ++ - str " cannot be polymorphic here for the moment") + (str "The inductive type " ++ pr_qualid ty ++ + str " cannot be used in numeral notations because" ++ + str " support for polymorphic inductive types is not yet implemented") | ConstRef _ | ConstructRef _ | VarRef _ -> CErrors.user_err - (pr_reference ty ++ str " is not an inductive type") + (pr_qualid ty ++ str " is not an inductive type") in (* Check the type of f *) let to_kind = if Global.is_polymorphic (Nametab.global f) then CErrors.user_err - (pr_reference f ++ str " cannot be polymorphic for the moment") + (str "The function " ++ pr_qualid f ++ str " cannot be used" ++ + str " in numeral notations because support for polymorphic" ++ + str " printing and parsing functions is not yet implemented.") else if has_type f (arrow cint cty) then Int int_ty, Direct else if has_type f (arrow cint (opt cty)) then Int int_ty, Option else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct @@ -447,7 +455,7 @@ let vernac_numeral_notation ty f g scope opts = let of_kind = if Global.is_polymorphic (Nametab.global g) then CErrors.user_err - (pr_reference g ++ str " cannot be polymorphic for the moment") + (pr_qualid g ++ str " cannot be polymorphic for the moment") else if has_type g (arrow cty cint) then Int int_ty, Direct else if has_type g (arrow cty (opt cint)) then Int int_ty, Option else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v new file mode 100644 index 0000000000..a06327c5e6 --- /dev/null +++ b/test-suite/success/NumeralNotations.v @@ -0,0 +1,55 @@ + +(* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *) + +(* https://github.com/coq/coq/pull/8064#discussion_r202497516 *) +Module Test1. + Axiom hold : forall {A B C}, A -> B -> C. + Definition opaque3 (x : Decimal.int) : Decimal.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). + Numeral Notation Decimal.int opaque3 opaque3 : opaque_scope. + Delimit Scope opaque_scope with opaque. + Fail Check 1%opaque. +End Test1. + +(* https://github.com/coq/coq/pull/8064#discussion_r202497990 *) +Module Test2. + Axiom opaque4 : option Decimal.int. + Definition opaque6 (x : Decimal.int) : option Decimal.int := opaque4. + Numeral Notation Decimal.int opaque6 opaque6 : opaque_scope. + Delimit Scope opaque_scope with opaque. + Open Scope opaque_scope. + Fail Check 1%opaque. +End Test2. + +Module Test3. + Inductive silly := SILLY (v : Decimal.uint) (f : forall A, A -> A). + Definition to_silly (v : Decimal.uint) := SILLY v (fun _ x => x). + Definition of_silly (v : silly) := match v with SILLY v _ => v end. + Numeral Notation silly to_silly of_silly : silly_scope. + Delimit Scope silly_scope with silly. + Fail Check 1%silly. +End Test3. + + +Module Test4. + Polymorphic Inductive punit := ptt. + Polymorphic Definition pto_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. + Polymorphic Definition pof_punit (v : punit) : Decimal.uint := Nat.to_uint 0. + Definition to_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. + Definition of_punit (v : punit) : Decimal.uint := Nat.to_uint 0. + Polymorphic Definition pto_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end. + Polymorphic Definition pof_unit (v : unit) : Decimal.uint := Nat.to_uint 0. + Definition to_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end. + Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0. + Fail Numeral Notation punit to_punit of_punit : pto. + Fail Numeral Notation punit pto_punit of_punit : ppo. + Fail Numeral Notation punit to_punit pof_punit : ptp. + Fail Numeral Notation punit pto_punit pof_punit : ppp. + Numeral Notation unit to_unit of_unit : uto. + Delimit Scope uto with uto. + Check let v := 0%uto in v : unit. + Fail Check 1%uto. + Fail Check (-1)%uto. + Fail Numeral Notation unit pto_unit of_unit : upo. + Fail Numeral Notation unit to_unit pof_unit : utp. + Fail Numeral Notation unit pto_unit pof_unit : upp. +End Test4. diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v index 595934ad89..c7e3999691 100644 --- a/theories/Numbers/AltBinNotations.v +++ b/theories/Numbers/AltBinNotations.v @@ -1,34 +1,35 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let (sigma, env) = Pfedit.get_current_context () in strbrk "To avoid stack overflow, large numbers in " ++ pr_qualid ty ++ strbrk " are interpreted as applications of " ++ - Printer.pr_constr_env env sigma f ++ strbrk ".") + Printer.pr_constant (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 @@ -216,12 +213,14 @@ let bigint_of_z z = match Constr.kind z with 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 g = match DAst.get g with - | Glob_term.GRef (ConstructRef c, _) -> mkConstruct c +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 c = constr_of_glob gc in - let cl = List.map constr_of_glob gcl in - mkApp (c, Array.of_list cl) + 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 @@ -280,9 +279,9 @@ type numnot_option = type numeral_notation_obj = { to_kind : conversion_kind; - to_ty : constr; + to_ty : Constant.t; of_kind : conversion_kind; - of_ty : constr; + of_ty : Constant.t; num_ty : Libnames.qualid; (* for warnings / error messages *) warning : numnot_option } @@ -298,19 +297,28 @@ let interp o ?loc 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_constant_instance env sigma o.to_ty in + let to_ty = mkConstU 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 (mkApp (o.to_ty,[|c|])) + glob_of_constr ?loc (mkApp (to_ty,[|c|])) | _ -> - let res = eval_constr_app o.to_ty c in + let res = eval_constr_app env sigma to_ty c in match snd o.to_kind with | Direct -> glob_of_constr ?loc res | Option -> interp_option o.num_ty ?loc 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_constant_instance env sigma o.of_ty in + let of_ty = mkConstU of_ty in try - let c = eval_constr_app o.of_ty (constr_of_glob n) in + 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) @@ -406,8 +414,8 @@ let vernac_numeral_notation ty f g scope opts = let int_ty = locate_int () in let z_pos_ty = locate_z () in let tyc = locate_globref ty in - let to_ty = mkConst (locate_constant f) in - let of_ty = mkConst (locate_constant g) in + let to_ty = locate_constant f in + let of_ty = locate_constant g in let cty = mkRefC ty in let app x y = mkAppC (x,[y]) in let cref q = mkRefC q in @@ -421,25 +429,15 @@ let vernac_numeral_notation ty f g scope opts = let opt r = app coption r in (* Check that [ty] is an inductive type *) let constructors = match tyc with - | IndRef ind when not (Global.is_polymorphic tyc) -> + | IndRef ind -> get_constructors ind - | IndRef _ -> - CErrors.user_err - (str "The inductive type " ++ pr_qualid ty ++ - str " cannot be used in numeral notations because" ++ - str " support for polymorphic inductive types is not yet implemented") | ConstRef _ | ConstructRef _ | VarRef _ -> CErrors.user_err (pr_qualid ty ++ str " is not an inductive type") in (* Check the type of f *) let to_kind = - if Global.is_polymorphic (Nametab.global f) then - CErrors.user_err - (str "The function " ++ pr_qualid f ++ str " cannot be used" ++ - str " in numeral notations because support for polymorphic" ++ - str " printing and parsing functions is not yet implemented.") - else if has_type f (arrow cint cty) then Int int_ty, Direct + if has_type f (arrow cint cty) then Int int_ty, Direct else if has_type f (arrow cint (opt cty)) then Int int_ty, Option else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct else if has_type f (arrow cuint (opt cty)) then UInt int_ty.uint, Option @@ -453,10 +451,7 @@ let vernac_numeral_notation ty f g scope opts = in (* Check the type of g *) let of_kind = - if Global.is_polymorphic (Nametab.global g) then - CErrors.user_err - (pr_qualid g ++ str " cannot be polymorphic for the moment") - else if has_type g (arrow cty cint) then Int int_ty, Direct + if has_type g (arrow cty cint) then Int int_ty, Direct else if has_type g (arrow cty (opt cint)) then Int int_ty, Option else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct else if has_type g (arrow cty (opt cuint)) then UInt int_ty.uint, Option -- cgit v1.2.3 From ebf453d4ae4e4f0312f3fd696da26c03671bc906 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 24 Jul 2018 13:06:03 -0400 Subject: Update doc and test-suite after supporting univ poly Also make `Check S` no longer anomaly Add a couple more test cases for numeral notations Also add another possibly-confusing error message to the doc. Respond to Hugo's doc request with Zimmi48's suggestion From https://github.com/coq/coq/pull/8064/files#r204191608 --- doc/sphinx/user-extensions/syntax-extensions.rst | 48 ++++----- plugins/syntax/g_numeral.ml4 | 11 +- test-suite/interactive/PrimNotation.v | 58 +++++++++-- test-suite/success/NumeralNotations.v | 123 +++++++++++++++++++++-- 4 files changed, 195 insertions(+), 45 deletions(-) diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index ca588acf29..50425c8a5d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1376,16 +1376,15 @@ Abbreviations Numeral notations ----------------- -Starting with version 8.9, the following command allows the user to customize -the way numeral literals are parsed and printed: - .. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. - In the previous line, :n:`@ident__1` should be the name of an - inductive type, while :n:`@ident__2` and :n:`@ident__3` should be - the names of the parsing and printing functions, respectively. The - parsing function :n:`@ident__2` should have one of the following - types: + This command allows the user to customize the way numeral literals + are parsed and printed. + + The token :n:`@ident__1` should be the name of an inductive type, + while :n:`@ident__2` and :n:`@ident__3` should be the names of the + parsing and printing functions, respectively. The parsing function + :n:`@ident__2` should have one of the following types: * :n:`Decimal.int -> @ident__1` * :n:`Decimal.int -> option @ident__1` @@ -1404,6 +1403,10 @@ the way numeral literals are parsed and printed: * :n:`@ident__1 -> Z` * :n:`@ident__1 -> option Z` + When parsing, the application of the parsing function + :n:`@ident__2` to the number will be fully reduced, and universes + of the resulting term will be refreshed. + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). When a literal larger than :token:`num` is parsed, a warning @@ -1420,12 +1423,13 @@ the way numeral literals are parsed and printed: more compact representation of literals in types such as :g:`nat`, and limits parse failures due to stack overflow. Note that a warning will be emitted when an integer larger than :token:`num` - is parsed. + is parsed. Note that :n:`(abstract after @num)` has no effect + when :n:`@ident__2` lands in an :g:`option` type. .. exn:: Cannot interpret this number as a value of type @type - The numeral notation registered for :g:`ty` does not support the - given numeral. This error is given when the interpretation + The numeral notation registered for :token:`type` does not support + the given numeral. This error is given when the interpretation function returns :g:`None`, or if the interpretation is registered for only non-negative integers, and the given numeral is negative. @@ -1434,7 +1438,7 @@ the way numeral literals are parsed and printed: The parsing function given to the :cmd:`Numeral Notation` vernacular is not of the right type. - .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the the types Decimal.uint or Z could be used{? (require BinNums first)}. + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. The printing function given to the :cmd:`Numeral Notation` vernacular is not of the right type. @@ -1444,20 +1448,6 @@ the way numeral literals are parsed and printed: Numeral notations can only be declared for inductive types with no arguments. - .. exn:: The inductive type @type cannot be used in numeral notations because support for polymorphic inductive types is not yet implemented. - - Numeral notations do not currently support polymorphic inductive - types. Ensure that all types involved in numeral notations are - declared with :g:`Unset Universe Polymorphism`, or with the - :g:`Monomorphic` attribute. - - .. exn:: The function @ident cannot be used in numeral notations because support for polymorphic printing and parsing functions is not yet implemented. - - Numeral notations do not currently support polymorphic functions - for printing and parsing. Ensure that both functions passed to - :cmd:`Numeral Notation` are defined with :g:`Unset Universe - Polymorphism`, or with the :g:`Monomorphic` attribute. - .. exn:: Unexpected term while parsing a numeral notation Parsing functions must always return ground terms, made up of @@ -1482,6 +1472,12 @@ the way numeral literals are parsed and printed: Both functions passed to :cmd:`Numeral Notation` must be single identifiers. + .. exn:: The reference @ident was not found in the current environment. + + Identifiers passed to :cmd:`Numeral Notation` must be global + definitions, not notations, section variables, section-local + :g:`Let` bound identifiers, etc. + .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). When a :cmd:`Numeral Notation` is registered in the current scope diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index 1d2d47fbaa..a097adec24 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -36,13 +36,14 @@ open Constr 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 + 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 (c : constr) = - let (sigma, env) = Lemmas.get_current_context () in - Tacred.compute env sigma c +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 = @@ -325,7 +326,7 @@ let uninterp o (Glob_term.AnyGlobConstr n) = | UInt _ -> Some (rawnum_of_coquint c, true) | Z _ -> Some (big2raw (bigint_of_z c)) with - | Type_errors.TypeError _ -> None (* cf. eval_constr_app *) + | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *) | NotANumber -> None (* all other functions except big2raw *) (* Here we only register the interp and uninterp functions diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v index 4c81095c68..07986b0df3 100644 --- a/test-suite/interactive/PrimNotation.v +++ b/test-suite/interactive/PrimNotation.v @@ -5,14 +5,60 @@ Delimit Scope Z_scope with Z. Open Scope Z_scope. -Check 0. -(* 0 : nat *) +Check let v := 0 in v : nat. +(* let v := 0 in v : nat : nat *) Require BinInt. -Check 0. -(* 0 : BinNums.Z *) +Check let v := 0 in v : BinNums.Z. +(* let v := 0 in v : BinNums.Z : BinNums.Z *) Back 2. -Check 0. -(* Expected answer: 0 : nat *) +Check let v := 0 in v : nat. +(* Expected answer: let v := 0 in v : nat : nat *) (* Used to fail with: Error: Cannot interpret in Z_scope without requiring first module BinNums. *) + +Local Set Universe Polymorphism. +Delimit Scope punit_scope with punit. +Delimit Scope pcunit_scope with pcunit. +Delimit Scope int_scope with int. +Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : int_scope. +Module A. + NonCumulative Inductive punit@{u} : Type@{u} := ptt. + Cumulative Inductive pcunit@{u} : Type@{u} := pctt. + Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. + Definition to_pcunit : Decimal.int -> option pcunit + := fun v => match v with 0%int => Some pctt | _ => None end. + Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. + Definition of_pcunit : pcunit -> Decimal.uint := fun _ => Nat.to_uint 0. + Numeral Notation punit to_punit of_punit : punit_scope. + Check let v := 0%punit in v : punit. + Back 2. + Numeral Notation pcunit to_pcunit of_pcunit : punit_scope. + Check let v := 0%punit in v : pcunit. +End A. +Reset A. +Local Unset Universe Polymorphism. +Module A. + Inductive punit : Set := ptt. + Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. + Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. + Numeral Notation punit to_punit of_punit : punit_scope. + Check let v := 0%punit in v : punit. +End A. +Local Set Universe Polymorphism. +Inductive punit@{u} : Type@{u} := ptt. +Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. +Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. +Numeral Notation punit to_punit of_punit : punit_scope. +Check let v := 0%punit in v : punit. +Back 6. (* check backtracking of registering universe polymorphic constants *) +Local Unset Universe Polymorphism. +Inductive punit : Set := ptt. +Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. +Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. +Numeral Notation punit to_punit of_punit : punit_scope. +Check let v := 0%punit in v : punit. diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v index a06327c5e6..907ec32671 100644 --- a/test-suite/success/NumeralNotations.v +++ b/test-suite/success/NumeralNotations.v @@ -31,8 +31,9 @@ End Test3. Module Test4. - Polymorphic Inductive punit := ptt. + Polymorphic NonCumulative Inductive punit := ptt. Polymorphic Definition pto_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. + Polymorphic Definition pto_punit_all (v : Decimal.uint) : punit := ptt. Polymorphic Definition pof_punit (v : punit) : Decimal.uint := Nat.to_uint 0. Definition to_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. Definition of_punit (v : punit) : Decimal.uint := Nat.to_uint 0. @@ -40,16 +41,122 @@ Module Test4. Polymorphic Definition pof_unit (v : unit) : Decimal.uint := Nat.to_uint 0. Definition to_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end. Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0. - Fail Numeral Notation punit to_punit of_punit : pto. - Fail Numeral Notation punit pto_punit of_punit : ppo. - Fail Numeral Notation punit to_punit pof_punit : ptp. - Fail Numeral Notation punit pto_punit pof_punit : ppp. + Numeral Notation punit to_punit of_punit : pto. + Numeral Notation punit pto_punit of_punit : ppo. + Numeral Notation punit to_punit pof_punit : ptp. + Numeral Notation punit pto_punit pof_punit : ppp. Numeral Notation unit to_unit of_unit : uto. + Delimit Scope pto with pto. + Delimit Scope ppo with ppo. + Delimit Scope ptp with ptp. + Delimit Scope ppp with ppp. Delimit Scope uto with uto. + Check let v := 0%pto in v : punit. + Check let v := 0%ppo in v : punit. + Check let v := 0%ptp in v : punit. + Check let v := 0%ppp in v : punit. Check let v := 0%uto in v : unit. Fail Check 1%uto. Fail Check (-1)%uto. - Fail Numeral Notation unit pto_unit of_unit : upo. - Fail Numeral Notation unit to_unit pof_unit : utp. - Fail Numeral Notation unit pto_unit pof_unit : upp. + Numeral Notation unit pto_unit of_unit : upo. + Numeral Notation unit to_unit pof_unit : utp. + Numeral Notation unit pto_unit pof_unit : upp. + Delimit Scope upo with upo. + Delimit Scope utp with utp. + Delimit Scope upp with upp. + Check let v := 0%upo in v : unit. + Check let v := 0%utp in v : unit. + Check let v := 0%upp in v : unit. + + Polymorphic Definition pto_punits := pto_punit_all@{Set}. + Polymorphic Definition pof_punits := pof_punit@{Set}. + Numeral Notation punit pto_punits pof_punits : ppps (abstract after 1). + Delimit Scope ppps with ppps. + Universe u. + Constraint Set < u. + Check let v := 0%ppps in v : punit@{u}. (* Check that universes are refreshed *) + Fail Check let v := 1%ppps in v : punit@{u}. (* Note that universes are not refreshed here *) End Test4. + +Module Test5. + Check S. (* At one point gave Error: Anomaly "Uncaught exception Pretype_errors.PretypeError(_, _, _)." Please report at http://coq.inria.fr/bugs/. *) +End Test5. + +Module Test6. + (* Check that numeral notations on enormous terms don't take forever to print/parse *) + (* Ackerman definition from https://stackoverflow.com/a/10303475/377022 *) + Fixpoint ack (n m : nat) : nat := + match n with + | O => S m + | S p => let fix ackn (m : nat) := + match m with + | O => ack p 1 + | S q => ack p (ackn q) + end + in ackn m + end. + + Timeout 1 Check (S (ack 4 4)). (* should be instantaneous *) + + Local Set Primitive Projections. + Record > wnat := wrap { unwrap :> nat }. + Definition to_uint (x : wnat) : Decimal.uint := Nat.to_uint x. + Definition of_uint (x : Decimal.uint) : wnat := Nat.of_uint x. + Module Export Scopes. + Delimit Scope wnat_scope with wnat. + End Scopes. + Module Export Notations. + Export Scopes. + Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000). + End Notations. + Check let v := 0%wnat in v : wnat. + Check wrap O. + Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *) +End Test6. + +Module Test6_2. + Import Test6.Scopes. + Check Test6.wrap 0. + Import Test6.Notations. + Check let v := 0%wnat in v : Test6.wnat. +End Test6_2. + +Module Test7. + Local Set Primitive Projections. + Record > wuint := wrap { unwrap : Decimal.uint }. + Delimit Scope wuint_scope with wuint. + Fail Numeral Notation wuint wrap unwrap : wuint_scope. +End Test7. + +Module Test8. + Local Set Primitive Projections. + Record > wuint := wrap { unwrap : Decimal.uint }. + Delimit Scope wuint_scope with wuint. + Section with_var. + Context (dummy : unit). + Definition wrap' := let __ := dummy in wrap. + Definition unwrap' := let __ := dummy in unwrap. + Global Numeral Notation wuint wrap' unwrap' : wuint_scope. + Check let v := 0%wuint in v : wuint. + End with_var. + Fail Check let v := 0%wuint in v : wuint. + Compute wrap (Nat.to_uint 0). + + Notation wrap'' := wrap. + Notation unwrap'' := unwrap. + Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope. +End Test8. + +Module Test9. + Section with_let. + Local Set Primitive Projections. + Record > wuint := wrap { unwrap : Decimal.uint }. + Let wrap' := wrap. + Let unwrap' := unwrap. + Local Notation wrap'' := wrap. + Local Notation unwrap'' := unwrap. + Delimit Scope wuint_scope with wuint. + Fail Numeral Notation wuint wrap' unwrap' : wuint_scope. + Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope. + End with_let. +End Test9. -- cgit v1.2.3 From 85d5b246b0fbf845c6c61ffac6f0e2563c237d69 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 26 Jul 2018 09:54:42 -0400 Subject: Update CHANGES --- CHANGES | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/CHANGES b/CHANGES index a42c44c09b..b1f9d46ed8 100644 --- a/CHANGES +++ b/CHANGES @@ -65,6 +65,15 @@ Standard Library - Added `Ndigits.N2Bv_sized`, and proved some lemmas about it. +- The scopes `int_scope` and `uint_scope` have been renamed to + `dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect + and other packages. They are still delimited by `%int` and `%uint`. + +- Numeral syntax for `nat` is no longer available without loading the + entire prelude (`Require Import Coq.Init.Prelude`). This only + impacts users running Coq without the init library (`-nois` or + `-noinit`) and also issuing `Require Import Coq.Init.Datatypes`. + Tools - Coq_makefile lets one override or extend the following variables from @@ -98,6 +107,8 @@ Vernacular Commands overwritting the opacity set of the hint database. - Added generic syntax for “attributes”, as in: `#[local] Lemma foo : bar.` +- Added the `Numeral Notation` command for registering decimal numeral + notations for custom types - The `Set SsrHave NoTCResolution` command no longer has special global scope. If you want the previous behavior, use `Global Set SsrHave NoTCResolution`. -- cgit v1.2.3 From 296ac045fdfe6d6ae4875d7a6c89cad0c64c2e97 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 14 Aug 2018 11:25:19 -0400 Subject: Add a warning about abstract after being a no-op As per https://github.com/coq/coq/pull/8064#discussion_r209875616 I decided to make it a warning because it seems more flexible that way; users to are flipping back and forth between option types and not option types while designing won't have to update their `abstract after` directives to do so, and users who don't want to allow this can make it an actual error message. --- doc/sphinx/user-extensions/syntax-extensions.rst | 4 ++++ plugins/syntax/g_numeral.ml4 | 11 +++++++++++ test-suite/success/NumeralNotations.v | 15 +++++++++++++++ 3 files changed, 30 insertions(+) diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 50425c8a5d..2f7a7d42c1 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1499,6 +1499,10 @@ Numeral notations Check 90000. + .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type. + + As noted above, the :n:`(abstract after @num)` directive has no + effect when :n:`@ident__2` lands in an :g:`option` type. .. _TacticNotation: diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index a097adec24..fceb0b961f 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -66,6 +66,14 @@ let warn_abstract_large_num = pr_qualid ty ++ strbrk " are interpreted as applications of " ++ Printer.pr_constant (Global.env ()) f ++ strbrk ".") +let warn_abstract_large_num_no_op = + CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers" + (fun f -> + strbrk "The 'abstract after' directive has no effect when " ++ + strbrk "the parsing function (" ++ + Printer.pr_constant (Global.env ()) f ++ strbrk ") targets an " ++ + strbrk "option type.") + (** 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). *) @@ -468,6 +476,9 @@ let vernac_numeral_notation ty f g scope opts = num_ty = ty; warning = opts } in + (match opts, to_kind with + | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty + | _ -> ()); (* TODO: un hash suffit-il ? *) let uid = Marshal.to_string o [] in let i = Notation.( diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v index 907ec32671..2072fbbf62 100644 --- a/test-suite/success/NumeralNotations.v +++ b/test-suite/success/NumeralNotations.v @@ -160,3 +160,18 @@ Module Test9. Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope. End with_let. End Test9. + +Module Test10. + (* Test that it is only a warning to add abstract after to an optional parsing function *) + Definition to_uint (v : unit) := Nat.to_uint 0. + Definition of_uint (v : Decimal.uint) := match Nat.of_uint v with O => Some tt | _ => None end. + Definition of_any_uint (v : Decimal.uint) := tt. + Delimit Scope unit_scope with unit. + Delimit Scope unit2_scope with unit2. + Numeral Notation unit of_uint to_uint : unit_scope (abstract after 1). + Local Set Warnings Append "+abstract-large-number-no-op". + (* Check that there is actually a warning here *) + Fail Numeral Notation unit of_uint to_uint : unit2_scope (abstract after 1). + (* Check that there is no warning here *) + Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1). +End Test10. -- cgit v1.2.3 From 6a280b70fc66ff0231a9945cc3b3718385d3971c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 14 Aug 2018 14:04:08 -0400 Subject: Move g_numeral.ml4 to numeral.ml As per https://github.com/coq/coq/pull/8064#pullrequestreview-145971522 --- plugins/syntax/g_numeral.ml4 | 480 +------------------------ plugins/syntax/numeral.ml | 490 ++++++++++++++++++++++++++ plugins/syntax/numeral.mli | 21 ++ plugins/syntax/numeral_notation_plugin.mlpack | 1 + 4 files changed, 513 insertions(+), 479 deletions(-) create mode 100644 plugins/syntax/numeral.ml create mode 100644 plugins/syntax/numeral.mli diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index fceb0b961f..4e29e6a6a4 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -10,487 +10,9 @@ DECLARE PLUGIN "numeral_notation_plugin" +open Numeral open Pp -open Util open Names -open Libnames -open Globnames -open Constrexpr -open Constrexpr_ops -open Constr - -(** * 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 " ++ - Printer.pr_constant (Global.env ()) f ++ strbrk ".") - -let warn_abstract_large_num_no_op = - CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers" - (fun f -> - strbrk "The 'abstract after' directive has no effect when " ++ - strbrk "the parsing function (" ++ - Printer.pr_constant (Global.env ()) f ++ strbrk ") targets an " ++ - strbrk "option type.") - -(** 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 *) - -type int_ty = - { uint : Names.inductive; - int : Names.inductive } - -(** 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 *) - -type z_pos_ty = - { z_ty : Names.inductive; - pos_ty : Names.inductive } - -(** 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 c = match Constr.kind c with - | App (c, ca) -> - let c = glob_of_constr ?loc c in - let cel = List.map (glob_of_constr ?loc) (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)) - | _ -> let (sigma, env) = Pfedit.get_current_context () in - CErrors.user_err ?loc - (str "Unexpected term while parsing a numeral notation:" ++ fnl () ++ - Printer.pr_constr_env env sigma 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 c = - match Constr.kind c with - | App (_Some, [| _; c |]) -> glob_of_constr ?loc c - | App (_None, [| _ |]) -> no_such_number ?loc ty - | x -> let (sigma, env) = Pfedit.get_current_context () in - CErrors.user_err ?loc - (str "Unexpected non-option term while parsing a numeral notation:" ++ fnl () ++ - Printer.pr_constr_env env sigma 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) - -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 numnot_option = - | Nop - | Warning of raw_natural_number - | Abstract of raw_natural_number - -type numeral_notation_obj = - { to_kind : conversion_kind; - to_ty : Constant.t; - of_kind : conversion_kind; - of_ty : Constant.t; - num_ty : Libnames.qualid; (* for warnings / error messages *) - warning : numnot_option } - -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_constant_instance env sigma o.to_ty in - let to_ty = mkConstU 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 (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 res - | Option -> interp_option o.num_ty ?loc 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_constant_instance env sigma o.of_ty in - let of_ty = mkConstU 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 *) - -(* Here we only register the interp and uninterp functions - for a particular Numeral Notation (determined by a unique - string). The actual activation of the notation will be done - later (cf. Notation.enable_prim_token_interpretation). - This registration of interp/uninterp must be added in the - libstack, otherwise this won't work through a Require. *) - -let load_numeral_notation _ (_, (uid,opts)) = - Notation.register_rawnumeral_interpretation - ~allow_overwrite:true uid (interp opts, uninterp opts) - -let cache_numeral_notation x = load_numeral_notation 1 x - -(* TODO: substitution ? - TODO: uid pas stable par substitution dans opts - *) - -let inNumeralNotation : string * numeral_notation_obj -> Libobject.obj = - Libobject.declare_object { - (Libobject.default_object "NUMERAL NOTATION") with - Libobject.cache_function = cache_numeral_notation; - Libobject.load_function = load_numeral_notation } - -let get_constructors ind = - let mib,oib = Global.lookup_inductive ind in - let mc = oib.Declarations.mind_consnames in - Array.to_list - (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc) - -let q_z = qualid_of_string "Coq.Numbers.BinNums.Z" -let q_positive = qualid_of_string "Coq.Numbers.BinNums.positive" -let q_int = qualid_of_string "Coq.Init.Decimal.int" -let q_uint = qualid_of_string "Coq.Init.Decimal.uint" -let q_option = qualid_of_string "Coq.Init.Datatypes.option" - -let unsafe_locate_ind q = - match Nametab.locate q with - | IndRef i -> i - | _ -> raise Not_found - -let locate_ind q = - try unsafe_locate_ind q - with Not_found -> Nametab.error_global_not_found q - -let locate_z () = - try - Some { z_ty = unsafe_locate_ind q_z; - pos_ty = unsafe_locate_ind q_positive } - with Not_found -> None - -let locate_int () = - { uint = locate_ind q_uint; - int = locate_ind q_int } - -let locate_globref q = - try Nametab.locate q - with Not_found -> Nametab.error_global_not_found q - -let locate_constant q = - try Nametab.locate_constant q - with Not_found -> Nametab.error_global_not_found q - -let has_type f ty = - let (sigma, env) = Pfedit.get_current_context () in - let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in - try let _ = Constrintern.interp_constr env sigma c in true - with Pretype_errors.PretypeError _ -> false - -let type_error_to f ty loadZ = - CErrors.user_err - (pr_qualid f ++ str " should go from Decimal.int to " ++ - pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ - fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ - (if loadZ then str " (require BinNums first)." else str ".")) - -let type_error_of g ty loadZ = - CErrors.user_err - (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ - str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ - str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ - (if loadZ then str " (require BinNums first)." else str ".")) - -let vernac_numeral_notation ty f g scope opts = - let int_ty = locate_int () in - let z_pos_ty = locate_z () in - let tyc = locate_globref ty in - let to_ty = locate_constant f in - let of_ty = locate_constant g in - let cty = mkRefC ty in - let app x y = mkAppC (x,[y]) in - let cref q = mkRefC q in - let arrow x y = - mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) - in - let cZ = cref q_z in - let cint = cref q_int in - let cuint = cref q_uint in - let coption = cref q_option in - let opt r = app coption r in - (* Check that [ty] is an inductive type *) - let constructors = match tyc with - | IndRef ind -> - get_constructors ind - | ConstRef _ | ConstructRef _ | VarRef _ -> - CErrors.user_err - (pr_qualid ty ++ str " is not an inductive type") - in - (* Check the type of f *) - let to_kind = - if has_type f (arrow cint cty) then Int int_ty, Direct - else if has_type f (arrow cint (opt cty)) then Int int_ty, Option - else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct - else if has_type f (arrow cuint (opt cty)) then UInt int_ty.uint, Option - else - match z_pos_ty with - | Some z_pos_ty -> - if has_type f (arrow cZ cty) then Z z_pos_ty, Direct - else if has_type f (arrow cZ (opt cty)) then Z z_pos_ty, Option - else type_error_to f ty false - | None -> type_error_to f ty true - in - (* Check the type of g *) - let of_kind = - if has_type g (arrow cty cint) then Int int_ty, Direct - else if has_type g (arrow cty (opt cint)) then Int int_ty, Option - else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct - else if has_type g (arrow cty (opt cuint)) then UInt int_ty.uint, Option - else - match z_pos_ty with - | Some z_pos_ty -> - if has_type g (arrow cty cZ) then Z z_pos_ty, Direct - else if has_type g (arrow cty (opt cZ)) then Z z_pos_ty, Option - else type_error_of g ty false - | None -> type_error_of g ty true - in - let o = { to_kind; to_ty; of_kind; of_ty; - num_ty = ty; - warning = opts } - in - (match opts, to_kind with - | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty - | _ -> ()); - (* TODO: un hash suffit-il ? *) - let uid = Marshal.to_string o [] in - let i = Notation.( - { pt_scope = scope; - pt_uid = uid; - pt_required = Nametab.path_of_global tyc,[]; - pt_refs = constructors; - pt_in_match = true }) - in - Lib.add_anonymous_leaf (inNumeralNotation (uid,o)); - Notation.enable_prim_token_interpretation i - open Ltac_plugin open Stdarg open Pcoq.Prim diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml new file mode 100644 index 0000000000..901d4f0cb4 --- /dev/null +++ b/plugins/syntax/numeral.ml @@ -0,0 +1,490 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + 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 " ++ + Printer.pr_constant (Global.env ()) f ++ strbrk ".") + +let warn_abstract_large_num_no_op = + CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers" + (fun f -> + strbrk "The 'abstract after' directive has no effect when " ++ + strbrk "the parsing function (" ++ + Printer.pr_constant (Global.env ()) f ++ strbrk ") targets an " ++ + strbrk "option type.") + +(** 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 *) + +type int_ty = + { uint : Names.inductive; + int : Names.inductive } + +(** 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 *) + +type z_pos_ty = + { z_ty : Names.inductive; + pos_ty : Names.inductive } + +(** 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 c = match Constr.kind c with + | App (c, ca) -> + let c = glob_of_constr ?loc c in + let cel = List.map (glob_of_constr ?loc) (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)) + | _ -> let (sigma, env) = Pfedit.get_current_context () in + CErrors.user_err ?loc + (str "Unexpected term while parsing a numeral notation:" ++ fnl () ++ + Printer.pr_constr_env env sigma 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 c = + match Constr.kind c with + | App (_Some, [| _; c |]) -> glob_of_constr ?loc c + | App (_None, [| _ |]) -> no_such_number ?loc ty + | x -> let (sigma, env) = Pfedit.get_current_context () in + CErrors.user_err ?loc + (str "Unexpected non-option term while parsing a numeral notation:" ++ fnl () ++ + Printer.pr_constr_env env sigma 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) + +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 numnot_option = + | Nop + | Warning of raw_natural_number + | Abstract of raw_natural_number + +type numeral_notation_obj = + { to_kind : conversion_kind; + to_ty : Constant.t; + of_kind : conversion_kind; + of_ty : Constant.t; + num_ty : Libnames.qualid; (* for warnings / error messages *) + warning : numnot_option } + +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_constant_instance env sigma o.to_ty in + let to_ty = mkConstU 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 (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 res + | Option -> interp_option o.num_ty ?loc 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_constant_instance env sigma o.of_ty in + let of_ty = mkConstU 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 *) + +(* Here we only register the interp and uninterp functions + for a particular Numeral Notation (determined by a unique + string). The actual activation of the notation will be done + later (cf. Notation.enable_prim_token_interpretation). + This registration of interp/uninterp must be added in the + libstack, otherwise this won't work through a Require. *) + +let load_numeral_notation _ (_, (uid,opts)) = + Notation.register_rawnumeral_interpretation + ~allow_overwrite:true uid (interp opts, uninterp opts) + +let cache_numeral_notation x = load_numeral_notation 1 x + +(* TODO: substitution ? + TODO: uid pas stable par substitution dans opts + *) + +let inNumeralNotation : string * numeral_notation_obj -> Libobject.obj = + Libobject.declare_object { + (Libobject.default_object "NUMERAL NOTATION") with + Libobject.cache_function = cache_numeral_notation; + Libobject.load_function = load_numeral_notation } + +let get_constructors ind = + let mib,oib = Global.lookup_inductive ind in + let mc = oib.Declarations.mind_consnames in + Array.to_list + (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc) + +let q_z = qualid_of_string "Coq.Numbers.BinNums.Z" +let q_positive = qualid_of_string "Coq.Numbers.BinNums.positive" +let q_int = qualid_of_string "Coq.Init.Decimal.int" +let q_uint = qualid_of_string "Coq.Init.Decimal.uint" +let q_option = qualid_of_string "Coq.Init.Datatypes.option" + +let unsafe_locate_ind q = + match Nametab.locate q with + | IndRef i -> i + | _ -> raise Not_found + +let locate_ind q = + try unsafe_locate_ind q + with Not_found -> Nametab.error_global_not_found q + +let locate_z () = + try + Some { z_ty = unsafe_locate_ind q_z; + pos_ty = unsafe_locate_ind q_positive } + with Not_found -> None + +let locate_int () = + { uint = locate_ind q_uint; + int = locate_ind q_int } + +let locate_globref q = + try Nametab.locate q + with Not_found -> Nametab.error_global_not_found q + +let locate_constant q = + try Nametab.locate_constant q + with Not_found -> Nametab.error_global_not_found q + +let has_type f ty = + let (sigma, env) = Pfedit.get_current_context () in + let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in + try let _ = Constrintern.interp_constr env sigma c in true + with Pretype_errors.PretypeError _ -> false + +let type_error_to f ty loadZ = + CErrors.user_err + (pr_qualid f ++ str " should go from Decimal.int to " ++ + pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ + fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ + (if loadZ then str " (require BinNums first)." else str ".")) + +let type_error_of g ty loadZ = + CErrors.user_err + (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ + str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ + str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ + (if loadZ then str " (require BinNums first)." else str ".")) + +let vernac_numeral_notation ty f g scope opts = + let int_ty = locate_int () in + let z_pos_ty = locate_z () in + let tyc = locate_globref ty in + let to_ty = locate_constant f in + let of_ty = locate_constant g in + let cty = mkRefC ty in + let app x y = mkAppC (x,[y]) in + let cref q = mkRefC q in + let arrow x y = + mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) + in + let cZ = cref q_z in + let cint = cref q_int in + let cuint = cref q_uint in + let coption = cref q_option in + let opt r = app coption r in + (* Check that [ty] is an inductive type *) + let constructors = match tyc with + | IndRef ind -> + get_constructors ind + | ConstRef _ | ConstructRef _ | VarRef _ -> + CErrors.user_err + (pr_qualid ty ++ str " is not an inductive type") + in + (* Check the type of f *) + let to_kind = + if has_type f (arrow cint cty) then Int int_ty, Direct + else if has_type f (arrow cint (opt cty)) then Int int_ty, Option + else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct + else if has_type f (arrow cuint (opt cty)) then UInt int_ty.uint, Option + else + match z_pos_ty with + | Some z_pos_ty -> + if has_type f (arrow cZ cty) then Z z_pos_ty, Direct + else if has_type f (arrow cZ (opt cty)) then Z z_pos_ty, Option + else type_error_to f ty false + | None -> type_error_to f ty true + in + (* Check the type of g *) + let of_kind = + if has_type g (arrow cty cint) then Int int_ty, Direct + else if has_type g (arrow cty (opt cint)) then Int int_ty, Option + else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct + else if has_type g (arrow cty (opt cuint)) then UInt int_ty.uint, Option + else + match z_pos_ty with + | Some z_pos_ty -> + if has_type g (arrow cty cZ) then Z z_pos_ty, Direct + else if has_type g (arrow cty (opt cZ)) then Z z_pos_ty, Option + else type_error_of g ty false + | None -> type_error_of g ty true + in + let o = { to_kind; to_ty; of_kind; of_ty; + num_ty = ty; + warning = opts } + in + (match opts, to_kind with + | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty + | _ -> ()); + (* TODO: un hash suffit-il ? *) + let uid = Marshal.to_string o [] in + let i = Notation.( + { pt_scope = scope; + pt_uid = uid; + pt_required = Nametab.path_of_global tyc,[]; + pt_refs = constructors; + pt_in_match = true }) + in + Lib.add_anonymous_leaf (inNumeralNotation (uid,o)); + Notation.enable_prim_token_interpretation i diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli new file mode 100644 index 0000000000..2ad3574fe7 --- /dev/null +++ b/plugins/syntax/numeral.mli @@ -0,0 +1,21 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit diff --git a/plugins/syntax/numeral_notation_plugin.mlpack b/plugins/syntax/numeral_notation_plugin.mlpack index 643c148979..f4d9cae3ff 100644 --- a/plugins/syntax/numeral_notation_plugin.mlpack +++ b/plugins/syntax/numeral_notation_plugin.mlpack @@ -1 +1,2 @@ +Numeral G_numeral -- cgit v1.2.3 From 581bbbb23fcb488d5c1a10f360a6705a6792b2b1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 14 Aug 2018 20:19:07 -0400 Subject: Add periods in response to PR comments --- doc/sphinx/user-extensions/syntax-extensions.rst | 6 +++--- plugins/syntax/numeral.ml | 12 +++++++----- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 2f7a7d42c1..6f655340da 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1443,19 +1443,19 @@ Numeral notations The printing function given to the :cmd:`Numeral Notation` vernacular is not of the right type. - .. exn:: @type is not an inductive type + .. exn:: @type is not an inductive type. Numeral notations can only be declared for inductive types with no arguments. - .. exn:: Unexpected term while parsing a numeral notation + .. exn:: Unexpected term @term while parsing a numeral notation. Parsing functions must always return ground terms, made up of applications of constructors and inductive types. Parsing functions may not return terms containing axioms, bare (co)fixpoints, lambdas, etc. - .. exn:: Unexpected non-option term while parsing a numeral notation + .. exn:: Unexpected non-option term @term while parsing a numeral notation. Parsing functions expected to return an :g:`option` must always return a concrete :g:`Some` or :g:`None` when applied to a diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 901d4f0cb4..8dced1a8de 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -242,8 +242,9 @@ let rec glob_of_constr ?loc c = match Constr.kind c with | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None)) | _ -> let (sigma, env) = Pfedit.get_current_context () in CErrors.user_err ?loc - (str "Unexpected term while parsing a numeral notation:" ++ fnl () ++ - Printer.pr_constr_env env sigma c) + (strbrk "Unexpected term " ++ + Printer.pr_constr_env env sigma c ++ + strbrk " while parsing a numeral notation.") let no_such_number ?loc ty = CErrors.user_err ?loc @@ -256,8 +257,9 @@ let interp_option ty ?loc c = | App (_None, [| _ |]) -> no_such_number ?loc ty | x -> let (sigma, env) = Pfedit.get_current_context () in CErrors.user_err ?loc - (str "Unexpected non-option term while parsing a numeral notation:" ++ fnl () ++ - Printer.pr_constr_env env sigma c) + (strbrk "Unexpected non-option term " ++ + Printer.pr_constr_env env sigma c ++ + strbrk " while parsing a numeral notation.") let uninterp_option c = match Constr.kind c with @@ -440,7 +442,7 @@ let vernac_numeral_notation ty f g scope opts = get_constructors ind | ConstRef _ | ConstructRef _ | VarRef _ -> CErrors.user_err - (pr_qualid ty ++ str " is not an inductive type") + (pr_qualid ty ++ str " is not an inductive type.") in (* Check the type of f *) let to_kind = -- cgit v1.2.3 From 14626ba6a27323ac5a329c9f246bf64282738e5e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 15 Aug 2018 11:03:42 -0400 Subject: Add Numeral Notation GlobRef printing/parsing Now we support using inductive constructors and section-local variables as numeral notation printing and parsing functions. I'm not sure that I got the econstr conversion right. --- plugins/syntax/numeral.ml | 24 ++++++++---------- test-suite/success/NumeralNotations.v | 48 ++++++++++++++++++++++++++--------- 2 files changed, 46 insertions(+), 26 deletions(-) diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 8dced1a8de..6f657fc3a5 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -62,14 +62,14 @@ let warn_abstract_large_num = (fun (ty,f) -> strbrk "To avoid stack overflow, large numbers in " ++ pr_qualid ty ++ strbrk " are interpreted as applications of " ++ - Printer.pr_constant (Global.env ()) f ++ strbrk ".") + Printer.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".") let warn_abstract_large_num_no_op = CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers" (fun f -> strbrk "The 'abstract after' directive has no effect when " ++ strbrk "the parsing function (" ++ - Printer.pr_constant (Global.env ()) f ++ strbrk ") targets an " ++ + Printer.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++ strbrk "option type.") (** Comparing two raw numbers (base 10, big-endian, non-negative). @@ -288,9 +288,9 @@ type numnot_option = type numeral_notation_obj = { to_kind : conversion_kind; - to_ty : Constant.t; + to_ty : GlobRef.t; of_kind : conversion_kind; - of_ty : Constant.t; + of_ty : GlobRef.t; num_ty : Libnames.qualid; (* for warnings / error messages *) warning : numnot_option } @@ -308,8 +308,8 @@ let interp o ?loc n = in let env = Global.env () in let sigma = Evd.from_env env in - let sigma,to_ty = Evd.fresh_constant_instance env sigma o.to_ty in - let to_ty = mkConstU to_ty 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); @@ -323,8 +323,8 @@ let interp o ?loc n = 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_constant_instance env sigma o.of_ty in - let of_ty = mkConstU of_ty 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 @@ -395,10 +395,6 @@ let locate_globref q = try Nametab.locate q with Not_found -> Nametab.error_global_not_found q -let locate_constant q = - try Nametab.locate_constant q - with Not_found -> Nametab.error_global_not_found q - let has_type f ty = let (sigma, env) = Pfedit.get_current_context () in let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in @@ -423,8 +419,8 @@ let vernac_numeral_notation ty f g scope opts = let int_ty = locate_int () in let z_pos_ty = locate_z () in let tyc = locate_globref ty in - let to_ty = locate_constant f in - let of_ty = locate_constant g in + let to_ty = locate_globref f in + let of_ty = locate_globref g in let cty = mkRefC ty in let app x y = mkAppC (x,[y]) in let cref q = mkRefC q in diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v index 2072fbbf62..e63b9dc4c7 100644 --- a/test-suite/success/NumeralNotations.v +++ b/test-suite/success/NumeralNotations.v @@ -123,42 +123,52 @@ End Test6_2. Module Test7. Local Set Primitive Projections. - Record > wuint := wrap { unwrap : Decimal.uint }. + Record wuint := wrap { unwrap : Decimal.uint }. Delimit Scope wuint_scope with wuint. - Fail Numeral Notation wuint wrap unwrap : wuint_scope. + Numeral Notation wuint wrap unwrap : wuint_scope. + Check let v := 0%wuint in v : wuint. + Check let v := 1%wuint in v : wuint. End Test7. Module Test8. Local Set Primitive Projections. - Record > wuint := wrap { unwrap : Decimal.uint }. - Delimit Scope wuint_scope with wuint. + Record wuint := wrap { unwrap : Decimal.uint }. + Delimit Scope wuint8_scope with wuint8. + Delimit Scope wuint8'_scope with wuint8'. Section with_var. Context (dummy : unit). Definition wrap' := let __ := dummy in wrap. Definition unwrap' := let __ := dummy in unwrap. - Global Numeral Notation wuint wrap' unwrap' : wuint_scope. - Check let v := 0%wuint in v : wuint. + Global Numeral Notation wuint wrap' unwrap' : wuint8_scope. + Check let v := 0%wuint8 in v : wuint. End with_var. - Fail Check let v := 0%wuint in v : wuint. + Check let v := 0%wuint8 in v : nat. + Fail Check let v := 0%wuint8 in v : wuint. Compute wrap (Nat.to_uint 0). Notation wrap'' := wrap. Notation unwrap'' := unwrap. - Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope. + Fail Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope. + Fail Check let v := 0%wuint8' in v : wuint. End Test8. Module Test9. + Delimit Scope wuint9_scope with wuint9. + Delimit Scope wuint9'_scope with wuint9'. Section with_let. Local Set Primitive Projections. - Record > wuint := wrap { unwrap : Decimal.uint }. + Record wuint := wrap { unwrap : Decimal.uint }. Let wrap' := wrap. Let unwrap' := unwrap. Local Notation wrap'' := wrap. Local Notation unwrap'' := unwrap. - Delimit Scope wuint_scope with wuint. - Fail Numeral Notation wuint wrap' unwrap' : wuint_scope. - Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope. + Numeral Notation wuint wrap' unwrap' : wuint9_scope. + Check let v := 0%wuint9 in v : wuint. + Fail Numeral Notation wuint wrap'' unwrap'' : wuint9'_scope. + Fail Check let v := 0%wuint9' in v : wuint. End with_let. + Check let v := 0%wuint9 in v : nat. + Fail Check let v := 0%wuint9 in v : wuint. End Test9. Module Test10. @@ -175,3 +185,17 @@ Module Test10. (* Check that there is no warning here *) Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1). End Test10. + +Module Test11. + (* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *) + Inductive unit11 := tt11. + Delimit Scope unit11_scope with unit11. + Goal True. + evar (to_uint : unit11 -> Decimal.uint). + evar (of_uint : Decimal.uint -> unit11). + Fail Numeral Notation unit11 of_uint to_uint : uint11_scope. + exact I. + Unshelve. + all: solve [ constructor ]. + Qed. +End Test11. -- cgit v1.2.3 From 548976ac825298f27e6be00bbbb1be0752568f6f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 16 Aug 2018 10:35:11 -0400 Subject: [numeral notations] support aliases Aliases of global references can now be used in numeral notations --- doc/sphinx/user-extensions/syntax-extensions.rst | 8 +++-- plugins/syntax/numeral.ml | 21 ++++---------- test-suite/success/NumeralNotations.v | 37 +++++++++++++++++++++--- 3 files changed, 44 insertions(+), 22 deletions(-) diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 6f655340da..886ca0472a 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1474,9 +1474,13 @@ Numeral notations .. exn:: The reference @ident was not found in the current environment. + Identifiers passed to :cmd:`Numeral Notation` must exist in the + global environment. + + .. exn:: @ident is bound to a notation that does not denote a reference. + Identifiers passed to :cmd:`Numeral Notation` must be global - definitions, not notations, section variables, section-local - :g:`Let` bound identifiers, etc. + references, or notations which denote to single identifiers. .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 6f657fc3a5..321992eda6 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -391,10 +391,6 @@ let locate_int () = { uint = locate_ind q_uint; int = locate_ind q_int } -let locate_globref q = - try Nametab.locate q - with Not_found -> Nametab.error_global_not_found q - let has_type f ty = let (sigma, env) = Pfedit.get_current_context () in let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in @@ -418,9 +414,9 @@ let type_error_of g ty loadZ = let vernac_numeral_notation ty f g scope opts = let int_ty = locate_int () in let z_pos_ty = locate_z () in - let tyc = locate_globref ty in - let to_ty = locate_globref f in - let of_ty = locate_globref g in + let tyc = Smartlocate.global_inductive_with_alias ty in + let to_ty = Smartlocate.global_with_alias f in + let of_ty = Smartlocate.global_with_alias g in let cty = mkRefC ty in let app x y = mkAppC (x,[y]) in let cref q = mkRefC q in @@ -432,14 +428,7 @@ let vernac_numeral_notation ty f g scope opts = let cuint = cref q_uint in let coption = cref q_option in let opt r = app coption r in - (* Check that [ty] is an inductive type *) - let constructors = match tyc with - | IndRef ind -> - get_constructors ind - | ConstRef _ | ConstructRef _ | VarRef _ -> - CErrors.user_err - (pr_qualid ty ++ str " is not an inductive type.") - in + let constructors = get_constructors tyc in (* Check the type of f *) let to_kind = if has_type f (arrow cint cty) then Int int_ty, Direct @@ -480,7 +469,7 @@ let vernac_numeral_notation ty f g scope opts = let i = Notation.( { pt_scope = scope; pt_uid = uid; - pt_required = Nametab.path_of_global tyc,[]; + pt_required = Nametab.path_of_global (IndRef tyc),[]; pt_refs = constructors; pt_in_match = true }) in diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v index e63b9dc4c7..5a58a1b72d 100644 --- a/test-suite/success/NumeralNotations.v +++ b/test-suite/success/NumeralNotations.v @@ -148,8 +148,8 @@ Module Test8. Notation wrap'' := wrap. Notation unwrap'' := unwrap. - Fail Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope. - Fail Check let v := 0%wuint8' in v : wuint. + Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope. + Check let v := 0%wuint8' in v : wuint. End Test8. Module Test9. @@ -164,8 +164,8 @@ Module Test9. Local Notation unwrap'' := unwrap. Numeral Notation wuint wrap' unwrap' : wuint9_scope. Check let v := 0%wuint9 in v : wuint. - Fail Numeral Notation wuint wrap'' unwrap'' : wuint9'_scope. - Fail Check let v := 0%wuint9' in v : wuint. + Numeral Notation wuint wrap'' unwrap'' : wuint9'_scope. + Check let v := 0%wuint9' in v : wuint. End with_let. Check let v := 0%wuint9 in v : nat. Fail Check let v := 0%wuint9 in v : wuint. @@ -199,3 +199,32 @@ Module Test11. all: solve [ constructor ]. Qed. End Test11. + +Module Test12. + (* Test for numeral notations on context variables *) + Delimit Scope test12_scope with test12. + Section test12. + Context (to_uint : unit -> Decimal.uint) (of_uint : Decimal.uint -> unit). + + Numeral Notation unit of_uint to_uint : test12_scope. + Check let v := 1%test12 in v : unit. + End test12. +End Test12. + +Module Test13. + (* Test for numeral notations on notations which do not denote references *) + Delimit Scope test13_scope with test13. + Delimit Scope test13'_scope with test13'. + Delimit Scope test13''_scope with test13''. + Definition to_uint (x y : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Definition to_uint_good := to_uint tt. + Notation to_uint' := (to_uint tt). + Notation to_uint'' := (to_uint _). + Numeral Notation unit of_uint to_uint_good : test13_scope. + Check let v := 0%test13 in v : unit. + Fail Numeral Notation unit of_uint to_uint' : test13'_scope. + Fail Check let v := 0%test13' in v : unit. + Fail Numeral Notation unit of_uint to_uint'' : test13''_scope. + Fail Check let v := 0%test13'' in v : unit. +End Test13. -- cgit v1.2.3 From 6dcbbeb95682bbf470e58e25e0a357a84c3283b6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Aug 2018 11:03:29 -0400 Subject: Make Numeral Notation follow Import, not Require Because that's the sane thing to do. This will inevitably cause issues for projects which do not `Import Coq.Strings.Ascii` before trying to use ascii notations. We also move the syntax plugin for `int31` notations from `Cyclic31` to `Int31`, so that users (like CompCert) who merely `Require Import Coq.Numbers.Cyclic.Int31.Int31` get the `int31` numeral syntax. Since `Cyclic31` `Export`s `Int31`, this should not cause any additional incompatibilities. --- CHANGES | 18 ++++++++++++++++++ interp/notation.ml | 2 +- test-suite/success/Compat88.v | 18 ++++++++++++++++++ test-suite/success/NumeralNotations.v | 19 +++++++++++++++++++ theories/Compat/Coq88.v | 14 ++++++++++++++ theories/NArith/BinNat.v | 2 ++ theories/NArith/BinNatDef.v | 3 +++ theories/Numbers/Cyclic/Int31/Cyclic31.v | 4 +--- theories/Numbers/Cyclic/Int31/Int31.v | 2 ++ theories/PArith/BinPos.v | 2 ++ theories/PArith/BinPosDef.v | 3 +++ theories/ZArith/BinInt.v | 2 ++ theories/ZArith/BinIntDef.v | 3 +++ 13 files changed, 88 insertions(+), 4 deletions(-) create mode 100644 test-suite/success/Compat88.v diff --git a/CHANGES b/CHANGES index b1f9d46ed8..5d1c9a9c2d 100644 --- a/CHANGES +++ b/CHANGES @@ -69,6 +69,24 @@ Standard Library `dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect and other packages. They are still delimited by `%int` and `%uint`. +- Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`, + and `int31` are no longer available merely by `Require`ing the files + that define the inductives. You must `Import` `Coq.Strings.String`, + `Coq.Strings.Ascii`, `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`, + `Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and + `Coq.Numbers.Cyclic.Int31.Int31`, respectively, to be able to use + these notations. Note that passing `-compat 8.8` or issuing + `Require Import Coq.Compat.Coq88` will make these notations + available. Users wishing to port their developments automatically + may download `fix.py` from + + and run a command like `while true; do make -Okj 2>&1 | + /path/to/fix.py; done` and get a cup of coffee. (This command must + be manually interrupted once the build finishes all the way though. + Note also that this method is not fail-proof; you may have to adjust + some scopes if you were relying on string notations not being + available even when `string_scope` was open.) + - Numeral syntax for `nat` is no longer available without loading the entire prelude (`Require Import Coq.Init.Prelude`). This only impacts users running Coq without the init library (`-nois` or diff --git a/interp/notation.ml b/interp/notation.ml index 56d6acbdae..d6bd62e121 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -431,8 +431,8 @@ let subst_prim_token_interpretation (subs,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; - load_function = (fun _ -> cache_prim_token_interpretation); subst_function = subst_prim_token_interpretation; classify_function = (fun o -> Substitute o)} diff --git a/test-suite/success/Compat88.v b/test-suite/success/Compat88.v new file mode 100644 index 0000000000..e2045900d5 --- /dev/null +++ b/test-suite/success/Compat88.v @@ -0,0 +1,18 @@ +(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(** Check that various syntax usage is available without importing + relevant files. *) +Require Coq.Strings.Ascii Coq.Strings.String. +Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef. +Require Coq.Reals.Rdefinitions. +Require Coq.Numbers.Cyclic.Int31.Cyclic31. + +Require Import Coq.Compat.Coq88. (* XXX FIXME Should not need [Require], see https://github.com/coq/coq/issues/8311 *) + +Check String.String "a" String.EmptyString. +Check String.eqb "a" "a". +Check Nat.eqb 1 1. +Check BinNat.N.eqb 1 1. +Check BinInt.Z.eqb 1 1. +Check BinPos.Pos.eqb 1 1. +Check Rdefinitions.Rplus 1 1. +Check Int31.iszero 1. diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v index 5a58a1b72d..bacc982ccc 100644 --- a/test-suite/success/NumeralNotations.v +++ b/test-suite/success/NumeralNotations.v @@ -228,3 +228,22 @@ Module Test13. Fail Numeral Notation unit of_uint to_uint'' : test13''_scope. Fail Check let v := 0%test13'' in v : unit. End Test13. + +Module Test14. + (* Test that numeral notations follow [Import], not [Require], and + also test for current (INCORRECT!!) behavior that [Local] has no + effect in modules. *) + Delimit Scope test14_scope with test14. + Delimit Scope test14'_scope with test14'. + Module Inner. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Local Numeral Notation unit of_uint to_uint : test14_scope. + Global Numeral Notation unit of_uint to_uint : test14'_scope. + End Inner. + Fail Check let v := 0%test14 in v : unit. + Fail Check let v := 0%test14' in v : unit. + Import Inner. + Check let v := 0%test14 in v : unit. (* THIS SHOULD FAIL!! *) + Check let v := 0%test14' in v : unit. +End Test14. diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v index 4142af05d2..578425bfb5 100644 --- a/theories/Compat/Coq88.v +++ b/theories/Compat/Coq88.v @@ -9,3 +9,17 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.8 *) +(** In Coq 8.9, prim token notations follow [Import] rather than + [Require]. So we make all of the relevant notations accessible in + compatibility mode. *) +Require Coq.Strings.Ascii Coq.Strings.String. +Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef. +Require Coq.Reals.Rdefinitions. +Require Coq.Numbers.Cyclic.Int31.Int31. +Declare ML Module "string_syntax_plugin". +Declare ML Module "ascii_syntax_plugin". +Declare ML Module "r_syntax_plugin". +Declare ML Module "int31_syntax_plugin". +Numeral Notation BinNums.Z BinIntDef.Z.of_int BinIntDef.Z.to_int : Z_scope. +Numeral Notation BinNums.positive BinPosDef.Pos.of_int BinPosDef.Pos.to_int : positive_scope. +Numeral Notation BinNums.N BinNatDef.N.of_int BinNatDef.N.to_int : N_scope. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 5d3ec5abc7..bd27f94abd 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -930,6 +930,8 @@ Bind Scope N_scope with N.t N. (** Exportation of notations *) +Numeral Notation N N.of_uint N.to_uint : N_scope. + Infix "+" := N.add : N_scope. Infix "-" := N.sub : N_scope. Infix "*" := N.mul : N_scope. diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 8bbecf9acb..be12fffaaf 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -402,6 +402,9 @@ Definition to_uint n := Definition to_int n := Decimal.Pos (to_uint n). +Numeral Notation N of_uint to_uint : N_scope. + End N. +(** Re-export the notation for those who just [Import NatIntDef] *) Numeral Notation N N.of_uint N.to_uint : N_scope. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index bd4f0279d4..ec480bb1eb 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -23,8 +23,6 @@ Require Import Zpow_facts. Require Import CyclicAxioms. Require Import ROmega. -Declare ML Module "int31_syntax_plugin". - Local Open Scope nat_scope. Local Open Scope int31_scope. @@ -128,7 +126,7 @@ Section Basics. Lemma nshiftl_S_tail : forall n x, nshiftl x (S n) = nshiftl (shiftl x) n. - Proof. + Proof. intros n; elim n; simpl; intros; now f_equal. Qed. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 9f8da831d8..39af62c32f 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -15,6 +15,8 @@ Require Import Wf_nat. Require Export ZArith. Require Export DoubleType. +Declare ML Module "int31_syntax_plugin". + (** * 31-bit integers *) (** This file contains basic definitions of a 31-bit integer diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 000d895e10..dcaae1606d 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1871,6 +1871,8 @@ Bind Scope positive_scope with Pos.t positive. (** Exportation of notations *) +Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. + Infix "+" := Pos.add : positive_scope. Infix "-" := Pos.sub : positive_scope. Infix "*" := Pos.mul : positive_scope. diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 39b609e9dd..7f30733559 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -616,6 +616,9 @@ Definition to_uint p := Decimal.rev (to_little_uint p). Definition to_int n := Decimal.Pos (to_uint n). +Numeral Notation positive of_int to_uint : positive_scope. + End Pos. +(** Re-export the notation for those who just [Import BinPosDef] *) Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index cf7397b57e..a11d491a8b 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1248,6 +1248,8 @@ Bind Scope Z_scope with Z.t Z. (** Re-export Notations *) +Numeral Notation Z Z.of_int Z.to_int : Z_scope. + Infix "+" := Z.add : Z_scope. Notation "- x" := (Z.opp x) : Z_scope. Infix "-" := Z.sub : Z_scope. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index 8abcd15700..8cb62622db 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -639,6 +639,9 @@ Definition lxor a b := | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b)) end. +Numeral Notation Z of_int to_int : Z_scope. + End Z. +(** Re-export the notation for those who just [Import BinIntDef] *) Numeral Notation Z Z.of_int Z.to_int : Z_scope. -- cgit v1.2.3 From e9d44aefa9d6058c72845788745468aa010708b5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Aug 2018 15:10:58 -0400 Subject: Make Numeral Notation obey Local/Global Thanks to Emilio and Pierre-Marie Pédrot for pointers. --- interp/notation.ml | 16 +++++++++++----- interp/notation.mli | 5 +++-- plugins/syntax/ascii_syntax.ml | 3 ++- plugins/syntax/g_numeral.ml4 | 3 ++- plugins/syntax/int31_syntax.ml | 3 ++- plugins/syntax/numeral.ml | 5 +++-- plugins/syntax/numeral.mli | 3 ++- plugins/syntax/r_syntax.ml | 3 ++- plugins/syntax/string_syntax.ml | 3 ++- test-suite/success/NumeralNotations.v | 22 ++++++++++++++++++---- 10 files changed, 47 insertions(+), 19 deletions(-) diff --git a/interp/notation.ml b/interp/notation.ml index d6bd62e121..551f1bfa83 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -407,6 +407,7 @@ let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninter (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp) type prim_token_infos = { + pt_local : bool; (** Is this interpretation local? *) pt_scope : scope_name; (** Concerned scope *) pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) pt_required : required_module; (** Module that should be loaded first *) @@ -429,12 +430,15 @@ 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 = (fun o -> Substitute o)} + classify_function = classify_prim_token_interpretation} let enable_prim_token_interpretation infos = Lib.add_anonymous_leaf (inPrimTokenInterp infos) @@ -450,20 +454,22 @@ let fresh_string_of = let count = ref 0 in fun root -> count := !count+1; (string_of_int !count)^"_"^root -let declare_numeral_interpreter sc dir interp (patl,uninterp,b) = +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_scope = sc; + { pt_local = local; + pt_scope = sc; pt_uid = uid; pt_required = dir; pt_refs = List.map_filter glob_prim_constr_key patl; pt_in_match = b } -let declare_string_interpreter sc dir interp (patl,uninterp,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_scope = sc; + { pt_local = local; + pt_scope = sc; pt_uid = uid; pt_required = dir; pt_refs = List.map_filter glob_prim_constr_key patl; diff --git a/interp/notation.mli b/interp/notation.mli index 1d01d75c82..e5478eff48 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -100,6 +100,7 @@ val register_string_interpretation : ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit type prim_token_infos = { + pt_local : bool; (** Is this interpretation local? *) pt_scope : scope_name; (** Concerned scope *) pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) pt_required : required_module; (** Module that should be loaded first *) @@ -123,10 +124,10 @@ val enable_prim_token_interpretation : prim_token_infos -> unit (the latter inside a [Mltop.declare_cache_obj]). *) -val declare_numeral_interpreter : scope_name -> required_module -> +val declare_numeral_interpreter : ?local:bool -> scope_name -> required_module -> Bigint.bigint prim_token_interpreter -> glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit -val declare_string_interpreter : scope_name -> required_module -> +val declare_string_interpreter : ?local:bool -> scope_name -> required_module -> string prim_token_interpreter -> glob_constr list * string prim_token_uninterpreter * bool -> unit diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 9bf0b29b61..5e36fbeb81 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -92,7 +92,8 @@ let _ = let sc = "char_scope" in register_string_interpretation sc (interp_ascii_string,uninterp_ascii_string); at_declare_ml_module enable_prim_token_interpretation - { pt_scope = sc; + { pt_local = false; + pt_scope = sc; pt_uid = sc; pt_required = (ascii_path,ascii_module); pt_refs = [static_glob_Ascii]; diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index 4e29e6a6a4..ec14df3baa 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -13,6 +13,7 @@ DECLARE PLUGIN "numeral_notation_plugin" open Numeral open Pp open Names +open Vernacinterp open Ltac_plugin open Stdarg open Pcoq.Prim @@ -32,5 +33,5 @@ END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(o) ] -> - [ vernac_numeral_notation ty f g (Id.to_string sc) o ] + [ vernac_numeral_notation (Locality.make_module_locality atts.locality) ty f g (Id.to_string sc) o ] END diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml index 731eae349a..d3ffe936a9 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -106,7 +106,8 @@ let at_declare_ml_module f x = let _ = register_bignumeral_interpretation int31_scope (interp_int31,uninterp_int31); at_declare_ml_module enable_prim_token_interpretation - { pt_scope = int31_scope; + { pt_local = false; + pt_scope = int31_scope; pt_uid = int31_scope; pt_required = (int31_path,int31_module); pt_refs = [int31_construct]; diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 321992eda6..fee93593d0 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -411,7 +411,7 @@ let type_error_of g ty loadZ = str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ (if loadZ then str " (require BinNums first)." else str ".")) -let vernac_numeral_notation ty f g scope opts = +let vernac_numeral_notation local ty f g scope opts = let int_ty = locate_int () in let z_pos_ty = locate_z () in let tyc = Smartlocate.global_inductive_with_alias ty in @@ -467,7 +467,8 @@ let vernac_numeral_notation ty f g scope opts = (* TODO: un hash suffit-il ? *) let uid = Marshal.to_string o [] in let i = Notation.( - { pt_scope = scope; + { pt_local = local; + pt_scope = scope; pt_uid = uid; pt_required = Nametab.path_of_global (IndRef tyc),[]; pt_refs = constructors; diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli index 2ad3574fe7..83ede6f48f 100644 --- a/plugins/syntax/numeral.mli +++ b/plugins/syntax/numeral.mli @@ -10,6 +10,7 @@ open Libnames open Constrexpr +open Vernacexpr (** * Numeral notation *) @@ -18,4 +19,4 @@ type numnot_option = | Warning of raw_natural_number | Abstract of raw_natural_number -val vernac_numeral_notation : qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit +val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index eccc544e41..04946c158b 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -141,7 +141,8 @@ let r_scope = "R_scope" let _ = register_bignumeral_interpretation r_scope (r_of_int,uninterp_r); at_declare_ml_module enable_prim_token_interpretation - { pt_scope = r_scope; + { pt_local = false; + pt_scope = r_scope; pt_uid = r_scope; pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]); pt_refs = [glob_IZR]; diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index ca1bf0df27..640bcfde91 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -73,7 +73,8 @@ let _ = let sc = "string_scope" in register_string_interpretation sc (interp_string,uninterp_string); at_declare_ml_module enable_prim_token_interpretation - { pt_scope = sc; + { pt_local = false; + pt_scope = sc; pt_uid = sc; pt_required = (string_path,["Coq";"Strings";"String"]); pt_refs = [static_glob_String; static_glob_EmptyString]; diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v index bacc982ccc..4521ad0e37 100644 --- a/test-suite/success/NumeralNotations.v +++ b/test-suite/success/NumeralNotations.v @@ -139,7 +139,7 @@ Module Test8. Context (dummy : unit). Definition wrap' := let __ := dummy in wrap. Definition unwrap' := let __ := dummy in unwrap. - Global Numeral Notation wuint wrap' unwrap' : wuint8_scope. + Numeral Notation wuint wrap' unwrap' : wuint8_scope. Check let v := 0%wuint8 in v : wuint. End with_var. Check let v := 0%wuint8 in v : nat. @@ -231,19 +231,33 @@ End Test13. Module Test14. (* Test that numeral notations follow [Import], not [Require], and - also test for current (INCORRECT!!) behavior that [Local] has no - effect in modules. *) + also test that [Local Numeral Notation]s do not escape modules + nor sections. *) Delimit Scope test14_scope with test14. Delimit Scope test14'_scope with test14'. + Delimit Scope test14''_scope with test14''. + Delimit Scope test14'''_scope with test14'''. Module Inner. Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. Definition of_uint (x : Decimal.uint) : unit := tt. Local Numeral Notation unit of_uint to_uint : test14_scope. Global Numeral Notation unit of_uint to_uint : test14'_scope. + Check let v := 0%test14 in v : unit. + Check let v := 0%test14' in v : unit. End Inner. Fail Check let v := 0%test14 in v : unit. Fail Check let v := 0%test14' in v : unit. Import Inner. - Check let v := 0%test14 in v : unit. (* THIS SHOULD FAIL!! *) + Fail Check let v := 0%test14 in v : unit. Check let v := 0%test14' in v : unit. + Section InnerSection. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Local Numeral Notation unit of_uint to_uint : test14''_scope. + Fail Global Numeral Notation unit of_uint to_uint : test14'''_scope. + Check let v := 0%test14'' in v : unit. + Fail Check let v := 0%test14''' in v : unit. + End InnerSection. + Fail Check let v := 0%test14'' in v : unit. + Fail Check let v := 0%test14''' in v : unit. End Test14. -- cgit v1.2.3 From 31d58c9ee979699e733a561ec4eef6b0829fe73a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 31 Aug 2018 15:22:26 -0400 Subject: Add some module tests to numeral notations --- test-suite/success/NumeralNotations.v | 41 +++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v index 4521ad0e37..4a275de5b5 100644 --- a/test-suite/success/NumeralNotations.v +++ b/test-suite/success/NumeralNotations.v @@ -261,3 +261,44 @@ Module Test14. Fail Check let v := 0%test14'' in v : unit. Fail Check let v := 0%test14''' in v : unit. End Test14. + +Module Test15. + (** Test module include *) + Delimit Scope test15_scope with test15. + Module Inner. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Numeral Notation unit of_uint to_uint : test15_scope. + Check let v := 0%test15 in v : unit. + End Inner. + Module Inner2. + Include Inner. + Check let v := 0%test15 in v : unit. + End Inner2. + Import Inner Inner2. + Check let v := 0%test15 in v : unit. +End Test15. + +Module Test16. + (** Test functors *) + Delimit Scope test16_scope with test16. + Module Type A. + Axiom T : Set. + Axiom t : T. + End A. + Module F (a : A). + Inductive Foo := foo (_ : a.T). + Definition to_uint (x : Foo) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : Foo := foo a.t. + Numeral Notation Foo of_uint to_uint : test16_scope. + Check let v := 0%test16 in v : Foo. (* Prints wrong: let v := foo a.t in v : Foo *) + End F. + Module a <: A. + Definition T : Set := unit. + Definition t : T := tt. + End a. + Module Import f := F a. + (* Check let v := 0%test16 in v : Foo. *) + (* Error: Anomaly "Uncaught exception Failure("List.last")." +Please report at http://coq.inria.fr/bugs/. *) +End Test16. -- cgit v1.2.3 From 17cb475550a0f4efe9f3f4c58fdbd9039f5fdd68 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 31 Aug 2018 17:01:43 -0400 Subject: Give a proper error message on num-not in functor Numeral Notations are not well-supported inside functors. We now give a proper error message rather than an anomaly when this occurs. --- doc/sphinx/user-extensions/syntax-extensions.rst | 12 ++++++++++++ interp/notation.ml | 7 +++++-- test-suite/success/NumeralNotations.v | 10 ++++------ 3 files changed, 21 insertions(+), 8 deletions(-) diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 886ca0472a..b46382dbbf 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1462,6 +1462,18 @@ Numeral notations concrete numeral expressed as a decimal. They may not return opaque constants. + .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment. + + The inductive type used to register the numeral notation is no + longer available in the environment. Most likely, this is because + the numeral notation was declared inside a functor for an + inductive type inside the functor. This use case is not currently + supported. + + Alternatively, you might be trying to use a primitive token + notation from a plugin which forgot to specify which module you + must :g:`Require` for access to that notation. + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). The type passed to :cmd:`Numeral Notation` must be a single diff --git a/interp/notation.ml b/interp/notation.ml index 551f1bfa83..55ead946cb 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -479,8 +479,11 @@ let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) = 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 *) diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v index 4a275de5b5..47ef381270 100644 --- a/test-suite/success/NumeralNotations.v +++ b/test-suite/success/NumeralNotations.v @@ -1,4 +1,3 @@ - (* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *) (* https://github.com/coq/coq/pull/8064#discussion_r202497516 *) @@ -290,15 +289,14 @@ Module Test16. Inductive Foo := foo (_ : a.T). Definition to_uint (x : Foo) : Decimal.uint := Nat.to_uint O. Definition of_uint (x : Decimal.uint) : Foo := foo a.t. - Numeral Notation Foo of_uint to_uint : test16_scope. - Check let v := 0%test16 in v : Foo. (* Prints wrong: let v := foo a.t in v : Foo *) + Global Numeral Notation Foo of_uint to_uint : test16_scope. + Check let v := 0%test16 in v : Foo. End F. Module a <: A. Definition T : Set := unit. Definition t : T := tt. End a. Module Import f := F a. - (* Check let v := 0%test16 in v : Foo. *) - (* Error: Anomaly "Uncaught exception Failure("List.last")." -Please report at http://coq.inria.fr/bugs/. *) + (** Ideally this should work, but it should definitely not anomaly *) + Fail Check let v := 0%test16 in v : Foo. End Test16. -- cgit v1.2.3 From f7cf1f7e6f7f010e57e925e2fbb76a52fef74068 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 31 Aug 2018 15:22:52 -0400 Subject: Add overlay for HoTT The overlay for HoTT should be merged right after this PR. --- dev/ci/user-overlays/jasongross-numeral-notation-4.sh | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 dev/ci/user-overlays/jasongross-numeral-notation-4.sh diff --git a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh new file mode 100644 index 0000000000..76aa37d380 --- /dev/null +++ b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "8064" ] || [ "$CI_BRANCH" = "numeral-notation-4" ]; then + HoTT_CI_REF=fix-for-numeral-notations + HoTT_CI_GITURL=https://github.com/JasonGross/HoTT + HoTT_CI_ARCHIVEURL=${HoTT_CI_GITURL}/archive +fi -- cgit v1.2.3