%{
Require Import Cabs.
Require Import List.
Require Import Maps.
Require Import Streams.

Section DelayedMonad.

Inductive name_type : Type :=
  Typedef | Var.

Definition env := 
  PTree.tree name_type.

Inductive outcome (out:Type) : Type :=
  | Fail : outcome out
  | Timeout : outcome out
  | Success : env -> out -> outcome out.

Variable term: Type.
Variable terminal_semantic_type: term -> Type.

Definition parsing_routine (out:Type) :=
  Stream (sigT terminal_semantic_type) -> env -> outcome out.

Record parsing_routines: Type := {
  declaration_or_expression_pr : parsing_routine (definition + (expression * cabsloc) + unit);
  expression_pr : parsing_routine (expression * cabsloc);
  c_initializer_pr : parsing_routine init_expression;
  expression_option_pr : parsing_routine (option (expression * cabsloc));
  constant_expression_pr : parsing_routine (expression * cabsloc);
  type_qualifier_list_assignment_expression_pr : parsing_routine (list cvspec * option expression);
  parameter_declaration_abstract_declarator_pr : parsing_routine parameter;
  parameter_declaration_declarator_pr : parsing_routine parameter
}.

Definition delayed (out:Type) : Type :=
  parsing_routines -> env -> outcome out.

Definition bind {A B:Type} (v:delayed A) (f:A -> delayed B): delayed B :=
  (fun rec env =>
    match v rec env with
      | Fail => Fail _
      | Timeout => Timeout _
      | Success env out => (f out) rec env
    end).

Definition ret {out:Type} (v:out): delayed out :=
  fun rec env => Success _ env v.

Definition try {out:Type} (v1 v2:delayed out): delayed out :=
  (fun rec env =>
    match v1 rec env with
      | Fail => v2 rec env
      | Timeout => Timeout _
      | Success env out => Success _ env out
    end).

Definition in_scope {out:Type} (v:delayed out): delayed out :=
  (fun rec env =>
    match v rec env with
      | Fail => Fail _
      | Timeout => Timeout _
      | Success _ out => Success _ env out
    end).

Definition bind_identifier (n:atom) (nt:name_type) : delayed unit :=
  (fun rec env => Success _ (PTree.set n nt env) tt).

Definition call_parsing_routine {out:Type}
  (routine:parsing_routines -> parsing_routine out) (chunk:Stream (sigT terminal_semantic_type))
  : delayed out :=
  fun rec => routine rec chunk.

End DelayedMonad.

Implicit Arguments parsing_routine [[term]].
Implicit Arguments parsing_routines [[term]].
Implicit Arguments delayed [[term]].
Implicit Arguments bind [[term] [terminal_semantic_type] [A] [B]].
Implicit Arguments ret [[term] [terminal_semantic_type] [out]].
Implicit Arguments try [[term] [terminal_semantic_type] [out]].
Implicit Arguments bind_identifier [[term] [terminal_semantic_type]].
Implicit Arguments in_scope [[term] [terminal_semantic_type] [out]].
Implicit Arguments call_parsing_routine [[term] [terminal_semantic_type] [out]].
Implicit Arguments declaration_or_expression_pr [[term] [terminal_semantic_type]].
Implicit Arguments expression_pr [[term] [terminal_semantic_type]].
Implicit Arguments c_initializer_pr [[term] [terminal_semantic_type]].
Implicit Arguments expression_option_pr [[term] [terminal_semantic_type]].
Implicit Arguments constant_expression_pr [[term] [terminal_semantic_type]].
Implicit Arguments type_qualifier_list_assignment_expression_pr [[term] [terminal_semantic_type]].
Implicit Arguments parameter_declaration_abstract_declarator_pr [[term] [terminal_semantic_type]].
Implicit Arguments parameter_declaration_declarator_pr [[term] [terminal_semantic_type]].

Notation "'do' X <- A ; B" := (bind A (fun X => B))
  (at level 200, X ident, A at level 100, B at level 200).

(* Returns Typedef if it does, and Var if it does not (that is, it returns the
   name_type corresponding to the declaration. *)
Fixpoint contains_typedef (lst:list spec_elem) : name_type :=
  match lst with
    | nil => Var
    | SpecStorage TYPEDEF::_ => Typedef
    | _::q => contains_typedef q
  end.

Fixpoint bind_function_parameters (decl:decl_type) (env:env) :=
  match decl with
    | PROTO JUSTBASE (plist, _) =>
      fold_left (fun acc param =>
	  match param with
	    | PARAM _ (Some a) _ _ _ => 
	      PTree.set a Var acc
            | _ => acc
          end) plist env
    | JUSTBASE => env
    | ARRAY decl2 _ _ _ => bind_function_parameters decl2 env
    | PTR _ _ decl2 => bind_function_parameters decl2 env
    | PROTO decl2 _ => bind_function_parameters decl2 env
  end.

Definition do_bind_function_parameters {term:Type} {terminal_semantic_type:term -> Type} 
                                       (decl:decl_type) : delayed terminal_semantic_type unit :=
  (fun rec env => Success _ (bind_function_parameters decl env) tt).

Extraction Inline bind ret try bind_identifier in_scope call_parsing_routine.

Parameter func_atom : atom.

%}

%token<atom * cabsloc> VAR_NAME TYPEDEF_NAME UNKNOWN_NAME BUILTIN
%token<atom * cabsloc> PRAGMA
%token<constant * cabsloc> LITERAL
%token<atom * cabsloc> STRING_LITERAL
%token<cabsloc> SIZEOF PTR INC DEC LEFT RIGHT LEQ GEQ EQEQ EQ NEQ LT GT
  ANDAND BARBAR PLUS MINUS STAR TILDE BANG SLASH PERCENT HAT BAR QUESTION
  COLON AND ALIGNOF

%token<cabsloc> MUL_ASSIGN DIV_ASSIGN MOD_ASSIGN ADD_ASSIGN SUB_ASSIGN
  LEFT_ASSIGN RIGHT_ASSIGN AND_ASSIGN XOR_ASSIGN OR_ASSIGN

%token<cabsloc> LPAREN RPAREN LBRACK RBRACK LBRACE RBRACE DOT COMMA
  SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT AUTO REGISTER INLINE
  CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE CONST VOLATILE VOID STRUCT
  UNION ENUM BOOL

%token<cabsloc> CASE DEFAULT IF ELSE SWITCH WHILE DO FOR GOTO CONTINUE BREAK
  RETURN BUILTIN_VA_ARG

%token EOF

%type<list atom (* Reverse order *) * cabsloc>
  string_literal
%type<constant * cabsloc>
  constant
%type<unary_operator * cabsloc>
  unary_operator
%type<binary_operator>
  assignment_operator
%type<delayed terminal_semantic_type (expression * cabsloc)>
  primary_expression postfix_expression unary_expression cast_expression
  multiplicative_expression additive_expression shift_expression
  relational_expression equality_expression AND_expression
  exclusive_OR_expression inclusive_OR_expression logical_AND_expression
  logical_OR_expression conditional_expression assignment_expression
  constant_expression expression expression_eof constant_expression_eof
%type<delayed terminal_semantic_type (list expression (* Reverse order *))>
  argument_expression_list
%type<delayed terminal_semantic_type definition>
  declaration_no_semicolon(identifier) declaration_no_semicolon(TYPEDEF_NAME)
  external_declaration function_definition
%type<delayed terminal_semantic_type (list spec_elem)>
  specifier_qualifier_list_notypedef declaration_specifiers_notypedef 
%type<delayed terminal_semantic_type (list spec_elem * cabsloc)>
  specifier_qualifier_list(identifier)  declaration_specifiers(identifier)
  specifier_qualifier_list(TYPEDEF_NAME)   declaration_specifiers(TYPEDEF_NAME)
%type<name_type -> delayed terminal_semantic_type (list init_name (* Reverse order *))>
  init_declarator_list
%type<name_type -> delayed terminal_semantic_type init_name>
  init_declarator
%type<storage * cabsloc>
  storage_class_specifier
%type<delayed terminal_semantic_type (typeSpecifier * cabsloc)>
  type_specifier struct_or_union_specifier enum_specifier
%type<structOrUnion * cabsloc>
  struct_or_union
%type<delayed terminal_semantic_type (list field_group (* Reverse order *))>
  struct_declaration_list
%type<delayed terminal_semantic_type field_group>
  struct_declaration
%type<delayed terminal_semantic_type (list (option name * option expression) (* Reverse order *))>
  struct_declarator_list
%type<delayed terminal_semantic_type (option name * option expression)>
  struct_declarator
%type<delayed terminal_semantic_type (list (atom * option expression * cabsloc) (* Reverse order *))>
  enumerator_list
%type<delayed terminal_semantic_type (atom * option expression * cabsloc)>
  enumerator
%type<cvspec * cabsloc>
  type_qualifier
%type<cabsloc>
  function_specifier
%type<delayed terminal_semantic_type name>
  declarator direct_declarator
%type<(decl_type -> decl_type) * cabsloc>
  pointer
%type<list cvspec (* Reverse order *)> 
  type_qualifier_list
%type<delayed terminal_semantic_type (list parameter * bool)>
  parameter_type_list
%type<delayed terminal_semantic_type (list parameter (* Reverse order *))>
  parameter_list
%type<delayed terminal_semantic_type parameter>
  parameter_declaration
  parameter_declaration_abstract_declarator parameter_declaration_declarator
  parameter_declaration_abstract_declarator_eof parameter_declaration_declarator_eof
%type<delayed terminal_semantic_type (list spec_elem * decl_type)>
  type_name
%type<delayed terminal_semantic_type decl_type>
  abstract_declarator direct_abstract_declarator option_direct_abstract_declarator
%type<delayed terminal_semantic_type init_expression>
  c_initializer c_initializer_eof
%type<delayed terminal_semantic_type (list (list initwhat * init_expression) (* Reverse order *))>
  initializer_list
%type<delayed terminal_semantic_type (list initwhat)>
  designation
%type<delayed terminal_semantic_type (list initwhat (* Reverse order *))>
  designator_list
%type<delayed terminal_semantic_type initwhat>
  designator
%type<delayed terminal_semantic_type statement>
  labeled_statement(statement_safe) labeled_statement(statement_dangerous)
  iteration_statement(statement_safe) iteration_statement(statement_dangerous)
  compound_statement block_item selection_statement_dangerous
  selection_statement_safe jump_statement
%type<bool -> delayed terminal_semantic_type statement(* The bool parameter is true when the statement can be a declaration *)>
  statement_dangerous statement_safe expression_or_declaration_statement
%type<delayed terminal_semantic_type (list statement (* Reverse order *))>
  block_item_list
%type<delayed terminal_semantic_type (list definition)>
  translation_unit(* Reverse order *) translation_unit_file
%type<atom * cabsloc>
  identifier
%type<delayed terminal_semantic_type (sigT terminal_semantic_type)>
  parameter_declaration_first innocent_list_token innocent_token internal_token identifier_token
%type<Stream (sigT terminal_semantic_type) -> delayed terminal_semantic_type (Stream (sigT terminal_semantic_type))>
  delayed_chunk_internal delayed_chunk_innocent_list delayed_chunk_nonbracebegin(innocent_token)
  delayed_chunk_nonbracebegin(internal_token) delayed_chunk_nonbracebegin(innocent_list_token)
  delayed_chunk(internal_token) delayed_chunk(innocent_list_token) delayed_chunk(innocent_token)
%type<delayed terminal_semantic_type (definition + (expression * cabsloc) + unit)>
  declaration_or_expression_eof
%type<delayed terminal_semantic_type (option (expression * cabsloc))>
  expression_option_eof
%type<delayed terminal_semantic_type (list cvspec * option expression)>
  type_qualifier_list_assignment_expression_eof

%start translation_unit_file declaration_or_expression_eof expression_eof
  c_initializer_eof expression_option_eof constant_expression_eof
  type_qualifier_list_assignment_expression_eof
  parameter_declaration_abstract_declarator_eof parameter_declaration_declarator_eof

%%

declaration_or_expression_eof:
| decl = declaration_no_semicolon(TYPEDEF_NAME) EOF
    { do decl <- decl;
      ret (inl _ (inl _ decl)) }
| expr = expression EOF
    { do expr <- expr;
      ret (inl _ (inr _ expr)) }
| EOF
    { ret (inr tt) }

type_qualifier_list_assignment_expression_eof:
| qual_lst = type_qualifier_list expr = assignment_expression EOF
    { do expr <- expr;
      ret (rev' qual_lst, Some (fst expr)) }
| qual_lst = type_qualifier_list EOF
    { ret (rev' qual_lst, None) }
| expr = assignment_expression EOF
    { do expr <- expr;
      ret ([], Some (fst expr)) }
| EOF
    { ret ([], None) }

expression_eof:
| expr = expression EOF
    { expr }

expression_option_eof:
| expr = expression EOF
    { do expr <- expr;
      ret (Some expr) }
| EOF
    { ret None }

constant_expression_eof:
| expr = constant_expression EOF
    { expr }

parameter_declaration_abstract_declarator_eof:
| param = parameter_declaration_abstract_declarator EOF
    { param }

parameter_declaration_declarator_eof:
| param = parameter_declaration_declarator EOF
    { param }

c_initializer_eof:
| init = c_initializer EOF
    { init }

identifier:
| i = VAR_NAME
| i = TYPEDEF_NAME
| i = UNKNOWN_NAME
    { i }

identifier_token:
| i = VAR_NAME
| i = TYPEDEF_NAME
| i = UNKNOWN_NAME
    { fun _ env =>
	Success _ env (
          match PTree.get (fst i) env with
            | Some Typedef => existT _ TYPEDEF_NAME_t i
            | Some Var => existT _ VAR_NAME_t i
            | None => existT _ UNKNOWN_NAME_t i
	  end)
    }

parameter_declaration_first:
| d = TYPEDEF          { ret (existT _ TYPEDEF_t d) }
| d = EXTERN           { ret (existT _ EXTERN_t d) }
| d = STATIC           { ret (existT _ STATIC_t d) }
| d = AUTO             { ret (existT _ AUTO_t d) }
| d = REGISTER         { ret (existT _ REGISTER_t d) }
| d = VOID             { ret (existT _ VOID_t d) }
| d = CHAR             { ret (existT _ CHAR_t d) }
| d = SHORT            { ret (existT _ SHORT_t d) }
| d = INT              { ret (existT _ INT_t d) }
| d = LONG             { ret (existT _ LONG_t d) }
| d = FLOAT            { ret (existT _ FLOAT_t d) }
| d = DOUBLE           { ret (existT _ DOUBLE_t d) }
| d = SIGNED           { ret (existT _ SIGNED_t d) }
| d = UNSIGNED         { ret (existT _ UNSIGNED_t d) }
| d = BOOL             { ret (existT _ BOOL_t d) }
| d = STRUCT           { ret (existT _ STRUCT_t d) }
| d = UNION            { ret (existT _ UNION_t d) }
| d = ENUM             { ret (existT _ ENUM_t d) }
| d = CONST            { ret (existT _ CONST_t d) }
| d = RESTRICT         { ret (existT _ RESTRICT_t d) }
| d = VOLATILE         { ret (existT _ VOLATILE_t d) }
| d = INLINE           { ret (existT _ INLINE_t d) }
| d = BUILTIN          { ret (existT _ BUILTIN_t d) }
| t = identifier_token { t }

(* Every terminal except: 
     COMMA ELLIPSIS LPAREN RPAREN LBRACK RBRACK LBRACE 
     RBRACE QUESTION COLON PRAGMA SEMICOLON
     CASE DEFAULT IF ELSE SWITCH WHILE DO FOR GOTO CONTINUE
     BREAK RETURN EOF *)
innocent_token:
| d = LITERAL         { ret (existT _ LITERAL_t d) }
| d = STRING_LITERAL  { ret (existT _ STRING_LITERAL_t d) }
| d = SIZEOF           { ret (existT _ SIZEOF_t d) }
| d = PTR              { ret (existT _ PTR_t d) }
| d = INC              { ret (existT _ INC_t d) }
| d = DEC              { ret (existT _ DEC_t d) }
| d = LEFT             { ret (existT _ LEFT_t d) }
| d = RIGHT            { ret (existT _ RIGHT_t d) }
| d = LEQ              { ret (existT _ LEQ_t d) }
| d = GEQ              { ret (existT _ GEQ_t d) }
| d = EQEQ             { ret (existT _ EQEQ_t d) }
| d = EQ               { ret (existT _ EQ_t d) }
| d = NEQ              { ret (existT _ NEQ_t d) }
| d = LT               { ret (existT _ LT_t d) }
| d = GT               { ret (existT _ GT_t d) }
| d = ANDAND           { ret (existT _ ANDAND_t d) }
| d = BARBAR           { ret (existT _ BARBAR_t d) }
| d = PLUS             { ret (existT _ PLUS_t d) }
| d = MINUS            { ret (existT _ MINUS_t d) }
| d = STAR             { ret (existT _ STAR_t d) }
| d = TILDE            { ret (existT _ TILDE_t d) }
| d = BANG             { ret (existT _ BANG_t d) }
| d = SLASH            { ret (existT _ SLASH_t d) }
| d = PERCENT          { ret (existT _ PERCENT_t d) }
| d = HAT              { ret (existT _ HAT_t d) }
| d = DOT              { ret (existT _ DOT_t d) }
| d = BAR              { ret (existT _ BAR_t d) }
| d = AND              { ret (existT _ AND_t d) }
| d = ALIGNOF          { ret (existT _ ALIGNOF_t d) }
| d = MUL_ASSIGN       { ret (existT _ MUL_ASSIGN_t d) }
| d = DIV_ASSIGN       { ret (existT _ DIV_ASSIGN_t d) }
| d = MOD_ASSIGN       { ret (existT _ MOD_ASSIGN_t d) }
| d = ADD_ASSIGN       { ret (existT _ ADD_ASSIGN_t d) }
| d = SUB_ASSIGN       { ret (existT _ SUB_ASSIGN_t d) }
| d = LEFT_ASSIGN      { ret (existT _ LEFT_ASSIGN_t d) }
| d = RIGHT_ASSIGN     { ret (existT _ RIGHT_ASSIGN_t d) }
| d = AND_ASSIGN       { ret (existT _ AND_ASSIGN_t d) }
| d = XOR_ASSIGN       { ret (existT _ XOR_ASSIGN_t d) }
| d = OR_ASSIGN        { ret (existT _ OR_ASSIGN_t d) }
| d = TYPEDEF          { ret (existT _ TYPEDEF_t d) }
| d = EXTERN           { ret (existT _ EXTERN_t d) }
| d = STATIC           { ret (existT _ STATIC_t d) }
| d = RESTRICT         { ret (existT _ RESTRICT_t d) }
| d = AUTO             { ret (existT _ AUTO_t d) }
| d = REGISTER         { ret (existT _ REGISTER_t d) }
| d = INLINE           { ret (existT _ INLINE_t d) }
| d = CHAR             { ret (existT _ CHAR_t d) }
| d = SHORT            { ret (existT _ SHORT_t d) }
| d = INT              { ret (existT _ INT_t d) }
| d = LONG             { ret (existT _ LONG_t d) }
| d = SIGNED           { ret (existT _ SIGNED_t d) }
| d = UNSIGNED         { ret (existT _ UNSIGNED_t d) }
| d = FLOAT            { ret (existT _ FLOAT_t d) }
| d = DOUBLE           { ret (existT _ DOUBLE_t d) }
| d = CONST            { ret (existT _ CONST_t d) }
| d = VOLATILE         { ret (existT _ VOLATILE_t d) }
| d = VOID             { ret (existT _ VOID_t d) }
| d = STRUCT           { ret (existT _ STRUCT_t d) }
| d = UNION            { ret (existT _ UNION_t d) }
| d = ENUM             { ret (existT _ ENUM_t d) }
| d = BOOL             { ret (existT _ BOOL_t d) }
| d = BUILTIN_VA_ARG   { ret (existT _ BUILTIN_VA_ARG_t d) }
| d = BUILTIN          { ret (existT _ BUILTIN_t d) }
| t = identifier_token { t }

innocent_list_token:
| t = innocent_token   { t }
| d = COMMA            { ret (existT _ COMMA_t d) }
| d = ELLIPSIS         { ret (existT _ ELLIPSIS_t d) }

internal_token:
| t = innocent_list_token
                       { t }
| d = SEMICOLON        { ret (existT _ SEMICOLON_t d) }
| d = COLON            { ret (existT _ COLON_t d) }

delayed_chunk_nonbracebegin(token):
| (* Empty *)
    { fun s => ret s }
| t = token q = delayed_chunk(token)
    { fun s => 
        do t <- t;
        do q <- q s;
	ret (Cons t q) }
| quest = QUESTION c1 = delayed_chunk_innocent_list colon = COLON c2 = delayed_chunk(token)
    { fun s => 
        do c2 <- c2 s;
        do c1 <- c1 (Cons (existT _ COLON_t colon) c2);
        ret (Cons (existT _ QUESTION_t quest) c1) }
| lparen = LPAREN c1 = delayed_chunk_internal rparen = RPAREN c2 = delayed_chunk(token)
    { fun s =>
        do c2 <- c2 s;
        do c1 <- c1 (Cons (existT _ RPAREN_t rparen) c2);
        ret (Cons (existT _ LPAREN_t lparen) c1) }
| lbrack = LBRACK c1 = delayed_chunk_internal rbrack = RBRACK c2 = delayed_chunk(token)
    { fun s => 
        do c2 <- c2 s;
        do c1 <- c1 (Cons (existT _ RBRACK_t rbrack) c2);
        ret (Cons (existT _ LBRACK_t lbrack) c1) }

delayed_chunk(token):
| c = delayed_chunk_nonbracebegin(token)
    { c }
| lbrace = LBRACE c1 = delayed_chunk_internal rbrace = RBRACE c2 = delayed_chunk(token)
    { fun s => 
        do c2 <- c2 s;
        do c1 <- c1 (Cons (existT _ RBRACE_t rbrace) c2);
        ret (Cons (existT _ LBRACE_t lbrace) c1) }

delayed_chunk_internal:
| c = delayed_chunk(internal_token)
    { c }

delayed_chunk_innocent_list:
| c = delayed_chunk(innocent_list_token)
    { c }

string_literal:
| s = STRING_LITERAL
    { ([fst s], snd s) }
| q = string_literal t = STRING_LITERAL
    { (fst t::fst q, snd q) }

constant:
| l = string_literal
    { (CONST_STRING (rev' (fst l)), snd l) }
| l = LITERAL
    { l }

(* Actual grammar *)
(* 6.5.1 *)

(* Known context *)
primary_expression:
| i = VAR_NAME
| i = BUILTIN
    { ret (VARIABLE (fst i), snd i) }
| c = constant
    { ret (CONSTANT (fst c), snd c) }
| loc = LPAREN expr = expression RPAREN
    { do expr <- expr;
      ret (fst expr, loc) }

(* 6.5.2 *)
(* Known context *)
postfix_expression:
| expr = primary_expression
    { expr }
| expr1 = postfix_expression LBRACK expr2 = expression RBRACK
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (INDEX (fst expr1) (fst expr2), snd expr1) }
| expr = postfix_expression LPAREN args = argument_expression_list RPAREN
    { do expr <- expr;
      do args <- args;
      ret (CALL (fst expr) (rev' args), snd expr) }
| expr = postfix_expression LPAREN RPAREN
    { do expr <- expr;
      ret (CALL (fst expr) [], snd expr) }
| expr = postfix_expression DOT mem = identifier
    { do expr <- expr;
      ret (MEMBEROF (fst expr) (fst mem), snd expr) }
| expr = postfix_expression PTR mem = identifier
    { do expr <- expr;
      ret (MEMBEROFPTR (fst expr) (fst mem), snd expr) }
| expr = postfix_expression INC
    { do expr <- expr;
      ret (UNARY POSINCR (fst expr), snd expr) }
| expr = postfix_expression DEC
    { do expr <- expr;
      ret (UNARY POSDECR (fst expr), snd expr) }
| loc = LPAREN ty = type_name RPAREN LBRACE init = initializer_list RBRACE
| loc = LPAREN ty = type_name RPAREN LBRACE init = initializer_list COMMA RBRACE
    { do ty <- ty;
      do init <- init;
      ret (CAST ty (COMPOUND_INIT (rev' init)), loc) }

(* Non-standard *)
| loc = BUILTIN_VA_ARG LPAREN expr = assignment_expression COMMA ty = type_name RPAREN
    { do expr <- expr;
      do ty <- ty;
      ret (BUILTIN_VA_ARG (fst expr) ty, loc) }

(* Known context *)
argument_expression_list:
| expr = assignment_expression
    { do expr <- expr;
      ret [fst expr] }
| exprq = argument_expression_list COMMA exprt = assignment_expression
    { do exprq <- exprq;
      do exprt <- exprt;
      ret (fst exprt::exprq) }

(* 6.5.3 *)
(* Known context *)
unary_expression:
| expr = postfix_expression
    { expr }
| loc = INC expr = unary_expression
    { do expr <- expr;
      ret (UNARY PREINCR (fst expr), loc) }
| loc = DEC expr = unary_expression
    { do expr <- expr;
      ret (UNARY PREDECR (fst expr), loc) }
| op = unary_operator expr = cast_expression
    { do expr <- expr;
      ret (UNARY (fst op) (fst expr), snd op) }
| loc = SIZEOF expr = unary_expression
    { do expr <- expr;
      ret (EXPR_SIZEOF (fst expr), loc) }
| loc = SIZEOF LPAREN ty = type_name RPAREN
    { do ty <- ty;
      ret (TYPE_SIZEOF ty, loc) }

(* Non-standard *)
| loc = ALIGNOF expr = unary_expression
    { do expr <- expr;
      ret (EXPR_ALIGNOF (fst expr), loc) }
| loc = ALIGNOF LPAREN ty = type_name RPAREN
    { do ty <- ty;
      ret (TYPE_ALIGNOF ty, loc) }

unary_operator:
| loc = AND
    { (ADDROF, loc) }
| loc = STAR
    { (MEMOF, loc) } 
| loc = PLUS
    { (PLUS, loc) }
| loc = MINUS
    { (MINUS, loc) }
| loc = TILDE
    { (BNOT, loc) }
| loc = BANG
    { (NOT, loc) }

(* 6.5.4 *)
(* Known context *)
cast_expression:
| expr = unary_expression
    { expr }
| loc = LPAREN ty = type_name RPAREN expr = cast_expression
    { do ty <- ty;
      do expr <- expr;
      ret (CAST ty (SINGLE_INIT (fst expr)), loc) }

(* 6.5.5 *)
(* Known context *)
multiplicative_expression:
| expr = cast_expression
    { expr }
| expr1 = multiplicative_expression STAR expr2 = cast_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY MUL (fst expr1) (fst expr2), snd expr1) }
| expr1 = multiplicative_expression SLASH expr2 = cast_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY DIV (fst expr1) (fst expr2), snd expr1) }
| expr1 = multiplicative_expression PERCENT expr2 = cast_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY MOD (fst expr1) (fst expr2), snd expr1) }

(* 6.5.6 *)
(* Known context *)
additive_expression:
| expr = multiplicative_expression
    { expr }
| expr1 = additive_expression PLUS expr2 = multiplicative_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY ADD (fst expr1) (fst expr2), snd expr1) }
| expr1 = additive_expression MINUS expr2 = multiplicative_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY SUB (fst expr1) (fst expr2), snd expr1) }

(* 6.5.7 *)
(* Known context *)
shift_expression:
| expr = additive_expression
    { expr }
| expr1 = shift_expression LEFT expr2 = additive_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY SHL (fst expr1) (fst expr2), snd expr1) }
| expr1 = shift_expression RIGHT expr2 = additive_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY SHR (fst expr1) (fst expr2), snd expr1) }

