aboutsummaryrefslogtreecommitdiffstats
path: root/caml/CMparser.mly
diff options
context:
space:
mode:
Diffstat (limited to 'caml/CMparser.mly')
-rw-r--r--caml/CMparser.mly541
1 files changed, 0 insertions, 541 deletions
diff --git a/caml/CMparser.mly b/caml/CMparser.mly
deleted file mode 100644
index 25fb0321..00000000
--- a/caml/CMparser.mly
+++ /dev/null
@@ -1,541 +0,0 @@
-/* *********************************************************************/
-/* */
-/* The Compcert verified compiler */
-/* */
-/* Xavier Leroy, INRIA Paris-Rocquencourt */
-/* */
-/* Copyright Institut National de Recherche en Informatique et en */
-/* Automatique. All rights reserved. This file is distributed */
-/* under the terms of the GNU General Public License as published by */
-/* the Free Software Foundation, either version 2 of the License, or */
-/* (at your option) any later version. This file is also distributed */
-/* under the terms of the INRIA Non-Commercial License Agreement. */
-/* */
-/* *********************************************************************/
-
-%{
-open Datatypes
-open CList
-open Camlcoq
-open BinPos
-open BinInt
-open Integers
-open AST
-open Cminor
-
-(** Naming function calls in expressions *)
-
-type rexpr =
- | Rvar of ident
- | Rconst of constant
- | Runop of unary_operation * rexpr
- | Rbinop of binary_operation * rexpr * rexpr
- | Rload of memory_chunk * rexpr
- | Rcondition of rexpr * rexpr * rexpr
- | Rcall of signature * rexpr * rexpr list
- | Ralloc of rexpr
-
-let temp_counter = ref 0
-
-let temporaries = ref []
-
-let mktemp () =
- incr temp_counter;
- let n = Printf.sprintf "__t%d" !temp_counter in
- let id = intern_string n in
- temporaries := id :: !temporaries;
- id
-
-let convert_accu = ref []
-
-let rec convert_rexpr = function
- | Rvar id -> Evar id
- | Rconst c -> Econst c
- | Runop(op, e1) -> Eunop(op, convert_rexpr e1)
- | Rbinop(op, e1, e2) ->
- let c1 = convert_rexpr e1 in
- let c2 = convert_rexpr e2 in
- Ebinop(op, c1, c2)
- | Rload(chunk, e1) -> Eload(chunk, convert_rexpr e1)
- | Rcondition(e1, e2, e3) ->
- let c1 = convert_rexpr e1 in
- let c2 = convert_rexpr e2 in
- let c3 = convert_rexpr e3 in
- Econdition(c1, c2, c3)
- | Rcall(sg, e1, el) ->
- let c1 = convert_rexpr e1 in
- let cl = convert_rexpr_list el in
- let t = mktemp() in
- convert_accu := Scall(Some t, sg, c1, cl) :: !convert_accu;
- Evar t
- | Ralloc e1 ->
- let c1 = convert_rexpr e1 in
- let t = mktemp() in
- convert_accu := Salloc(t, c1) :: !convert_accu;
- Evar t
-
-and convert_rexpr_list = function
- | [] -> []
- | e1 :: el ->
- let c1 = convert_rexpr e1 in
- let cl = convert_rexpr_list el in
- c1 :: cl
-
-let rec prepend_seq stmts last =
- match stmts with
- | [] -> last
- | s1 :: sl -> prepend_seq sl (Sseq(s1, last))
-
-let mkeval e =
- convert_accu := [];
- match e with
- | Rcall(sg, e1, el) ->
- let c1 = convert_rexpr e1 in
- let cl = convert_rexpr_list el in
- prepend_seq !convert_accu (Scall(None, sg, c1, cl))
- | _ ->
- ignore (convert_rexpr e);
- prepend_seq !convert_accu Sskip
-
-let mkassign id e =
- convert_accu := [];
- match e with
- | Rcall(sg, e1, el) ->
- let c1 = convert_rexpr e1 in
- let cl = convert_rexpr_list el in
- prepend_seq !convert_accu (Scall(Some id, sg, c1, cl))
- | Ralloc(e1) ->
- let c1 = convert_rexpr e1 in
- prepend_seq !convert_accu (Salloc(id, c1))
- | _ ->
- let c = convert_rexpr e in
- prepend_seq !convert_accu (Sassign(id, c))
-
-let mkstore chunk e1 e2 =
- convert_accu := [];
- let c1 = convert_rexpr e1 in
- let c2 = convert_rexpr e2 in
- prepend_seq !convert_accu (Sstore(chunk, c1, c2))
-
-let mkifthenelse e s1 s2 =
- convert_accu := [];
- let c = convert_rexpr e in
- prepend_seq !convert_accu (Sifthenelse(c, s1, s2))
-
-let mkreturn_some e =
- convert_accu := [];
- let c = convert_rexpr e in
- prepend_seq !convert_accu (Sreturn (Some c))
-
-let mktailcall sg e1 el =
- convert_accu := [];
- let c1 = convert_rexpr e1 in
- let cl = convert_rexpr_list el in
- prepend_seq !convert_accu (Stailcall(sg, c1, cl))
-
-(** Other constructors *)
-
-let intconst n =
- Rconst(Ointconst(coqint_of_camlint n))
-
-let andbool e1 e2 =
- Rcondition(e1, e2, intconst 0l)
-let orbool e1 e2 =
- Rcondition(e1, intconst 1l, e2)
-
-let exitnum n = nat_of_camlint(Int32.pred n)
-
-let mkswitch expr (cases, dfl) =
- convert_accu := [];
- let c = convert_rexpr expr in
- let rec mktable = function
- | [] -> []
- | (key, exit) :: rem ->
- Coq_pair(coqint_of_camlint key, exitnum exit) :: mktable rem in
- prepend_seq !convert_accu (Sswitch(c, 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] -> []
- | (key, action) :: rem ->
- 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 =
- convert_accu := [];
- let c = convert_rexpr expr in
- let s =
- match cases with
- | [] -> Sskip (* ??? *)
- | [key, action] -> action
- | _ -> mkmatch_aux c cases in
- prepend_seq !convert_accu s
-
-%}
-
-%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 INTUOFFLOAT
-%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 TAILCALL
-%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 INTUOFFLOAT 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 */ { [] }
- | global_declarations global_declaration { $2 :: $1 }
-;
-
-global_declaration:
- VAR STRINGLIT LBRACKET INTLIT RBRACKET
- { Coq_pair(Coq_pair($2, [ Init_space (z_of_camlint $4) ]), ()) }
-;
-
-proc_list:
- /* empty */ { [] }
- | proc_list proc { $2 :: $1 }
-;
-
-/* Procedures */
-
-proc:
- STRINGLIT LPAREN parameters RPAREN COLON signature
- LBRACE
- stack_declaration
- var_declarations
- stmt_list
- RBRACE
- { let tmp = !temporaries in
- temporaries := [];
- temp_counter := 0;
- Coq_pair($1,
- Internal { fn_sig = $6;
- fn_params = CList.rev $3;
- fn_vars = CList.rev (CList.app tmp $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 = []; sig_res = Some $1} }
- | VOID
- { {sig_args = []; sig_res = None} }
- | type_ MINUSGREATER signature
- { let s = $3 in {s with sig_args = $1 :: s.sig_args} }
-;
-
-parameters:
- /* empty */ { [] }
- | parameter_list { $1 }
-;
-
-parameter_list:
- IDENT { $1 :: [] }
- | parameter_list COMMA IDENT { $3 :: $1 }
-;
-
-stack_declaration:
- /* empty */ { Z0 }
- | STACK INTLIT SEMICOLON { z_of_camlint $2 }
-;
-
-var_declarations:
- /* empty */ { [] }
- | var_declarations var_declaration { CList.app $2 $1 }
-;
-
-var_declaration:
- VAR parameter_list SEMICOLON { $2 }
-;
-
-/* Statements */
-
-stmt:
- expr SEMICOLON { mkeval $1 }
- | IDENT EQUAL expr SEMICOLON { mkassign $1 $3 }
- | memory_chunk LBRACKET expr RBRACKET EQUAL expr SEMICOLON
- { mkstore $1 $3 $6 }
- | IF LPAREN expr RPAREN stmts ELSE stmts { mkifthenelse $3 $5 $7 }
- | IF LPAREN expr RPAREN stmts { mkifthenelse $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 { mkreturn_some $2 }
- | SWITCH LPAREN expr RPAREN LBRACE switch_cases RBRACE
- { mkswitch $3 $6 }
- | MATCH LPAREN expr RPAREN LBRACE match_cases RBRACE
- { mkmatch $3 $6 }
- | TAILCALL expr LPAREN expr_list RPAREN COLON signature SEMICOLON
- { mktailcall $7 $2 $4 }
-;
-
-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 { Rvar $1 }
- | INTLIT { intconst $1 }
- | FLOATLIT { Rconst(Ofloatconst $1) }
- | STRINGLIT { Rconst(Oaddrsymbol($1, Int.zero)) }
- | AMPERSAND INTLIT { Rconst(Oaddrstack(coqint_of_camlint $2)) }
- | MINUS expr %prec p_uminus { Rbinop(Osub, intconst 0l, $2) } /***FIXME***/
- | MINUSF expr %prec p_uminus { Runop(Onegf, $2) }
- | ABSF expr { Runop(Oabsf, $2) }
- | INTOFFLOAT expr { Runop(Ointoffloat, $2) }
- | INTUOFFLOAT expr { Runop(Ointuoffloat, $2) }
- | FLOATOFINT expr { Runop(Ofloatofint, $2) }
- | FLOATOFINTU expr { Runop(Ofloatofintu, $2) }
- | TILDE expr { Runop(Onotint, $2) }
- | BANG expr { Runop(Onotbool, $2) }
- | INT8S expr { Runop(Ocast8signed, $2) }
- | INT8U expr { Runop(Ocast8unsigned, $2) }
- | INT16S expr { Runop(Ocast16signed, $2) }
- | INT16U expr { Runop(Ocast16unsigned, $2) }
- | FLOAT32 expr { Runop(Osingleoffloat, $2) }
- | expr PLUS expr { Rbinop(Oadd, $1, $3) }
- | expr MINUS expr { Rbinop(Osub, $1, $3) }
- | expr STAR expr { Rbinop(Omul, $1, $3) }
- | expr SLASH expr { Rbinop(Odiv, $1, $3) }
- | expr PERCENT expr { Rbinop(Omod, $1, $3) }
- | expr SLASHU expr { Rbinop(Odivu, $1, $3) }
- | expr PERCENTU expr { Rbinop(Omodu, $1, $3) }
- | expr AMPERSAND expr { Rbinop(Oand, $1, $3) }
- | expr BAR expr { Rbinop(Oor, $1, $3) }
- | expr CARET expr { Rbinop(Oxor, $1, $3) }
- | expr LESSLESS expr { Rbinop(Oshl, $1, $3) }
- | expr GREATERGREATER expr { Rbinop(Oshr, $1, $3) }
- | expr GREATERGREATERU expr { Rbinop(Oshru, $1, $3) }
- | expr PLUSF expr { Rbinop(Oaddf, $1, $3) }
- | expr MINUSF expr { Rbinop(Osubf, $1, $3) }
- | expr STARF expr { Rbinop(Omulf, $1, $3) }
- | expr SLASHF expr { Rbinop(Odivf, $1, $3) }
- | expr EQUALEQUAL expr { Rbinop(Ocmp Ceq, $1, $3) }
- | expr BANGEQUAL expr { Rbinop(Ocmp Cne, $1, $3) }
- | expr LESS expr { Rbinop(Ocmp Clt, $1, $3) }
- | expr LESSEQUAL expr { Rbinop(Ocmp Cle, $1, $3) }
- | expr GREATER expr { Rbinop(Ocmp Cgt, $1, $3) }
- | expr GREATEREQUAL expr { Rbinop(Ocmp Cge, $1, $3) }
- | expr EQUALEQUALU expr { Rbinop(Ocmpu Ceq, $1, $3) }
- | expr BANGEQUALU expr { Rbinop(Ocmpu Cne, $1, $3) }
- | expr LESSU expr { Rbinop(Ocmpu Clt, $1, $3) }
- | expr LESSEQUALU expr { Rbinop(Ocmpu Cle, $1, $3) }
- | expr GREATERU expr { Rbinop(Ocmpu Cgt, $1, $3) }
- | expr GREATEREQUALU expr { Rbinop(Ocmpu Cge, $1, $3) }
- | expr EQUALEQUALF expr { Rbinop(Ocmpf Ceq, $1, $3) }
- | expr BANGEQUALF expr { Rbinop(Ocmpf Cne, $1, $3) }
- | expr LESSF expr { Rbinop(Ocmpf Clt, $1, $3) }
- | expr LESSEQUALF expr { Rbinop(Ocmpf Cle, $1, $3) }
- | expr GREATERF expr { Rbinop(Ocmpf Cgt, $1, $3) }
- | expr GREATEREQUALF expr { Rbinop(Ocmpf Cge, $1, $3) }
- | memory_chunk LBRACKET expr RBRACKET { Rload($1, $3) }
- | expr AMPERSANDAMPERSAND expr { andbool $1 $3 }
- | expr BARBAR expr { orbool $1 $3 }
- | expr QUESTION expr COLON expr { Rcondition($1, $3, $5) }
- | expr LPAREN expr_list RPAREN COLON signature{ Rcall($6, $1, $3) }
- | ALLOC expr { Ralloc $2 }
-;
-
-expr_list:
- /* empty */ { [] }
- | expr_list_1 { $1 }
-;
-
-expr_list_1:
- expr %prec COMMA { $1 :: [] }
- | expr COMMA expr_list_1 { $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 }
-;
generated by cgit (git 2.34.1) at 2024-07-24 23:06:32 +0000