%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Type system for verification of register allocation settings.
%%
%% Author: Fernando Magno Quintao Pereira, 03-26-2007
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Base types:

tp: type.

% Const is the base type of the bullet (blt) operand.
Const : tp.

% Pseudo is the base type of a register.
Pseudo : nat -> tp.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% The type of a code sequence is a list containing the environment that the
% code sequence expects to receive:

CodeExp : exps -> exp.

CodeTp : exps -> tp.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
sub: tp -> tp -> type.
%mode sub *T *T'.
%tabled sub.

sub_empbk : sub (CodeTp nil_exp) (CodeTp nil_exp).

sub_rzero : sub (CodeTp (cons_exp (psd N) G)) (CodeTp (cons_exp (psd z) G'))
	<- sub (CodeTp G) (CodeTp G').

sub_rnotz : sub (CodeTp (cons_exp (psd (s N)) G)) (CodeTp (cons_exp (psd (s N)) G'))
	<- sub (CodeTp G) (CodeTp G').


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Types of operands of instructions:

tpop: exps -> exp -> tp -> type.

tpop_gab : tpop G blt Const.

tpop_reg : tpop G (reg Nr Np) (Pseudo Np)
	<- proj_exp G Nr (psd Np)
	<- not_zero Np.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Type of a label:

tplb : exps -> exp -> tp -> type.

tplb_ : tplb Psi (lbl N) (CodeTp R)
	<- proj_exp Psi N (CodeExp R).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Types of instructions:

% An instruction receives a type environment Gamma_0 (G0), and produces a
% type environment Gamma_1 (G1). Thus, the type of an instruction is a
% function G0 -> G1.
InstType : tp -> tp -> tp.

tpIns : exps -> exp -> tp -> type.

tpIns_mov : tpIns Psi (i_mov (reg Nr Np) O) (InstType (CodeTp G0) (CodeTp G1))
	<- tpop G0 O TO
	<- not_zero Np
	<- update_exp G0 (psd Np) Nr G1 P'.

tpIns_cnd : tpIns Psi (i_cnd (reg Nr Np) (lbl N)) (InstType (CodeTp G) (CodeTp G))
	<- tpop G (reg Nr Np) TO
	<- tplb Psi (lbl N) (CodeTp G')
	<- sub (CodeTp G) (CodeTp G').


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Types of instruction sequences:
% tpSeq Psi |- (i;I) : Gamma

tpSeq : exps -> exps -> tp -> type.

tpSeq_seq : tpSeq Psi (cons_exp Inst I) (CodeTp G)
	<- tpIns Psi Inst (InstType (CodeTp G) (CodeTp G'))
	<- tpSeq Psi I (CodeTp G').

tpSeq_jmp : tpSeq Psi (cons_exp (i_jmp (lbl N)) nil_exp) (CodeTp G)
	<- tplb Psi (lbl N) (CodeTp G')
	<- sub (CodeTp G) (CodeTp G').


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Type of the Bank of Registers:
tpRegBank : exps -> tp -> type.

tpRegBank_nil : tpRegBank nil_exp (CodeTp nil_exp).

tpRegBank_con : tpRegBank (cons_exp (psd N) R') (CodeTp (cons_exp (psd N) G'))
	<- tpRegBank R' (CodeTp G').


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Type of the code Heap:
CodeHeapTp : exps -> tp.

tpCodeHeapAux : exps -> exps -> tp -> type.

tpCodeHeapAux_nil : tpCodeHeapAux Psi nil_exp (CodeHeapTp nil_exp).

tpCodeHeapAux_con : tpCodeHeapAux Psi (cons_exp (i_seq I) C) (CodeHeapTp (cons_exp (CodeExp G) Psi'))
	<- tpSeq Psi I (CodeTp G)
	<- tpCodeHeapAux Psi C (CodeHeapTp Psi').

tpCodeHeap: exps -> exps -> type.

tpCodeHeap_ : tpCodeHeap Psi C
	<- tpCodeHeapAux Psi C (CodeHeapTp Psi).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Type of a machine state:

tpState : exps -> exps -> exps -> type.

tpState_ : tpState C R I
	<- tpCodeHeap Psi C
	<- tpRegBank R (CodeTp G)
	<- tpSeq Psi I (CodeTp G')
	<- sub (CodeTp G) (CodeTp G').