+ {-# LANGUAGE DeriveGeneric #-}
+
+ module GardGround.Syntax.Abstract (
+ NeutralRoot,
+ Neutral,
+ ValueError,
+ Value,
+ vapp,
+ quote,
+ ) where
+
+ import Control.Monad (foldM)
+ import qualified Deque.Strict as Deq
+ import Generic.Data (Generic)
+ import Numeric.Natural (Natural)
+
+ import GardGround.Syntax.Literal (Literal)
+ import GardGround.Utils.SteParser.Lex (Ident)
+
+ data NeutralRoot = NrLiteral Literal
+ | Global Ident
+ | Local Natural
+ | Quote Natural
+ -- note that Local and Quote are numbered in opposite directions
+ deriving (Eq, Generic)
+
+ instance Show NeutralRoot where
+ show (NrLiteral lit) = show lit
+ show (Global i) = "Global:" <> show i
+ show (Local i) = "Local:" <> show i
+ show (Quote i) = "Quote:" <> show i
+
+ type Deque a = Deq.Deque a
+
+ -- | neutral values (a root, to which might be some values applied)
+ -- values at the front are applied first, further applications get appended to back
+ data Neutral = Neutral NeutralRoot (Deque Value)
+
+ data ValueError =
+ VEInvalidApply Value Value
+ | VEOutOfRangeQuote Natural
+
+ data Value = VLam (Value -> Either ValueError Value)
+ | VPi Value (Value -> Either ValueError Value)
+ | VNeutral Neutral
+ | VRefOf Value -- ^ value being pointed to
+ | VRefOfTy Natural Value -- ^ region and type being pointed to
+
+ -- base design based upon LambdaPi (https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf)
+ -- and with advanced techniques from smalltt (https://github.com/AndrasKovacs/smalltt)
+
+ type EvalResult = Either ValueError Value
+
+ vapp :: Value -> Value -> EvalResult
+ vapp (VLam f) = f
+ vapp (VPi _ f) = f -- ^ this is mostly for convenience
+ vapp (VRefOf r) = vapp r
+ vapp (VNeutral (Neutral (NrLiteral lit) xs)) = Left . VEInvalidApply (VNeutral $ Neutral (NrLiteral lit) xs)
+ vapp (VNeutral (Neutral nam xs)) = \v -> Right . VNeutral . Neutral nam $ Deq.snoc v xs
+ vapp l = Left . VEInvalidApply l
+
+ vfree :: NeutralRoot -> Value
+ vfree r = VNeutral $ Neutral r mempty
+
+ data Expr =
+ ENeutralRoot NeutralRoot
+ | EApply Expr Expr
+ | ELam Expr
+ | EPi Expr Expr
+ | ERefOf Expr
+ | ERefOfTy Natural Expr
+
+ type QuoteResult = Either ValueError Expr
+
+ neutralQuote :: Natural -> Neutral -> QuoteResult
+ neutralQuote i (Neutral nam xs) =
+ let
+ boundfree = case nam of
+ Quote j ->
+ let jp1 = j + 1 in
+ if i < jp1
+ then Left . VEOutOfRangeQuote $ jp1 - i
+ else Right . Local $ i - jp1
+ _ -> Right nam
+ in
+ boundfree >>= \bf -> foldM (\a b -> EApply a <$> quote i b) (ENeutralRoot bf) xs
+
+ -- quote0 = quote 0
+
+ quote :: Natural -> Value -> QuoteResult
+ quote i (VLam f) = ELam <$> ((f . vfree $ Quote i) >>= quote (i + 1))
+ quote i (VNeutral neut) = neutralQuote i neut
+ quote i (VPi arg f) = do
+ arge <- quote i arg
+ fe <- (f . vfree $ Quote i) >>= quote (i + 1)
+ pure (EPi arge fe)
+
+ quote i (VRefOf pt) = ERefOf <$> quote i pt
+ quote i (VRefOfTy j pt) = ERefOfTy j <$> quote i pt