%
% eval-contexts.elf
%
% Evaluation contexts; the type family `eval-context' is a first-order object,
% but can be turned into a higher-order object of type (exp -> exp) through
% the `fill' relation.
%


eval-context : type.
%name eval-context _EC.

ec/hole   : eval-context.                         % []

ec/app1   : eval-context -> exp -> eval-context.  % app EC E

ec/app2   : {E1 : exp} is-value E1
         -> eval-context
         -> eval-context.                         % app V EC

ec/merge1 : eval-context -> exp -> eval-context.  % merge EC E
ec/merge2 : exp -> eval-context -> eval-context.  % merge E EC



fill : eval-context -> (exp -> exp) -> type.
%name fill _Fill.

%mode fill +EC -Eout.

fill/hole :    fill ec/hole ([e] e).

fill/app1 :    fill (ec/app1 EC E2) ([e] app (Eout e) E2)
            <- fill EC Eout.

fill/app2 :    fill (ec/app2 V1 _ EC) ([e] app V1 (Eout e))
            <- fill EC Eout.

fill/merge1 :   fill (ec/merge1 EC E2) ([e] merge (Eout e) E2)
             <- fill EC Eout.

fill/merge2 :   fill (ec/merge2 E1 EC) ([e] merge E1 (Eout e))
             <- fill EC Eout.

%worlds () (fill EC Efn).
%total  EC (fill EC Efn).


%
%  If EC[E'] is a value then E' is a value.
%
eval-contexts-value :
   % If
      {E' : exp}
      {EC : eval-context}
      {Fill : fill EC EH}
       is-value (EH E')
   % then
    -> is-value E'
  -> type.
%mode eval-contexts-value +E' +EC +Fill +WholeIsVal
                              -PartIsVal.

- :
     eval-contexts-value E' (ec/hole) (fill/hole) WholeIsVal WholeIsVal.

- :
     eval-contexts-value E' (ec/merge1 EC E2) (fill/merge1 Fill) (is-value/merge IsVal1 IsVal2) IsVal1'
  <- eval-contexts-value E' EC Fill IsVal1 IsVal1'.

- :
     eval-contexts-value E' (ec/merge2 E1 EC) (fill/merge2 Fill) (is-value/merge IsVal1 IsVal2) IsVal2'
  <- eval-contexts-value E' EC Fill IsVal2 IsVal2'.


%worlds ()                   (eval-contexts-value _ _  _    _           _).
%total  {EC Fill WholeIsVal} (eval-contexts-value _ EC Fill WholeIsVal  _).