{-# 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

        GardGround.Syntax.Abstract

      , deque        ^>= 0.4.0.0