% Elaboration of external language (el.elf) into
% internal language (il.elf). This translation is
% mostly pointwise, except that it converts the
% box and dia connectives into uses of 
% quantification and the 'at' modality.

% relates EL types to IL types
ettoit : tye -> typ -> type.
%mode ettoit +A -A'.

ettoit_& : ettoit A A' ->
           ettoit B B' ->
           ettoit (A &e B) (A' & B').
       
ettoit_=> : ettoit A A' ->
            ettoit B B' ->
            ettoit (A =>e B) (A' => B').

ettoit_at : ettoit A A' ->
            ettoit (A ate W) (A' at W).

ettoit_circ : ettoit A A' ->
             ettoit (circe A) (circ A').

ettoit_addr : ettoit (addre W) (addr W).

ettoit_! : ettoit A A' ->
           ettoit (!e A) (all [w] ((unit => A') at w)).

ettoit_? : ettoit A A' ->
           ettoit (?e A) (exists [w:world] ((A' at w) & addr w)).

%worlds (blockw) (ettoit _ _).
%total A (ettoit A _).

eqtyp : typ -> typ -> type.
eqtyp_ : eqtyp A A.

% these are compatibility cases... 
eqtyp_& : eqtyp A A' -> eqtyp B B' -> eqtyp (A & B) (A' & B') -> type.
%mode eqtyp_& +A +B -C.
eqtyp_&_ : eqtyp_& eqtyp_ eqtyp_ eqtyp_.

eqtyp_=> : eqtyp A A' -> eqtyp B B' -> eqtyp (A => B) (A' => B') -> type.
%mode eqtyp_=> +A +B -C.
eqtyp_=>_ : eqtyp_=> eqtyp_ eqtyp_ eqtyp_.

eqtyp_all : ({w} eqtyp (A w) (A' w)) -> 
            eqtyp (all A) (all A') -> type.
%mode eqtyp_all +A -B.
eqtyp_all_ : eqtyp_all ([w] eqtyp_) eqtyp_.

eqtyp_exists : ({w} eqtyp (A w) (A' w)) -> 
            eqtyp (exists A) (exists A') -> type.
%mode eqtyp_exists +A -B.
eqtyp_exists_ : eqtyp_exists ([w] eqtyp_) eqtyp_.

eqtyp_at : {W:world} eqtyp A A' -> eqtyp (A at W) (A' at W) -> type.
%mode eqtyp_at +W +A -B.
eqtyp_at_ : eqtyp_at _ eqtyp_ eqtyp_.

eqtyp_circ : eqtyp A A' -> eqtyp (circ A) (circ A') -> type.
%mode eqtyp_circ +A -B.
eqtyp_circ_ : eqtyp_circ eqtyp_ eqtyp_.

%worlds (blockw) (eqtyp_& _ _ _) (eqtyp_=> _ _ _) (eqtyp_all _ _) (eqtyp_exists _ _) (eqtyp_at _ _ _) (eqtyp_circ _ _).
%total D (eqtyp_& D _ _).
%total D (eqtyp_=> D _ _).
%total D (eqtyp_all D _).
%total D (eqtyp_exists D _).
%total D (eqtyp_at _ D _).
%total D (eqtyp_circ D _).



of_resp : of M A W -> eqtyp A A' -> of M A' W -> type.
%mode of_resp +BOF +EQ -BOF'.
of_resp_ : of_resp D eqtyp_ D.

ofv_resp : ofv M A W -> eqtyp A A' -> ofv M A' W -> type.
%mode ofv_resp +BOF +EQ -BOF'.
ofv_resp_ : ofv_resp D eqtyp_ D.


ettoit_fun : ettoit A A' -> ettoit A A'' -> eqtyp A' A'' -> type.
%mode ettoit_fun +X +Y -Z.

- : ettoit_fun (ettoit_& E1 E2) (ettoit_& E1' E2') D3
 <- ettoit_fun E1 E1' D1
 <- ettoit_fun E2 E2' D2
 <- eqtyp_& D1 D2 D3.

- : ettoit_fun (ettoit_=> E1 E2) (ettoit_=> E1' E2') D3
 <- ettoit_fun E1 E1' D1
 <- ettoit_fun E2 E2' D2
 <- eqtyp_=> D1 D2 D3.

- : ettoit_fun (ettoit_at E) (ettoit_at E') D'
 <- ettoit_fun E E' D
 <- eqtyp_at _ D D'.

- : ettoit_fun (ettoit_circ E) (ettoit_circ E') D'
 <- ettoit_fun E E' D
 <- eqtyp_circ D D'.

- : ettoit_fun ettoit_addr ettoit_addr eqtyp_.

- : ettoit_fun (ettoit_! E) (ettoit_! E') D'
 <- ettoit_fun E E' D
 <- eqtyp_=> (eqtyp_ : eqtyp unit unit) D Da
 <- ({w} eqtyp_at w Da (Dat w))
 <- eqtyp_all Dat D'.

- : ettoit_fun (ettoit_? E) (ettoit_? E') D'
 <- ettoit_fun E E' D
 <- ({w} eqtyp_at w D (Dat w))
 <- ({w} eqtyp_& (Dat w) eqtyp_ (Dand w))
 <- eqtyp_exists Dand D'.

%worlds (blockw) (ettoit_fun _ _ _).
%total D (ettoit_fun D _ _).

ettoit_gimme : {A:tye} {A':typ} ettoit A A' -> type.
%mode ettoit_gimme +A -A' -D.

- : ettoit_gimme (A &e B) _ (ettoit_& Da Db)
 <- ettoit_gimme A _ Da
 <- ettoit_gimme B _ Db.

- : ettoit_gimme (A ate W) _ (ettoit_at D)
 <- ettoit_gimme A _ D.

- : ettoit_gimme (A =>e B) _ (ettoit_=> Da Db)
 <- ettoit_gimme A _ Da
 <- ettoit_gimme B _ Db.

- : ettoit_gimme (!e A) _ (ettoit_! D)
 <- ettoit_gimme A _ D.

- : ettoit_gimme (?e A) _ (ettoit_? D)
 <- ettoit_gimme A _ D.

- : ettoit_gimme (addre _) _ ettoit_addr.

- : ettoit_gimme (circe A) _ (ettoit_circ D)
 <- ettoit_gimme A _ D.

%worlds (blockw) (ettoit_gimme _ _ _).

mobemob : mobilee A -> ettoit A A' -> mobile A' -> type.
%mode mobemob +BM +T -MOB.

bmm& : mobemob (&Me B1 B2) (ettoit_& T1 T2) (&M M1 M2)
    <- mobemob B1 T1 M1
    <- mobemob B2 T2 M2.

bmmat : mobemob atMe _ atM.
bmmaddr : mobemob addrMe _ addrM.

% weird: change (ettoit_! _) to _ and get freezing violation (??)
bmm! : mobemob boxMe (ettoit_! _) (allM [w] atM).
bmm? : mobemob diaMe (ettoit_? _) (existsM [w] &M atM addrM).

%worlds (blockw) (mobemob _ _ _).
%total D (mobemob D _ _).

% converts typing derivations for EL to IL
elab : {A:tye} {E : expe} ofe E A W ->
       ettoit A A' ->
       {M : exp} of M A' W -> type.
%mode elab +A +B +BW +BT -E -OE.

elab' : {A:tye} {E : expe} ofe E A W ->
        ettoit A A' ->
        {M : exp} of M A' W -> type.
%mode elab' +A +B +BW -BT -E -OE.

elabv : {A:tye} {V : vale} ofve V A W ->
        ettoit A A' ->
        {VV : val} ofv VV A' W -> type.
%mode elabv +A +B +BW +BT -E -OE.

elabvv: {A:tye} {V : vvale} ofvve V A ->
        ettoit A A' ->
        {VV : vval} ofvv VV A' -> type.
%mode elabvv +A +B +C -D -E -F.

elabv' : {A:tye} {V : vale} ofve V A W ->
         ettoit A A' ->
         {VV : val} ofv VV A' W -> type.
%mode elabv' +A +B +BW -BT -E -OE.

elabs' : {A:tye} {S : vexpe} ofse S A W ->
         ettoit A A' ->
         {SS : vexp} ofs SS A' W -> type.
%mode elabs' +A +B +BW -BT -E -OE.

- : elabs' _ _ (ofscvale OVV) ET _ (ofscval OVV')
 <- elabvv _ _ OVV ET _ OVV'.

- : elabs' _ _ (ofsmobce MOB OE) ET _ (ofsmobc MOB' OE')
 <- elab' _ _ OE ET _ OE'
 <- mobemob MOB ET MOB'.

% need to convince Twelf that the I/O behavior
% of the ettoit argument is irrelevant, since
% it's a total function of the first argument.
el : elab  A B BW BTi E OE'
  <- elab' A B BW BTo E OE
  <- ettoit_fun BTo BTi EQ
  <- of_resp OE EQ OE'.

- : elab' _ _ (&Ie D1 D2) (ettoit_& ET1 ET2) _ (&I D1' D2')
 <- elab' _ _ D1 ET1 _ D1'
 <- elab' _ _ D2 ET2 _ D2'.    

- : elab' _ _ (&E1e D) ET _ (&E1 D')
 <- elab' _ _ D (ettoit_& ET _) _ D'.
- : elab' _ _ (&E2e D) ET _ (&E2 D')
 <- elab' _ _ D (ettoit_& _ ET) _ D'.

- : elab' _ _ oflocalhoste ettoit_addr _ oflocalhost.

- : elab' _ _ (=>Ee Df Da) ET _ (=>E Df' Da')
 <- elab' _ _ Df (ettoit_=> ET' ET) _ Df'
 <- elab  _ _ Da ET' _ Da'.

- : elab' _ _ (atEe Dm Dn) ET _ (atE Dm' Dn')
 <- ettoit_gimme A A' ETv
 <- elab  _ _ Dm (ettoit_at ETv) _ Dm'
 <- ({ve : vale}{ove : ofve ve A W}
     {v  : val} {ov  : ofv  v  A' W} elabv' A ve ove ETv v ov ->
       elab' _ _ (Dn ve ove) ET _ (Dn' v ov)).

% interesting cases
- : elab' _ _ (!Ee D) ET _ 
          (atE (allE D') [x][ofx] =>E (ofvalue ofx) (ofvalue unitI))
 <- elab' _ _ D (ettoit_! ET) _ D'.

- : elab' _ _ (?Ie D) (ettoit_? ET) _
          (oflet D' [x][ofx] 
           oflet oflocalhost [a][ofa]
           oflet (ofvalue (&Iv (atI ofx) ofa)) [p][ofp]
             ofvalue (existsI _ ofp))
 <- elab' _ _ D ET _ D'.

- : elab' _ _ (ofgete ME Da Dm) ET _ (ofget ME' Da' Dm')
 <- elab  _ _ Da ettoit_addr _ Da'
 <- elab' _ _ Dm ET _ Dm'
 <- mobemob ME ET ME'.

- : elab' _ _ (?Ee Dm Dn) ET _
     (existsE Dm' [w][p][ofp]
        oflet (&E1 (ofvalue ofp)) [v][ov]
        oflet (&E2 (ofvalue ofp)) [a][oa]
        atE (ofvalue ov) [v'][ov']
        Dn' w a oa v' ov')
 <- ettoit_gimme C C' ET
 <- elab' _ _ Dm (ettoit_? ETv) _ Dm'
 <- ({w : world}
     % address
     {ae : vale}{oae : ofve ae (addre w) W}
     {a  : val} {oa  : ofv  a  (addr w) W} 
     {_ : elabv' (addre w) ae oae ettoit_addr a oa}
     % value
     {ve : vale}{ove : ofve ve A w}
     {v  : val} {ov  : ofv  v  A' w} 
     {_ : elabv' A ve ove ETv v ov}

       elab _ _ (Dn w ae oae ve ove) ET _ (Dn' w a oa v ov)).

- : elab' _ _ (cirEe Dm Dn) ET _ (cirE Dm' Dn')
 <- ettoit_gimme A A' ETv
 <- elab _ _ Dm (ettoit_circ ETv) _ Dm'
 <- ({ve : vvale}{ove : ofvve ve A}
     {v : vval}{ov : ofvv v A'}
     {thm : elabvv A ve ove ETv v ov}
       elab' _ _ (Dn ve ove) ET _ (Dn' v ov)).

% other judgments
- : elab' _ _ (ofvaluee D) ET _ (ofvalue D')
 <- elabv' _ _ D ET _ D'.

% elaboration of value judgment

% XXX unnecessary?
elv : elabv  A B BW BTi E OE'
   <- elabv' A B BW BTo E OE
   <- ettoit_fun BTo BTi EQ
   <- ofv_resp OE EQ OE'.

- : elabv' _ _ (addrIe : ofve _ _ W) ettoit_addr _ 
               (addrI : ofv _ _ W).

- : elabv' _ _ (&Ive Da Db) (ettoit_& ETa ETb) _ (&Iv Da' Db')
 <- elabv' _ _ Da ETa _ Da'
 <- elabv' _ _ Db ETb _ Db'.

- : elabv' _ _ (=>Ie D) (ettoit_=> ETa ETb) _ (=>I D')
 <- ettoit_gimme A A' ETa
 <- ({ve : vale}{ove : ofve ve A W}
     {v  : val} {ov  : ofv  v  A' W} 
     {thm : elabv' A ve ove ETa v ov}
       elab' _ _ (D ve ove) ETb _ (D' v ov)).

- : elabv' _ _ (atIe D) (ettoit_at ET) _ (atI D')
 <- elabv' _ _ D ET _ D'.

- : elabv' _ _ (cirIe Ds) (ettoit_circ ET) _ (cirI Ds')
 <- elabs' _ _ Ds ET _ Ds'.

% interesting cases
- : elabv' _ _ (!Ie D) (ettoit_! ET) _
     (allI [w] atI (=>I [u][ofu] (D' w)))
 <- ettoit_gimme _ _ ET
 <- ({w : world}
       elab _ _ (D w) ET _ (D' w)).

%block blockve : some  {A:tye}{A':typ}{W:world}
                       {ETv : ettoit A A'}
                 block {ve : vale}{ove : ofve ve A W}
                       {v  : val} {ov  : ofv  v  A' W} 
                       {thm : elabv' A ve ove ETv v ov}.


%block blockvve : some  {A:tye}{A':typ}
                        {ETv : ettoit A A'}
                  block {ve : vvale}{ove : ofvve ve A}
                        {v : vval}{ov : ofvv v A'}
                        {thm : elabvv A ve ove ETv v ov}.

%worlds (blockw | blockve | blockvve) 
                 (elab _ _ _ _ _ _) (elab' _ _ _ _ _ _)
                 (elabv _ _ _ _ _ _) (elabv' _ _ _ _ _ _)
                 (elabvv _ _ _ _ _ _)
                 (elabs' _ _ _ _ _ _)
                 (ofv_resp _ _ _) 
                 (of_resp _ _ _).


%total D (ettoit_gimme D _ _).
%total D (of_resp _ D _).
%total D (ofv_resp _ D _).

%total (C B A Z Y X)
                 (elab' _ _ C _ _ _) (elab _ _ B _ _ _)
                 (elabv' _ _ A _ _ _) (elabv _ _ Z _ _ _)
                 (elabvv _ _ Y _ _ _) 
                 (elabs' _ _ X _ _ _).