PatternParameters.ma

data Unit { unit }
data Bool { false ; true }

data Nat { zero ; suc (n : Nat) }

fun plus : Nat -> Nat -> Nat
{ plus zero    m = m
; plus (suc n) m = suc (plus n m)
}

data List ++(A : Set) { nil ; cons (x : A) (xs : List A) }

-- * Vectors

data OldVec ++(A : Set) : (n : Nat) -> Set
{ oldvnil                                                   : OldVec A zero
; oldvcons (n : Nat) (oldvhead : A) (oldvtail : OldVec A n) : OldVec A (suc n)
} fields oldvhead, oldvtail

data Vec ++(A : Set) (n : Nat)
{ vnil                                : Vec A zero
; vcons (vhead : A) (vtail : Vec A n) : Vec A (suc n)
} fields vhead, vtail

fun append : [A : Set] (n : Nat) [m : Nat] -> Vec A n -> Vec A m -> Vec A (plus n m)
{ append A zero    m vnil         ys = ys
; append A (suc n) m (vcons x xs) ys = vcons x (append A n m xs ys)
}

data Fin (n : Nat)
{ fzero            : Fin (suc n)
; fsuc (i : Fin n) : Fin (suc n)
}

fun lookup : [A : Set] (n : Nat) (i : Fin n) (xs : Vec A n) -> A
{ lookup A zero    ()       vnil
; lookup A (suc n) fzero    (vcons x xs) = x
; lookup A (suc n) (fsuc i) (vcons x xs) = lookup A n i xs
}

{- untyped terms

data Tm (n : Nat)
{ var (x    : Fin n)
; app (r, s : Tm n)
; abs (t    : Tm (suc n))
}

let Subst (n, m : Nat) = Vec (Tm m) n

fun liftSubst : (n : Nat) [m : Nat] -> Subst n m -> Subst (suc n) (suc m)
{}

fun subst : (n : Nat) [m : Nat] -> Tm n -> Subst n m -> Tm m
{ subst n m (var i)   rho = lookup (Tm m) n i rho
; subst n m (app r s) rho = app (subst n m r rho) (subst n m s rho)
; subst n m (abs t)   rho = abs (subst (suc n) (suc m) t (liftSubst n m rho))
}
-}

-- * Simply typed lambda terms.

data Ty { nat ; arr (a, b : Ty) }

let Cxt = List Ty

data Var (cxt : Cxt) (a : Ty)
{ vzero                 : Var (cons a cxt) a -- non-linearity ok!
; vsuc  (x : Var cxt b) : Var (cons a cxt) b
}

data Tm (cxt : Cxt) (a : Ty)
{ var (x : Var cxt a)                                : Tm cxt a
; app (a : Ty) (r : Tm cxt (arr a b)) (s : Tm cxt a) : Tm cxt b
; abs (t : Tm (cons a cxt) b)                        : Tm cxt (arr a b)
}

fun Sem : Ty -> Set
{ Sem nat       = Nat
; Sem (arr a b) = Sem a -> Sem b
}

fun Env : Cxt -> Set
{ Env nil         = Unit
; Env (cons a as) = Sem a & Env as
}

fun val : (cxt : Cxt) [a : Ty] -> Var cxt a -> Env cxt -> Sem a
{ val (cons a cxt) .a vzero   (v, vs) = v
; val (cons a cxt) b (vsuc x) (v, vs) = val cxt b x vs
}

fun sem : (cxt : Cxt) (a : Ty) -> Tm cxt a -> Env cxt -> Sem a
{ sem cxt a         (var x)     rho = val cxt a x rho
; sem cxt b         (app a r s) rho = sem cxt (arr a b) r rho (sem cxt a s rho)
; sem cxt (arr a b) (abs t)     rho v = sem (cons a cxt) b t (v, rho)
}

-- * Identity type.

data Id (A : Set) (x, y : A) { refl : Id A x x }

fun subst : [A : Set] [P : A -> Set] [x, y : A] -> Id A x y -> P x -> P y
{ subst A P x .x refl h = h }

fail let trueIsFalse : Id Bool true false = refl

{- How to check a data constructor

Case 1: no target given, e.g.

    cons (x : A) (xs : List A)

  Bring the parameters of the data telescope into scope, then
  check constructor telescope

Case 2: target given, e.g.

    vcons (vhead : A) (vtail : Vec A n) : Vec A (suc n)

  Take the parameters off the target, treat them like patterns,
  and check them against the data telecope (or type of data name).
  We get out a context

    A : Set
    n : Nat

  use this context to check full type of constructor.
  Also, check that no binding in constructor type shadows the
  pattern variables of the target (would be confusing).
  In the end, prepend the context to the constructor type.

Case 3: target is function type.

  Extract final target and proceed as in 2.

-}