Commit 02c66f55 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

negative literals: support in meta "syntax_literal"

parent f8dd6af6
......@@ -254,6 +254,7 @@ let syntax_arguments_typed =
let syntax_range_literal s fmt c =
let f s b e fmt =
let v = Number.compute_int_literal c.Number.ic_abs in
let base = match s.[e-1] with
| 'x' -> 16
| 'd' -> 10
......@@ -267,8 +268,20 @@ let syntax_range_literal s fmt c =
else
None
in
let v = Number.compute_int_literal c in
Number.print_in_base base digits fmt v
if base = 10 then begin
if c.Number.ic_negative then fprintf fmt "-";
Number.print_in_base base digits fmt v
end
else
let v =
if c.Number.ic_negative then
match digits with
| Some d ->
BigInt.sub (BigInt.pow_int_pos base d) v
| None -> failwith ("number of digits must be given for printing negative literals in base " ^ string_of_int base)
else v
in
Number.print_in_base base digits fmt v
in
global_substitute_fmt opt_search_forward_literal_format f s fmt
......
......@@ -103,7 +103,7 @@ val syntax_arguments_typed :
the list l using the template templ and the printer print_arg *)
val syntax_range_literal :
string -> Number.integer_literal Pp.pp
string -> Number.integer_constant Pp.pp
val syntax_float_literal :
string -> Number.float_format -> Number.real_literal Pp.pp
......
......@@ -179,9 +179,7 @@ let rec print_term info fmt t =
(* look for syntax literal ts in driver *)
begin match query_syntax info.info_rliteral ts.ts_name, c with
| Some st, Number.ConstInt c ->
if c.Number.ic_negative then
failwith "not supported yet: syntax literal for negative integer literals";
syntax_range_literal st fmt c.Number.ic_abs
syntax_range_literal st fmt c
| Some st, Number.ConstReal c ->
if c.Number.rc_negative then
failwith "not supported yet: syntax literal for negative float literals";
......
......@@ -214,9 +214,7 @@ let rec print_term info fmt t =
(* look for syntax literal ts in driver *)
begin match query_syntax info.info_rliteral ts.ts_name, c with
| Some st, Number.ConstInt c ->
if c.Number.ic_negative then
failwith "not supported yet: syntax literal for negative integer literals";
syntax_range_literal st fmt c.Number.ic_abs
syntax_range_literal st fmt c
| Some st, Number.ConstReal c ->
if c.Number.rc_negative then
failwith "not supported yet: syntax literal for negative real literals";
......
......@@ -351,7 +351,7 @@ let rec print_in_base_aux radix digits fmt i =
fprintf fmt "%c" (char_of_int (to_int i))
end
else
let d,m = computer_div_mod i radix in
let d,m = euclidean_div_mod i radix in
let digits = Opt.map ((+) (-1)) digits in
print_in_base_aux radix digits fmt d;
fprintf fmt "%c" (char_of_int (to_int m))
......
......@@ -111,7 +111,8 @@ val print : number_support -> formatter -> constant -> unit
val print_in_base : int -> int option -> formatter -> BigInt.t -> unit
(** [print_in_base radix digits fmt i] prints the value of [i] in base
[radix]. If digits is not [None] adds leading 0s to have [digits]
characters. *)
characters.
REQUIRES [i] non-negative *)
(** Range checking *)
......
module M
use import int.Int
type byte = < range -128 127 >
meta "literal:keep" type byte
meta "syntax_literal" type byte,"#b%8b",0
let constant zero = (0:byte)
let constant c42 = (42:byte)
let constant cm17 = (-17:byte)
(* rejected as expected
let constant cm200 = (-200:byte)
*)
goal g : byte'int (-1:byte) < 0
type word = < range -0x8000 0x7fff >
meta "literal:keep" type word
meta "syntax_literal" type word,"#x%4x",0
let constant wzero = (0:word)
let constant w42 = (0x42:word)
let constant wm17 = (-17:word)
(* rejected as expected
let constant wm200 = (32768:byte)
*)
goal wg : word'int wm17 < 0
end
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment