Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit ba4e2c29 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

negative literals: support in extraction

parent 200d4cb8
......@@ -388,7 +388,7 @@ module Translate = struct
let test = ML.mk_expr (Mltree.Eapp (op_b_rs, [i_expr; to_expr]))
(Mltree.I ity_bool) eff_empty in
let next_expr =
let one_const = Number.int_const_dec "1" in
let one_const = Number.int_const_of_int 1 in
let one_expr =
ML.mk_expr (Mltree.Econst one_const) ML.ity_int eff_empty in
let i_op_one = Mltree.Eapp (op_a_rs, [i_expr; one_expr]) in
......@@ -440,9 +440,7 @@ module Translate = struct
| Econst c ->
let c = match c with
Number.ConstInt c -> c | _ -> assert false in
if c.Number.ic_negative then
failwith "negative integer literals not yet supported";
ML.mk_expr (Mltree.Econst c.Number.ic_abs) (Mltree.I e.e_ity) eff
ML.mk_expr (Mltree.Econst c) (Mltree.I e.e_ity) eff
| Evar pv ->
ML.mk_expr (Mltree.Evar pv) (Mltree.I e.e_ity) eff
| Elet (LDvar (_, e1), e2) when e_ghost e1 ->
......
......@@ -36,7 +36,7 @@ type expr = {
}
and expr_node =
| Econst of Number.integer_literal
| Econst of Number.integer_constant
| Evar of pvsymbol
| Eapp of rsymbol * expr list
| Efun of var list * expr
......
......@@ -280,8 +280,9 @@ module Print = struct
| Some s, _, [{e_node = Econst _}] ->
let print_constant fmt e = match e.e_node with
| Econst c ->
let s = BigInt.to_string (Number.compute_int_literal c) in
fprintf fmt "%s" s
let s = BigInt.to_string (Number.compute_int_constant c) in
if c.Number.ic_negative then fprintf fmt "(%s)" s
else fprintf fmt "%s" s
| _ -> assert false in
syntax_arguments s print_constant fmt pvl
| _, Some s, _ ->
......@@ -359,7 +360,7 @@ module Print = struct
and print_enode ?(paren=false) info fmt = function
| Econst c ->
let n = Number.compute_int_literal c in
let n = Number.compute_int_constant c in
fprintf fmt "(Z.of_string \"%s\")" (BigInt.to_string n)
| Evar pvs ->
(print_lident info) fmt (pv_name pvs)
......@@ -385,8 +386,9 @@ module Print = struct
| Some s, [{e_node = Econst _}] ->
let print_constant fmt e = begin match e.e_node with
| Econst c ->
let s = BigInt.to_string (Number.compute_int_literal c) in
fprintf fmt "%s" s
let s = BigInt.to_string (Number.compute_int_constant c) in
if c.Number.ic_negative then fprintf fmt "(%s)" s
else fprintf fmt "%s" s
| _ -> assert false end in
syntax_arguments s print_constant fmt pvl
| _ ->
......
......@@ -73,6 +73,17 @@ let int_const_bin s =
check_integer_literal 2 is_bin s;
IConstBin s
let int_const_of_int n =
let neg,a =
if n >= 0 then
false,n
else
true,-n
in
assert (a >= 0);
let a = int_const_dec (string_of_int a) in
{ic_negative = neg ;ic_abs = a}
let const_of_big_int n =
let neg,a =
if BigInt.ge n BigInt.zero then
......
......@@ -50,6 +50,7 @@ val int_const_bin : string -> integer_literal
InvalidConstantLiteral(base,s) is raised if [s] contains invalid
characters for the given base. *)
val int_const_of_int : int -> integer_constant
val const_of_big_int : BigInt.t -> constant
val real_const_dec : string -> string -> string option -> real_literal
......@@ -57,10 +58,6 @@ val real_const_hex : string -> string -> string option -> real_literal
(** Pretty-printing *)
(* see which are used
val print_integer_literal : formatter -> integer_literal -> unit
val print_real_literal : formatter -> real_literal -> unit
*)
val print_constant : formatter -> constant -> unit
(** Pretty-printing with conversion *)
......
......@@ -49,4 +49,15 @@ module Float
goal g : Float32.lt (-1.0:Float32.t) x
end
\ No newline at end of file
end
module M
use import int.Int
let constant x = -42
let f (y:int) = y + x
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