Created
October 29, 2009 21:54
-
-
Save jlouis/221886 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
%{ 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