diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-04-26 17:30:30 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-14 09:44:21 +0200 |
| commit | d038839a32978548051573286e22462d68d42ee6 (patch) | |
| tree | 14af8ed8354ef5ace1f685b1593529a2394f86d8 /parsing | |
| parent | 7e63c300a3aa1e3befb29bab9094e8b1939824bb (diff) | |
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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egramcoq.ml | 8 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 10 |
2 files changed, 11 insertions, 7 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 890ce2dec..f2ec6e8b7 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 54bac253d..de7611802 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: |