(* 6.5.8 *)
(* Known context *)
relational_expression:
| expr = shift_expression
    { expr }
| expr1 = relational_expression LT expr2 = shift_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY LT (fst expr1) (fst expr2), snd expr1) }
| expr1 = relational_expression GT expr2 = shift_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY GT (fst expr1) (fst expr2), snd expr1) }
| expr1 = relational_expression LEQ expr2 = shift_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY LE (fst expr1) (fst expr2), snd expr1) }
| expr1 = relational_expression GEQ expr2 = shift_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY GE (fst expr1) (fst expr2), snd expr1) }

(* 6.5.9 *)
(* Known context *)
equality_expression:
| expr = relational_expression
    { expr }
| expr1 = equality_expression EQEQ expr2 = relational_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY EQ (fst expr1) (fst expr2), snd expr1) }
| expr1 = equality_expression NEQ expr2 = relational_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY NE (fst expr1) (fst expr2), snd expr1) }

(* 6.5.10 *)
(* Known context *)
AND_expression:
| expr = equality_expression
    { expr }
| expr1 = AND_expression AND expr2 = equality_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY BAND (fst expr1) (fst expr2), snd expr1) }

(* 6.5.11 *)
(* Known context *)
exclusive_OR_expression:
| expr = AND_expression
    { expr }
