%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% This file implements the operational semantics of The Simple MIRA %%%%%%%%%%
% language.
%
% Author: Fernando Magno Quintao Pereira, 03-26-2007
%
% R = (cons_exp (psd z) (cons_exp (psd z) (cons_exp (psd z) (cons_exp (psd z) nil_exp))))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
not_zero : nat -> type.
%mode not_zero +N.

not_zero_ : not_zero (s N).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% The values in SMIRA semantics %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% The type of a pseudo
psd : nat -> exp.

% This symbol denotes elements that have no influence on the register
% allocation process.
blt : exp.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% The operands %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% A register is a pair, where the first element denotes a position in the
% register bank, and the second denotes the pseudo that is stored in that
% position.
% For example, reg 4 2 denotes that physical register R4 is holding the value
% of pseudo P2.
reg : nat -> nat -> exp.

% This is the label of basic blocks. A program is a list of basic blocks,
% each of them addressed by a single label.
lbl : nat -> exp.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Rules for evaluating operands: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

eval: exps -> exp -> exp -> type.
%mode eval +R +Reg -V.

eval_blt : eval R blt blt.

eval_reg: eval R (reg Nr Np) (psd Np)
	<- proj_exp R Nr (psd Np)
	<- not_zero Np.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Instructions: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Instruction sequence:
i_seq : exps -> exp.

% Individual instructions:
i_mov : exp -> exp -> exp.

i_cnd : exp -> exp -> exp.

i_jmp : exp -> exp.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Evaluation of instructions: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% The step function takes a list R that represents the bank of registers, a
% code heap C, that represents the program under evaluation, and
% a list I that represents the sequence of instructions to be processed. It
% then evaluates the first instruction in the sequence.

step: exps -> exps -> exps -> exps -> exps -> exps -> type.
%mode step +C +R +I -C' -R' -I'.

step_mov : step C R (cons_exp (i_mov (reg Nr Np) O) I) C R' I
	<- eval R O V
	<- update_exp R (psd Np) Nr R' P.

step_jmp : step C R (cons_exp (i_jmp (lbl N)) nil_exp) C R I'
	<- proj_exp C N (i_seq I').

step_jeq : step C R (cons_exp (i_cnd (reg Nr Np) (lbl N)) I) C R I
	<- eval R (reg Nr Np) V.

step_jne : step C R (cons_exp (i_cnd (reg Nr Np) (lbl N)) I) C R I'
	<- eval R (reg Nr Np) V
	<- proj_exp C N (i_seq I').