pi.ott

% This file includes the specification of the core grammar, operational semantics
% and typing rules for the pi-forall language.
%
% It also includes typesetting directives that control how the language is presented
% in the lecture notes.

metavar tname, x, y, z, f, g, n ::=
  {{ com variables }}
  {{ lex alphanum }}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% pi-forall core language

grammar

tm, a , b , A , B :: '' ::= {{ com terms and types }}

  | Type            ::   :: Type
    {{ com sort }}

  | x               ::   :: Var
    {{ com variable }}

  | \ x . a         ::   :: Lam
    {{ tex \lambda [[x]]. [[a]] }}
    {{ com function definition }}

  | a b             ::   :: App
    {{ tex [[a]] \; [[b]] }}
    {{ com function application }}

  | ( x : A ) -> B  ::   :: Pi
    {{ tex ([[x]]\!:\![[A]]) [[->]] [[B]] }}
    {{ com dependent function type }}

  | a [ b / x ]     :: S :: SubstOp
    {{ com substitution }}

  | A -> B          :: M :: Arrow
    {{ com syntactic sugar for function types }}

  | ( a : A )       ::   :: Ann
    {{ com type annotation }}

  | ( a )           :: S :: Paren
    {{ com parenthesis }}

  | TRUSTME         ::   :: TrustMe
    {{ com term that has any type }}

  | PRINTME         ::   :: PrintMe
    {{ com print the current context }}


  | Unit            ::   :: TyUnit
    {{ com unit type }}

  | ()              ::   :: LitUnit
    {{ com unit term }}

v :: 'v_' ::= {{ com values }}

  | Type            ::   :: Type

  | \ x . a         ::   :: Lam

  | ( x : A ) -> B  ::   :: Pi

  | Unit            ::   :: TyUnit

  | ()              ::   :: LitUnit

  | ( v )           :: S :: Paren

neutral, ne :: 'n_' ::= {{ com neutral terms }}

  | x               ::   :: Var

  | ne a             ::   :: App

  | ( ne )           :: S :: Paren

nf :: 'nf_' ::= {{ com weak head normal forms }}

  | Type            ::   :: Type

  | \ x . a         ::   :: Lam

  | ( x : A ) -> B  ::   :: Pi

  | Unit            ::   :: TyUnit

  | ()              ::   :: LitUnit

  | x               ::   :: Var

  | ne b            ::   :: App

  | ( nf )           :: S :: Paren

subrules
  ne <:: nf
  v <:: nf
  nf <:: a

substitutions
  single a x     :: subst_tm

freevars
  a x   :: fv_tm

parsing
Ann right Arrow
Arrow right Arrow

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

grammar

context, G {{ tex \Gamma }} :: 'ctx_' ::= {{ com contexts }}

   |                 ::    :: Nil
   {{ tex \emptyset }}

   | G , x : A       ::    :: Cons   {{ tex [[G]], [[x]]\! :\![[A]] }}

   | x : A           ::    :: Single {{ tex [[x]]\! :\![[A]] }}

   | ( G )           ::    :: Paren

