Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
POTTIER Francois
menhir
Commits
4172c02f
Commit
4172c02f
authored
Apr 28, 2016
by
POTTIER Francois
Browse files
Replace all tabs with spaces (expand -t 8).
parent
004933c6
Changes
66
Hide whitespace changes
Inline
Side-by-side
src/Engine.ml
View file @
4172c02f
...
...
@@ -326,7 +326,7 @@ module Make (T : TABLE) = struct
else
begin
(* The stack is nonempty. Pop a cell, updating the current state
with that found in the popped cell, and try again. *)
with that found in the popped cell, and try again. *)
let
env
=
{
env
with
stack
=
next
;
...
...
src/Engine.mli
View file @
4172c02f
...
...
@@ -4,5 +4,5 @@ open EngineTypes
module
Make
(
T
:
TABLE
)
:
ENGINE
with
type
state
=
T
.
state
and
type
token
=
T
.
token
and
type
semantic_value
=
T
.
semantic_value
and
type
semantic_value
=
T
.
semantic_value
and
type
production
=
T
.
production
src/Fix.ml
View file @
4172c02f
...
...
@@ -197,16 +197,16 @@ end
assert
(
src
.
outgoing
=
[]
);
let
rec
loop
=
function
|
[]
->
()
()
|
dst
::
dsts
->
if
dst
.
marked
then
loop
dsts
(* skip duplicate elements *)
else
begin
dst
.
marked
<-
true
;
link
src
dst
;
loop
dsts
;
dst
.
marked
<-
false
end
if
dst
.
marked
then
loop
dsts
(* skip duplicate elements *)
else
begin
dst
.
marked
<-
true
;
link
src
dst
;
loop
dsts
;
dst
.
marked
<-
false
end
in
loop
dsts
...
...
src/Maps.ml
View file @
4172c02f
...
...
@@ -33,7 +33,7 @@ end
module
PersistentMapsToImperativeMaps
(
M
:
PERSISTENT_MAPS
)
:
IMPERATIVE_MAPS
with
type
key
=
M
.
key
and
type
'
data
t
=
'
data
M
.
t
ref
and
type
'
data
t
=
'
data
M
.
t
ref
=
struct
type
key
=
...
...
@@ -63,7 +63,7 @@ module ImperativeMapsToImperativeMap
(
M
:
IMPERATIVE_MAPS
)
(
D
:
sig
type
data
end
)
:
IMPERATIVE_MAP
with
type
key
=
M
.
key
and
type
data
=
D
.
data
and
type
data
=
D
.
data
=
struct
type
key
=
...
...
@@ -113,17 +113,17 @@ module ArrayAsImperativeMaps
let
find
key
m
=
match
m
.
(
key
)
with
|
None
->
raise
Not_found
raise
Not_found
|
Some
data
->
data
data
let
iter
f
m
=
Array
.
iteri
(
fun
key
data
->
match
data
with
|
None
->
()
()
|
Some
data
->
f
key
data
f
key
data
)
m
end
...
...
src/Maps.mli
View file @
4172c02f
...
...
@@ -44,7 +44,7 @@ end
module
PersistentMapsToImperativeMaps
(
M
:
PERSISTENT_MAPS
)
:
IMPERATIVE_MAPS
with
type
key
=
M
.
key
and
type
'
data
t
=
'
data
M
.
t
ref
and
type
'
data
t
=
'
data
M
.
t
ref
(* An implementation of imperative maps can be made to satisfy the interface
of a single imperative map. This map is obtained via a single call to [create]. *)
...
...
@@ -53,7 +53,7 @@ module ImperativeMapsToImperativeMap
(
M
:
IMPERATIVE_MAPS
)
(
D
:
sig
type
data
end
)
:
IMPERATIVE_MAP
with
type
key
=
M
.
key
and
type
data
=
D
.
data
and
type
data
=
D
.
data
(* An implementation of imperative maps as arrays is possible if keys
are consecutive integers. *)
...
...
src/PackedIntArray.ml
View file @
4172c02f
...
...
@@ -22,12 +22,12 @@ let magnitude (v : int) =
else
let
rec
check
k
max
=
(* [max] equals [2^k] *)
if
(
max
<=
0
)
||
(
v
<
max
)
then
k
(* if [max] just overflew, then [v] requires a full ocaml
integer, and [k] is the number of bits in an ocaml integer
plus one, that is, [Sys.word_size]. *)
k
(* if [max] just overflew, then [v] requires a full ocaml
integer, and [k] is the number of bits in an ocaml integer
plus one, that is, [Sys.word_size]. *)
else
check
(
2
*
k
)
(
max
*
max
)
check
(
2
*
k
)
(
max
*
max
)
in
check
1
2
...
...
@@ -68,9 +68,9 @@ let pack (a : int array) : t =
let
n
=
if
m
mod
w
=
0
then
m
/
w
m
/
w
else
m
/
w
+
1
m
/
w
+
1
in
let
s
=
...
...
@@ -84,11 +84,11 @@ let pack (a : int array) : t =
let
next
()
=
let
ii
=
!
i
in
if
ii
=
m
then
0
(* ran off the end, pad with zeroes *)
0
(* ran off the end, pad with zeroes *)
else
let
v
=
a
.
(
ii
)
in
i
:=
ii
+
1
;
v
let
v
=
a
.
(
ii
)
in
i
:=
ii
+
1
;
v
in
(* Fill up the string. *)
...
...
@@ -96,7 +96,7 @@ let pack (a : int array) : t =
for
j
=
0
to
n
-
1
do
let
c
=
ref
0
in
for
_x
=
1
to
w
do
c
:=
(
!
c
lsl
k
)
lor
next
()
c
:=
(
!
c
lsl
k
)
lor
next
()
done
;
Bytes
.
set
s
j
(
Char
.
chr
!
c
)
done
;
...
...
@@ -128,8 +128,8 @@ let pack (a : int array) : t =
for
i
=
0
to
m
-
1
do
let
v
=
ref
a
.
(
i
)
in
for
x
=
1
to
w
do
Bytes
.
set
s
((
i
+
1
)
*
w
-
x
)
(
Char
.
chr
(
!
v
land
255
));
v
:=
!
v
lsr
8
Bytes
.
set
s
((
i
+
1
)
*
w
-
x
)
(
Char
.
chr
(
!
v
land
255
));
v
:=
!
v
lsr
8
done
done
;
...
...
src/RowDisplacement.ml
View file @
4172c02f
...
...
@@ -82,13 +82,13 @@ let compress
let
rec
loop
(
j
:
int
)
(
rank
:
int
)
(
row
:
'
a
row
)
=
if
j
<
0
then
i
,
rank
,
row
i
,
rank
,
row
else
let
x
=
line
.
(
j
)
in
if
insignificant
x
then
loop
(
j
-
1
)
rank
row
else
loop
(
j
-
1
)
(
1
+
rank
)
((
j
,
x
)
::
row
)
let
x
=
line
.
(
j
)
in
if
insignificant
x
then
loop
(
j
-
1
)
rank
row
else
loop
(
j
-
1
)
(
1
+
rank
)
((
j
,
x
)
::
row
)
in
loop
(
n
-
1
)
0
[]
...
...
@@ -138,31 +138,31 @@ let compress
let
rec
loop
=
function
|
[]
->
true
true
|
(
j
,
x
)
::
row
->
(* [x] is a significant element. *)
(* [x] is a significant element. *)
(* By hypothesis, [k + j] is nonnegative. If it is greater than or
equal to the current length of the data array, stop -- the row
fits. *)
(* By hypothesis, [k + j] is nonnegative. If it is greater than or
equal to the current length of the data array, stop -- the row
fits. *)
assert
(
k
+
j
>=
0
);
assert
(
k
+
j
>=
0
);
if
k
+
j
>=
d
then
true
if
k
+
j
>=
d
then
true
(* We now know that [k + j] is within bounds of the data
array. Check whether it is compatible with the element [y] found
there. If it is, continue. If it isn't, stop -- the row does not
fit. *)
(* We now know that [k + j] is within bounds of the data
array. Check whether it is compatible with the element [y] found
there. If it is, continue. If it isn't, stop -- the row does not
fit. *)
else
let
y
=
InfiniteArray
.
get
data
(
k
+
j
)
in
if
insignificant
y
||
equal
x
y
then
loop
row
else
false
else
let
y
=
InfiniteArray
.
get
data
(
k
+
j
)
in
if
insignificant
y
||
equal
x
y
then
loop
row
else
false
in
loop
row
...
...
@@ -191,19 +191,19 @@ let compress
let
fit
row
=
match
row
with
|
[]
->
0
(* irrelevant *)
0
(* irrelevant *)
|
(
j
,
_
)
::
_
->
fit
(
-
j
)
row
fit
(
-
j
)
row
in
(* Write [row] at (compatible) offset [k]. *)
let
rec
write
k
=
function
|
[]
->
()
()
|
(
j
,
x
)
::
row
->
InfiniteArray
.
set
data
(
k
+
j
)
x
;
write
k
row
InfiniteArray
.
set
data
(
k
+
j
)
x
;
write
k
row
in
(* Iterate over the sorted array of rows. Fit and write each row at
...
...
src/TableInterpreter.ml
View file @
4172c02f
...
...
@@ -15,13 +15,13 @@ module Make (T : TableFormat.TABLES)
type
semantic_value
=
Obj
.
t
let
token2terminal
=
T
.
token2terminal
let
token2value
=
T
.
token2value
let
error_terminal
=
T
.
error_terminal
...
...
@@ -57,21 +57,21 @@ module Make (T : TableFormat.TABLES)
let
action
state
terminal
value
shift
reduce
fail
env
=
match
PackedIntArray
.
unflatten1
T
.
error
state
terminal
with
|
1
->
let
action
=
unmarshal2
T
.
action
state
terminal
in
let
opcode
=
action
land
0b11
and
param
=
action
lsr
2
in
if
opcode
>=
0b10
then
(* 0b10 : shift/discard *)
(* 0b11 : shift/nodiscard *)
let
please_discard
=
(
opcode
=
0b10
)
in
shift
env
please_discard
terminal
value
param
else
(* 0b01 : reduce *)
(* 0b00 : cannot happen *)
reduce
env
param
let
action
=
unmarshal2
T
.
action
state
terminal
in
let
opcode
=
action
land
0b11
and
param
=
action
lsr
2
in
if
opcode
>=
0b10
then
(* 0b10 : shift/discard *)
(* 0b11 : shift/nodiscard *)
let
please_discard
=
(
opcode
=
0b10
)
in
shift
env
please_discard
terminal
value
param
else
(* 0b01 : reduce *)
(* 0b00 : cannot happen *)
reduce
env
param
|
c
->
assert
(
c
=
0
);
fail
env
assert
(
c
=
0
);
fail
env
let
goto
state
prod
=
let
code
=
unmarshal2
T
.
goto
state
(
PackedIntArray
.
get
T
.
lhs
prod
)
in
...
...
@@ -79,12 +79,12 @@ module Make (T : TableFormat.TABLES)
code
-
1
exception
Error
=
T
.
Error
T
.
Error
type
semantic_action
=
(
state
,
semantic_value
,
token
)
EngineTypes
.
env
->
(
state
,
semantic_value
)
EngineTypes
.
stack
let
semantic_action
prod
=
(* Indexing into the array [T.semantic_action] is off by [T.start],
because the start productions do not have entries in this array. *)
...
...
@@ -104,21 +104,21 @@ module Make (T : TableFormat.TABLES)
|
Some
_
->
fprintf
stderr
"State %d:
\n
%!"
state
|
None
->
()
()
let
shift
terminal
state
=
match
T
.
trace
with
|
Some
(
terminals
,
_
)
->
fprintf
stderr
"Shifting (%s) to state %d
\n
%!"
terminals
.
(
terminal
)
state
|
None
->
()
()
let
reduce_or_accept
prod
=
match
T
.
trace
with
|
Some
(
_
,
productions
)
->
fprintf
stderr
"%s
\n
%!"
productions
.
(
prod
)
|
None
->
()
()
let
lookahead_token
token
startp
endp
=
match
T
.
trace
with
...
...
@@ -128,28 +128,28 @@ module Make (T : TableFormat.TABLES)
startp
.
Lexing
.
pos_cnum
endp
.
Lexing
.
pos_cnum
|
None
->
()
()
let
initiating_error_handling
()
=
match
T
.
trace
with
|
Some
_
->
fprintf
stderr
"Initiating error handling
\n
%!"
|
None
->
()
()
let
resuming_error_handling
()
=
match
T
.
trace
with
|
Some
_
->
fprintf
stderr
"Resuming error handling
\n
%!"
|
None
->
()
()
let
handling_error
state
=
match
T
.
trace
with
|
Some
_
->
fprintf
stderr
"Handling error in state %d
\n
%!"
state
|
None
->
()
()
end
...
...
src/TableInterpreter.mli
View file @
4172c02f
...
...
@@ -12,6 +12,6 @@ module Make (T : TableFormat.TABLES)
:
EngineTypes
.
ENGINE
with
type
state
=
int
and
type
token
=
T
.
token
and
type
semantic_value
=
Obj
.
t
and
type
semantic_value
=
Obj
.
t
and
type
production
=
int
src/action.ml
View file @
4172c02f
...
...
@@ -137,8 +137,8 @@ let keywords action =
let
print
f
action
=
let
module
P
=
Printer
.
Make
(
struct
let
f
=
f
let
locate_stretches
=
None
end
)
let
locate_stretches
=
None
end
)
in
P
.
expr
action
.
expr
...
...
src/astar.ml
100755 → 100644
View file @
4172c02f
...
...
@@ -160,16 +160,16 @@ end) = struct
inode
.
priority
<-
priority
;
match
InfiniteArray
.
get
a
priority
with
|
None
->
InfiniteArray
.
set
a
priority
(
Some
inode
);
InfiniteArray
.
set
a
priority
(
Some
inode
);
(* Decrease [best], if necessary, so as not to miss the new element.
In the special case of A*, this never happens. *)
assert
(
!
best
<=
priority
);
(* if priority < !best then best := priority *)
(* if priority < !best then best := priority *)
|
Some
inode'
->
inode
.
next
<-
inode'
;
inode
.
prev
<-
inode'
.
prev
;
inode'
.
prev
.
next
<-
inode
;
inode'
.
prev
<-
inode
inode
.
next
<-
inode'
;
inode
.
prev
<-
inode'
.
prev
;
inode'
.
prev
.
next
<-
inode
;
inode'
.
prev
<-
inode
(* Takes a node off its doubly linked list. Does not adjust [best],
as this is not necessary in order to preserve the invariant. *)
...
...
@@ -179,16 +179,16 @@ end) = struct
InfiniteArray
.
set
a
inode
.
priority
None
else
begin
InfiniteArray
.
set
a
inode
.
priority
(
Some
inode
.
next
);
inode
.
next
.
prev
<-
inode
.
prev
;
inode
.
prev
.
next
<-
inode
.
next
;
inode
.
next
<-
inode
;
inode
.
prev
<-
inode
inode
.
next
.
prev
<-
inode
.
prev
;
inode
.
prev
.
next
<-
inode
.
next
;
inode
.
next
<-
inode
;
inode
.
prev
<-
inode
end
;
inode
.
priority
<-
-
1
let
rec
get
()
=
if
!
cardinal
=
0
then
None
None
else
get_nonempty
()
...
...
@@ -207,7 +207,7 @@ end) = struct
let
add_or_decrease
inode
priority
=
if
inode
.
priority
>=
0
then
remove
inode
;
remove
inode
;
add
inode
priority
end
...
...
src/attic/heap.ml
View file @
4172c02f
...
...
@@ -68,10 +68,10 @@ module Imperative(X : Ordered) = struct
let
rec
moveup
i
=
let
fi
=
(
i
-
1
)
/
2
in
if
i
>
0
&&
X
.
compare
d
.
(
fi
)
x
<
0
then
begin
d
.
(
i
)
<-
d
.
(
fi
);
moveup
fi
d
.
(
i
)
<-
d
.
(
fi
);
moveup
fi
end
else
d
.
(
i
)
<-
x
d
.
(
i
)
<-
x
in
moveup
n
;
h
.
size
<-
n
+
1
...
...
@@ -90,17 +90,17 @@ module Imperative(X : Ordered) = struct
let
rec
movedown
i
=
let
j
=
2
*
i
+
1
in
if
j
<
n
then
let
j
=
let
j'
=
j
+
1
in
if
j'
<
n
&&
X
.
compare
d
.
(
j'
)
d
.
(
j
)
>
0
then
j'
else
j
in
if
X
.
compare
d
.
(
j
)
x
>
0
then
begin
d
.
(
i
)
<-
d
.
(
j
);
movedown
j
end
else
d
.
(
i
)
<-
x
let
j
=
let
j'
=
j
+
1
in
if
j'
<
n
&&
X
.
compare
d
.
(
j'
)
d
.
(
j
)
>
0
then
j'
else
j
in
if
X
.
compare
d
.
(
j
)
x
>
0
then
begin
d
.
(
i
)
<-
d
.
(
j
);
movedown
j
end
else
d
.
(
i
)
<-
x
else
d
.
(
i
)
<-
x
d
.
(
i
)
<-
x
in
movedown
0
...
...
src/attic/minimal.ml
View file @
4172c02f
...
...
@@ -35,8 +35,8 @@ let () =
Error
.
logG
2
(
fun
f
->
for
nt
=
Nonterminal
.
start
to
Nonterminal
.
n
-
1
do
Printf
.
fprintf
f
"minimal(%s) = %s
\n
"
(
Nonterminal
.
print
false
nt
)
(
CompletedNatWitness
.
print
Terminal
.
print
(
MINIMAL
.
nonterminal
nt
))
(
Nonterminal
.
print
false
nt
)
(
CompletedNatWitness
.
print
Terminal
.
print
(
MINIMAL
.
nonterminal
nt
))
done
)
src/attic/nonpositiveCycles.ml
View file @
4172c02f
...
...
@@ -38,28 +38,28 @@ end) = struct
match
d1
,
d2
with
|
Infinity
,
_
|
_
,
Infinity
->
Infinity
Infinity
|
Finite
i1
,
Finite
i2
->
Finite
(
i1
+
i2
)
Finite
(
i1
+
i2
)
let
min
d1
d2
=
match
d1
,
d2
with
|
Infinity
,
d
|
d
,
Infinity
->
d
d
|
Finite
i1
,
Finite
i2
->
Finite
(
min
i1
i2
)
Finite
(
min
i1
i2
)
let
le
d1
d2
=
match
d1
,
d2
with
|
Infinity
,
Infinity
->
true
true
|
Infinity
,
Finite
_
->
false
false
|
Finite
_
,
Infinity
->
true
true
|
Finite
i1
,
Finite
i2
->
i1
<=
i2
i1
<=
i2
(* Allocate and initialize a distance matrix. At allocation time, every entry
is initialized to infinity. Then, we iterate over all edges, and copy them
...
...
@@ -73,18 +73,18 @@ end) = struct
let
d
=
Array
.
init
n
(
fun
i
->
Array
.
init
n
(
fun
j
->
Infinity
Infinity
)
)
let
()
=
iter
(
fun
source
->
successors
(
fun
weight
target
->
(* We use a min operation, so the graph may be a multi-graph, that is,
multiple edges between two nodes are permitted. *)
let
i
=
index
source
and
j
=
index
target
in
d
.
(
i
)
.
(
j
)
<-
min
(
Finite
weight
)
d
.
(
i
)
.
(
j
)
(* We use a min operation, so the graph may be a multi-graph, that is,
multiple edges between two nodes are permitted. *)
let
i
=
index
source
and
j
=
index
target
in
d
.
(
i
)
.
(
j
)
<-
min
(
Finite
weight
)
d
.
(
i
)
.
(
j
)
)
source
)
...
...
@@ -100,13 +100,13 @@ end) = struct
let
graph_has_nonpositive_simple_cycle
:
bool
=
try
for
k
=
0
to
n
-
1
do
for
i
=
0
to
n
-
1
do
for
j
=
0
to
n
-
1
do
d
.
(
i
)
.
(
j
)
<-
min
d
.
(
i
)
.
(
j
)
(
add
d
.
(
i
)
.
(
k
)
d
.
(
k
)
.
(
j
));
if
i
=
j
&&
le
d
.
(
i
)
.
(
j
)
(
Finite
0
)
then
raise
Detection
done
done
for
i
=
0
to
n
-
1
do
for
j
=
0
to
n
-
1
do
d
.
(
i
)
.
(
j
)
<-
min
d
.
(
i
)
.
(
j
)
(
add
d
.
(
i
)
.
(
k
)
d
.
(
k
)
.
(
j
));
if
i
=
j
&&
le
d
.
(
i
)
.
(
j
)
(
Finite
0
)
then
raise
Detection
done
done
done
;
false
with
Detection
->
...
...
src/attic/reductionGraphs.ml
View file @
4172c02f
...
...
@@ -27,7 +27,7 @@ let make_reduction_graph tok =
let
module
ReductionGraph
=
struct
type
node
=
Lr1
.
node
Lr1
.
node
let
n
=
Lr1
.
n
...
...
@@ -42,14 +42,14 @@ let make_reduction_graph tok =
let
rec
pop_word
n
states
w
=
if
n
=
0
then
states
states
else
match
w
with
|
[]
->
(* the invariant is too weak to ensure that reduction is possible! *)