|
|
- {-# LANGUAGE PatternSynonyms #-}
- module Syntax where
-
- import Data.Function (on)
- import Data.Text (Text)
-
- import Presyntax.Presyntax (Plicity(..))
- import qualified Data.Text as T
- import Data.IORef (IORef)
-
- data Term
- = Ref Name
- | App Plicity Term Term
- | Lam Plicity Text Term
- | Pi Plicity Text Term Term
- | Meta MV
- | Type
-
- | Sigma Text Term Term
- | Pair Term Term
- | Proj1 Term
- | Proj2 Term
- deriving (Eq, Show, Ord)
-
- data MV =
- MV { mvName :: Text
- , mvCell :: {-# UNPACK #-} !(IORef (Maybe Value))
- }
-
- instance Eq MV where
- (==) = (==) `on` mvName
- instance Ord MV where
- (<=) = (<=) `on` mvName
- instance Show MV where
- show = ('?':) . T.unpack . mvName
-
- data Name
- = Bound Text
- | Defined Text
- | Builtin Text WiredIn
- deriving (Eq, Show, Ord)
-
- data WiredIn
- = WiType
- deriving (Eq, Show, Ord)
-
- type NFType = Value
-
- data Value
- = VNe Head [Projection]
- | VLam Plicity Closure
- | VPi Plicity Value Closure
- | VSigma Value Closure
- | VPair Value Value
- | VType
- deriving (Eq, Show, Ord)
-
- pattern VVar :: Name -> Value
- pattern VVar x = VNe (HVar x) []
-
- quote :: Value -> Term
- quote (VNe h sp) = foldl goSpine (goHead h) (reverse sp) where
- goHead (HVar v) = Ref v
- goHead (HMeta m) = Meta m
-
- goSpine t (PApp p v) = App p t (quote v)
- goSpine t PProj1 = Proj1 t
- goSpine t PProj2 = Proj2 t
-
- quote (VLam p (Closure n k)) = Lam p n (quote (k (VVar (Bound n))))
- quote (VPi p d (Closure n k)) = Pi p n (quote d) (quote (k (VVar (Bound n))))
- quote (VSigma d (Closure n k)) = Sigma n (quote d) (quote (k (VVar (Bound n))))
- quote (VPair a b) = Pair (quote a) (quote b)
- quote VType = Type
-
- data Closure
- = Closure
- { clArgName :: Text
- , clCont :: Value -> Value
- }
-
- instance Show Closure where
- show (Closure n c) = "Closure \\" ++ show n ++ " -> " ++ show (c (VVar (Bound n)))
-
- instance Eq Closure where
- Closure _ k == Closure _ k' =
- k (VVar (Bound (T.pack "_"))) == k' (VVar (Bound (T.pack "_")))
-
- instance Ord Closure where
- Closure _ k <= Closure _ k' =
- k (VVar (Bound (T.pack "_"))) <= k' (VVar (Bound (T.pack "_")))
-
- data Head
- = HVar Name
- | HMeta MV
- deriving (Eq, Show, Ord)
-
- data Projection
- = PApp Plicity Value
- | PProj1
- | PProj2
- deriving (Eq, Show, Ord)
|