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
cduce
cduce
Commits
dfdb313f
Commit
dfdb313f
authored
Jul 10, 2007
by
Pietro Abate
Browse files
[r2004-12-22 00:41:57 by afrisch] Better factorization
Original author: afrisch Date: 2004-12-22 00:41:57+00:00
parent
659f225d
Changes
3
Hide whitespace changes
Inline
Side-by-side
types/patterns.ml
View file @
dfdb313f
...
...
@@ -1545,12 +1545,29 @@ module Compile2 = struct
i) t != Empty
ii) X \subset fv(p) *)
module
NodeSet
=
Set
.
Make
(
Node
)
let
pi1
t
=
Types
.
Product
.
pi1
(
Types
.
Product
.
get
t
)
let
pi2
t
=
Types
.
Product
.
pi2
(
Types
.
Product
.
get
t
)
module
Approx
=
struct
type
t
=
(
bool
*
Types
.
const
option
)
option
(* - None: cannot match
- Some (true,_): can only bind to the matched value
- Some (_, Some c): can only bind to the constant c *)
let
merge_times2
a
b
=
match
(
a
,
b
)
with
|
Some
(
x1
,
c1
)
,
Some
(
x2
,
c2
)
->
Some
(
x1
&&
x2
,
match
c1
,
c2
with
|
Some
c1
,
Some
c2
->
Some
(
Types
.
Pair
(
c1
,
c2
))
|
_
->
None
)
|
_
->
Some
(
true
,
None
)
(* Todo: Pair (c,None) *)
let
merge_times1
=
function
|
Some
(
x
,
c
)
->
Some
(
false
,
c
)
|
None
->
None
let
merge
a
b
=
match
(
a
,
b
)
with
|
None
,
x
|
x
,
None
->
x
|
Some
(
x1
,
c1
)
,
Some
(
x2
,
c2
)
->
...
...
@@ -1565,29 +1582,40 @@ module Compile2 = struct
*)
|
_
->
None
)
let
rec
approx
(
a
,
fv
,
d
)
t
xs
=
let
rec
approx
seen
(
(
a
,
fv
,
d
)
as
p
)
t
xs
=
assert
(
Types
.
subtype
t
a
);
assert
(
IdSet
.
subset
xs
fv
);
if
IdSet
.
is_empty
xs
then
IdSet
.
Map
.
empty
else
if
Types
.
is_empty
t
then
IdSet
.
Map
.
constant
None
xs
else
if
(
Types
.
is_empty
t
)
then
IdSet
.
Map
.
constant
None
xs
else
match
d
with
|
Cup
((
a1
,_,_
)
as
p1
,
p2
)
->
IdSet
.
Map
.
merge
merge
(
approx
p1
(
Types
.
cap
t
a1
)
xs
)
(
approx
p2
(
Types
.
diff
t
a1
)
xs
)
(
approx
seen
p1
(
Types
.
cap
t
a1
)
xs
)
(
approx
seen
p2
(
Types
.
diff
t
a1
)
xs
)
|
Cap
((
_
,
fv1
,_
)
as
p1
,
((
_
,
fv2
,_
)
as
p2
))
->
IdSet
.
Map
.
union_disj
(
approx
p1
t
(
IdSet
.
cap
fv1
xs
))
(
approx
p2
t
(
IdSet
.
cap
fv2
xs
))
(
approx
seen
p1
t
(
IdSet
.
cap
fv1
xs
))
(
approx
seen
p2
t
(
IdSet
.
cap
fv2
xs
))
|
Capture
x
->
IdSet
.
Map
.
singleton
x
(
Some
(
true
,
Sample
.
single_opt
t
))
|
Constant
(
x
,
c
)
->
IdSet
.
Map
.
singleton
x
(
Some
(
Types
.
subtype
t
(
Types
.
constant
c
)
,
Some
c
))
|
Times
(
q1
,
q2
)
->
IdSet
.
Map
.
combine
merge_times1
merge_times1
merge_times2
(
approx_node
seen
q1
(
pi1
t
)
(
IdSet
.
cap
q1
.
fv
xs
))
(
approx_node
seen
q2
(
pi2
t
)
(
IdSet
.
cap
q2
.
fv
xs
))
|
_
->
IdSet
.
Map
.
constant
(
Some
(
false
,
None
))
xs
(* TODO: recursive factorization (x,x) -> x *)
and
approx_node
seen
q
t
xs
=
if
(
NodeSet
.
mem
q
seen
)
then
IdSet
.
Map
.
constant
None
xs
else
approx
(
NodeSet
.
add
q
seen
)
q
.
descr
t
xs
let
approx
=
approx
NodeSet
.
empty
end
type
dpat
=
...
...
@@ -1603,8 +1631,6 @@ module Compile2 = struct
and
pat
=
dpat
and
req
=
descr
*
Types
.
t
*
fv
let
pi1
t
=
Types
.
Product
.
pi1
(
Types
.
Product
.
get
t
)
let
pi2
t
=
Types
.
Product
.
pi2
(
Types
.
Product
.
get
t
)
let
rec
eval_pat
(
a
,
fv
,
d
)
t
xs
=
if
Types
.
disjoint
a
t
then
TFail
...
...
types/sortedList.ml
View file @
dfdb313f
...
...
@@ -197,6 +197,16 @@ module Map = struct
|
([]
,
l2
)
->
l2
|
(
l1
,
[]
)
->
l1
let
rec
combine
f1
f2
f12
l1
l2
=
match
(
l1
,
l2
)
with
|
(
x1
,
y1
)
::
q1
,
(
x2
,
y2
)
::
q2
->
let
c
=
X
.
compare
x1
x2
in
if
c
=
0
then
(
x1
,
(
f12
y1
y2
))
::
(
combine
f1
f2
f12
q1
q2
)
else
if
c
<
0
then
(
x1
,
f1
y1
)
::
(
combine
f1
f2
f12
q1
l2
)
else
(
x2
,
f2
y2
)
::
(
combine
f1
f2
f12
l1
q2
)
|
[]
,
l2
->
List
.
map
(
fun
(
x2
,
y2
)
->
(
x2
,
f2
y2
))
l2
|
l1
,
[]
->
List
.
map
(
fun
(
x1
,
y1
)
->
(
x1
,
f1
y1
))
l1
let
rec
cap
f
l1
l2
=
match
(
l1
,
l2
)
with
|
((
x1
,
y1
)
as
t1
)
::
q1
,
((
x2
,
y2
)
as
t2
)
::
q2
->
...
...
types/sortedList.mli
View file @
dfdb313f
...
...
@@ -39,6 +39,8 @@ sig
val
assoc_remove
:
X
.
t
->
'
a
map
->
'
a
*
'
a
map
val
remove
:
X
.
t
->
'
a
map
->
'
a
map
val
merge
:
(
'
a
->
'
a
->
'
a
)
->
'
a
map
->
'
a
map
->
'
a
map
val
combine
:
(
'
a
->
'
c
)
->
(
'
b
->
'
c
)
->
(
'
a
->
'
b
->
'
c
)
->
'
a
map
->
'
b
map
->
'
c
map
val
cap
:
(
'
a
->
'
a
->
'
a
)
->
'
a
map
->
'
a
map
->
'
a
map
val
sub
:
(
'
a
->
'
a
->
'
a
)
->
'
a
map
->
'
a
map
->
'
a
map
...
...
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