{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards   #-}

-- | Structured diagnostics for rzk: type errors and holes as data (severity,
-- a stable code, a source location, and a message) rather than a single
-- pre-formatted string. The core library produces these; the LSP maps them to
-- LSP diagnostics, and the CLI can emit them as JSON (@rzk typecheck --json@).
--
-- Locations are line-level: rzk currently retains only file + line at the point
-- an error is produced (the column is discarded, and core terms keep no
-- per-node position), so diagnostics point at the enclosing command's line.
module Rzk.Diagnostic where

import           Data.Aeson           (ToJSON (..), Value (String), object,
                                       (.=))

import           Rzk.TypeCheck

-- | Diagnostic severity, mirroring the usual LSP levels.
data Severity
  = SeverityError
  | SeverityWarning
  | SeverityInformation
  | SeverityHint
  deriving (Severity -> Severity -> Bool
(Severity -> Severity -> Bool)
-> (Severity -> Severity -> Bool) -> Eq Severity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Severity -> Severity -> Bool
== :: Severity -> Severity -> Bool
$c/= :: Severity -> Severity -> Bool
/= :: Severity -> Severity -> Bool
Eq, Int -> Severity -> ShowS
[Severity] -> ShowS
Severity -> String
(Int -> Severity -> ShowS)
-> (Severity -> String) -> ([Severity] -> ShowS) -> Show Severity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Severity -> ShowS
showsPrec :: Int -> Severity -> ShowS
$cshow :: Severity -> String
show :: Severity -> String
$cshowList :: [Severity] -> ShowS
showList :: [Severity] -> ShowS
Show)

-- | A structured diagnostic. Independent of any editor protocol: the LSP maps
-- it to its own @Diagnostic@, and the CLI serialises it as JSON.
--
-- == JSON wire format (@rzk typecheck --json@)
--
-- This is a stable format that downstream tools (e.g. richer LSP hovers) pin
-- to. Each diagnostic is an object:
--
-- > { "severity": "error" | "warning" | "information" | "hint"
-- > , "code":     <string>           -- "hole", or a TypeError tag (e.g. "TypeErrorUnify")
-- > , "location": { "file": <string|null>, "line": <int|null> } | null
-- > , "message":  <string>           -- human-facing prose (the CLI/LSP display text)
-- > , "hole":     <HoleData> | null  -- present only for hole diagnostics (see 'HoleData')
-- > }
--
-- The @message@ field is kept for back-compat (the LSP and the CLI human mode
-- use it). Structured consumers should read the @hole@ object instead of
-- parsing @message@. For non-hole diagnostics @hole@ is @null@.
data Diagnostic = Diagnostic
  { Diagnostic -> Severity
diagnosticSeverity :: Severity
  , Diagnostic -> String
diagnosticCode     :: String            -- ^ stable category, e.g. @\"TypeErrorUnify\"@ or @\"hole\"@
  , Diagnostic -> Maybe LocationInfo
diagnosticLocation :: Maybe LocationInfo -- ^ file + line (line-level granularity)
  , Diagnostic -> String
diagnosticMessage  :: String
  , Diagnostic -> Maybe HoleData
diagnosticHole     :: Maybe HoleData     -- ^ structured hole payload ('Nothing' for type errors)
  } deriving (Diagnostic -> Diagnostic -> Bool
(Diagnostic -> Diagnostic -> Bool)
-> (Diagnostic -> Diagnostic -> Bool) -> Eq Diagnostic
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Diagnostic -> Diagnostic -> Bool
== :: Diagnostic -> Diagnostic -> Bool
$c/= :: Diagnostic -> Diagnostic -> Bool
/= :: Diagnostic -> Diagnostic -> Bool
Eq, Int -> Diagnostic -> ShowS
[Diagnostic] -> ShowS
Diagnostic -> String
(Int -> Diagnostic -> ShowS)
-> (Diagnostic -> String)
-> ([Diagnostic] -> ShowS)
-> Show Diagnostic
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Diagnostic -> ShowS
showsPrec :: Int -> Diagnostic -> ShowS
$cshow :: Diagnostic -> String
show :: Diagnostic -> String
$cshowList :: [Diagnostic] -> ShowS
showList :: [Diagnostic] -> ShowS
Show)

-- | The structured payload of a hole diagnostic: the goal and local context as
-- already-rendered display strings (the same strings the LSP/CLI show, i.e.
-- @show@ = @printTree@ on the underlying terms). Consumers render hole panels
-- from these fields directly, without parsing the human-facing @message@.
--
-- == JSON wire format
--
-- > { "name":     <string|null>                 -- the ?name, if the hole was named
-- > , "goal":     <string>                       -- the expected type (the goal)
-- > , "shape":    { "binder": <string>, "tope": <string> } | null
-- > , "termVars": [ { "name": <string>, "type": <string> }, ... ]
-- > , "cubeVars": [ { "name": <string>, "type": <string> }, ... ]
-- > , "topes":    [ <string>, ... ]              -- local tope assumptions (excludes ⊤)
-- > }
--
-- Notes for consumers:
--
-- * @shape@ is non-null only for a shape-restricted /argument/ goal, where the
--   goal reads @(binder : goal | tope)@. For an /extension/ type the boundary is
--   already part of @goal@ (a restricted type @A [ … ↦ … ]@), and @shape@ is
--   @null@ — read the boundary out of @goal@.
-- * @cubeVars@ names can be patterns like @\"(t, s)\"@ (pair-pattern binders);
--   they are display strings, not single identifiers.
data HoleData = HoleData
  { HoleData -> Maybe String
holeDataName     :: Maybe String           -- ^ the @?name@, if named
  , HoleData -> String
holeDataGoal     :: String                 -- ^ the goal (expected type)
  , HoleData -> Maybe (String, String)
holeDataShape    :: Maybe (String, String) -- ^ (binder, tope) for a shape-argument goal
  , HoleData -> [(String, String)]
holeDataTermVars :: [(String, String)]     -- ^ local hypotheses: (name, type)
  , HoleData -> [(String, String)]
holeDataCubeVars :: [(String, String)]     -- ^ local cube variables: (name, type)
  , HoleData -> [String]
holeDataTopes    :: [String]               -- ^ local tope assumptions (excluding ⊤)
  } deriving (HoleData -> HoleData -> Bool
(HoleData -> HoleData -> Bool)
-> (HoleData -> HoleData -> Bool) -> Eq HoleData
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HoleData -> HoleData -> Bool
== :: HoleData -> HoleData -> Bool
$c/= :: HoleData -> HoleData -> Bool
/= :: HoleData -> HoleData -> Bool
Eq, Int -> HoleData -> ShowS
[HoleData] -> ShowS
HoleData -> String
(Int -> HoleData -> ShowS)
-> (HoleData -> String) -> ([HoleData] -> ShowS) -> Show HoleData
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HoleData -> ShowS
showsPrec :: Int -> HoleData -> ShowS
$cshow :: HoleData -> String
show :: HoleData -> String
$cshowList :: [HoleData] -> ShowS
showList :: [HoleData] -> ShowS
Show)

instance ToJSON Severity where
  toJSON :: Severity -> Value
toJSON = Text -> Value
String (Text -> Value) -> (Severity -> Text) -> Severity -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
    Severity
SeverityError       -> Text
"error"
    Severity
SeverityWarning     -> Text
"warning"
    Severity
SeverityInformation -> Text
"information"
    Severity
SeverityHint        -> Text
"hint"

-- | Encode a location as JSON. A plain helper rather than a @ToJSON@ instance,
-- to avoid an orphan instance ('LocationInfo' is defined in "Rzk.TypeCheck").
locationToJSON :: LocationInfo -> Value
locationToJSON :: LocationInfo -> Value
locationToJSON (LocationInfo Maybe String
path Maybe Int
line Maybe Int
column) = [Pair] -> Value
object
  [ Key
"file" Key -> Maybe String -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Maybe String
path
  , Key
"line" Key -> Maybe Int -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Maybe Int
line
  , Key
"column" Key -> Maybe Int -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Maybe Int
column
  ]

instance ToJSON Diagnostic where
  toJSON :: Diagnostic -> Value
toJSON Diagnostic{String
Maybe LocationInfo
Maybe HoleData
Severity
diagnosticSeverity :: Diagnostic -> Severity
diagnosticCode :: Diagnostic -> String
diagnosticLocation :: Diagnostic -> Maybe LocationInfo
diagnosticMessage :: Diagnostic -> String
diagnosticHole :: Diagnostic -> Maybe HoleData
diagnosticSeverity :: Severity
diagnosticCode :: String
diagnosticLocation :: Maybe LocationInfo
diagnosticMessage :: String
diagnosticHole :: Maybe HoleData
..} = [Pair] -> Value
object
    [ Key
"severity" Key -> Severity -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Severity
diagnosticSeverity
    , Key
"code"     Key -> String -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= String
diagnosticCode
    , Key
"location" Key -> Maybe Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (LocationInfo -> Value) -> Maybe LocationInfo -> Maybe Value
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LocationInfo -> Value
locationToJSON Maybe LocationInfo
diagnosticLocation
    , Key
"message"  Key -> String -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= String
diagnosticMessage
    , Key
"hole"     Key -> Maybe HoleData -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Maybe HoleData
diagnosticHole
    ]

instance ToJSON HoleData where
  toJSON :: HoleData -> Value
toJSON HoleData{String
[String]
[(String, String)]
Maybe String
Maybe (String, String)
holeDataName :: HoleData -> Maybe String
holeDataGoal :: HoleData -> String
holeDataShape :: HoleData -> Maybe (String, String)
holeDataTermVars :: HoleData -> [(String, String)]
holeDataCubeVars :: HoleData -> [(String, String)]
holeDataTopes :: HoleData -> [String]
holeDataName :: Maybe String
holeDataGoal :: String
holeDataShape :: Maybe (String, String)
holeDataTermVars :: [(String, String)]
holeDataCubeVars :: [(String, String)]
holeDataTopes :: [String]
..} = [Pair] -> Value
object
    [ Key
"name"     Key -> Maybe String -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Maybe String
holeDataName
    , Key
"goal"     Key -> String -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= String
holeDataGoal
    , Key
"shape"    Key -> Maybe Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= ((String, String) -> Value)
-> Maybe (String, String) -> Maybe Value
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String, String) -> Value
forall {v} {v}. (ToJSON v, ToJSON v) => (v, v) -> Value
shapeToJSON Maybe (String, String)
holeDataShape
    , Key
"termVars" Key -> [Value] -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= ((String, String) -> Value) -> [(String, String)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (String, String) -> Value
forall {v} {v}. (ToJSON v, ToJSON v) => (v, v) -> Value
entryToJSON [(String, String)]
holeDataTermVars
    , Key
"cubeVars" Key -> [Value] -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= ((String, String) -> Value) -> [(String, String)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (String, String) -> Value
forall {v} {v}. (ToJSON v, ToJSON v) => (v, v) -> Value
entryToJSON [(String, String)]
holeDataCubeVars
    , Key
"topes"    Key -> [String] -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [String]
holeDataTopes
    ]
    where
      shapeToJSON :: (v, v) -> Value
shapeToJSON (v
binder, v
tope) = [Pair] -> Value
object [ Key
"binder" Key -> v -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= v
binder, Key
"tope" Key -> v -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= v
tope ]
      entryToJSON :: (v, v) -> Value
entryToJSON (v
name, v
ty)     = [Pair] -> Value
object [ Key
"name" Key -> v -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= v
name, Key
"type" Key -> v -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= v
ty ]

-- | A stable tag for a type error, used as its diagnostic code. Independent of
-- the variable type, so it survives the scoped-error unfolding.
typeErrorTag :: TypeError n -> String
typeErrorTag :: forall (n :: S). TypeError n -> String
typeErrorTag = \case
  TypeErrorOther{}                 -> String
"TypeErrorOther"
  TypeErrorUnify{}                 -> String
"TypeErrorUnify"
  TypeErrorUnifyTerms{}            -> String
"TypeErrorUnifyTerms"
  TypeErrorNotPair{}               -> String
"TypeErrorNotPair"
  TypeErrorNotModal{}              -> String
"TypeErrorNotModal"
  TypeErrorModalityMismatch{}      -> String
"TypeErrorModalityMismatch"
  TypeErrorUnaccessibleVar{}       -> String
"TypeErrorUnaccessibleVar"
  TypeErrorNotTypeInModal{}        -> String
"TypeErrorNotTypeInModal"
  TypeErrorNotFunction{}           -> String
"TypeErrorNotFunction"
  TypeErrorUnexpectedLambda{}      -> String
"TypeErrorUnexpectedLambda"
  TypeErrorUnexpectedPair{}        -> String
"TypeErrorUnexpectedPair"
  TypeErrorUnexpectedRefl{}        -> String
"TypeErrorUnexpectedRefl"
  TypeErrorCannotInferBareLambda{} -> String
"TypeErrorCannotInferBareLambda"
  TypeErrorCannotInferBareRefl{}   -> String
"TypeErrorCannotInferBareRefl"
  TypeErrorCannotInferHole{}       -> String
"TypeErrorCannotInferHole"
  TypeErrorUnsolvedHole{}          -> String
"TypeErrorUnsolvedHole"
  TypeErrorUndefined{}             -> String
"TypeErrorUndefined"
  TypeErrorTopeNotSatisfied{}      -> String
"TypeErrorTopeNotSatisfied"
  TypeErrorTopeContextDisjoint{}   -> String
"TypeErrorTopeContextDisjoint"
  TypeErrorTopesNotEquivalent{}    -> String
"TypeErrorTopesNotEquivalent"
  TypeErrorInvalidArgumentType{}   -> String
"TypeErrorInvalidArgumentType"
  TypeErrorDuplicateTopLevel{}     -> String
"TypeErrorDuplicateTopLevel"
  TypeErrorUnusedVariable{}        -> String
"TypeErrorUnusedVariable"
  TypeErrorUnusedUsedVariables{}   -> String
"TypeErrorUnusedUsedVariables"
  TypeErrorImplicitAssumption{}    -> String
"TypeErrorImplicitAssumption"
  TypeErrorNotIntervalCube{}       -> String
"TypeErrorNotIntervalCube"
  TypeErrorRepeatedBinder{}        -> String
"TypeErrorRepeatedBinder"
  TypeErrorMatchScrutineeNotData{} -> String
"TypeErrorMatchScrutineeNotData"
  TypeErrorMatchCannotInfer{}      -> String
"TypeErrorMatchCannotInfer"
  TypeErrorMatchMissingBranch{}    -> String
"TypeErrorMatchMissingBranch"
  TypeErrorMatchDuplicateBranch{}  -> String
"TypeErrorMatchDuplicateBranch"
  TypeErrorMatchUnknownBranch{}    -> String
"TypeErrorMatchUnknownBranch"
  TypeErrorMatchBranchArity{}      -> String
"TypeErrorMatchBranchArity"
  TypeErrorReascribedTypeMismatch{} -> String
"TypeErrorReascribedTypeMismatch"

-- | The tag of a type error.
--
-- An error carries the context it was raised in, so there are no binder layers to
-- peel: the old representation nested the error one Inc deeper at every binder.
typeErrorTagInScopedContext :: TypeErrorInScopedContext -> String
typeErrorTagInScopedContext :: TypeErrorInScopedContext -> String
typeErrorTagInScopedContext (TypeErrorInScopedContext Context n
_ctx TypeError n
err) = TypeError n -> String
forall (n :: S). TypeError n -> String
typeErrorTag TypeError n
err

-- | The source location of a type error (the enclosing command's line).
locationOfTypeError :: TypeErrorInScopedContext -> Maybe LocationInfo
locationOfTypeError :: TypeErrorInScopedContext -> Maybe LocationInfo
locationOfTypeError (TypeErrorInScopedContext Context n
ctx TypeError n
_err) = Context n -> Maybe LocationInfo
forall (n :: S). Context n -> Maybe LocationInfo
ctxLocation Context n
ctx

-- | A structured diagnostic for a type error. The message is the usual
-- formatted error text; severity is always 'SeverityError'.
diagnoseTypeError :: OutputDirection -> TypeErrorInScopedContext -> Diagnostic
diagnoseTypeError :: OutputDirection -> TypeErrorInScopedContext -> Diagnostic
diagnoseTypeError OutputDirection
dir TypeErrorInScopedContext
err = Diagnostic
  { diagnosticSeverity :: Severity
diagnosticSeverity = Severity
SeverityError
  , diagnosticCode :: String
diagnosticCode     = TypeErrorInScopedContext -> String
typeErrorTagInScopedContext TypeErrorInScopedContext
err
  , diagnosticLocation :: Maybe LocationInfo
diagnosticLocation = TypeErrorInScopedContext -> Maybe LocationInfo
locationOfTypeError TypeErrorInScopedContext
err
  , diagnosticMessage :: String
diagnosticMessage  = OutputDirection -> TypeErrorInScopedContext -> String
ppTypeErrorInScopedContext OutputDirection
dir TypeErrorInScopedContext
err
  , diagnosticHole :: Maybe HoleData
diagnosticHole     = Maybe HoleData
forall a. Maybe a
Nothing
  }

-- | A checker warning as a diagnostic: warning severity, with the warning's
-- constructor name as the stable code (like 'diagnoseTypeError' does for
-- errors).
diagnoseCheckWarning :: CheckWarning -> Diagnostic
diagnoseCheckWarning :: CheckWarning -> Diagnostic
diagnoseCheckWarning (LargeInductiveTypeWarning VarIdent
dataName VarIdent
conName Maybe LocationInfo
loc) = Diagnostic
  { diagnosticSeverity :: Severity
diagnosticSeverity = Severity
SeverityWarning
  , diagnosticCode :: String
diagnosticCode     = String
"LargeInductiveTypeWarning"
  , diagnosticLocation :: Maybe LocationInfo
diagnosticLocation = Maybe LocationInfo
loc
  , diagnosticMessage :: String
diagnosticMessage  =
      String
"large inductive type: a field of constructor " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> VarIdent -> String
forall a. Show a => a -> String
show VarIdent
conName
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" stores a universe; predicatively " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> VarIdent -> String
forall a. Show a => a -> String
show VarIdent
dataName
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" lives above U"
  , diagnosticHole :: Maybe HoleData
diagnosticHole     = Maybe HoleData
forall a. Maybe a
Nothing
  }
diagnoseCheckWarning (MetaPrefixWarning VarIdent
defName VarIdent
usedName Int
supplied Int
required MetaPrefixRule
rule Maybe LocationInfo
loc) = Diagnostic
  { diagnosticSeverity :: Severity
diagnosticSeverity = Severity
SeverityWarning
  , diagnosticCode :: String
diagnosticCode     = case MetaPrefixRule
rule of
      MetaPrefixRule
MetaPrefixBoth       -> String
"MetaPrefixWarning"
      MetaPrefixRule
MetaPrefixStrictOnly -> String
"MetaPrefixWarningStrictOnly"
  , diagnosticLocation :: Maybe LocationInfo
diagnosticLocation = Maybe LocationInfo
loc
  , diagnosticMessage :: String
diagnosticMessage  =
      String
"meta-parameter layer: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> VarIdent -> String
forall a. Show a => a -> String
show VarIdent
usedName String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" is used with "
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
supplied String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" of its " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
required
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" meta-prefix arguments"
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> (case MetaPrefixRule
rule of
              MetaPrefixRule
MetaPrefixBoth       -> String
" at an object-level position"
              MetaPrefixRule
MetaPrefixStrictOnly -> String
" outside another declaration's meta prefix")
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" (in " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> VarIdent -> String
forall a. Show a => a -> String
show VarIdent
defName String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  , diagnosticHole :: Maybe HoleData
diagnosticHole     = Maybe HoleData
forall a. Maybe a
Nothing
  }

-- | A checker warning as a human-readable line (the CLI).
ppCheckWarning :: CheckWarning -> String
ppCheckWarning :: CheckWarning -> String
ppCheckWarning = (String
"Warning: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<>) ShowS -> (CheckWarning -> String) -> CheckWarning -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Diagnostic -> String
diagnosticMessage (Diagnostic -> String)
-> (CheckWarning -> Diagnostic) -> CheckWarning -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckWarning -> Diagnostic
diagnoseCheckWarning

-- | The stable tag of a warning (its diagnostic code), used to match
-- @warnings@ in fixtures; sharing the definition keeps the two from
-- drifting apart.
checkWarningTag :: CheckWarning -> String
checkWarningTag :: CheckWarning -> String
checkWarningTag = Diagnostic -> String
diagnosticCode (Diagnostic -> String)
-> (CheckWarning -> Diagnostic) -> CheckWarning -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckWarning -> Diagnostic
diagnoseCheckWarning

-- | A structured diagnostic for a hole, carrying the hole's goal and local
-- context. A hole is an unfilled obligation, so it is a 'SeverityWarning' —
-- mirroring Agda's yellow \"unsolved\" highlight, and visible in the editor's
-- problems panel (unlike 'SeverityHint', which editors render almost
-- invisibly). Finished work still rejects holes outright: the strict default
-- of @rzk typecheck@ reports them as errors (cf. Agda's @--safe@).
diagnoseHole :: HoleInfo -> Diagnostic
diagnoseHole :: HoleInfo -> Diagnostic
diagnoseHole HoleInfo
hole = Diagnostic
  { diagnosticSeverity :: Severity
diagnosticSeverity = Severity
SeverityWarning
  , diagnosticCode :: String
diagnosticCode     = String
"hole"
  , diagnosticLocation :: Maybe LocationInfo
diagnosticLocation = HoleInfo -> Maybe LocationInfo
holeLocation HoleInfo
hole
  , diagnosticMessage :: String
diagnosticMessage  = HoleInfo -> String
ppHoleInfo HoleInfo
hole
  , diagnosticHole :: Maybe HoleData
diagnosticHole     = HoleData -> Maybe HoleData
forall a. a -> Maybe a
Just (HoleInfo -> HoleData
holeData HoleInfo
hole)
  }

-- | The structured payload of a hole: its goal and local context rendered to
-- display strings (the same rendering 'ppHoleInfo' uses, but kept as separate
-- fields rather than concatenated into prose). See 'HoleData'.
holeData :: HoleInfo -> HoleData
holeData :: HoleInfo -> HoleData
holeData HoleInfo{[Rendered]
[HoleEntry]
Maybe String
Maybe (VarIdent, Rendered)
Maybe VarIdent
Maybe LocationInfo
Rendered
holeLocation :: HoleInfo -> Maybe LocationInfo
holeName :: Maybe VarIdent
holeGoal :: Rendered
holeGoalShape :: Maybe (VarIdent, Rendered)
holeTermVars :: [HoleEntry]
holeCubeVars :: [HoleEntry]
holeTopes :: [Rendered]
holeCandidates :: [Rendered]
holeIntroductions :: [Rendered]
holeDiagram :: Maybe String
holeLocation :: Maybe LocationInfo
holeDiagram :: HoleInfo -> Maybe String
holeIntroductions :: HoleInfo -> [Rendered]
holeCandidates :: HoleInfo -> [Rendered]
holeTopes :: HoleInfo -> [Rendered]
holeCubeVars :: HoleInfo -> [HoleEntry]
holeTermVars :: HoleInfo -> [HoleEntry]
holeGoalShape :: HoleInfo -> Maybe (VarIdent, Rendered)
holeGoal :: HoleInfo -> Rendered
holeName :: HoleInfo -> Maybe VarIdent
..} = HoleData
  { holeDataName :: Maybe String
holeDataName     = (VarIdent -> String) -> Maybe VarIdent -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VarIdent -> String
forall a. Show a => a -> String
show Maybe VarIdent
holeName
  , holeDataGoal :: String
holeDataGoal     = Rendered -> String
forall a. Show a => a -> String
show Rendered
holeGoal
  , holeDataShape :: Maybe (String, String)
holeDataShape    = ((VarIdent, Rendered) -> (String, String))
-> Maybe (VarIdent, Rendered) -> Maybe (String, String)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(VarIdent
s, Rendered
tope) -> (VarIdent -> String
forall a. Show a => a -> String
show VarIdent
s, Rendered -> String
forall a. Show a => a -> String
show Rendered
tope)) Maybe (VarIdent, Rendered)
holeGoalShape
  , holeDataTermVars :: [(String, String)]
holeDataTermVars = (HoleEntry -> (String, String))
-> [HoleEntry] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
map HoleEntry -> (String, String)
entry [HoleEntry]
holeTermVars
  , holeDataCubeVars :: [(String, String)]
holeDataCubeVars = (HoleEntry -> (String, String))
-> [HoleEntry] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
map HoleEntry -> (String, String)
entry [HoleEntry]
holeCubeVars
  , holeDataTopes :: [String]
holeDataTopes    = (Rendered -> String) -> [Rendered] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Rendered -> String
forall a. Show a => a -> String
show [Rendered]
holeTopes
  }
  where
    entry :: HoleEntry -> (String, String)
entry HoleEntry
e = (VarIdent -> String
forall a. Show a => a -> String
show (HoleEntry -> VarIdent
holeEntryName HoleEntry
e), Rendered -> String
forall a. Show a => a -> String
show (HoleEntry -> Rendered
holeEntryType HoleEntry
e))

-- | Render a hole's goal and local context (the structured query) for display,
-- separating term variables, cube variables, and tope assumptions.
ppHoleInfo :: HoleInfo -> String
ppHoleInfo :: HoleInfo -> String
ppHoleInfo HoleInfo{[Rendered]
[HoleEntry]
Maybe String
Maybe (VarIdent, Rendered)
Maybe VarIdent
Maybe LocationInfo
Rendered
holeLocation :: HoleInfo -> Maybe LocationInfo
holeDiagram :: HoleInfo -> Maybe String
holeIntroductions :: HoleInfo -> [Rendered]
holeCandidates :: HoleInfo -> [Rendered]
holeTopes :: HoleInfo -> [Rendered]
holeCubeVars :: HoleInfo -> [HoleEntry]
holeTermVars :: HoleInfo -> [HoleEntry]
holeGoalShape :: HoleInfo -> Maybe (VarIdent, Rendered)
holeGoal :: HoleInfo -> Rendered
holeName :: HoleInfo -> Maybe VarIdent
holeName :: Maybe VarIdent
holeGoal :: Rendered
holeGoalShape :: Maybe (VarIdent, Rendered)
holeTermVars :: [HoleEntry]
holeCubeVars :: [HoleEntry]
holeTopes :: [Rendered]
holeCandidates :: [Rendered]
holeIntroductions :: [Rendered]
holeDiagram :: Maybe String
holeLocation :: Maybe LocationInfo
..} = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
  [ String
"Hole" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String -> (VarIdent -> String) -> Maybe VarIdent -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (\VarIdent
name -> String
" ?" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> VarIdent -> String
forall a. Show a => a -> String
show VarIdent
name) Maybe VarIdent
holeName
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String -> (LocationInfo -> String) -> Maybe LocationInfo -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (\LocationInfo
loc -> String
" at " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> LocationInfo -> String
ppLocationInfo LocationInfo
loc) Maybe LocationInfo
holeLocation
  , String
"  goal:"
  , String
"    " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
goalStr
  ]
  [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> String -> [HoleEntry] -> [String]
section String
"context" [HoleEntry]
holeTermVars
  [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> String -> [HoleEntry] -> [String]
section String
"cube variables" [HoleEntry]
holeCubeVars
  [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> (if [Rendered] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Rendered]
holeTopes
        then []
        else String
"  tope context:" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [ String
"    " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Rendered -> String
forall a. Show a => a -> String
show Rendered
t | Rendered
t <- [Rendered]
holeTopes ])
  where
    -- a shape goal reads (binder : cube | tope); otherwise just the type
    goalStr :: String
goalStr = case Maybe (VarIdent, Rendered)
holeGoalShape of
      Maybe (VarIdent, Rendered)
Nothing        -> Rendered -> String
forall a. Show a => a -> String
show Rendered
holeGoal
      Just (VarIdent
s, Rendered
tope) -> String
"(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> VarIdent -> String
forall a. Show a => a -> String
show VarIdent
s String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" : " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Rendered -> String
forall a. Show a => a -> String
show Rendered
holeGoal String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" | " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Rendered -> String
forall a. Show a => a -> String
show Rendered
tope String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
    section :: String -> [HoleEntry] -> [String]
section String
title [HoleEntry]
entries
      | [HoleEntry] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [HoleEntry]
entries = []
      | Bool
otherwise = (String
"  " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
title String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
":")
          String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [ String
"    " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> VarIdent -> String
forall a. Show a => a -> String
show (HoleEntry -> VarIdent
holeEntryName HoleEntry
e) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" : " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Rendered -> String
forall a. Show a => a -> String
show (HoleEntry -> Rendered
holeEntryType HoleEntry
e)
            | HoleEntry
e <- [HoleEntry]
entries ]

ppLocationInfo :: LocationInfo -> String
ppLocationInfo :: LocationInfo -> String
ppLocationInfo (LocationInfo Maybe String
mpath Maybe Int
mline Maybe Int
mcol) =
  String -> ShowS -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"<input>" ShowS
forall a. a -> a
id Maybe String
mpath
    String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String -> (Int -> String) -> Maybe Int -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" ((String
":" String -> ShowS
forall a. Semigroup a => a -> a -> a
<>) ShowS -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show) Maybe Int
mline
    String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String -> (Int -> String) -> Maybe Int -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" ((String
":" String -> ShowS
forall a. Semigroup a => a -> a -> a
<>) ShowS -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show) Maybe Int
mcol