Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
8c230484
Commit
8c230484
authored
Nov 06, 2012
by
Andrei Paskevich
Browse files
move everything related to numerals to Number
parent
a77f70a0
Changes
28
Hide whitespace changes
Inline
Side-by-side
Makefile.in
View file @
8c230484
...
...
@@ -106,7 +106,7 @@ LIBGENERATED = src/util/config.ml src/util/rc.ml src/parser/lexer.ml \
LIB_UTIL
=
config util opt lists strings extmap exthtbl weakhtbl
\
hashcons stdlib exn_printer pp debug loc print_tree
\
cmdline warning sysutil rc plugin
cmdline warning sysutil rc plugin
number
LIB_CORE
=
ident ty term pattern decl theory task pretty
env
trans printer
...
...
@@ -127,7 +127,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
introduction abstraction close_epsilon lift_epsilon
\
eval_match instantiate_predicate smoke_detector
LIB_PRINTER
=
print_number
alt_ergo why3printer smtv1 smtv2 coq pvs
\
LIB_PRINTER
=
alt_ergo why3printer smtv1 smtv2 coq pvs
\
simplify gappa cvc3 yices
LIB_SESSION
=
xml termcode session session_tools session_scheduler
...
...
plugins/tptp/tptp_printer.ml
View file @
8c230484
...
...
@@ -84,18 +84,18 @@ and print_term info fmt t = match t.t_node with
print_app
info
fmt
ls
tl
t
.
t_ty
|
Tconst
c
->
let
number_format
=
{
Print_n
umber
.
long_int_support
=
true
;
Print_n
umber
.
dec_int_support
=
Print_n
umber
.
Number_default
;
Print_n
umber
.
hex_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
oct_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
bin_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
def_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
dec_real_support
=
Print_n
umber
.
Number_default
;
Print_n
umber
.
hex_real_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
frac_real_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
def_real_support
=
Print_n
umber
.
Number_unsupported
;
N
umber
.
long_int_support
=
true
;
N
umber
.
dec_int_support
=
N
umber
.
Number_default
;
N
umber
.
hex_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
oct_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
bin_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
def_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
dec_real_support
=
N
umber
.
Number_default
;
N
umber
.
hex_real_support
=
N
umber
.
Number_unsupported
;
N
umber
.
frac_real_support
=
N
umber
.
Number_unsupported
;
N
umber
.
def_real_support
=
N
umber
.
Number_unsupported
;
}
in
Print_n
umber
.
print
number_format
fmt
c
N
umber
.
print
number_format
fmt
c
|
Tlet
(
t1
,
tb
)
->
let
v
,
t2
=
t_open_bound
tb
in
fprintf
fmt
"$let_tt(%a@ =@ %a,@ %a)"
...
...
plugins/tptp/tptp_typing.ml
View file @
8c230484
...
...
@@ -285,8 +285,8 @@ let rec ty denv env impl { e_loc = loc; e_node = n } = match n with
|
Elet
_
|
Eite
_
|
Eqnt
_
|
Ebin
_
|
Enot
_
|
Eequ
_
|
Edob
_
|
Enum
_
->
error
~
loc
TypeExpected
let
t_int_const
s
=
t_const
(
ConstInt
(
int_const_dec
imal
s
))
let
t_real_const
r
=
t_const
(
ConstReal
r
)
let
t_int_const
s
=
t_const
(
Number
.
ConstInt
(
Number
.
int_const_dec
s
))
let
t_real_const
r
=
t_const
(
Number
.
ConstReal
r
)
let
rec
term
denv
env
impl
{
e_loc
=
loc
;
e_node
=
n
}
=
match
n
with
|
Eapp
(
aw
,
al
)
->
...
...
@@ -305,7 +305,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_real_const
(
RConstDecimal
(
i
,
Opt
.
get_def
"0"
f
,
e
))
t_const
(
Number
.
ConstReal
(
Number
.
real_const_dec
i
(
Opt
.
get_def
"0"
f
)
e
))
|
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.ml
View file @
8c230484
...
...
@@ -391,7 +391,7 @@ let rec tr_positive p = match kind_of_term p with
let
const_of_big_int
b
=
Term
.
t_const
(
T
er
m
.
ConstInt
(
T
er
m
.
int_const_dec
imal
(
Big_int
.
string_of_big_int
b
)))
(
Numb
er
.
ConstInt
(
Numb
er
.
int_const_dec
(
Big_int
.
string_of_big_int
b
)))
(* translates a closed Coq term t:Z or R into a FOL term of type int or real *)
let
rec
tr_arith_constant
t
=
match
kind_of_term
t
with
...
...
@@ -401,9 +401,9 @@ let rec tr_arith_constant t = match kind_of_term t with
|
App
(
f
,
[
|
a
|
])
when
is_constant
f
coq_Zneg
->
const_of_big_int
(
Big_int
.
minus_big_int
(
tr_positive
a
))
|
Const
_
when
is_constant
t
coq_R0
->
Term
.
t_const
(
T
er
m
.
ConstReal
(
Term
.
RConstDecimal
(
"0"
,
"0"
,
None
))
)
Term
.
t_const
(
Numb
er
.
ConstReal
(
Number
.
real_const_dec
"0"
"0"
None
))
|
Const
_
when
is_constant
t
coq_R1
->
Term
.
t_const
(
T
er
m
.
ConstReal
(
Term
.
RConstDecimal
(
"1"
,
"0"
,
None
))
)
Term
.
t_const
(
Numb
er
.
ConstReal
(
Number
.
real_const_dec
"1"
"0"
None
))
(* | App (f, [|a;b|]) when f = Lazy.force coq_Rplus -> *)
(* let ta = tr_arith_constant a in *)
(* let tb = tr_arith_constant b in *)
...
...
src/core/pretty.ml
View file @
8c230484
...
...
@@ -12,6 +12,7 @@
open
Format
open
Pp
open
Stdlib
open
Number
open
Ident
open
Ty
open
Term
...
...
@@ -129,13 +130,14 @@ let rec print_ty_node inn fmt ty = match ty.ty_node with
let
print_ty
=
print_ty_node
false
let
print_const
fmt
=
function
|
ConstInt
(
IConstDecimal
s
)
->
fprintf
fmt
"%s"
s
|
ConstInt
(
IConstHexa
s
)
->
fprintf
fmt
"0x%s"
s
|
ConstInt
(
IConstOctal
s
)
->
fprintf
fmt
"0o%s"
s
|
ConstInt
(
IConstBinary
s
)
->
fprintf
fmt
"0b%s"
s
|
ConstReal
(
RConstDecimal
(
i
,
f
,
None
))
->
fprintf
fmt
"%s.%s"
i
f
|
ConstReal
(
RConstDecimal
(
i
,
f
,
Some
e
))
->
fprintf
fmt
"%s.%se%s"
i
f
e
|
ConstReal
(
RConstHexa
(
i
,
f
,
e
))
->
fprintf
fmt
"0x%s.%sp%s"
i
f
e
|
ConstInt
(
IConstDec
s
)
->
fprintf
fmt
"%s"
s
|
ConstInt
(
IConstHex
s
)
->
fprintf
fmt
"0x%s"
s
|
ConstInt
(
IConstOct
s
)
->
fprintf
fmt
"0o%s"
s
|
ConstInt
(
IConstBin
s
)
->
fprintf
fmt
"0b%s"
s
|
ConstReal
(
RConstDec
(
i
,
f
,
None
))
->
fprintf
fmt
"%s.%s"
i
f
|
ConstReal
(
RConstDec
(
i
,
f
,
Some
e
))
->
fprintf
fmt
"%s.%se%s"
i
f
e
|
ConstReal
(
RConstHex
(
i
,
f
,
Some
e
))
->
fprintf
fmt
"0x%s.%sp%s"
i
f
e
|
ConstReal
(
RConstHex
(
i
,
f
,
None
))
->
fprintf
fmt
"0x%s.%s"
i
f
(* can the type of a value be derived from the type of the arguments? *)
let
unambig_fs
fs
=
...
...
@@ -518,8 +520,6 @@ let () = Exn_printer.register
fprintf
fmt
"Variable %a is used twice"
print_vsty
vs
|
Term
.
UncoveredVar
vs
->
fprintf
fmt
"Variable %a uncovered in
\"
or
\"
-pattern"
print_vsty
vs
|
Term
.
InvalidConstantLiteral
(
n
,
s
)
->
fprintf
fmt
"Invalid constant literal in base %d: '%s'"
n
s
|
Term
.
FunctionSymbolExpected
ls
->
fprintf
fmt
"Not a function symbol: %a"
print_ls
ls
|
Term
.
PredicateSymbolExpected
ls
->
...
...
src/core/pretty.mli
View file @
8c230484
...
...
@@ -35,7 +35,7 @@ val print_vsty : formatter -> vsymbol -> unit (* variable : type *)
val
print_quant
:
formatter
->
quant
->
unit
(* quantifier *)
val
print_binop
:
asym
:
bool
->
formatter
->
binop
->
unit
(* binary operator *)
val
print_const
:
formatter
->
constant
->
unit
(* int/real constant *)
val
print_const
:
formatter
->
Number
.
constant
->
unit
(* int/real constant *)
val
print_pat
:
formatter
->
pattern
->
unit
(* pattern *)
val
print_term
:
formatter
->
term
->
unit
(* term *)
...
...
src/core/term.ml
View file @
8c230484
...
...
@@ -251,51 +251,6 @@ type binop =
|
Timplies
|
Tiff
type
integer_constant
=
|
IConstDecimal
of
string
|
IConstHexa
of
string
|
IConstOctal
of
string
|
IConstBinary
of
string
exception
InvalidConstantLiteral
of
int
*
string
let
invalid_constant_literal
n
s
=
raise
(
InvalidConstantLiteral
(
n
,
s
))
let
check_integer_literal
n
f
s
=
let
l
=
String
.
length
s
in
if
l
=
0
then
invalid_constant_literal
n
s
;
for
i
=
0
to
l
-
1
do
if
not
(
f
s
.
[
i
])
then
invalid_constant_literal
n
s
;
done
let
int_const_decimal
s
=
check_integer_literal
10
(
function
'
0
'
..
'
9
'
->
true
|
_
->
false
)
s
;
IConstDecimal
s
let
int_const_hexa
s
=
check_integer_literal
16
(
function
'
0
'
..
'
9
'
|
'
A'
..
'
F'
|
'
a'
..
'
f'
->
true
|
_
->
false
)
s
;
IConstHexa
s
let
int_const_octal
s
=
check_integer_literal
8
(
function
'
0
'
..
'
7
'
->
true
|
_
->
false
)
s
;
IConstOctal
s
let
int_const_binary
s
=
check_integer_literal
8
(
function
'
0
'
..
'
1
'
->
true
|
_
->
false
)
s
;
IConstBinary
s
type
real_constant
=
|
RConstDecimal
of
string
*
string
*
string
option
(* int / frac / exp *)
|
RConstHexa
of
string
*
string
*
string
type
constant
=
|
ConstInt
of
integer_constant
|
ConstReal
of
real_constant
type
term
=
{
t_node
:
term_node
;
t_ty
:
ty
option
;
...
...
@@ -307,7 +262,7 @@ type term = {
and
term_node
=
|
Tvar
of
vsymbol
|
Tconst
of
constant
|
Tconst
of
Number
.
constant
|
Tapp
of
lsymbol
*
term
list
|
Tif
of
term
*
term
*
term
|
Tlet
of
term
*
term_bound
...
...
@@ -758,11 +713,11 @@ let fs_app fs tl ty = t_app fs tl (Some ty)
let
ps_app
ps
tl
=
t_app
ps
tl
None
let
t_const
c
=
match
c
with
|
ConstInt
_
->
t_const
c
ty_int
|
ConstReal
_
->
t_const
c
ty_real
|
Number
.
ConstInt
_
->
t_const
c
ty_int
|
Number
.
ConstReal
_
->
t_const
c
ty_real
let
t_nat_const
n
=
t_const
(
ConstInt
(
int_const_dec
imal
(
string_of_int
n
)))
t_const
(
Number
.
ConstInt
(
Number
.
int_const_dec
(
string_of_int
n
)))
let
t_if
f
t1
t2
=
t_ty_check
t2
t1
.
t_ty
;
...
...
src/core/term.mli
View file @
8c230484
...
...
@@ -62,7 +62,6 @@ exception UncoveredVar of vsymbol
exception
BadArity
of
lsymbol
*
int
*
int
exception
FunctionSymbolExpected
of
lsymbol
exception
PredicateSymbolExpected
of
lsymbol
exception
InvalidConstantLiteral
of
int
*
string
(** {2 Patterns} *)
...
...
@@ -110,29 +109,6 @@ type binop =
|
Timplies
|
Tiff
type
integer_constant
=
private
|
IConstDecimal
of
string
|
IConstHexa
of
string
|
IConstOctal
of
string
|
IConstBinary
of
string
val
int_const_decimal
:
string
->
integer_constant
val
int_const_hexa
:
string
->
integer_constant
val
int_const_octal
:
string
->
integer_constant
val
int_const_binary
:
string
->
integer_constant
(** these four functions construct integer constant terms from some
string [s] of digits in the corresponding base. Exception
InvalidConstantLiteral(base,s) is raised if [s] contains invalid
characters for the given base. *)
type
real_constant
=
|
RConstDecimal
of
string
*
string
*
string
option
(* int / frac / exp *)
|
RConstHexa
of
string
*
string
*
string
type
constant
=
|
ConstInt
of
integer_constant
|
ConstReal
of
real_constant
type
term
=
private
{
t_node
:
term_node
;
t_ty
:
ty
option
;
...
...
@@ -144,7 +120,7 @@ type term = private {
and
term_node
=
private
|
Tvar
of
vsymbol
|
Tconst
of
constant
|
Tconst
of
Number
.
constant
|
Tapp
of
lsymbol
*
term
list
|
Tif
of
term
*
term
*
term
|
Tlet
of
term
*
term_bound
...
...
@@ -220,7 +196,7 @@ val ls_arg_inst : lsymbol -> term list -> ty Mtv.t
val
ls_app_inst
:
lsymbol
->
term
list
->
ty
option
->
ty
Mtv
.
t
val
t_var
:
vsymbol
->
term
val
t_const
:
constant
->
term
val
t_const
:
Number
.
constant
->
term
val
t_if
:
term
->
term
->
term
->
term
val
t_let
:
term
->
term_bound
->
term
val
t_case
:
term
->
term_branch
list
->
term
...
...
src/parser/denv.mli
View file @
8c230484
...
...
@@ -60,7 +60,7 @@ type dterm = { dt_node : dterm_node; dt_ty : dty }
and
dterm_node
=
|
Tvar
of
string
|
Tgvar
of
vsymbol
|
Tconst
of
constant
|
Tconst
of
Number
.
constant
|
Tapp
of
lsymbol
*
dterm
list
|
Tif
of
dfmla
*
dterm
*
dterm
|
Tlet
of
dterm
*
ident
*
dterm
...
...
src/parser/lexer.mll
View file @
8c230484
...
...
@@ -184,22 +184,23 @@ rule token = parse
|
uident
as
id
{
UIDENT
id
}
|
[
'
0
'
-
'
9
'
]
[
'
0
'
-
'
9
'
'
_'
]
*
as
s
{
INTEGER
(
int_const_dec
imal
(
remove_underscores
s
))
}
{
INTEGER
(
Number
.
int_const_dec
(
remove_underscores
s
))
}
|
'
0
'
[
'
x'
'
X'
]
([
'
0
'
-
'
9
'
'
A'
-
'
F'
'
a'
-
'
f'
][
'
0
'
-
'
9
'
'
A'
-
'
F'
'
a'
-
'
f'
'
_'
]
*
as
s
)
{
INTEGER
(
int_const_hex
a
(
remove_underscores
s
))
}
{
INTEGER
(
Number
.
int_const_hex
(
remove_underscores
s
))
}
|
'
0
'
[
'
o'
'
O'
]
([
'
0
'
-
'
7
'
]
[
'
0
'
-
'
7
'
'
_'
]
*
as
s
)
{
INTEGER
(
int_const_oct
al
(
remove_underscores
s
))
}
{
INTEGER
(
Number
.
int_const_oct
(
remove_underscores
s
))
}
|
'
0
'
[
'
b'
'
B'
]
([
'
0
'
-
'
1
'
]
[
'
0
'
-
'
1
'
'
_'
]
*
as
s
)
{
INTEGER
(
int_const_bin
ary
(
remove_underscores
s
))
}
{
INTEGER
(
Number
.
int_const_bin
(
remove_underscores
s
))
}
|
(
digit
+
as
i
)
(
""
as
f
)
[
'
e'
'
E'
]
([
'
-
'
'
+
'
]
?
digit
+
as
e
)
|
(
digit
+
as
i
)
'.'
(
digit
*
as
f
)
([
'
e'
'
E'
]
([
'
-
'
'
+
'
]
?
digit
+
as
e
))
?
|
(
digit
*
as
i
)
'.'
(
digit
+
as
f
)
([
'
e'
'
E'
]
([
'
-
'
'
+
'
]
?
digit
+
as
e
))
?
{
FLOAT
(
RConstDecimal
(
i
,
f
,
Opt
.
map
remove_leading_plus
e
))
}
|
'
0
'
[
'
x'
'
X'
]
((
hexadigit
*
as
i
)
'.'
(
hexadigit
+
as
f
)
|
(
hexadigit
+
as
i
)
'.'
(
hexadigit
*
as
f
)
|
(
hexadigit
+
as
i
)
(
""
as
f
))
[
'
p'
'
P'
]
([
'
-
'
'
+
'
]
?
digit
+
as
e
)
{
FLOAT
(
RConstHexa
(
i
,
f
,
remove_leading_plus
e
))
}
{
FLOAT
(
Number
.
real_const_dec
i
f
(
Opt
.
map
remove_leading_plus
e
))
}
|
'
0
'
[
'
x'
'
X'
]
(
digit
+
as
i
)
(
""
as
f
)
[
'
p'
'
P'
]
([
'
-
'
'
+
'
]
?
digit
+
as
e
)
|
'
0
'
[
'
x'
'
X'
]
(
digit
+
as
i
)
'.'
(
digit
*
as
f
)
([
'
p'
'
P'
]
([
'
-
'
'
+
'
]
?
digit
+
as
e
))
?
|
'
0
'
[
'
x'
'
X'
]
(
digit
*
as
i
)
'.'
(
digit
+
as
f
)
([
'
p'
'
P'
]
([
'
-
'
'
+
'
]
?
digit
+
as
e
))
?
{
FLOAT
(
Number
.
real_const_hex
i
f
(
Opt
.
map
remove_leading_plus
e
))
}
|
"(*)"
{
LEFTPAR_STAR_RIGHTPAR
}
|
"(*"
...
...
src/parser/parser.mly
View file @
8c230484
...
...
@@ -157,10 +157,10 @@ end
let
small_integer
i
=
try
match
i
with
|
T
er
m
.
IConstDec
imal
s
->
int_of_string
s
|
T
er
m
.
IConstHex
a
s
->
int_of_string
(
"0x"
^
s
)
|
T
er
m
.
IConstOct
al
s
->
int_of_string
(
"0o"
^
s
)
|
T
er
m
.
IConstBin
ary
s
->
int_of_string
(
"0b"
^
s
)
|
Numb
er
.
IConstDec
s
->
int_of_string
s
|
Numb
er
.
IConstHex
s
->
int_of_string
(
"0x"
^
s
)
|
Numb
er
.
IConstOct
s
->
int_of_string
(
"0o"
^
s
)
|
Numb
er
.
IConstBin
s
->
int_of_string
(
"0b"
^
s
)
with
Failure
_
->
raise
Parsing
.
Parse_error
let
qualid_last
=
function
...
...
@@ -670,8 +670,8 @@ list1_lexpr_arg:
;
constant
:
|
INTEGER
{
T
er
m
.
ConstInt
$
1
}
|
FLOAT
{
T
er
m
.
ConstReal
$
1
}
|
INTEGER
{
Numb
er
.
ConstInt
$
1
}
|
FLOAT
{
Numb
er
.
ConstReal
$
1
}
;
lexpr_arg
:
...
...
src/parser/ptree.ml
View file @
8c230484
...
...
@@ -15,9 +15,9 @@ type loc = Loc.position
(*s Logical expressions (for both terms and predicates) *)
type
integer_constant
=
T
er
m
.
integer_constant
type
real_constant
=
T
er
m
.
real_constant
type
constant
=
T
er
m
.
constant
type
integer_constant
=
Numb
er
.
integer_constant
type
real_constant
=
Numb
er
.
real_constant
type
constant
=
Numb
er
.
constant
type
label
=
|
Lstr
of
Ident
.
label
...
...
src/parser/typing.ml
View file @
8c230484
...
...
@@ -471,9 +471,9 @@ and dterm_node ~localize loc uc env = function
let
s
,
tyl
,
ty
=
specialize_fsymbol
(
Qident
x
)
uc
in
let
tl
=
dtype_args
~
localize
s
loc
uc
env
tyl
[
e1
;
e2
]
in
Tapp
(
s
,
tl
)
,
ty
|
PPconst
(
ConstInt
_
as
c
)
->
|
PPconst
(
Number
.
ConstInt
_
as
c
)
->
Tconst
c
,
tyapp
Ty
.
ts_int
[]
|
PPconst
(
ConstReal
_
as
c
)
->
|
PPconst
(
Number
.
ConstReal
_
as
c
)
->
Tconst
c
,
tyapp
Ty
.
ts_real
[]
|
PPlet
(
x
,
e1
,
e2
)
->
let
e1
=
dterm
~
localize
uc
env
e1
in
...
...
src/printer/alt_ergo.ml
View file @
8c230484
...
...
@@ -102,18 +102,18 @@ let unambig_fs fs =
let
rec
print_term
info
fmt
t
=
match
t
.
t_node
with
|
Tconst
c
->
let
number_format
=
{
Print_n
umber
.
long_int_support
=
true
;
Print_n
umber
.
dec_int_support
=
Print_n
umber
.
Number_default
;
Print_n
umber
.
hex_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
oct_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
bin_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
def_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
dec_real_support
=
Print_n
umber
.
Number_default
;
Print_n
umber
.
hex_real_support
=
Print_n
umber
.
Number_default
;
Print_n
umber
.
frac_real_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
def_real_support
=
Print_n
umber
.
Number_unsupported
;
N
umber
.
long_int_support
=
true
;
N
umber
.
dec_int_support
=
N
umber
.
Number_default
;
N
umber
.
hex_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
oct_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
bin_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
def_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
dec_real_support
=
N
umber
.
Number_default
;
N
umber
.
hex_real_support
=
N
umber
.
Number_default
;
N
umber
.
frac_real_support
=
N
umber
.
Number_unsupported
;
N
umber
.
def_real_support
=
N
umber
.
Number_unsupported
;
}
in
Print_n
umber
.
print
number_format
fmt
c
N
umber
.
print
number_format
fmt
c
|
Tvar
{
vs_name
=
id
}
->
print_ident
fmt
id
|
Tapp
(
ls
,
tl
)
->
begin
match
query_syntax
info
.
info_syn
ls
.
ls_name
with
...
...
src/printer/coq.ml
View file @
8c230484
...
...
@@ -253,19 +253,19 @@ and print_tnode opl opr info fmt t = match t.t_node with
print_vs
fmt
v
|
Tconst
c
->
let
number_format
=
{
Print_n
umber
.
long_int_support
=
true
;
Print_n
umber
.
dec_int_support
=
Print_n
umber
.
Number_custom
"%s%%Z"
;
Print_n
umber
.
hex_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
oct_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
bin_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
def_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
dec_real_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
hex_real_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
frac_real_support
=
Print_n
umber
.
Number_custom
(
Print_n
umber
.
PrintFracReal
(
"%s%%R"
,
"(%s * %s)%%R"
,
"(%s / %s)%%R"
));
Print_n
umber
.
def_real_support
=
Print_n
umber
.
Number_unsupported
;
N
umber
.
long_int_support
=
true
;
N
umber
.
dec_int_support
=
N
umber
.
Number_custom
"%s%%Z"
;
N
umber
.
hex_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
oct_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
bin_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
def_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
dec_real_support
=
N
umber
.
Number_unsupported
;
N
umber
.
hex_real_support
=
N
umber
.
Number_unsupported
;
N
umber
.
frac_real_support
=
N
umber
.
Number_custom
(
N
umber
.
PrintFracReal
(
"%s%%R"
,
"(%s * %s)%%R"
,
"(%s / %s)%%R"
));
N
umber
.
def_real_support
=
N
umber
.
Number_unsupported
;
}
in
Print_n
umber
.
print
number_format
fmt
c
N
umber
.
print
number_format
fmt
c
|
Tif
(
f
,
t1
,
t2
)
->
fprintf
fmt
(
protect_on
opr
"if %a@ then %a@ else %a"
)
(
print_fmla
info
)
f
(
print_term
info
)
t1
(
print_opl_term
info
)
t2
...
...
src/printer/cvc3.ml
View file @
8c230484
...
...
@@ -120,19 +120,19 @@ let print_var_list info fmt vsl =
let
rec
print_term
info
fmt
t
=
match
t
.
t_node
with
|
Tconst
c
->
let
number_format
=
{
Print_n
umber
.
long_int_support
=
true
;
Print_n
umber
.
dec_int_support
=
Print_n
umber
.
Number_default
;
Print_n
umber
.
hex_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
oct_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
bin_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
def_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
dec_real_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
hex_real_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
frac_real_support
=
Print_n
umber
.
Number_custom
(
Print_n
umber
.
PrintFracReal
(
"%s"
,
"(%s * %s)"
,
"(%s / %s)"
));
Print_n
umber
.
def_real_support
=
Print_n
umber
.
Number_unsupported
;
N
umber
.
long_int_support
=
true
;
N
umber
.
dec_int_support
=
N
umber
.
Number_default
;
N
umber
.
hex_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
oct_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
bin_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
def_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
dec_real_support
=
N
umber
.
Number_unsupported
;
N
umber
.
hex_real_support
=
N
umber
.
Number_unsupported
;
N
umber
.
frac_real_support
=
N
umber
.
Number_custom
(
N
umber
.
PrintFracReal
(
"%s"
,
"(%s * %s)"
,
"(%s / %s)"
));
N
umber
.
def_real_support
=
N
umber
.
Number_unsupported
;
}
in
Print_n
umber
.
print
number_format
fmt
c
N
umber
.
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
|
Some
s
->
syntax_arguments_typed
s
(
print_term
info
)
...
...
src/printer/gappa.ml
View file @
8c230484
...
...
@@ -145,24 +145,24 @@ let print_ident fmt id =
let
constant_value
=
let
number_format
=
{
Print_n
umber
.
long_int_support
=
true
;
Print_n
umber
.
dec_int_support
=
Print_n
umber
.
Number_default
;
Print_n
umber
.
hex_int_support
=
Print_n
umber
.
Number_default
;
Print_n
umber
.
oct_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
bin_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
def_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
dec_real_support
=
Print_n
umber
.
Number_default
;
Print_n
umber
.
hex_real_support
=
Print_n
umber
.
Number_default
;
Print_n
umber
.
frac_real_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
def_real_support
=
Print_n
umber
.
Number_unsupported
;
N
umber
.
long_int_support
=
true
;
N
umber
.
dec_int_support
=
N
umber
.
Number_default
;
N
umber
.
hex_int_support
=
N
umber
.
Number_default
;
N
umber
.
oct_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
bin_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
def_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
dec_real_support
=
N
umber
.
Number_default
;
N
umber
.
hex_real_support
=
N
umber
.
Number_default
;
N
umber
.
frac_real_support
=
N
umber
.
Number_unsupported
;
N
umber
.
def_real_support
=
N
umber
.
Number_unsupported
;
}
in
fun
t
->
match
t
.
t_node
with
|
Tconst
c
->
fprintf
str_formatter
"%a"
(
Print_n
umber
.
print
number_format
)
c
;
fprintf
str_formatter
"%a"
(
N
umber
.
print
number_format
)
c
;
flush_str_formatter
()
|
Tapp
(
ls
,
[{
t_node
=
Tconst
c
}])
when
ls_equal
ls
!
int_minus
||
ls_equal
ls
!
real_minus
->
fprintf
str_formatter
"-%a"
(
Print_n
umber
.
print
number_format
)
c
;
fprintf
str_formatter
"-%a"
(
N
umber
.
print
number_format
)
c
;
flush_str_formatter
()
|
_
->
raise
Not_found
...
...
src/printer/pvs.ml
View file @
8c230484
...
...
@@ -296,21 +296,21 @@ and print_tnode opl opr info fmt t = match t.t_node with
print_vs
fmt
v
|
Tconst
c
->
let
number_format
=
{
Print_n
umber
.
long_int_support
=
true
;
Print_n
umber
.
dec_int_support
=
Print_n
umber
.
Number_custom
"%s"
;
Print_n
umber
.
hex_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
oct_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
bin_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
def_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
dec_real_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
hex_real_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
frac_real_support
=
Print_n
umber
.
Number_custom
(
Print_n
umber
.
PrintFracReal
N
umber
.
long_int_support
=
true
;
N
umber
.
dec_int_support
=
N
umber
.
Number_custom
"%s"
;
N
umber
.
hex_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
oct_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
bin_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
def_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
dec_real_support
=
N
umber
.
Number_unsupported
;
N
umber
.
hex_real_support
=
N
umber
.
Number_unsupported
;
N
umber
.
frac_real_support
=
N
umber
.
Number_custom
(
N
umber
.
PrintFracReal
(
"%s"
,
"(%s * %s)"
,
"(%s / %s)"
));
Print_n
umber
.
def_real_support
=
Print_n
umber
.
Number_unsupported
;
N
umber
.
def_real_support
=
N
umber
.
Number_unsupported
;
}
in
Print_n
umber
.
print
number_format
fmt
c
N
umber
.
print
number_format
fmt
c
|
Tif
(
f
,
t1
,
t2
)
->
fprintf
fmt
"IF %a@ THEN %a@ ELSE %a ENDIF"
(
print_fmla
info
)
f
(
print_term
info
)
t1
(
print_opl_term
info
)
t2
...
...
src/printer/simplify.ml
View file @
8c230484
...
...
@@ -37,18 +37,18 @@ type info = {
let
rec
print_term
info
fmt
t
=
match
t
.
t_node
with
|
Tconst
c
->
let
number_format
=
{
Print_n
umber
.
long_int_support
=
false
;
Print_n
umber
.
dec_int_support
=
Print_n
umber
.
Number_default
;
Print_n
umber
.
hex_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
oct_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
bin_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
def_int_support
=
Print_n
umber
.
Number_custom
"constant_too_large_%s"
;
Print_n
umber
.
dec_real_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
hex_real_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
frac_real_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
def_real_support
=
Print_n
umber
.
Number_custom
"real_constant_%s"
;
N
umber
.
long_int_support
=
false
;
N
umber
.
dec_int_support
=
N
umber
.
Number_default
;
N
umber
.
hex_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
oct_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
bin_int_support
=
N
umber
.
Number_unsupported
;
N
umber
.
def_int_support
=
N
umber
.
Number_custom
"constant_too_large_%s"
;
N
umber
.
dec_real_support
=
N
umber
.
Number_unsupported
;
N
umber
.
hex_real_support
=
N
umber
.
Number_unsupported
;
N
umber
.
frac_real_support
=
N
umber
.
Number_unsupported
;
N
umber
.
def_real_support
=
N
umber
.
Number_custom
"real_constant_%s"
;
}
in
Print_n
umber
.
print
number_format
fmt
c
N
umber
.
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
...
...
src/printer/smtv1.ml
View file @
8c230484
...
...
@@ -62,19 +62,19 @@ let print_type info fmt = catch_unsupportedType (print_type info fmt)
let
rec
print_term
info
fmt
t
=
match
t
.
t_node
with
|
Tconst
c
->
let
number_format
=
{
Print_n
umber
.
long_int_support
=
true
;
Print_n
umber
.
dec_int_support
=
Print_n
umber
.
Number_default
;
Print_n
umber
.
hex_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
oct_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
bin_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
def_int_support
=
Print_n
umber
.
Number_unsupported
;
Print_n
umber
.
dec_real_support
=
Print_n
umber
.
Number_unsupported
;