fun-test.elf

%{ Small playtoy language for
   working with function calls

   TODO: add F and Gamma!

}%

%{ ** SYNTAX ** }%

nat : type.

z : nat.
s : nat -> nat.

fid : type.
fid/ : nat -> type.

tm : type.

tm/skip : tm.

tm/fcall : fid -> tm.
tm/semi  : tm -> tm -> tm.

fun : type.
fun/ : fid -> tm -> fun.


fun-list : type.

fun-list/z : fun-list.
fun-list/s : fun -> fun-list -> fun-list.

pgm : type.

pgm/ : fun-list -> tm -> pgm.

%{ ** Lookup ** }%

lookup : fid -> fun-list -> tm -> type.
%mode lookup +F +FL -T.

%{ ** STATIC SEMANTICS ** }%
fun-list-lookup : fun-list -> fid -> tm -> type.
%mode fun-list-lookup +FL +Fid -T.

fun-list-lookup/hit : fun-list-lookup (fun-list/s (fun/ N B) _) N B.

fun-list-lookup/miss : fun-list-lookup (fun-list/s (fun/ K _) R) N B
			<- fun-list-lookup R N B.

value : tm -> type.

value/skip : value tm/skip.



%{ ** "TYPES" ** }%

funl : fun-list -> type.
%mode funl +FL.

gamma : type.

gammal : gamma -> type.

gamma/z : gamma.
gamma/s : fid -> gamma -> gamma.

gamma-lookup : fid -> gamma -> type.
gamma-lookup/hit : gamma-lookup F (gamma/s F _).
gamma-lookup/miss : gamma-lookup F (gamma/s _ R)
		     <- gamma-lookup F R.

valid : fun-list -> gamma -> type.

valid/z : valid fun-list/z gamma/z.
valid/s : valid (fun-list/s (fun/ Fid _) RF) (gamma/s _ RG)
	   <- gammal GL
	   <- gamma-lookup Fid GL
	   <- valid RF RG.

wellformed : tm -> type.

wellformed/skip : wellformed tm/skip.

wellformed/semi : wellformed (tm/semi T1 T2)
		   <- wellformed T1
		   <- wellformed T2.

wellformed/fcall : wellformed (tm/fcall F)
		    <- funl FL
		    <- fun-list-lookup FL F _.

wellformed-pgm : pgm -> type.

wellformed-pgm/ : wellformed-pgm (pgm/ _ T)
		   <- wellformed T.

valid-fun : fun-list -> type.

valid-fun/z : valid-fun fun-list/z.

valid-fun/s : valid-fun (fun-list/s (fun/ F T) R)
	       <- valid-fun R
	       <- wellformed T.

vf-map : {FL} valid-fun FL -> type.
%mode vf-map +FL -VF.

vl-map_0 : vf-map fun-list/z valid-fun/z.

valid-pgm : pgm -> type.

valid-pgm/ : valid-pgm (pgm/ FL T)
	      <- valid-fun FL.

%{ ** DYNAMIC SEMANTICS ** }%
step-tm : tm -> tm -> type.

step-tm/semi : step-tm (tm/semi B1 B2) (tm/semi B1' B2)
		  <- step-tm B1 B1'.

step-tm/fcall : step-tm (tm/fcall Fid) B1
		 <- funl FL
		 <- fun-list-lookup FL Fid B1.

step-tm/skip : step-tm (tm/semi tm/skip B) B.

step-pgm : pgm -> pgm -> type.

step-pgm/ : step-pgm (pgm/ F T) (pgm/ F T')
	     <- step-tm T T'.

steps : pgm -> pgm -> type.

steps/0 : steps P P.

steps/s : steps P P'
	   <- step-pgm P P''
	   <- steps P'' P'.

steps-to : pgm -> pgm -> type.

steps-to/ : steps-to P (pgm/ X V)
	     <- steps P (pgm/ X V)
	     <- value V.


%{ ** PROPERTIES ** }%

pgood : tm -> type.

pgood/val : pgood V
	     <- value V.

pgood/step : pgood T
	      <- step-tm T T'.

pgood-pgm : pgm -> type.

pgood-pgm/ : pgood-pgm (pgm/ _ B)
	      <- pgood B.

progress-tm-semi : pgood T -> pgood (tm/semi T T2) -> type.
%mode +{T : tm}
      +{T2 : tm}
      +{PGT : pgood T}
      -{PGG : pgood (tm/semi T T2)}
      progress-tm-semi PGT PGG.

- : progress-tm-semi (pgood/step SP) (pgood/step (step-tm/semi SP)).

- : progress-tm-semi (pgood/val value/skip) (pgood/step step-tm/skip).


progress-tm : {T : tm} wellformed T -> pgood T -> type.
%mode progress-tm +T +WP -Good.

- : progress-tm tm/skip _ (pgood/val value/skip).

- : progress-tm (tm/semi T1 T2) (wellformed/semi WP2 WP1) PG
     <- progress-tm T1 WP1 PG1
     <- progress-tm-semi PG1 PG.

- : progress-tm (tm/fcall F) (wellformed/fcall Lookup Exist)
       (pgood/step (step-tm/fcall Lookup Exist)).

progress : {P : pgm} wellformed-pgm P -> pgood-pgm P -> type.
%mode progress +P +WP -Good.

- : progress (pgm/ Funs T) (wellformed-pgm/ WP) (pgood-pgm/ Q)
     <- progress-tm T WP Q.

valid-lookup : fun-list-lookup FL F T -> valid-fun FL -> wellformed T -> type.
%mode valid-lookup +FLL +VF -WF.

- : valid-lookup fun-list-lookup/hit (valid-fun/s WF _) WF.

- : valid-lookup (fun-list-lookup/miss LL) (valid-fun/s _ S) Q
     <- valid-lookup LL S Q.

preservation-tm : fun-list -> wellformed T -> step-tm T T' -> wellformed T' -> type.
%mode preservation-tm +FL +WP +SP -WP'.

- : preservation-tm FL (wellformed/semi WP2 WP1) step-tm/skip WP2.

- : preservation-tm FL (wellformed/semi WP2 WP1) (step-tm/semi SP) (wellformed/semi WP2 WP1')
     <- preservation-tm FL WP1 SP WP1'.

- : preservation-tm FL (wellformed/fcall Lookup Exist) (step-tm/fcall Lookup Exist) Q
     <- vf-map FL VF
     <- valid-lookup Lookup VF Q.

preservation : {P} wellformed-pgm P -> valid-pgm P -> step-pgm P P' -> wellformed-pgm P' -> type.
%mode preservation +P +WP +VP +SP -WP'.

- : preservation (pgm/ FL T) (wellformed-pgm/ WP) (valid-pgm/ VF) (step-pgm/ SP)
%%
     (wellformed-pgm/ WP')
     <- (vf-map FL VF -> preservation-tm FL WP SP WP').

%block vf-block : some {FL : fun-list} {VF : valid-fun FL} block {vfm : vf-map FL VF}.

%worlds (vf-block) (funl _).
%worlds (vf-block) (vf-map _ _).
%worlds (vf-block) (valid-lookup _ _ _).
%worlds (vf-block) (preservation-tm _ _ _ _).
%worlds (vf-block) (preservation _ _ _ _ _).

%total FL (valid-lookup FL _ _).
%total F (vf-map F _).
%total S (preservation-tm _ _ S _).
%total P (preservation P _ _ _ _).

%worlds () (progress-tm-semi _ _).
%total PG (progress-tm-semi PG _).

%worlds () (progress-tm _ _ _).
%total T (progress-tm T _ _).

%worlds () (progress _ _ _).
%total P (progress P _ _).