Skip to content

Instantly share code, notes, and snippets.

@jlouis
Created October 29, 2009 21:54
Embed
What would you like to do?
%{ 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 _ _).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment