STLCWithValueInclusion.agda

module STLCWithValueInclusion where



data Type : Set where
  Bool : Type
  _*_ _=>_ : Type -> Type -> Type

data Context : Set where
  [] : Context
  _,_ : Context -> Type -> Context

data Var : (G : Context) -> (A : Type) -> Set where
  here : forall {G A} -> Var (G , A) A
  there : forall {G A B} -> Var G A -> Var (G , B) A

mutual
  
  data Term (G : Context) : (A : Type) -> Set where
    var : forall {A} -> Var G A -> Term G A
    true false : Term G Bool
    if_then_else_ : forall {A} -> Term G Bool -> Term G A -> Term G A -> Term G A
    <_,_> : forall {A B} -> Term G A -> Term G B -> Term G (A * B)
    fst : forall {A B} -> Term G (A * B) -> Term G A
    snd : forall {A B} -> Term G (A * B) -> Term G B
    lam : forall {A B} -> Term (G , A) B -> Term G (A => B)
    _$_ : forall {A B} -> Term G (A => B) -> Term G A -> Term G B
    [_] : forall {A} -> Value A -> Term G A

  data Value : (A : Type) -> Set where
    true false : Value Bool
    <_,_> : forall {A B} -> Value A -> Value B -> Value (A * B)
    clo : forall {G A B} -> Env G -> Term (G , A) B -> Value (A => B)

  Env : Context -> Set
  Env G = forall {A} -> Var G A -> Value A

extend : forall {G A} -> Env G -> Value A -> Env (G , A)
extend e V here = V
extend e V (there x) = e x

{-# TERMINATING #-}
normalize : forall {G A} -> Env G -> Term G A -> Value A
normalize e (var x) = e x
normalize e true = true
normalize e false = false
normalize e (if M then N else P) with normalize e M
normalize e (if M then N else P) | true = normalize e N
normalize e (if M then N else P) | false = normalize e P
normalize e < M , N > = < normalize e M , normalize e N >
normalize e (fst P) with normalize e P
normalize e (fst P) | < U , V > = U
normalize e (snd P) with normalize e P
normalize e (snd P) | < U , V > = V
normalize e (lam M) = clo e M
normalize e (M $ N) with normalize e M | normalize e N
normalize e (M $ N) | clo e' M' | V = normalize (extend e' V) M'
normalize e [ V ] = V