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
b9df0ec0
Commit
b9df0ec0
authored
Jul 21, 2010
by
Andrei Paskevich
Browse files
rename trl_equal to tr_equal for consistency with tr_map and tr_fold
parent
c0c56b43
Changes
4
Hide whitespace changes
Inline
Side-by-side
src/core/term.ml
View file @
b9df0ec0
...
...
@@ -325,8 +325,7 @@ let e_equal e1 e2 = match e1, e2 with
|
Fmla
f1
,
Fmla
f2
->
f_equal
f1
f2
|
_
->
false
let
tr_equal
=
list_all2
e_equal
let
trl_equal
=
list_all2
tr_equal
let
tr_equal
=
list_all2
(
list_all2
e_equal
)
(* expr and trigger traversal *)
...
...
@@ -430,7 +429,7 @@ module Hsfmla = Hashcons.Make (struct
let
f_eq_quant
(
vl1
,_,_,
s1
,
tl1
,
f1
)
(
vl2
,_,_,
s2
,
tl2
,
f2
)
=
f_equal
f1
f2
&&
list_all2
vs_equal
vl1
vl2
&&
bmap_equal
s1
s2
&&
tr
l
_equal
tl1
tl2
bmap_equal
s1
s2
&&
tr_equal
tl1
tl2
let
f_equal_node
f1
f2
=
match
f1
,
f2
with
|
Fapp
(
s1
,
l1
)
,
Fapp
(
s2
,
l2
)
->
...
...
@@ -1139,7 +1138,7 @@ let f_map fnT fnF f = f_label_copy f (match f.f_node with
|
Fapp
(
p
,
tl
)
->
f_app_unsafe
p
(
List
.
map
fnT
tl
)
|
Fquant
(
q
,
b
)
->
let
vl
,
tl
,
f1
=
f_open_quant
b
in
let
f1'
=
fnF
f1
in
let
tl'
=
tr_map
fnT
fnF
tl
in
if
f_equal
f1'
f1
&&
tr
l
_equal
tl'
tl
then
f
if
f_equal
f1'
f1
&&
tr_equal
tl'
tl
then
f
else
f_quant
q
vl
tl'
f1'
|
Fbinop
(
op
,
f1
,
f2
)
->
f_binary
op
(
fnF
f1
)
(
fnF
f2
)
|
Fnot
f1
->
f_not
(
fnF
f1
)
...
...
@@ -1295,7 +1294,7 @@ let f_map_cont fnT fnF contF f =
|
Fquant
(
q
,
b
)
->
let
vl
,
tl
,
f1
=
f_open_quant
b
in
let
f_quant
el
e1
=
if
f_equal
e1
f1
&&
tr
l
_equal
el
tl
if
f_equal
e1
f1
&&
tr_equal
el
tl
then
f
else
f_quant
q
vl
el
e1
in
let
cont_dot
tl
f1
=
contF
(
f_quant
tl
f1
)
in
...
...
@@ -1695,7 +1694,7 @@ let f_map_simp fnT fnF f = f_label_copy f (match f.f_node with
|
Fapp
(
p
,
tl
)
->
f_app_unsafe
p
(
List
.
map
fnT
tl
)
|
Fquant
(
q
,
b
)
->
let
vl
,
tl
,
f1
=
f_open_quant
b
in
let
f1'
=
fnF
f1
in
let
tl'
=
tr_map
fnT
fnF
tl
in
if
f_equal
f1'
f1
&&
tr
l
_equal
tl'
tl
&&
not
(
is_true_false
f1
)
then
f
if
f_equal
f1'
f1
&&
tr_equal
tl'
tl
&&
not
(
is_true_false
f1
)
then
f
else
f_quant_simp
q
vl
tl'
f1'
|
Fbinop
(
op
,
f1
,
f2
)
->
f_binary_simp
op
(
fnF
f1
)
(
fnF
f2
)
|
Fnot
f1
->
f_not_simp
(
fnF
f1
)
...
...
src/core/term.mli
View file @
b9df0ec0
...
...
@@ -177,8 +177,7 @@ val t_equal : term -> term -> bool
val
f_equal
:
fmla
->
fmla
->
bool
val
e_equal
:
expr
->
expr
->
bool
val
tr_equal
:
trigger
->
trigger
->
bool
val
trl_equal
:
trigger
list
->
trigger
list
->
bool
val
tr_equal
:
trigger
list
->
trigger
list
->
bool
(** smart constructors for term *)
...
...
src/transform/eliminate_algebraic.ml
View file @
b9df0ec0
...
...
@@ -145,7 +145,7 @@ and rewriteF kn state av sign f = match f.f_node with
(
rewriteF
kn
state
Svs
.
empty
sign
)
tr
in
let
av
=
List
.
fold_left
(
fun
s
v
->
Svs
.
add
v
s
)
av
vl
in
let
f1'
=
rewriteF
kn
state
av
sign
f1
in
if
f_equal
f1'
f1
&&
tr
l
_equal
tr'
tr
then
f
else
f_quant
q
vl
tr'
f1'
if
f_equal
f1'
f1
&&
tr_equal
tr'
tr
then
f
else
f_quant
q
vl
tr'
f1'
|
Fbinop
(
o
,
_
,
_
)
when
(
o
=
Fand
&&
sign
)
||
(
o
=
For
&&
not
sign
)
->
f_map_sign
(
rewriteT
kn
state
)
(
rewriteF
kn
state
av
)
sign
f
|
Flet
(
t1
,
_
)
->
...
...
src/transform/encoding_simple.ml
View file @
b9df0ec0
...
...
@@ -158,7 +158,7 @@ and rewrite_fmla tenv vm f =
let
vm'
,
vl'
=
Util
.
map_fold_left
add
vm
vl
in
let
tl'
=
tr_map
(
fnT
vm'
)
(
fnF
vm'
)
tl
in
let
f1'
=
fnF
vm'
f1
in
if
List
.
for_all2
vs_equal
vl
vl'
&&
tr
l
_equal
tl
tl'
&&
f_equal
f1
f1'
if
List
.
for_all2
vs_equal
vl
vl'
&&
tr_equal
tl
tl'
&&
f_equal
f1
f1'
then
f
else
f_quant
q
vl'
tl'
f1'
|
Flet
(
t1
,
b
)
->
let
u
,
f1
=
f_open_bound
b
in
...
...
Write
Preview
Markdown
is supported
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