| expr1 = exclusive_OR_expression HAT expr2 = AND_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY XOR (fst expr1) (fst expr2), snd expr1) }

(* 6.5.12 *)
(* Known context *)
inclusive_OR_expression:
| expr = exclusive_OR_expression
    { expr }
| expr1 = inclusive_OR_expression BAR expr2 = exclusive_OR_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY BOR (fst expr1) (fst expr2), snd expr1) }

(* 6.5.13 *)
(* Known context *)
logical_AND_expression:
| expr = inclusive_OR_expression
    { expr }
| expr1 = logical_AND_expression ANDAND expr2 = inclusive_OR_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY AND (fst expr1) (fst expr2), snd expr1) }

(* 6.5.14 *)
(* Known context *)
logical_OR_expression:
| expr = logical_AND_expression
    { expr }
| expr1 = logical_OR_expression BARBAR expr2 = logical_AND_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY OR (fst expr1) (fst expr2), snd expr1) }

(* 6.5.15 *)
(* Known context *)
conditional_expression:
| expr = logical_OR_expression
    { expr }
| expr1 = logical_OR_expression QUESTION expr2 = expression COLON expr3 = conditional_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      do expr3 <- expr3; 
      ret (QUESTION (fst expr1) (fst expr2) (fst expr3), snd expr1) }

