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
8c5d10f2
Commit
8c5d10f2
authored
Jul 10, 2007
by
Pietro Abate
Browse files
[r2004-12-23 15:16:34 by afrisch] Simplify
Original author: afrisch Date: 2004-12-23 15:16:34+00:00
parent
3ba84a1e
Changes
1
Hide whitespace changes
Inline
Side-by-side
types/patterns.ml
View file @
8c5d10f2
...
...
@@ -1563,11 +1563,7 @@ end
module
Compile2
=
struct
module
PatList
=
SortedList
.
Make
(
struct
include
Custom
.
Dummy
include
Pat
end
)
module
PatList
=
SortedList
.
Make
(
struct
include
Custom
.
Dummy
include
Pat
end
)
module
TypesFv
=
Custom
.
Pair
(
Types
)(
IdSet
)
module
Req
=
PatList
.
MakeMap
(
TypesFv
)
(* Invariant for (p |-> (t,X)):
...
...
@@ -1641,12 +1637,12 @@ x=(1,2)
end
module
TargExpr
=
struct
type
'
a
t
=
'
a
source
IdMap
.
map
and
'
a
source
=
type
t
=
source
IdMap
.
map
and
source
=
|
SrcCapture
|
SrcCst
of
Types
.
const
|
SrcPair
of
'
a
source
*
'
a
source
|
SrcFetch
of
'
a
|
SrcPair
of
source
*
source
|
SrcFetch
of
int
let
capture
x
=
IdMap
.
singleton
x
SrcCapture
let
captures
xs
=
IdMap
.
constant
SrcCapture
xs
...
...
@@ -1655,33 +1651,33 @@ x=(1,2)
let
empty
=
IdMap
.
empty
let
merge
e1
e2
=
IdMap
.
merge
(
fun
s1
s2
->
SrcPair
(
s1
,
s2
))
e1
e2
let
rec
print_src
f
ppf
=
function
let
rec
print_src
ppf
=
function
|
SrcCapture
->
Format
.
fprintf
ppf
"#"
|
SrcCst
c
->
Types
.
Print
.
print_const
ppf
c
|
SrcPair
(
s1
,
s2
)
->
Format
.
fprintf
ppf
"(%a,%a)"
(
print_src
f
)
s1
(
print_src
f
)
s2
|
SrcFetch
x
->
f
ppf
x
Format
.
fprintf
ppf
"(%a,%a)"
print_src
s1
print_src
s2
|
SrcFetch
x
->
Format
.
fprintf
ppf
"$%i"
x
let
print
f
ppf
r
=
let
print
ppf
r
=
Format
.
fprintf
ppf
"{ "
;
List
.
iter
(
fun
(
x
,
s
)
->
Format
.
fprintf
ppf
"%a:=%a "
U
.
print
(
Id
.
value
x
)
(
print_src
f
)
s
)
(
IdMap
.
get
r
);
print_src
s
)
(
IdMap
.
get
r
);
Format
.
fprintf
ppf
"}"
;
end
end
module
Derivation
=
struct
type
(
'
a
,
'
b
)
t
=
type
t
=
|
TSucceed
|
TFail
|
TC
apt
of
'
a
TargExpr
.
t
*
(
'
a
,
'
b
)
t
|
T
Al
t
of
descr
*
Types
.
t
*
(
'
a
,
'
b
)
t
*
(
'
a
,
'
b
)
t
|
T
Conj
of
Types
.
t
*
fv
*
(
'
a
,
'
b
)
t
*
(
'
a
,
'
b
)
t
|
T
Other
of
descr
*
Types
.
t
*
fv
*
'
b
type
atoms
=
|
TConstr
of
Types
.
t
|
TC
onstr
of
Types
.
t
*
Types
.
t
|
T
Cap
t
of
TargExpr
.
t
*
t
|
T
Alt
of
descr
*
Types
.
t
*
t
*
t
|
T
Conj
of
Types
.
t
*
fv
*
t
*
t
|
TOther
of
descr
*
Types
.
t
*
fv
*
atoms
(*
| TTimes of descr * Types.t * fv * node * node *)
and
atoms
=
|
TTimes
of
node
*
node
|
TXml
of
node
*
node
|
TRecord
of
label
*
node
...
...
@@ -1707,40 +1703,54 @@ x=(1,2)
assumption is empty in this case). *)
|
r1
,
r2
->
TAlt
(
p
,
a1
,
r1
,
r2
)
let
rec
print
f
g
ppf
=
function
let
rec
print
ppf
=
function
|
TSucceed
->
Format
.
fprintf
ppf
"Succeed"
|
TFail
->
Format
.
fprintf
ppf
"Fail"
|
TConstr
(
t
,
s
)
->
Format
.
fprintf
ppf
"%a/%a"
Types
.
Print
.
print
t
Types
.
Print
.
print
s
|
TCapt
(
pr
,
r
)
->
Format
.
fprintf
ppf
"{%a}(%a)"
(
TargExpr
.
print
f
)
pr
(
print
f
g
)
r
Format
.
fprintf
ppf
"{%a}(%a)"
TargExpr
.
print
pr
print
r
|
TAlt
(
_
,_,
l
,
r
)
->
Format
.
fprintf
ppf
"(%a | %a)"
(
print
f
g
)
l
(
print
f
g
)
r
Format
.
fprintf
ppf
"(%a | %a)"
print
l
print
r
|
TConj
(
_
,_,
l
,
r
)
->
Format
.
fprintf
ppf
"(%a & %a)"
(
print
f
g
)
l
(
print
f
g
)
r
Format
.
fprintf
ppf
"(%a & %a)"
print
l
print
r
|
TOther
(
_
,
t
,
xs
,
x
)
->
Format
.
fprintf
ppf
"<t=%a;xs=%a;%a>"
Types
.
Print
.
print
t
Print
.
print_xs
xs
g
(
t
,
xs
,
x
)
print_atom
(
t
,
xs
,
x
)
and
print_atom
ppf
(
t
,
xs
,
d
)
=
match
d
with
|
TTimes
(
q1
,
q2
)
->
if
IdSet
.
is_empty
xs
then
Format
.
fprintf
ppf
"(%a,%a)"
Types
.
Print
.
print_node
q1
.
accept
Types
.
Print
.
print_node
q2
.
accept
else
Format
.
fprintf
ppf
"(%a,%a)"
Print
.
print
q1
.
descr
Print
.
print
q2
.
descr
|
TXml
_
->
Format
.
fprintf
ppf
"<_>_"
|
TRecord
_
->
Format
.
fprintf
ppf
"{_}"
let
get_result
=
function
|
TSucceed
->
Some
TargExpr
.
empty
|
TCapt
(
r
,
TSucceed
)
->
Some
r
|
TFail
->
None
|
r
->
Format
.
fprintf
Format
.
std_formatter
"ERR: %a@."
(
print
(
fun
ppf
_
->
()
)
(
fun
ppf
_
->
()
))
r
;
Format
.
fprintf
Format
.
std_formatter
"ERR: %a@."
print
r
;
assert
false
let
print_result
f
ppf
=
function
let
print_result
ppf
=
function
|
None
->
Format
.
fprintf
ppf
"Fail"
|
Some
r
->
TargExpr
.
print
f
ppf
r
|
Some
r
->
TargExpr
.
print
ppf
r
let
rec
mk
((
a
,
fv
,
d
)
as
p
)
=
let
oth
x
=
TOther
(
p
,
Types
.
any
,
fv
,
x
)
in
match
d
with
|
Constr
t
->
oth
(
TConstr
t
)
|
Constr
t
->
TConstr
(
t
,
Types
.
any
)
|
Cup
((
a1
,_,_
)
as
p1
,
p2
)
->
TAlt
(
p
,
a1
,
mk
p1
,
mk
p2
)
|
Cap
((
a1
,
fv1
,_
)
as
p1
,
p2
)
->
TConj
(
a1
,
fv1
,
mk
p1
,
mk
p2
)
|
Capture
x
->
TCapt
(
TargExpr
.
capture
x
,
TSucceed
)
...
...
@@ -1750,17 +1760,19 @@ x=(1,2)
|
Record
(
l
,
q
)
->
oth
(
TRecord
(
l
,
q
))
|
Dummy
->
assert
false
let
constr
a
t
=
if
Types
.
disjoint
a
t
then
TFail
else
if
Types
.
subtype
t
a
then
TSucceed
else
TConstr
(
a
,
t
)
let
factorize
((
a
,_,_
)
as
p
)
t
xs
f
=
if
Types
.
disjoint
a
t
then
TFail
else
let
vs
=
Approx
.
approx_var
p
t
xs
in
let
xs
=
IdSet
.
diff
xs
vs
in
let
pr
=
TargExpr
.
captures
vs
in
capt
pr
(
if
(
Types
.
subtype
t
a
)
&&
(
IdSet
.
is_empty
xs
)
then
TSucceed
else
f
xs
)
capt
pr
(
if
(
IdSet
.
is_empty
xs
)
then
constr
a
t
else
f
xs
)
let
rec
optimize
t
xs
=
function
|
TCapt
(
pr
,
p
)
->
...
...
@@ -1778,39 +1790,35 @@ x=(1,2)
conj
a1
fv1
(
optimize
t
(
IdSet
.
cap
xs
fv1
)
p1
)
(
optimize
(
Types
.
cap
t
a1
)
(
IdSet
.
diff
xs
fv1
)
p2
)
|
TConstr
(
a
,_
)
->
constr
a
t
|
TOther
(
p
,_,_,
x
)
->
factorize
p
t
xs
(
fun
xs
->
TOther
(
p
,
t
,
xs
,
x
))
|
TSucceed
->
if
Types
.
is_empty
t
then
TFail
else
TSucceed
|
TFail
->
TFail
let
rec
fold
f
accu
=
function
|
TCapt
(
_
,
p
)
->
fold
f
accu
p
|
TAlt
(
_
,_,
p1
,
p2
)
|
TConj
(
_
,_,
p1
,
p2
)
->
fold
f
(
fold
f
accu
p1
)
p2
|
TOther
(
_
,
t
,
xs
,
x
)
->
f
accu
t
xs
x
|
_
->
accu
let
collect_basic
accu
p
=
fold
(
fun
accu
s
xs
x
->
match
x
with
|
TConstr
t
->
(
t
,
s
)
::
accu
|
_
->
accu
)
accu
p
let
rec
collect_constr
accu
=
function
|
TCapt
(
_
,
p
)
->
collect_constr
accu
p
|
TAlt
(
_
,_,
p1
,
p2
)
|
TConj
(
_
,_,
p1
,
p2
)
->
collect_constr
(
collect_constr
accu
p1
)
p2
|
TConstr
(
t
,
s
)
->
(
t
,
s
)
::
accu
|
_
->
accu
let
collect_basic
=
collect_constr
let
mkopt
p
t
xs
=
optimize
t
xs
(
mk
p
)
let
demo
ppf
((
_
,
fv
,_
)
as
p
)
t
=
let
oth
ppf
(
t
,
xs
,
d
)
=
match
d
with
|
TConstr
t
->
Types
.
Print
.
print
ppf
t
|
TTimes
(
q1
,
q2
)
->
if
IdSet
.
is_empty
xs
then
Format
.
fprintf
ppf
"(%a,%a)"
Types
.
Print
.
print_node
q1
.
accept
Types
.
Print
.
print_node
q2
.
accept
else
Format
.
fprintf
ppf
"(%a,%a)"
Print
.
print
q1
.
descr
Print
.
print
q2
.
descr
|
TXml
_
->
Format
.
fprintf
ppf
"<_>_"
|
TRecord
_
->
Format
.
fprintf
ppf
"{_}"
in
let
p
=
mkopt
p
t
fv
in
print
oth
oth
ppf
p
;
print
ppf
p
;
let
qs
=
collect_basic
[]
p
in
let
part
=
Types
.
cond_partition
Types
.
non_constructed
qs
in
...
...
@@ -1821,9 +1829,9 @@ x=(1,2)
let
r
=
optimize
t
fv
p
in
Format
.
fprintf
ppf
"%a => %a@."
Types
.
Print
.
print
t
(
print
oth
oth
)
r
;
(*
Format.fprintf ppf " => %a@."
(
print_result
oth)
(get_result r)
*)
print
r
;
Format
.
fprintf
ppf
" => %a@."
print_result
(
get_result
r
)
)
part
end
...
...
@@ -1839,11 +1847,11 @@ x=(1,2)
type
t
=
{
outputs
:
output
array
;
rescode
:
rescode
;
reqs
:
(
(
unit
,
Derivation
.
atoms
)
Derivation
.
t
*
Types
.
t
*
fv
)
list
;
reqs
:
(
Derivation
.
t
*
Types
.
t
*
fv
)
list
;
assumpt
:
Types
.
t
;
}
type
basic_disp
=
(
Types
.
t
*
int
*
unit
TargExpr
.
source
array
)
list
type
basic_disp
=
(
Types
.
t
*
int
*
TargExpr
.
source
array
)
list
let
print
ppf
r
=
Format
.
fprintf
ppf
"Request@."
;
...
...
@@ -1856,10 +1864,8 @@ x=(1,2)
List
.
iter
(
fun
(
t
,
code
,
a
)
->
Format
.
fprintf
ppf
"%a => $%i("
Types
.
Print
.
print
t
code
;
Array
.
iter
(
fun
x
->
Format
.
fprintf
ppf
"%a;"
(
TargExpr
.
print_src
(
fun
ppf
_
->
assert
false
))
x
)
a
;
Array
.
iter
(
fun
x
->
Format
.
fprintf
ppf
"%a;"
TargExpr
.
print_src
x
)
a
;
Format
.
fprintf
ppf
")@."
;
)
l
...
...
@@ -1880,7 +1886,7 @@ x=(1,2)
if
Types
.
is_empty
t0
then
RFail
else
match
l
with
|
[]
->
incr
nb
;
codes
:=
(
t0
,
ar
,
List
.
rev
binds
)
::
!
codes
;
RCode
!
nb
|
((
a
,
fv
,_
)
as
p
,
(
t
,
xs
))
::
rem
->
|
((
a
,
fv
,_
)
,
(
t
,
xs
))
::
rem
->
let
(
alc
,
ar'
)
=
alloc
ar
fv
in
RSwitch
(
aux
(
Types
.
cap
t0
a
)
...
...
@@ -1926,7 +1932,7 @@ x=(1,2)
let
res
=
get_results
reqs
in
let
code
=
find_code
res
r
.
rescode
in
let
(
_
,
ar
,
fill
)
=
r
.
outputs
.
(
code
)
in
let
o
=
Array
.
make
ar
(
TargExpr
.
SrcFetch
()
)
in
let
o
=
Array
.
make
ar
(
TargExpr
.
SrcFetch
(
-
1
))
in
List
.
iter2
(
fun
res
fill
->
match
(
res
,
fill
)
with
|
Some
res
,
Some
fill
->
...
...
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