path: root/caml/CMparser.mly

/* $Id: CMparser.mly,v 1.2 2005/03/21 15:53:00 xleroy Exp $ */

%{
open Datatypes
open CList
open Camlcoq
open BinPos
open BinInt
open Integers
open AST
open Cminor

let intconst n =
  Econst(Ointconst(coqint_of_camlint n))

let andbool e1 e2 =
  Econdition(e1, e2, intconst 0l)
let orbool e1 e2 =
  Econdition(e1, intconst 1l, e2)

let exitnum n = nat_of_camlint(Int32.pred n)

let mkswitch expr (cases, dfl) =
  let rec mktable = function
  | [] -> Coq_nil
  | (key, exit) :: rem ->
      Coq_cons(Coq_pair(coqint_of_camlint key, exitnum exit), mktable rem) in
  Sswitch(expr, mktable cases, exitnum dfl)

(***
   match (a) { case 0: s0; case 1: s1; case 2: s2; }  --->

   block {
   block {
   block {
   block {
     switch(a) { case 0: exit 0; case 1: exit 1; default: exit 2; }
   }; s0; exit 2;
   }; s1; exit 1;
   }; s2;
   }

   Note that matches are assumed to be exhaustive
***)

let mkmatch_aux expr cases =
  let ncases = Int32.of_int (List.length cases) in
  let rec mktable n = function
    | [] -> assert false
    | [key, action] -> Coq_nil
    | (key, action) :: rem ->
        Coq_cons(Coq_pair(coqint_of_camlint key, nat_of_camlint n),
                 mktable (Int32.succ n) rem) in
  let sw =
    Sswitch(expr, mktable 0l cases, nat_of_camlint (Int32.pred ncases)) in
  let rec mkblocks body n = function
    | [] -> assert false
    | [key, action] ->
        Sblock(Sseq(body, action))
    | (key, action) :: rem ->
        mkblocks
          (Sblock(Sseq(body, Sseq(action, Sexit (nat_of_camlint n)))))
          (Int32.pred n)
          rem in
  mkblocks (Sblock sw) (Int32.pred ncases) cases

let mkmatch expr cases =
  match cases with
  | [] -> Sskip (* ??? *)
  | [key, action] -> action
  | _ -> mkmatch_aux expr cases

%}

%token ABSF
%token AMPERSAND
%token AMPERSANDAMPERSAND
%token ALLOC
%token BANG
%token BANGEQUAL
%token BANGEQUALF
%token BANGEQUALU
%token BAR
%token BARBAR
%token CARET
%token CASE
%token COLON
%token COMMA
%token DEFAULT
%token DOLLAR
%token ELSE
%token EQUAL
%token EQUALEQUAL
%token EQUALEQUALF
%token EQUALEQUALU
%token EOF
%token EXIT
%token EXTERN
%token FLOAT
%token FLOAT32
%token FLOAT64
%token <float> FLOATLIT
%token FLOATOFINT
%token FLOATOFINTU
%token GREATER
%token GREATERF
%token GREATERU
%token GREATEREQUAL
%token GREATEREQUALF
%token GREATEREQUALU
%token GREATERGREATER
%token GREATERGREATERU
%token <AST.ident> IDENT
%token IF
%token IN
%token INT
%token INT16S
%token INT16U
%token INT32
%token INT8S
%token INT8U
%token <int32> INTLIT
%token INTOFFLOAT
%token LBRACE
%token LBRACELBRACE
%token LBRACKET
%token LESS
%token LESSU
%token LESSF
%token LESSEQUAL
%token LESSEQUALU
%token LESSEQUALF
%token LESSLESS
%token LET
%token LOOP
%token LPAREN
%token MATCH
%token MINUS
%token MINUSF
%token MINUSGREATER
%token PERCENT
%token PERCENTU
%token PLUS
%token PLUSF
%token QUESTION
%token RBRACE
%token RBRACERBRACE
%token RBRACKET
%token RETURN
%token RPAREN
%token SEMICOLON
%token SLASH
%token SLASHF
%token SLASHU
%token STACK
%token STAR
%token STARF
%token <AST.ident> STRINGLIT
%token SWITCH
%token TILDE
%token VAR
%token VOID

/* Precedences from low to high */

%left COMMA
%left p_let
%right EQUAL
%right QUESTION COLON
%left BARBAR
%left AMPERSANDAMPERSAND
%left BAR
%left CARET
%left AMPERSAND
%left EQUALEQUAL BANGEQUAL LESS LESSEQUAL GREATER GREATEREQUAL EQUALEQUALU BANGEQUALU LESSU LESSEQUALU GREATERU GREATEREQUALU EQUALEQUALF BANGEQUALF LESSF LESSEQUALF GREATERF GREATEREQUALF 
%left LESSLESS GREATERGREATER GREATERGREATERU
%left PLUS PLUSF MINUS MINUSF
%left STAR SLASH PERCENT STARF SLASHF SLASHU PERCENTU
%nonassoc BANG TILDE p_uminus ABSF INTOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 ALLOC
%left LPAREN

/* Entry point */

%start prog
%type <Cminor.program> prog

%%

