Commit 200d4cb8 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

negative literals: support for negative floats

parent 02c66f55
......@@ -300,9 +300,10 @@ let syntax_float_literal s fp fmt c =
else
None
in
let e,m = Number.compute_float c fp in
let e,m = Number.compute_float c.Number.rc_abs fp in
let sg = if c.Number.rc_negative then BigInt.one else BigInt.zero in
match s.[b] with
| 's' -> Number.print_in_base base digits fmt BigInt.zero
| 's' -> Number.print_in_base base digits fmt sg
| 'e' -> Number.print_in_base base digits fmt e
| 'm' -> Number.print_in_base base digits fmt m
| _ -> assert false
......
......@@ -106,7 +106,7 @@ val syntax_range_literal :
string -> Number.integer_constant Pp.pp
val syntax_float_literal :
string -> Number.float_format -> Number.real_literal Pp.pp
string -> Number.float_format -> Number.real_constant Pp.pp
(** {2 pretty-printing transformations (useful for caching)} *)
......
......@@ -181,12 +181,10 @@ let rec print_term info fmt t =
| Some st, Number.ConstInt c ->
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";
let fp = match ts.ts_def with
| Float fp -> fp
| _ -> assert false in
syntax_float_literal st fp fmt c.Number.rc_abs
syntax_float_literal st fp fmt c
| None, _ -> Number.print number_format fmt c
(* TODO/FIXME: we must assert here that the type is either
ty_int or ty_real, otherwise it makes no sense to print
......
......@@ -216,12 +216,10 @@ let rec print_term info fmt t =
| Some st, Number.ConstInt c ->
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";
let fp = match ts.ts_def with
| Float fp -> fp
| _ -> assert false in
syntax_float_literal st fp fmt c.Number.rc_abs
syntax_float_literal st fp fmt c
| None, _ -> Number.print number_format fmt c
(* TODO/FIXME: we must assert here that the type is either
ty_int or ty_real, otherwise it makes no sense to print
......
module M
module Range
use import int.Int
......@@ -39,3 +39,14 @@ module M
end
module Float
use import ieee_float.Float32
let constant x = (-0.125:Float32.t)
goal g : Float32.lt (-1.0:Float32.t) x
end
\ No newline at end of file
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