{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards   #-}

-- | The checker's monad.
--
-- @TypeCheck n@ is the old @TypeCheck var@ with the scope index in place of the
-- variable type. The error channel, though, is /not/ indexed: an error carries
-- the context it was raised in (see "Rzk.TypeCheck.Error"). That is what makes
-- 'inContext' a one-liner — running a judgement in an inner scope is just running
-- it under a different reader, with nothing to re-index on the way out. The old
-- @closeScope@ had to wrap the error one binder deeper and re-emit the holes.
module Rzk.TypeCheck.Monad where

import           Control.Monad            (unless)
import           Control.Monad.Except     (ExceptT,
                                           MonadError (catchError, throwError),
                                           runExceptT)
import           Control.Monad.Reader     (ReaderT (..), ask, asks, local)
import           Control.Monad.Trans      (lift)
import           Control.Monad.Trans.State.Strict (State, get, modify', put,
                                           runState)
import           Debug.Trace              (trace)

import           Control.Monad.Foil       (Distinct)
import qualified Control.Monad.Foil       as Foil

import           Language.Rzk.Foil.Names (VarIdent)
import           Language.Rzk.Foil.Syntax (positionOfTerm)
import           Rzk.TypeCheck.Context
import           Rzk.TypeCheck.Display
import           Rzk.TypeCheck.Error

-- | A binding shown in a hole's local context: the display name and its type,
-- already rendered.
data HoleEntry = HoleEntry
  { HoleEntry -> VarIdent
holeEntryName :: VarIdent
  , HoleEntry -> Rendered
holeEntryType :: Rendered
  } deriving (HoleEntry -> HoleEntry -> Bool
(HoleEntry -> HoleEntry -> Bool)
-> (HoleEntry -> HoleEntry -> Bool) -> Eq HoleEntry
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HoleEntry -> HoleEntry -> Bool
== :: HoleEntry -> HoleEntry -> Bool
$c/= :: HoleEntry -> HoleEntry -> Bool
/= :: HoleEntry -> HoleEntry -> Bool
Eq, Int -> HoleEntry -> ShowS
[HoleEntry] -> ShowS
HoleEntry -> String
(Int -> HoleEntry -> ShowS)
-> (HoleEntry -> String)
-> ([HoleEntry] -> ShowS)
-> Show HoleEntry
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HoleEntry -> ShowS
showsPrec :: Int -> HoleEntry -> ShowS
$cshow :: HoleEntry -> String
show :: HoleEntry -> String
$cshowList :: [HoleEntry] -> ShowS
showList :: [HoleEntry] -> ShowS
Show)

-- | The structured goal and context at a hole, recorded in lenient mode (see
-- 'allowHoles'). Everything is rendered to user-facing names at record time, so
-- 'HoleInfo' is independent of the scope it came from. Local hypotheses are split
-- into ordinary term variables and cube variables (the cube/tope layer is
-- specific to Rzk); the global environment is deliberately excluded — it belongs
-- in a searchable inventory, not the goal panel.
data HoleInfo = HoleInfo
  { HoleInfo -> Maybe VarIdent
holeName          :: Maybe VarIdent -- ^ the @?name@, if the hole was named
  , HoleInfo -> Rendered
holeGoal          :: Rendered       -- ^ expected type (the goal), kept symbolic
  , HoleInfo -> Maybe (VarIdent, Rendered)
holeGoalShape     :: Maybe (VarIdent, Rendered)
    -- ^ when the goal is a /shape/ (the hole is the argument of a
    -- shape-restricted function), the shape's bound variable and its tope: the
    -- goal then reads @(binder : holeGoal | tope)@. 'Nothing' for an ordinary
    -- goal. (Extension-type goals need no special handling — they are already a
    -- restricted type in 'holeGoal'.)
  , HoleInfo -> [HoleEntry]
holeTermVars      :: [HoleEntry]    -- ^ local hypotheses whose type is not a cube
  , HoleInfo -> [HoleEntry]
holeCubeVars      :: [HoleEntry]    -- ^ local cube variables (type is a cube)
  , HoleInfo -> [Rendered]
holeTopes         :: [Rendered]     -- ^ local tope assumptions (excluding ⊤)
  , HoleInfo -> [Rendered]
holeCandidates    :: [Rendered]
    -- ^ elimination spines over the local hypotheses whose type fits the goal,
    -- with applied arguments left as holes. Already rendered, like the rest.
  , HoleInfo -> [Rendered]
holeIntroductions :: [Rendered]
    -- ^ introduction forms for the goal type, built from its head constructor
    -- with the constituents left as holes. Already rendered, like the rest.
  , HoleInfo -> Maybe String
holeDiagram       :: Maybe String
    -- ^ an SVG of the goal cell, when the goal is a renderable shape (an arrow,
    -- triangle, or square up to dimension 3).
  , HoleInfo -> Maybe LocationInfo
holeLocation      :: Maybe LocationInfo
  } deriving (HoleInfo -> HoleInfo -> Bool
(HoleInfo -> HoleInfo -> Bool)
-> (HoleInfo -> HoleInfo -> Bool) -> Eq HoleInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HoleInfo -> HoleInfo -> Bool
== :: HoleInfo -> HoleInfo -> Bool
$c/= :: HoleInfo -> HoleInfo -> Bool
/= :: HoleInfo -> HoleInfo -> Bool
Eq, Int -> HoleInfo -> ShowS
[HoleInfo] -> ShowS
HoleInfo -> String
(Int -> HoleInfo -> ShowS)
-> (HoleInfo -> String) -> ([HoleInfo] -> ShowS) -> Show HoleInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HoleInfo -> ShowS
showsPrec :: Int -> HoleInfo -> ShowS
$cshow :: HoleInfo -> String
show :: HoleInfo -> String
$cshowList :: [HoleInfo] -> ShowS
showList :: [HoleInfo] -> ShowS
Show)

-- | A non-fatal finding of the checker, recorded on the writer channel
-- beside the holes and carried out of a run in @Checked@. Structured, so
-- the CLI, the LSP, and (later) safe mode each decide how to present or
-- escalate it.
data CheckWarning
  = LargeInductiveTypeWarning
      VarIdent              -- ^ the data type
      VarIdent              -- ^ the constructor whose field stores a universe
      (Maybe LocationInfo)
  | MetaPrefixWarning
      VarIdent              -- ^ the declaration whose type or body contains the use
      VarIdent              -- ^ the declaration used with too few meta-prefix arguments
      Int                   -- ^ the arguments supplied
      Int                   -- ^ the length of the meta prefix
      MetaPrefixRule
      (Maybe LocationInfo)
  deriving (CheckWarning -> CheckWarning -> Bool
(CheckWarning -> CheckWarning -> Bool)
-> (CheckWarning -> CheckWarning -> Bool) -> Eq CheckWarning
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CheckWarning -> CheckWarning -> Bool
== :: CheckWarning -> CheckWarning -> Bool
$c/= :: CheckWarning -> CheckWarning -> Bool
/= :: CheckWarning -> CheckWarning -> Bool
Eq, Int -> CheckWarning -> ShowS
[CheckWarning] -> ShowS
CheckWarning -> String
(Int -> CheckWarning -> ShowS)
-> (CheckWarning -> String)
-> ([CheckWarning] -> ShowS)
-> Show CheckWarning
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CheckWarning -> ShowS
showsPrec :: Int -> CheckWarning -> ShowS
$cshow :: CheckWarning -> String
show :: CheckWarning -> String
$cshowList :: [CheckWarning] -> ShowS
showList :: [CheckWarning] -> ShowS
Show)

-- | Where a warning points, for per-file attribution.
warningLocation :: CheckWarning -> Maybe LocationInfo
warningLocation :: CheckWarning -> Maybe LocationInfo
warningLocation (LargeInductiveTypeWarning VarIdent
_ VarIdent
_ Maybe LocationInfo
loc)  = Maybe LocationInfo
loc
warningLocation (MetaPrefixWarning VarIdent
_ VarIdent
_ Int
_ Int
_ MetaPrefixRule
_ Maybe LocationInfo
loc)    = Maybe LocationInfo
loc

-- | Which candidate rule of the meta-parameter layer check flags a
-- 'MetaPrefixWarning' (see "Rzk.TypeCheck.MetaPrefix"): the structural
-- rule, or only its stricter variant. Both are emitted so the two
-- candidate defaults can be measured on a corpus side by side.
data MetaPrefixRule
  = MetaPrefixBoth
  | MetaPrefixStrictOnly
  deriving (MetaPrefixRule -> MetaPrefixRule -> Bool
(MetaPrefixRule -> MetaPrefixRule -> Bool)
-> (MetaPrefixRule -> MetaPrefixRule -> Bool) -> Eq MetaPrefixRule
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MetaPrefixRule -> MetaPrefixRule -> Bool
== :: MetaPrefixRule -> MetaPrefixRule -> Bool
$c/= :: MetaPrefixRule -> MetaPrefixRule -> Bool
/= :: MetaPrefixRule -> MetaPrefixRule -> Bool
Eq, Int -> MetaPrefixRule -> ShowS
[MetaPrefixRule] -> ShowS
MetaPrefixRule -> String
(Int -> MetaPrefixRule -> ShowS)
-> (MetaPrefixRule -> String)
-> ([MetaPrefixRule] -> ShowS)
-> Show MetaPrefixRule
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MetaPrefixRule -> ShowS
showsPrec :: Int -> MetaPrefixRule -> ShowS
$cshow :: MetaPrefixRule -> String
show :: MetaPrefixRule -> String
$cshowList :: [MetaPrefixRule] -> ShowS
showList :: [MetaPrefixRule] -> ShowS
Show)

-- | What a run records besides its result: the holes it found and the non-fatal
-- findings it made. Both accumulate in reverse and are turned around by
-- 'checkLog' when the run ends.
data CheckLog = CheckLog
  { CheckLog -> [HoleInfo]
logHolesRev    :: [HoleInfo]
  , CheckLog -> [CheckWarning]
logWarningsRev :: [CheckWarning]
  }

emptyCheckLog :: CheckLog
emptyCheckLog :: CheckLog
emptyCheckLog = [HoleInfo] -> [CheckWarning] -> CheckLog
CheckLog [] []

-- | What a run recorded, in the order it was recorded.
checkLog :: CheckLog -> ([HoleInfo], [CheckWarning])
checkLog :: CheckLog -> ([HoleInfo], [CheckWarning])
checkLog (CheckLog [HoleInfo]
holes [CheckWarning]
warnings) = ([HoleInfo] -> [HoleInfo]
forall a. [a] -> [a]
reverse [HoleInfo]
holes, [CheckWarning] -> [CheckWarning]
forall a. [a] -> [a]
reverse [CheckWarning]
warnings)

-- | The record of a run is kept in the /state/, beneath the error channel,
-- rather than on a writer channel above it.
--
-- The two differ exactly where a caught error is concerned: a writer discards
-- what the failing action wrote, and the state keeps it. That is what the
-- checker wants. A command that fails still reports the holes the user wrote in
-- it, and checking goes on to the next command with those holes in hand (see
-- @withCommand@ in "Rzk.TypeCheck.Decl"). A probe that wants the older
-- behaviour asks for it, with 'suppressing'.
type TypeCheck n =
  ReaderT (Context n)
    (ExceptT TypeErrorInScopedContext (State CheckLog))

-- | Run a judgement in a given context, keeping what it recorded.
runTypeCheckWith
  :: Context n -> TypeCheck n a
  -> (Either TypeErrorInScopedContext a, ([HoleInfo], [CheckWarning]))
runTypeCheckWith :: forall (n :: S) a.
Context n
-> TypeCheck n a
-> (Either TypeErrorInScopedContext a,
    ([HoleInfo], [CheckWarning]))
runTypeCheckWith Context n
ctx TypeCheck n a
tc =
  case State CheckLog (Either TypeErrorInScopedContext a)
-> CheckLog -> (Either TypeErrorInScopedContext a, CheckLog)
forall s a. State s a -> s -> (a, s)
runState (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity) a
-> State CheckLog (Either TypeErrorInScopedContext a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (TypeCheck n a
-> Context n
-> ExceptT TypeErrorInScopedContext (StateT CheckLog Identity) a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT TypeCheck n a
tc Context n
ctx)) CheckLog
emptyCheckLog of
    (Either TypeErrorInScopedContext a
result, CheckLog
logged) -> (Either TypeErrorInScopedContext a
result, CheckLog -> ([HoleInfo], [CheckWarning])
checkLog CheckLog
logged)

-- | Run a judgement in the empty context, discarding the holes it records.
runTypeCheck :: TypeCheck Foil.VoidS a -> Either TypeErrorInScopedContext a
runTypeCheck :: forall a. TypeCheck 'VoidS a -> Either TypeErrorInScopedContext a
runTypeCheck = Context 'VoidS
-> TypeCheck 'VoidS a -> Either TypeErrorInScopedContext a
forall (n :: S) a.
Context n -> TypeCheck n a -> Either TypeErrorInScopedContext a
runTypeCheckIn Context 'VoidS
emptyContext

-- | Run a judgement in a given context, discarding the holes it records.
runTypeCheckIn :: Context n -> TypeCheck n a -> Either TypeErrorInScopedContext a
runTypeCheckIn :: forall (n :: S) a.
Context n -> TypeCheck n a -> Either TypeErrorInScopedContext a
runTypeCheckIn Context n
ctx TypeCheck n a
tc = (Either TypeErrorInScopedContext a, ([HoleInfo], [CheckWarning]))
-> Either TypeErrorInScopedContext a
forall a b. (a, b) -> a
fst (Context n
-> TypeCheck n a
-> (Either TypeErrorInScopedContext a,
    ([HoleInfo], [CheckWarning]))
forall (n :: S) a.
Context n
-> TypeCheck n a
-> (Either TypeErrorInScopedContext a,
    ([HoleInfo], [CheckWarning]))
runTypeCheckWith Context n
ctx TypeCheck n a
tc)

-- | Run a judgement in another scope's context.
--
-- The error channel and the hole channel are shared and carry no scope index, so
-- there is nothing to translate: this is 'runReaderT' with the inner scope's
-- context, lifted back. Holes recorded inside land in the same state, and an
-- error thrown inside already carries its own context.
inContext :: Context l -> TypeCheck l a -> TypeCheck n a
inContext :: forall (l :: S) a (n :: S).
Context l -> TypeCheck l a -> TypeCheck n a
inContext Context l
ctx = ExceptT TypeErrorInScopedContext (StateT CheckLog Identity) a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall (m :: * -> *) a. Monad m => m a -> ReaderT (Context n) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity) a
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a)
-> (TypeCheck l a
    -> ExceptT TypeErrorInScopedContext (StateT CheckLog Identity) a)
