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. --- 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 ++++++++++++++-------- 8 files changed, 111 insertions(+), 49 deletions(-) (limited to 'plugins/syntax') 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 } -- 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. --- plugins/syntax/NatSyntaxViaZ.v | 56 +++++ plugins/syntax/g_numeral.ml4 | 283 ++++++++++++++++++++++++++ plugins/syntax/numeral_notation_plugin.mlpack | 1 + 3 files changed, 340 insertions(+) create mode 100644 plugins/syntax/NatSyntaxViaZ.v create mode 100644 plugins/syntax/g_numeral.ml4 create mode 100644 plugins/syntax/numeral_notation_plugin.mlpack (limited to 'plugins/syntax') 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(-) (limited to 'plugins/syntax') 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 (limited to 'plugins/syntax') 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 ++++++++++++++++++++++++++++++++----------- 1 file changed, 289 insertions(+), 97 deletions(-) (limited to 'plugins/syntax') 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 -- 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 --- 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 - 8 files changed, 378 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 (limited to 'plugins/syntax') 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 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(-) (limited to 'plugins/syntax') 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(-) (limited to 'plugins/syntax') 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 --- plugins/syntax/g_numeral.ml4 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/syntax') 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(-) (limited to 'plugins/syntax') 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 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 ++++++++++++++++++++++---------------------- 1 file changed, 29 insertions(+), 28 deletions(-) (limited to 'plugins/syntax') 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 -- 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(-) (limited to 'plugins/syntax') 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). --- plugins/syntax/g_numeral.ml4 | 80 ++++++++++++++++++++++++-------------------- 1 file changed, 44 insertions(+), 36 deletions(-) (limited to 'plugins/syntax') 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 -- cgit v1.2.3 From d1460484d4804f953c8997eb7d1cf9d1384a82c9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 24 Jul 2018 10:18:01 +0200 Subject: Add support for polymorphic constants. --- plugins/syntax/g_numeral.ml4 | 73 +++++++++++++++++++++----------------------- 1 file changed, 34 insertions(+), 39 deletions(-) (limited to 'plugins/syntax') diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index 19a15fd1df..1d2d47fbaa 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -33,14 +33,11 @@ open Constr as [coqint_of_rawnum]. *) -let eval_constr (c : Constr.t) = - let env = Global.env () 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' +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 (c : constr) = @@ -48,7 +45,8 @@ let eval_constr (c : constr) = Tacred.compute env sigma c *) -let eval_constr_app c1 c2 = eval_constr (mkApp (c1,[| c2 |])) +let eval_constr_app env sigma c1 c2 = + eval_constr env sigma (mkApp (c1,[| c2 |])) exception NotANumber @@ -63,10 +61,9 @@ let warn_large_num = 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_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 --- plugins/syntax/g_numeral.ml4 | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'plugins/syntax') 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 -- 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. --- plugins/syntax/g_numeral.ml4 | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'plugins/syntax') 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.( -- 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 (limited to 'plugins/syntax') 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 --- plugins/syntax/numeral.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'plugins/syntax') 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 ++++++++++-------------- 1 file changed, 10 insertions(+), 14 deletions(-) (limited to 'plugins/syntax') 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 -- 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 --- plugins/syntax/numeral.ml | 21 +++++---------------- 1 file changed, 5 insertions(+), 16 deletions(-) (limited to 'plugins/syntax') 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 -- 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. --- 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 ++- 7 files changed, 15 insertions(+), 8 deletions(-) (limited to 'plugins/syntax') 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]; -- cgit v1.2.3