plp

module IMP-SYNTAX
    syntax AExp ::= Int | Id | String
                | "++" Id
                | Id "++"
                | "read" "(" ")"
                | Id "(" Params ")"  [strict(2)]
                | AExp "/" AExp      [left, strict, div]
                | AExp "*" AExp      [left, strict, mult]
                > AExp "+" AExp      [left, strict, plus]
                | AExp "-" AExp      [left, strict, minus]
                | "(" AExp ")"       [bracket]
                | AExp "=" AExp

    syntax BExp ::= Bool
                | "!" BExp       [strict]
                | BExp "&&" BExp [strict(1)]
                | BExp "||" BExp [strict(1)]
                | AExp "<=" AExp [strict]
                | AExp "!=" AExp [strict]
                | AExp ">=" AExp [strict]
                | AExp "==" AExp [strict]
                | AExp "<" AExp  [strict]
                | AExp ">" AExp  [strict]
                | "(" BExp ")"   [bracket]

    syntax Block ::= "{" "}" | "{" Stmt "}"

        syntax Ids ::= List{Id, ","}

    syntax Stmt ::= Block
                | "return" ";"
                | "int" Id ";"
                | Decl
                | "return" AExp ";"                     [strict]
                | "print" "(" AExp ")" ";"              [strict]
                | Id "=" AExp ";"                       [strict(2)]
                | "if" "(" BExp ")" Stmt "else" Stmt    [strict(1)]
                | BExp "?" Stmt ":" Stmt                [strict(1)]
                | "while" "(" BExp ")" Stmt             [strict(1)]
                | "repeat" Stmt "until" BExp "end"
                > Stmt Stmt [left]

    syntax Pgm ::= List{Decl,";"}
    syntax Decl ::= VarDecl | FunDecl
    syntax VarDecl ::= "int" Exps ";" | "int" Ids ";"

     syntax Decl ::= "int" Exps ";" | FunDecl

    syntax FunDecl ::= "function" Id "(" VarDecls ")" Block
    syntax VarDecls ::= List{VarDecl, ","}
    syntax Params ::= List{AExp, ","} [strict]

    syntax Exps ::= List{AExp,","}          [strict]

    syntax Id ::= "main" [token]
    syntax KItem ::= "execute"


    rule int E1:AExp, E2:AExp, Es:Exps; => int E1; int E2, Es;          [macro]
        rule int X:Id = E; => int X; X = E;                             [macro]

endmodule

