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
d7957a85
Commit
d7957a85
authored
Feb 12, 2014
by
Pietro Abate
Browse files
First attempt to implement a constructor for recursive types in types.ml
parent
18c814a6
Changes
4
Hide whitespace changes
Inline
Side-by-side
tests/libtest/tallyingTest.ml
View file @
d7957a85
...
...
@@ -71,7 +71,7 @@ let mk_union_res l1 l2 =
|
(
k
,
None
,
None
)
->
assert
false
|
(
k
,
Some
v
,
None
)
->
Some
v
|
(
k
,
None
,
Some
v
)
->
Some
v
|
((
_
,
v
)
,
Some
x
,
Some
y
)
when
Types
.
equ
al
x
y
->
Some
x
|
((
_
,
v
)
,
Some
x
,
Some
y
)
when
Types
.
equ
iv
x
y
->
Some
x
|
((
true
,
v
)
,
Some
x
,
Some
y
)
->
assert
false
|
((
false
,
v
)
,
Some
x
,
Some
y
)
->
assert
false
in
...
...
types/types.ml
View file @
d7957a85
...
...
@@ -520,58 +520,6 @@ let get_record r =
in
List
.
map
line
(
Rec
.
get
r
)
(*
let rec subst t (v,s) =
let module C ( X : BoolVar.S ) =
struct
let atom_aux ?f v (s,ss) =
let open X in function
|`Var z when (Var.equal (`Var z) v) -> ss
|`Var z -> vars (`Var z)
|`Atm bdd when X.T.is_empty bdd || X.T.is_full bdd -> atom (`Atm bdd)
|`Atm bdd ->
begin match f with
|None -> atom (`Atm bdd)
|Some f -> f bdd v (s,ss)
end
|_ -> assert false
let subst ?f v s bdd =
let open X in
let atom z = atom_aux ?f v s z in
compute ~empty ~full:`True ~cup ~cap ~diff ~atom bdd
end
in
let subpairs bdd v (s,_) =
List.fold_left (fun acc (left,rigth) ->
let deep_subst f l =
List.fold_left (fun acc (t1,t2) ->
let d1 = cons (subst (descr t1) (v,s)) in
let d2 = cons (subst (descr t2) (v,s)) in
BoolPair.cap acc (f(BoolPair.atom(`Atm (Pair.atom (d1,d2)))))
) BoolPair.full l
in
let neg_atm x = BoolPair.diff BoolPair.full x in
let pos_atm x = x in
let acc1 = BoolPair.cap (deep_subst pos_atm left) (deep_subst neg_atm rigth) in
BoolPair.cup acc acc1
) BoolPair.empty (Pair.get bdd)
in
{
atoms = (let module M = C(BoolAtoms) in M.subst) v (s,s.atoms) t.atoms;
ints = (let module M = C(BoolIntervals) in M.subst) v (s,s.ints) t.ints;
chars = (let module M = C(BoolChars) in M.subst) v (s,s.chars) t.chars;
times = (let module M = C(BoolPair) in M.subst) ~f:subpairs v (s,s.times) t.times;
xml = (let module M = C(BoolPair) in M.subst) ~f:subpairs v (s,s.xml) t.xml;
(* XXX record still not done . need to define ~f:subrecord *)
record= (let module M = C(BoolRec) in M.subst) v (s,s.record) t.record;
arrow = (let module M = C(BoolPair) in M.subst) ~f:subpairs v (s,s.arrow) t.arrow;
abstract = t.abstract;
absent= t.absent;
toplvars = { t.toplvars with s = Var.Set.remove v t.toplvars.s }
}
*)
(* substitute variables occurring in t accoding to the function subvar *)
let
rec
substfree_aux
subvar
t
=
let
module
C
(
X
:
BoolVar
.
S
)
=
...
...
@@ -1676,25 +1624,25 @@ struct
(* xml pairs *)
List
.
iter
(
fun
(
t1
,
t2
)
->
try
let
n
=
DescrPairMap
.
find
(
t1
,
t2
)
!
named_xml
in
add
(
Name
n
)
with
Not_found
->
let
tag
=
match
Atoms
.
print_tag
(
BoolAtoms
.
leafconj
t1
.
atoms
)
with
|
Some
a
when
is_empty
{
t1
with
atoms
=
BoolAtoms
.
empty
}
->
`Tag
a
|
_
->
`Type
(
prepare
t1
)
in
assert
(
equal
{
t2
with
times
=
empty
.
times
}
empty
);
List
.
iter
(
fun
(
ta
,
tb
)
->
add
(
Xml
(
tag
,
prepare
ta
,
prepare
tb
)))
(
Product
.
get
t2
);
try
let
n
=
DescrPairMap
.
find
(
t1
,
t2
)
!
named_xml
in
add
(
Name
n
)
with
Not_found
->
let
tag
=
match
Atoms
.
print_tag
(
BoolAtoms
.
leafconj
t1
.
atoms
)
with
|
Some
a
when
is_empty
{
t1
with
atoms
=
BoolAtoms
.
empty
}
->
`Tag
a
|
_
->
`Type
(
prepare
t1
)
in
assert
(
equal
{
t2
with
times
=
empty
.
times
}
empty
);
List
.
iter
(
fun
(
ta
,
tb
)
->
add
(
Xml
(
tag
,
prepare
ta
,
prepare
tb
)))
(
Product
.
get
t2
);
)
(
Product
.
get
~
kind
:
`XML
not_seq
);
(* records *)
List
.
iter
(
fun
(
r
,
some
,
none
)
->
let
r
=
LabelMap
.
map
(
fun
(
o
,
t
)
->
(
o
,
prepare
t
))
r
in
add
(
Record
(
r
,
some
,
none
))
List
.
iter
(
fun
(
r
,
some
,
none
)
->
let
r
=
LabelMap
.
map
(
fun
(
o
,
t
)
->
(
o
,
prepare
t
))
r
in
add
(
Record
(
r
,
some
,
none
))
)
(
Record
.
get
not_seq
);
(
match
Chars
.
is_char
(
BoolChars
.
leafconj
not_seq
.
chars
)
with
...
...
@@ -2132,6 +2080,8 @@ module Positive =
struct
type
rhs
=
[
|
`Type
of
descr
|
`Variable
of
Var
.
var
|
`Neg
of
v
|
`Cup
of
v
list
|
`Cap
of
v
list
|
`Arrow
of
v
*
v
...
...
@@ -2144,12 +2094,14 @@ struct
else
let
seen
=
v
::
seen
in
match
v
.
def
with
|
`Type
d
->
d
|
`Cup
vl
->
List
.
fold_left
(
fun
acc
v
->
cup
acc
(
make_descr
seen
v
))
empty
vl
|
`Cap
vl
->
List
.
fold_left
(
fun
acc
v
->
cap
acc
(
make_descr
seen
v
))
any
vl
|
`Times
(
v1
,
v2
)
->
times
(
make_node
v1
)
(
make_node
v2
)
|
`Arrow
(
v1
,
v2
)
->
arrow
(
make_node
v1
)
(
make_node
v2
)
|
`Xml
(
v1
,
v2
)
->
xml
(
make_node
v1
)
(
make_node
v2
)
|
`Type
d
->
d
|
`Variable
d
->
var
d
|
`Cup
vl
->
List
.
fold_left
(
fun
acc
v
->
cup
acc
(
make_descr
seen
v
))
empty
vl
|
`Cap
vl
->
List
.
fold_left
(
fun
acc
v
->
cap
acc
(
make_descr
seen
v
))
any
vl
|
`Times
(
v1
,
v2
)
->
times
(
make_node
v1
)
(
make_node
v2
)
|
`Arrow
(
v1
,
v2
)
->
arrow
(
make_node
v1
)
(
make_node
v2
)
|
`Xml
(
v1
,
v2
)
->
xml
(
make_node
v1
)
(
make_node
v2
)
|
`Neg
v
->
neg
(
make_descr
seen
v
)
and
make_node
v
=
match
v
.
node
with
...
...
@@ -2165,14 +2117,83 @@ struct
let
def
v
d
=
v
.
def
<-
d
let
cons
d
=
let
v
=
forward
()
in
def
v
d
;
v
let
ty
d
=
cons
(
`Type
d
)
let
var
d
=
cons
(
`Variable
d
)
let
neg
v
=
cons
(
`Neg
v
)
let
cup
vl
=
cons
(
`Cup
vl
)
let
cap
vl
=
cons
(
`Cap
vl
)
let
times
d
1
d
2
=
cons
(
`Times
(
d
1
,
d
2
))
let
arrow
d
1
d
2
=
cons
(
`Arrow
(
d
1
,
d
2
))
let
xml
d
1
d
2
=
cons
(
`Xml
(
d
1
,
d
2
))
let
times
v
1
v
2
=
cons
(
`Times
(
v
1
,
v
2
))
let
arrow
v
1
v
2
=
cons
(
`Arrow
(
v
1
,
v
2
))
let
xml
v
1
v
2
=
cons
(
`Xml
(
v
1
,
v
2
))
let
define
v1
v2
=
def
v1
(
`Cup
[
v2
])
let
rec
transform
t
=
let
aux_bdd
?
noderec
constr
(
p
,
n
)
=
let
aux
polarity
constr
l
=
cap
(
List
.
map
(
function
|
`Var
a
->
(
polarity
(
var
(
`Var
a
)))
|
`Atm
bdd
->
match
noderec
with
|
None
->
(
polarity
(
ty
(
constr
bdd
)))
|
Some
g
->
polarity
(
g
bdd
)
)
l
)
in
cap
[(
aux
(
fun
x
->
x
)
constr
p
);(
aux
neg
constr
n
)]
in
(* constr : times, arrow, xml *)
let
subpairs
(
constr
:
v
->
v
->
v
)
bdd
=
cup
(
List
.
map
(
fun
(
left
,
rigth
)
->
let
deep
polarity
l
=
cap
(
List
.
map
(
fun
(
t1
,
t2
)
->
let
d1
=
transform
(
descr
t1
)
in
let
d2
=
transform
(
descr
t2
)
in
polarity
(
constr
d1
d2
)
)
l
)
in
cap
[(
deep
(
fun
x
->
x
)
left
);(
deep
neg
rigth
)]
)
(
Pair
.
get
bdd
)
)
in
let
transform_aux
?
noderec
constr
l
=
cup
(
List
.
map
(
fun
(
p
,
n
)
->
(
aux_bdd
?
noderec
constr
(
p
,
n
)))
l
)
in
cup
[
transform_aux
atom
(
BoolAtoms
.
get
t
.
atoms
);
transform_aux
interval
(
BoolIntervals
.
get
t
.
ints
);
transform_aux
char
(
BoolChars
.
get
t
.
chars
);
transform_aux
~
noderec
:
(
subpairs
arrow
)
(
fun
p
->
{
empty
with
arrow
=
BoolPair
.
atom
(
`Atm
p
)
})
(
BoolPair
.
get
t
.
arrow
);
transform_aux
~
noderec
:
(
subpairs
xml
)
(
fun
p
->
{
empty
with
xml
=
BoolPair
.
atom
(
`Atm
p
)
})
(
BoolPair
.
get
t
.
xml
);
transform_aux
~
noderec
:
(
subpairs
times
)
(
fun
p
->
{
empty
with
times
=
BoolPair
.
atom
(
`Atm
p
)
})
(
BoolPair
.
get
t
.
times
);
]
let
solve
v
=
internalize
(
make_node
v
)
(* returns a recursive type where all occurrences of alpha n t
* are substituted with a recursive variable X *)
let
substitute
t
alpha
=
let
rec
aux_subst
v
(
alpha
,
x
)
=
match
v
.
def
with
|
`Type
d
->
ty
d
|
`Variable
d
when
Var
.
equal
alpha
d
->
x
|
`Variable
d
->
var
d
|
`Cup
vl
->
cup
(
List
.
map
(
fun
v
->
aux_subst
v
(
alpha
,
x
))
vl
)
|
`Cap
vl
->
cap
(
List
.
map
(
fun
v
->
aux_subst
v
(
alpha
,
x
))
vl
)
|
`Times
(
v1
,
v2
)
->
times
(
aux_subst
v1
(
alpha
,
x
))
(
aux_subst
v2
(
alpha
,
x
))
|
`Arrow
(
v1
,
v2
)
->
arrow
(
aux_subst
v1
(
alpha
,
x
))
(
aux_subst
v2
(
alpha
,
x
))
|
`Xml
(
v1
,
v2
)
->
xml
(
aux_subst
v1
(
alpha
,
x
))
(
aux_subst
v2
(
alpha
,
x
))
|
`Neg
v
->
neg
(
aux_subst
v
(
alpha
,
x
))
in
let
x
=
forward
()
in
let
t1
=
solve
(
aux_subst
(
transform
t
)
(
alpha
,
x
))
in
t1
.
Node
.
descr
<-
(
descr
t1
);
descr
t1
end
let
memo_normalize
=
ref
DescrMap
.
empty
...
...
@@ -2761,6 +2782,8 @@ module Tallying = struct
let
e1
=
CS
.
E
.
remove
alpha
e
in
(* remove from E \ { (alpha,t) } every occurrences of alpha
* by mu X . (t{X/alpha}) with X fresh *)
(* Positive.transform : Descr.s -> Positive.t
* and then Positive.solve on the result ... *)
let
es
=
CS
.
E
.
fold
(
fun
beta
s
acc
->
CS
.
E
.
add
beta
(
subst
s
(
alpha
,
t
))
acc
)
e1
CS
.
E
.
empty
in
aux
((
CS
.
E
.
add
alpha
t
sol
)
,
(
CS
.
E
.
add
alpha
(
subst
t
(
alpha
,
t
))
acc
))
es
in
...
...
types/types.mli
View file @
d7957a85
...
...
@@ -156,6 +156,8 @@ sig
val
times
:
v
->
v
->
v
val
xml
:
v
->
v
->
v
val
transform
:
t
->
v
val
substitute
:
t
->
Var
.
var
->
t
val
solve
:
v
->
Node
.
t
end
...
...
typing/typepat.ml
View file @
d7957a85
...
...
@@ -287,7 +287,6 @@ let deferr s = raise (Patterns.Error s)
(* From the intermediate representation to the internal one *)
let
rec
typ
n
=
let
n
=
repr
n
in
match
n
.
t
with
...
...
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