Something went wrong. Try again.
dependent-types proof-assistant
Something went wrong. Try again.
1.8 kB · 49 lines
Haskell
at main
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950
module Core.MetaState where
{- |The metastate is relevant for the /current elaboration unit/ and irrelevant for any definition ordeclaration that comes from a different elaboration unit.
The defining property of being a unit is /freezing/: when elaboration exits a unit, its metastate isturned 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 Commonimport Core.Syntaximport 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 Solvedtype MetaState = Array MetaEntrytype MetaStateArg = (?metaState :: MetaState)type ForceArgs = (LvlArg, MetaStateArg)
lookupMeta :: MetaStateArg => MetaVar -> MetaEntrylookupMeta (MkMetaVar i) = Array.index ?metaState i
sameMetaState :: MetaState -> MetaState -> BoolsameMetaState = Array.same