module IMP
    imports IMP-SYNTAX

    configuration <T>
            <k> $PGM:Pgm ~> execute </k>
            <env> .Map </env>
            <store> .Map </store>
            <in stream="stdin"> .List </in>
            <out stream="stdout"> .List </out>
            <fstack> .List </fstack>
            <return> dummy </return>
            </T>

    syntax Val ::= Int | Bool | "dummy" | String
    syntax Vals ::= List{Val, ","}
    syntax KResult ::= Val | Vals

    syntax Params ::= Vals
    syntax AExp ::= Val

    // sequecing declarations
    rule D:Decl ; Ds:Pgm => D ~> Ds

    // var decl
    //rule <k> (int X:Id => .)  ...</k>
    //  <env> Rho:Map => Rho[X <- !L:Int] </env>
    //  <store> Sigma => Sigma[!L <- 0] </store>

    // fun decl
    syntax Lambda ::= "lambda" "(" VarDecls "," Block ")"
    rule <k> (function X:Id ( P:VarDecls ) B => .) ...</k>
        <env> Rho:Map => Rho[X <- !L:Int] </env>
        <store> Sigma:Map => Sigma[!L <- lambda(P, B)] </store>

    // execute
    rule (.Pgm ~> execute) => main(.Params)

    // function call setup
    syntax KItem ::= "saveEnv"
    syntax KItem ::= "mkDecl" "(" VarDecls "," Vals ")"
    rule <k> X:Id (Vs:Vals) => saveEnv ~> mkDecl(P, Vs) ~> B ...</k>
        <env>... X |-> L:Int </env>
        <store>... L |-> lambda(P, B) ...</store>

    // save environment
    rule <k> saveEnv => . ...</k>
        <env> Rho </env>
        <fstack> (.List => ListItem(Rho)) ...</fstack>

    // make declarations
    rule <k> mkDecl((int X:Id, P:VarDecls), (V:Val, Vs:Vals)) => mkDecl(P, Vs) ...</k>
        <env> Rho:Map => Rho[X <- !L:Int] </env>
        <store> Sigma:Map => Sigma[!L <- V] </store>

    rule mkDecl(.VarDecls, .Vals) => .

    // return
    rule <k> return V:Val ; => V ...</k>
        <env> _ => Rho  </env>
        <fstack> (ListItem(Rho) => .List) ...</fstack>
        <return> _ => V </return>

    rule <k> return ; => . ...</k>
        <env> _ => Rho  </env>
        <fstack> (ListItem(Rho) => .List) ...</fstack>
        <return> _ => dummy </return>

    // AExp
    rule I1:Int + I2:Int => I1 +Int I2
    rule I1:Int - I2:Int => I1 -Int I2
    rule I1:Int * I2:Int => I1 *Int I2
    rule I1:Int / I2:Int => I1 /Int I2 requires I2 =/=Int 0

    // ++x
    rule <k> (++X:Id => I:Int +Int 1) ...</k>
        <env>... X |-> L:Int ...</env>
        <store>... L |-> (I:Int => I +Int 1) ...</store>
    //x++
    rule <k> (X:Id++ => I:Int) ...</k>
        <env>... X |-> L:Int ...</env>
        <store>... L |-> (I:Int => I +Int 1) ...</store>

    // read
    rule <k> (read() => I)...</k>
        <in> (ListItem(I:Int) => .List) ...</in>

    // print
    syntax Printable ::= Int | String
    syntax AExp ::= Printable
    rule <k> (print(I:Printable); => .) ...</k>
        <out>... (.List => ListItem(I)) </out>

        syntax Printable ::= Int | String
        syntax AExp ::= Printable
        rule <k> (print(I:Printable); => .) ...</k>
            <out>... (.List => ListItem(I)) </out>


    // BExp
    rule ! false => true
    rule ! true  => false
    rule true  && B => B
    rule false && _ => false
    rule false  || B => B
    rule true || _ => true
    rule I1:Int <= I2:Int => I1 <=Int I2
    rule I1:Int >= I2:Int => I1 >=Int I2
    rule I1:Int < I2:Int => I1 <Int I2
    rule I1:Int > I2:Int => I1 >Int I2
        rule I1:Int == I2:Int => I1 ==Int I2
        rule I1:Int != I2:Int => I1 =/=Int I2
    // sequences
    rule S1:Stmt S2:Stmt => S1 ~> S2


    // var declarations
        rule <k> int (X, Xs => Xs) ; ...</k>
        <env> Rho:Map  => Rho[X <- !L:Int] </env>
        <store> Sigma:Map (. => (!L |-> 0)) </store>
        rule int .Ids ; => .


    // assignment
    rule <k> (X = V:Int ; => .) ...</k>
        <env>... X |-> L ...</env>
        <store>... L |-> (_ => V) ...</store>

    // if
    rule if (true)  S else _ => S
    rule if (false) _ else S => S
    // ? :
    rule (true) ? S : _ => S
    rule (false) ? _ : S => S

    // lookup
    rule <k> (X => V) ...</k>
        <env>... X |-> L:Int ...</env>
        <store>... L |-> V ...</store>

    // blocks
    rule { } => .
    rule { S:Stmt } => S

    //while
    rule while (B) S => if (B) { S while (B) S } else { }
    // repeat { ... }  until (cond) end
    rule repeat S until (B) end => S if (B) { S while (B) S} else { }

endmodule