Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
POTTIER Francois
menhir
Commits
1a96b802
Commit
1a96b802
authored
Nov 01, 2018
by
POTTIER Francois
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Remove trailing whitespace in test files.
parent
041bd10d
Changes
230
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
75 changed files
with
2294 additions
and
2294 deletions
+2294
-2294
test/bad/constant-inline-in-multiple-def-1.mly
test/bad/constant-inline-in-multiple-def-1.mly
+1
-1
test/bad/epsilon-cycle.mly
test/bad/epsilon-cycle.mly
+1
-1
test/bad/invalid-declarations-d.mly
test/bad/invalid-declarations-d.mly
+1
-1
test/bad/invalid-declarations-e.mly
test/bad/invalid-declarations-e.mly
+1
-1
test/bad/obc.mly
test/bad/obc.mly
+41
-41
test/bad/producer-with-a-positional-name.mly
test/bad/producer-with-a-positional-name.mly
+1
-1
test/bad/undefined-position.mly
test/bad/undefined-position.mly
+1
-1
test/bad/undefined-producer.mly
test/bad/undefined-producer.mly
+1
-1
test/good/alphaCaml-demos-poplmark.mly
test/good/alphaCaml-demos-poplmark.mly
+11
-11
test/good/alphaprolog.mly
test/good/alphaprolog.mly
+60
-60
test/good/alphaprolog.opp.exp
test/good/alphaprolog.opp.exp
+34
-34
test/good/amalthea.mly
test/good/amalthea.mly
+4
-4
test/good/attapl-deptypes.mly
test/good/attapl-deptypes.mly
+21
-21
test/good/attapl-deptypes.opp.exp
test/good/attapl-deptypes.opp.exp
+3
-3
test/good/attapl-mini.mly
test/good/attapl-mini.mly
+1
-1
test/good/bauer.mly
test/good/bauer.mly
+3
-3
test/good/bauer.opp.exp
test/good/bauer.opp.exp
+1
-1
test/good/bibtex_parser.mly
test/good/bibtex_parser.mly
+6
-6
test/good/bran.mly
test/good/bran.mly
+4
-4
test/good/christian.mly
test/good/christian.mly
+78
-78
test/good/cigen-cparser.mly
test/good/cigen-cparser.mly
+8
-8
test/good/cigen-cparser.opp.exp
test/good/cigen-cparser.opp.exp
+1
-1
test/good/cil-cparser.mly
test/good/cil-cparser.mly
+134
-134
test/good/cil-cparser.opp.exp
test/good/cil-cparser.opp.exp
+38
-38
test/good/cil-formatparse.mly
test/good/cil-formatparse.mly
+376
-376
test/good/cil-formatparse.opp.exp
test/good/cil-formatparse.opp.exp
+278
-278
test/good/cime-genpoly.mly
test/good/cime-genpoly.mly
+9
-9
test/good/cime-genpoly.opp.exp
test/good/cime-genpoly.opp.exp
+7
-7
test/good/cime-parameterized-signatures.mly
test/good/cime-parameterized-signatures.mly
+15
-15
test/good/cime-parameterized-signatures.opp.exp
test/good/cime-parameterized-signatures.opp.exp
+1
-1
test/good/cime-poly-interp.mly
test/good/cime-poly-interp.mly
+4
-4
test/good/cime-poly-interp.opp.exp
test/good/cime-poly-interp.opp.exp
+3
-3
test/good/cime-poly.mly
test/good/cime-poly.mly
+21
-21
test/good/cime-poly.opp.exp
test/good/cime-poly.opp.exp
+2
-2
test/good/cime-signature.mly
test/good/cime-signature.mly
+9
-9
test/good/cime-syntax.mly
test/good/cime-syntax.mly
+62
-62
test/good/cime-syntax.opp.exp
test/good/cime-syntax.opp.exp
+28
-28
test/good/cime-term.mly
test/good/cime-term.mly
+5
-5
test/good/cime-term.opp.exp
test/good/cime-term.opp.exp
+2
-2
test/good/cime-terms-signature.mly
test/good/cime-terms-signature.mly
+10
-10
test/good/cime-terms-signature.opp.exp
test/good/cime-terms-signature.opp.exp
+3
-3
test/good/cime-terms.mly
test/good/cime-terms.mly
+13
-13
test/good/cime-theory.mly
test/good/cime-theory.mly
+18
-18
test/good/cime-theory.opp.exp
test/good/cime-theory.opp.exp
+9
-9
test/good/cime-toplevel.mly
test/good/cime-toplevel.mly
+21
-21
test/good/cime-word.mly
test/good/cime-word.mly
+19
-19
test/good/cime-word.opp.exp
test/good/cime-word.opp.exp
+5
-5
test/good/cminor.mly
test/good/cminor.mly
+1
-1
test/good/cocci.mly
test/good/cocci.mly
+15
-15
test/good/coercion-constraint.mly
test/good/coercion-constraint.mly
+47
-47
test/good/coercion-constraint.opp.exp
test/good/coercion-constraint.opp.exp
+34
-34
test/good/coercion-mini.mly
test/good/coercion-mini.mly
+118
-118
test/good/coercion-mini.opp.exp
test/good/coercion-mini.opp.exp
+83
-83
test/good/compcert_pre_parser.mly
test/good/compcert_pre_parser.mly
+2
-2
test/good/compcert_pre_parser_new.mly
test/good/compcert_pre_parser_new.mly
+1
-1
test/good/compsyn.mly
test/good/compsyn.mly
+106
-106
test/good/compsyn.opp.exp
test/good/compsyn.opp.exp
+1
-1
test/good/condition_parser.mly
test/good/condition_parser.mly
+7
-7
test/good/confluence-psl.mly
test/good/confluence-psl.mly
+2
-2
test/good/confluence.mly
test/good/confluence.mly
+2
-2
test/good/cutdown.mly
test/good/cutdown.mly
+1
-1
test/good/dml.mly
test/good/dml.mly
+5
-5
test/good/dule.mly
test/good/dule.mly
+26
-26
test/good/dule.opp.exp
test/good/dule.opp.exp
+11
-11
test/good/execparser.mly
test/good/execparser.mly
+75
-75
test/good/execparser.opp.exp
test/good/execparser.opp.exp
+26
-26
test/good/featherweight.mly
test/good/featherweight.mly
+266
-266
test/good/featherweight.opp.exp
test/good/featherweight.opp.exp
+24
-24
test/good/flowcaml-docgen.mly
test/good/flowcaml-docgen.mly
+2
-2
test/good/flowcaml-docgen.opp.exp
test/good/flowcaml-docgen.opp.exp
+2
-2
test/good/flowcaml.mly
test/good/flowcaml.mly
+31
-31
test/good/flowcaml.opp.exp
test/good/flowcaml.opp.exp
+11
-11
test/good/focc-pure-def.mly
test/good/focc-pure-def.mly
+9
-9
test/good/focc-pure-def.opp.exp
test/good/focc-pure-def.opp.exp
+5
-5
test/good/fp.mly
test/good/fp.mly
+6
-6
No files found.
test/bad/constant-inline-in-multiple-def-1.mly
View file @
1a96b802
%
start
<
int
>
b
%
start
<
int
>
b
%%
b
:
{}
...
...
test/bad/epsilon-cycle.mly
View file @
1a96b802
%
start
a
%
start
a
%
type
<
unit
>
a
%
token
B
...
...
test/bad/invalid-declarations-d.mly
View file @
1a96b802
...
...
@@ -7,7 +7,7 @@
%
token
BAZAR
%
left
FOO
BAR
%
right
/*
error
*/
%
nonassoc
BAR
QWD
QWD
QWD
ASD
QWD
D
QWD
WQD
QWD
%
nonassoc
BAR
QWD
QWD
QWD
ASD
QWD
D
QWD
WQD
QWD
%
token
BAR
%%
...
...
test/bad/invalid-declarations-e.mly
View file @
1a96b802
...
...
@@ -6,7 +6,7 @@
%
type
<
int
>
date
time
%
token
BAZAR
%
left
FOO
BAR
%
nonassoc
BAR
QWD
QWD
QWD
ASD
QWD
D
QWD
WQD
QWD
%
nonassoc
BAR
QWD
QWD
QWD
ASD
QWD
D
QWD
WQD
QWD
%
token
BAR
%%
...
...
test/bad/obc.mly
View file @
1a96b802
...
...
@@ -24,12 +24,12 @@ let rcsid = "$Id: obc.mly,v 1.1 2005/08/23 11:15:14 fpottier Exp $"
/*
punctuation
*/
%
token
SEMI
DOT
COLON
LPAR
RPAR
COMMA
SUB
BUS
LBRACE
RBRACE
%
token
STAR
UPARROW
EQUAL
MINUS
PLUS
ASSIGN
VBAR
DOTDOT
%
token
STAR
UPARROW
EQUAL
MINUS
PLUS
ASSIGN
VBAR
DOTDOT
%
token
BADTOK
/*
keywords
*/
%
token
ARRAY
BEGIN
CONST
DO
ELSE
ELSIF
END
IF
IMPORT
IS
OF
%
token
FOR
MODULE
PROCEDURE
RECORD
REPEAT
RETURN
THEN
TO
TYPE
%
token
ARRAY
BEGIN
CONST
DO
ELSE
ELSIF
END
IF
IMPORT
IS
OF
%
token
FOR
MODULE
PROCEDURE
RECORD
REPEAT
RETURN
THEN
TO
TYPE
%
token
UNTIL
VAR
WHILE
NOT
POINTER
NIL
WITH
%
token
CASE
LOOP
EXIT
BY
LOCAL
ABSTRACT
...
...
@@ -48,7 +48,7 @@ let rcsid = "$Id: obc.mly,v 1.1 2005/08/23 11:15:14 fpottier Exp $"
%
start
program
%
{
let
parse_error
msg
=
let
parse_error
msg
=
syn_error
"$ at token '$'"
[
fStr
msg
;
fToken
]
let
parse_error2
msg
loc2
=
...
...
@@ -79,7 +79,7 @@ let make_call e =
let
fix
e
=
match
e
.
e_guts
with
Decimal
s
->
Decimal
s
->
makeExpr
(
Const
(
IntVal
(
Int32
.
of_string
s
)
,
numtype
)
,
e
.
e_loc
)
|
_
->
e
...
...
@@ -93,12 +93,12 @@ let neg e =
let
mkExpr
e
=
makeExpr
(
e
,
lloc
()
)
let
mkTypexpr
tx
=
makeTypexpr
(
tx
,
lloc
()
)
%
}
%%
program
:
MODULE
modname
semi
imports
block
opt_ident
DOT
{
check_end
$
2
.
x_name
$
6
(
rloc
6
);
program
:
MODULE
modname
semi
imports
block
opt_ident
DOT
{
check_end
$
2
.
x_name
$
6
(
rloc
6
);
Module
(
$
2
,
$
4
,
$
5
,
ref
[]
)
}
;
modname
:
...
...
@@ -115,22 +115,22 @@ import :
name
{
(
$
1
,
$
1
.
x_name
,
ref
0
)
}
|
name
ASSIGN
IDENT
{
(
$
1
,
$
3
,
ref
0
)
}
;
block
:
block
:
decls
body
END
{
Block
(
$
1
,
$
2
,
ref
0
)
}
;
body
:
/*
empty
*/
{
makeStmt
(
SkipStmt
,
no_loc
)
}
|
BEGIN
stmts
{
$
2
}
;
decls
:
decls
:
/*
empty
*/
{
[]
}
|
decls
decl
{
$
1
@
$
2
}
;
decl
:
decl
:
CONST
const_decls
{
$
2
}
|
VAR
var_decls
{
$
2
}
|
TYPE
type_decls
{
$
2
}
|
proc
{
[
$
1
]
}
|
TYPE
type_decls
{
$
2
}
|
proc
{
[
$
1
]
}
|
error
SEMI
{
[]
}
;
const_decls
:
...
...
@@ -144,7 +144,7 @@ type_decls :
type_decl
{
[
$
1
]
}
|
type_decl
type_decls
{
$
1
::
$
2
}
;
type_decl
:
type_decl
:
defid
EQUAL
typexpr
semi
{
TypeDecl
(
$
1
,
$
3
)
}
;
var_decls
:
...
...
@@ -155,7 +155,7 @@ var_decl :
defids
COLON
typexpr
semi
{
VarDecl
(
VarDef
,
$
1
,
$
3
)
}
;
proc
:
PROCEDURE
defid
params
semi
block
opt_ident
semi
PROCEDURE
defid
params
semi
block
opt_ident
semi
{
check_end
$
2
.
x_name
$
6
(
rloc
6
);
ProcDecl
(
Procedure
,
$
2
,
$
3
,
$
5
)
}
|
PROCEDURE
receiver
defid
params
semi
block
opt_ident
semi
...
...
@@ -166,14 +166,14 @@ proc :
{
let
(
Heading
(
ps
,
r
))
=
$
5
in
ProcDecl
(
AbsMeth
,
$
4
,
Heading
(
$
3
::
ps
,
r
)
,
NoBlock
)
}
|
PROCEDURE
defid
params
IS
STRING
semi
{
PrimDecl
(
$
2
,
$
3
,
$
5
)
}
{
PrimDecl
(
$
2
,
$
3
,
$
5
)
}
|
PROCEDURE
error
block
opt_ident
semi
{
DummyDecl
}
;
receiver
:
LPAR
defid
COLON
typename
RPAR
LPAR
defid
COLON
typename
RPAR
{
VarDecl
(
ParamDef
,
[
$
2
]
,
$
4
)
}
|
LPAR
VAR
defid
COLON
typename
RPAR
|
LPAR
VAR
defid
COLON
typename
RPAR
{
VarDecl
(
VParamDef
,
[
$
3
]
,
$
5
)
}
;
params
:
...
...
@@ -181,11 +181,11 @@ params :
|
LPAR
RPAR
result
{
Heading
([]
,
$
3
)
}
|
LPAR
formals
RPAR
result
{
Heading
(
$
2
,
$
4
)
}
;
formals
:
formals
:
formal
{
[
$
1
]
}
|
formal
semi
formals
{
$
1
::
$
3
}
;
formal
:
formal
:
defids
COLON
typexpr
{
VarDecl
(
ParamDef
,
$
1
,
$
3
)
}
|
VAR
defids
COLON
typexpr
{
VarDecl
(
VParamDef
,
$
2
,
$
4
)
}
;
...
...
@@ -202,7 +202,7 @@ gracefully with missing and duplicated semicolons. The nonterminal
'
stmts_a'
generates
sequences
that
(
if
non
-
empty
)
end
with
a
semicolon
,
and
'
stmts_b'
generates
non
-
empty
sequences
that
do
not
end
with
a
semicolon
.
Missing
semicolons
are
inserted
before
any
statement
that
begins
with
a
keyword
.
statement
that
begins
with
a
keyword
.
The
salient
fact
is
that
the
parser
ends
up
with
two
states
,
one
(
linked
to
stmts_a
)
where
it
has
sen
a
semicolon
and
is
ready
to
see
...
...
@@ -216,12 +216,12 @@ stmts :
stmts_a
:
/*
empty
*/
{
[]
}
|
stmts_a
SEMI
{
$
1
}
|
stmts_b
SEMI
{
$
1
}
|
stmts_b
SEMI
{
$
1
}
|
stmts_b
error
SEMI
{
$
1
}
;
stmts_b
:
stmts_a
stmt0
{
makeStmt
(
$
2
,
rloc
2
)
::
$
1
}
|
stmts_a
stmt1
{
makeStmt
(
$
2
,
rloc
2
)
::
$
1
}
stmts_a
stmt0
{
makeStmt
(
$
2
,
rloc
2
)
::
$
1
}
|
stmts_a
stmt1
{
makeStmt
(
$
2
,
rloc
2
)
::
$
1
}
|
stmts_b
missing
stmt1
{
makeStmt
(
$
3
,
rloc
3
)
::
$
1
}
;
missing
:
...
...
@@ -244,8 +244,8 @@ stmt1 :
|
LOOP
stmts
END
{
LoopStmt
$
2
}
|
EXIT
{
ExitStmt
}
|
FOR
designator
ASSIGN
expr
TO
expr
by_part
DO
stmts
END
{
ForStmt
(
$
2
,
$
4
,
$
6
,
$
7
,
$
9
,
ref
dummy_def
)
}
|
WITH
with_branches
else_part
END
{
ForStmt
(
$
2
,
$
4
,
$
6
,
$
7
,
$
9
,
ref
dummy_def
)
}
|
WITH
with_branches
else_part
END
{
WithStmt
(
$
2
,
$
3
)
}
|
LOCAL
decls
body
END
{
LocalStmt
(
$
2
,
$
3
)
}
|
error
{
ErrStmt
}
;
...
...
@@ -293,7 +293,7 @@ by_part :
expr
:
simple
%
prec
error
{
$
1
}
|
simple
RELOP
simple
{
mkExpr
(
Binop
(
$
2
,
$
1
,
$
3
))
}
|
simple
EQUAL
simple
{
mkExpr
(
Binop
(
Eq
,
$
1
,
$
3
))
}
|
simple
EQUAL
simple
{
mkExpr
(
Binop
(
Eq
,
$
1
,
$
3
))
}
|
simple
IS
qualid
{
mkExpr
(
TypeTest
(
$
1
,
$
3
))
}
;
simple
:
...
...
@@ -314,16 +314,16 @@ factor :
|
DECIMAL
{
mkExpr
(
Decimal
$
1
)
}
|
FLOCON
{
mkExpr
(
Const
(
FloVal
$
1
,
realtype
))
}
|
DBLCON
{
mkExpr
(
Const
(
FloVal
$
1
,
longreal
))
}
|
CHAR
{
mkExpr
(
Const
(
IntVal
(
Int32
.
of_int
|
CHAR
{
mkExpr
(
Const
(
IntVal
(
Int32
.
of_int
(
int_of_char
$
1
))
,
character
))
}
|
STRING
{
mkExpr
(
String
(
save_string
$
1
,
|
STRING
{
mkExpr
(
String
(
save_string
$
1
,
String
.
length
$
1
))
}
|
NIL
{
mkExpr
Nil
}
|
designator
%
prec
error
{
$
1
}
|
LBRACE
RBRACE
{
mkExpr
(
Set
[]
)
}
|
LBRACE
elements
RBRACE
{
mkExpr
(
Set
$
2
)
}
|
NOT
factor
{
mkExpr
(
Monop
(
Not
,
fix
$
2
))
}
|
LPAR
expr
RPAR
{
$
2
}
|
LPAR
expr
RPAR
{
$
2
}
|
LPAR
expr
%
prec
error
{
parse_error2
"mismatched brackets"
(
rloc
1
);
raise
Parse_error
}
;
...
...
@@ -332,32 +332,32 @@ designator :
|
designator
UPARROW
{
mkExpr
(
Deref
$
1
)
}
|
designator
SUB
exprs
BUS
{
let
sub
a
i
=
mkExpr
(
Sub
(
a
,
i
))
in
List
.
fold_left
sub
$
1
$
3
}
|
designator
SUB
exprs
%
prec
error
|
designator
SUB
exprs
%
prec
error
{
parse_error2
"mismatched brackets"
(
rloc
2
);
raise
Parse_error
}
|
designator
DOT
name
{
mkExpr
(
Select
(
$
1
,
$
3
))
}
|
designator
actuals
{
mkExpr
(
FuncCall
(
$
1
,
$
2
))
}
;
actuals
:
actuals
:
LPAR
RPAR
{
[]
}
|
LPAR
exprs
RPAR
{
$
2
}
|
LPAR
exprs
%
prec
error
{
parse_error2
"mismatched brackets in procedure call"
|
LPAR
exprs
%
prec
error
{
parse_error2
"mismatched brackets in procedure call"
(
rloc
1
);
raise
Parse_error
}
;
exprs
:
exprs
:
expr
%
prec
error
{
[
$
1
]
}
|
expr
COMMA
exprs
{
$
1
::
$
3
}
;
typexpr
:
typexpr
:
typename
{
$
1
}
|
LPAR
defids
RPAR
{
mkTypexpr
(
Enum
$
2
)
}
|
POINTER
TO
typexpr
{
mkTypexpr
(
Pointer
$
3
)
}
|
ARRAY
exprs
OF
typexpr
{
let
array
n
t
=
mkTypexpr
(
Array
(
n
,
t
))
in
List
.
fold_right
array
$
2
$
4
}
|
ARRAY
OF
typexpr
{
mkTypexpr
(
Flex
$
3
)
}
|
absmark
RECORD
parent
fields
END
|
absmark
RECORD
parent
fields
END
{
mkTypexpr
(
Record
(
$
1
,
$
3
,
$
4
))
}
|
PROCEDURE
params
{
mkTypexpr
(
Proc
$
2
)
}
;
...
...
@@ -376,15 +376,15 @@ fields :
fieldlist
{
$
1
}
|
fieldlist
SEMI
fields
{
$
1
@
$
3
}
;
fieldlist
:
fieldlist
:
/*
empty
*/
{
[]
}
|
defids
COLON
typexpr
{
[
VarDecl
(
FieldDef
,
$
1
,
$
3
)]
}
;
qualid
:
qualid
:
IDENT
%
prec
DOT
{
makeName
(
!
current
,
$
1
,
lloc
()
)
}
|
IDENT
DOT
IDENT
{
makeName
(
$
1
,
$
3
,
lloc
()
)
};
name
:
name
:
IDENT
{
makeName
(
!
current
,
$
1
,
lloc
()
)
}
;
defids
:
...
...
test/bad/producer-with-a-positional-name.mly
View file @
1a96b802
%
start
<
unit
>
s
%
token
A
%%
s
:
A
_1
=
A
{
()
}
s
:
A
_1
=
A
{
()
}
test/bad/undefined-position.mly
View file @
1a96b802
%
start
<
int
>
a
%%
a
:
{
$
startpos
(
x
)
}
a
:
{
$
startpos
(
x
)
}
test/bad/undefined-producer.mly
View file @
1a96b802
%
start
<
int
>
a
%
start
<
int
>
a
%
token
A
%%
...
...
test/good/alphaCaml-demos-poplmark.mly
View file @
1a96b802
/*
/*
*
Parts
of
this
file
taken
from
the
fullfsub
implementation
*
by
the
POPLmark
team
.
*
...
...
@@ -68,9 +68,9 @@ Type :
/*
Atomic
types
are
those
that
never
need
extra
parentheses
*/
AType
:
|
LPAREN
Type
RPAREN
{
$
2
}
|
UCID
|
LPAREN
Type
RPAREN
{
$
2
}
|
UCID
{
TVar
$
1
}
|
TTOP
{
TTop
}
...
...
@@ -94,7 +94,7 @@ ArrowType :
Term
:
|
AppTerm
{
$
1
}
|
LAMBDA
LCID
COLON
Type
DOT
Term
|
LAMBDA
LCID
COLON
Type
DOT
Term
{
EAbs
(
$
2
,
$
4
,
$
6
)
}
|
LET
Pattern
EQ
Term
IN
Term
{
ELet
(
$
2
,
$
4
,
$
6
)
}
...
...
@@ -128,16 +128,16 @@ NEFieldTypes :
{
StringMap
.
add
$
1
$
3
$
5
}
TermSeq
:
|
Term
|
Term
{
$
1
}
|
Term
SEMI
TermSeq
|
Term
SEMI
TermSeq
{
ELet
(
PWildcard
,
$
1
,
$
3
)
}
/*
Atomic
terms
are
ones
that
never
require
extra
parentheses
*/
ATerm
:
|
LPAREN
TermSeq
RPAREN
{
$
2
}
|
LCID
|
LPAREN
TermSeq
RPAREN
{
$
2
}
|
LCID
{
EVar
$
1
}
|
LCURLY
Fields
RCURLY
{
ERecord
$
2
}
...
...
@@ -157,7 +157,7 @@ NEFields :
OType
:
|
/*
empty
*/
{
TTop
}
|
LEQ
Type
|
LEQ
Type
{
$
2
}
Pattern
:
...
...
test/good/alphaprolog.mly
View file @
1a96b802
/*
Yet
another
attempt
to
parse
nicely
.
This
parses
to
tree
-
structured
preterms
with
remaining
ambiguity
as
follows
:
1
.
Commas
might
be
either
pair
constructors
(
within
parens
inside
terms
)
or
and
-
constructors
1
.
Commas
might
be
either
pair
constructors
(
within
parens
inside
terms
)
or
and
-
constructors
(
outside
of
propositions
)
.
2
.
Identifiers
are
not
resolved
to
syntactic
classes
2
.
Identifiers
are
not
resolved
to
syntactic
classes
(
e
.
g
.
atom
,
variable
,
term
symbol
)
.
These
preterms
are
the
input
to
typechecking
,
These
preterms
are
the
input
to
typechecking
,
Typechecking
resolves
identifiers
to
variables
,
symbols
,
or
atoms
and
translates
propositions
to
goals
/
program
clauses
and
translates
terms
to
internal
terms
.
and
translates
propositions
to
goals
/
program
clauses
and
translates
terms
to
internal
terms
.
*/
%
{
open
Absyn
;;
...
...
@@ -17,9 +17,9 @@ open Nstbl;;
type
quantifier
=
QForall
|
QExists
|
QNew
;;
let
do_quantify
q
tvs
e
=
let
do_quantifier
q
(
tv
,
st
)
e
=
match
q
with
let
do_quantify
q
tvs
e
=
let
do_quantifier
q
(
tv
,
st
)
e
=
match
q
with
QForall
->
Forall
(
tv
,
st
,
e
)
|
QExists
->
Exists
(
tv
,
st
,
e
)
|
QNew
->
New
(
tv
,
st
,
e
)
...
...
@@ -27,9 +27,9 @@ let do_quantify q tvs e =
List
.
fold_right
(
do_quantifier
q
)
tvs
e
;;
let
do_literal'
s
t
=
let
do_literal'
s
t
=
let
n
=
String
.
length
s
in
let
rec
go
i
=
let
rec
go
i
=
if
i
=
n
then
t
else
Cons
(
CharC
(
String
.
get
s
i
)
,
go
(
i
+
1
))
in
go
0
...
...
@@ -43,47 +43,47 @@ type dcg_term = Nonterm of atomic | Char of char | Seq of dcg_term * dcg_term
;;
let
translate_dcg
(
hd
,
tl
)
t
=
let
rec
tr
t
x
y
=
match
t
with
let
translate_dcg
(
hd
,
tl
)
t
=
let
rec
tr
t
x
y
=
match
t
with
Char
c
->
Eq
(
Var
x
,
Cons
(
CharC
c
,
Var
y
))
|
Literal
s
->
Eq
(
Var
x
,
do_literal'
s
(
Var
y
))
|
Seq
(
t1
,
t2
)
->
|
Seq
(
t1
,
t2
)
->
let
w
=
Var
.
mkvar
"W"
in
And
(
tr
t1
x
w
,
tr
t2
w
y
)
|
Alt
(
t1
,
t2
)
->
|
Alt
(
t1
,
t2
)
->
Or
(
tr
t1
x
y
,
tr
t2
x
y
)
|
Goal
(
t
)
->
|
Goal
(
t
)
->
And
(
Eq
(
Var
x
,
Var
y
)
,
t
)
|
Nonterm
(
hd
,
tl
)
->
Atomic
(
hd
,
tl
@
[
Var
x
;
Var
y
])
in
|
Nonterm
(
hd
,
tl
)
->
Atomic
(
hd
,
tl
@
[
Var
x
;
Var
y
])
in
let
x
=
Var
.
mkvar
"X"
in
let
y
=
Var
.
mkvar
"Y"
in
Implies
(
tr
t
x
y
,
Atomic
(
hd
,
tl
@
[
Var
x
;
Var
y
]))
let
mk_toplevel_decl
rdecl
=
let
mk_toplevel_decl
rdecl
=
{
pos
=
None
;
rdecl
=
rdecl
}
;;
let
mk_decl
rdecl
=
let
mk_decl
rdecl
=
{
pos
=
Some
(
Pos
.
mk_pos
(
Lineno
.
filename
()
)
(
Lineno
.
lineno
()
));
rdecl
=
rdecl
}
;;
exception
Eof
;;
let
rec
kd_app
ks
k
=
let
rec
kd_app
ks
k
=
match
ks
with
[]
->
k
[]
->
k
|
k'
::
ks
->
ArrowK
(
k'
,
kd_app
ks
k
)
;;
let
rec
ty_app
ts
t
=
let
rec
ty_app
ts
t
=
match
ts
with
[]
->
t
[]
->
t
|
t'
::
ts
->
ArrowTy
(
t'
,
ty_app
ts
t
)
%
}
...
...
@@ -93,20 +93,20 @@ let rec ty_app ts t =
%
token
<
Nstbl
.
path
>
QUAL_ID
%
token
<
char
>
CHAR
%
token
USE
TRACE
QUIT
OPEN
TYPEQ
HELP
%
token
NAME_TYPE
TYPE
INFIXL
INFIXR
INFIXN
NAMESPACE
FUNC
PRED
CNST
%
token
NAME_TYPE
TYPE
INFIXL
INFIXR
INFIXN
NAMESPACE
FUNC
PRED
CNST
%
token
LPAREN
RPAREN
LBRACK
RBRACK
LBRACE
RBRACE
%
token
QUESTION
DOT
COLON
UNDERSCORE
TILDE
%
token
ARROW
DCG_ARROW
LARROW
DARROW
COMMA
SEMI
%
token
TRUE
NOT
CUT
BAR
HASH
SLASH
BACKSLASH
EQ
IS
%
token
FORALL
EXISTS
NEW
%
token
CONS
%
token
<
string
>
INFIXL1
INFIXL2
INFIXL3
INFIXL4
INFIXL5
%
token
TRUE
NOT
CUT
BAR
HASH
SLASH
BACKSLASH
EQ
IS
%
token
FORALL
EXISTS
NEW
%
token
CONS
%
token
<
string
>
INFIXL1
INFIXL2
INFIXL3
INFIXL4
INFIXL5
%
token
<
string
>
INFIXL6
INFIXL7
INFIXL8
INFIXL9
%
token
<
string
>
INFIXR1
INFIXR2
INFIXR3
INFIXR4
INFIXR5
%
token
<
string
>
INFIXR1
INFIXR2
INFIXR3
INFIXR4
INFIXR5
%
token
<
string
>
INFIXR6
INFIXR7
INFIXR8
INFIXR9
%
token
<
string
>
INFIXN1
INFIXN2
INFIXN3
INFIXN4
INFIXN5
%
token
<
string
>
INFIXN1
INFIXN2
INFIXN3
INFIXN4
INFIXN5
%
token
<
string
>
INFIXN6
INFIXN7
INFIXN8
INFIXN9
%
token
EOF
%
token
EOF
%
type
<
Absyn
.
decl
list
>
parse
parse_input_line
...
...
@@ -116,7 +116,7 @@ let rec ty_app ts t =
%
left
INFIXL1
%
right
INFIXR1
%
nonassoc
INFIXN1
%
right
ARROW
DARROW
%
right
ARROW
DARROW
%
left
LARROW
%
nonassoc
SLASH
%
nonassoc
BAR
...
...
@@ -136,11 +136,11 @@ let rec ty_app ts t =
%
nonassoc
INFIXN4
%
nonassoc
EQ
HASH
IS
/*
5
*/
%
left
INFIXL5
%
left
INFIXL5
%
right
INFIXR5
%
nonassoc
INFIXN5
/*
6
*/
%
left
INFIXL6
%
left
INFIXL6
%
right
INFIXR6
%
nonassoc
INFIXN6
%
right
CONS
...
...
@@ -157,7 +157,7 @@ let rec ty_app ts t =
%
right
INFIXR9
%
nonassoc
INFIXN9
/*
10
*/
%
right
BACKSLASH
%
right
BACKSLASH
%
start
parse
%
start
parse_input_line
...
...
@@ -187,19 +187,19 @@ decl : sig_decl { mk_decl $1}
|
directive
{
mk_decl
$
1
}
|
infix_decl
{
mk_decl
$
1
}
|
NAMESPACE
ID
LPAREN
decls
RPAREN
{
mk_decl
{
mk_decl
(
NamespaceDecl
(
$
2
,
List
.
rev
$
4
))
}
;
sig_decl
:
sig_decl
:
ID
COLON
kind
{
KindDecl
(
$
1
,$
3
)
}
|
ID
COLON
ty
{
SymDecl
(
$
1
,$
3
)
}
|
PRED
ID
ty0s
{
PredDecl
(
$
2
,
List
.
rev
$
3
)
}
|
CNST
ID
EQ
ty
{
FuncDecl
(
$
2
,
[]
,$
4
)
}
|
FUNC
ID
ty0s
EQ
ty
{
FuncDecl
(
$
2
,
List
.
rev
$
3
,
$
5
)
}
|
TYPE
ID
vars
EQ
ty
{
let
rvs
=
$
3
in
|
TYPE
ID
vars
EQ
ty
{
let
rvs
=
$
3
in
TypeDefn
(
$
2
,
List
.
rev
rvs
,$
5
)
}
;
...
...
@@ -208,7 +208,7 @@ vars : { [] }
|
vars
ID
{
Var
.
mkvar'
$
2
::$
1
}
;
kind
:
kind
:
TYPE
{
TypeK
}
|
NAME_TYPE
{
NameK
}
|
kind
ARROW
kind
{
ArrowK
(
$
1
,$
3
)
}
...
...
@@ -236,9 +236,9 @@ prog: preterm { $1 }
|
dcg_rule
{
$
1
}
;
dcg_rule
:
app_or_qid
DCG_ARROW
dcg_term
dcg_rule
:
app_or_qid
DCG_ARROW
dcg_term
{
translate_dcg
$
1
$
3
}
|
app_or_qid
DCG_ARROW
dcg_term
SLASH
constr
|
app_or_qid
DCG_ARROW
dcg_term
SLASH
constr
{
Constr
(
translate_dcg
$
1
$
3
,$
5
)
}
;
...
...
@@ -284,14 +284,14 @@ qual_id : QUAL_ID { $1 }
preterm0
:
LPAREN
preterm
RPAREN
{
$
2
}
|
qual_id
{
Atomic
(
$
1
,
[]
)
}
|
const
{
$
1
}
|
LBRACK
preterms_brack
RBRACK
{
List
.
fold_right
(
fun
x
y
->
Cons
(
x
,
y
))
|
LBRACK
preterms_brack
RBRACK
{
List
.
fold_right
(
fun
x
y
->
Cons
(
x
,
y
))
(
List
.
rev
$
2
)
Nil
}
|
LBRACK
preterms_brack
BAR
preterm_brack
RBRACK
{
List
.
fold_right
(
fun
x
y
->
Cons
(
x
,
y
))
|
LBRACK
preterms_brack
BAR
preterm_brack
RBRACK
{
List
.
fold_right
(
fun
x
y
->
Cons
(
x
,
y
))
(
List
.
rev
$
2
)
$
4
}