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
1a96118d
Commit
1a96118d
authored
Oct 05, 2007
by
Pietro Abate
Browse files
[r2002-11-20 17:50:57 by cvscast] Empty log message
Original author: cvscast Date: 2002-11-20 17:50:57+00:00
parent
0746e040
Changes
1
Hide whitespace changes
Inline
Side-by-side
types/patterns.ml
View file @
1a96118d
...
...
@@ -181,84 +181,185 @@ struct
type
disp
=
{
did
:
int
;
result
s
:
(
int
*
(
capture
,
int
)
SortedMap
.
t
option
array
*
bool
array
)
array
nb_code
s
:
int
;
results
:
res
;
}
and
bind
=
(
capture
,
int
)
SortedMap
.
t
and
res
=
[
`Return
of
int
|
`Fail
|
`Branch
of
(
bind
*
res
*
res
)
]
type
p
=
[
`Pat
of
node
|
`Typ
of
Types
.
descr
]
module
DispMap
=
Map
.
Make
(
struct
type
t
=
(
node
*
Types
.
descr
)
array
*
(
Types
.
descr
*
Types
.
descr
)
array
type
t
=
Types
.
descr
*
(
p
,
Types
.
descr
)
SortedMap
.
t
let
compare
=
compare
end
)
let
dispatchers
=
ref
DispMap
.
empty
let
nb_disp
=
ref
0
let
rec
make_res
codes
pos
t
l
=
if
Types
.
is_empty
t
then
`Fail
else
match
l
with
|
[]
->
incr
codes
;
`Return
(
!
codes
-
1
)
|
(
p
,
restr
)
::
rem
->
let
(
pos
,
bind
,
a
)
=
match
p
with
|
`Pat
p
->
let
pos
=
ref
pos
in
let
bind
=
List
.
map
(
fun
v
->
incr
pos
;
(
v
,!
pos
-
1
))
(
fv
p
)
in
(
!
pos
,
bind
,
Types
.
descr
(
accept
p
))
|
`Typ
a
->
(
pos
,
[]
,
a
)
in
let
oth
=
Types
.
diff
t
restr
in
(* assert (Types.subtype restr t);*)
let
yes
=
make_res
codes
pos
(
Types
.
cup
(
Types
.
cap
t
a
)
oth
)
rem
and
no
=
make_res
codes
pos
(
Types
.
cup
(
Types
.
diff
t
a
)
oth
)
rem
in
`Branch
(
bind
,
yes
,
no
)
let
dispatcher
pats
typs
:
disp
=
try
DispMap
.
find
(
pats
,
typs
)
!
dispatchers
let
make_
dispatcher
t
pats
:
disp
=
try
DispMap
.
find
(
t
,
pats
)
!
dispatchers
with
Not_found
->
incr
nb_disp
;
let
d
=
{
did
=
!
nb_disp
;
results
=
[
|
|
]
}
in
dispatchers
:=
DispMap
.
add
(
pats
,
typs
)
d
!
dispatchers
;
let
nbc
=
ref
0
in
let
res
=
make_res
nbc
0
t
pats
in
let
d
=
{
did
=
!
nb_disp
;
results
=
res
;
nb_codes
=
!
nbc
}
in
dispatchers
:=
DispMap
.
add
(
t
,
pats
)
d
!
dispatchers
;
d
let
dispatcher
t
(
args
:
(
p
*
Types
.
descr
*
bind
option
ref
)
list
)
f
=
let
args
=
List
.
map
(
fun
(
p
,
restr
,
flag
)
->
(
p
,
(
restr
,
[
flag
])))
args
in
let
args
=
SortedMap
.
from_list
(
fun
(
r1
,
f1
)
(
r2
,
f2
)
->
Types
.
cup
r1
r2
,
f1
@
f2
)
args
in
let
pats
=
List
.
map
(
fun
(
p
,
(
r
,_
))
->
(
p
,
r
))
args
in
let
d
=
make_dispatcher
t
pats
in
let
res
=
Array
.
create
d
.
nb_codes
(
Obj
.
magic
0
)
in
let
rec
aux
=
function
|
(
`Fail
,_
)
->
()
|
(
`Return
c
,
[]
)
->
res
.
(
c
)
<-
f
()
|
(
`Branch
(
bind
,
yes
,
no
)
,
(
_
,
(
_
,
fl
))
::
rem
)
->
List
.
iter
(
fun
r
->
r
:=
Some
bind
)
fl
;
aux
(
yes
,
rem
);
List
.
iter
(
fun
r
->
r
:=
None
)
fl
;
aux
(
no
,
rem
)
|
_
->
assert
false
in
aux
(
d
.
results
,
args
);
(
d
,
res
)
let
sort_list
l
=
Array
.
of_list
(
SortedList
.
from_list
l
)
type
'
a
pat
=
|
One
|
Zero
|
Capt
of
capture
|
Const
of
capture
*
Types
.
const
|
Alt
of
'
a
pat
*
'
a
pat
|
And
of
'
a
pat
*
'
a
pat
|
Type
of
Types
.
descr
*
Types
.
descr
|
Atom
of
Types
.
descr
*
'
a
let
rec
print
f
ppf
=
function
|
One
->
Format
.
fprintf
ppf
"One"
|
Zero
->
Format
.
fprintf
ppf
"Zero"
|
Capt
x
->
Format
.
fprintf
ppf
"%s"
x
|
Const
(
x
,
c
)
->
Format
.
fprintf
ppf
"(%s := %a)"
x
Types
.
Print
.
print_const
c
|
Alt
(
p1
,
p2
)
->
Format
.
fprintf
ppf
"(%a | %a)"
(
print
f
)
p1
(
print
f
)
p2
|
And
(
p1
,
p2
)
->
Format
.
fprintf
ppf
"(%a & %a)"
(
print
f
)
p1
(
print
f
)
p2
|
Atom
(
d
,
a
)
->
Format
.
fprintf
ppf
"[%a]%a"
Types
.
Print
.
print_descr
d
f
a
|
Type
(
d
,
a
)
->
Format
.
fprintf
ppf
"[%a]%a"
Types
.
Print
.
print_descr
d
Types
.
Print
.
print_descr
a
let
alt
=
function
|
(
Zero
,
p
)
|
(
p
,
Zero
)
->
p
|
(
p1
,
p2
)
->
Alt
(
p1
,
p2
)
let
and_
=
function
|
(
Zero
,_
)
|
(
_
,
Zero
)
->
Zero
|
(
One
,
p
)
|
(
p
,
One
)
->
p
|
(
p1
,
p2
)
->
And
(
p1
,
p2
)
let
atom
s
a
p
=
if
Types
.
is_empty
(
Types
.
cap
s
a
)
then
Zero
else
Atom
(
s
,
p
)
let
rec
get
f
(
a
,_,
d
)
s
=
if
Types
.
is_empty
(
Types
.
cap
s
a
)
then
Zero
else
match
d
with
|
Constr
t
->
if
Types
.
subtype
s
t
then
One
else
Type
(
s
,
Types
.
cap
s
t
)
|
Cup
((
a1
,_,_
)
as
d1
,
d2
)
->
let
p1
=
get
f
d1
s
in
let
p2
=
get
f
d2
(
Types
.
diff
s
a1
)
in
alt
(
p1
,
p2
)
|
Cap
((
a1
,_,_
)
as
d1
,
d2
)
->
(* could swap the two to optimize ? ... *)
let
p1
=
get
f
d1
s
in
let
p2
=
get
f
d2
(
Types
.
cap
s
a1
)
in
and_
(
p1
,
p2
)
|
Capture
x
->
Capt
x
|
Constant
(
x
,
c
)
->
Const
(
x
,
c
)
|
d
->
(
match
f
d
with
None
->
Zero
|
Some
x
->
Atom
(
s
,
x
))
type
'
a
pat
=
|
One
|
Zero
|
Capt
of
capture
|
Const
of
capture
*
Types
.
const
|
Alt
of
'
a
pat
*
'
a
pat
|
And
of
'
a
pat
*
'
a
pat
|
Atom
of
'
a
let
rec
print
f
ppf
=
function
|
One
->
Format
.
fprintf
ppf
"One"
|
Zero
->
Format
.
fprintf
ppf
"Zero"
|
Capt
x
->
Format
.
fprintf
ppf
"%s"
x
|
Const
(
x
,
c
)
->
Format
.
fprintf
ppf
"(%s:=%a)"
x
Types
.
Print
.
print_const
c
|
Alt
(
p1
,
p2
)
->
Format
.
fprintf
ppf
"(%a | %a)"
(
print
f
)
p1
(
print
f
)
p2
|
And
(
p1
,
p2
)
->
Format
.
fprintf
ppf
"(%a & %a)"
(
print
f
)
p1
(
print
f
)
p2
|
Atom
a
->
Format
.
fprintf
ppf
"%a"
f
a
let
alt
=
function
|
(
Zero
,
p
)
|
(
p
,
Zero
)
->
p
|
(
p1
,
p2
)
->
Alt
(
p1
,
p2
)
let
and_
=
function
|
(
Zero
,_
)
|
(
_
,
Zero
)
->
Zero
|
(
One
,
p
)
|
(
p
,
One
)
->
p
|
(
p1
,
p2
)
->
And
(
p1
,
p2
)
let
atom
s
a
p
=
if
Types
.
is_empty
(
Types
.
cap
s
a
)
then
Zero
else
Atom
(
s
,
p
)
let
rec
map
f
=
function
|
One
->
One
|
Zero
->
Zero
|
Capt
x
->
Capt
x
|
Const
(
x
,
c
)
->
Const
(
x
,
c
)
|
Alt
(
p1
,
p2
)
->
Alt
(
map
f
p1
,
map
f
p2
)
|
And
(
p1
,
p2
)
->
And
(
map
f
p1
,
map
f
p2
)
|
Atom
a
->
Atom
(
f
a
)
let
rec
get
f
(
a
,_,
d
)
s
=
if
Types
.
is_empty
(
Types
.
cap
s
a
)
then
Zero
else
match
d
with
|
Constr
t
when
Types
.
subtype
s
t
->
One
|
Cup
((
a1
,_,_
)
as
d1
,
d2
)
->
let
p1
=
get
f
d1
s
in
let
p2
=
get
f
d2
(
Types
.
diff
s
a1
)
in
alt
(
p1
,
p2
)
|
Cap
((
a1
,_,_
)
as
d1
,
d2
)
->
(* could swap the two to optimize ? ... *)
let
p1
=
get
f
d1
s
in
let
p2
=
get
f
d2
(
Types
.
cap
s
a1
)
in
and_
(
p1
,
p2
)
|
Capture
x
->
Capt
x
|
Constant
(
x
,
c
)
->
Const
(
x
,
c
)
|
d
->
f
d
s
let
prepare_prod
=
get
(
fun
d
r
->
match
d
with
|
Times
(
n1
,
n2
)
->
let
r
=
Types
.
Product
.
normal
r
in
Atom
(
`Pat
(
n1
,
n2
,
r
))
|
Constr
t
->
Atom
(
`Typ
(
t
,
r
))
|
_
->
Zero
)
let
dispatch_record
t
pats
=
let
pats
=
List
.
map
(
fun
(
p
,
restr
)
->
match
p
with
|
`Pat
p
->
prepare_prod
(
descr
p
)
restr
|
`Typ
s
->
Atom
(
`Typ
(
s
,
restr
))
(* TODO: special case here ... restr<=t...*)
)
pats
in
(* Make dispatcher on first component *)
let
lefts
=
ref
[]
in
let
pats
=
List
.
map
(
map
(
function
|
`Pat
(
n1
,
n2
,
r
)
->
let
pat
=
List
.
map
(
fun
(
r1
,
r2
)
->
let
fl
=
ref
None
in
lefts
:=
(
`Pat
n1
,
r1
,
fl
)
::
!
lefts
;
(
fl
,
n2
,
r2
)
)
r
in
`Pat
pat
|
`Typ
(
s
,
r
)
->
(*...*)
assert
false
))
pats
in
let
(
disp1
,
f1
)
=
dispatcher
(
Types
.
Product
.
pi1
(
Types
.
Product
.
get
t
))
!
lefts
(
fun
()
->
0
)
in
()
(*
let rec collect typ f (a,_,d) s =
if Types.is_empty (Types.cap s a) then () else
match d with
...
...
@@ -307,6 +408,7 @@ let demo ppf p t =
to_print := n1 :: !to_print
| _ -> ()) p t
*)
end
let
demo
ppf
p
t
=
...
...
@@ -314,8 +416,11 @@ let demo ppf p t =
Compiler.demo ppf p t;
dump_print ppf
*)
(*
Format.fprintf ppf "PROD:%a@\n" Compiler.print_prod (Compiler.get_prod p (Types.cap Types.Product.any t));
Format.fprintf ppf "REC :%a@\n" Compiler.print_record (Compiler.get_record p (Types.cap Types.Record.any t))
*)
()
let
rec
restrict
((
a
,
fv
,
d
)
as
p
)
t
=
...
...
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