terminals :: 'terminals_' ::=
  | <->               ::   :: iso           {{ tex \leftrightarrow }}
  | <=>               ::   :: lrarrow       {{ tex \Leftrightarrow }}
  | -->               ::   :: step          {{ tex \longrightarrow }}
  | min               ::   :: min           {{ tex \mathsf{min} }}
  | ==                ::   :: definitional  {{ tex \equiv }}
  | all               ::   :: forall        {{ tex \forall }}
  | elem              ::   :: elem          {{ tex \in }}
  | notin             ::   :: notin         {{ tex \not\in }}
  | <=                ::   :: check         {{ tex \Leftarrow }}
  | =>                ::   :: infer         {{ tex \Rightarrow }}
  | =>*               ::   :: minfer        {{ tex \Rightarrow^{\ast} }}
  | ->                ::   :: arrow         {{ tex \to }}
  | /\                ::   :: ilam          {{ tex \mathrm{\Lambda} }}
  | []                ::   :: box           {{ tex \Box }}
  | |-                ::   :: entails       {{ tex \vdash }}
  | |=                ::   :: hs_entails    {{ tex \vDash }}
  | /=                ::   :: neq           {{ tex \neq }}
  | |>                ::   :: cast          {{ tex \triangleright }}
  | ok                ::   :: ok            {{ tex \ \mathsf{ok} }}
  | _                 ::   :: blank         {{ tex \_ }}
  | ~>                ::   :: produce       {{ tex \leadsto }}
  | ~>*               ::   :: multistep     {{ tex \leadsto^{\ast} }}
  | empty             ::   :: empty         {{ tex \varnothing }}
  | hole              ::   :: hole          {{ tex \circ }}
  | fv                ::   :: fv            {{ tex \mathsf{fv}\! }}
  | dom               ::   :: dom           {{ tex \mathsf{dom} }}
  | ~                 ::   :: twiddle       {{ tex \sim }}
  | ~~                ::   :: compatible    {{ tex \asymp }}
  | '|'               ::   :: bar           {{ tex | }}
  | o                 ::   :: bullet        {{ tex \bullet }}
  | fst               ::   :: fst
  | snd               ::   :: snd
  | ==>               ::   :: impl          {{ tex \implies }}

formula :: 'formula_' ::=
  | judgement                ::   :: judgement
  | formula1 .. formulai     ::   :: dots
  | x : A elem G             ::   :: inG
  | G |- A <=> B             ::   :: equate
  | notlam a                 ::   :: notlam
     {{ tex [[a]]\mbox{ is not a $\lambda$-expression } }}
  | notwhnf a                ::   :: notwhnf
     {{ tex [[a]]\mbox{ is not in weak-head normal form } }}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

defns
Jwhnf :: '' ::=

% For closed terms, these rules correspond to a big-step evaluation relation.
% This relation is semi-decidable, so we can express it as a Haskell function
% in our implementation.

defn
whnf G |- a ~> nf ::    :: whnf :: 'whnf_' 
{{ tex  [[G]] [[|-]] [[whnf]]\ [[a]] \leadsto [[nf]] }}
{{ com weak head normalize a to nf (if possible) }}
by

% reduction rules