/* Programs */

prog:
    global_declarations proc_list EOF
      { { prog_funct = CList.rev $2;
          prog_main = intern_string "main";
          prog_vars = CList.rev $1; } }
;

global_declarations:
    /* empty */                                 { Coq_nil }
  | global_declarations global_declaration      { Coq_cons($2, $1) }
;

global_declaration:
    VAR STRINGLIT LBRACKET INTLIT RBRACKET
      { Coq_pair(Coq_pair($2,
                          Coq_cons(Init_space (z_of_camlint $4), Coq_nil)),
                 ()) }
;

proc_list:
    /* empty */                                 { Coq_nil }
  | proc_list proc                              { Coq_cons($2, $1) }
;

/* Procedures */

proc:
    STRINGLIT LPAREN parameters RPAREN COLON signature
    LBRACE
      stack_declaration
      var_declarations
      stmt_list
    RBRACE
      { Coq_pair($1,
        Internal { fn_sig = $6;
                   fn_params = CList.rev $3;
                   fn_vars = CList.rev $9;
                   fn_stackspace = $8;
                   fn_body = $10 }) }
  | EXTERN STRINGLIT COLON signature 
      { Coq_pair($2,
        External { ef_id = $2;
                   ef_sig = $4 }) }
;

signature:
    type_ 
               { {sig_args = Coq_nil; sig_res = Some $1} }
  | VOID
               { {sig_args = Coq_nil; sig_res = None} }
  | type_ MINUSGREATER signature
               { let s = $3 in {s with sig_args = Coq_cons($1, s.sig_args)} }
;

parameters:
    /* empty */                                 { Coq_nil }
  | parameter_list                              { $1 }
;

parameter_list:
    IDENT                                       { Coq_cons($1, Coq_nil) }
  | parameter_list COMMA IDENT                  { Coq_cons($3, $1) }
;

stack_declaration:
    /* empty */                                 { Z0 }
  | STACK INTLIT SEMICOLON                      { z_of_camlint $2 }
;

var_declarations:
    /* empty */                                 { Coq_nil }
  | var_declarations var_declaration            { CList.app $2 $1 }
;

var_declaration:
    VAR parameter_list SEMICOLON                { $2 }
;

/* Statements */

stmt:
    expr SEMICOLON                              { Sexpr $1 }
  | IDENT EQUAL expr SEMICOLON                  { Sassign($1, $3) }
  | IF LPAREN expr RPAREN stmts ELSE stmts      { Sifthenelse($3, $5, $7) }
  | IF LPAREN expr RPAREN stmts                 { Sifthenelse($3, $5, Sskip) }
  | LOOP stmts                                  { Sloop($2) }
  | LBRACELBRACE stmt_list RBRACERBRACE         { Sblock($2) }
  | EXIT SEMICOLON                              { Sexit O }
  | EXIT INTLIT SEMICOLON                       { Sexit (exitnum $2) }
  | RETURN SEMICOLON                            { Sreturn None }
  | RETURN expr SEMICOLON                       { Sreturn (Some $2) }
  | SWITCH LPAREN expr RPAREN LBRACE switch_cases RBRACE
                                                { mkswitch $3 $6 }
  | MATCH LPAREN expr RPAREN LBRACE match_cases RBRACE
                                                { mkmatch $3 $6 }
;

stmts:
    LBRACE stmt_list RBRACE                     { $2 }
  | stmt                                        { $1 }
;

stmt_list:
    /* empty */                                 { Sskip }
  | stmt stmt_list                              { Sseq($1, $2) }
;

switch_cases:
    DEFAULT COLON EXIT INTLIT SEMICOLON
           { ([], $4) }
  | CASE INTLIT COLON EXIT INTLIT SEMICOLON switch_cases
           { let (cases, dfl) = $7 in (($2, $5) :: cases, dfl) }
;

match_cases:
    /* empty */                                 { [] }
  | CASE INTLIT COLON stmt_list match_cases     { ($2, $4) :: $5 }
;

/* Expressions */

