50 lines
1.8 KiB
Idris
50 lines
1.8 KiB
Idris
module Term
|
|
|
|
import Data.Nat
|
|
import Data.Vect
|
|
import Data.Fin
|
|
|
|
import Misc
|
|
|
|
%default total
|
|
|
|
{-
|
|
Can things be ereased?
|
|
-}
|
|
|
|
|
|
mutual
|
|
{-
|
|
The type of terms is indexed by the size of the environment in which
|
|
they are valid, that is, it is impossible to construct an ill-scoped term.
|
|
|
|
It is also indexed by the number of tags of the defined inductive types.
|
|
-}
|
|
public export
|
|
data Term : (ctx : Index) -> (tags : Vect n Nat) -> Type where
|
|
TType : Term n v -- Type of types
|
|
TLam : Term (S n) v -> Term n v -- Lambda (λ _ . #0)
|
|
TPi : Term n v -> Term (S n) v -> Term n v -- Pi type (∏ _ : #0 . #1 _ )
|
|
TApp : Term n v -> Term n v -> Term n v -- Appliction
|
|
TVar : Fin n -> Term n v -- Variable
|
|
TLet : Term n v -> Term n v -> Term (S n) v -> Term n v -- Let (let _ = #1 : #0 in #2)
|
|
TIType : Fin (len v) -> Term n v -- Inductive type
|
|
TIElim : Fin (len v) -> Term n v -- Inductive eliminator
|
|
TICons : (n : Fin (len v)) -> Fin (index n v) -> Term m v -- Inductive constructor
|
|
|
|
|
|
{-
|
|
Use some different brackets to make it easier to read
|
|
-}
|
|
public export
|
|
Show (Term n v) where
|
|
show TType = "Type"
|
|
show (TLam sc) = "Lam {" ++ show sc ++ "}"
|
|
show (TPi ty sc) = "Pi [" ++ show ty ++ "] [" ++ show sc ++ "]"
|
|
show (TApp f x) = "App (" ++ show f ++ ") (" ++ show x ++ ")"
|
|
show (TVar i) = "Var " ++ show i
|
|
show (TLet tr ty sc) = "Let <" ++ show tr ++ "> : <" ++ show ty ++ "> in <" ++ show sc ++ ">"
|
|
show (TIType n) = "IType[#" ++ show n ++ "]"
|
|
show (TIElim n) = "IElim[#" ++ show n ++ "]"
|
|
show (TICons n m) = "ICons[#" ++ show n ++ "][#" ++ show m ++ "]"
|