module TCQuestions where

{-

There are no goals to fill in in this buffer. Instead you must extend
the language given below in three different ways. Make each extension
in a seperate file named TCQuestions[A-C].agda. 

For each extension:

1. Extend the untyped and typed languages.

2. Extend the type inferer

3. Extend the type checker

4. Extend the evaluator 

5. Give simple test expressions for the extended functionality which
can be first typechecked and then evaluated.

Note:
Do not just paste the syntactic extensions from the last
coursework. This time you your syntactic constructors can take other 
syntactic expressions as arguments.

-}

data Base : Set where

data Nat : Set where
 z : Nat
 s : Nat → Nat

data Fin : Nat → Set where
  z : ∀{n} → Fin (s n)
  s : ∀{n} → Fin n → Fin (s n)

data Ty : Set where
  ι    : Ty
  _⇒_ : Ty → Ty → Ty

data RawTm : Nat → Set where
  var : ∀{n} → Fin n → RawTm n
  _$_ : ∀{n} → RawTm n → RawTm n → RawTm n
  lam : ∀{n} → Ty → RawTm (s n) → RawTm n 

data Con : Set where
  ε   : Con
  _<_ : Con → Ty → Con

len : Con → Nat
len ε        = z
len (Γ  < σ) = s (len Γ) 

data Var : Con → Ty → Set where
  z : ∀{Γ σ} → Var (Γ < σ) σ
  s : ∀{Γ σ τ} → Var Γ τ → Var (Γ < σ) τ

data Tm : Con → Ty → Set where
  var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
  _$_ : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
  lam : ∀{Γ σ τ} → Tm (Γ < σ) τ → Tm Γ (σ ⇒ τ)

data Maybe (A : Set) : Set where
  Just : A → Maybe A
  Nothing : Maybe A

data Σ (A : Set)(B : A → Set) : Set where
  _,_ : (a : A) → B a → Σ A B

fstΣ : ∀{A B} → Σ A B → A
fstΣ (a , b) = a

sndΣ : ∀{A B}(p : Σ A B) → B (fstΣ p) 
sndΣ (a , b) = b

lookup : ∀ Γ → Fin (len Γ) → Σ Ty (Var Γ)
lookup ε       ()
lookup (Γ < σ) z     = σ , z
lookup (Γ < σ) (s i) = let x = lookup Γ i in fstΣ x , s (sndΣ x) 

data eqTy : Ty → Ty → Set where
  eq : ∀{σ} → eqTy σ σ
  uneq : ∀{σ τ} → eqTy σ τ 

