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
f5cbbde4
Commit
f5cbbde4
authored
Oct 05, 2007
by
Pietro Abate
Browse files
[r2003-03-06 21:51:57 by cvscast] Empty log message
Original author: cvscast Date: 2003-03-06 21:51:57+00:00
parent
1f0b52f8
Changes
3
Hide whitespace changes
Inline
Side-by-side
types/atoms.ml
View file @
f5cbbde4
...
...
@@ -57,4 +57,4 @@ let print any f = function
List
.
iter
(
fun
x
->
Format
.
fprintf
ppf
" |@ %a"
f
x
)
t
;
Format
.
fprintf
ppf
")@]"
]
types/recursive_noshare.ml
View file @
f5cbbde4
...
...
@@ -3,19 +3,9 @@ open Recursive
module
Make
(
X
:
S
)
=
struct
type
state
=
Undefined
|
Defined
type
node
=
{
id
:
int
;
mutable
descr
:
descr
;
mutable
recurs
:
int
;
(* -1 means "not yet computed"
-2 means "no"
-3 means "marked"
id>=0 means "yes"
*)
mutable
marked
:
int
;
}
and
descr
=
node
X
.
t
...
...
@@ -28,9 +18,6 @@ struct
{
id
=
!
counter
;
descr
=
Obj
.
magic
0
;
recurs
=
-
1
;
marked
=
-
1
;
}
let
equal
x
y
=
x
.
id
=
y
.
id
...
...
@@ -54,38 +41,7 @@ struct
with
NotEqual
->
false
(*
let rec mark_path start = function
| [] -> ()
| n::q -> if n.recurs = -3 then (n.recurs <- start; mark_path start q)
(* This algo is wrong: rework it ... *)
let rec compute_recurs path start n =
match n.recurs with
| -3 -> n.recurs <- start; mark_path start path
| -1 ->
n.recurs <- (-3);
X.iter (compute_recurs (n :: path) start) n.descr;
if n.recurs = -3 then n.recurs <- (-2)
| id when id = start -> mark_path start path
| _ -> () (* "no" or id <> start *)
let is_recurs n =
if (n.recurs = -1) then compute_recurs [] n.id n;
n.recurs >= 0
*)
let
rec
compute_recurs
start
n
=
if
n
.
marked
=
start
then
(
if
n
.
id
=
start
then
raise
Exit
)
else
(
n
.
marked
<-
start
;
X
.
iter
(
compute_recurs
start
)
n
.
descr
)
let
is_recurs
n
=
(* if (n.recurs = -1) then
(try compute_recurs n.id n; n.recurs <- (-2)
with Exit -> n.recurs <- 1); *)
(* n.recurs >= 0 *)
true
let
is_recurs_descr
d
=
...
...
types/types.ml
View file @
f5cbbde4
...
...
@@ -22,17 +22,20 @@ type const = Integer of Big_int.big_int | Atom of atom | Char of Chars.Unichar.t
type
pair_kind
=
[
`Normal
|
`XML
]
module
I
=
struct
type
'
a
t
=
{
type
descr
=
{
atoms
:
atom
Atoms
.
t
;
ints
:
Intervals
.
t
;
chars
:
Chars
.
t
;
times
:
(
'
a
*
'
a
)
Boolean
.
t
;
xml
:
(
'
a
*
'
a
)
Boolean
.
t
;
arrow
:
(
'
a
*
'
a
)
Boolean
.
t
;
record
:
(
bool
*
(
label
,
(
bool
*
'
a
))
SortedMap
.
t
)
Boolean
.
t
;
times
:
(
node
*
node
)
Boolean
.
t
;
xml
:
(
node
*
node
)
Boolean
.
t
;
arrow
:
(
node
*
node
)
Boolean
.
t
;
record
:
(
bool
*
(
label
,
(
bool
*
node
))
SortedMap
.
t
)
Boolean
.
t
;
}
and
node
=
{
id
:
int
;
mutable
descr
:
descr
;
}
let
empty
=
{
times
=
Boolean
.
empty
;
xml
=
Boolean
.
empty
;
...
...
@@ -69,9 +72,8 @@ module I = struct
|
Atom
a
->
atom
(
Atoms
.
atom
a
)
|
Char
c
->
char
(
Chars
.
atom
c
)
let
cup
x
y
=
if
x
=
y
then
x
else
{
if
x
=
=
y
then
x
else
{
times
=
Boolean
.
cup
x
.
times
y
.
times
;
xml
=
Boolean
.
cup
x
.
xml
y
.
xml
;
arrow
=
Boolean
.
cup
x
.
arrow
y
.
arrow
;
...
...
@@ -82,7 +84,7 @@ module I = struct
}
let
cap
x
y
=
if
x
=
y
then
x
else
{
if
x
=
=
y
then
x
else
{
times
=
Boolean
.
cap
x
.
times
y
.
times
;
xml
=
Boolean
.
cap
x
.
xml
y
.
xml
;
record
=
Boolean
.
cap
x
.
record
y
.
record
;
...
...
@@ -93,7 +95,7 @@ module I = struct
}
let
diff
x
y
=
if
x
=
y
then
empty
else
{
if
x
=
=
y
then
empty
else
{
times
=
Boolean
.
diff
x
.
times
y
.
times
;
xml
=
Boolean
.
diff
x
.
xml
y
.
xml
;
arrow
=
Boolean
.
diff
x
.
arrow
y
.
arrow
;
...
...
@@ -103,57 +105,101 @@ module I = struct
chars
=
Chars
.
diff
x
.
chars
y
.
chars
;
}
let
count
=
ref
0
let
make
()
=
incr
count
;
{
id
=
!
count
;
descr
=
empty
}
let
define
n
d
=
n
.
descr
<-
d
let
cons
d
=
incr
count
;
{
id
=
!
count
;
descr
=
d
}
let
descr
n
=
n
.
descr
let
internalize
n
=
n
let
id
n
=
n
.
id
let
rec
equal_rec
e
r1
r2
=
let
rec
equal_rec
r1
r2
=
(
r1
==
r2
)
||
match
(
r1
,
r2
)
with
|
[]
,
[]
->
()
|
(
l1
,
(
o1
,
x1
))
::
r1
,
(
l2
,
(
o2
,
x2
))
::
r2
->
if
(
l1
<>
l2
)
||
(
o1
<>
o2
)
then
raise
NotEqual
;
e
x1
x2
;
equal_rec
e
r1
r2
|
_
->
raise
NotEqual
(* check: faster to reverse the calls to e and to equal_rec ? *)
let
equal
e
a
b
=
if
a
.
atoms
<>
b
.
atoms
then
raise
NotEqual
;
if
a
.
chars
<>
b
.
chars
then
raise
NotEqual
;
if
a
.
ints
<>
b
.
ints
then
raise
NotEqual
;
Boolean
.
equal
(
fun
(
x1
,
x2
)
(
y1
,
y2
)
->
e
x1
y1
;
e
x2
y2
)
a
.
times
b
.
times
;
Boolean
.
equal
(
fun
(
x1
,
x2
)
(
y1
,
y2
)
->
e
x1
y1
;
e
x2
y2
)
a
.
xml
b
.
xml
;
Boolean
.
equal
(
fun
(
x1
,
x2
)
(
y1
,
y2
)
->
e
x1
y1
;
e
x2
y2
)
a
.
arrow
b
.
arrow
;
Boolean
.
equal
(
fun
(
o1
,
r1
)
(
o2
,
r2
)
->
if
(
o1
<>
o2
)
then
raise
NotEqual
;
equal_rec
e
r1
r2
)
a
.
record
b
.
record
let
map
f
a
=
{
times
=
Boolean
.
map
(
fun
(
x1
,
x2
)
->
(
f
x1
,
f
x2
))
a
.
times
;
xml
=
Boolean
.
map
(
fun
(
x1
,
x2
)
->
(
f
x1
,
f
x2
))
a
.
xml
;
arrow
=
Boolean
.
map
(
fun
(
x1
,
x2
)
->
(
f
x1
,
f
x2
))
a
.
arrow
;
record
=
Boolean
.
map
(
fun
(
o
,
r
)
->
(
o
,
List
.
map
(
fun
(
l
,
(
o
,
x
))
->
(
l
,
(
o
,
f
x
)))
r
))
a
.
record
;
ints
=
a
.
ints
;
atoms
=
a
.
atoms
;
chars
=
a
.
chars
;
}
let
hash
h
a
=
Hashtbl
.
hash
(
map
h
a
)
(*
(Hashtbl.hash { (map h a) with ints = Intervals.empty })
+ (Intervals.hash a.ints)
*)
let
iter
f
a
=
ignore
(
map
f
a
)
let
deep
=
4
end
(
l1
=
l2
)
&&
(
o1
=
o2
)
&&
(
x1
.
id
=
x2
.
id
)
&&
(
equal_rec
r1
r2
)
|
_
->
false
let
rec
equal_rec_list
l1
l2
=
(
l1
==
l2
)
||
match
(
l1
,
l2
)
with
|
(
o1
,
r1
)
::
l1
,
(
o2
,
r2
)
::
l2
->
(
o1
=
o2
)
&&
(
equal_rec
r1
r2
)
|
_
->
false
let
rec
equal_rec_bool
l1
l2
=
(
l1
==
l2
)
||
match
(
l1
,
l2
)
with
|
(
p1
,
n1
)
::
l1
,
(
p2
,
n2
)
::
l2
->
(
equal_rec_list
p1
p2
)
&&
(
equal_rec_list
n1
n2
)
&&
(
equal_rec_bool
l1
l2
)
|
_
->
false
let
rec
equal_times_list
l1
l2
=
(
l1
==
l2
)
||
match
(
l1
,
l2
)
with
|
(
x1
,
y1
)
::
l1
,
(
x2
,
y2
)
::
l2
->
(
x1
.
id
=
x2
.
id
)
&&
(
y1
.
id
=
y2
.
id
)
&&
(
equal_times_list
l1
l2
)
|
_
->
false
let
rec
equal_times_bool
l1
l2
=
(
l1
==
l2
)
||
match
(
l1
,
l2
)
with
|
(
p1
,
n1
)
::
l1
,
(
p2
,
n2
)
::
l2
->
(
equal_times_list
p1
p2
)
&&
(
equal_times_list
n1
n2
)
&&
(
equal_times_bool
l1
l2
)
|
_
->
false
let
equal_descr
a
b
=
(
a
.
atoms
=
b
.
atoms
)
&&
(
a
.
chars
=
b
.
chars
)
&&
(
a
.
ints
=
b
.
ints
)
&&
(
equal_times_bool
a
.
times
b
.
times
)
&&
(
equal_times_bool
a
.
xml
b
.
xml
)
&&
(
equal_times_bool
a
.
arrow
b
.
arrow
)
&&
(
equal_rec_bool
a
.
record
b
.
record
)
let
rec
hash_times_list
accu
=
function
|
(
x
,
y
)
::
l
->
hash_times_list
(
accu
*
257
+
x
.
id
*
17
+
y
.
id
)
l
|
[]
->
accu
+
17
let
rec
hash_times_bool
accu
=
function
|
(
p
,
n
)
::
l
->
hash_times_bool
(
hash_times_list
(
hash_times_list
accu
p
)
n
)
l
|
[]
->
accu
+
3
let
rec
hash_rec
accu
=
function
|
(
l
,
(
o
,
x
))
::
rem
->
hash_rec
(
257
*
accu
+
17
*
(
LabelPool
.
hash
l
)
+
x
.
id
)
rem
|
[]
->
accu
+
5
let
rec
hash_rec_list
accu
=
function
|
(
o
,
r
)
::
l
->
hash_rec_list
(
hash_rec
accu
r
)
l
|
[]
->
accu
+
17
let
rec
hash_rec_bool
accu
=
function
|
(
p
,
n
)
::
l
->
hash_rec_bool
(
hash_rec_list
(
hash_rec_list
accu
p
)
n
)
l
|
[]
->
accu
+
3
let
hash_descr
a
=
let
accu
=
(
Hashtbl
.
hash
a
.
ints
)
+
17
*
(
Hashtbl
.
hash
a
.
atoms
)
+
257
*
(
Hashtbl
.
hash
a
.
chars
)
in
let
accu
=
hash_times_bool
accu
a
.
times
in
let
accu
=
hash_times_bool
accu
a
.
xml
in
let
accu
=
hash_times_bool
accu
a
.
arrow
in
let
accu
=
hash_rec_bool
accu
a
.
record
in
accu
module
Algebra
=
Recursive_noshare
.
Make
(
I
)
include
I
include
Algebra
module
DescrHash
=
Hashtbl
.
Make
(
struct
...
...
@@ -169,11 +215,6 @@ let print_descr = ref (fun _ _ -> assert false)
let define n d = check d; define n d
*)
let
cons
d
=
let
n
=
make
()
in
define
n
d
;
internalize
n
(*
let any_rec = cons { empty with record = Boolean.full }
let any_node = make ();;
...
...
@@ -404,20 +445,10 @@ and empty_rec_record_aux (labels,(oleft,(left_opt,left)),rights) =
and
empty_rec_record
c
=
(*
let aux = List.exists (fun (_,(opt,t)) -> (not opt) && (empty_rec t)) in
*)
List
.
for_all
empty_rec_record_aux
(
get_record
c
)
let
is_empty
d
=
(* Printf.eprintf "+"; flush stderr; *)
let
old
=
!
memo
in
let
r
=
empty_rec
d
in
if
not
r
then
memo
:=
old
else
if
not
(
is_recurs_descr
d
)
then
memo
:=
Assumptions
.
add
d
!
memo
;
(* cache_false := Assumptions.empty; *)
(* Printf.eprintf "-\n"; flush stderr; *)
r
empty_rec
d
let
non_empty
d
=
not
(
is_empty
d
)
...
...
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