-- The scope-extension evidence on the three sinkers that are coercions
-- ('sinkContextUnchecked', 'sinkVars', 'sinkNamed') is their soundness contract,
-- not an argument they can consume, so GHC calls it redundant. It stays.
{-# OPTIONS_GHC -fno-warn-name-shadowing -fno-warn-redundant-constraints #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE RecordWildCards     #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | The typing context on free-foil.
--
-- The successor of @Rzk.TypeCheck@'s @Context var@. Two things change, and they
-- are the point of the migration.
--
-- [A variable is a name, and so is a top-level entry.] A free-foil term refers to
-- a variable by 'Foil.Name' (an @Int@), and by nothing else: there is no way to
-- put a 'VarIdent' inside a term. So a top-level definition is a name too, bound
-- in the outermost scope with no binder above it, and the hypotheses — global and
-- local alike — are one 'Foil.NameMap', looked up in constant time. The old
-- context was an association list keyed by a @var@ whose equality walked an
-- @S@-chain; @lookupVarInfo@ alone was 11.5% of the checker's time. The surface
-- name of an entry is resolved through 'ctxNamed'.
--
-- This also gives sections their natural shape. A @#assume@d assumption is an
-- ordinary binder, so the definitions of a section are checked in its scope, and
-- closing the section abstracts the assumption by pairing its binder with the
-- body — no rewrite of the elaborated terms (see @Rzk.TypeCheck.Decl@).
--
-- [Entering a binder rebuilds nothing.] 'enterBinder' extends the scope and
-- sinks the rest of the context by coercion, so it costs O(1) rather than a walk
-- of the context. The old @enterScopeContext@ mapped @S \<$\>@ over the whole
-- context, rebuilding every elaborated term it held; the heap profile showed
-- those forced copies retaining most of the live heap, and @GlobalScopeInfo@ /
-- @globalEmbed@ (PR #277) exist only to keep that shift off the ~1500 top-level
-- entries. All of that machinery is gone.
module Rzk.TypeCheck.Context where

import           Control.Monad.Foil          (DExt, Distinct, NameBinder,
                                              NameMap, Scope)
import qualified Control.Monad.Foil          as Foil
-- NOTE: free-foil 0.2.0 gives 'NameMap' no 'Functor' instance (it has one on the
-- unreleased main), so 'mapNameMap' goes through the underlying 'IntMap'.
import           Control.Monad.Foil.Internal (NameMap (..))
import qualified Data.IntMap                 as IntMap
import           Data.Map                    (Map)
import qualified Data.Map                    as Map
import           Unsafe.Coerce               (unsafeCoerce)

import           Language.Rzk.Foil.Syntax
import           Language.Rzk.Foil.Names    (Binder (..), RzkPosition (..),
                                              TModality (..), VarIdent,
                                              binderName)
import qualified Language.Rzk.Syntax         as Rzk

-- * The pieces of a context

data Covariance
  = Covariant     -- ^ Positive position.
  | Contravariant -- ^ Negative position.
  | Invariant     -- ^ Unknown position.

data RenderBackend
  = RenderSVG
  | RenderLaTeX

data Verbosity
  = Debug
  | Normal
  | Silent
  deriving (Verbosity -> Verbosity -> Bool
(Verbosity -> Verbosity -> Bool)
-> (Verbosity -> Verbosity -> Bool) -> Eq Verbosity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Verbosity -> Verbosity -> Bool
== :: Verbosity -> Verbosity -> Bool
$c/= :: Verbosity -> Verbosity -> Bool
/= :: Verbosity -> Verbosity -> Bool
Eq, Eq Verbosity
Eq Verbosity =>
(Verbosity -> Verbosity -> Ordering)
-> (Verbosity -> Verbosity -> Bool)
-> (Verbosity -> Verbosity -> Bool)
-> (Verbosity -> Verbosity -> Bool)
-> (Verbosity -> Verbosity -> Bool)
-> (Verbosity -> Verbosity -> Verbosity)
-> (Verbosity -> Verbosity -> Verbosity)
-> Ord Verbosity
Verbosity -> Verbosity -> Bool
Verbosity -> Verbosity -> Ordering
Verbosity -> Verbosity -> Verbosity
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Verbosity -> Verbosity -> Ordering
compare :: Verbosity -> Verbosity -> Ordering
$c< :: Verbosity -> Verbosity -> Bool
< :: Verbosity -> Verbosity -> Bool
$c<= :: Verbosity -> Verbosity -> Bool
<= :: Verbosity -> Verbosity -> Bool
$c> :: Verbosity -> Verbosity -> Bool
> :: Verbosity -> Verbosity -> Bool
$c>= :: Verbosity -> Verbosity -> Bool
>= :: Verbosity -> Verbosity -> Bool
$cmax :: Verbosity -> Verbosity -> Verbosity
max :: Verbosity -> Verbosity -> Verbosity
$cmin :: Verbosity -> Verbosity -> Verbosity
min :: Verbosity -> Verbosity -> Verbosity
Ord)

-- | Where a diagnostic points.
--
-- The line and column are the start of whatever the diagnostic is about: the
-- declaration being checked, narrowed to the sub-term as the checker descends
-- into it (see @narrowLocation@ in "Rzk.TypeCheck.Monad"). The surface syntax
-- records the start of a node and not its extent, so there is no end position
-- to carry.
data LocationInfo = LocationInfo
  { LocationInfo -> Maybe FilePath
locationFilePath :: Maybe FilePath
  , LocationInfo -> Maybe Int
locationLine     :: Maybe Int
  , LocationInfo -> Maybe Int
locationColumn   :: Maybe Int
  } deriving (LocationInfo -> LocationInfo -> Bool
(LocationInfo -> LocationInfo -> Bool)
-> (LocationInfo -> LocationInfo -> Bool) -> Eq LocationInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LocationInfo -> LocationInfo -> Bool
== :: LocationInfo -> LocationInfo -> Bool
$c/= :: LocationInfo -> LocationInfo -> Bool
/= :: LocationInfo -> LocationInfo -> Bool
Eq, Int -> LocationInfo -> ShowS
[LocationInfo] -> ShowS
LocationInfo -> FilePath
(Int -> LocationInfo -> ShowS)
-> (LocationInfo -> FilePath)
-> ([LocationInfo] -> ShowS)
-> Show LocationInfo
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LocationInfo -> ShowS
showsPrec :: Int -> LocationInfo -> ShowS
$cshow :: LocationInfo -> FilePath
show :: LocationInfo -> FilePath
$cshowList :: [LocationInfo] -> ShowS
showList :: [LocationInfo] -> ShowS
Show)

-- | Point a location at a position in the same file.
atPosition :: RzkPosition -> LocationInfo -> LocationInfo
atPosition :: RzkPosition -> LocationInfo -> LocationInfo
atPosition RzkPosition
pos LocationInfo
loc = case RzkPosition -> BNFC'Position
rzkLineCol RzkPosition
pos of
  BNFC'Position
Nothing          -> LocationInfo
loc
  Just (Int
line, Int
col) -> LocationInfo
loc { locationLine = Just line, locationColumn = Just col }

-- | What is known about a hypothesis, local or top-level.
data VarInfo n = VarInfo
  { forall (n :: S). VarInfo n -> TermT n
varType                :: TermT n
  , forall (n :: S). VarInfo n -> Maybe (TermT n)
varValue               :: Maybe (TermT n)
  , forall (n :: S). VarInfo n -> TModality
varModality            :: TModality
  , forall (n :: S). VarInfo n -> TModality
varModAccum            :: TModality
  , forall (n :: S). VarInfo n -> Binder
varOrig                :: Binder
    -- ^ the names the binder introduced, for display only
  , forall (n :: S). VarInfo n -> Bool
varIsAssumption        :: Bool -- FIXME: perhaps, introduce something like decl kind?
  , forall (n :: S). VarInfo n -> Bool
varIsTopLevel          :: Bool
  , forall (n :: S). VarInfo n -> [Name n]
varDeclaredAssumptions :: [Foil.Name n]
  , forall (n :: S). VarInfo n -> Maybe LocationInfo
varLocation            :: Maybe LocationInfo
  , forall (n :: S). VarInfo n -> Maybe (DataRole n)
varDataRole            :: Maybe (DataRole n)
    -- ^ the role the entry plays for a @#data@ declaration, if any
  , forall (n :: S). VarInfo n -> Int
varMetaPrefix          :: Int
    -- ^ the length of the entry's meta-parameter prefix (0 for locals and
    -- for declarations with no meta parameters); see
    -- "Rzk.TypeCheck.MetaPrefix". Recomputed when a section close rewrites
    -- the entry's type.
  }

-- | The role a top-level entry plays for a @#data@ declaration. The ι-rule
-- (in 'Rzk.TypeCheck.Eval') recognises an eliminator head and a
-- constructor-headed scrutinee by these; both entries are otherwise opaque
-- (they carry no value).
--
-- The argument counts speak of the entry's elaborated type: a constructor
-- takes the datatype's parameters and then its own fields; an eliminator
-- takes the parameters, the motive, one method per constructor (in
-- declaration order), and the scrutinee. Closing a section prepends the
-- section's assumptions uniformly to all entries of a declaration, so
-- 'abstractOver' bumps the parameter counts.
data DataRole n = DataRole
  { forall (n :: S). DataRole n -> Name n
dataRoleDataType  :: Foil.Name n
    -- ^ the type former this entry belongs to
  , forall (n :: S). DataRole n -> Int
dataRoleNumParams :: Int
    -- ^ the datatype parameters the entry takes before anything else
  , forall (n :: S). DataRole n -> DataRoleKind
dataRoleKind      :: DataRoleKind
  }

data DataRoleKind
  = DataConKind ConSort Int Int [Int]
    -- ^ a constructor: its sort, its 0-based position among the
    -- constructors (= the method index), the number of its own fields
    -- after the parameters, and the 0-based positions of its recursive
    -- fields (each contributes an induction hypothesis right after the
    -- field in the method)
  | DataElimKind Int Int ElimKind
    -- ^ an eliminator: the number of methods (one per constructor, in
    -- declaration order) and the number of indices of the family; the
    -- spine is parameters, motive, methods, indices, scrutinee

-- | A point constructor inhabits the datatype and the ι-rule dispatches on
-- it as a scrutinee head. A path constructor inhabits an identity type over
-- the datatype, so it can never head a well-typed scrutinee, and the ι-rule
-- must not fire on it: its computation rule is the propositional
-- @compute-@ lemma generated alongside the eliminators.
data ConSort = PointCon | PathCon
  deriving (ConSort -> ConSort -> Bool
(ConSort -> ConSort -> Bool)
-> (ConSort -> ConSort -> Bool) -> Eq ConSort
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ConSort -> ConSort -> Bool
== :: ConSort -> ConSort -> Bool
$c/= :: ConSort -> ConSort -> Bool
/= :: ConSort -> ConSort -> Bool
Eq)

-- | Which eliminator; the ι-rule is the same for both.
data ElimKind = ElimInd | ElimRec
  deriving (ElimKind -> ElimKind -> Bool
(ElimKind -> ElimKind -> Bool)
-> (ElimKind -> ElimKind -> Bool) -> Eq ElimKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ElimKind -> ElimKind -> Bool
== :: ElimKind -> ElimKind -> Bool
$c/= :: ElimKind -> ElimKind -> Bool
/= :: ElimKind -> ElimKind -> Bool
Eq)

-- | Add one leading parameter (a section assumption made explicit).
bumpDataRoleParams :: DataRole n -> DataRole n
bumpDataRoleParams :: forall (n :: S). DataRole n -> DataRole n
bumpDataRoleParams DataRole n
role = DataRole n
role { dataRoleNumParams = dataRoleNumParams role + 1 }

-- | A tope, together with the modalities under which it is available.
data ModalTope n = ModalTope
  { forall (n :: S). ModalTope n -> TModality
tModAccum :: TModality
  , forall (n :: S). ModalTope n -> TModality
tModVar   :: TModality
  , forall (n :: S). ModalTope n -> TermT n
tTope     :: TermT n
  }

-- | The judgement being performed, for tracing and for the error report.
data Action n
  = ActionTypeCheck (Term n) (TermT n)
  | ActionUnify (TermT n) (TermT n) (TermT n)
  | ActionUnifyTerms (TermT n) (TermT n)
  | ActionInfer (Term n)
  | ActionContextEntailedBy [TermT n] (TermT n)
  | ActionContextEntails [TermT n] (TermT n)
  | ActionContextEntailsUnion [TermT n] [TermT n]
  | ActionWHNF (TermT n)
  | ActionNF (TermT n)
  | ActionCheckCoherence (TermT n, TermT n) (TermT n, TermT n)
  | ActionCloseSection (Maybe Rzk.SectionName)
  | ActionCheckLetValue (Maybe VarIdent)

-- | The state of the tope-saturation cache in a 'Context'
-- (see 'ctxTopesSaturated').
data CachedSaturation n
  = SaturationUncached
    -- ^ No cache was installed for this tope context (entailment falls back to
    -- the per-query pipeline).
  | SaturationCached (Maybe [[ModalTope n]])
    -- ^ A deferred pipeline run: forced by the first query under this context.
    -- 'Nothing' records that the pipeline errored; queries then fall back, so
    -- the error surfaces exactly where it would have.

-- * The context

data Context n = Context
  { forall (n :: S). Context n -> Scope n
ctxScope               :: Scope n
    -- ^ Every name in scope: the top-level entries, the section assumptions and
    -- the binders entered on the way here. Substitution and freshness need it.
  , forall (n :: S). Context n -> NameMap n (VarInfo n)
ctxVars                :: NameMap n (VarInfo n)
    -- ^ What each name in scope stands for. Total on 'ctxScope', which is what
    -- 'Foil.lookupName' assumes.
  , forall (n :: S). Context n -> Map VarIdent (Name n)
ctxNamed               :: Map VarIdent (Foil.Name n)
    -- ^ The surface name of each top-level entry (and of each named binder), for
    -- resolving an identifier the parser produced.
  , forall (n :: S). Context n -> [Name n]
ctxBound               :: [Foil.Name n]
    -- ^ Every name in scope, most recently bound first.
    --
    -- The order has to be recorded, not recovered: free-foil refreshes a binder
    -- only when its name clashes, so after a substitution an inner binder may
    -- well carry a /smaller/ id than an outer one (@\\ x2 -> \\ x1 -> …@), and the
    -- ascending order of 'ctxVars' is not the order things were bound in. Display
    -- depends on this: names claim their display name oldest-first, so that an
    -- inner binder is the one refreshed away from an outer name, and not the
    -- other way round.
  , forall (n :: S). Context n -> [SectionInfo n]
ctxSections            :: [SectionInfo n]
    -- ^ The open sections, innermost first. Each records the entries declared in
    -- it, so closing it can turn them into declarations.
  , forall (n :: S). Context n -> [ModalTope n]
ctxDiscreteTopes       :: [ModalTope n]
    -- ^ Discreteness axioms for the flat cube variables in scope (a flat point of
    -- @2@ or @I@ is an endpoint). Maintained at binder entry, so entailment does
    -- not rescan the context on every query.
  , forall (n :: S). Context n -> [ModalTope n]
ctxTopes               :: [ModalTope n]
  , forall (n :: S). Context n -> [ModalTope n]
ctxTopesNF             :: [ModalTope n]
  , forall (n :: S). Context n -> [[ModalTope n]]
ctxTopesNFUnion        :: [[ModalTope n]]
  , forall (n :: S). Context n -> Maybe Bool
ctxTopesEntailBottom   :: Maybe Bool
  , forall (n :: S). Context n -> CachedSaturation n
ctxTopesSaturated      :: CachedSaturation n
    -- ^ The saturated alternatives for this tope context, cached at the points
    -- where the tope context changes.
  , forall (n :: S). Context n -> Map VarIdent [VarIdent]
ctxShadow              :: Map VarIdent [VarIdent]
    -- ^ The identifiers in scope, keyed by their spelling (a 'VarIdent' compares by
    -- spelling and carries the position of its defining occurrence, so the values
    -- are what a shadowing report names).
    --
    -- The check runs at every binder entry, and scanning every name in scope each
    -- time was O(context) per binder — with every top-level definition of a project
    -- in scope, that is most of them.
  , forall (n :: S). Context n -> [Action n]
ctxActionStack         :: [Action n]
  , forall (n :: S). Context n -> Int
ctxActionStackDepth    :: Int
    -- ^ The length of 'ctxActionStack', maintained alongside it: measuring the
    -- list on every judgement made each action cost O(depth), and each path
    -- O(depth²).
  , forall (n :: S). Context n -> Maybe Command
ctxCurrentCommand      :: Maybe Rzk.Command
  , forall (n :: S). Context n -> Maybe LocationInfo
ctxLocation            :: Maybe LocationInfo
  , forall (n :: S). Context n -> Verbosity
ctxVerbosity           :: Verbosity
  , forall (n :: S). Context n -> Covariance
ctxCovariance          :: Covariance
  , forall (n :: S). Context n -> Maybe RenderBackend
ctxRenderBackend       :: Maybe RenderBackend
  , forall (n :: S). Context n -> Bool
ctxRenderHideTerm      :: Bool
    -- ^ When rendering a diagram, hide the proof term: drop the @\<title\>@ (which
    -- carries the full term) from every cell and blank the visible label of
    -- proof-coloured (interior) cells, keeping the given boundary labels.
  , forall (n :: S). Context n -> Bool
ctxHolesAreErrors      :: Bool
    -- ^ When 'True' (the default), an unfilled hole is reported as a
    -- @TypeErrorUnsolvedHole@; finished work (and CI) must have no holes. The
    -- lenient mode ('allowHoles') instead records each hole's goal and context.
  , forall (n :: S). Context n -> Bool
ctxDeferHoleMismatches :: Bool
    -- ^ How holes behave during unification, giving three modes overall. With
    -- 'ctxHolesAreErrors' a hole is rejected outright (strict). Otherwise a hole
    -- always unifies as a leaf; this flag then chooses what happens when the
    -- /surrounding/ structure disagrees: 'True' (the default) defers — any term
    -- containing a hole is accepted, for an in-progress sketch — while 'False'
    -- keeps such a mismatch an error ('structuralHoleUnify').
  , forall (n :: S). Context n -> [VarIdent]
ctxHintLemmas          :: [VarIdent]
    -- ^ Named top-level definitions a hole's candidate list may draw on, beyond
    -- the local hypotheses (see 'withHintLemmas').
  , forall (n :: S). Context n -> Bool
ctxWarnOverhang        :: Bool
    -- ^ When 'True', a restriction face or @recOR@ guard that overhangs the
    -- local tope context (is not entailed by it, while still overlapping it)
    -- is reported with a non-fatal hint. Off by default: deciding the
    -- overhang costs a solver entailment per face and guard, and the overhang
    -- is legitimate (see @happy-restrict-face-not-contained@). Enabled with
    -- @#set-option "warn-overhang" "yes"@. The /disjointness/ error next to
    -- it is unaffected: a vacuous face is always rejected.
  , forall (n :: S). Context n -> MetaPrefixSensitivity
ctxMetaPrefixSensitivity :: MetaPrefixSensitivity
    -- ^ How sensitively the meta-parameter layer check classifies use
    -- positions (see "Rzk.TypeCheck.MetaPrefix"). Strict by default; set
    -- with @#set-option "warn-meta-prefix" = "off" | "structural" | "strict"@.
  }

-- | The sensitivity levels of the meta-parameter layer check.
data MetaPrefixSensitivity
  = MetaPrefixOff
    -- ^ no meta-prefix warnings
  | MetaPrefixStructural
    -- ^ warn only at structurally object-level positions
  | MetaPrefixStrict
    -- ^ additionally require an unsaturated schema argument to sit within
    -- a top-level receiver's meta prefix (the default)
  deriving (MetaPrefixSensitivity -> MetaPrefixSensitivity -> Bool
(MetaPrefixSensitivity -> MetaPrefixSensitivity -> Bool)
-> (MetaPrefixSensitivity -> MetaPrefixSensitivity -> Bool)
-> Eq MetaPrefixSensitivity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MetaPrefixSensitivity -> MetaPrefixSensitivity -> Bool
== :: MetaPrefixSensitivity -> MetaPrefixSensitivity -> Bool
$c/= :: MetaPrefixSensitivity -> MetaPrefixSensitivity -> Bool
/= :: MetaPrefixSensitivity -> MetaPrefixSensitivity -> Bool
Eq, Int -> MetaPrefixSensitivity -> ShowS
[MetaPrefixSensitivity] -> ShowS
MetaPrefixSensitivity -> FilePath
(Int -> MetaPrefixSensitivity -> ShowS)
-> (MetaPrefixSensitivity -> FilePath)
-> ([MetaPrefixSensitivity] -> ShowS)
-> Show MetaPrefixSensitivity
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MetaPrefixSensitivity -> ShowS
showsPrec :: Int -> MetaPrefixSensitivity -> ShowS
$cshow :: MetaPrefixSensitivity -> FilePath
show :: MetaPrefixSensitivity -> FilePath
$cshowList :: [MetaPrefixSensitivity] -> ShowS
showList :: [MetaPrefixSensitivity] -> ShowS
Show)

-- | An open section: the entries declared in it, newest first.
data SectionInfo n = SectionInfo
  { forall (n :: S). SectionInfo n -> Maybe SectionName
sectionName    :: Maybe Rzk.SectionName
  , forall (n :: S). SectionInfo n -> [Name n]
sectionEntries :: [Foil.Name n]
  }

emptyContext :: Context Foil.VoidS
emptyContext :: Context 'VoidS
emptyContext = Context
  { ctxScope :: Scope 'VoidS
ctxScope = Scope 'VoidS
Foil.emptyScope
  , ctxVars :: NameMap 'VoidS (VarInfo 'VoidS)
ctxVars = NameMap 'VoidS (VarInfo 'VoidS)
forall a. NameMap 'VoidS a
Foil.emptyNameMap
  , ctxNamed :: Map VarIdent (Name 'VoidS)
ctxNamed = Map VarIdent (Name 'VoidS)
forall k a. Map k a
Map.empty
  , ctxBound :: [Name 'VoidS]
ctxBound = []
  , ctxSections :: [SectionInfo 'VoidS]
ctxSections = [Maybe SectionName -> [Name 'VoidS] -> SectionInfo 'VoidS
forall (n :: S). Maybe SectionName -> [Name n] -> SectionInfo n
SectionInfo Maybe SectionName
forall a. Maybe a
Nothing []]
  , ctxDiscreteTopes :: [ModalTope 'VoidS]
ctxDiscreteTopes = []
  , ctxTopes :: [ModalTope 'VoidS]
ctxTopes = [ModalTope 'VoidS]
forall (n :: S). [ModalTope n]
emptyTopeContext
  , ctxTopesNF :: [ModalTope 'VoidS]
ctxTopesNF = [ModalTope 'VoidS]
forall (n :: S). [ModalTope n]
emptyTopeContext
  , ctxTopesNFUnion :: [[ModalTope 'VoidS]]
ctxTopesNFUnion = [[ModalTope 'VoidS]
forall (n :: S). [ModalTope n]
emptyTopeContext]
  , ctxTopesEntailBottom :: Maybe Bool
ctxTopesEntailBottom = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
  , ctxTopesSaturated :: CachedSaturation 'VoidS
ctxTopesSaturated = CachedSaturation 'VoidS
forall (n :: S). CachedSaturation n
SaturationUncached
  , ctxShadow :: Map VarIdent [VarIdent]
ctxShadow = Map VarIdent [VarIdent]
forall k a. Map k a
Map.empty
  , ctxActionStack :: [Action 'VoidS]
ctxActionStack = []
  , ctxActionStackDepth :: Int
ctxActionStackDepth = Int
0
  , ctxCurrentCommand :: Maybe Command
ctxCurrentCommand = Maybe Command
forall a. Maybe a
Nothing
  , ctxLocation :: Maybe LocationInfo
ctxLocation = Maybe LocationInfo
forall a. Maybe a
Nothing
  , ctxVerbosity :: Verbosity
ctxVerbosity = Verbosity
Normal
  , ctxCovariance :: Covariance
ctxCovariance = Covariance
Covariant
  , ctxRenderBackend :: Maybe RenderBackend
ctxRenderBackend = Maybe RenderBackend
forall a. Maybe a
Nothing
  , ctxRenderHideTerm :: Bool
ctxRenderHideTerm = Bool
False
  , ctxHolesAreErrors :: Bool
ctxHolesAreErrors = Bool
True
  , ctxDeferHoleMismatches :: Bool
ctxDeferHoleMismatches = Bool
True
  , ctxHintLemmas :: [VarIdent]
ctxHintLemmas = []
  , ctxWarnOverhang :: Bool
ctxWarnOverhang = Bool
False
  , ctxMetaPrefixSensitivity :: MetaPrefixSensitivity
ctxMetaPrefixSensitivity = MetaPrefixSensitivity
MetaPrefixStrict
  }

-- | The tope context of an empty context: @⊤@ holds under every modality.
emptyTopeContext :: [ModalTope n]
emptyTopeContext :: forall (n :: S). [ModalTope n]
emptyTopeContext =
  [ TModality -> TModality -> TermT n -> ModalTope n
forall (n :: S). TModality -> TModality -> TermT n -> ModalTope n
ModalTope TModality
Id TModality
Id    TermT n
forall (n :: S). TermT n
topeTopT
  , TModality -> TModality -> TermT n -> ModalTope n
forall (n :: S). TModality -> TModality -> TermT n -> ModalTope n
ModalTope TModality
Id TModality
Flat  TermT n
forall (n :: S). TermT n
topeTopT
  , TModality -> TModality -> TermT n -> ModalTope n
forall (n :: S). TModality -> TModality -> TermT n -> ModalTope n
ModalTope TModality
Id TModality
Op    TermT n
forall (n :: S). TermT n
topeTopT
  , TModality -> TModality -> TermT n -> ModalTope n
forall (n :: S). TModality -> TModality -> TermT n -> ModalTope n
ModalTope TModality
Id TModality
Sharp TermT n
forall (n :: S). TermT n
topeTopT
  ]

-- * Entering a binder
--
-- $sinking
--
-- Everything in a context that mentions the scope is a term, or a container of
-- terms, and so is sinkable: a term whose free names lie in @n@ has its free
-- names in any @l@ that extends @n@. free-foil sinks such a value by coercion
-- (@sink = unsafeCoerce@, sound because @DExt n l@ makes the renaming the
-- identity on raw names; see §3.5 of the Foil paper), and the same argument
-- applies to a whole record of them: renaming every field along the identity is
-- the identity on the representation.
--
-- Two fields are /not/ sinkable, and 'enterBinder' restores both in the same
-- breath, which is why the coercion below is not exported:
--
--   * 'ctxScope' is the set of names /in/ @n@. It has to grow, not coerce —
--     tellingly, free-foil gives 'Foil.Scope' no 'Foil.Sinkable' instance.
--   * 'ctxVars' must stay total on the names in scope ('Foil.lookupName' assumes
--     it), so the new binder's entry has to be added.

-- | Sink a context along a scope extension. Unsound on its own: leaves 'ctxScope'
-- and 'ctxVars' describing the /old/ scope, and the caller must fix both. See the
-- note above; 'enterBinder' is the only caller.
sinkContextUnchecked :: DExt n l => Context n -> Context l
sinkContextUnchecked :: forall (n :: S) (l :: S). DExt n l => Context n -> Context l
sinkContextUnchecked = Context n -> Context l
forall a b. a -> b
unsafeCoerce

-- | Enter the scope of a binder: extend the scope with it, record what it is
-- called and what it stands for, and carry the rest of the context in.
enterBinder
  :: DExt n l
  => NameBinder n l
  -> VarInfo n       -- ^ its type, value and modality
  -> [ModalTope l]   -- ^ discreteness axioms the binder brings (a flat cube point,
                     --   which are about the variable itself, hence at its scope)
  -> Context n
  -> Context l
enterBinder :: forall (n :: S) (l :: S).
DExt n l =>
NameBinder n l
-> VarInfo n -> [ModalTope l] -> Context n -> Context l
enterBinder NameBinder n l
binder VarInfo n
info [ModalTope l]
discrete Context n
ctx = (Context n -> Context l
forall (n :: S) (l :: S). DExt n l => Context n -> Context l
sinkContextUnchecked Context n
ctx)
  { ctxScope = Foil.extendScope binder (ctxScope ctx)
  , ctxVars = Foil.addNameBinder binder (Foil.sink info) (sinkVars (ctxVars ctx))
  , ctxBound = Foil.nameOf binder : sinkNames (ctxBound ctx)
  , ctxNamed = case binderName (varOrig info) of
      Maybe VarIdent
Nothing   -> Map VarIdent (Name n) -> Map VarIdent (Name l)
forall (n :: S) (l :: S).
DExt n l =>
Map VarIdent (Name n) -> Map VarIdent (Name l)
sinkNamed (Context n -> Map VarIdent (Name n)
forall (n :: S). Context n -> Map VarIdent (Name n)
ctxNamed Context n
ctx)
      Just VarIdent
name -> VarIdent
-> Name l -> Map VarIdent (Name l) -> Map VarIdent (Name l)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VarIdent
name (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder) (Map VarIdent (Name n) -> Map VarIdent (Name l)
forall (n :: S) (l :: S).
DExt n l =>
Map VarIdent (Name n) -> Map VarIdent (Name l)
sinkNamed (Context n -> Map VarIdent (Name n)
forall (n :: S). Context n -> Map VarIdent (Name n)
ctxNamed Context n
ctx))
  , ctxDiscreteTopes = discrete <> sinkTopes (ctxDiscreteTopes ctx)
  , ctxShadow = addBinderNames (varOrig info) (ctxShadow ctx)
  }

-- | Enter a /fresh/ binder: one the checker invents rather than one a term
-- carries (to look under a Π when comparing two of them, say).
withFreshBinder
  :: Distinct n
  => Context n
  -> VarInfo n
  -> (forall l. DExt n l => NameBinder n l -> Context l -> r)
  -> r
withFreshBinder :: forall (n :: S) r.
Distinct n =>
Context n
-> VarInfo n
-> (forall (l :: S). DExt n l => NameBinder n l -> Context l -> r)
-> r
withFreshBinder Context n
ctx VarInfo n
info forall (l :: S). DExt n l => NameBinder n l -> Context l -> r
k =
  Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh (Context n -> Scope n
forall (n :: S). Context n -> Scope n
ctxScope Context n
ctx) ((forall (l :: S). DExt n l => NameBinder n l -> r) -> r)
-> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
    NameBinder n l -> Context l -> r
forall (l :: S). DExt n l => NameBinder n l -> Context l -> r
k NameBinder n l
binder (NameBinder n l
-> VarInfo n -> [ModalTope l] -> Context n -> Context l
forall (n :: S) (l :: S).
DExt n l =>
NameBinder n l
-> VarInfo n -> [ModalTope l] -> Context n -> Context l
enterBinder NameBinder n l
binder VarInfo n
info [] Context n
ctx)

-- | Record the name a binder introduces (if any), for the shadowing check.
addBinderNames :: Binder -> Map VarIdent [VarIdent] -> Map VarIdent [VarIdent]
addBinderNames :: Binder -> Map VarIdent [VarIdent] -> Map VarIdent [VarIdent]
addBinderNames Binder
orig Map VarIdent [VarIdent]
names =
  case Binder -> Maybe VarIdent
binderName Binder
orig of
    Maybe VarIdent
Nothing   -> Map VarIdent [VarIdent]
names
    Just VarIdent
name -> ([VarIdent] -> [VarIdent] -> [VarIdent])
-> VarIdent
-> [VarIdent]
-> Map VarIdent [VarIdent]
-> Map VarIdent [VarIdent]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [VarIdent] -> [VarIdent] -> [VarIdent]
forall a. Semigroup a => a -> a -> a
(<>) VarIdent
name [VarIdent
name] Map VarIdent [VarIdent]
names

-- | The identifiers in scope spelled like this one.
shadowedBy :: VarIdent -> Context n -> [VarIdent]
shadowedBy :: forall (n :: S). VarIdent -> Context n -> [VarIdent]
shadowedBy VarIdent
name Context n
ctx = [VarIdent] -> VarIdent -> Map VarIdent [VarIdent] -> [VarIdent]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] VarIdent
name (Context n -> Map VarIdent [VarIdent]
forall (n :: S). Context n -> Map VarIdent [VarIdent]
ctxShadow Context n
ctx)

-- * Sinking the parts

instance Foil.Sinkable VarInfo where
  sinkabilityProof :: forall (n :: S) (l :: S).
(Name n -> Name l) -> VarInfo n -> VarInfo l
sinkabilityProof Name n -> Name l
rename VarInfo n
info = VarInfo n
info
    { varType = Foil.sinkabilityProof rename (varType info)
    , varValue = Foil.sinkabilityProof rename <$> varValue info
    , varDeclaredAssumptions = rename <$> varDeclaredAssumptions info
    , varDataRole = renameRole <$> varDataRole info
    }
    where
      renameRole :: DataRole n -> DataRole l
renameRole DataRole n
role = DataRole n
role { dataRoleDataType = rename (dataRoleDataType role) }

instance Foil.Sinkable ModalTope where
  sinkabilityProof :: forall (n :: S) (l :: S).
(Name n -> Name l) -> ModalTope n -> ModalTope l
sinkabilityProof Name n -> Name l
rename ModalTope n
tope =
    ModalTope n
tope { tTope = Foil.sinkabilityProof rename (tTope tope) }

sinkVars :: DExt n l => NameMap n (VarInfo n) -> NameMap n (VarInfo l)
sinkVars :: forall (n :: S) (l :: S).
DExt n l =>
NameMap n (VarInfo n) -> NameMap n (VarInfo l)
sinkVars = NameMap n (VarInfo n) -> NameMap n (VarInfo l)
forall (f :: * -> *) (e :: S -> *) (n :: S) (l :: S).
(Functor f, Sinkable e, DExt n l) =>
f (e n) -> f (e l)
Foil.sink1

sinkTopes :: DExt n l => [ModalTope n] -> [ModalTope l]
sinkTopes :: forall (n :: S) (l :: S).
DExt n l =>
[ModalTope n] -> [ModalTope l]
sinkTopes = [ModalTope n] -> [ModalTope l]
forall (f :: * -> *) (e :: S -> *) (n :: S) (l :: S).
(Functor f, Sinkable e, DExt n l) =>
f (e n) -> f (e l)
Foil.sink1

sinkNamed :: DExt n l => Map VarIdent (Foil.Name n) -> Map VarIdent (Foil.Name l)
sinkNamed :: forall (n :: S) (l :: S).
DExt n l =>
Map VarIdent (Name n) -> Map VarIdent (Name l)
sinkNamed = Map VarIdent (Name n) -> Map VarIdent (Name l)
forall (f :: * -> *) (e :: S -> *) (n :: S) (l :: S).
(Functor f, Sinkable e, DExt n l) =>
f (e n) -> f (e l)
Foil.sink1

sinkNames :: DExt n l => [Foil.Name n] -> [Foil.Name l]
sinkNames :: forall (n :: S) (l :: S). DExt n l => [Name n] -> [Name l]
sinkNames = [Name n] -> [Name l]
forall (f :: * -> *) (e :: S -> *) (n :: S) (l :: S).
(Functor f, Sinkable e, DExt n l) =>
f (e n) -> f (e l)
Foil.sink1

-- * Lookup

-- | What a name stands for. Total: every name in scope has an entry.
lookupVarInfo :: Foil.Name n -> Context n -> VarInfo n
lookupVarInfo :: forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo Name n
name Context n
ctx = Name n -> NameMap n (VarInfo n) -> VarInfo n
forall (n :: S) a. Name n -> NameMap n a -> a
Foil.lookupName Name n
name (Context n -> NameMap n (VarInfo n)
forall (n :: S). Context n -> NameMap n (VarInfo n)
ctxVars Context n
ctx)

-- | What every name in scope stands for, in no particular order.
varInfos :: Context n -> [VarInfo n]
varInfos :: forall (n :: S). Context n -> [VarInfo n]
varInfos Context n
ctx = IntMap (VarInfo n) -> [VarInfo n]
forall a. IntMap a -> [a]
IntMap.elems IntMap (VarInfo n)
m
  where
    NameMap IntMap (VarInfo n)
m = Context n -> NameMap n (VarInfo n)
forall (n :: S). Context n -> NameMap n (VarInfo n)
ctxVars Context n
ctx

-- | Every hypothesis in scope, oldest binding first (see 'ctxBound': the ids
-- themselves do not tell us this).
varsInScope :: Context n -> [(Foil.Name n, VarInfo n)]
varsInScope :: forall (n :: S). Context n -> [(Name n, VarInfo n)]
varsInScope Context n
ctx =
  [ (Name n
name, Name n -> Context n -> VarInfo n
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo Name n
name Context n
ctx) | Name n
name <- [Name n] -> [Name n]
forall a. [a] -> [a]
reverse (Context n -> [Name n]
forall (n :: S). Context n -> [Name n]
ctxBound Context n
ctx) ]

-- | The name a surface identifier resolves to, if any.
lookupNamed :: VarIdent -> Context n -> Maybe (Foil.Name n)
lookupNamed :: forall (n :: S). VarIdent -> Context n -> Maybe (Name n)
lookupNamed VarIdent
name Context n
ctx = VarIdent -> Map VarIdent (Name n) -> Maybe (Name n)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VarIdent
name (Context n -> Map VarIdent (Name n)
forall (n :: S). Context n -> Map VarIdent (Name n)
ctxNamed Context n
ctx)

-- | The display binder of a name (the whole pattern, for projection folding).
binderOfName :: Foil.Name n -> Context n -> Binder
binderOfName :: forall (n :: S). Name n -> Context n -> Binder
binderOfName Name n
name = VarInfo n -> Binder
forall (n :: S). VarInfo n -> Binder
varOrig (VarInfo n -> Binder)
-> (Context n -> VarInfo n) -> Context n -> Binder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name n -> Context n -> VarInfo n
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo Name n
name

-- * Modalities

class ModeTheory m where
    iden :: m
    comp :: m -> m -> m
    coe :: m -> m -> Bool
    isRA :: m -> Bool

instance ModeTheory TModality where
  iden :: TModality
iden = TModality
Id

  comp :: TModality -> TModality -> TModality
comp TModality
Flat TModality
Flat   = TModality
Flat
  comp TModality
Flat TModality
Sharp  = TModality
Flat
  comp TModality
Flat TModality
Op     = TModality
Flat
  comp TModality
Op TModality
Flat     = TModality
Flat
  comp TModality
Sharp TModality
Sharp = TModality
Sharp
  comp TModality
Sharp TModality
Flat  = TModality
Sharp
  comp TModality
Sharp TModality
Op    = TModality
Sharp
  comp TModality
Op TModality
Sharp    = TModality
Sharp
  comp TModality
Op TModality
Op       = TModality
Id
  comp TModality
Id TModality
m        = TModality
m
  comp TModality
m TModality
Id        = TModality
m

  coe :: TModality -> TModality -> Bool
coe TModality
Flat TModality
Id    = Bool
True
  coe TModality
Flat TModality
Op    = Bool
True
  coe TModality
Id TModality
Sharp   = Bool
True
  coe TModality
Flat TModality
Sharp = Bool
True
  coe TModality
Op TModality
Sharp   = Bool
True
  coe TModality
a TModality
b        = TModality
a TModality -> TModality -> Bool
forall a. Eq a => a -> a -> Bool
== TModality
b

  isRA :: TModality -> Bool
isRA TModality
Sharp = Bool
True
  isRA TModality
Op    = Bool
True
  isRA TModality
Id    = Bool
True
  isRA TModality
_     = Bool
False

-- | Accumulate a modality (a lock) over the hypotheses and the topes.
--
-- Note that top-level entries are /not/ touched: a top-level variable is exempt
-- from the accessibility check (see @infer@), so accumulating a modality over
-- them was work with no observable effect. The old context did it to all ~1500
-- of them on every modal binder.
applyModality :: TModality -> Context n -> Context n
applyModality :: forall (n :: S). TModality -> Context n -> Context n
applyModality TModality
md Context n
ctx = Context n
ctx
  { ctxVars = mapNameMap addToVar (ctxVars ctx)
  , ctxTopes = map addToTope (ctxTopes ctx)
  , ctxTopesNF = map addToTope (ctxTopesNF ctx)
  , ctxTopesNFUnion = map (map addToTope) (ctxTopesNFUnion ctx)
  , ctxTopesSaturated = SaturationUncached  -- accessibility changed
  }
  where
    addToVar :: VarInfo n -> VarInfo n
addToVar VarInfo n
info
      | VarInfo n -> Bool
forall (n :: S). VarInfo n -> Bool
varIsTopLevel VarInfo n
info = VarInfo n
info
      | Bool
otherwise = VarInfo n
info { varModAccum = comp (varModAccum info) md }
    addToTope :: ModalTope n -> ModalTope n
addToTope ModalTope n
tope = ModalTope n
tope { tModAccum = comp (tModAccum tope) md }

-- | Map the values of a name map, keeping its keys.
mapNameMap :: (a -> b) -> NameMap n a -> NameMap n b
mapNameMap :: forall a b (n :: S). (a -> b) -> NameMap n a -> NameMap n b
mapNameMap a -> b
f (NameMap IntMap a
m) = IntMap b -> NameMap n b
forall (n :: S) a. IntMap a -> NameMap n a
NameMap ((a -> b) -> IntMap a -> IntMap b
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map a -> b
f IntMap a
m)

-- | Replace what a name stands for.
--
-- Closing a section rewrites the definitions made in it, so that each takes the
-- section's assumptions as explicit parameters; this is how the rewritten entries
-- go back into the context.
insertVarInfo :: Foil.Name n -> VarInfo n -> Context n -> Context n
insertVarInfo :: forall (n :: S). Name n -> VarInfo n -> Context n -> Context n
insertVarInfo Name n
name VarInfo n
info Context n
ctx = Context n
ctx { ctxVars = replace (ctxVars ctx) }
  where
    replace :: NameMap n (VarInfo n) -> NameMap n (VarInfo n)
replace (NameMap IntMap (VarInfo n)
m) = IntMap (VarInfo n) -> NameMap n (VarInfo n)
forall (n :: S) a. IntMap a -> NameMap n a
NameMap (Int -> VarInfo n -> IntMap (VarInfo n) -> IntMap (VarInfo n)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (Name n -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name n
name) VarInfo n
info IntMap (VarInfo n)
m)

-- * Topes

isAccessible :: ModalTope n -> Bool
isAccessible :: forall (n :: S). ModalTope n -> Bool
isAccessible ModalTope n
mt = TModality -> TModality -> Bool
forall m. ModeTheory m => m -> m -> Bool
coe (ModalTope n -> TModality
forall (n :: S). ModalTope n -> TModality
tModVar ModalTope n
mt) (ModalTope n -> TModality
forall (n :: S). ModalTope n -> TModality
tModAccum ModalTope n
mt)

filterAccessible :: [ModalTope n] -> [ModalTope n]
filterAccessible :: forall (n :: S). [ModalTope n] -> [ModalTope n]
filterAccessible = (ModalTope n -> Bool) -> [ModalTope n] -> [ModalTope n]
forall a. (a -> Bool) -> [a] -> [a]
filter ModalTope n -> Bool
forall (n :: S). ModalTope n -> Bool
isAccessible

accessibleTopes :: [ModalTope n] -> [TermT n]
accessibleTopes :: forall (n :: S). [ModalTope n] -> [TermT n]
accessibleTopes = (ModalTope n -> TermT n) -> [ModalTope n] -> [TermT n]
forall a b. (a -> b) -> [a] -> [b]
map ModalTope n -> TermT n
forall (n :: S). ModalTope n -> TermT n
tTope ([ModalTope n] -> [TermT n])
-> ([ModalTope n] -> [ModalTope n]) -> [ModalTope n] -> [TermT n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ModalTope n] -> [ModalTope n]
forall (n :: S). [ModalTope n] -> [ModalTope n]
filterAccessible

plainTope :: TermT n -> ModalTope n
plainTope :: forall (n :: S). TermT n -> ModalTope n
plainTope = TModality -> TModality -> TermT n -> ModalTope n
forall (n :: S). TModality -> TModality -> TermT n -> ModalTope n
ModalTope TModality
Id TModality
Id

availableTopes :: Context n -> [TermT n]
availableTopes :: forall (n :: S). Context n -> [TermT n]
availableTopes = [ModalTope n] -> [TermT n]
forall (n :: S). [ModalTope n] -> [TermT n]
accessibleTopes ([ModalTope n] -> [TermT n])
-> (Context n -> [ModalTope n]) -> Context n -> [TermT n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context n -> [ModalTope n]
forall (n :: S). Context n -> [ModalTope n]
ctxTopes

availableTopesNF :: Context n -> [TermT n]
availableTopesNF :: forall (n :: S). Context n -> [TermT n]
availableTopesNF = [ModalTope n] -> [TermT n]
forall (n :: S). [ModalTope n] -> [TermT n]
accessibleTopes ([ModalTope n] -> [TermT n])
-> (Context n -> [ModalTope n]) -> Context n -> [TermT n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context n -> [ModalTope n]
forall (n :: S). Context n -> [ModalTope n]
ctxTopesNF

-- * Hole modes

-- | Switch to lenient hole mode: record each hole's goal and context instead of
-- reporting it as an error.
allowHoles :: Context n -> Context n
allowHoles :: forall (n :: S). Context n -> Context n
allowHoles Context n
ctx = Context n
ctx { ctxHolesAreErrors = False }

-- | Allow a hole's candidate list to draw on the given named top-level
-- definitions, in addition to the local hypotheses.
withHintLemmas :: [VarIdent] -> Context n -> Context n
withHintLemmas :: forall (n :: S). [VarIdent] -> Context n -> Context n
withHintLemmas [VarIdent]
lemmas Context n
ctx = Context n
ctx { ctxHintLemmas = lemmas }

-- | Within the given action, a hole unifies only as a leaf of an otherwise
-- matching structure: a structural mismatch around a hole stays an error rather
-- than being deferred (see 'ctxDeferHoleMismatches').
structuralHoleUnify :: Context n -> Context n
structuralHoleUnify :: forall (n :: S). Context n -> Context n
structuralHoleUnify Context n
ctx = Context n
ctx { ctxDeferHoleMismatches = False }