k

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 "%" AExp 							[left, strict, mod]
				| "(" AExp ")"  							[bracket]

	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]
				| "(" BExp ")"   							[bracket]

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

	syntax Stmt ::= Block
                | "return" ";"
				| "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" Id
	syntax FunDecl ::= "function" Id "(" VarDecls ")" Block
	syntax VarDecls ::= List{VarDecl, ","}
	syntax Params ::= List{AExp, ","} 						[strict]

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

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 ; => dummy ...</k>
		<env> _ => Rho  </env>
		<fstack> (ListItem(Rho) => .List) ...</fstack>
		<return> _ => dummy </return>

	// AExp
	rule I1:Int + I2:Int => I1 +Int I2 								[plus]
	rule I1:Int - I2:Int => I1 -Int I2 								[minus]
	rule I1:Int * I2:Int => I1 *Int I2 								[mult]
	rule I1:Int / I2:Int => I1 /Int I2 requires I2 =/=Int 0	 		[div]
	rule I1:Int % I2:Int => I1 %Int I2 								[mod]

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

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

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

	// print cu --output none
	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

	// sequences
	rule S1:Stmt S2:Stmt => S1 ~> S2

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

	// 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: loop unrolling
	rule while (B) S => if (B) { S while (B) S } else { }
	// repeat [] until [] end
	rule repeat S until (B) end => S if (B) { S while (B) S} else { }

endmodule