(* 6.5.16 *)
(* Known context *)
assignment_expression:
| expr = conditional_expression
    { expr }
| expr1 = unary_expression op = assignment_operator expr2 = assignment_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY op (fst expr1) (fst expr2), snd expr1) }

assignment_operator:
| EQ
    { ASSIGN  }
| MUL_ASSIGN
    { MUL_ASSIGN }
| DIV_ASSIGN
    { DIV_ASSIGN }
| MOD_ASSIGN
    { MOD_ASSIGN }
| ADD_ASSIGN
    { ADD_ASSIGN }
| SUB_ASSIGN
    { SUB_ASSIGN }
| LEFT_ASSIGN
    { SHL_ASSIGN }
| RIGHT_ASSIGN
    { SHR_ASSIGN }
| XOR_ASSIGN
    { XOR_ASSIGN }
| OR_ASSIGN
    { BOR_ASSIGN }
| AND_ASSIGN
    { BAND_ASSIGN }

(* 6.5.17 *)
(* Known context *)
expression:
| expr = assignment_expression
    { expr }
| expr1 = expression COMMA expr2 = assignment_expression
    { do expr1 <- expr1;
      do expr2 <- expr2;
      ret (BINARY COMMA (fst expr1) (fst expr2), snd expr1) }

(* 6.6 *)
(* Known context *)
constant_expression:
| expr = conditional_expression
    { expr }

