LambdaLetRec.idr

module LambdaLetRec

import Data.List1
import Data.List.Quantifiers

--------------------------------------------------------------------------------
-- types

infixr 5 ~>

data Ty
  = IntTy
  | (~>) Ty Ty

--------------------------------------------------------------------------------
-- primops

data Prim : List Ty -> Ty -> Type where
  Neg : Prim [IntTy]        IntTy
  Add : Prim [IntTy, IntTy] IntTy
  Sub : Prim [IntTy, IntTy] IntTy
  Mul : Prim [IntTy, IntTy] IntTy
  IfZ : Prim [IntTy, t, t]  t

--------------------------------------------------------------------------------

data Literal : Ty -> Type where
  IntLit : Int -> Literal IntTy

--------------------------------------------------------------------------------
-- (well-typed) lambda calculus terms

IsVar : List Ty -> Ty -> Type
IsVar ctx v = Any (v ===) ctx

mutual

  data Term : List Ty -> Ty -> Type where
    Var : IsVar ctx ty -> Term ctx ty
    Lam : {s : Ty} -> Term (s :: ctx) t -> Term ctx (s ~> t)
    App : Term ctx (s ~> t) -> Term ctx s -> Term ctx t
    Let : {s : Ty} -> Term ctx s -> Term (s :: ctx) t -> Term ctx t
    Lit : (lit : Literal s) -> Term ctx s
    Pri : Prim ts t -> All (Term ctx) ts -> Term ctx t
    Rec : {ts : List1 Ty} -> All (LetBound (forget ts ++ ctx)) (forget ts) ->
          Term (forget ts ++ ctx) t -> Term ctx t

  -- in recursive lets, we only allow lambdas
  data LetBound : List Ty -> Ty -> Type where
    MkLetBound : Term ctx (s ~> t) -> LetBound ctx (s ~> t)

data OPE : List a -> List a -> Type where
  Nil  : OPE [] []
  (::) : (x : a) -> OPE xs ys -> OPE (x :: xs) (x :: ys)
  Skip : (x : a) -> OPE xs ys -> OPE       xs  (x :: ys)

(++) : OPE xs ys -> OPE us vs -> OPE (xs ++ us) (ys ++ vs)
[]           ++ uvs = uvs
(xy :: xys)  ++ uvs = xy :: (xys ++ uvs)
(Skip x xys) ++ uvs = Skip x (xys ++ uvs)

fromList : (xs : List a) -> OPE xs xs
fromList [] = []
fromList (x :: xs) = x :: fromList xs

namespace IsVar
  export
  weaken : OPE xs ys -> IsVar xs s -> IsVar ys s
  weaken (Skip _ ope) var         = There (weaken ope var)
  weaken (x   :: ope) (Here eq)   = Here eq
  weaken (x   :: ope) (There var) = There (weaken ope var)

namespace Term
  export
  weaken : OPE xs ys -> Term xs s -> Term ys s

namespace LetBound
  export
  weaken : OPE xs ys -> LetBound xs s -> LetBound ys s
  weaken ope (MkLetBound t) = MkLetBound (Term.weaken ope t)

namespace Term
  weaken ope (Var v)    = Var (weaken ope v)
  weaken ope (Lam b)    = Lam (weaken (_ :: ope) b)
  weaken ope (App f t)  = App (weaken ope f) (weaken ope t)
  weaken ope (Let e t)  = Let (weaken ope e) (weaken (_ :: ope) t)
  weaken ope (Lit lit)  = Lit lit
  weaken ope (Pri p ts) = Pri p (mapProperty (weaken ope) ts)
  weaken ope (Rec es t) = let ope = fromList ? ++ ope in
                          Rec (mapProperty (weaken ope) es) (weaken ope t)