Commit b6762126 authored by MARCHE Claude's avatar MARCHE Claude

support for negative literals, first step

- requires a lot more testing
- support in extraction missing (exception raised)
- interaction with "syntax literal" remains to investigate
parent 54e5a079
......@@ -7,7 +7,7 @@
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../12475.why" expanded="true">
<theory name="Stmt" sum="f2e23bc6c52360c346f78a5be969b6b4" expanded="true">
<theory name="Stmt" sum="875cae0dd4a2795d1efc5e3e1180b734" expanded="true">
<goal name="toto" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
......
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="3" name="Z3" version="4.3.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -12,7 +12,7 @@
<file name="../agatha.why" expanded="true">
<theory name="Agatha" sum="65caf34afba9724ec20c2e4ca302503d" expanded="true">
<goal name="Diff1" expanded="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.00" steps="5"/></proof>
......@@ -21,7 +21,7 @@
<proof prover="10"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Diff2" expanded="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.01" steps="6"/></proof>
......@@ -30,7 +30,7 @@
<proof prover="10"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Diff3" expanded="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.01" steps="7"/></proof>
......@@ -39,7 +39,7 @@
<proof prover="10"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Enigma" expanded="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="0"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
......
......@@ -2,8 +2,8 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="8" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="9" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="0"/>
......@@ -16,8 +16,8 @@
</theory>
<theory name="Example" sum="befcd266c1f484dfa381084b8131ba5c" expanded="true">
<goal name="G1">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.02"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
......@@ -27,19 +27,19 @@
<proof prover="13"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G2">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.02"/></proof>
<proof prover="9"><result status="valid" time="0.06"/></proof>
<proof prover="10" timelimit="10"><result status="valid" time="0.03" steps="45"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="1.32"/></proof>
<proof prover="12"><result status="valid" time="2.09"/></proof>
<proof prover="13"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="G5b">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
......@@ -49,8 +49,8 @@
<proof prover="13"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G5c">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.06"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
......@@ -59,30 +59,30 @@
<proof prover="13"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G5">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.05"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.47"/></proof>
<proof prover="12"><result status="valid" time="0.73"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="G3">
<proof prover="6" timelimit="9"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.03"/></proof>
<proof prover="9"><result status="valid" time="0.07"/></proof>
<proof prover="11"><result status="valid" time="0.17"/></proof>
<proof prover="12"><result status="valid" time="0.85"/></proof>
<proof prover="11"><result status="valid" time="0.34"/></proof>
<proof prover="12"><result status="valid" time="1.31"/></proof>
</goal>
<goal name="G4">
<proof prover="2"><result status="valid" time="0.53"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.82"/></proof>
<proof prover="6" timelimit="7"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.07"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.83"/></proof>
<proof prover="11"><result status="valid" time="0.13"/></proof>
<proof prover="12"><result status="valid" time="1.37"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
......@@ -90,7 +90,7 @@
</theory>
<theory name="Example2" sum="ab79d277a8f71ff7d72600bdefbe809e" expanded="true">
<goal name="G1">
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
......@@ -107,7 +107,7 @@
<proof prover="13" memlimit="1000"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="G5b">
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
......@@ -116,7 +116,7 @@
<proof prover="13"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G5c">
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
......@@ -125,7 +125,7 @@
<proof prover="13"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G5">
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
......@@ -135,8 +135,8 @@
</goal>
<goal name="G3">
<proof prover="6"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.03"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.14"/></proof>
<proof prover="9"><result status="valid" time="0.14"/></proof>
<proof prover="11"><result status="valid" time="0.04"/></proof>
<proof prover="12"><result status="valid" time="0.00"/></proof>
</goal>
......
......@@ -5,9 +5,9 @@
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../real.why" expanded="true">
<theory name="CosineSingle" sum="97f9e06974199fb947370814aa2ff134" expanded="true">
<theory name="CosineSingle" sum="7dae6c2648a23c62f67c4fd7bc4654d3" expanded="true">
<goal name="MethodError" expanded="true">
<proof prover="0" edited="real_CosineSingle_MethodError_1.v"><result status="valid" time="1.82"/></proof>
<proof prover="0" edited="real_CosineSingle_MethodError_1.v"><result status="valid" time="1.31"/></proof>
<proof prover="2"><result status="valid" time="0.11"/></proof>
</goal>
</theory>
......
......@@ -98,7 +98,7 @@
</theory>
<theory name="HdTlNoOpt" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="NthHdTl" sum="3d14df5fb64a9db0c86e94f99cbc6759">
<theory name="NthHdTl" sum="2df5f3b79d8ce9a9de7c60035dab5135">
<goal name="Nth_tl">
<proof prover="6"><result status="valid" time="0.00" steps="21"/></proof>
</goal>
......@@ -153,7 +153,7 @@
<proof prover="6"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="mem_decomp.1.2" expl="2.">
<proof prover="3"><result status="valid" time="0.83"/></proof>
<proof prover="3"><result status="valid" time="0.59"/></proof>
</goal>
</transf>
</goal>
......@@ -345,7 +345,7 @@
<proof prover="6"><result status="valid" time="0.03" steps="63"/></proof>
</goal>
<goal name="rev_append_sorted_incr.1.7" expl="7.">
<proof prover="6"><result status="valid" time="1.58" steps="2697"/></proof>
<proof prover="6"><result status="valid" time="0.94" steps="2697"/></proof>
</goal>
<goal name="rev_append_sorted_incr.1.8" expl="8.">
<proof prover="4"><result status="valid" time="1.59"/></proof>
......@@ -377,7 +377,7 @@
<proof prover="6"><result status="valid" time="0.03" steps="75"/></proof>
</goal>
<goal name="rev_append_sorted_decr.1.7" expl="7.">
<proof prover="6"><result status="valid" time="1.47" steps="2409"/></proof>
<proof prover="6"><result status="valid" time="1.13" steps="2409"/></proof>
</goal>
<goal name="rev_append_sorted_decr.1.8" expl="8.">
<proof prover="2"><result status="valid" time="0.07"/></proof>
......@@ -462,7 +462,7 @@
<proof prover="6"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="Permut_length">
<proof prover="7" edited="list_Permut_Permut_length_2.v"><result status="valid" time="2.14"/></proof>
<proof prover="7" edited="list_Permut_Permut_length_2.v"><result status="valid" time="1.54"/></proof>
</goal>
</theory>
<theory name="Distinct" sum="12ed45bbf4afe5f5deaa62646cbf49f3">
......
......@@ -4,9 +4,9 @@
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../coq-interval.why" expanded="true">
<theory name="P" sum="c76b54c1e6453d33af15a42fd9489845" expanded="true">
<theory name="P" sum="7f6fe6b31b02a544c60045c0aec7b149" expanded="true">
<goal name="pow_eps2_max_int" expanded="true">
<proof prover="0" edited="coqmninterval_P_pow_eps2_max_int_1.v"><result status="valid" time="1.21"/></proof>
<proof prover="0" edited="coqmninterval_P_pow_eps2_max_int_1.v"><result status="valid" time="0.80"/></proof>
</goal>
</theory>
</file>
......
......@@ -17,7 +17,7 @@
<proof prover="1" memlimit="1000"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="P3" sum="6c869b810ccce7e54679d67b1e628afa" expanded="true">
<theory name="P3" sum="6963eeaec55244f198b193c068311ae7" expanded="true">
<goal name="cos_bound" expanded="true">
<proof prover="1"><result status="timeout" time="5.20"/></proof>
</goal>
......@@ -42,9 +42,9 @@
<proof prover="1"><result status="unknown" time="0.23"/></proof>
</goal>
</theory>
<theory name="PolyPaverExamples" sum="610ebe5089f186069f185ce34e8d16b6" expanded="true">
<theory name="PolyPaverExamples" sum="a06fb800674a994e8bf9b744d8665392" expanded="true">
<goal name="g1" expanded="true">
<proof prover="1"><result status="unknown" time="0.24"/></proof>
<proof prover="1"><result status="unknown" time="0.39"/></proof>
</goal>
</theory>
</file>
......
......@@ -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 =
......
......@@ -307,7 +307,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 }
......
......@@ -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
......
......@@ -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
......
......@@ -524,25 +524,26 @@ let rec tr_positive p = match kind_of_term p with
| _ ->
raise NotArithConstant
let const_of_big_int b =
let const_of_big_int is_negative b =
Term.t_const
(Number.ConstInt (Number.int_const_dec (Big_int.string_of_big_int b)))
(Number.(ConstInt { ic_negative = is_negative ;
ic_abs = Number.int_const_dec (Big_int.string_of_big_int b) }))
ty_int
(* translates a closed Coq term t:Z or R into a FOL term of type int or real *)
let rec tr_arith_constant dep t = match kind_of_term t with
| Construct _ when is_global coq_Z0 t -> Term.t_nat_const 0
| App (f, [|a|]) when is_global coq_Zpos f ->
const_of_big_int (tr_positive a)
const_of_big_int false (tr_positive a)
| App (f, [|a|]) when is_global coq_Zneg f ->
let t = const_of_big_int (tr_positive 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 a)
| Const _ when is_global 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 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 *)
......
......@@ -267,7 +267,7 @@ let syntax_range_literal s fmt c =
else
None
in
let v = Number.compute_int c in
let v = Number.compute_int_literal c in
Number.print_in_base base digits fmt v
in
global_substitute_fmt opt_search_forward_literal_format f s fmt
......
......@@ -103,10 +103,10 @@ val syntax_arguments_typed :
the list l using the template templ and the printer print_arg *)
val syntax_range_literal :
string -> Number.integer_constant Pp.pp
string -> Number.integer_literal Pp.pp
val syntax_float_literal :
string -> Number.float_format -> Number.real_constant Pp.pp
string -> Number.float_format -> Number.real_literal Pp.pp
(** {2 pretty-printing transformations (useful for caching)} *)
......
......@@ -822,7 +822,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 InvalidLiteralType of ty
......@@ -831,14 +837,14 @@ let check_literal c ty =
| Tyapp (ts,[]) -> ts
| _ -> raise (InvalidLiteralType ty) in
match c with
| Number.ConstInt c when not (ts_equal ts ts_int) ->
| Number.ConstInt n when not (ts_equal ts ts_int) ->
begin match ts.ts_def with
| Range ir -> Number.check_range c ir
| Range ir -> Number.(check_range n ir)
| _ -> raise (InvalidLiteralType ty)
end
| Number.ConstReal c when not (ts_equal ts ts_real) ->
| Number.ConstReal x when not (ts_equal ts ts_real) ->
begin match ts.ts_def with
| Float fp -> Number.check_float c fp
| Float fp -> Number.(check_float x.Number.rc_abs fp)
| _ -> raise (InvalidLiteralType ty)
end
| _ -> ()
......
......@@ -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 stop_split : label
val asym_split : label
......
......@@ -191,7 +191,7 @@ let create_tysymbol name args def =
ignore (ty_v_all check def)
| Range ir ->
if args <> [] then raise IllegalTypeParameters;
if BigInt.lt ir.Number.ir_upper ir.Number.ir_lower
if BigInt.lt ir.Number.ir_upper_val ir.Number.ir_lower_val
then raise EmptyRange
| Float fp ->
if args <> [] then raise IllegalTypeParameters;
......
......@@ -438,8 +438,11 @@ module Translate = struct
assert (not eff.eff_ghost);
match e.e_node with
| Econst c ->
let c = match c with Number.ConstInt c -> c | _ -> assert false in
ML.mk_expr (Mltree.Econst c) (Mltree.I e.e_ity) eff
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
| Evar pv ->
ML.mk_expr (Mltree.Evar pv) (Mltree.I e.e_ity) eff
| Elet (LDvar (_, e1), e2) when e_ghost e1 ->
......
......@@ -483,7 +483,11 @@ let e_const c ity =
mk_expr (Econst c) ity MaskVisible eff_empty
let e_nat_const n =
e_const (Number.ConstInt (Number.int_const_dec (string_of_int n))) ity_int
assert (n >= 0);
let a =
Number.{ ic_negative = false ; ic_abs = int_const_dec (string_of_int n)}
in
e_const (Number.ConstInt a) ity_int
let e_ghostify gh ({e_effect = eff} as e) =
if not gh then e else
......
......@@ -36,7 +36,7 @@ type expr = {
}
and expr_node =
| Econst of Number.integer_constant
| Econst of Number.integer_literal
| Evar of pvsymbol
| Eapp of rsymbol * expr list
| Efun of var list * expr
......
......@@ -280,7 +280,7 @@ 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 c) in
let s = BigInt.to_string (Number.compute_int_literal c) in
fprintf fmt "%s" s
| _ -> assert false in
syntax_arguments s print_constant fmt pvl
......@@ -359,7 +359,7 @@ module Print = struct
and print_enode ?(paren=false) info fmt = function
| Econst c ->
let n = Number.compute_int c in
let n = Number.compute_int_literal c in
fprintf fmt "(Z.of_string \"%s\")" (BigInt.to_string n)
| Evar pvs ->
(print_lident info) fmt (pv_name pvs)
......@@ -385,7 +385,7 @@ 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 c) in
let s = BigInt.to_string (Number.compute_int_literal c) in
fprintf fmt "%s" s
| _ -> assert false end in
syntax_arguments s print_constant fmt pvl
......
......@@ -334,14 +334,12 @@ let create_type_decl dl =
(* create max attribute *)
let max_id = id_derive (nm ^ "'maxInt") id in
let max_ls = create_fsymbol max_id [] ty_int in
let max_ic = Number.(int_const_dec (BigInt.to_string ir.ir_upper)) in
let max_defn = t_const (Number.ConstInt max_ic) ty_int in
let max_defn = t_const Number.(ConstInt ir.ir_upper) ty_int in
let max_decl = create_logic_decl [make_ls_defn max_ls [] max_defn] in
(* create min attribute *)
let min_id = id_derive (nm ^ "'minInt") id in
let min_ls = create_fsymbol min_id [] ty_int in
let min_ic = Number.(int_const_dec (BigInt.to_string ir.ir_lower)) in
let min_defn = t_const (Number.ConstInt min_ic) ty_int in
let min_defn = t_const Number.(ConstInt ir.ir_lower) ty_int in
let min_decl = create_logic_decl [make_ls_defn min_ls [] min_defn] in
let pure = [create_ty_decl ts; pj_decl; max_decl; min_decl] in
let meta = Theory.(meta_range, [MAts ts; MAls pj_ls]) in
......
......@@ -136,7 +136,7 @@ exception NotNum
let big_int_of_const c =
match c with
| Number.ConstInt i -> Number.compute_int i
| Number.ConstInt i -> Number.compute_int_constant i
| _ -> raise NotNum
let big_int_of_value v =
......
......@@ -48,6 +48,12 @@
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)
......@@ -94,14 +100,6 @@
{ 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"
......@@ -115,9 +113,9 @@
(* Tokens *)
%token <string> LIDENT LIDENT_QUOTE UIDENT UIDENT_QUOTE
%token <Number.integer_constant> INTEGER
%token <Number.integer_literal> INTEGER
%token <string> OP1 OP2 OP3 OP4 OPPREF
%token <Number.real_constant> REAL
%token <Number.real_literal> REAL
%token <string> STRING
%token <Loc.position> POSITION
%token <string> QUOTE_LIDENT
......@@ -267,7 +265,7 @@ meta_arg:
| LEMMA qualid { Mlm $2 }
| GOAL qualid { Mgl $2 }
| STRING { Mstr $1 }
| INTEGER { Mint (small_integer $1) }
| INTEGER { Mint (Number.to_small_integer $1) }
(* Theory declarations *)
......@@ -305,12 +303,16 @@ typedefn:
| EQUAL vis_mut ty
{ $2, TDalias $3 }
(* FIXME: allow negative bounds *)
| EQUAL LT RANGE INTEGER INTEGER GT
| EQUAL LT RANGE int_constant int_constant GT
{ (Public, false),
TDrange (Number.compute_int $4, Number.compute_int $5) }
TDrange ($4,$5) }
| EQUAL LT FLOAT INTEGER INTEGER GT
{ (Public, false),
TDfloat (small_integer $4, small_integer $5) }
TDfloat (Number.to_small_integer $4, Number.to_small_integer $5) }
int_constant:
| INTEGER { mk_int_const false $1 }
| MINUS INTEGER { mk_int_const true $2 }
vis_mut:
| (* epsilon *) { Public, false }
......@@ -514,11 +516,9 @@ term_:
| prefix_op term %prec prec_prefix_op
{ Tidapp (Qident $1, [$2]) }
| MINUS INTEGER
{ Tidapp (Qident (mk_id (prefix "-") $startpos($1) $endpos($1)),
[mk_term (Tconst (Number.ConstInt $2)) $startpos($2) $endpos($2)]) }
{ Tconst (Number.ConstInt (mk_int_const true $2)) }
| MINUS REAL
{ Tidapp (Qident (mk_id (prefix "-") $startpos($1) $endpos($1)),
[mk_term (Tconst (Number.ConstReal $2)) $startpos($2) $endpos($2)]) }
{ Tconst (Number.ConstReal (mk_real_const true $2)) }
| l = term ; o = bin_op ; r = term
{ Tbinop (l, o, r) }
| l = term ; o = infix_op_1 ; r = term
......@@ -630,8 +630,8 @@ quant:
| EXISTS { Dterm.DTexists }
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 *)
......@@ -696,11 +696,9 @@ expr_:
| prefix_op expr %prec prec_prefix_op
{ Eidapp (Qident $1, [$2]) }
| MINUS INTEGER
{ Eidapp (Qident (mk_id (prefix "-") $startpos($1) $endpos($1)),
[mk_expr (Econst (Number.ConstInt $2)) $startpos($2) $endpos($2)]) }
{ Econst (Number.ConstInt (mk_int_const true $2)) }
| MINUS REAL
{ Eidapp (Qident (mk_id (prefix "-") $startpos($1) $endpos($1)),
[mk_expr (Econst (Number.ConstReal $2)) $startpos($2) $endpos($2)]) }
{ Econst (Number.ConstReal (mk_real_const true $2)) }
| l = expr ; o = infix_op_1 ; r = expr
{ Einfix (l,o,r) }
| l = expr ; o = infix_op_234 ; r = expr
......
......@@ -170,7 +170,7 @@ type type_def =
| TDalias of pty
| TDalgebraic of (Loc.position * ident * param list) list
| TDrecord of field list
| TDrange of BigInt.t * BigInt.t
| TDrange of Number.integer_constant * Number.integer_constant
| TDfloat of int * int
type visibility = Public | Private | Abstract (* = Private + ghost fields *)
......
......@@ -932,8 +932,7 @@ let add_types muc tdl =
end
| TDrange (lo,hi) ->
check_public ~loc d "Range";
let ir = { Number.ir_lower = lo;
Number.ir_upper = hi } in
let ir = Number.create_range lo hi in
let itd = create_range_decl id ir in
Hstr.add hts x itd.itd_its; Hstr.add htd x itd
| TDfloat (eb,sb) ->
......
......@@ -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