Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
58a9737b
Commit
58a9737b
authored
Mar 14, 2016
by
Andrei Paskevich
Browse files
Split_goal: remove the nowdead code
parent
b831b8b5
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
2 additions
and
18 deletions
+2
18
src/transform/split_goal.ml
src/transform/split_goal.ml
+2
18
No files found.
src/transform/split_goal.ml
View file @
58a9737b
...
...
@@ 47,27 +47,11 @@ module M = struct
(* inject formula into monoid. *)
let
(
!+
)
a
=
Comb
(
Base
a
)
let
rec
filter
c
=
match
c
with

Base
_
>
None

Op
(
a
,
b
)
>
match
filter
a
,
filter
b
with

None
,
u

u
,
None
>
u

Some
a
,
Some
b
>
Some
(
Op
(
a
,
b
))
(* monoid law. *)
let
(
++
)
a
b
=
match
a
,
b
with

_
,
Unit
>
a

Unit
,
_
>
b

Zero
ta
,
Comb
b
>
begin
match
filter
b
with

None
>
a

Some
b
>
Comb
(
Op
(
Base
ta
,
b
))
end

Comb
a
,
Zero
tb
>
begin
match
filter
a
with

None
>
b

Some
a
>
Comb
(
Op
(
a
,
Base
tb
))
end

Zero
_
,
Zero
_
>
a

_
,
Unit

Zero
_
,
_
>
a

Unit
,
_

_
,
Zero
_
>
b

Comb
ca
,
Comb
cb
>
Comb
(
Op
(
ca
,
cb
))
(* (base > base) morphism application. *)
...
...
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