-> TypeCheck l a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeCheck l a
 -> Context l
 -> ExceptT TypeErrorInScopedContext (StateT CheckLog Identity) a)
-> Context l
-> TypeCheck l a
-> ExceptT TypeErrorInScopedContext (StateT CheckLog Identity) a
forall a b c. (a -> b -> c) -> b -> a -> c
flip TypeCheck l a
-> Context l
-> ExceptT TypeErrorInScopedContext (StateT CheckLog Identity) a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Context l
ctx

-- * Errors

-- | Raise a type error, capturing the context it happened in.
issueTypeError :: Distinct n => TypeError n -> TypeCheck n a
issueTypeError :: forall (n :: S) a. Distinct n => TypeError n -> TypeCheck n a
issueTypeError TypeError n
err = do
  ctx <- ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
  (Context n)
forall r (m :: * -> *). MonadReader r m => m r
ask
  throwError (TypeErrorInScopedContext ctx err)

issueWarning :: String -> TypeCheck n ()
issueWarning :: forall (n :: S). String -> TypeCheck n ()
issueWarning String
message = String -> TypeCheck n () -> TypeCheck n ()
forall a. String -> a -> a
trace (String
"Warning: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
message) (() -> TypeCheck n ()
forall a.
a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return ())

-- * Tracing

