/* $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 FLOATLIT %token FLOATOFINT %token FLOATOFINTU %token GREATER %token GREATERF %token GREATERU %token GREATEREQUAL %token GREATEREQUALF %token GREATEREQUALU %token GREATERGREATER %token GREATERGREATERU %token IDENT %token IF %token IN %token INT %token INT16S %token INT16U %token INT32 %token INT8S %token INT8U %token 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 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 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 } ;