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
3ba84a1e
Commit
3ba84a1e
authored
Jul 10, 2007
by
Pietro Abate
Browse files
[r2004-12-23 13:31:47 by afrisch] Compil
Original author: afrisch Date: 2004-12-23 13:31:48+00:00
parent
84a60742
Changes
7
Hide whitespace changes
Inline
Side-by-side
driver/cduce.ml
View file @
3ba84a1e
...
...
@@ -194,7 +194,8 @@ let debug ppf tenv cenv = function
Format
.
fprintf
ppf
"[DEBUG:compile]@."
;
let
t
=
Typer
.
typ
tenv
t
and
pl
=
List
.
map
(
Typer
.
pat
tenv
)
pl
in
Patterns
.
Compile
.
debug_compile
ppf
t
pl
(* Patterns.Compile.debug_compile ppf t pl *)
Patterns
.
demo_compile
ppf
(
Types
.
descr
t
)
(
List
.
map
Patterns
.
descr
pl
)
|
`Explain
(
t
,
e
)
->
Format
.
fprintf
ppf
"[DEBUG:explain]@."
;
let
t
=
Typer
.
typ
tenv
t
in
...
...
types/patterns.ml
View file @
3ba84a1e
...
...
@@ -236,7 +236,7 @@ end
module
Pat
=
struct
type
t
=
descr
let
rec
compare
(
t1
,
fv1
,
d1
)
(
t2
,
fv2
,
d2
)
=
if
d1
==
d2
then
0
else
let
rec
compare
(
_
,_,
d1
)
(
_
,_
,
d2
)
=
if
d1
==
d2
then
0
else
match
(
d1
,
d2
)
with
|
Constr
t1
,
Constr
t2
->
Types
.
compare
t1
t2
|
Constr
_
,
_
->
-
1
|
_
,
Constr
_
->
1
...
...
@@ -268,6 +268,19 @@ module Pat = struct
|
Constant
_
,
_
->
-
1
|
_
,
Constant
_
->
1
|
Dummy
,
Dummy
->
assert
false
let
equal
p1
p2
=
compare
p1
p2
==
0
let
rec
hash
(
_
,_,
d
)
=
match
d
with
|
Constr
t
->
1
+
17
*
(
Types
.
hash
t
)
|
Cup
(
p1
,
p2
)
->
2
+
17
*
(
hash
p1
)
+
257
*
(
hash
p2
)
|
Cap
(
p1
,
p2
)
->
3
+
17
*
(
hash
p1
)
+
257
*
(
hash
p2
)
|
Times
(
q1
,
q2
)
->
4
+
17
*
q1
.
id
+
257
*
q2
.
id
|
Xml
(
q1
,
q2
)
->
5
+
17
*
q1
.
id
+
257
*
q2
.
id
|
Record
(
l
,
q
)
->
6
+
17
*
(
LabelPool
.
hash
l
)
+
257
*
q
.
id
|
Capture
x
->
7
+
(
Id
.
hash
x
)
|
Constant
(
x
,
c
)
->
8
+
17
*
(
Id
.
hash
x
)
+
257
*
(
Types
.
Const
.
hash
c
)
|
Dummy
->
assert
false
end
module
Print
=
struct
...
...
@@ -1556,11 +1569,20 @@ module Compile2 = struct
include
Pat
end
)
module
TypesFv
=
Custom
.
Pair
(
Types
)(
IdSet
)
module
Req
uest
=
PatList
.
MakeMap
(
TypesFv
)
module
Req
=
PatList
.
MakeMap
(
TypesFv
)
(* Invariant for (p |-> (t,X)):
i) t != Empty
ii) X \subset fv(p) *)
let
empty_reqs
=
PatList
.
Map
.
empty
let
merge_reqs
=
PatList
.
Map
.
merge
(
fun
(
t1
,
xs1
)
(
t2
,
xs2
)
->
Types
.
cup
t1
t2
,
IdSet
.
cup
xs1
xs2
)
let
add_req
reqs
p
t
xs
=
merge_reqs
reqs
(
PatList
.
Map
.
singleton
p
(
t
,
xs
))
module
NodeSet
=
Set
.
Make
(
Node
)
let
pi1
t
=
Types
.
Product
.
pi1
(
Types
.
Product
.
get
t
)
...
...
@@ -1658,6 +1680,12 @@ x=(1,2)
|
TConj
of
Types
.
t
*
fv
*
(
'
a
,
'
b
)
t
*
(
'
a
,
'
b
)
t
|
TOther
of
descr
*
Types
.
t
*
fv
*
'
b
type
atoms
=
|
TConstr
of
Types
.
t
|
TTimes
of
node
*
node
|
TXml
of
node
*
node
|
TRecord
of
label
*
node
let
capt
pr
p
=
if
IdMap
.
is_empty
pr
then
p
else
match
p
with
|
TCapt
(
pr2
,
p
)
->
TCapt
(
TargExpr
.
merge
pr
pr2
,
p
)
...
...
@@ -1680,11 +1708,6 @@ x=(1,2)
|
r1
,
r2
->
TAlt
(
p
,
a1
,
r1
,
r2
)
let
get_result
=
function
|
TCapt
(
r
,
TSucceed
)
->
Some
r
|
TFail
->
None
|
_
->
assert
false
let
rec
print
f
g
ppf
=
function
|
TSucceed
->
Format
.
fprintf
ppf
"Succeed"
|
TFail
->
Format
.
fprintf
ppf
"Fail"
...
...
@@ -1700,18 +1723,31 @@ x=(1,2)
Print
.
print_xs
xs
g
(
t
,
xs
,
x
)
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
;
assert
false
let
print_result
f
ppf
=
function
|
None
->
Format
.
fprintf
ppf
"Fail"
|
Some
r
->
TargExpr
.
print
f
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
(
`
Constr
t
)
|
Constr
t
->
oth
(
T
Constr
t
)
|
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
)
|
Constant
(
x
,
c
)
->
TCapt
(
TargExpr
.
cst
x
c
,
TSucceed
)
|
Times
(
q1
,
q2
)
->
oth
(
`
Times
(
q1
,
q2
))
|
Xml
(
q1
,
q2
)
->
oth
(
`
Xml
(
q1
,
q2
))
|
Record
(
l
,
q
)
->
oth
(
`
Record
(
l
,
q
))
|
Times
(
q1
,
q2
)
->
oth
(
T
Times
(
q1
,
q2
))
|
Xml
(
q1
,
q2
)
->
oth
(
T
Xml
(
q1
,
q2
))
|
Record
(
l
,
q
)
->
oth
(
T
Record
(
l
,
q
))
|
Dummy
->
assert
false
let
factorize
((
a
,_,_
)
as
p
)
t
xs
f
=
...
...
@@ -1744,24 +1780,174 @@ x=(1,2)
(
optimize
(
Types
.
cap
t
a1
)
(
IdSet
.
diff
xs
fv1
)
p2
)
|
TOther
(
p
,_,_,
x
)
->
factorize
p
t
xs
(
fun
xs
->
TOther
(
p
,
t
,
xs
,
x
))
|
(
TFail
|
TSucceed
)
as
p
->
p
|
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
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
|
`
Constr
t
->
Types
.
Print
.
print
ppf
t
|
`
Times
(
q1
,
q2
)
->
|
T
Constr
t
->
Types
.
Print
.
print
ppf
t
|
T
Times
(
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
|
`Xml
_
->
Format
.
fprintf
ppf
"<_>_"
|
`Record
_
->
Format
.
fprintf
ppf
"{_}"
in
print
oth
oth
ppf
(
optimize
t
fv
(
mk
p
))
|
TXml
_
->
Format
.
fprintf
ppf
"<_>_"
|
TRecord
_
->
Format
.
fprintf
ppf
"{_}"
in
let
p
=
mkopt
p
t
fv
in
print
oth
oth
ppf
p
;
let
qs
=
collect_basic
[]
p
in
let
part
=
Types
.
cond_partition
Types
.
non_constructed
qs
in
let
t
=
Types
.
cap
t
Types
.
non_constructed
in
Format
.
fprintf
ppf
"@.Partition:@."
;
List
.
iter
(
fun
t'
->
let
t
=
Types
.
cap
t
t'
in
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) *)
)
part
end
module
Request
=
struct
type
output
=
Types
.
t
*
int
*
int
id_map
option
list
type
rescode
=
|
RFail
|
RCode
of
int
|
RSwitch
of
rescode
*
rescode
type
t
=
{
outputs
:
output
array
;
rescode
:
rescode
;
reqs
:
((
unit
,
Derivation
.
atoms
)
Derivation
.
t
*
Types
.
t
*
fv
)
list
;
assumpt
:
Types
.
t
;
}
type
basic_disp
=
(
Types
.
t
*
int
*
unit
TargExpr
.
source
array
)
list
let
print
ppf
r
=
Format
.
fprintf
ppf
"Request@."
;
Array
.
iteri
(
fun
i
(
t
,
ar
,_
)
->
Format
.
fprintf
ppf
"[%i] %a@."
i
Types
.
Print
.
print
t
)
r
.
outputs
let
print_basic_disp
ppf
l
=
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
;
Format
.
fprintf
ppf
")@."
;
)
l
let
rec
find_code
bl
rc
=
match
(
bl
,
rc
)
with
|
Some
_
::
bl
,
RSwitch
(
rc
,_
)
|
None
::
bl
,
RSwitch
(
_
,
rc
)
->
find_code
bl
rc
|
([]
,
RCode
i
)
->
i
|
_
->
assert
false
let
alloc
pos
fv
=
let
i
=
ref
(
pos
-
1
)
in
let
r
=
IdMap
.
map_from_slist
(
fun
x
->
incr
i
;
!
i
)
fv
in
(
r
,!
i
+
1
)
let
mk
reqs
t0
=
let
nb
=
ref
(
-
1
)
in
let
codes
=
ref
[]
in
let
rec
aux
t0
ar
binds
l
=
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
->
let
(
alc
,
ar'
)
=
alloc
ar
fv
in
RSwitch
(
aux
(
Types
.
cap
t0
a
)
ar'
(
Some
alc
::
binds
)
rem
,
aux
(
Types
.
diff
t0
a
)
ar
(
None
::
binds
)
rem
)
in
let
reqs
=
PatList
.
Map
.
get
reqs
in
(* let t0 =
List.fold_left
(fun accu (_,(t,_)) -> Types.cup accu t) Types.empty
reqs in *)
let
rc
=
aux
t0
0
[]
reqs
in
let
os
=
Array
.
of_list
(
List
.
rev
!
codes
)
in
let
ders
=
List
.
map
(
fun
(
p
,
(
t
,
xs
))
->
(
Derivation
.
mkopt
p
t
xs
,
t
,
xs
))
reqs
in
{
outputs
=
os
;
rescode
=
rc
;
reqs
=
ders
;
assumpt
=
t0
}
let
opt_all
t0
=
List
.
map
(
fun
(
p
,
t
,
xs
)
->
if
Types
.
subtype
t
t0
then
(
p
,
t
,
xs
)
else
let
t
=
Types
.
cap
t
t0
in
(
Derivation
.
optimize
t
xs
p
,
t
,
xs
))
let
get_results
reqs
=
List
.
map
(
fun
(
p
,_,_
)
->
Derivation
.
get_result
p
)
reqs
let
basic_disp
r
:
basic_disp
=
let
t0
=
Types
.
cap
r
.
assumpt
Types
.
non_constructed
in
let
reqs
=
opt_all
t0
r
.
reqs
in
let
qs
=
List
.
fold_left
(
fun
accu
(
p
,_,_
)
->
Derivation
.
collect_basic
accu
p
)
[]
reqs
in
let
part
=
Types
.
cond_partition
t0
qs
in
List
.
map
(
fun
t
->
let
reqs
=
opt_all
t
reqs
in
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
List
.
iter2
(
fun
res
fill
->
match
(
res
,
fill
)
with
|
Some
res
,
Some
fill
->
IdMap
.
iteri
(
fun
x
i
->
o
.
(
i
)
<-
IdMap
.
assoc
x
res
)
fill
|
None
,
None
->
()
|
_
->
assert
false
)
res
fill
;
(
t
,
code
,
o
)
)
part
let
demo
ppf
t
pl
=
let
(
reqs
,_
)
=
List
.
fold_left
(
fun
(
reqs
,
t
)
((
a
,
fv
,_
)
as
p
)
->
(
add_req
reqs
p
t
fv
,
Types
.
diff
t
a
))
(
empty_reqs
,
t
)
pl
in
let
r
=
mk
reqs
t
in
print
ppf
r
;
print_basic_disp
ppf
(
basic_disp
r
)
end
end
let
approx
((
_
,
fv
,_
)
as
p
)
t
=
...
...
@@ -1771,3 +1957,4 @@ let approx ((_,fv,_) as p) t =
let
demo
=
Compile2
.
Derivation
.
demo
let
demo_compile
=
Compile2
.
Request
.
demo
types/patterns.mli
View file @
3ba84a1e
...
...
@@ -88,3 +88,4 @@ val approx :
id
list
*
(
id
*
Types
.
Const
.
t
)
list
val
demo
:
Format
.
formatter
->
descr
->
Types
.
descr
->
unit
val
demo_compile
:
Format
.
formatter
->
Types
.
descr
->
descr
list
->
unit
types/sortedList.ml
View file @
3ba84a1e
...
...
@@ -162,6 +162,10 @@ module Map = struct
|
(
_
,
y
)
::
l
->
f
y
;
iter
f
l
|
[]
->
()
let
rec
iteri
f
=
function
|
(
x
,
y
)
::
l
->
f
x
y
;
iteri
f
l
|
[]
->
()
let
rec
filter
f
=
function
|
((
x
,
y
)
as
c
)
::
l
->
if
f
x
y
then
c
::
(
filter
f
l
)
else
filter
f
l
|
[]
->
[]
...
...
types/sortedList.mli
View file @
3ba84a1e
...
...
@@ -35,6 +35,7 @@ sig
val
restrict
:
'
a
map
->
t
->
'
a
map
val
empty
:
'
a
map
val
iter
:
(
'
a
->
unit
)
->
'
a
map
->
unit
val
iteri
:
(
X
.
t
->
'
a
->
unit
)
->
'
a
map
->
unit
val
filter
:
(
X
.
t
->
'
a
->
bool
)
->
'
a
map
->
'
a
map
val
is_empty
:
'
a
map
->
bool
val
singleton
:
X
.
t
->
'
a
->
'
a
map
...
...
types/types.ml
View file @
3ba84a1e
...
...
@@ -1869,3 +1869,18 @@ let empty_closed_record = rec_of_list ~opened:false []
let
empty_opened_record
=
rec_of_list
~
opened
:
true
[]
(* </helpers> *)
let
cond_partition
univ
qs
=
let
rec
add
accu
(
t
,
s
)
=
let
t
=
if
subtype
t
s
then
t
else
cap
t
s
in
if
(
subtype
s
t
)
||
(
is_empty
t
)
then
accu
else
let
rec
aux
accu
u
=
let
c
=
cap
u
t
in
if
(
is_empty
c
)
||
(
subtype
(
cap
u
s
)
t
)
then
u
::
accu
else
c
::
(
diff
u
t
)
::
accu
in
List
.
fold_left
aux
[]
accu
in
List
.
fold_left
add
[
univ
]
qs
types/types.mli
View file @
3ba84a1e
...
...
@@ -249,6 +249,15 @@ val non_empty: t -> bool
val
subtype
:
t
->
t
->
bool
val
disjoint
:
t
->
t
->
bool
(** Tools for compilation of PM **)
val
cond_partition
:
t
->
(
t
*
t
)
list
->
t
list
(* The second argument is a list of pair of types (ti,si)
interpreted as the question "member of ti under the assumption si".
The result is a partition of the first argument which is precise enough
to answer all the questions. *)
module
Print
:
sig
val
register_global
:
U
.
t
->
t
->
unit
...
...
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