%
% step.elf:  Operational semantics of source expressions
%

% "Administrative" stepping, corresponding to `step/unmerge {left,right}'

adstep : exp -> exp -> type.

left  : adstep (merge E1 E2) E1.
right : adstep (merge E1 E2) E2.



% multiple adsteps

adstep* : exp -> exp -> type.

%name adstep* _Adsteps.

adstep*/zero : adstep* E E.

adstep*/left : adstep  E1 E2
            -> adstep* E2 EZ
            -> adstep* E1 EZ.



% Adding a step at the end

adstep*snoc :
  % If
       adstep* E EY
    -> adstep EY EZ
  % then
    -> adstep* E EZ
  -> type.
%mode adstep*snoc +Adsteps +Adstep -Adsteps'.

adstep*snoc/zero : adstep*snoc adstep*/zero Adstep (adstep*/left Adstep adstep*/zero).

adstep*snoc/n    : adstep*snoc (adstep*/left Adstep1 Adsteps) Adstep (adstep*/left Adstep1 Adsteps')
                <- adstep*snoc Adsteps Adstep Adsteps'.

%worlds ()        (adstep*snoc _ _ _).
%total  (Adsteps) (adstep*snoc Adsteps _ _).


adstep*append :
  % If
       adstep* E1 E2
    -> adstep* E2 E3
  % then
    -> adstep* E1 E3
  -> type.
%mode adstep*append +Adsteps12 +Adsteps23 -Adsteps13.

adstep*append/zero : adstep*append adstep*/zero Adsteps23 Adsteps23.

adstep*append/n    : adstep*append (adstep*/left Adstep1 Adsteps12) Adsteps23 (adstep*/left Adstep1 Adsteps13)
                  <- adstep*append Adsteps12 Adsteps23 Adsteps13.

%worlds ()          (adstep*append _ _ _).
%total  (Adsteps12) (adstep*append Adsteps12 _ _).



%
% Main stepping relation on source expressions
%

step : exp -> exp -> type.
%name step _Step.


% application

step/app1 : step E1 E1'
         -> step (app E1 E2) (app E1' E2).

step/app2 : is-value V1
         -> step E2 E2'
         -> step (app V1 E2) (app V1 E2').

step/beta : is-value Varg
         -> step (app (lam [x] Ebody x) Varg) (Ebody Varg).


% fix

step/fix  : step (fix ([u] Ebody u))
                 (Ebody (fix ([u] Ebody u))).


% unmerge left, unmerge right

step/unmerge : adstep E1 E2 -> step E1 E2.


% split and merge_k (evaluation under merge)

step/split  : step E (merge E E).

step/merge1 : step E1 E1'
           -> step (merge E1 E2) (merge E1' E2).
step/merge2 : step E2 E2'
           -> step (merge E1 E2) (merge E1 E2').


%
% step* : multiple steps
%

step* : exp -> exp -> type.
%name step* _Steps.

step*/zero : step* E E.

step*/left : step  E1 E2
          -> step* E2 EZ
          -> step* E1 EZ.


% If E1 -->* E1' then E1 E2 -->* E1' E2.
step*app1 :
   % If
      {E2 : exp}
       step* E1 E1'
   % then
    -> step* (app E1 E2) (app E1' E2)
  -> type.
%mode step*app1 +E +In -Out.

% If E1 = E1' then E1 E2 = E1' E2.
step*app1/zero : step*app1 E2 step*/zero step*/zero.

% If E1 --> E1X and E1X -->* E1' then E1 E2 -->* E1' E2:
% By i.h., E1X E2 -->* E1' E2.
% 
step*app1/left : step*app1 E2 (step*/left Step StepsIn) (step*/left (step/app1 Step) StepsOut)
              <- step*app1 E2 StepsIn StepsOut.

%worlds ()   (step*app1 _ _ _).
%total  (In) (step*app1 _ In _).


% If E2 -->* E2' then E1 E2 -->* E1 E2'.

step*app2 :
   % If
       {V1 : exp}
        is-value V1
     -> step* E2 E2'
   % then
     -> step* (app V1 E2) (app V1 E2')
   -> type.
%mode step*app2 +V1 +IsVal1 +In -Out.

step*app2/zero : step*app2 _ _ step*/zero step*/zero.

step*app2/left : step*app2 V1 IsVal1 (step*/left Step StepsIn) (step*/left (step/app2 IsVal1 Step) StepsOut)
              <- step*app2 V1 IsVal1 StepsIn StepsOut.

%worlds ()   (step*app2  _ _ _   _).
%total  (In) (step*app2  _ _ In  _).



% If E1 -->* E1' then E1 E2 -->* E1' E2.

step*merge1 :
    % If
       {E2 : exp}
        step* E1 E1'
    % then
     -> step* (merge E1 E2) (merge E1' E2)
   -> type.
%mode step*merge1 +E +In -Out.

step*merge1/zero : step*merge1 E2 step*/zero step*/zero.

step*merge1/left : step*merge1 E2 (step*/left Step StepsIn) (step*/left (step/merge1 Step) StepsOut)
                <- step*merge1 E2 StepsIn StepsOut.

%worlds ()   (step*merge1 _ _   _).
%total  (In) (step*merge1 _ In  _).


% If E2 -->* E2' then E1 ,, E2 -->* E1' E2.

step*merge2 :
  % If
      {E1 : exp}
       step* E2 E2'
  % then
    -> step* (merge E1 E2) (merge E1 E2')
  -> type.
%mode step*merge2 +E +In -Out.

step*merge2/zero : step*merge2 E2 step*/zero step*/zero.

step*merge2/left : step*merge2 E2 (step*/left Step StepsIn) (step*/left (step/merge2 Step) StepsOut)
                <- step*merge2 E2 StepsIn StepsOut.

%worlds ()   (step*merge2 _ _   _).
%total  (In) (step*merge2 _ In  _).


% If E -->* EY and EY --> EZ then E -->* EZ.
step*snoc :
  % If
       step* E EY
    -> step EY EZ
  % then
    -> step* E EZ
  -> type.
%mode step*snoc +Steps +Step -Steps'.

step*snoc/zero : step*snoc step*/zero Step (step*/left Step step*/zero).

step*snoc/n    : step*snoc (step*/left Step1 Steps) Step (step*/left Step1 Steps')
              <- step*snoc Steps Step Steps'.

%worlds ()      (step*snoc _ _      _).
%total  (Steps) (step*snoc Steps _  _).


% If E1 -->* E2 and E2 -->* E3 then E1 -->* E3.
step*append :
   % If
        step* E1 E2
     -> step* E2 E3
   % then
     -> step* E1 E3
   -> type.
%mode step*append +Steps12 +Steps23 -Steps13.

step*append/zero : step*append step*/zero Steps23 Steps23.
step*append/n    : step*append (step*/left Step1 Steps12) Steps23 (step*/left Step1 Steps13)
                <- step*append Steps12 Steps23 Steps13.

%worlds ()        (step*append _ _        _).
%total  (Steps12) (step*append Steps12 _  _).


step*adstep* :
   % If
       adstep* E1 E2
   % then
    -> step* E1 E2
  -> type.
%mode step*adstep* +Adsteps -Steps.

step*adstep*/zero : step*adstep* adstep*/zero step*/zero.
step*adstep*/n    : step*adstep* (adstep*/left Adstep Adsteps) (step*/left (step/unmerge Adstep) Steps)
                 <- step*adstep* Adsteps Steps.

%worlds ()        (step*adstep*  _  _).
%total  (Adsteps) (step*adstep*  Adsteps  _).


%freeze adstep adstep* step step*.