Commit a6d9f858 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

New test grammar.

parent ea8cc7d6
Warning: you are using the standard library and/or the %inline keyword. We
recommend switching on --infer in order to avoid obscure type error messages.
Grammar has 7 nonterminal symbols, among which 1 start symbols.
Grammar has 14 terminal symbols.
Grammar has 16 productions.
nullable(recursive) = true
nullable(left_associative_level(multiplicative_term_,ADDOP,mkbinop)) = false
nullable(left_associative_level(application_term_,MULOP,mkbinop)) = false
nullable(entry) = false
nullable(atomic_term_) = false
nullable(application_term_) = false
nullable(any_term_) = false
first(recursive) = REC
first(left_associative_level(multiplicative_term_,ADDOP,mkbinop)) = PRINT LPAREN INTLITERAL IDENT
first(left_associative_level(application_term_,MULOP,mkbinop)) = PRINT LPAREN INTLITERAL IDENT
first(entry) = PRINT LPAREN LET INTLITERAL IDENT FUN
first(atomic_term_) = LPAREN INTLITERAL IDENT
first(application_term_) = PRINT LPAREN INTLITERAL IDENT
first(any_term_) = PRINT LPAREN LET INTLITERAL IDENT FUN
follow(recursive) = IDENT
follow(left_associative_level(multiplicative_term_,ADDOP,mkbinop)) = RPAREN IN EOF ADDOP
follow(left_associative_level(application_term_,MULOP,mkbinop)) = RPAREN MULOP IN EOF ADDOP
follow(entry) = #
follow(atomic_term_) = RPAREN MULOP LPAREN INTLITERAL IN IDENT EOF ADDOP
follow(application_term_) = RPAREN MULOP LPAREN INTLITERAL IN IDENT EOF ADDOP
follow(any_term_) = RPAREN IN EOF
Built an LR(0) automaton with 32 states.
The grammar is SLR(1).
Built an LR(1) automaton with 32 states.
11 out of 32 states have a default reduction.
10 out of 32 states are represented.
11 out of 24 symbols keep track of their start position.
8 out of 24 symbols keep track of their end position.
9 out of 17 productions exploit shiftreduce optimization.
0 out of 32 states can peek at an error.
94 functions before inlining, 17 functions after inlining.
%token<string> IDENT
%token<int> INTLITERAL
%token FUN IN LET PRINT REC
%token ARROW EQ LPAREN RPAREN
%token<RawLambda.binop> MULOP ADDOP
%token EOF
%start<RawLambda.term> entry
%{
open RawLambda
%}
%%
(* -------------------------------------------------------------------------- *)
(* A toplevel phrase is just a term. *)
entry:
t = any_term EOF
{ t }
(* -------------------------------------------------------------------------- *)
(* The syntax of terms is stratified as follows:
atomic_term -- unambiguously delimited terms
application_term -- n-ary applications of atomic terms
multiplicative_term -- built using multiplication & division
additive_term -- built using addition & subtraction
any_term -- everything
A [match/with/end] construct is terminated with an [end] keyword, as in Coq,
so it is an atomic term. *)
atomic_term_:
| LPAREN t = any_term RPAREN
{ t.value }
| x = IDENT
{ Var x }
| i = INTLITERAL
{ Lit i }
application_term_:
| t = atomic_term_
{ t }
| t1 = placed(application_term_) t2 = placed(atomic_term_)
{ App (t1, t2) }
| PRINT t2 = placed(atomic_term_)
{ Print t2 }
%inline multiplicative_term_:
t = left_associative_level(application_term_, MULOP, mkbinop)
{ t }
%inline additive_term_:
t = left_associative_level(multiplicative_term_, ADDOP, mkbinop)
{ t }
any_term_:
| t = additive_term_
{ t }
| FUN x = IDENT ARROW t = any_term
{ Lam (x, t) }
| LET mode = recursive x = IDENT EQ t1 = any_term IN t2 = any_term
{ Let (mode, x, t1, t2) }
%inline any_term:
t = placed(any_term_)
{ t }
(* -------------------------------------------------------------------------- *)
(* An infix-left-associative-operator level in a hierarchy of arithmetic
expressions. *)
(* [basis] is the next lower level in the hierarchy.
[op] is the category of binary operators.
[action] is a ternary sequencing construct. *)
left_associative_level(basis, op, action):
| t = basis
| t = action(
left_associative_level(basis, op, action),
op,
basis
)
{ t }
(* -------------------------------------------------------------------------- *)
(* A ternary sequence whose semantic action builds a [BinOp] node. *)
%inline mkbinop(term1, op, term2):
t1 = placed(term1) op = op t2 = placed(term2)
{ BinOp (t1, op, t2) }
(* -------------------------------------------------------------------------- *)
(* A [let] construct carries an optional [rec] annotation. *)
recursive:
| REC { Recursive }
| { NonRecursive }
(* -------------------------------------------------------------------------- *)
(* A term is annotated with its start and end positions, for use in error
messages. *)
%inline placed(X):
x = X
{ { place = ($startpos, $endpos); value = x } }
(* -------------------------------------------------------------------------- *)
(* In a right-flexible list, the last delimiter is optional, i.e., [delim] can
be viewed as a terminator or a separator, as desired. *)
(* There are several ways of expressing this. One could say it is either a
separated list or a terminated list; this works if one uses right recursive
lists. Or, one could say that it is a separated list followed with an
optional delimiter; this works if one uses a left-recursive list. The
following formulation is direct and seems most natural. It should lead to
the smallest possible automaton. *)
right_flexible_list(delim, X):
| (* nothing *)
{ [] }
| x = X
{ [x] }
| x = X delim xs = right_flexible_list(delim, X)
{ x :: xs }
(* In a left-flexible list, the first delimiter is optional, i.e., [delim] can
be viewed as an opening or as a separator, as desired. *)
(* Again, there are several ways of expressing this, and again, I suppose the
following formulation is simplest. It is the mirror image of the above
definition, so it is naturally left-recursive, this time. *)
reverse_left_flexible_list(delim, X):
| (* nothing *)
{ [] }
| x = X
{ [x] }
| xs = reverse_left_flexible_list(delim, X) delim x = X
{ x :: xs }
%inline left_flexible_list(delim, X):
xs = reverse_left_flexible_list(delim, X)
{ List.rev xs }
Warning: you are using the standard library and/or the %inline keyword. We
recommend switching on --infer in order to avoid obscure type error messages.
%{
open RawLambda
%}
%start entry
%token <RawLambda.binop> ADDOP
%token ARROW
%token EOF
%token EQ
%token FUN
%token <string> IDENT
%token IN
%token <int> INTLITERAL
%token LET
%token LPAREN
%token <RawLambda.binop> MULOP
%token PRINT
%token REC
%token RPAREN
%type <RawLambda.term> entry
%%
entry:
x00 = any_term_ _2 = EOF
{let t =
let _endpos_x0_ = _endpos_x00_ in
let _startpos_x0_ = _startpos_x00_ in
let x0 = x00 in
let t =
let _endpos_x_ = _endpos_x0_ in
let _startpos_x_ = _startpos_x0_ in
let x = x0 in
let _endpos = _endpos_x_ in
let _startpos = _startpos_x_ in
( { place = (_startpos, _endpos); value = x } )
in
( t )
in
( t )}
atomic_term_:
_1 = LPAREN x00 = any_term_ _3 = RPAREN
{let t =
let _endpos_x0_ = _endpos_x00_ in
let _startpos_x0_ = _startpos_x00_ in
let x0 = x00 in
let t =
let _endpos_x_ = _endpos_x0_ in
let _startpos_x_ = _startpos_x0_ in
let x = x0 in
let _endpos = _endpos_x_ in
let _startpos = _startpos_x_ in
( { place = (_startpos, _endpos); value = x } )
in
( t )
in
( t.value )}
| x = IDENT
{ ( Var x )}
| i = INTLITERAL
{ ( Lit i )}
application_term_:
t = atomic_term_
{ ( t )}
| x0 = application_term_ x1 = atomic_term_
{let t2 =
let _endpos_x_ = _endpos_x1_ in
let _startpos_x_ = _startpos_x1_ in
let x = x1 in
let _endpos = _endpos_x_ in
let _startpos = _startpos_x_ in
( { place = (_startpos, _endpos); value = x } )
in
let t1 =
let _endpos_x_ = _endpos_x0_ in
let _startpos_x_ = _startpos_x0_ in
let x = x0 in
let _endpos = _endpos_x_ in
let _startpos = _startpos_x_ in
( { place = (_startpos, _endpos); value = x } )
in
( App (t1, t2) )}
| _1 = PRINT x0 = atomic_term_
{let t2 =
let _endpos_x_ = _endpos_x0_ in
let _startpos_x_ = _startpos_x0_ in
let x = x0 in
let _endpos = _endpos_x_ in
let _startpos = _startpos_x_ in
( { place = (_startpos, _endpos); value = x } )
in
( Print t2 )}
any_term_:
t0 = left_associative_level_multiplicative_term__ADDOP_mkbinop_
{let t =
let t = t0 in
( t )
in
( t )}
| _1 = FUN x = IDENT _3 = ARROW x00 = any_term_
{let t =
let _endpos_x0_ = _endpos_x00_ in
let _startpos_x0_ = _startpos_x00_ in
let x0 = x00 in
let t =
let _endpos_x_ = _endpos_x0_ in
let _startpos_x_ = _startpos_x0_ in
let x = x0 in
let _endpos = _endpos_x_ in
let _startpos = _startpos_x_ in
( { place = (_startpos, _endpos); value = x } )
in
( t )
in
( Lam (x, t) )}
| _1 = LET mode = recursive x = IDENT _4 = EQ x00 = any_term_ _6 = IN x01 = any_term_
{let t2 =
let _endpos_x0_ = _endpos_x01_ in
let _startpos_x0_ = _startpos_x01_ in
let x0 = x01 in
let t =
let _endpos_x_ = _endpos_x0_ in
let _startpos_x_ = _startpos_x0_ in
let x = x0 in
let _endpos = _endpos_x_ in
let _startpos = _startpos_x_ in
( { place = (_startpos, _endpos); value = x } )
in
( t )
in
let t1 =
let _endpos_x0_ = _endpos_x00_ in
let _startpos_x0_ = _startpos_x00_ in
let x0 = x00 in
let t =
let _endpos_x_ = _endpos_x0_ in
let _startpos_x_ = _startpos_x0_ in
let x = x0 in
let _endpos = _endpos_x_ in
let _startpos = _startpos_x_ in
( { place = (_startpos, _endpos); value = x } )
in
( t )
in
( Let (mode, x, t1, t2) )}
left_associative_level_application_term__MULOP_mkbinop_:
t = application_term_
{ ( t )}
| x00 = left_associative_level_application_term__MULOP_mkbinop_ op0 = MULOP x10 = application_term_
{let t =
let _endpos_x1_ = _endpos_x10_ in
let _startpos_x1_ = _startpos_x10_ in
let _endpos_x0_ = _endpos_x00_ in
let _startpos_x0_ = _startpos_x00_ in
let x1 = x10 in
let op = op0 in
let x0 = x00 in
let t2 =
let _endpos_x_ = _endpos_x1_ in
let _startpos_x_ = _startpos_x1_ in
let x = x1 in
let _endpos = _endpos_x_ in
let _startpos = _startpos_x_ in
( { place = (_startpos, _endpos); value = x } )
in
let t1 =
let _endpos_x_ = _endpos_x0_ in
let _startpos_x_ = _startpos_x0_ in
let x = x0 in
let _endpos = _endpos_x_ in
let _startpos = _startpos_x_ in
( { place = (_startpos, _endpos); value = x } )
in
( BinOp (t1, op, t2) )
in
( t )}
left_associative_level_multiplicative_term__ADDOP_mkbinop_:
t0 = left_associative_level_application_term__MULOP_mkbinop_
{let t =
let t = t0 in
( t )
in
( t )}
| x00 = left_associative_level_multiplicative_term__ADDOP_mkbinop_ op0 = ADDOP t000 = left_associative_level_application_term__MULOP_mkbinop_
{let t =
let _endpos_x0_ = _endpos_x00_ in
let _startpos_x0_ = _startpos_x00_ in
let _endpos_t00_ = _endpos_t000_ in
let _startpos_t00_ = _startpos_t000_ in
let t00 = t000 in
let op = op0 in
let x0 = x00 in
let t2 =
let _endpos_t0_ = _endpos_t00_ in
let _startpos_t0_ = _startpos_t00_ in
let t0 = t00 in
let x =
let t = t0 in
( t )
in
let _endpos_x_ = _endpos_t0_ in
let _startpos_x_ = _startpos_t0_ in
let _endpos = _endpos_x_ in
let _startpos = _startpos_x_ in
( { place = (_startpos, _endpos); value = x } )
in
let t1 =
let _endpos_x_ = _endpos_x0_ in
let _startpos_x_ = _startpos_x0_ in
let x = x0 in
let _endpos = _endpos_x_ in
let _startpos = _startpos_x_ in
( { place = (_startpos, _endpos); value = x } )
in
( BinOp (t1, op, t2) )
in
( t )}
recursive:
_1 = REC
{ ( Recursive )}
|
{ ( NonRecursive )}
%%
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment