core.ott

grammar
ec {{ tex \nonterm{ec} }}, tc {{ tex \nonterm{tc} }} :: tmCore_ ::= {{ com expressions }}
  | x                   ::   :: var {{ com variable }}
  | s                   ::   :: sort {{ com sort }}
  | Pi x : ec1 . ec2    ::   :: piabs {{ com $\Pi$-type }}
  | \ x : ec1 . ec2     ::   :: lamabs {{ com abstraction }}
  | ec1 ec2             ::   :: app {{ com application }}
  | unitc               ::   :: unit {{ com unit value }}
  | Unitc               ::   :: Unit {{ com unit type }}
  | < </ li : eci // i /> >
                        ::   :: variant {{ com ADT }}
  | < l = ec > as < </ li : eci // i /> >
                        ::   :: adt {{ com ADT construction }}
  | case ec of </ li = xi proof pi -> eci // i />
                        ::   :: case {{ com ADT case }}

  | [ x |-> ec1 ] ec2   :: M :: xsubst
  | [ p |-> ec1 ] ec2   :: M :: psubst
  | p                   :: M :: proofterm
  | ec1 -> ec2          :: M :: nondep_arrow
  | ec1 equal ec2 of ec :: M :: equality
  | < l = ec > as ec'   :: M :: adtcon_arb
  | vc                  :: M :: value
  | ( ec )              :: M :: parens
  | eqrefl tc ec        :: M :: eq_introduction
  | BC                  :: M :: base {{ tex \Basec }}
  | ( tc1 , tc2 )       :: M :: pair
  | ( ec1 : tc1 , ec2 : tc2 )
                        :: M :: paircon
  | Sigma tc ec         :: M :: dvpair
  | < ec : tc , p of Pred >
                        :: M :: dxpaircon
  | Pred                :: M :: predicate
  | v                   :: M :: vvar
  | f                   :: M :: fvar
  | \ bnds : ec1 . ec2  :: M :: lambndsabs
  | \ _ : ec1 . ec2     :: M :: lamirrabs {{ com abstraction irrelevant }}
  | Pi _ : ec1 . ec2    :: M :: piirr {{ com pi type irrelevant }}
  | seconddp            :: M :: map_second_dp {{ tex \secondDP }}
  | sigma               :: M :: oracle_sigma {{ tex \sigma }}
  | alpha               :: M :: alpha_type {{ tex \alpha }}
  | gamma               :: M :: subtyping_conversion
  | Pi bnds : ec . ec'  :: M :: pibndsabs

bnds :: bnds_ ::=
  | ec , bnds           :: :: pair
  | ec                  :: :: ec

s {{ tex \nonterm{s} }} :: s_ ::= {{ com sorts }}
  | sst                 ::   :: type {{ com types }}
  | ssq                 ::   :: kind {{ com kinds }}

vc {{ tex \nonterm{vc} }} :: vc_ ::= {{ com values }}
  | \ x : ec1 . ec2     ::   :: abs {{ com abstraction value }}
  | unitc               ::   :: top {{ com unit value }}
  | < l = vc > as < </ li : eci // i /> >
                        ::   :: adt {{ com ADT value }}

GC {{ tex \nonterm{GC} }} :: coreenv_ ::=
  | empty               ::   :: nil
  | GC , x : ec         ::   :: var
  | GC , p : ec         :: M :: proofvar

defns Jctype :: '' ::=

defn GC |- ec1 : ec2 :: :: coretyping :: CT_ {{ com typing }} by

------------------ :: Sort
empty |- sst : ssq

GC |- ec : s
--------------------- :: Var
GC , x : ec |- x : ec

GC |- ec1 : tc1
GC |- tc2 : s
------------------------- :: Weaken
GC , x : tc2 |- ec1 : tc1

GC |- tc1 : s1
GC , x : tc1 |- tc2 : s2
--------------------------- :: Form
GC |- Pi x : tc1 . tc2 : s2

GC |- ec1 : Pi x : tc1 . tc2
GC |- ec2 : tc1
----------------------------- :: App
GC |- ec1 ec2 : [ x |-> ec2 ] tc2

GC , x : tc1 |- ec : tc2
GC |- Pi x : tc1 . tc2 : s
----------------------------- :: Abs
GC |- \ x : tc1 . ec : Pi x : tc1 . tc2

GC |- ec : tc1
GC |- tc2 : s
tc1 =b tc2
-------------- :: Conv
GC |- ec : tc2

GC |- sst : ssq
------------------- :: UnitTerm
GC |- unitc : Unitc

GC |- sst : ssq
------------------ :: UnitType
GC |- Unitc : sst

</ GC |- tci : sst // i />
---------------------------------- :: ADTForm
GC |- < </ li : tci // i /> > : sst

GC |- ec : tcj
lj in </ li // i />
GC |- < </ li : tci // i /> > : sst
--------------------------------------------------------------------- :: ADTCon
GC |- < lj = ec> as < </ li : tci // i /> > : < </ li : tci // i /> >

tc def < </ li : tci // i /> >
GC |- tc' : sst
GC |- ec : tc
</ GC , xi : tci , pi : ec equal ( < li = xi > as tc ) of tc |- eci : tc' // i />
------------------------------------------------------------------------- :: ADTCase
GC |- case ec of </ li = xi proof pi -> eci // i />  : tc'


% Helper rules

GC |- ec : s
x : ec in GC
------------ :: VarW
GC |- x : ec



defns Jcop :: '' ::=

defn ec1 ~~> ec2 :: :: evalcore :: CE_ {{ com evaluation }} by

ec1 ~~> ec1'
-------------------- :: AppL
ec1 ec2 ~~> ec1' ec2

ec2 ~~> ec2'
-------------------- :: AppR
vc1 ec2 ~~> vc1 ec2'


---------------------------------------- :: AppAbs
( \x : ec0. ec1 ) vc2 ~~> [x |-> vc2] ec1

ec ~~> ec'
-------------------------------------------------------------------------------- :: ADT
< lj = ec > as < </ li : eci // i /> > ~~> < lj = ec' > as < </ li : eci // i /> >

ec ~~> ec'
------------------------------------------------------------------------------------------------ :: CaseScrut
case ec of </ li = xi proof pi -> eci // i /> ~~> case ec' of </ li = xi proof pi -> eci // i />


ec0 def < </ li : eci // i /> >
--------------------------------------------------------------------------------------------------------------- :: CaseMatch
case < lj = vc > as ec0 of </ li = xi proof pi -> eci // i /> ~~> [xj |-> vc] [pj |-> eqrefl ec0 (< lj = vc > as ec0)] ecj