expr:
    LPAREN expr RPAREN                          { $2 }
  | IDENT                                       { Evar $1 }
  | INTLIT                                      { intconst $1 }
  | FLOATLIT                                    { Econst(Ofloatconst $1) }
  | STRINGLIT                                   { Econst(Oaddrsymbol($1, Int.zero)) }
  | AMPERSAND INTLIT                            { Econst(Oaddrstack(coqint_of_camlint $2)) }
  | MINUS expr    %prec p_uminus                { Eunop(Onegint, $2) }
  | MINUSF expr   %prec p_uminus                { Eunop(Onegf, $2) }
  | ABSF expr                                   { Eunop(Oabsf, $2) }
  | INTOFFLOAT expr                             { Eunop(Ointoffloat, $2) }
  | FLOATOFINT expr                             { Eunop(Ofloatofint, $2) }
  | FLOATOFINTU expr                            { Eunop(Ofloatofintu, $2) }
  | TILDE expr                                  { Eunop(Onotint, $2) }
  | BANG expr                                   { Eunop(Onotbool, $2) }
  | INT8S expr                                  { Eunop(Ocast8signed, $2) }
  | INT8U expr                                  { Eunop(Ocast8unsigned, $2) }
  | INT16S expr                                 { Eunop(Ocast16signed, $2) }
  | INT16U expr                                 { Eunop(Ocast16unsigned, $2) }
  | FLOAT32 expr                                { Eunop(Osingleoffloat, $2) }
  | ALLOC expr                                  { Ealloc $2 }
  | expr PLUS expr                              { Ebinop(Oadd, $1, $3) }
  | expr MINUS expr                             { Ebinop(Osub, $1, $3) }
  | expr STAR expr                              { Ebinop(Omul, $1, $3) }
  | expr SLASH expr                             { Ebinop(Odiv, $1, $3) }
  | expr PERCENT expr                           { Ebinop(Omod, $1, $3) }
  | expr SLASHU expr                            { Ebinop(Odivu, $1, $3) }
  | expr PERCENTU expr                          { Ebinop(Omodu, $1, $3) }
  | expr AMPERSAND expr                         { Ebinop(Oand, $1, $3) }
  | expr BAR expr                               { Ebinop(Oor, $1, $3) }
  | expr CARET expr                             { Ebinop(Oxor, $1, $3) }
  | expr LESSLESS expr                          { Ebinop(Oshl, $1, $3) }
  | expr GREATERGREATER expr                    { Ebinop(Oshr, $1, $3) }
  | expr GREATERGREATERU expr                   { Ebinop(Oshru, $1, $3) }
  | expr PLUSF expr                             { Ebinop(Oaddf, $1, $3) }
  | expr MINUSF expr                            { Ebinop(Osubf, $1, $3) }
  | expr STARF expr                             { Ebinop(Omulf, $1, $3) }
  | expr SLASHF expr                            { Ebinop(Odivf, $1, $3) }
  | expr EQUALEQUAL expr                        { Ebinop(Ocmp Ceq, $1, $3) }
  | expr BANGEQUAL expr                         { Ebinop(Ocmp Cne, $1, $3) }
  | expr LESS expr                              { Ebinop(Ocmp Clt, $1, $3) }
  | expr LESSEQUAL expr                         { Ebinop(Ocmp Cle, $1, $3) }
  | expr GREATER expr                           { Ebinop(Ocmp Cgt, $1, $3) }
  | expr GREATEREQUAL expr                      { Ebinop(Ocmp Cge, $1, $3) }
  | expr EQUALEQUALU expr                       { Ebinop(Ocmpu Ceq, $1, $3) }
  | expr BANGEQUALU expr                        { Ebinop(Ocmpu Cne, $1, $3) }
  | expr LESSU expr                             { Ebinop(Ocmpu Clt, $1, $3) }
  | expr LESSEQUALU expr                        { Ebinop(Ocmpu Cle, $1, $3) }
  | expr GREATERU expr                          { Ebinop(Ocmpu Cgt, $1, $3) }
  | expr GREATEREQUALU expr                     { Ebinop(Ocmpu Cge, $1, $3) }
  | expr EQUALEQUALF expr                       { Ebinop(Ocmpf Ceq, $1, $3) }
  | expr BANGEQUALF expr                        { Ebinop(Ocmpf Cne, $1, $3) }
  | expr LESSF expr                             { Ebinop(Ocmpf Clt, $1, $3) }
  | expr LESSEQUALF expr                        { Ebinop(Ocmpf Cle, $1, $3) }
  | expr GREATERF expr                          { Ebinop(Ocmpf Cgt, $1, $3) }
  | expr GREATEREQUALF expr                     { Ebinop(Ocmpf Cge, $1, $3) }
  | memory_chunk LBRACKET expr RBRACKET         { Eload($1, $3) }
  | memory_chunk LBRACKET expr RBRACKET EQUAL expr
                                                { Estore($1, $3, $6) }
  | expr LPAREN expr_list RPAREN COLON signature
                                                { Ecall($6, $1, $3) }
  | expr AMPERSANDAMPERSAND expr                { andbool $1 $3 }
  | expr BARBAR expr                            { orbool $1 $3 }
  | expr QUESTION expr COLON expr               { Econdition($1, $3, $5) }
  | LET expr IN expr %prec p_let                { Elet($2, $4) }
  | DOLLAR INTLIT                               { Eletvar (nat_of_camlint $2) }
;

expr_list:
    /* empty */                                 { Enil }
  | expr_list_1                                 { $1 }
;

expr_list_1:
    expr                     %prec COMMA        { Econs($1, Enil) }
  | expr COMMA expr_list_1                      { Econs($1, $3) }
;

memory_chunk:
    INT8S                                       { Mint8signed }
  | INT8U                                       { Mint8unsigned }
  | INT16S                                      { Mint16signed }
  | INT16U                                      { Mint16unsigned }
  | INT32                                       { Mint32 }
  | INT                                         { Mint32 }
  | FLOAT32                                     { Mfloat32 }
  | FLOAT64                                     { Mfloat64 }
  | FLOAT                                       { Mfloat64 }
;

/* Types */

type_:
    INT                                         { Tint }
  | FLOAT                                       { Tfloat }
;