Commit d3d7c7ac authored by Guillaume Melquiond's avatar Guillaume Melquiond

Rework numerical constants.

Main changes are:
- Real constants now offer a normalized representation usable for internal
  computations.
- Constants are no longer stored in textual form.
parent d36d163b
......@@ -51,9 +51,9 @@ let deref_id ~loc id =
let array_set ~loc a i v =
mk_expr ~loc (Eidapp (set_op ~loc, [a; i; v]))
let constant ~loc i =
mk_expr ~loc (Econst (Number.const_of_int i))
mk_expr ~loc (Econst (Number.int_const_of_int i))
let constant_s ~loc s =
mk_expr ~loc (Econst (Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec s})))
mk_expr ~loc (Econst (Number.(ConstInt (int_literal ILitDec ~neg:false s))))
let len ~loc =
Qident (mk_id ~loc "len")
let break ~loc =
......
......@@ -306,7 +306,7 @@ term_arg: mk_term(term_arg_) { $1 }
term_arg_:
| ident { Tident (Qident $1) }
| INTEGER { Tconst (Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec $1})) }
| INTEGER { Tconst Number.(ConstInt (int_literal ILitDec ~neg:false $1)) }
| NONE { Ttuple [] }
| TRUE { Ttrue }
| FALSE { Tfalse }
......
......@@ -92,28 +92,30 @@ let print_type info fmt ty = try print_type info fmt ty
with Unsupported s -> raise (UnsupportedType (ty,s))
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
(Number.PrintFracReal ("$to_real(%s)",
"$product($to_real(%s),$to_real(%s))",
"$quotient($to_real(%s),$to_real(%s))"));
Number.def_real_support = Number.Number_unsupported;
Number.long_int_support = `Default;
Number.negative_int_support = `Default;
Number.dec_int_support = `Default;
Number.hex_int_support = `Unsupported;
Number.oct_int_support = `Unsupported;
Number.bin_int_support = `Unsupported;
Number.negative_real_support = `Default;
Number.dec_real_support = `Default;
Number.hex_real_support = `Unsupported;
Number.frac_real_support =
`Custom
((fun fmt i -> fprintf fmt "$to_real(%s)" i),
(fun fmt i n -> fprintf fmt "$product($to_real(%s),$to_real(%s))" i n),
(fun fmt i n -> fprintf fmt "$quotient($to_real(%s),$to_real(%s))" i n));
}
let number_format_metitarski = { number_format with
Number.frac_real_support = Number.Number_custom
(Number.PrintFracReal ("%s", "(%s * %s)", "(%s / %s)"));
}
let number_format_metitarski = {
number_format with
Number.frac_real_support =
`Custom
((fun fmt i -> pp_print_string fmt i),
(fun fmt i n -> fprintf fmt "(%s * %s)" i n),
(fun fmt i n -> fprintf fmt "(%s / %s)" i n));
}
let print_number info fmt c = Number.print (match info.info_num with
| TPTP -> number_format | MetiTarski -> number_format_metitarski) fmt c
......
......@@ -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 { ic_negative = false; ic_abs = int_literal_dec s})) ty_int
t_const (Number.(ConstInt (int_literal ILitDec ~neg:false s))) ty_int
(* unused
let t_real_const r = t_const (Number.ConstReal r)
......@@ -308,8 +308,7 @@ 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 { rc_negative = false ;
rc_abs = real_const_dec i (Opt.get_def "0" f) e})) ty_real
t_const (Number.(ConstReal (real_literal ~radix:10 ~neg:false ~int:i ~frac:(Opt.get_def "0" f) ~exp: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
......
......@@ -266,7 +266,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 v = c.Number.il_int in
let base = match s.[e-1] with
| 'x' -> 16
| 'd' -> 10
......@@ -281,16 +281,16 @@ let syntax_range_literal s fmt c =
None
in
if base = 10 then begin
if c.Number.ic_negative then fprintf fmt "-";
Number.print_in_base base digits fmt v
if BigInt.lt v BigInt.zero then fprintf fmt "-";
Number.print_in_base base digits fmt (BigInt.abs v)
end
else
let v =
if c.Number.ic_negative then
if BigInt.lt v BigInt.zero 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)
| Some d ->
BigInt.add (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
......@@ -312,8 +312,8 @@ let syntax_float_literal s fp fmt c =
else
None
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
let e,m = Number.compute_float c fp in
let m,sg = if BigInt.lt m BigInt.zero then BigInt.abs m, BigInt.one else m, BigInt.zero in
match s.[b] with
| 's' -> Number.print_in_base base digits fmt sg
| 'e' -> Number.print_in_base base digits fmt e
......
......@@ -116,7 +116,7 @@ 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.int_constant Pp.pp
val syntax_float_literal :
string -> Number.float_format -> Number.real_constant Pp.pp
......
......@@ -330,14 +330,7 @@ let t_compare trigger attr t1 t2 =
| Tvar v1, Tvar v2 ->
comp_raise (vs_compare v1 v2)
| Tconst c1, Tconst c2 ->
let open Number in
begin match c1, c2 with
| ConstInt { ic_negative = s1; ic_abs = IConstRaw b1 },
ConstInt { ic_negative = s2; ic_abs = IConstRaw b2 } ->
perv_compare s1 s2;
comp_raise (BigInt.compare b1 b2)
| _, _ -> perv_compare c1 c2
end
comp_raise (Number.compare_const c1 c2)
| Tapp (s1,l1), Tapp (s2,l2) ->
comp_raise (ls_compare s1 s2);
List.iter2 (t_compare bnd vml1 vml2) l1 l2
......@@ -412,7 +405,7 @@ let t_similar t1 t2 =
oty_equal t1.t_ty t2.t_ty &&
match t1.t_node, t2.t_node with
| Tvar v1, Tvar v2 -> vs_equal v1 v2
| Tconst c1, Tconst c2 -> c1 = c2
| Tconst c1, Tconst c2 -> Number.compare_const c1 c2 = 0
| Tapp (s1,l1), Tapp (s2,l2) -> ls_equal s1 s2 && Lists.equal (==) l1 l2
| Tif (f1,t1,e1), Tif (f2,t2,e2) -> f1 == f2 && t1 == t2 && e1 == e2
| Tlet (t1,bv1), Tlet (t2,bv2) -> t1 == t2 && bv1 == bv2
......@@ -854,33 +847,30 @@ let ps_app ps tl = t_app ps tl None
let t_nat_const n =
assert (n >= 0);
t_const (Number.const_of_int n) ty_int
t_const (Number.int_const_of_int n) ty_int
let t_bigint_const n = t_const (Number.const_of_big_int n) Ty.ty_int
let t_int_const n =
t_const (Number.int_const n) Ty.ty_int
let t_real_const ?pow2 ?pow5 s =
t_const (Number.real_const ?pow2 ?pow5 s) Ty.ty_real
exception InvalidIntegerLiteralType of ty
exception InvalidRealLiteralType of ty
let check_literal c ty =
let ts = match ty.ty_node with
| Tyapp (ts,[]) -> ts
| _ -> match c with
| Number.ConstInt _ -> raise (InvalidIntegerLiteralType ty)
| Number.ConstReal _ -> raise (InvalidRealLiteralType ty)
in
match c with
| Number.ConstInt _ when ts_equal ts ts_int -> ()
| Number.ConstInt n ->
begin match ts.ts_def with
| Range ir -> Number.(check_range n ir)
| _ -> raise (InvalidIntegerLiteralType ty)
end
| Number.ConstReal _ when ts_equal ts ts_real -> ()
| Number.ConstReal x ->
begin match ts.ts_def with
| Float fp -> Number.(check_float x.Number.rc_abs fp)
| _ -> raise (InvalidRealLiteralType ty)
end
let open Number in
let ts = match ty.ty_node, c with
| Tyapp (ts,[]), _ -> ts
| _, ConstInt _ -> raise (InvalidIntegerLiteralType ty)
| _, ConstReal _ -> raise (InvalidRealLiteralType ty) in
match c, ts.ts_def with
| ConstInt _, _ when ts_equal ts ts_int -> ()
| ConstInt n, Range ir -> check_range n ir
| ConstInt _, _ -> raise (InvalidIntegerLiteralType ty)
| ConstReal _, _ when ts_equal ts ts_real -> ()
| ConstReal x, Float fp -> check_float x fp
| ConstReal _, _ -> raise (InvalidRealLiteralType ty)
let t_const c ty = check_literal c ty; t_const c ty
......
......@@ -235,7 +235,8 @@ 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 t_int_const : BigInt.t -> term
val t_real_const : ?pow2:BigInt.t -> ?pow5:BigInt.t -> BigInt.t -> term
val stop_split : attribute
val asym_split : attribute
......
......@@ -114,8 +114,9 @@ module Print = struct
let print_constant fmt e = begin match e.e_node with
| Econst c ->
let s = BigInt.to_string (Number.compute_int_constant c) in
if c.Number.ic_negative then fprintf fmt "(%s)" s
let v = c.Number.il_int in
let s = BigInt.to_string v in
if BigInt.lt v BigInt.zero then fprintf fmt "(%s)" s
else fprintf fmt "%s" s
| _ -> assert false end
......@@ -224,7 +225,7 @@ module Print = struct
and print_expr ?(paren=false) info fmt e =
match e.e_node with
| Econst c ->
let n = Number.compute_int_constant c in
let n = c.Number.il_int in
let n = BigInt.to_string n in
let id = match e.e_ity with
| I { ity_node = Ityapp ({its_ts = ts},_,_) } -> ts.ts_name
......
......@@ -799,7 +799,7 @@ module MLToC = struct
let e = C.Evar (pv_name pv) in
([], return_or_expr env e)
| Mltree.Econst ic ->
let n = Number.compute_int_constant ic in
let n = ic.Number.il_int in
let e = C.(Econst (Cint (BigInt.to_string n))) in
([], return_or_expr env e)
| Eapp (rs, el)
......
......@@ -490,7 +490,7 @@ let e_const c ity =
let e_nat_const n =
assert (n >= 0);
e_const (Number.const_of_int n) ity_int
e_const (Number.int_const_of_int n) ity_int
let e_ghostify gh ({e_effect = eff} as e) =
if not gh then e else
......
......@@ -61,7 +61,7 @@ let is_range_small_int ir =
(* a value with a range type included in [min_int, max_int]
can be interpreted as an int *)
let value_of_const ic ty =
let bc = Number.compute_int_constant ic in
let bc = ic.Number.il_int in
match ty with
| Some { ty_node = Tyapp ({ ts_def = Range ir }, [])}
when is_range_small_int ir
......@@ -73,7 +73,7 @@ open Format
let rec print_value fmt = function
| Vvoid -> fprintf fmt "()"
| Vbool b -> fprintf fmt "%b" b
| Vbigint i -> fprintf fmt "%a" Number.print_constant (Number.const_of_big_int i)
| Vbigint i -> Number.print_constant fmt (Number.int_const i)
| Vint i -> fprintf fmt "%d" i
| Vtuple l -> fprintf fmt "@[<hov 2>(%a)@]"
(Pp.print_list Pp.comma print_value) l
......@@ -844,7 +844,7 @@ let rec value_of_term kn t =
let rec term_of_value = function
| Vbool true -> t_bool_true
| Vbool false -> t_bool_false
| Vbigint i -> t_bigint_const i
| Vbigint i -> t_int_const i
| Vint _ -> raise CannotReduce
| Vtuple l -> t_tuple (List.map term_of_value l)
| Vconstr (rs, lf) ->
......
......@@ -48,7 +48,7 @@ type expr = {
}
and expr_node =
| Econst of Number.integer_constant
| Econst of Number.int_constant
| Evar of pvsymbol
| Eapp of rsymbol * expr list
| Efun of var list * expr
......
......@@ -290,8 +290,9 @@ module Print = struct
let print_constant fmt e = begin match e.e_node with
| Econst c ->
let s = BigInt.to_string (Number.compute_int_constant c) in
if c.Number.ic_negative then fprintf fmt "(%s)" s
let v = c.Number.il_int in
let s = BigInt.to_string v in
if BigInt.lt v BigInt.zero then fprintf fmt "(%s)" s
else fprintf fmt "%s" s
| _ -> assert false end
......@@ -420,7 +421,7 @@ module Print = struct
and print_expr ?(paren=false) info fmt e =
match e.e_node with
| Econst c ->
let n = Number.compute_int_constant c in
let n = c.Number.il_int in
let n = BigInt.to_string n in
let id = match e.e_ity with
| I { ity_node = Ityapp ({its_ts = ts},_,_) } -> ts.ts_name
......
......@@ -351,12 +351,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_defn = t_const Number.(const_of_big_int ir.ir_upper) ty_int in
let max_defn = t_const Number.(int_const 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_defn = t_const Number.(const_of_big_int ir.ir_lower) ty_int in
let min_defn = t_const Number.(int_const 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_constant i
| Number.ConstInt i -> i.Number.il_int
| _ -> raise NotNum
let big_int_of_value v =
......
......@@ -160,29 +160,27 @@ rule token = parse
| core_uident as id
{ CORE_UIDENT id }
| dec dec_sep* as s
{ INTEGER (Number.int_literal_dec (Lexlib.remove_underscores s)) }
{ INTEGER Number.(int_literal ILitDec ~neg:false (Lexlib.remove_underscores s)) }
| '0' ['x' 'X'] (hex hex_sep* as s)
{ INTEGER (Number.int_literal_hex (Lexlib.remove_underscores s)) }
{ INTEGER Number.(int_literal ILitHex ~neg:false (Lexlib.remove_underscores s)) }
| '0' ['o' 'O'] (oct oct_sep* as s)
{ INTEGER (Number.int_literal_oct (Lexlib.remove_underscores s)) }
{ INTEGER Number.(int_literal ILitOct ~neg:false (Lexlib.remove_underscores s)) }
| '0' ['b' 'B'] (bin bin_sep* as s)
{ INTEGER (Number.int_literal_bin (Lexlib.remove_underscores s)) }
{ INTEGER Number.(int_literal ILitBin ~neg:false (Lexlib.remove_underscores s)) }
| (dec+ as i) ".."
{ Lexlib.backjump lexbuf 2; INTEGER (Number.int_literal_dec i) }
{ Lexlib.backjump lexbuf 2; INTEGER Number.(int_literal ILitDec ~neg:false i) }
| '0' ['x' 'X'] (hex+ as i) ".."
{ Lexlib.backjump lexbuf 2; INTEGER (Number.int_literal_hex i) }
{ Lexlib.backjump lexbuf 2; INTEGER Number.(int_literal ILitHex ~neg:false i) }
| (dec+ as i) ("" as f) ['e' 'E'] (['-' '+']? dec+ as e)
| (dec+ as i) '.' (dec* as f) (['e' 'E'] (['-' '+']? dec+ as e))?
| (dec* as i) '.' (dec+ as f) (['e' 'E'] (['-' '+']? dec+ as e))?
{ REAL (Number.real_const_dec i f
(Opt.map Lexlib.remove_leading_plus e)) }
{ REAL (Number.real_literal ~radix:10 ~neg:false ~int:i ~frac:f ~exp:(Opt.map Lexlib.remove_leading_plus e)) }
| '0' ['x' 'X'] (hex+ as i) ("" as f) ['p' 'P'] (['-' '+']? dec+ as e)
| '0' ['x' 'X'] (hex+ as i) '.' (hex* as f)
(['p' 'P'] (['-' '+']? dec+ as e))?
| '0' ['x' 'X'] (hex* as i) '.' (hex+ as f)
(['p' 'P'] (['-' '+']? dec+ as e))?
{ REAL (Number.real_const_hex i f
(Opt.map Lexlib.remove_leading_plus e)) }
{ REAL (Number.real_literal ~radix:16 ~neg:false ~int:i ~frac:f ~exp:(Opt.map Lexlib.remove_leading_plus e)) }
| "(*)"
{ Lexlib.backjump lexbuf 2; LEFTPAR }
| "(*"
......
......@@ -23,12 +23,6 @@
let id_anonymous loc = { id_str = "_"; id_ats = []; 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_ats = []; id_loc = floc s e }
let get_op q s e = Qident (mk_id (Ident.op_get q) s e)
......@@ -205,9 +199,9 @@
(* Tokens *)
%token <string> LIDENT CORE_LIDENT UIDENT CORE_UIDENT
%token <Number.integer_literal> INTEGER
%token <Number.int_constant> INTEGER
%token <string> OP1 OP2 OP3 OP4 OPPREF
%token <Number.real_literal> REAL
%token <Number.real_constant> REAL
%token <string> STRING
%token <string> ATTRIBUTE
%token <Loc.position> POSITION
......@@ -444,8 +438,8 @@ typedefn:
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) }
| INTEGER { $1.Number.il_int }
| MINUS INTEGER { BigInt.minus ($2.Number.il_int) }
vis_mut:
| (* epsilon *) { Public, false }
......@@ -684,10 +678,8 @@ single_term_:
{ Tat ($1, $3) }
| prefix_op single_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)) }
| MINUS numeral
{ Tconst (Number.neg $2) }
| l = single_term ; o = bin_op ; r = single_term
{ Tbinop (l, o, r) }
| l = single_term ; o = infix_op_1 ; r = single_term
......@@ -804,8 +796,8 @@ quant:
| EXISTS { Dterm.DTexists }
numeral:
| INTEGER { Number.ConstInt (mk_int_const false $1) }
| REAL { Number.ConstReal (mk_real_const false $1) }
| INTEGER { Number.ConstInt $1 }
| REAL { Number.ConstReal $1 }
(* Program declarations *)
......@@ -954,10 +946,8 @@ single_expr_:
{ Enot $2 }
| prefix_op single_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)) }
| MINUS numeral
{ Econst (Number.neg $2) }
| l = single_expr ; o = infix_op_1 ; r = single_expr
{ Einfix (l,o,r) }
| l = single_expr ; o = infix_op_234 ; r = single_expr
......
......@@ -151,6 +151,19 @@ let unambig_fs fs =
in
inspect (Opt.get fs.ls_value)
let number_format = {
Number.long_int_support = `Default;
Number.negative_int_support = `Default;
Number.dec_int_support = `Default;
Number.hex_int_support = `Unsupported;
Number.oct_int_support = `Unsupported;
Number.bin_int_support = `Unsupported;
Number.negative_real_support = `Default;
Number.dec_real_support = `Default;
Number.hex_real_support = `Default;
Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
}
let rec print_term info fmt t =
if check_for_counterexample t then
info.info_model <- add_model_element t info.info_model;
......@@ -159,21 +172,6 @@ let rec print_term info fmt t =
let () = match t.t_node with
| Tconst c ->
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;
Number.def_real_support = Number.Number_unsupported;
} in
Number.print number_format fmt c
| Tvar { vs_name = id } ->
print_ident info fmt id
......
......@@ -233,6 +233,26 @@ let print_binop fmt = function
| Timplies -> fprintf fmt "->"
| Tiff -> fprintf fmt "<->"
let number_format info = {
Number.long_int_support = `Default;
Number.negative_int_support = `Custom (fun fmt f -> fprintf fmt "(-%t)%%Z" f);
Number.dec_int_support =
`Custom (fun fmt i ->
fprintf fmt (if info.ssreflect then "%s%%:Z" else "%s%%Z") (BigInt.to_string i));
Number.hex_int_support = `Unsupported;
Number.oct_int_support = `Unsupported;
Number.bin_int_support = `Unsupported;
Number.negative_real_support = `Custom (fun fmt f -> fprintf fmt "(-%t)%%R" f);
Number.dec_real_support = `Unsupported;
Number.hex_real_support = `Unsupported;
Number.frac_real_support =
`Custom
((fun fmt i -> fprintf fmt "%s%%R" i),
(fun fmt i n -> fprintf fmt "(%s * %s)%%R" i n),
(fun fmt i n -> fprintf fmt "(%s / %s)%%R" i n));
}
(* [opl] means that there is no delimiter on the left of the term, so
parentheses should be put around the term if it does not start with a
delimiter; [opr] is similar, but on the right of the term *)
......@@ -244,25 +264,7 @@ and print_tnode ?(boxed=false) opl opr info fmt t = match t.t_node with
| Tvar v ->
print_vs fmt v
| Tconst c ->
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";
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_custom "(-%a)%%R";
Number.dec_real_support = Number.Number_unsupported;
Number.hex_real_support = Number.Number_unsupported;
Number.frac_real_support = Number.Number_custom
(Number.PrintFracReal ("%s%%R", "(%s * %s)%%R", "(%s / %s)%%R"));
Number.def_real_support = Number.Number_unsupported;
} in
Number.print number_format fmt c
Number.print (number_format info) fmt c
| Tlet (t1,tb) ->
let v,t2 = t_open_bound tb in
fprintf fmt (protect_on opr "let %a :=@ %a in@ %a")
......
......@@ -96,25 +96,26 @@ let print_typed_var info fmt vs =
let print_var_list info fmt vsl =
print_list comma (print_typed_var info) fmt vsl
let number_format = {
Number.long_int_support = `Default;
Number.negative_int_support = `Default;
Number.dec_int_support = `Default;
Number.hex_int_support = `Unsupported;
Number.oct_int_support = `Unsupported;
Number.bin_int_support = `Unsupported;
Number.negative_real_support = `Default;
Number.dec_real_support = `Unsupported;
Number.hex_real_support = `Unsupported;
Number.frac_real_support =
`Custom
((fun fmt i -> pp_print_string fmt i),
(fun fmt i n -> fprintf fmt "(%s * %s)" i n),
(fun fmt i n -> fprintf fmt "(%s / %s)" i n));
}
(** expr *)
let rec print_term info fmt t = match t.t_node with
| Tconst c ->
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
(Number.PrintFracReal ("%s", "(%s * %s)", "(%s / %s)"));
Number.def_real_support = Number.Number_unsupported;
} in
Number.print number_format fmt c
| Tvar v -> print_var fmt v
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
......
......@@ -144,19 +144,16 @@ let print_ident fmt id =
fprintf fmt "%s" (id_unique ident_printer id)
let number_format = {
Number.long_int_support = true;
Number.extra_leading_zeros_support = true;
Number.negative_int_support = Number.Number_custom "-%a";
Number.dec_int_support = Number.Number_default;
Number.hex_int_support = Number.Number_default;
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";
Number.dec_real_support = Number.Number_default;
Number.hex_real_support = Number.Number_default;
Number.frac_real_support = Number.Number_unsupported;
Number.def_real_support = Number.Number_unsupported;
Number.long_int_support = `Default;
Number.negative_int_support = `Custom (fun fmt f -> fprintf fmt "-%t" f);
Number.dec_int_support = `Default;
Number.hex_int_support = `Default;
Number.oct_int_support = `Unsupported;
Number.bin_int_support = `Unsupported;
Number.negative_real_support = `Custom (fun fmt f -> fprintf fmt "-%t" f);
Number.dec_real_support = `Default;
Number.hex_real_support = `Default;
Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
}
type constant = Enum of term * int | Value of term | Varying
......
......@@ -193,37 +193,37 @@ let binop_name = function
| Timplies -> "HOL.implies"
| Tiff -> "HOL.eq"
let rec print_term info defs fmt t = match t.t_node with
| Tvar v ->
print_var info fmt v
| Tconst c ->
let number_format = {
Number.long_int_support = true;
Number.extra_leading_zeros_support = true;
Number.negative_int_support = Number.Number_unsupported;
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_unsupported;
Number.dec_real_support = Number.Number_unsupported;
Number.hex_real_support = Number.Number_unsupported;
Number.frac_real_support = Number.Number_custom
(Number.PrintFracReal
("<num val=\"%s\"><type name=\"Real.real\"/></num>",
let number_format = {
Number.long_int_support = `Default;
Number.negative_int_support = `Custom (fun _ _ -> assert false);
Number.dec_int_support = `Default;
Number.hex_int_support = `Unsupported;
Number.oct_int_support = `Unsupported;
Number.bin_int_support = `Unsupported;
Number.negative_real_support = `Custom (fun _ _ -> assert false);
Number.dec_real_support = `Unsupported;
Number.hex_real_support = `Unsupported;
Number.frac_real_support =
`Custom
((fun fmt i -> fprintf fmt "<num val=\"%s\"><type name=\"Real.real\"/></num>" i),
(fun fmt i n -> fprintf fmt
"<app>\
<const name=\"Groups.times_class.times\"/>\