46 lines
836 B
Idris
46 lines
836 B
Idris
module Core.Value
|
|
|
|
import Core.Term
|
|
import Core.Misc
|
|
|
|
import Data.Vect
|
|
|
|
%default total
|
|
|
|
mutual
|
|
public export
|
|
data Value : Type where
|
|
VType : Value
|
|
|
|
VTop : Value
|
|
VStar : Value
|
|
|
|
VBot : Value
|
|
|
|
VNat : Value
|
|
|
|
VGen : Nat -> Value
|
|
VApp : Value -> Value -> Value
|
|
VClos : Ctx n -> Term n -> Value
|
|
|
|
infixl 2 `VApp`
|
|
|
|
public export
|
|
Ctx : Index -> Type
|
|
Ctx i = Vect i Value
|
|
|
|
public export
|
|
ctx0 : Ctx 0
|
|
ctx0 = []
|
|
|
|
public export
|
|
Show Value where
|
|
show VType = "VType"
|
|
show VTop = "VTop"
|
|
show VStar = "VStar"
|
|
show VBot = "VBot"
|
|
show VNat = "VNat"
|
|
show (VGen i) = "VGen " ++ show i
|
|
show (VApp f x) = "VApp (" ++ show f ++ ") (" ++ show x ++ ")"
|
|
show (VClos e t) = "VClos (" ++ assert_total (show e) ++ ") (" ++ show t ++ ")"
|