POPL Tutorial/Control machine

%sort exp %.
%term lam %pi (%pi exp %-> exp) %-> exp %.
%term app %pi exp %-> exp %-> exp %.
%sort ev {_ exp} {_ exp} %.
%term ev_lam ev (lam ([x] E x)) (lam ([x] E x)) %.
%term ev_app %pi (ev (app E1 E2) V) %<- (ev E1 (lam ([x] E x))) %<- (ev E2 V2) %<- (ev (E V2) V) %.
%sort stack %.
%term # stack %.
%term app1 %pi exp %-> stack %-> stack %.
%term app2 %pi exp %-> stack %-> stack %.
%sort state %.
%term eval %pi stack %-> exp %-> state %.
%term return %pi stack %-> exp %-> state %.
%sort step {_ state} {_ state} %.
%term step_lam step (eval K (lam E)) (return K (lam E)) %.
%term step_app1 step (eval K (app E1 E2)) (eval (app1 E2 K) E1) %.
%term step_app2 step (return (app1 E2 K) V) (eval (app2 V K) E2) %.
%term step_red step (return (app2 (lam E) K) V) (eval K (E V)) %.
%sort steps {_ state} {_ state} %.
%term steps_refl steps S S %.
%term steps_trans %pi (step S S') %-> (steps S' S'') %-> (steps S S'') %.
%sort steps_steps {_ steps S S'} {_ steps S' S''} {_ steps S S''} %.
%term _ steps_steps steps_refl W W %.
%term _
  %pi (steps_steps (steps_trans W Ws) Ws' (steps_trans W Ws''))
  %<- (steps_steps Ws Ws' Ws'') %.
%mode steps_steps %in %in %out %.
%worlds () (steps_steps _ _ _) %.
%total T (steps_steps T _ _) %.
%sort sound {_ ev E V} {_ steps (eval K E) (return K V)} %.
%mode {%in E exp} {%in V exp} {%in K stack} {%in E1 ev E V} {%out V1 steps (eval K E) (return K V)} sound E1 V1 %.
%term _ sound ev_lam (steps_trans step_lam steps_refl) %.
%term _
  %pi (sound (ev_app D D2 D1) W123)
  %<- (sound D1 (%the (steps (eval (app1 E2 K) E1) (return (app1 E2 K) (lam E))) W1))
  %<- (sound D2 (%the (steps (eval (app2 (lam E) K) E2) (return (app2 (lam E) K) V2)) W2))
  %<- (sound D (%the (steps (eval K (E V2)) (return K V)) W3))
  %<- (steps_steps (steps_trans step_app1 W1) (steps_trans step_app2 W2) (%the (steps (eval K (app E1 E2)) (return (app2 (lam E) K) V2)) W12))
  %<- (steps_steps W12 (steps_trans step_red W3) (%the (steps (eval K (app E1 E2)) (return K V)) W123)) %.
%worlds () (sound _ _) %.
%total T (sound T _) %.
%sort invert_app2 {_ steps (return (app1 E2 K) V) (return # V')} {_ steps (eval (app2 V K) E2) (return # V')} %.
%term _ invert_app2 (steps_trans step_app2 W) W %.
%mode invert_app2 %in %out %.
%worlds () (invert_app2 _ _) %.
%total {} (invert_app2 _ _) %.
%reduces < C A (invert_app2 A C) %.
%sort id {_ exp} {_ exp} %.
%term refl id E E %.
%sort invert_red {_ steps (return (app2 Vlam K) V) (return # V')} {_ id Vlam (lam E)} {_ steps (eval K (E V)) (return # V')} %.
%term _ invert_red (steps_trans step_red W) refl W %.
%mode invert_red %in %out %out %.
%worlds () (invert_red _ _ _) %.
%total {} (invert_red _ _ _) %.
%reduces < C A (invert_red A _ C) %.
%sort use_id {_ id V1 (lam E)} {_ ev E1 V1} {_ ev E2 V2} {_ ev (E V2) V} {_ ev (app E1 E2) V} %.
%term _ use_id refl E1 E2 E (ev_app E E2 E1) %.
%mode use_id %in %in %in %in %out %.
%worlds () (use_id _ _ _ _ _) %.
%total {} (use_id _ _ _ _ _) %.
%sort complete {_ steps (eval K E) (return # V0)} {_ ev E V} {_ steps (return K V) (return # V0)} %.
%mode complete %in %out %out %.
%term _ complete (%the (steps (eval K (lam E)) (return # V0)) (steps_trans step_lam W)) ev_lam W %.
%term _
  %pi (complete (%the (steps (eval K (app E1 E2)) (return # V0)) (steps_trans step_app1 W)) D' W5)
  %<- (complete (%the (steps (eval (app1 E2 K) E1) (return # V0)) W) (%the (ev E1 V1) D1) (%the (steps (return (app1 E2 K) V1) (return # V0)) W1))
  %<- (invert_app2 W1 (%the (steps (eval (app2 V1 K) E2) (return # V0)) W2))
  %<- (complete W2 (%the (ev E2 V2) D2) (%the (steps (return (app2 V1 K) V2) (return # V0)) W3))
  %<- (invert_red W3 (%the (id V1 (lam E)) ID) (%the (steps (eval K (E V2)) (return # V0)) W4))
  %<- (complete W4 (%the (ev (E V2) V) D) (%the (steps (return K V) (return # V0)) W5))
  %<- (use_id ID D1 D2 D D') %.
%worlds () (complete _ _ _) %.
%reduces < C A (complete A _ C) %.
%total T (complete T _ _) %.