Iterated Let Bindings

Let with iterated bindings.

Preliminaries

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort add {_ nat} {_ nat} {_ nat} %.
%mode add %in %in %out %.
%term add/z add z N N %.
%term add/s %pi (add (s N) M (s P)) %<- (add N M P) %.
%worlds () (add _ _ _) %.
%total M (add M _ _) %.

Syntax

%sort exp %.
%% oexp N is morally exp^N -> exp, but curried
%sort oexp {_ nat} %.
%% binds N M is a list of length M - N with types
%% (oexp N , oexp (s N) , ... , oexp (M - 1))
%sort binds {_ nat} {_ nat} %.
%term oexp/done %pi exp %-> (oexp z) %.
%term oexp/bind %pi (%pi exp %-> (oexp N)) %-> (oexp (s N)) %.
%term binds/done binds N N %.
%term binds/cons %pi (oexp F) %-> (binds (s F) L) %-> (binds F L) %.
%term let* %pi (binds z N) %-> (oexp N) %-> exp %.
%term num %pi nat %-> exp %.
%term plus %pi exp %-> exp %-> exp %.

Evaluation

%% substitute the expression for the first var in each of the binds
%sort map-subst {_ exp} {_ binds (s N) (s M)} {_ binds N M} %.
%mode map-subst %in %in %out %.
%term _ map-subst E binds/done binds/done %.
%term _
  %pi (map-subst E (binds/cons (oexp/bind OE) B) (binds/cons (OE E) B'))
  %<- (map-subst E B B') %.
%worlds () (map-subst _ _ _) %.
%total D (map-subst _ D _) %.
%% contradict the existence of binds (s N) z;
%% return a nat
%sort binds-imposs {_ binds (s N) z} {_ nat} %.
%mode binds-imposs %in %out %.
%term _ %pi (binds-imposs (binds/cons _ B) X) %<- (binds-imposs B X) %.
%worlds () (binds-imposs _ _) %.
%total D (binds-imposs D _) %.
%sort eval {_ exp} {_ nat} %.
%mode eval %in %out %.
%term _ %pi (eval (let* binds/done (oexp/done E)) N) %<- (eval E N) %.
%term _
  %pi (eval (let* (binds/cons (oexp/done E) Bs) (oexp/bind E')) N)
  %<- (map-subst E Bs Bs')
  %<- (eval (let* Bs' (E' E)) N) %.
%term _ %pi (eval (plus E1 E2) N) %<- (eval E1 N1) %<- (eval E2 N2) %<- (add N1 N2 N) %.
%term _ eval (num N) N %.
%% silly contradictory case so it coverage checks
%term _ %pi (eval (let* (binds/cons _ B) (oexp/done E)) X) %<- (binds-imposs B X) %.
%worlds () (eval _ _) %.
%covers eval %in %out %.

Example

%% let* x = 3
%%      y = x + 2
%%   in x + y
%% N should be 8
%solve D : eval (let* (binds/cons (oexp/done (num (s (s (s z))))) (binds/cons (oexp/bind ([x] oexp/done (plus x (num (s (s z)))))) binds/done)) (oexp/bind ([x] oexp/bind ([y] oexp/done (plus x y))))) N %.