Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
70ec8ece
Commit
70ec8ece
authored
Jul 19, 2010
by
Andrei Paskevich
Browse files
do not keep ts_int and ts_real in "encoding_simple" (tptp)
parent
6fe4bfe8
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/transform/encoding_simple.ml
View file @
70ec8ece
...
...
@@ -68,14 +68,14 @@ let init_tenv kept =
create_prop_decl
Paxiom
pr_t
t2u2t
]
in
task
,
{
kept
=
option_map
(
Sts
.
add
Explicit_polymorphism
.
ts_ty
)
kept
;
{
kept
=
kept
;
declare_kept
=
Wts
.
memoize
7
declare_kept
;
specials
=
specials
;
ty_uni
=
ty_uni
;
trans_lsymbol
=
Hls
.
create
17
}
let
is_kept
tenv
ts
=
ts_equal
ts
ts_int
||
ts_equal
ts
ts_real
||
ts_equal
ts
Explicit_polymorphism
.
ts_ty
||
ts
.
ts_args
=
[]
&&
match
tenv
.
kept
with
|
Some
s
->
Sts
.
mem
ts
s
|
None
->
true
...
...
@@ -193,7 +193,8 @@ let decl tenv d =
[
decl_map
(
fnT
Mvs
.
empty
)
(
fnF
Mvs
.
empty
)
d
]
let
t
=
Trans
.
on_meta
meta_kept
(
fun
tds
->
let
s
=
Task
.
find_tagged_ts
meta_kept
tds
Sts
.
empty
in
let
s
=
Sts
.
add
ts_int
(
Sts
.
singleton
ts_real
)
in
let
s
=
Task
.
find_tagged_ts
meta_kept
tds
s
in
let
task
,
tenv
=
init_tenv
(
Some
s
)
in
Trans
.
decl
(
decl
tenv
)
task
)
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment