% elab.elf
%
% Elaboration typing

%
% elab E A M  :     E : A `--> M
%
elab : {E : exp} {A : ty} {M : tm} type.
%name elab _Elab.


% Top

elab/topintro : is-value V
             -> elab V topty unittm.


% Arrow

elab/arrintro :
             ({x : exp}
              {x' : tm}
                elab x Adom x' -> elab (Ebody x) Acod (Mbody x'))
            ->
                elab (lam ([x] Ebody x))
                     (arr Adom Acod)
                     (lamtm ([x] Mbody x)).

elab/arrelim :
               elab E1 (arr Adom Acod) M1
            -> elab E2 Adom M2
            -> elab (app E1 E2) Acod (apptm M1 M2).


% Merge

elab/merge1 : elab E1 A M
           -> elab (merge E1 E2) A M.
elab/merge2 : elab E2 A M
           -> elab (merge E1 E2) A M.


% Fix

elab/fix :
          ({u : exp}
           {u' : tm}
             elab u A u' -> elab (Ebody u) A (Mbody u'))
         ->
             elab (fix ([u] Ebody u))
                  A
                  (fixtm ([u'] Mbody u')).


% Intersection

elab/sectintro : elab E A1 M1
              -> elab E A2 M2
              -> elab E (sectty A1 A2) (pairtm M1 M2).


elab/sectelim1 : elab E (sectty A1 A2) M
              -> elab E A1 (fsttm M).

elab/sectelim2 : elab E (sectty A1 A2) M
              -> elab E A2 (sndtm M).


% Union (and `direct')

elab/unintro1 : elab E A1 M
             -> elab E (unty A1 A2) (inltm M).

elab/unintro2 : elab E A2 M
             -> elab E (unty A1 A2) (inrtm M).

elab/unelim : 
            fill EC EH
         -> elab E' (unty A1 A2) M'
         -> ({x1 : exp} {m1 : tm}  elab x1 A1 m1 -> elab (EH x1) C (N1 m1))
         -> ({x2 : exp} {m2 : tm}  elab x2 A2 m2 -> elab (EH x2) C (N2 m2))
         -> elab (EH E') C (casetm M' N1 N2).

elab/direct : 
            fill EC EH
         -> elab E' A M'
         -> ({x : exp} {m : tm} elab x A m -> elab (EH x) C (N m))
         -> elab (EH E') C (apptm (lamtm N) M').

%freeze elab.

%query * 1 elab (lam ([x]x)) (arr topty topty) (lamtm ([y] y)).