module Core.MetaState where

{- |
The metastate is relevant for the /current elaboration unit/ and irrelevant for any definition or
declaration that comes from a different elaboration unit.

The defining property of being a unit is /freezing/: when elaboration exits a unit, its metastate is
turned immutable and persisted into the elaboration output. If we have multi-threaded elaboration,
this freezing is also the synchronization point.
-}
import Data.IntSet (IntSet)

import Common
import Core.Syntax
import Utils.TreeArray (Array)
import Utils.TreeArray qualified as Array

data Unsolved = Unsolved {
    unsolvedLocals   :: Locals
  , unsolvedTy       :: Ty     -- the type is under the Locals
  , unsolvedBlocking :: IntSet -- problems being blocked by this one
  }
makeFields ''Unsolved

-- TODO: optimize closed solutions by using call-by-need instead of call-by-name?
data Solved = Solved {
    solvedLocals      :: Locals
  , solvedTy          :: Ty
  , solvedSolution    :: Tm    -- ^ the type and solution are under the Locals
  , solvedIsInline    :: Bool  -- ^ should we immediately unfold the meta?
  , solvedOccursCache :: MetaVar
    -- ^ cache for approximate occurs checking.
    --   We initialize it to (-1). It holds the last meta
    --   that we succefully checked for *not occurring*
    --   in the solution. TODO: check if this can be a mutable ref.
  }
makeFields ''Solved

data MetaEntry    = MEUnsolved Unsolved | MESolved Solved
type MetaState    = Array MetaEntry
type MetaStateArg = (?metaState :: MetaState)
type ForceArgs    = (LvlArg, MetaStateArg)

lookupMeta :: MetaStateArg => MetaVar -> MetaEntry
lookupMeta (MkMetaVar i) = Array.index ?metaState i

sameMetaState :: MetaState -> MetaState -> Bool
sameMetaState = Array.same