POPL Tutorial/Evaluation Contexts Intrinsic

Evaluation Contexts, Intrinsically Typed

%sort tp %.
%term b tp %.
%term arr %pi tp %-> tp %-> tp %.
%sort tm {_ tp} %.
%sort val {_ tp} %.
%term app %pi (tm (arr A B)) %-> (tm A) %-> (tm B) %.
%term ret %pi (val A) %-> (tm A) %.
%term lam %pi (%pi (val A) %-> (tm B)) %-> (val (arr A B)) %.
%block tmb [A tp] {x val A}%.
%worlds (tmb) (tm _) (val _) %.
%sort ec {_ %pi (tm A) %-> (tm C)} %.
%term ec/var ec ([x] x) %.
%term ec/app1 %pi (ec ([x] app (E x) M)) %<- (ec E) %.
%term ec/app2 %pi (ec ([x] app (ret V) (E x))) %<- (ec E) %.
%sort redex {_ tm A} %.
%mode redex %in %.
%term redex/beta redex (app (ret V1) (ret V2)) %.
%sort factored {_ tm A} %.
%term f/val factored (ret V) %.
%term f/ec %pi (factored (E M0)) %<- (ec E) %<- (redex M0) %.
%sort factorapp {_ factored M1} {_ factored M2} {_ factored (app M1 M2)} %.
%mode factorapp %in %in %out %.
%term _ factorapp f/val f/val (f/ec redex/beta ec/var) %.
%term _ factorapp (f/ec (%the (redex M0) Dred0) (%the (ec E) Dec)) (%the (factored M2) _) (f/ec Dred0 (ec/app1 Dec)) %.
%term _ factorapp f/val (f/ec (%the (redex M0) Dred0) (%the (ec E) Dec)) (f/ec Dred0 (ec/app2 Dec)) %.
%worlds () (factorapp _ _ _) %.
%total {} (factorapp _ _ _) %.
%unique factorapp %in %in %out %.
%sort factor {M tm A} {_ factored M} %.
%mode factor %in %out %.
%term factor/val factor (ret V) f/val %.
%term factor/app
  %pi (factor (app E1 E2) F)
  %<- (factor E1 F1)
  %<- (factor E2 F2)
  %<- (factorapp F1 F2 F) %.
%worlds () (factor _ _) %.
%total M (factor M _) %.
%unique factor %in %out %.
%sort result {_ tm A} %.
%term done result (ret V) %.
%term stepped %pi (tm A) %-> (result M) %.
%sort contract {_ redex (%the (tm A) M)} {_ tm A} %.
%mode contract %in %out %.
%term _ contract (%the (redex (app (ret (lam M)) (ret V))) redex/beta) (M V) %.
%worlds () (contract _ _) %.
%total {} (contract _ _) %.
%unique contract %in %out %.
%sort stepf {_ factored (%the (tm A) M)} {_ result M} %.
%mode stepf %in %out %.
%term _ stepf f/val done %.
%term _ %pi (stepf (f/ec Dr (%the (ec E) Dec)) (stepped (E Mred))) %<- (contract Dr Mred) %.
%worlds () (stepf _ _) %.
%total {} (stepf _ _) %.
%unique stepf %in %out %.
%sort step {M tm A} {_ result M} %.
%mode step %in %out %.
%term step/i %pi (step M M') %<- (factor M F) %<- (stepf F M') %.
%worlds () (step _ _) %.
%total {} (step _ _) %.
%unique step %in %out %.