Skip to content
GitLab
Commit 3aae32e7 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Backport support for negative literals.

parent 2d250689
Hide whitespace changes
Inline Side-by-side
drivers/metitarski.drv
View file @ 3aae32e7
......@@ -34,6 +34,7 @@ transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "eliminate_negative_constants" (* due to integers, see below *)
transformation "simplify_formula"
transformation "simplify_unknown_lsymbols"
......
drivers/tptp.gen
View file @ 3aae32e7
......@@ -22,6 +22,7 @@ transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_negative_constants"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
examples/use_api/logic.ml
View file @ 3aae32e7
......@@ -348,7 +348,7 @@ let d2 =
let e1 = Mlw_expr.e_arrow ref_fun [Mlw_ty.ity_int] ity in
(* we apply it to 0 *)
let c0 = Mlw_expr.e_const
(Number.ConstInt (Number.int_const_dec "0")) Mlw_ty.ity_int in
Number.(ConstInt { ic_negative = false ; ic_abs = int_const_dec "0" }) Mlw_ty.ity_int in
Mlw_expr.e_app e1 [c0]
in
(* building the first part of the let x = ref 0 *)
......
examples/use_api/mlw.ml
View file @ 3aae32e7
......@@ -135,7 +135,7 @@ let d2 =
let e1 = Mlw_expr.e_arrow ref_fun [Mlw_ty.ity_int] ity in
(* we apply it to 0 *)
let c0 = Mlw_expr.e_const
(Number.ConstInt (Number.int_const_dec "0")) Mlw_ty.ity_int in
Number.(ConstInt { ic_negative = false ; ic_abs = int_const_dec "0" }) Mlw_ty.ity_int in
Mlw_expr.e_app e1 [c0]
in
(* building the first part of the let x = ref 0 *)
......
examples/use_api/mlw_tree.ml
View file @ 3aae32e7
......@@ -97,7 +97,7 @@ let mk_lexpr p = { term_loc = Loc.dummy_position;
term_desc = p }
let mk_const s =
mk_lexpr (Tconst(Number.ConstInt(Number.int_const_dec s)))
mk_lexpr (Tconst Number.(ConstInt { ic_negative = false ; ic_abs = int_const_dec s }))
let mk_expr e = { expr_desc = e; expr_loc = Loc.dummy_position }
......
plugins/python/py_main.ml
View file @ 3aae32e7
......@@ -45,7 +45,7 @@ let deref_id ~loc id =
let array_set ~loc a i v =
mk_expr ~loc (Eidapp (mixfix ~loc "[]<-", [a; i; v]))
let constant ~loc s =
mk_expr ~loc (Econst (Number.ConstInt (Number.int_const_dec s)))
mk_expr ~loc (Econst (Number.(ConstInt { ic_negative = false ; ic_abs = int_const_dec s})))
let len ~loc =
Qident (mk_id ~loc "len")
let break ~loc =
......
plugins/python/py_parser.mly
View file @ 3aae32e7
......@@ -308,7 +308,7 @@ term_arg: mk_term(term_arg_) { $1 }
term_arg_:
| ident { Tident (Qident $1) }
| INTEGER { Tconst (Number.ConstInt ((Number.int_const_dec $1))) }
| INTEGER { Tconst (Number.(ConstInt { ic_negative = false ; ic_abs = int_const_dec $1})) }
| NONE { Ttuple [] }
| TRUE { Ttrue }
| FALSE { Tfalse }
......
plugins/tptp/tptp_printer.ml
View file @ 3aae32e7
......@@ -94,11 +94,13 @@ let print_type info fmt ty = try print_type info fmt ty
let number_format = {
Number.long_int_support = true;
Number.extra_leading_zeros_support = false;
Number.negative_int_support = Number.Number_default;
Number.dec_int_support = Number.Number_default;
Number.hex_int_support = Number.Number_unsupported;
Number.oct_int_support = Number.Number_unsupported;
Number.bin_int_support = Number.Number_unsupported;
Number.def_int_support = Number.Number_unsupported;
Number.negative_real_support = Number.Number_default;
Number.dec_real_support = Number.Number_default;
Number.hex_real_support = Number.Number_unsupported;
Number.frac_real_support = Number.Number_custom
......
plugins/tptp/tptp_typing.ml
View file @ 3aae32e7
......@@ -285,7 +285,7 @@ let rec ty denv env impl { e_loc = loc; e_node = n } = match n with
| Enot _ | Eequ _ | Edob _ | Enum _ -> error ~loc TypeExpected
let t_int_const s =
t_const (Number.ConstInt (Number.int_const_dec s)) ty_int
t_const (Number.(ConstInt { ic_negative = false; ic_abs = int_const_dec s})) ty_int
(* unused
let t_real_const r = t_const (Number.ConstReal r)
......@@ -308,8 +308,8 @@ let rec term denv env impl { e_loc = loc; e_node = n } = match n with
find_dobj ~loc denv env impl s
| Enum (Nint s) -> t_int_const s
| Enum (Nreal (i,f,e)) ->
t_const (Number.ConstReal
(Number.real_const_dec i (Opt.get_def "0" f) e)) ty_real
t_const (Number.(ConstReal { rc_negative = false ;
rc_abs = real_const_dec i (Opt.get_def "0" f) e})) ty_real
| Enum (Nrat (n,d)) ->
let n = t_int_const n and d = t_int_const d in
let frac = ns_find_ls denv.th_rat.th_export ["frac"] in
......
src/coq-tactic/why3tac.ml4
View file @ 3aae32e7
......@@ -479,25 +479,28 @@ let rec tr_positive evd p = match kind evd p with
| _ ->
raise NotArithConstant
let const_of_big_int b =
let const_of_big_int is_neg b =
Term.t_const
(Number.ConstInt (Number.int_const_dec (Big_int.string_of_big_int b)))
(Number.(ConstInt { ic_negative = is_neg ;
ic_abs = Number.int_const_dec (Big_int.string_of_big_int b) }))
ty_int
let const_of_big_int_real b =
let const_of_big_int_real is_neg b =
let s = Big_int.string_of_big_int b in
Term.t_const (Number.ConstReal (Number.real_const_dec s "0" None)) ty_real
Term.t_const (Number.(ConstReal { rc_negative = is_neg ;
rc_abs = real_const_dec s "0" None}))
ty_real
(* translates a closed Coq term t:Z or R into a FOL term of type int or real *)
let rec tr_arith_constant_IZR evd dep t = match kind evd t with
| Construct _ when is_global evd coq_Z0 t ->
Term.t_const (Number.ConstReal (Number.real_const_dec "0" "0" None)) ty_real
Term.t_const (Number.(ConstReal { rc_negative = false ;
rc_abs = real_const_dec "0" "0" None}))
ty_real
| App (f, [|a|]) when is_global evd coq_Zpos f ->
const_of_big_int_real (tr_positive evd a)
const_of_big_int_real false (tr_positive evd a)
| App (f, [|a|]) when is_global evd coq_Zneg f ->
let t = const_of_big_int_real (tr_positive evd a) in
let fs = why_constant_real dep ["prefix -"] in
Term.fs_app fs [t] ty_real
const_of_big_int_real true (tr_positive evd a)
| Cast (t, _, _) ->
tr_arith_constant_IZR evd dep t
| _ ->
......@@ -506,18 +509,18 @@ let rec tr_arith_constant_IZR evd dep t = match kind evd t with
let rec tr_arith_constant evd dep t = match kind evd t with
| Construct _ when is_global evd coq_Z0 t -> Term.t_nat_const 0
| App (f, [|a|]) when is_global evd coq_Zpos f ->
const_of_big_int (tr_positive evd a)
const_of_big_int false (tr_positive evd a)
| App (f, [|a|]) when is_global evd coq_Zneg f ->
let t = const_of_big_int (tr_positive evd a) in
let fs = why_constant_int dep ["prefix -"] in
Term.fs_app fs [t] Ty.ty_int
const_of_big_int true (tr_positive evd a)
| App (f, [|a|]) when is_global evd coq_IZR f ->
tr_arith_constant_IZR evd dep a
| Const _ when is_global evd coq_R0 t ->
Term.t_const (Number.ConstReal (Number.real_const_dec "0" "0" None))
Term.t_const (Number.(ConstReal { rc_negative = false ;
rc_abs = real_const_dec "0" "0" None }))
ty_real
| Const _ when is_global evd coq_R1 t ->
Term.t_const (Number.ConstReal (Number.real_const_dec "1" "0" None))
Term.t_const (Number.(ConstReal { rc_negative = false ;
rc_abs = real_const_dec "1" "0" None}))
ty_real
(* | App (f, [|a;b|]) when f = Lazy.force coq_Rplus -> *)
(* let ta = tr_arith_constant a in *)
......
src/core/printer.ml
View file @ 3aae32e7
......@@ -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 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
......@@ -287,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
......
src/core/term.ml
View file @ 3aae32e7
......@@ -823,7 +823,13 @@ let fs_app fs tl ty = t_app fs tl (Some ty)
let ps_app ps tl = t_app ps tl None
let t_nat_const n =
t_const (Number.ConstInt (Number.int_const_dec (string_of_int n))) ty_int
assert (n >= 0);
let a =
Number.{ic_negative = false ; ic_abs = int_const_dec (string_of_int n)}
in
t_const (Number.ConstInt a) ty_int
let t_bigint_const n = t_const (Number.const_of_big_int n) Ty.ty_int
exception InvalidIntegerLiteralType of ty
exception InvalidRealLiteralType of ty
......@@ -848,7 +854,7 @@ let t_const c ty =
t_const c ty
| Number.ConstReal r ->
begin match ts.ts_def with
| Float fp -> Number.check_float r fp; t_const c ty
| Float fp -> Number.(check_float r.rc_abs) fp; t_const c ty
| _ -> raise (InvalidRealLiteralType ty)
end
......
src/core/term.mli
View file @ 3aae32e7
......@@ -224,6 +224,7 @@ val t_false : term
val t_nat_const : int -> term
(** [t_nat_const n] builds the constant integer term [n],
n must be non-negative *)
val t_bigint_const : BigInt.t -> term
val asym_label : label
val t_and_asym : term -> term -> term
......
src/mlw/expr.ml
View file @ 3aae32e7
......@@ -431,7 +431,11 @@ let e_const c =
mk_expr (Econst c) ity eff_empty
let e_nat_const n =
e_const (Number.ConstInt (Number.int_const_dec (string_of_int n)))
assert (n >= 0);
let a =
Number.{ ic_negative = false ; ic_abs = int_const_dec (string_of_int n)}
in
e_const (Number.ConstInt a)
let e_ghostify gh ({e_effect = eff} as e) =
if eff.eff_ghost || not gh then e else
......
src/parser/lexer.mll
View file @ 3aae32e7
......@@ -220,6 +220,8 @@ rule token = parse
{ LTGT }
| "="
{ EQUAL }
| "-"
{ MINUS }
| "["
{ LEFTSQ }
| "]"
......
src/parser/parser.mly
View file @ 3aae32e7
......@@ -82,6 +82,12 @@ end
let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
let mk_int_const neg lit =
Number.{ ic_negative = neg ; ic_abs = lit}
let mk_real_const neg lit =
Number.{ rc_negative = neg ; rc_abs = lit}
let mk_id id s e = { id_str = id; id_lab = []; id_loc = floc s e }
let get_op s e = Qident (mk_id (mixfix "[]") s e)
......@@ -128,14 +134,6 @@ end
{ e with expr_desc = Emark (init, e) }
*)
let small_integer i =
try match i with
| Number.IConstDec s -> int_of_string s
| Number.IConstHex s -> int_of_string ("0x"^s)
| Number.IConstOct s -> int_of_string ("0o"^s)
| Number.IConstBin s -> int_of_string ("0b"^s)
with Failure _ -> raise Error
let error_param loc =
Loc.errorm ~loc "cannot determine the type of the parameter"
......@@ -149,9 +147,9 @@ end
(* Tokens *)
%token <string> LIDENT LIDENT_QUOTE UIDENT UIDENT_QUOTE
%token <Ptree.integer_constant> INTEGER
%token <Number.integer_literal> INTEGER
%token <string> OP1 OP2 OP3 OP4 OPPREF
%token <Ptree.real_constant> REAL
%token <Number.real_literal> REAL
%token <string> STRING
%token <Loc.position> POSITION
%token <string> QUOTE_UIDENT QUOTE_LIDENT OPAQUE_QUOTE_LIDENT
......@@ -177,7 +175,7 @@ end
%token AND ARROW
%token BAR
%token COLON COMMA
%token DOT DOTDOT EQUAL LAMBDA LT GT LTGT
%token DOT DOTDOT EQUAL LAMBDA LT GT LTGT MINUS
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
%token LARROW LRARROW OR
%token RIGHTPAR RIGHTSQ
......@@ -208,10 +206,11 @@ end
%left EQUAL LTGT LT GT OP1
%nonassoc LARROW
%nonassoc RIGHTSQ (* stronger than <- for e1[e2 <- e3] *)
%left OP2
%left OP2 MINUS
%left OP3
%left OP4
%nonassoc prec_prefix_op
%nonassoc INTEGER REAL
%nonassoc LEFTSQ
%nonassoc OPPREF
......@@ -314,7 +313,7 @@ meta_arg:
| PREDICATE qualid { Mps $2 }
| PROP qualid { Mpr $2 }
| STRING { Mstr $1 }
| INTEGER { Mint (small_integer $1) }
| INTEGER { Mint (Number.to_small_integer $1) }
(* Type declarations *)
......@@ -344,13 +343,15 @@ typedefn:
{ $1, $2, TDrecord $4, $6 }
| model abstract ty invariant*
{ $1, $2, TDalias $3, $4 }
(* FIXME: allow negative bounds *)
| EQUAL LT RANGE INTEGER INTEGER GT
{ false, Public,
TDrange (Number.compute_int $4, Number.compute_int $5), [] }
| EQUAL LT RANGE int_constant int_constant GT
{ false, Public, TDrange ($4, $5), [] }
| EQUAL LT FLOAT INTEGER INTEGER GT
{ false, Public,
TDfloat (small_integer $4, small_integer $5), [] }
TDfloat (Number.to_small_integer $4, Number.to_small_integer $5), [] }
int_constant:
| INTEGER { Number.compute_int_literal $1 }
| MINUS INTEGER { BigInt.minus (Number.compute_int_literal $2) }
model:
| EQUAL { false }
......@@ -543,6 +544,10 @@ term_:
{ Tunop (Tnot, $2) }
| prefix_op term %prec prec_prefix_op
{ Tidapp (Qident $1, [$2]) }
| MINUS INTEGER
{ Tconst (Number.ConstInt (mk_int_const true $2)) }
| MINUS REAL
{ Tconst (Number.ConstReal (mk_real_const true $2)) }
| l = term ; o = bin_op ; r = term
{ Tbinop (l, o, r) }
| l = term ; o = infix_op ; r = term
......@@ -641,9 +646,9 @@ quant:
| LAMBDA { Tlambda }
numeral:
| INTEGER { Number.ConstInt $1 }
| REAL { Number.ConstReal $1 }
| INTEGER { Number.ConstInt (mk_int_const false $1) }
| REAL { Number.ConstReal (mk_real_const false $1) }
(* Program declarations *)
pdecl:
......@@ -706,6 +711,10 @@ expr_:
{ Enot $2 }
| prefix_op expr %prec prec_prefix_op
{ Eidapp (Qident $1, [$2]) }
| MINUS INTEGER
{ Econst (Number.ConstInt (mk_int_const true $2)) }
| MINUS REAL
{ Econst (Number.ConstReal (mk_real_const true $2)) }
| l = expr ; o = lazy_op ; r = expr
{ Elazy (l,o,r) }
| l = expr ; o = infix_op ; r = expr
......@@ -985,7 +994,9 @@ lident_op_id:
lident_op:
| op_symbol { infix $1 }
| op_symbol UNDERSCORE { prefix $1 }
| MINUS UNDERSCORE { prefix "-" }
| EQUAL { infix "=" }
| MINUS { infix "-" }
| OPPREF { prefix $1 }
| LEFTSQ RIGHTSQ { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
......@@ -1007,6 +1018,7 @@ op_symbol:
prefix_op:
| op_symbol { mk_id (prefix $1) $startpos $endpos }
| MINUS { mk_id (prefix "-") $startpos $endpos }
%inline infix_op:
| o = OP1 { mk_id (infix o) $startpos $endpos }
......@@ -1017,6 +1029,7 @@ prefix_op:
| LTGT { mk_id (infix "<>") $startpos $endpos }
| LT { mk_id (infix "<") $startpos $endpos }
| GT { mk_id (infix ">") $startpos $endpos }
| MINUS { mk_id (infix "-") $startpos $endpos }
(* Qualified idents *)
......
src/parser/typing.ml
View file @ 3aae32e7
......@@ -531,19 +531,13 @@ let add_types dl th =
let nm = ts.ts_name.id_string ^ "'maxInt" in
let id = id_derive nm ts.ts_name in
let ls = create_fsymbol id [] ty_int in
let t =
t_const Number.(ConstInt (int_const_dec (BigInt.to_string rg.ir_upper)))
ty_int
in
let t = t_const Number.(const_of_big_int rg.ir_upper) ty_int in
let uc = add_logic_decl uc [make_ls_defn ls [] t] in
(* create min attribute *)
let nm = ts.ts_name.id_string ^ "'minInt" in
let id = id_derive nm ts.ts_name in
let ls = create_fsymbol id [] ty_int in
let t =
t_const Number.(ConstInt (int_const_dec (BigInt.to_string rg.ir_lower)))
ty_int
in
let t = t_const Number.(const_of_big_int rg.ir_lower) ty_int in
add_logic_decl uc [make_ls_defn ls [] t]
| Float fmt ->
(* FIXME: "t'to_real" is probably better *)
......
src/printer/alt_ergo.ml
View file @ 3aae32e7
......@@ -151,11 +151,13 @@ let rec print_term info fmt t =
let number_format = {
Number.long_int_support = true;
Number.extra_leading_zeros_support = true;
Number.negative_int_support = Number.Number_default;
Number.dec_int_support = Number.Number_default;
Number.hex_int_support = Number.Number_unsupported;
Number.oct_int_support = Number.Number_unsupported;
Number.bin_int_support = Number.Number_unsupported;
Number.def_int_support = Number.Number_unsupported;
Number.negative_real_support = Number.Number_default;
Number.dec_real_support = Number.Number_default;
Number.hex_real_support = Number.Number_default;
Number.frac_real_support = Number.Number_unsupported;
......
src/printer/coq.ml
View file @ 3aae32e7
......@@ -262,6 +262,7 @@ and print_tnode _opl opr info fmt t = match t.t_node with
let number_format = {
Number.long_int_support = true;
Number.extra_leading_zeros_support = true;
Number.negative_int_support = Number.Number_custom "(-%a)%%Z";
Number.dec_int_support =
if info.ssreflect then Number.Number_custom "%s%%:Z"
else Number.Number_custom "%s%%Z";
......@@ -269,6 +270,7 @@ and print_tnode _opl opr info fmt t = match t.t_node with
Number.oct_int_support = Number.Number_unsupported;
Number.bin_int_support = Number.Number_unsupported;
Number.def_int_support = Number.Number_unsupported;
Number.negative_real_support = Number.Number_custom "(-%a)%%R";
Number.dec_real_support = Number.Number_unsupported;
Number.hex_real_support = Number.Number_unsupported;
Number.frac_real_support = Number.Number_custom
......
src/printer/cvc3.ml
View file @ 3aae32e7
......@@ -102,11 +102,13 @@ let rec print_term info fmt t = match t.t_node with
let number_format = {
Number.long_int_support = true;
Number.extra_leading_zeros_support = true;
Number.negative_int_support = Number.Number_default;
Number.dec_int_support = Number.Number_default;
Number.hex_int_support = Number.Number_unsupported;
Number.oct_int_support = Number.Number_unsupported;
Number.bin_int_support = Number.Number_unsupported;
Number.def_int_support = Number.Number_unsupported;
Number.negative_real_support = Number.Number_default;
Number.dec_real_support = Number.Number_unsupported;
Number.hex_real_support = Number.Number_unsupported;
Number.frac_real_support = Number.Number_custom
......
Supports Markdown
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