isEq : (σ τ : Ty) → eqTy σ τ
isEq ι          ι          = eq
isEq ι          (σ ⇒ τ)   = uneq
isEq (σ ⇒ τ)   ι          = uneq
isEq (σ ⇒ τ)   (σ' ⇒ τ') with isEq σ σ' | isEq τ τ'
isEq (.σ ⇒ .τ) (σ ⇒ τ)      | eq        | eq   = eq
isEq (.σ ⇒ τ)  (σ ⇒ τ')     | eq        | uneq = uneq
isEq (σ ⇒ τ)   (σ' ⇒ τ')    | uneq      | q    = uneq

infer : ∀ Γ → RawTm (len Γ) → Maybe (Σ Ty (Tm Γ))
infer Γ (var i)   = let x = lookup Γ i in Just (fstΣ x , var (sndΣ x)) 
infer Γ (t $ u) with infer Γ t
infer Γ (t $ u)    | Nothing = Nothing
infer Γ (t $ u)    | Just (ι , f)         = Nothing
infer Γ (t $ u)    | Just ((σ ⇒ τ) , f) with infer Γ u
infer Γ (t $ u)    | Just ((σ ⇒ τ) , f)    | Nothing = Nothing
infer Γ (t $ u)    | Just ((σ ⇒ τ) , f)    | Just (σ' , a) with isEq σ σ' 
infer Γ (t $ u)    | Just ((.σ ⇒ τ) , f)   | Just (σ , a)     | eq = Just (τ , (f $ a))
infer Γ (t $ u)    | Just ((σ ⇒ τ) , f)    | Just (σ' , a)    | uneq = Nothing
infer Γ (lam σ t) with infer (Γ < σ) t
infer Γ (lam σ t)    | Just p  = Just ((σ ⇒ (fstΣ p)) , lam (sndΣ p))
infer Γ (lam σ t)    | Nothing = Nothing

check : ∀ Γ (σ : Ty) → RawTm (len Γ) → Maybe (Tm Γ σ)
check Γ σ (var i) with lookup Γ i
check Γ σ (var i)    | σ' , x with isEq σ σ'
check Γ σ (var i)    | .σ , x    | eq   = Just (var x)
check Γ σ (var i)    | σ' , x    | uneq = Nothing
check Γ τ (t $ u) with infer Γ u
check Γ τ (t $ u)    | Nothing = Nothing
check Γ τ (t $ u)    | Just (σ , a) with check Γ (σ ⇒ τ) t
check Γ τ (t $ u)    | Just (σ , a)    | Just f  = Just (f $ a)
check Γ τ (t $ u)    | Just (σ , a)    | Nothing = Nothing 
check Γ ι (lam σ t) = Nothing
check Γ (σ ⇒ τ) (lam σ' t) with isEq σ σ'
check Γ (σ ⇒ τ) (lam σ' t)    | uneq = Nothing
check Γ (σ ⇒ τ) (lam .σ t)    | eq   with check (Γ < σ) τ t
check Γ (σ ⇒ τ) (lam .σ t)    | eq      | Just t' = Just (lam t')
check Γ (σ ⇒ τ) (lam .σ t)    | eq      | Nothing = Nothing

-- We only run the evaluator on well-typed expressions.

Val : Ty → Set
Val ι        = Base
Val (σ ⇒ τ) = Val σ → Val τ

data Env : Con → Set where
  ε : Env ε
  _<_ : ∀{Γ σ} → Env Γ → Val σ → Env (Γ < σ)

vlookup : ∀{Γ σ} → Var Γ σ → Env Γ → Val σ
vlookup z     (_ < v) = v
vlookup (s i) (γ < _) = vlookup i γ

eval : ∀{Γ σ} → Tm Γ σ → Env Γ → Val σ 
eval (var i) γ = vlookup i γ
eval (t $ u) γ = eval t γ (eval u γ)
eval (lam t) γ = λ v → eval t (γ < v)

{-
Question A
==========
Extend your language to support booleans with the following
functionality:
-}

data Bool : Set where
  tt : Bool
  ff : Bool

if_then_else_ : {S : Set} → Bool → S → S → S
if tt then x else _ = x
if ff then _ else y = y

{- 
Question B
========== 
Extend your language to support finite
products (a.k.a True and And, cartesian product and singleton, pairs
and unit type) with the following functionality: -}

data Unit : Set where
  void : Unit

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

fst× : ∀{A B} → A × B → A
fst× (a , b) = a

snd× : ∀{A B} → A × B → B
snd× (a , b) = b

{-
Question C
==========
Extend your language to support natural numbers with the following
functionality:
-}

-- (natural numbers defined above)

-- Primitive recursion (induction on natural numbers)

prim : {S : Set} → S → (Nat → S → S) → Nat → S
prim zz ss z     = zz
prim zz ss (s n) = ss n (prim zz ss n)

{- 

There are no explicit starred exercises but here are two suggestions:

1. Make some further language extensions. Failed extensions are also
interesting. E.g. explain why some feature cannot be added easily
added to this setup.


2. Experiment with the design of the typechecker. E.g. Can it be
simplified/made more readible whilst still supporting the same
functionality? Can it be nicely extended to provide more
functionality? One example of the latter is McBride and McKinna's
typechecker in the paper "the view from the left". Our typechecker
returns a typed term as evidence of success; their typechecker also
returns evidence of failure.

-}