trace' :: Verbosity -> Verbosity -> String -> a -> a
trace' :: forall a. Verbosity -> Verbosity -> String -> a -> a
trace' Verbosity
Silent Verbosity
_ String
_ = a -> a
forall a. a -> a
id
trace' Verbosity
Normal Verbosity
Debug String
_ = a -> a
forall a. a -> a
id
trace' Verbosity
_ Verbosity
_ String
msg = String -> a -> a
forall a. String -> a -> a
trace String
msg

traceTypeCheck :: Verbosity -> String -> TypeCheck n a -> TypeCheck n a
traceTypeCheck :: forall (n :: S) a.
Verbosity -> String -> TypeCheck n a -> TypeCheck n a
traceTypeCheck Verbosity
verbosity String
msg TypeCheck n a
action = do
  configuredVerbosity <- (Context n -> Verbosity)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     Verbosity
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context n -> Verbosity
forall (n :: S). Context n -> Verbosity
ctxVerbosity
  trace' configuredVerbosity verbosity msg action

localVerbosity :: Verbosity -> TypeCheck n a -> TypeCheck n a
localVerbosity :: forall (n :: S) a. Verbosity -> TypeCheck n a -> TypeCheck n a
localVerbosity Verbosity
verbosity = (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a.
(Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Context n -> Context n)
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a)
-> (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a b. (a -> b) -> a -> b
$ \Context n
ctx -> Context n
ctx { ctxVerbosity = verbosity }

localRenderBackend :: Maybe RenderBackend -> TypeCheck n a -> TypeCheck n a
localRenderBackend :: forall (n :: S) a.
Maybe RenderBackend -> TypeCheck n a -> TypeCheck n a
localRenderBackend Maybe RenderBackend
backend = (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a.
(Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Context n -> Context n)
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a)
-> (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a b. (a -> b) -> a -> b
$ \Context n
ctx -> Context n
ctx { ctxRenderBackend = backend }

localHideTerm :: Bool -> TypeCheck n a -> TypeCheck n a
localHideTerm :: forall (n :: S) a. Bool -> TypeCheck n a -> TypeCheck n a
localHideTerm Bool
hide = (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a.
(Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Context n -> Context n)
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a)
-> (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a b. (a -> b) -> a -> b
$ \Context n
ctx -> Context n
ctx { ctxRenderHideTerm = hide }

localWarnOverhang :: Bool -> TypeCheck n a -> TypeCheck n a
localWarnOverhang :: forall (n :: S) a. Bool -> TypeCheck n a -> TypeCheck n a
localWarnOverhang Bool
warn = (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a.
(Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Context n -> Context n)
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a)
-> (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a b. (a -> b) -> a -> b
$ \Context n
ctx -> Context n
ctx { ctxWarnOverhang = warn }

localMetaPrefixSensitivity :: MetaPrefixSensitivity -> TypeCheck n a -> TypeCheck n a
localMetaPrefixSensitivity :: forall (n :: S) a.
MetaPrefixSensitivity -> TypeCheck n a -> TypeCheck n a
localMetaPrefixSensitivity MetaPrefixSensitivity
sensitivity =
  (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a.
(Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Context n -> Context n)
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a)
-> (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a b. (a -> b) -> a -> b
$ \Context n
ctx -> Context n
ctx { ctxMetaPrefixSensitivity = sensitivity }

-- | Render the enclosed action with the proof term hidden.
hidingTerm :: TypeCheck n a -> TypeCheck n a
hidingTerm :: forall (n :: S) a. TypeCheck n a -> TypeCheck n a
hidingTerm = Bool -> TypeCheck n a -> TypeCheck n a
forall (n :: S) a. Bool -> TypeCheck n a -> TypeCheck n a
localHideTerm Bool
True

-- * Variance

switchVariance :: TypeCheck n a -> TypeCheck n a
switchVariance :: forall (n :: S) a. TypeCheck n a -> TypeCheck n a
switchVariance = (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a.
(Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Context n -> Context n)
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a)
-> (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a b. (a -> b) -> a -> b
$ \Context n
ctx -> Context n
ctx { ctxCovariance = switch (ctxCovariance ctx) }
  where
    switch :: Covariance -> Covariance
switch Covariance
Covariant     = Covariance
Contravariant
    switch Covariance
Contravariant = Covariance
Covariant
    switch Covariance
Invariant     = Covariance
Invariant

setVariance :: Covariance -> TypeCheck n a -> TypeCheck n a
setVariance :: forall (n :: S) a. Covariance -> TypeCheck n a -> TypeCheck n a
setVariance Covariance
variance = (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a.
(Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Context n -> Context n)
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a)
-> (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a b. (a -> b) -> a -> b
$ \Context n
ctx -> Context n
ctx { ctxCovariance = variance }

-- * The judgement stack

-- | The depth of nested judgements at which type checking gives up. Well-typed
-- input stays far below it; the cap catches a non-terminating search.
-- FIXME: expose as a parameter (@--max-depth@ and @rzk.yaml@).
maxActionStackDepth :: Int
maxActionStackDepth :: Int
maxActionStackDepth = Int
1000

performing :: Distinct n => Action n -> TypeCheck n a -> TypeCheck n a
performing :: forall (n :: S) a.
Distinct n =>
Action n -> TypeCheck n a -> TypeCheck n a
performing Action n
action TypeCheck n a
tc = do
  ctx@Context{..} <- ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
  (Context n)
forall r (m :: * -> *). MonadReader r m => m r
ask
  unless (ctxActionStackDepth < maxActionStackDepth) $
    issueTypeError $ TypeErrorOther "maximum depth reached"
  let ctx' = Context n
ctx
        { ctxActionStack = action : ctxActionStack
        , ctxActionStackDepth = ctxActionStackDepth + 1
        , ctxLocation = narrowLocation action ctxLocation
        }
  -- The trace message is built only when it is actually printed: at normal
  -- verbosity rendering the action's terms on every judgement would cost a
  -- thunk per judgement.
  if ctxVerbosity <= Debug
    then trace (ppAction (namingOfContext ctx) ctxActionStackDepth action) $
           local (const ctx') tc
    else local (const ctx') tc

-- | Point the location at the sub-term an action is about.
--
-- The checker descends through 'performing', so the location narrows as it
-- goes and an error is reported where the sub-term that caused it was written,
-- rather than at the declaration it is in (issue #81). A judgement about a term
-- the checker built itself carries no position, and leaves the location as it
-- found it: that is the innermost enclosing term the user did write.
narrowLocation :: Action n -> Maybe LocationInfo -> Maybe LocationInfo
narrowLocation :: forall (n :: S).
Action n -> Maybe LocationInfo -> Maybe LocationInfo
narrowLocation Action n
action Maybe LocationInfo
loc = case Action n -> Maybe (Term n)
forall {n :: S}. Action n -> Maybe (Term n)
termOf Action n
action of
  Just Term n
term | Just RzkPosition
pos <- Term n -> Maybe RzkPosition
forall (n :: S). Term n -> Maybe RzkPosition
positionOfTerm Term n
term -> RzkPosition -> LocationInfo -> LocationInfo
atPosition RzkPosition
pos (LocationInfo -> LocationInfo)
-> Maybe LocationInfo -> Maybe LocationInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe LocationInfo
loc
  Maybe (Term n)
_                                           -> Maybe LocationInfo
loc
  where
    termOf :: Action n -> Maybe (Term n)
termOf (ActionTypeCheck Term n
term TermT n
_) = Term n -> Maybe (Term n)
forall a. a -> Maybe a
Just Term n
term
    termOf (ActionInfer Term n
term)       = Term n -> Maybe (Term n)
forall a. a -> Maybe a
Just Term n
term
    termOf Action n
_                        = Maybe (Term n)
forall a. Maybe a
Nothing

-- * What a run records

modifyLog :: (CheckLog -> CheckLog) -> TypeCheck n ()
modifyLog :: forall (n :: S). (CheckLog -> CheckLog) -> TypeCheck n ()
modifyLog CheckLog -> CheckLog
f = ExceptT TypeErrorInScopedContext (StateT CheckLog Identity) ()
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT (Context n) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (State CheckLog ()
-> ExceptT TypeErrorInScopedContext (StateT CheckLog Identity) ()
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT TypeErrorInScopedContext m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ((CheckLog -> CheckLog) -> State CheckLog ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify' CheckLog -> CheckLog
f))

-- | Run a probe for its answer alone, discarding whatever it records.
--
-- A hole's inventory is built by trying candidate moves and seeing which fit,
-- and each trial checks terms of its own; their holes and warnings are not the
-- user's and must not reach the report. This is what the writer channel's
-- @censor@ did before the record moved into the state: the state survives an
-- error, so it is put back on that path too.
suppressing :: TypeCheck n a -> TypeCheck n a
suppressing :: forall (n :: S) a. TypeCheck n a -> TypeCheck n a
suppressing TypeCheck n a
action = do
  saved <- ExceptT
  TypeErrorInScopedContext (StateT CheckLog Identity) CheckLog
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     CheckLog
forall (m :: * -> *) a. Monad m => m a -> ReaderT (Context n) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (State CheckLog CheckLog
-> ExceptT
     TypeErrorInScopedContext (StateT CheckLog Identity) CheckLog
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT TypeErrorInScopedContext m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift State CheckLog CheckLog
forall (m :: * -> *) s. Monad m => StateT s m s
get)
  let restore = ExceptT TypeErrorInScopedContext (StateT CheckLog Identity) ()
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT (Context n) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (State CheckLog ()
-> ExceptT TypeErrorInScopedContext (StateT CheckLog Identity) ()
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT TypeErrorInScopedContext m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (CheckLog -> State CheckLog ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put CheckLog
saved))
  result <- action `catchError` \TypeErrorInScopedContext
err -> ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
  ()
restore ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
  ()
-> TypeCheck n a -> TypeCheck n a
forall a b.
ReaderT
  (Context n)
  (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
  a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     b
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TypeErrorInScopedContext -> TypeCheck n a
forall a.
TypeErrorInScopedContext
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TypeErrorInScopedContext
err
  restore
  return result

-- * Holes

recordHoleInfo :: HoleInfo -> TypeCheck n ()
recordHoleInfo :: forall (n :: S). HoleInfo -> TypeCheck n ()
recordHoleInfo HoleInfo
info =
  (CheckLog -> CheckLog) -> TypeCheck n ()
forall (n :: S). (CheckLog -> CheckLog) -> TypeCheck n ()
modifyLog ((CheckLog -> CheckLog) -> TypeCheck n ())
-> (CheckLog -> CheckLog) -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ \CheckLog
l -> CheckLog
l { logHolesRev = info : logHolesRev l }

-- * Warnings

recordCheckWarning :: CheckWarning -> TypeCheck n ()
recordCheckWarning :: forall (n :: S). CheckWarning -> TypeCheck n ()
recordCheckWarning CheckWarning
warning =
  (CheckLog -> CheckLog) -> TypeCheck n ()
forall (n :: S). (CheckLog -> CheckLog) -> TypeCheck n ()
modifyLog ((CheckLog -> CheckLog) -> TypeCheck n ())
-> (CheckLog -> CheckLog) -> TypeCheck n ()
forall a b. (a -> b) -> a -> b
$ \CheckLog
l -> CheckLog
l { logWarningsRev = warning : logWarningsRev l }

-- * Locations

withLocation :: LocationInfo -> TypeCheck n a -> TypeCheck n a
withLocation :: forall (n :: S) a. LocationInfo -> TypeCheck n a -> TypeCheck n a
withLocation LocationInfo
loc = (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a.
(Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((Context n -> Context n)
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
      a)
-> (Context n -> Context n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (StateT CheckLog Identity))
     a
forall a b. (a -> b) -> a -> b
$ \Context n
ctx -> Context n
ctx { ctxLocation = Just loc }