surface.ott

grammar
es {{ tex \nonterm{es} }} :: tmS_ ::= {{ com terms }}
  | x                   ::   :: var {{ com variable }}
  | \ x : ts . es       ::   :: abs {{ com abstraction }}
  | es1 es2             ::   :: app {{ com application }}
  | unit                ::   :: top {{ com unit value }}
  | case es of </ li = xi -> esi // i />
                        ::   :: case {{ com ADT case }}
  | < l = es > as < </ li : tsi // i /> >
                        ::   :: adt {{ com ADT construction }}
  | < l = es > as ts    :: M :: adt_ts
  | v                   :: M :: refvar
  | [ v |-> es' ] es    :: M :: evsubst
  | [ x |-> es' ] es    :: M :: varsubst
  | vs                  :: M :: value
  | ( es )              :: M :: parens

l {{ tex \nonterm l }} :: labels_ ::= {{ com ADT labels }}
  | <token>             ::   :: str {{ com token }}

r {{ tex \nonterm r }} :: ref_ ::= {{ com refinements }}
  | top                 ::   :: top {{ com trivially true refinement }}
  | es1 = es2 of ts     ::   :: rexpr {{ com atomic refinement }}  % TODO shall we note that having ts here is purely for convenience of translation?
  | r1 /\ r2            ::   :: rconj {{ com conjunction }}
  | [ v |-> es ] r      :: M :: vsubst {{ com subst }}
  | [ x |-> es ] r      :: M :: xsubst {{ com subst }}

B {{ tex \nonterm B }} :: tbasep_ ::= {{ com base types }}
  | Unit                ::   :: unit

ts {{ tex \nonterm{ts} }} :: ts_ ::= {{ com types }}
  | { v : B | r }           ::   :: tybase {{ com refined base type }}
  | { _ : B | r }           :: M :: irrelevant {{ com var-irrelevant refined base type }}
  | ( x : ts1 ) -> ts2      ::   :: tyarr  {{ com arrow type }}
  | [ x |-> es ] ts         :: M :: txsubst
  | < </ li : tsi // i /> > ::   :: variant {{ com ADT }}

vs {{ tex \nonterm{vs} }} :: vs_ ::= {{ com values }}
  | \ x : ts . es       ::   :: abs {{ com abstraction value }}
  | unit                ::   :: top {{ com unit value }}
  | < l = vs > as < </ li : tsi // i /> >
                        ::   :: adt {{ com ADT value }}

G {{ tex \nonterm G }} :: env_ ::= {{ com typing contexts }}
  | empty               ::   :: nil {{ com empty }}
  | G , x : ts          ::   :: var {{ com variable }}
  | G , v : ts          :: M :: refvar {{ com refvar }}
  | GD                  :: M :: otherctx {{ com otherctx }}
  | G , G'              :: M :: concat {{ com contexts concatenation }}
  | [ x |-> es ] G      :: M :: subst {{ com substition }}

L {{ tex \nonterm L }} :: logic_pred_ ::= {{ com logical predicate }}
  | es1 = es2           ::   :: termEq {{ com term equality }}
  | A v . L             ::   :: forall {{ com $\forall$ }}
  | ( L )               :: M :: parens {{ com parenthesizing }}
  | r1 => r2            ::   :: impl   {{ com implication }}

C {{ tex \nonterm C }} :: logic_ctx_ ::= {{ com logical context }}
  | empty               ::   :: nil
  | C, L                ::   :: pred
  | '[|' G '|]'         :: M :: ctx

defns Jtype :: '' ::=

defn ts1 requiv ts2 :: :: type_r_equiv :: RTEquiv_ {{ com restricted type equivalence }} by

es ~~> es'
------------------------------------- :: Forward
[ x |-> es' ] ts requiv [ x |-> es ] ts

es ~~> es'
------------------------------------- :: Backward
[ x |-> es ] ts requiv [ x |-> es' ] ts

defn G ok :: :: ctx_wf :: TCTX_ {{ com context well-formedness }} by

-------- :: Empty
empty ok

G ok
G |- ts
------------- :: Bind
G , x : ts ok


defn G |- ts :: :: type_wf :: TWF_ {{ com type well-formedness }} by

G ok
-------------------- :: TrueRef
G |- { v : B | top }

G , v : { v1 : B | top } |- es1 : { v2 : B' | top }
G , v : { v1 : B | top } |- es2 : { v2 : B' | top }
-------------------------------------------------- :: Base
G |- { v : B | es1 = es2 of { v2 : B' | top } }

G |- { v : B | r1 }
G |- { v : B | r2 }
------------------------- :: Conj
G |- { v : B | r1 /\ r2 }

G |- ts1
G, x : ts1 |- ts2
--------------------- :: Arr
G |- (x : ts1) -> ts2

</ G |- tsi // i />
---------------------------- :: ADT
G |- < </ li : tsi // i /> >


defn G |- es : ts :: :: typing :: T_ {{ com term typing }} by

G ok
x : ts in G
---------- :: Var
G |- x : ts

G ok
------------------------------ :: Unit
G |- unit : { v : Unit | top }

G |- es1 : ( x : ts1 ) -> ts2
G |- es2 : ts1
-------------------------- :: App
G |- es1 es2 : [ x |-> es2] ts2

G |- ( x : ts1 ) -> ts2
G , x : ts1 |- es : ts2
------------------------------------- :: Abs
G |- \x : ts1. es : ( x : ts1 ) -> ts2

ts def < </ li : tsi // i /> >
G |- ts'
G |- es : ts
</ G , xi : tsi , x : { _ : Unit | es = (< li = xi > as ts) of ts } |- esi : ts' // i />
x fresh
-------------------------------------------------------------------------- :: Case
G |- case es of </ li = xi -> esi // i />  : ts'

G |- es : tsj
lj in </ li // i />
G |- < </ li : tsi // i /> >
------------------------------------------ :: Con
G |- < lj = es > as < </ li : tsi // i /> > : < </ li : tsi // i /> >

G |- es : ts
G |- es : ts'
G |- ts <: ts'
------------ :: Sub
G |- es : ts'

G |- es : ts
G |- ts'
ts requiv ts'
------------- :: RConv
G |- es : ts'


defn G |- ts1 <: ts2 :: :: subtyping :: ST_ {{ com subtyping }} by

[| G |] => A v. (r1 => r2)
------------------------------------- :: Base
G |- { v : B | r1 } <: { v : B | r2 }


G |- ts1' <: ts1
G , x : ts1' |- ts2 <: ts2'
--------------------------------------- :: Arr
G |- (x : ts1) -> ts2 <: (x : ts1') -> ts2'



defns Jop :: '' ::=

defn es1 ~~> es2 :: :: eval :: E_ {{ com evaluation }} by

es1 ~~> es1'
-------------------- :: AppL
es1 es2 ~~> es1' es2

es2 ~~> es2'
-------------------- :: AppR
vs1 es2 ~~> vs1 es2'


---------------------------------------- :: AppAbs
( \x : ts. es1 ) vs2 ~~> [x |-> vs2] es1

es ~~> es'
-------------------------------------------------------------------------------- :: ADT
< lj = es > as < </ li : tsi // i /> > ~~> < lj = es' > as < </ li : tsi // i /> >

es ~~> es'
------------------------------------------------------------------------------ :: CaseScrut
case es of </ li = xi -> esi // i /> ~~> case es' of </ li = xi -> esi // i />


-------------------------------------------------------------------------------------------- :: CaseMatch
case < lj = vs > as < </ li : tsi // i /> > of </ li = xi -> esi // i /> ~~> [xj |-> vs] esj