|
|
- {-# LANGUAGE ViewPatterns #-}
- {-# LANGUAGE DeriveDataTypeable #-}
- {-# LANGUAGE StrictData, PatternSynonyms #-}
- module Value where
-
- import Data.Sequence (Seq)
- import Data.Text (Text)
-
- import Syntax
- import Data.Data
- import qualified Data.Sequence as Seq
-
- newtype Env =
- Env { locals :: Seq Value }
- deriving (Eq, Show, Ord, Data, Typeable)
-
- emptyEnv :: Env
- emptyEnv = Env mempty
-
- type VTy = Value
-
- data Closure
- = Closure !Env !Term
- | ClMeta MetaFun
- deriving (Eq, Ord, Data, Typeable)
-
- instance Show Closure where
- showsPrec x (Closure _ t) = showsPrec x t
- showsPrec x (ClMeta f) = showsPrec x f
-
- newtype MetaFun = MetaFun { runMC :: Value -> Value }
-
- instance Eq MetaFun where
- _ == _ = False
-
- instance Ord MetaFun where
- _ <= _ = True
-
- instance Show MetaFun where
- show _ = "«meta»"
-
- instance Data MetaFun where
- gunfold _ _ _ = error "gunfold MetaFun"
- toConstr _ = error "gunfold MetaFun"
- dataTypeOf _ = mkNoRepType "MetaFun"
-
- data Value
- -- Universes
- = VType
-
- -- Canonical Π-types and λ values
- | VPi Plicity Text ~Value {-# UNPACK #-} Closure
- | VLam Plicity Text {-# UNPACK #-} Closure
- -- Variable applied to some values, with a
- -- suspended evaluated result that might
- -- be forced later
- | VGlued Head (Seq SpineThing) ~(Maybe Value)
-
- -- Canonical Σ-types and pair values
- | VSigma Text ~Value {-# UNPACK #-} Closure
- | VPair Value Value
-
- -- Id A a b
- | VEq Value Value Value
- -- Id A a b ≡ t
- | VEqG Value Value Value Value
-
- | VTop | VUnit
- deriving (Eq, Show, Ord, Data, Typeable)
-
- data SpineThing
- = AppEx Value
- | AppIm Value
- | SProj1
- | SProj2
- deriving (Eq, Show, Ord, Data, Typeable)
-
- flexible :: Value -> Bool
- flexible VGlued{} = True
- flexible VEqG{} = True
- flexible _ = False
-
- pattern VNe :: Head -> Seq SpineThing -> Value
- pattern VNe x y = VGlued x y Nothing
-
- pattern VProj1 :: Value -> Value
- pattern VProj1 t <- (matchP1 -> Just t) where
- VProj1 t =
- case t of
- VGlued h s n -> VGlued h (s Seq.:|> SProj1) n
-
- matchP1 :: Value -> Maybe Value
- matchP1 (VPair x _) = Just x
- matchP1 (VGlued h (s Seq.:|> SProj1) n) = Just (VGlued h s n)
- matchP1 _ = Nothing
-
- pattern VProj2 :: Value -> Value
- pattern VProj2 t <- (matchP2 -> Just t) where
- VProj2 t =
- case t of
- VGlued h s n -> VGlued h (s Seq.:|> SProj2) n
-
- matchP2 :: Value -> Maybe Value
- matchP2 (VPair _ x) = Just x
- matchP2 (VGlued h (s Seq.:|> SProj2) n) = Just (VGlued h s n)
- matchP2 _ = Nothing
-
- data Meta
- = Unsolved [Text] Value
- | Solved Value
- deriving (Eq, Show)
-
- vVar :: Var -> Value
- vVar x = VGlued (HVar x) mempty Nothing
-
- data Head
- = HVar Var
- | HCon Text
- | HMeta MetaVar
- | HRefl
- | HCoe
- | HCong
- | HSym
- deriving (Eq, Show, Ord, Data, Typeable)
|