From d038839a32978548051573286e22462d68d42ee6 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 26 Apr 2016 17:30:30 +0200 Subject: Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t) This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml --- parsing/egramcoq.ml | 8 ++++++-- parsing/g_constr.ml4 | 10 +++++----- 2 files changed, 11 insertions(+), 7 deletions(-) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 890ce2deca..f2ec6e8b7c 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -324,6 +324,10 @@ type 'r env = { let push_constr subst v = { subst with constrs = v :: subst.constrs } +let mkNumeral n = + if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true) + else Numeral (Bigint.to_string (Bigint.neg n), false) + let push_item : type s r. s target -> (s, r) entry -> s env -> r -> s env = fun forpat e subst v -> match e with | TTConstr _ -> push_constr subst v @@ -337,8 +341,8 @@ match e with | TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders } | TTBigint -> begin match forpat with - | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral v)) - | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral v)) + | ForConstr -> push_constr subst (CAst.make @@ CPrim (mkNumeral v)) + | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (mkNumeral v)) end | TTReference -> begin match forpat with diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 54bac253d0..de76118026 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -203,7 +203,7 @@ GEXTEND Gram | c=match_constr -> c | "("; c = operconstr LEVEL "200"; ")" -> (match c.CAst.v with - CPrim (Numeral z) when Bigint.is_pos_or_zero z -> + | CPrim (Numeral (n,true)) -> CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[])) | _ -> c) | "{|"; c = record_declaration; "|}" -> c @@ -280,7 +280,7 @@ GEXTEND Gram atomic_constr: [ [ g=global; i=instance -> CAst.make ~loc:!@loc @@ CRef (g,i) | s=sort -> CAst.make ~loc:!@loc @@ CSort s - | n=INT -> CAst.make ~loc:!@loc @@ CPrim (Numeral (Bigint.of_string n)) + | n=INT -> CAst.make ~loc:!@loc @@ CPrim (Numeral (n,true)) | s=string -> CAst.make ~loc:!@loc @@ CPrim (String s) | "_" -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None) | "?"; "["; id=ident; "]" -> CAst.make ~loc:!@loc @@ CHole (None, IntroIdentifier id, None) @@ -395,18 +395,18 @@ GEXTEND Gram | "_" -> CAst.make ~loc:!@loc @@ CPatAtom None | "("; p = pattern LEVEL "200"; ")" -> (match p.CAst.v with - | CPatPrim (Numeral z) when Bigint.is_pos_or_zero z -> + | CPatPrim (Numeral (n,true)) -> CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[]) | _ -> p) | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" -> let p = match p with - | { CAst.v = CPatPrim (Numeral z) } when Bigint.is_pos_or_zero z -> + | { CAst.v = CPatPrim (Numeral (n,true)) } -> CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[]) | _ -> p in CAst.make ~loc:!@loc @@ CPatCast (p, ty) - | n = INT -> CAst.make ~loc:!@loc @@ CPatPrim (Numeral (Bigint.of_string n)) + | n = INT -> CAst.make ~loc:!@loc @@ CPatPrim (Numeral (n,true)) | s = string -> CAst.make ~loc:!@loc @@ CPatPrim (String s) ] ] ; impl_ident_tail: -- cgit v1.2.3 From 2bc76bf063da72d1db38c3c0d29c747b0fe23f78 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 22 Feb 2017 18:32:23 +0100 Subject: G_prim: the bigint entry keeps numbers in raw strings --- parsing/egramcoq.ml | 10 +++------- parsing/g_prim.ml4 | 4 ++-- parsing/pcoq.mli | 2 +- 3 files changed, 6 insertions(+), 10 deletions(-) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index f2ec6e8b7c..35ffa20d08 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -227,7 +227,7 @@ type prod_info = production_level * production_position type (_, _) entry = | TTName : ('self, Name.t Loc.located) entry | TTReference : ('self, reference) entry -| TTBigint : ('self, Bigint.bigint) entry +| TTBigint : ('self, Constrexpr.raw_natural_number) entry | TTBinder : ('self, local_binder_expr list) entry | TTConstr : prod_info * 'r target -> ('r, 'r) entry | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry @@ -324,10 +324,6 @@ type 'r env = { let push_constr subst v = { subst with constrs = v :: subst.constrs } -let mkNumeral n = - if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true) - else Numeral (Bigint.to_string (Bigint.neg n), false) - let push_item : type s r. s target -> (s, r) entry -> s env -> r -> s env = fun forpat e subst v -> match e with | TTConstr _ -> push_constr subst v @@ -341,8 +337,8 @@ match e with | TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders } | TTBigint -> begin match forpat with - | ForConstr -> push_constr subst (CAst.make @@ CPrim (mkNumeral v)) - | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (mkNumeral v)) + | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (v,true))) + | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (v,true))) end | TTReference -> begin match forpat with diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 78f75a73cb..c77d6e204e 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -114,7 +114,7 @@ GEXTEND Gram natural: [ [ i = INT -> my_int_of_string (!@loc) i ] ] ; - bigint: (* Negative numbers are dealt with specially *) - [ [ i = INT -> (Bigint.of_string i) ] ] + bigint: (* Negative numbers are dealt with elsewhere *) + [ [ i = INT -> i ] ] ; END diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 959e8ddf52..9fb3daabaf 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -199,7 +199,7 @@ module Prim : val pattern_identref : Id.t located Gram.entry val base_ident : Id.t Gram.entry val natural : int Gram.entry - val bigint : Bigint.bigint Gram.entry + val bigint : Constrexpr.raw_natural_number Gram.entry val integer : int Gram.entry val string : string Gram.entry val lstring : string located Gram.entry -- cgit v1.2.3