Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
POTTIER Francois
menhir
Commits
1f7802d0
Commit
1f7802d0
authored
Nov 20, 2020
by
POTTIER Francois
Browse files
Invariant: improve [StateVector.join] to preserve physical equality.
parent
5b3a736c
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/invariant.ml
View file @
1f7802d0
...
...
@@ -69,18 +69,24 @@ module StateVector = struct
to (and careful to) compare only vectors of equal length. *)
assert
false
let
rec
join
v1
v2
=
let
rec
leq_
join
v1
v2
=
match
v1
,
v2
with
|
[]
,
[]
->
[]
|
states1
::
v1
,
states2
::
v2
->
Lr1
.
NodeSet
.
union
states1
states2
::
join
v1
v2
|
states1
::
vtail1
,
states2
::
vtail2
->
let
states
=
Lr1
.
NodeSet
.
leq_join
states1
states2
and
vtail
=
leq_join
vtail1
vtail2
in
if
states2
==
states
&&
vtail2
==
vtail
then
v2
else
states
::
vtail
|
_
,
_
->
(* Because all heights are known ahead of time, we are able
to (and careful to) compare only vectors of equal length. *)
assert
false
let
join
=
leq_join
let
push
v
x
=
x
::
v
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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