whnf G |- a ~> (\x.a')
whnf G |- (a'[b/x]) ~> nf
---------------------- :: lam_beta
whnf G |- a b ~> nf


------------------ :: type
whnf G |- Type ~> Type

------------------ :: lam
whnf G |- \x.a ~> \x.a

----------------------------- :: pi
whnf G |- (x:A) -> B ~> (x:A) -> B

%% look up definition in the context
x = a elem G
whnf G |- a ~> nf
---------- :: var
whnf G |- x ~> nf

%% congruence rule
%%
%% for open terms (i.e terms with free variables), the result is not a value
%% but a path (or neutral term)

whnf G |- a ~> ne
---------------------- :: app
whnf G |- a b ~> ne b

% remove type annotations when normalizing
%
whnf G |- a ~> nf
------------------ :: annot
whnf G |- (a : A) ~> nf


defns
JEquate :: '' ::=

defn
G |- a <=> b ::    :: equate :: 'eq_'
by
{{ com compare $a$ and $b$ for equality }}

%% alpha-equivalent terms are equal

---------------- :: refl
G |- a <=> a


%% if whnfs are equal, then the terms are equal

whnf G |- a ~> nf1
whnf G |- b ~> nf2
G |- nf1 <=> nf2
------------- :: whnf
G |- a <=> b


%% if terms are in whnf, compare subterms

G |- a1 <=> a2
--------------------------------- :: abs
G |- \x. a1 <=> \x. a2

G |- A1 <=> A2
G |- B1 <=> B2
--------------------------------  :: pi
G |- (x : A1) -> B1 <=> (x:A2) -> B2


G |- ne1 <=> ne2
G |- b1 <=> b2
--------------------------------- :: app
G |- ne1 b1 <=> ne2 b2

defns
JOp :: '' ::=

defn
a ~> b ::   :: step :: 's_'
{{ com single-step operational semantics, i. e. head reduction }}
by

----------------------------------  :: lambeta
(\x.a) b ~> a [ b / x]


a ~> a'
------------------------  :: app
a b ~> a' b

defn
a ~>* b ::  :: reduction :: ''
{{ com multi-step head reduction }}
by

------------------- :: done
a ~>* a

a ~> b
b ~>* a'
------------------- :: step
a ~>* a'


defns
JEq :: '' ::=

defn
G |- A = B ::  :: eq :: 'e_'
{{ com Definitional equality }}
by

-------------------------- :: beta
G |- (\x.a)b = a [b/x]

----------  :: refl
G |- A = A

G |- A = B
-----------  :: sym
G |- B = A

G |- A1 = A2
G |- A2 = A3
------------------------- :: trans
G |- A1 = A3

G, x : A |- b : B
G |- a1 = a2
---------------------------------- :: lift
G |- b [a1 / x] = b [a2 / x]

G |- A1 = A2
G,x:A1 |- B1 = B2
------------------------------------ :: pi
G |- (x:A1) -> B1 = (x:A2) -> B2


G,x:A1 |- b1 = b2
------------------- :: lam
G |- \x.b1 = \x.b2


G |- a1 = a2
G |- b1 = b2
-------------------------- :: app
G |- a1 b1 = a2 b2


G |- a1 = a2
--------------------- :: annot
G |- (a1 : A) = a2

defns
JTyping :: '' ::=

defn

G |- a : A   ::   :: typing :: 't_'
{{ com Typing }}
by

x : A elem G
----------- :: var
G |- x : A


G, x:A |- a : B
------------------------  ::  slambda
G |- \x.a : (x:A) -> B


G, x:A |- a : B
G |- A : Type
------------------------  ::  lambda
G |- \x.a : (x:A) -> B

G, x:A |- a : B [ y / x]
G |- A : Type
------------------------  ::  altlambda
G |- \x.a : (y:A) -> B


G |- A : Type
G, x:A |- B : Type
-------------------------------------- :: pi
G |- (x:A) -> B : Type

----------------  :: type
G |- Type : Type


G |- a : (x:A) -> B
G |- b : A
--------------------------- ::  app
G |- a b : B [ b / x ]


G |- a : A
G |- A = B
------------ :: conv
G |- a : B


defns
JBidirectional :: '' ::=

defn
G |- a => A ::    :: inferType :: 'i_'
{{ com type synthesis (algorithmic) }}
by

x : A elem G
----------- :: var
G |- x => A

G |- a => (x:A) -> B
G |- b <= A
---------------------------  :: app_simple
G |- a b => B [ b / x ]

G |- a => A 
whnf G |- A ~> (x:A1) -> B 
G |- b <= A1
---------------------------  :: app
G |- a b => B [ b / x ]

G |- A <= Type
G, x:A |- B <= Type
-------------------------------------- :: pi
G |- (x:A) -> B => Type

------------------- :: type
G |- Type => Type

G |- A <= Type
G |- a <= A
------------------ :: annot
G |- (a : A) => A


defn
G |- a <= B ::    :: checkType :: 'c_'
{{ com type checking (algorithmic) }}
by

G, x:A |- a <= B
--------------------------- ::  lambda
G |- \x.a <= (x:A) -> B

notlam a
G |- a => A
------------- :: infer_simple
G |- a <= A

notlam a
G |- a => A
G |- A <=> B
-------------------------- :: infer
G |- a <= B

notwhnf A
G |- a <= nf
whnf G |-  A ~> nf
--------------- :: whnf
G |- a <= A

defn
|- G ::   :: checkCtx :: 'g_'
{{ com check all types in the context }}
by

-------- :: nil
|-


G |- A : Type
|- G
-------------- :: cons
|- G , x : A