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