(* 6.7 *)
(* Known context if typedef_name needs *)
declaration_no_semicolon(typedef_name):
| decspec = declaration_specifiers(typedef_name) decls = init_declarator_list
    { do decspec <- decspec;
      do decls <- decls (contains_typedef (fst decspec));
      ret (DECDEF (fst decspec, rev' decls) (snd decspec)) }
| decspec = declaration_specifiers(typedef_name)
    { do decspec <- decspec;
      ret (DECDEF (fst decspec, []) (snd decspec)) }

(* Known context if typedef_name needs *)
declaration_specifiers(typedef_name):
| storage = storage_class_specifier rest = declaration_specifiers(typedef_name)
    { do rest <- rest;
      ret (SpecStorage (fst storage)::fst rest, snd storage) }
| ty = type_specifier rest = declaration_specifiers_notypedef
    { do ty <- ty;
      do rest <- rest;
      ret (SpecType (fst ty)::rest, snd ty) }
| id = typedef_name rest = declaration_specifiers_notypedef
    { do rest <- rest;
      ret (SpecType (Tnamed (fst id))::rest, snd id) }
| qual = type_qualifier rest = declaration_specifiers(typedef_name)
    { do rest <- rest;
      ret (SpecCV (fst qual)::fst rest, snd qual) }
| loc = function_specifier rest = declaration_specifiers(typedef_name)
    { do rest <- rest;
      ret (SpecInline::fst rest, loc) }

declaration_specifiers_notypedef:
| (* Empty *)
    { ret ([]) }
| storage = storage_class_specifier rest = declaration_specifiers_notypedef
    { do rest <- rest;
      ret (SpecStorage (fst storage)::rest) }
| ty = type_specifier rest = declaration_specifiers_notypedef
    { do ty <- ty;
      do rest <- rest;
      ret (SpecType (fst ty)::rest) }
| qual = type_qualifier rest = declaration_specifiers_notypedef
    { do rest <- rest;
      ret (SpecCV (fst qual)::rest) }
| loc = function_specifier rest = declaration_specifiers_notypedef
    { do rest <- rest;
      ret (SpecInline::rest) }

init_declarator_list:
| init = init_declarator
    { fun name_type =>
        do init <- init name_type;
        ret [init] }
| initq = init_declarator_list COMMA initt = init_declarator
    { fun name_type =>
        do initq <- initq name_type;
        do initt <- initt name_type;
        ret (initt::initq) }

init_declarator:
| decl = declarator
    { fun name_type =>
        do decl <- decl;
        let 'Name name _ _ _ := decl in
        do dummy <- bind_identifier name name_type;
        ret (Init_name decl NO_INIT) }
| decl = declarator EQ chunk = delayed_chunk(innocent_token)
    { fun name_type =>
        do decl <- decl;
        let 'Name name _ _ _ := decl in
        do dummy <- bind_identifier name  name_type;
        do chunk <- chunk (const (existT _ EOF_t tt));
        do init <- call_parsing_routine c_initializer_pr chunk;
        ret (Init_name decl init) }

(* 6.7.1 *)
storage_class_specifier:
| loc = TYPEDEF
    { (TYPEDEF, loc) }
| loc = EXTERN
    { (EXTERN, loc) }
| loc = STATIC
    { (STATIC, loc) }
| loc = AUTO
    { (AUTO, loc) } 
| loc = REGISTER
    { (REGISTER, loc) }

(* 6.7.2 *)
type_specifier:
| loc = VOID
    { ret (Tvoid, loc) }
| loc = CHAR
    { ret (Tchar, loc) }
| loc = SHORT
    { ret (Tshort, loc) }
| loc = INT
    { ret (Tint, loc) }
| loc = LONG
    { ret (Tlong, loc) }
| loc = FLOAT
    { ret (Tfloat, loc) }
| loc = DOUBLE
    { ret (Tdouble, loc) }
| loc = SIGNED
    { ret (Tsigned, loc) }
| loc = UNSIGNED
    { ret (Tunsigned, loc) }
| loc = BOOL
    { ret (T_Bool, loc) }
| spec = struct_or_union_specifier
| spec = enum_specifier
    { spec }

(* 6.7.2.1 *)
struct_or_union_specifier:
| str_uni = struct_or_union id = identifier LBRACE decls = struct_declaration_list RBRACE
    { do decls <- decls;
      ret (Tstruct_union (fst str_uni) (Some (fst id)) (Some (rev' decls)) [], snd str_uni) }
| str_uni = struct_or_union LBRACE decls = struct_declaration_list RBRACE
    { do decls <- decls;
      ret (Tstruct_union (fst str_uni) None            (Some (rev' decls)) [], snd str_uni) }
| str_uni = struct_or_union id = identifier
    { ret (Tstruct_union (fst str_uni) (Some (fst id)) None               [], snd str_uni) }

struct_or_union:
| loc = STRUCT
    { (STRUCT, loc) }
| loc = UNION
    { (UNION, loc) }

struct_declaration_list:
| decl = struct_declaration
    { do decl <- decl;
      ret [decl] }
| qdecl = struct_declaration_list tdecl = struct_declaration
    { do qdecl <- qdecl;
      do tdecl <- tdecl;
      ret (tdecl::qdecl) }

struct_declaration:
| decspec = specifier_qualifier_list(identifier) decls = struct_declarator_list SEMICOLON
    { do decspec <- decspec;
      do decls <- decls;
      ret (Field_group (fst decspec) (rev' decls) (snd decspec)) }
(* Extension to C99 grammar needed to parse some GNU header files. *)
| decspec = specifier_qualifier_list(identifier) SEMICOLON
    { do decspec <- decspec;
      ret (Field_group (fst decspec) []          (snd decspec)) }

(* Known context if typedef_name needs *)
specifier_qualifier_list(typedef_name):
| ty = type_specifier rest = specifier_qualifier_list_notypedef
    { do ty <- ty;
      do rest <- rest;
      ret (SpecType (fst ty)::rest, snd ty) }
| id = typedef_name rest = specifier_qualifier_list_notypedef
    { do rest <- rest;
      ret (SpecType (Tnamed (fst id))::rest, snd id) }
| qual = type_qualifier rest = specifier_qualifier_list(typedef_name)
    { do rest <- rest;
      ret (SpecCV (fst qual)::fst rest, snd qual) }

specifier_qualifier_list_notypedef:
| (* Empty *)
    { ret ([]) }
| ty = type_specifier rest = specifier_qualifier_list_notypedef
    { do ty <- ty;
      do rest <- rest;
      ret (SpecType (fst ty)::rest) }
| qual = type_qualifier rest = specifier_qualifier_list_notypedef
    { do rest <- rest;
      ret (SpecCV (fst qual)::rest) }

struct_declarator_list:
| decl = struct_declarator
    { do decl <- decl;
      ret [decl] }
| declq = struct_declarator_list COMMA declt = struct_declarator
    { do declq <- declq;
      do declt <- declt;
      ret (declt::declq) }

struct_declarator:
| decl = declarator
    { do decl <- decl;
      ret (Some decl, None) }
| decl = declarator COLON chunk = delayed_chunk_nonbracebegin(innocent_token)
    { do decl <- decl;
      do chunk <- chunk (const (existT _ EOF_t tt));
      do expr <- call_parsing_routine constant_expression_pr chunk;
      ret (Some decl, Some (fst expr)) }
| COLON chunk = delayed_chunk_nonbracebegin(innocent_token)
    { do chunk <- chunk (const (existT _ EOF_t tt));
      do expr <- call_parsing_routine constant_expression_pr chunk;
      ret (None, Some (fst expr)) }

(* 6.7.2.2 *)
enum_specifier:
| loc = ENUM name = identifier LBRACE enum_list = enumerator_list RBRACE
| loc = ENUM name = identifier LBRACE enum_list = enumerator_list COMMA RBRACE
    { do enum_list <- enum_list;
      ret (Tenum (Some (fst name)) (Some (rev' enum_list)) [], loc) }
| loc = ENUM LBRACE enum_list = enumerator_list RBRACE
| loc = ENUM LBRACE enum_list = enumerator_list COMMA RBRACE
    { do enum_list <- enum_list;
      ret (Tenum None              (Some (rev' enum_list)) [], loc) }
| loc = ENUM name = identifier
    { ret (Tenum (Some (fst name)) None                   [], loc) }

enumerator_list:
| enum = enumerator
    { do enum <- enum;
      ret [enum] }
| enumq = enumerator_list COMMA enumt = enumerator
    { do enumq <- enumq;
      do enumt <- enumt;
      ret (enumt::enumq) }

enumerator:
| name = identifier
    { do dummy <- bind_identifier (fst name) Var;
      ret (fst name, None, snd name) }
| name = identifier EQ chunk = delayed_chunk_nonbracebegin(innocent_token)
    { do chunk <- chunk (const (existT _ EOF_t tt));
      do expr <- call_parsing_routine constant_expression_pr chunk;
      do dummy <- bind_identifier (fst name) Var;
      ret (fst name, Some (fst expr), snd name) }

(* 6.7.3 *)
type_qualifier:
| loc = CONST
    { (CV_CONST, loc) }
| loc = RESTRICT
    { (CV_RESTRICT, loc) }
| loc = VOLATILE
    { (CV_VOLATILE, loc) }

(* 6.7.4 *)
function_specifier:
| loc = INLINE
    { loc }

(* 6.7.5 *)
declarator:
| decl = direct_declarator
    { decl }
| pt = pointer decl = direct_declarator
    { do decl <- decl;
      ret (let 'Name name typ attr _ := decl in 
           Name name ((fst pt) typ) attr (snd pt)) }

direct_declarator:
| id = identifier
    { ret (Name (fst id) JUSTBASE [] (snd id)) }
| LPAREN decl = declarator RPAREN
    { decl }
| decl = direct_declarator LBRACK chunk = delayed_chunk_nonbracebegin(innocent_token) RBRACK
    { do decl <- decl;
      do chunk <- chunk (const (existT _ EOF_t tt));
      do in_brack <- call_parsing_routine type_qualifier_list_assignment_expression_pr chunk;
      ret (let 'Name name typ attr loc := decl in
           Name name (ARRAY typ (fst in_brack) [] (snd in_brack)) attr loc) }
(*| direct_declarator LBRACK ... STATIC ... RBRACK
| direct_declarator LBRACK STAR RBRACK*)
| decl = direct_declarator LPAREN params = parameter_type_list RPAREN
    { do decl <- decl;
      do params <- params;
      ret (let 'Name name typ attr loc := decl in 
           Name name (PROTO typ params) attr loc) }
| decl = direct_declarator LPAREN RPAREN
    { do decl <- decl;
      ret (let 'Name name typ attr loc := decl in
           Name name (PROTO typ ([], false)) attr loc) }

pointer:
| loc = STAR
    { (PTR [] [], loc) }
| loc = STAR quallst = type_qualifier_list
    { (PTR (rev' quallst) [], loc) }
| loc = STAR pt = pointer
    { (fun typ => PTR [] [] ((fst pt) typ), loc) }
| loc = STAR quallst = type_qualifier_list pt = pointer
    { (fun typ => PTR (rev' quallst) [] ((fst pt) typ), loc) }

type_qualifier_list:
| qual = type_qualifier
    { [fst qual] }
| qualq = type_qualifier_list qualt = type_qualifier
    { fst qualt::qualq }

parameter_type_list:
| params = parameter_list
    { do params <- in_scope(params);
      ret (rev' params, false) }
| params = parameter_list COMMA ELLIPSIS
    { do params <- in_scope(params);
      ret (rev' params, true) }

parameter_declaration:
| chunkt = parameter_declaration_first chunkq = delayed_chunk(innocent_token)
    { do chunkt <- chunkt;
      do chunkq <- chunkq (const (existT _ EOF_t tt));
      let chunk := Cons chunkt chunkq in
      do param <- 
        try (call_parsing_routine parameter_declaration_abstract_declarator_pr chunk)
            (call_parsing_routine parameter_declaration_declarator_pr chunk);
      ret param }

parameter_list:
| param = parameter_declaration
    { do param <- param;
      ret [param] }
| paramq = parameter_list COMMA paramt = parameter_declaration
    { do paramq <- paramq;
      do paramt <- paramt;
      ret (paramt::paramq) }

(* Known context *)
parameter_declaration_abstract_declarator:
| specs = declaration_specifiers(TYPEDEF_NAME) decl = abstract_declarator
    { do specs <- specs;
      do decl <- decl;
      ret (PARAM (fst specs) None decl [] (snd specs)) }
| specs = declaration_specifiers(TYPEDEF_NAME)
    { do specs <- specs;
      ret (PARAM (fst specs) None JUSTBASE [] (snd specs)) }

(* Known context *)
parameter_declaration_declarator:
| specs = declaration_specifiers(TYPEDEF_NAME) decl = declarator
    { do specs <- specs;
      do decl <- decl;
      let 'Name name typ attr _ := decl in
      do dummy <- bind_identifier name Var;
      ret (PARAM (fst specs) (Some name) typ attr (snd specs)) }

(* 6.7.6 *)
(* Known context *)
type_name:
| specqual = specifier_qualifier_list(TYPEDEF_NAME)
    { do specqual <- specqual;
      ret (fst specqual, JUSTBASE) }
| specqual = specifier_qualifier_list(TYPEDEF_NAME) decl = abstract_declarator
    { do specqual <- specqual;
      do decl <- decl;
      ret (fst specqual, decl) }

(* Known context *)
abstract_declarator:
| pt = pointer
    { ret ((fst pt) JUSTBASE) }
| pt = pointer decl = direct_abstract_declarator
    { do decl <- decl;
      ret ((fst pt) decl) }
| decl = direct_abstract_declarator
   { decl }

(* Known context *)
option_direct_abstract_declarator:
| (* Empty *)
    { ret JUSTBASE }
| decl = direct_abstract_declarator
    { decl }

(* Known context *)
direct_abstract_declarator:
| LPAREN decl = abstract_declarator RPAREN
    { decl }
| decl = option_direct_abstract_declarator LBRACK chunk = delayed_chunk_nonbracebegin(innocent_token) RBRACK
    { do decl <- decl;
      do chunk <- chunk (const (existT _ EOF_t tt));
      do in_brack <- call_parsing_routine type_qualifier_list_assignment_expression_pr chunk;
      ret (ARRAY decl (fst in_brack) [] (snd in_brack)) }
(*| direct_abstract_declarator? LBRACK STAR RBRACK*)
(*| direct_abstract_declarator? LBRACK ... STATIC ... RBRACK*)
| decl = direct_abstract_declarator LPAREN params = parameter_type_list RPAREN
    { do decl <- decl;
      do params <- params;
      ret (PROTO decl params) }
| decl = direct_abstract_declarator LPAREN RPAREN
    { do decl <- decl;
      ret (PROTO decl ([], false)) }
| LPAREN params = parameter_type_list RPAREN
    { do params <- params;
      ret (PROTO JUSTBASE params) }
| LPAREN RPAREN
    { ret (PROTO JUSTBASE ([], false)) }

(* 6.7.8 *)
(* Known context *)
c_initializer:
| expr = assignment_expression
    { do expr <- expr;
      ret (SINGLE_INIT (fst expr)) }
| LBRACE init = initializer_list RBRACE
| LBRACE init = initializer_list COMMA RBRACE
    { do init <- init;
      ret (COMPOUND_INIT (rev' init)) }

(* Known context *)
initializer_list:
| design = designation init = c_initializer
    { do design <- design;
      do init <- init;
      ret [(design, init)] }
| init = c_initializer
    { do init <- init;
      ret [([], init)] }
| initq = initializer_list COMMA design = designation init = c_initializer
    { do initq <- initq;
      do design <- design;
      do init <- init;
      ret ((design, init)::initq) }
| initq = initializer_list COMMA init = c_initializer
    { do initq <- initq;
      do init <- init;
      ret (([], init)::initq) }

(* Known context *)
designation:
| design = designator_list EQ
    { do design <- design;
      ret (rev' design) }

(* Known context *)
designator_list:
| design = designator
    { do design <- design;
      ret [design] }
| designq = designator_list designt = designator
    { do designq <- designq;
      do designt <- designt;
      ret (designt::designq) }

(* Known context *)
designator:
| LBRACK expr = constant_expression RBRACK
    { do expr <- expr;
      ret (ATINDEX_INIT (fst expr)) }
| DOT id = identifier
    { ret (INFIELD_INIT (fst id)) }

(* 6.8 *)
expression_or_declaration_statement:
| chunk = delayed_chunk_nonbracebegin(innocent_list_token) loc = SEMICOLON
    { fun declarationAllowed =>
      do chunk <- chunk (const (existT _ EOF_t tt));
      if declarationAllowed 
	then 
          do decl_or_stmt <- call_parsing_routine declaration_or_expression_pr chunk;
	  ret (match decl_or_stmt with
	         | inl (inl decl) => DEFINITION decl
		 | inl (inr expr) => COMPUTATION (fst expr) (snd expr)
		 | inr tt => NOP loc
	       end)
        else
          do expr <- call_parsing_routine expression_option_pr chunk;
	  ret (match expr with
                 | Some expr => COMPUTATION (fst expr) (snd expr)
	         | None => NOP loc
               end)
      }

statement_dangerous:
| stmt = labeled_statement(statement_dangerous)
| stmt = compound_statement
| stmt = selection_statement_dangerous
| stmt = iteration_statement(statement_dangerous)
| stmt = jump_statement
    { fun _ => stmt }
| stmt = expression_or_declaration_statement
    { stmt }	  

statement_safe:
| stmt = labeled_statement(statement_safe)
| stmt = compound_statement
| stmt = selection_statement_safe
| stmt = iteration_statement(statement_safe)
| stmt = jump_statement
    { fun _ => stmt }
| stmt = expression_or_declaration_statement
    { stmt }

(* 6.8.1 *)
labeled_statement(last_statement):
| lbl = identifier COLON stmt = last_statement
    { do stmt <- stmt false;
      ret (LABEL (fst lbl) stmt (snd lbl)) }
| loc = CASE chunk = delayed_chunk_nonbracebegin(innocent_token) COLON stmt = last_statement
    { do chunk <- chunk (const (existT _ EOF_t tt));
      do expr <- call_parsing_routine constant_expression_pr chunk;
      do stmt <- stmt false;
      ret (CASE (fst expr) stmt loc) }
| loc = DEFAULT COLON stmt = last_statement
    { do stmt <- stmt false;
      ret (DEFAULT stmt loc) }

(* 6.8.2 *)
compound_statement:
| loc = LBRACE block = block_item_list RBRACE
    { do block <- in_scope block;
      ret (BLOCK (rev' block) loc) }
| loc = LBRACE RBRACE
    { ret (BLOCK [] loc) }

block_item_list:
| stmt = block_item
    { do stmt <- stmt;
      ret [stmt] }
| stmtq = block_item_list stmtt = block_item
    { do stmtq <- stmtq;
      do stmtt <- stmtt;
      ret (stmtt::stmtq) }

block_item:
(*| declaration*)
| stmt = statement_dangerous
    { stmt true }

(* Non-standard *)
| p = PRAGMA
    { ret (DEFINITION (PRAGMA (fst p) (snd p))) }

(* 6.8.4 *)
selection_statement_dangerous:
| loc = IF LPAREN chunk = delayed_chunk_nonbracebegin(innocent_list_token) RPAREN stmt = statement_dangerous
    { do chunk <- chunk (const (existT _ EOF_t tt));
      do expr <- call_parsing_routine expression_pr chunk;
      do stmt <- stmt false;
      ret (If (fst expr) stmt None loc) }
| loc = IF LPAREN chunk = delayed_chunk_nonbracebegin(innocent_list_token) RPAREN stmt1 = statement_safe ELSE stmt2 = statement_dangerous
    { do chunk <- chunk (const (existT _ EOF_t tt));
      do expr <- call_parsing_routine expression_pr chunk;
      do stmt1 <- stmt1 false;
      do stmt2 <- stmt2 false;
      ret (If (fst expr) stmt1 (Some stmt2) loc) }
| loc = SWITCH LPAREN chunk = delayed_chunk_nonbracebegin(innocent_list_token) RPAREN stmt = statement_dangerous
    { do chunk <- chunk (const (existT _ EOF_t tt));
      do expr <- call_parsing_routine expression_pr chunk;
      do stmt <- stmt false;
      ret (SWITCH (fst expr) stmt loc) }

selection_statement_safe:
| loc = IF LPAREN chunk = delayed_chunk_nonbracebegin(innocent_list_token) RPAREN stmt1 = statement_safe ELSE stmt2 = statement_safe
    { do chunk <- chunk (const (existT _ EOF_t tt));
      do expr <- call_parsing_routine expression_pr chunk;
      do stmt1 <- stmt1 false;
      do stmt2 <- stmt2 false;
      ret (If (fst expr) stmt1 (Some stmt2) loc) }
| loc = SWITCH LPAREN chunk = delayed_chunk_nonbracebegin(innocent_list_token) RPAREN stmt = statement_safe
    { do chunk <- chunk (const (existT _ EOF_t tt));
      do expr <- call_parsing_routine expression_pr chunk;
      do stmt <- stmt false;
      ret (SWITCH (fst expr) stmt loc) }

(* 6.8.5 *)
iteration_statement(last_statement):
| loc = WHILE LPAREN chunk = delayed_chunk_nonbracebegin(innocent_list_token) RPAREN stmt = last_statement
    { do chunk <- chunk (const (existT _ EOF_t tt));
      do expr <- call_parsing_routine expression_pr chunk;
      do stmt <- stmt false;
      ret (WHILE (fst expr) stmt loc) }
| loc = DO stmt = statement_dangerous WHILE LPAREN chunk = delayed_chunk_nonbracebegin(innocent_list_token) RPAREN SEMICOLON
    { do stmt <- stmt false;
      do chunk <- chunk (const (existT _ EOF_t tt));
      do expr <- call_parsing_routine expression_pr chunk;
      ret (DOWHILE (fst expr) stmt loc) }
| loc = FOR LPAREN chunk1 = delayed_chunk_nonbracebegin(innocent_list_token) SEMICOLON chunk2 = delayed_chunk_nonbracebegin(innocent_list_token) SEMICOLON chunk3 = delayed_chunk_nonbracebegin(innocent_list_token) RPAREN stmt = last_statement
    { do chunk1 <- chunk1 (const (existT _ EOF_t tt));
      do decl_or_expr <- call_parsing_routine declaration_or_expression_pr chunk1;
      let clause1 := match decl_or_expr with
	| inl (inl decl) => Some (FC_DECL decl)
	| inl (inr expr) => Some (FC_EXP (fst expr))
	| inr tt => None
      end in
      do chunk2 <- chunk2 (const (existT _ EOF_t tt));
      do clause2 <- call_parsing_routine expression_option_pr chunk2;
      let clause2 := match clause2 with
	| Some expr => Some (fst expr)
	| None => None
      end in
      do chunk3 <- chunk3 (const (existT _ EOF_t tt));
      do clause3 <- call_parsing_routine expression_option_pr chunk3;
      let clause3 := match clause3 with
	| Some expr => Some (fst expr)
	| None => None
      end in
      do stmt <- stmt false;
      ret (FOR clause1 clause2 clause3 stmt loc) }


(* 6.8.6 *)
jump_statement:
| loc = GOTO id = identifier SEMICOLON
    { ret (GOTO (fst id) loc) }
| loc = CONTINUE SEMICOLON
    { ret (CONTINUE loc) }
| loc = BREAK SEMICOLON
    { ret (BREAK loc) }
| loc = RETURN chunk = delayed_chunk_nonbracebegin(innocent_list_token) SEMICOLON
    { do chunk <- chunk (const (existT _ EOF_t tt));
      do expr <- call_parsing_routine expression_option_pr chunk;
      ret (match expr with
             | Some expr => RETURN (Some (fst expr)) loc
	     | None => RETURN None loc end)}

(* 6.9 *)
translation_unit_file:
| lst = translation_unit EOF
    { do lst <- lst;
      ret (rev' lst) }

translation_unit:
| def = external_declaration
    { do def <- def;
      ret [def] }
| defq = translation_unit deft = external_declaration
    { do defq <- defq;
      do deft <- deft;
      ret (deft::defq) }

external_declaration:
| def = function_definition
| def = declaration_no_semicolon(identifier) SEMICOLON
    { def }
(* Non-standard *)
| p = PRAGMA
    { ret (PRAGMA (fst p) (snd p)) }

(* 6.9.1 *)
function_definition:
| specs = declaration_specifiers(identifier) decl = declarator stmt = compound_statement
    { do specs <- specs;
      do decl <- decl;
      let 'Name name ty _ _ := decl in
      do dummy <- bind_identifier name Var;
      do stmt <- in_scope (
        do dummy <- do_bind_function_parameters ty;
        do dummy <- bind_identifier func_atom Var;
        stmt);
      ret (FUNDEF (fst specs) decl stmt (snd specs)) }

%%

Fixpoint parsing_routines_fix (iterator:nat) : parsing_routines terminal_semantic_type :=
  match iterator with
    | 0 =>
      {| declaration_or_expression_pr := fun _ _ => Timeout _;
         expression_pr := fun _ _ => Timeout _;
         c_initializer_pr := fun _ _ => Timeout _;
         expression_option_pr := fun _ _ => Timeout _;
         constant_expression_pr := fun _ _ => Timeout _;
         type_qualifier_list_assignment_expression_pr := fun _ _ => Timeout _;
         parameter_declaration_abstract_declarator_pr := fun _ _ => Timeout _;
         parameter_declaration_declarator_pr := fun _ _ => Timeout _ |}
    | S k =>
      {| declaration_or_expression_pr := fun s env => 
           match declaration_or_expression_eof iterator s with
             | Parser.Inter.Parsed_pr sem _ =>
               sem (parsing_routines_fix k) env
             | Parser.Inter.Timeout_pr => Timeout _
             | Parser.Inter.Fail_pr => Fail _
           end;
         expression_pr := fun s env => 
           match expression_eof iterator s with
             | Parser.Inter.Parsed_pr sem _ =>
               sem (parsing_routines_fix k) env
             | Parser.Inter.Timeout_pr => Timeout _
             | Parser.Inter.Fail_pr => Fail _
           end;
         c_initializer_pr := fun s env => 
           match c_initializer_eof iterator s with
             | Parser.Inter.Parsed_pr sem _ =>
               sem (parsing_routines_fix k) env
             | Parser.Inter.Timeout_pr => Timeout _
             | Parser.Inter.Fail_pr => Fail _
           end;
         expression_option_pr := fun s env => 
           match expression_option_eof iterator s with
             | Parser.Inter.Parsed_pr sem _ =>
               sem (parsing_routines_fix k) env
             | Parser.Inter.Timeout_pr => Timeout _
             | Parser.Inter.Fail_pr => Fail _
           end;
         constant_expression_pr := fun s env => 
           match constant_expression_eof iterator s with
             | Parser.Inter.Parsed_pr sem _ =>
               sem (parsing_routines_fix k) env
             | Parser.Inter.Timeout_pr => Timeout _
             | Parser.Inter.Fail_pr => Fail _
           end;
         type_qualifier_list_assignment_expression_pr := fun s env => 
           match type_qualifier_list_assignment_expression_eof iterator s with
             | Parser.Inter.Parsed_pr sem _ =>
               sem (parsing_routines_fix k) env
             | Parser.Inter.Timeout_pr => Timeout _
             | Parser.Inter.Fail_pr => Fail _
           end;
         parameter_declaration_abstract_declarator_pr := fun s env => 
           match parameter_declaration_abstract_declarator_eof iterator s with
             | Parser.Inter.Parsed_pr sem _ =>
               sem (parsing_routines_fix k) env
             | Parser.Inter.Timeout_pr => Timeout _
             | Parser.Inter.Fail_pr => Fail _
           end;
         parameter_declaration_declarator_pr := fun s env => 
           match parameter_declaration_declarator_eof iterator s with
             | Parser.Inter.Parsed_pr sem _ =>
               sem (parsing_routines_fix k) env
             | Parser.Inter.Timeout_pr => Timeout _
             | Parser.Inter.Fail_pr => Fail _
           end |}
  end.

Inductive extractable_token : Type :=
| IDENTIFIER : atom -> cabsloc -> extractable_token
| BUILTIN : atom -> cabsloc -> extractable_token
| PRAGMA : atom -> cabsloc -> extractable_token
| LITERAL : constant -> cabsloc -> extractable_token
| STRING_LITERAL : atom -> cabsloc -> extractable_token
| SIZEOF : cabsloc -> extractable_token
| PTR : cabsloc -> extractable_token
| INC : cabsloc -> extractable_token
| DEC : cabsloc -> extractable_token
| LEFT : cabsloc -> extractable_token
| RIGHT : cabsloc -> extractable_token
| LEQ : cabsloc -> extractable_token
| GEQ : cabsloc -> extractable_token
| EQEQ : cabsloc -> extractable_token
| EQ : cabsloc -> extractable_token
| NEQ : cabsloc -> extractable_token
| LT : cabsloc -> extractable_token
| GT : cabsloc -> extractable_token
| ANDAND : cabsloc -> extractable_token
| BARBAR : cabsloc -> extractable_token
| PLUS : cabsloc -> extractable_token
| MINUS : cabsloc -> extractable_token
| STAR : cabsloc -> extractable_token
| TILDE : cabsloc -> extractable_token
| BANG : cabsloc -> extractable_token
| SLASH : cabsloc -> extractable_token
| PERCENT : cabsloc -> extractable_token
| HAT : cabsloc -> extractable_token
| BAR : cabsloc -> extractable_token
| QUESTION : cabsloc -> extractable_token
| COLON : cabsloc -> extractable_token
| AND : cabsloc -> extractable_token
| ALIGNOF : cabsloc -> extractable_token
| MUL_ASSIGN : cabsloc -> extractable_token
| DIV_ASSIGN : cabsloc -> extractable_token
| MOD_ASSIGN : cabsloc -> extractable_token
| ADD_ASSIGN : cabsloc -> extractable_token
| SUB_ASSIGN : cabsloc -> extractable_token
| LEFT_ASSIGN : cabsloc -> extractable_token
| RIGHT_ASSIGN : cabsloc -> extractable_token
| AND_ASSIGN : cabsloc -> extractable_token
| XOR_ASSIGN : cabsloc -> extractable_token
| OR_ASSIGN : cabsloc -> extractable_token
| LPAREN : cabsloc -> extractable_token
| RPAREN : cabsloc -> extractable_token
| LBRACK : cabsloc -> extractable_token
| RBRACK : cabsloc -> extractable_token
| LBRACE : cabsloc -> extractable_token
| RBRACE : cabsloc -> extractable_token
| DOT : cabsloc -> extractable_token
| COMMA : cabsloc -> extractable_token
| SEMICOLON : cabsloc -> extractable_token
| ELLIPSIS : cabsloc -> extractable_token
| TYPEDEF : cabsloc -> extractable_token
| EXTERN : cabsloc -> extractable_token
| STATIC : cabsloc -> extractable_token
| RESTRICT : cabsloc -> extractable_token
| AUTO : cabsloc -> extractable_token
| REGISTER : cabsloc -> extractable_token
| INLINE : cabsloc -> extractable_token
| CHAR : cabsloc -> extractable_token
| SHORT : cabsloc -> extractable_token
| INT : cabsloc -> extractable_token
| LONG : cabsloc -> extractable_token
| SIGNED : cabsloc -> extractable_token
| UNSIGNED : cabsloc -> extractable_token
| FLOAT : cabsloc -> extractable_token
| DOUBLE : cabsloc -> extractable_token
| CONST : cabsloc -> extractable_token
| VOLATILE : cabsloc -> extractable_token
| VOID : cabsloc -> extractable_token
| STRUCT : cabsloc -> extractable_token
| UNION : cabsloc -> extractable_token
| ENUM : cabsloc -> extractable_token
| BOOL : cabsloc -> extractable_token
| CASE : cabsloc -> extractable_token
| DEFAULT : cabsloc -> extractable_token
| If : cabsloc -> extractable_token
| ELSE : cabsloc -> extractable_token
| SWITCH : cabsloc -> extractable_token
| WHILE : cabsloc -> extractable_token
| DO : cabsloc -> extractable_token
| FOR : cabsloc -> extractable_token
| GOTO : cabsloc -> extractable_token
| CONTINUE : cabsloc -> extractable_token
| BREAK : cabsloc -> extractable_token
| RETURN : cabsloc -> extractable_token
| BUILTIN_VA_ARG : cabsloc -> extractable_token
| EOF : extractable_token.

Definition convert_extractable_token (env:env) (t:extractable_token) : token :=
  let box := existT terminal_semantic_type in
  match t with
    | IDENTIFIER a l => 
      match PTree.get a env with
        | Some 	 Typedef => box TYPEDEF_NAME_t (a, l)
        | Some Var => box VAR_NAME_t (a, l)
        | None => box UNKNOWN_NAME_t (a, l)
      end
    | BUILTIN a l => box BUILTIN_t (a, l)
    | PRAGMA a l => box PRAGMA_t (a, l)
    | LITERAL c l => box LITERAL_t (c, l)
    | STRING_LITERAL a l => box STRING_LITERAL_t (a, l)
    | SIZEOF l => box SIZEOF_t l
    | PTR l => box PTR_t l
    | INC l => box INC_t l
    | DEC l => box DEC_t l
    | LEFT l => box LEFT_t l
    | RIGHT l => box RIGHT_t l
    | LEQ l => box LEQ_t l
    | GEQ l => box GEQ_t l
    | EQEQ l => box EQEQ_t l
    | EQ l => box EQ_t l
    | NEQ l => box NEQ_t l
    | LT l => box LT_t l
    | GT l => box GT_t l
    | ANDAND l => box ANDAND_t l
    | BARBAR l => box BARBAR_t l
    | PLUS l => box PLUS_t l
    | MINUS l => box MINUS_t l
    | STAR l => box STAR_t l
    | TILDE l => box TILDE_t l
    | BANG l => box BANG_t l
    | SLASH l => box SLASH_t l
    | PERCENT l => box PERCENT_t l
    | HAT l => box HAT_t l
    | BAR l => box BAR_t l
    | QUESTION l => box QUESTION_t l
    | COLON l => box COLON_t l
    | AND l => box AND_t l
    | ALIGNOF l => box ALIGNOF_t l
    | MUL_ASSIGN l => box MUL_ASSIGN_t l
    | DIV_ASSIGN l => box DIV_ASSIGN_t l
    | MOD_ASSIGN l => box MOD_ASSIGN_t l
    | ADD_ASSIGN l => box ADD_ASSIGN_t l
    | SUB_ASSIGN l => box SUB_ASSIGN_t l
    | LEFT_ASSIGN l => box LEFT_ASSIGN_t l
    | RIGHT_ASSIGN l => box RIGHT_ASSIGN_t l
    | AND_ASSIGN l => box AND_ASSIGN_t l
    | XOR_ASSIGN l => box XOR_ASSIGN_t l
    | OR_ASSIGN l => box OR_ASSIGN_t l
    | LPAREN l => box LPAREN_t l
    | RPAREN l => box RPAREN_t l
    | LBRACK l => box LBRACK_t l
    | RBRACK l => box RBRACK_t l
    | LBRACE l => box LBRACE_t l
    | RBRACE l => box RBRACE_t l
    | DOT l => box DOT_t l
    | COMMA l => box COMMA_t l
    | SEMICOLON l => box SEMICOLON_t l
    | ELLIPSIS l => box ELLIPSIS_t l
    | TYPEDEF l => box TYPEDEF_t l
    | EXTERN l => box EXTERN_t l
    | STATIC l => box STATIC_t l
    | RESTRICT l => box RESTRICT_t l
    | AUTO l => box AUTO_t l
    | REGISTER l => box REGISTER_t l
    | INLINE l => box INLINE_t l
    | CHAR l => box CHAR_t l
    | SHORT l => box SHORT_t l
    | INT l => box INT_t l
    | LONG l => box LONG_t l
    | SIGNED l => box SIGNED_t l
    | UNSIGNED l => box UNSIGNED_t l
    | FLOAT l => box FLOAT_t l
    | DOUBLE l => box DOUBLE_t l
    | CONST l => box CONST_t l
    | VOLATILE l => box VOLATILE_t l
    | VOID l => box VOID_t l
    | STRUCT l => box STRUCT_t l
    | UNION l => box UNION_t l
    | ENUM l => box ENUM_t l
    | BOOL l => box BOOL_t l
    | CASE l => box CASE_t l
    | DEFAULT l => box DEFAULT_t l
    | If l => box IF_t l
    | ELSE l => box ELSE_t l
    | SWITCH l => box SWITCH_t l
    | WHILE l => box WHILE_t l
    | DO l => box DO_t l
    | FOR l => box FOR_t l
    | GOTO l => box GOTO_t l
    | CONTINUE l => box CONTINUE_t l
    | BREAK l => box BREAK_t l
    | RETURN l => box RETURN_t l
    | BUILTIN_VA_ARG l => box BUILTIN_VA_ARG_t l
    | EOF => box EOF_t tt
  end.
      
Definition main (iterator:nat) (s:Stream extractable_token) : outcome (list definition) :=
  let parsing_routines := parsing_routines_fix iterator in
  let init_env := PTree.empty _ in
  match translation_unit_file iterator (Streams.map (convert_extractable_token init_env) s) with
    | Parser.Inter.Parsed_pr sem _ =>
      sem parsing_routines init_env
    | Parser.Inter.Timeout_pr => Timeout _
    | Parser.Inter.Fail_pr => Fail _
  end.