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

-- | Type errors, and how they are shown.
--
-- An error is captured /at its own scope/: it packages the context it was raised
-- in, existentially, so its scope index does not escape into the error type. The
-- old representation instead nested the error one @Inc@ deeper at every binder
-- (@ScopedTypeError@) and unwound the whole stack at printing time, inventing a
-- name per binder as it went. That unwinding loop, and both of its
-- @FIXME: very inefficient filter@ sites, are gone: the context already knows what
-- everything in scope is called (see "Rzk.TypeCheck.Display").
--
-- The error type is therefore /not/ scope-indexed, which is why entering a binder
-- no longer has to re-index the error channel.
module Rzk.TypeCheck.Error where

import           Control.Monad.Foil       (Distinct)
import qualified Control.Monad.Foil       as Foil
import           Data.List                (intercalate)

import           Language.Rzk.Foil.Syntax
import           Language.Rzk.Foil.Names (TModality (..), VarIdent, getVarIdent,
                                           ppVarIdentWithLocation)
import qualified Language.Rzk.Syntax      as Rzk
import           Rzk.TypeCheck.Context
import           Rzk.TypeCheck.Display

data TypeError n
  = TypeErrorOther String
  | TypeErrorUnify (TermT n) (TermT n) (TermT n)
  | TypeErrorUnifyTerms (TermT n) (TermT n)
  | TypeErrorNotPair (TermT n) (TermT n)
  | TypeErrorNotModal (Term n) TModality (TermT n)
  | TypeErrorModalityMismatch TModality TModality (Term n)
  | TypeErrorUnaccessibleVar (Foil.Name n) TModality TModality
  | TypeErrorNotTypeInModal (TermT n)
  | TypeErrorNotFunction (TermT n) (TermT n)
  | TypeErrorUnexpectedLambda (Term n) (TermT n)
  | TypeErrorUnexpectedPair (Term n) (TermT n)
  | TypeErrorUnexpectedRefl (Term n) (TermT n)
  | TypeErrorCannotInferBareLambda (Term n)
  | TypeErrorCannotInferBareRefl (Term n)
  | TypeErrorCannotInferHole (Term n)
  | TypeErrorUnsolvedHole (Maybe VarIdent) (TermT n)
  | TypeErrorUndefined VarIdent
  | TypeErrorTopeNotSatisfied [TermT n] (TermT n)
  | TypeErrorTopeContextDisjoint (TermT n) [TermT n]
  | TypeErrorTopesNotEquivalent (TermT n) (TermT n)
  | TypeErrorInvalidArgumentType (Term n) (TermT n)
  | TypeErrorDuplicateTopLevel [VarIdent] VarIdent
  | TypeErrorUnusedVariable (Foil.Name n) (TermT n)
  | TypeErrorUnusedUsedVariables [Foil.Name n] (Foil.Name n)
  | TypeErrorImplicitAssumption (Foil.Name n, TermT n) (Foil.Name n)
  | TypeErrorNotIntervalCube String (TermT n) (TermT n)
  | TypeErrorRepeatedBinder VarIdent [VarIdent]
  | TypeErrorMatchScrutineeNotData (TermT n) (TermT n)
  | TypeErrorMatchCannotInfer (Term n)
  | TypeErrorMatchMissingBranch VarIdent
  | TypeErrorMatchDuplicateBranch VarIdent
  | TypeErrorMatchUnknownBranch VarIdent [VarIdent]
  | TypeErrorMatchBranchArity VarIdent Int Int
  | TypeErrorReascribedTypeMismatch VarIdent (TermT n) (TermT n)

-- | An error, together with the context it was raised in.
--
-- The scope index is existential: an error raised under a binder is /already/
-- complete (its context says what its names are called), so it needs nothing
-- from the enclosing scope and can be thrown straight through it.
data TypeErrorInScopedContext where
  TypeErrorInScopedContext
    :: Distinct n => Context n -> TypeError n -> TypeErrorInScopedContext

ppModality :: TModality -> String
ppModality :: TModality -> [Char]
ppModality = \case
  TModality
Flat  -> [Char]
"♭"
  TModality
Sharp -> [Char]
"♯"
  TModality
Op    -> [Char]
"ᵒᵖ"
  TModality
Id    -> [Char]
"_id"

-- * Rendering

data OutputDirection = TopDown | BottomUp
  deriving (OutputDirection -> OutputDirection -> Bool
(OutputDirection -> OutputDirection -> Bool)
-> (OutputDirection -> OutputDirection -> Bool)
-> Eq OutputDirection
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: OutputDirection -> OutputDirection -> Bool
== :: OutputDirection -> OutputDirection -> Bool
$c/= :: OutputDirection -> OutputDirection -> Bool
/= :: OutputDirection -> OutputDirection -> Bool
Eq)

block :: OutputDirection -> [String] -> String
block :: OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown  = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n"
block OutputDirection
BottomUp = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char])
-> ([[Char]] -> [[Char]]) -> [[Char]] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Char]] -> [[Char]]
forall a. [a] -> [a]
reverse

namedBlock :: OutputDirection -> String -> [String] -> String
namedBlock :: OutputDirection -> [Char] -> [[Char]] -> [Char]
namedBlock OutputDirection
dir [Char]
name [[Char]]
lines_ = OutputDirection -> [[Char]] -> [Char]
block OutputDirection
dir ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
  [Char]
name [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: ([Char] -> [Char]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> [Char]
indent [[Char]]
lines_
  where
    indent :: [Char] -> [Char]
indent = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> ([Char] -> [[Char]]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> [Char]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([[Char]] -> [[Char]])
-> ([Char] -> [[Char]]) -> [Char] -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[Char]]
lines

ppTypeError :: Naming n -> TypeError n -> String
ppTypeError :: forall (n :: S). Naming n -> TypeError n -> [Char]
ppTypeError Naming n
naming = \case
  TypeErrorOther [Char]
msg -> [Char]
msg
  TypeErrorUnify TermT n
term TermT n
expected TermT n
actual -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"cannot unify expected type"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
expected)
    , [Char]
"with actual type"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
actual)
    , [Char]
"for term"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
term) ]
  TypeErrorUnifyTerms TermT n
expected TermT n
actual -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"cannot unify term"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
expected)
    , [Char]
"with term"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
actual) ]
  TypeErrorNotPair TermT n
term TermT n
ty -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"expected a cube product or dependent pair"
    , [Char]
"but got type"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
ty)
    , [Char]
"for term"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
term)
    , case TermT n
ty of
        TypeFunT{} -> [Char]
"\nPerhaps the term is applied to too few arguments?"
        TermT n
_          -> [Char]
""
    ]
  TypeErrorNotModal Term n
term TModality
m TermT n
ty -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"expected modal type " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> TModality -> [Char]
ppModality TModality
m [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" ?"
    , [Char]
"but got type"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
ty)
    , [Char]
"for term"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU Term n
term
    ]
  TypeErrorModalityMismatch TModality
expected TModality
actual Term n
term -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"modality mismatch"
    , [Char]
"  expected " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> TModality -> [Char]
ppModality TModality
expected
    , [Char]
"  but got  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> TModality -> [Char]
ppModality TModality
actual
    , [Char]
"for term"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU Term n
term
    ]
  TypeErrorUnaccessibleVar Name n
_var TModality
varMod TModality
locks -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"unaccessible var with modality " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> TModality -> [Char]
ppModality TModality
varMod
    , [Char]
"  under locks " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> TModality -> [Char]
ppModality TModality
locks
    ]
  TypeErrorNotTypeInModal TermT n
ty -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"expected a type inside modal type"
    , [Char]
"but got"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
ty)
    ]

  TypeErrorUnexpectedLambda Term n
term TermT n
ty -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"unexpected lambda abstraction"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU Term n
term
    , [Char]
"when typechecking against a non-function type"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> TermT n -> [Char]
ppTyped TermT n
ty
    ]
  TypeErrorUnexpectedPair Term n
term TermT n
ty -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"unexpected pair"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU Term n
term
    , [Char]
"when typechecking against a type that is not a product or a dependent sum"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> TermT n -> [Char]
ppTyped TermT n
ty
    ]
  TypeErrorUnexpectedRefl Term n
term TermT n
ty -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"unexpected refl"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU Term n
term
    , [Char]
"when typechecking against a type that is not an identity type"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> TermT n -> [Char]
ppTyped TermT n
ty
    ]

  TypeErrorNotFunction TermT n
term TermT n
ty -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"expected a function or extension type"
    , [Char]
"but got type"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
ty)
    , [Char]
"for term"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
term)
    , case TermT n
term of
        AppT TypeInfo (TermT n)
_ty TermT n
f TermT n
_x -> [Char]
"\nPerhaps the term\n  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
f) [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"\nis applied to too many arguments?"
        TermT n
_             -> [Char]
""
    ]
  TypeErrorCannotInferBareLambda Term n
term -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"cannot infer the type of the argument"
    , [Char]
"in lambda abstraction"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU Term n
term
    ]
  TypeErrorCannotInferBareRefl Term n
term -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"cannot infer the type of term"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU Term n
term
    ]
  TypeErrorCannotInferHole Term n
term -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"cannot infer the type of a hole"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU Term n
term
    , [Char]
"a hole is only allowed where its type is already known (checking position)"
    ]
  TypeErrorUnsolvedHole Maybe VarIdent
mname TermT n
goal -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"found an unsolved hole" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char] -> (VarIdent -> [Char]) -> Maybe VarIdent -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
"" (\VarIdent
name -> [Char]
" ?" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> VarIdent -> [Char]
forall a. Show a => a -> [Char]
show VarIdent
name) Maybe VarIdent
mname
    , [Char]
"expected type (goal):"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
goal)
    ]
  TypeErrorUndefined VarIdent
var -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"undefined variable: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> VarIdent -> [Char]
forall a. Show a => a -> [Char]
show VarIdent
var ]
  TypeErrorTopeNotSatisfied [TermT n]
topes TermT n
tope -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"local context is not included in (does not entail) the tope"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
tope)
    , [Char]
"in local context (normalised)"
    , [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ((TermT n -> [Char]) -> [TermT n] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (([Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<>) ([Char] -> [Char]) -> (TermT n -> [Char]) -> TermT n -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermT n -> [Char]
ppTyped) [TermT n]
topes)] -- FIXME: remove
  TypeErrorTopeContextDisjoint TermT n
tope [TermT n]
topes -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"the tope"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
tope)
    , [Char]
"is disjoint from the local tope context (their conjunction is the empty tope ⊥),"
    , [Char]
"so this restriction face or recOR branch is vacuous everywhere"
    , [Char]
"in local context (normalised)"
    , [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ((TermT n -> [Char]) -> [TermT n] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (([Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<>) ([Char] -> [Char]) -> (TermT n -> [Char]) -> TermT n -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermT n -> [Char]
ppTyped) [TermT n]
topes)]
  TypeErrorTopesNotEquivalent TermT n
expected TermT n
actual -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"expected tope"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
expected)
    , [Char]
"but got"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
actual) ]

  TypeErrorInvalidArgumentType Term n
argType TermT n
argKind -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"invalid function parameter type"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU Term n
argType
    , [Char]
"function parameter can be a cube, a shape, or a type"
    , [Char]
"but given parameter type has type"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
argKind)
    ]

  TypeErrorDuplicateTopLevel [VarIdent]
previous VarIdent
lastName -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"duplicate top-level definition"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> VarIdent -> [Char]
ppVarIdentWithLocation VarIdent
lastName
    , [Char]
"previous top-level definitions found at"
    , [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n"
      [ [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> VarIdent -> [Char]
ppVarIdentWithLocation VarIdent
name
      | VarIdent
name <- [VarIdent]
previous ]
    ]

  TypeErrorUnusedVariable Name n
name TermT n
type_ -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"unused variable"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Name n -> [Char]
ppVar Name n
name [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" : " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
type_)
    ]

  TypeErrorUnusedUsedVariables [Name n]
vars Name n
name -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"unused variables"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [[Char]] -> [Char]
unwords ((Name n -> [Char]) -> [Name n] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Name n -> [Char]
ppVar [Name n]
vars)
    , [Char]
"declared as used in definition of"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Name n -> [Char]
ppVar Name n
name
    ]

  TypeErrorImplicitAssumption (Name n
a, TermT n
aType) Name n
name -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"implicit assumption"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Name n -> [Char]
ppVar Name n
a [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" : " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
aType)
    , [Char]
"used in definition of"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Name n -> [Char]
ppVar Name n
name
    ]

  TypeErrorNotIntervalCube [Char]
op TermT n
lType TermT n
rType -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
op [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" expects both points in the same interval cube (2 or 𝕀)"
    , [Char]
"but got a point of type"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
lType)
    , [Char]
"and a point of type"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
rType)
    ]

  TypeErrorRepeatedBinder VarIdent
name [VarIdent]
previous -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ VarIdent -> [Char]
forall a. Show a => a -> [Char]
show VarIdent
name [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" is bound multiple times in one binder group"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> VarIdent -> [Char]
ppVarIdentWithLocation VarIdent
name
    , [Char]
"already bound at"
    , [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n"
      [ [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> VarIdent -> [Char]
ppVarIdentWithLocation VarIdent
prev | VarIdent
prev <- [VarIdent]
previous ]
    ]

  TypeErrorMatchScrutineeNotData TermT n
scrut TermT n
ty -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"match scrutinee"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
scrut)
    , [Char]
"is not of a #data type; its type is"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
ty)
    ]
  TypeErrorMatchCannotInfer Term n
term -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"cannot infer the type of match"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU Term n
term
    , [Char]
"a match without \"into\" is only allowed where its type is already known (checking position)"
    ]
  TypeErrorMatchMissingBranch VarIdent
con -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"match has no branch for constructor " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> VarIdent -> [Char]
forall a. Show a => a -> [Char]
show VarIdent
con ]
  TypeErrorMatchDuplicateBranch VarIdent
con -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"duplicate match branch for constructor " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> VarIdent -> [Char]
forall a. Show a => a -> [Char]
show VarIdent
con ]
  TypeErrorMatchUnknownBranch VarIdent
con [VarIdent]
cons -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"match branch for " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> VarIdent -> [Char]
forall a. Show a => a -> [Char]
show VarIdent
con [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
", which is not a constructor of the scrutinee's type"
    , case [VarIdent]
cons of
        [] -> [Char]
"the type has no constructors"
        [VarIdent]
_  -> [Char]
"the constructors are: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [[Char]] -> [Char]
unwords ((VarIdent -> [Char]) -> [VarIdent] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent -> [Char]
forall a. Show a => a -> [Char]
show [VarIdent]
cons)
    ]
  TypeErrorMatchBranchArity VarIdent
con Int
expected Int
actual -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"match branch for constructor " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> VarIdent -> [Char]
forall a. Show a => a -> [Char]
show VarIdent
con
    , [Char]
"binds " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
actual [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" argument" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> (if Int
actual Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then [Char]
"" else [Char]
"s")
        [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
", but its method takes " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
expected
    ]
  TypeErrorReascribedTypeMismatch VarIdent
entryName TermT n
canonical TermT n
given -> OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ [Char]
"the re-ascribed type of " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> VarIdent -> [Char]
forall a. Show a => a -> [Char]
show VarIdent
entryName
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
given)
    , [Char]
"is not definitionally equal to its canonical type"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
canonical)
    ]
  where
    ppU :: Term n -> [Char]
ppU = Naming n -> Term n -> [Char]
forall (n :: S). Naming n -> Term n -> [Char]
ppTerm Naming n
naming
    ppTyped :: TermT n -> [Char]
ppTyped = Naming n -> TermT n -> [Char]
forall (n :: S). Naming n -> TermT n -> [Char]
ppTermT Naming n
naming
    ppVar :: Name n -> [Char]
ppVar = Naming n -> Name n -> [Char]
forall (n :: S). Naming n -> Name n -> [Char]
ppName Naming n
naming

ppAction :: Naming n -> Int -> Action n -> String
ppAction :: forall (n :: S). Naming n -> Int -> Action n -> [Char]
ppAction Naming n
naming Int
n = [[Char]] -> [Char]
unlines ([[Char]] -> [Char])
-> (Action n -> [[Char]]) -> Action n -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> [Char]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) Char
' ' [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<>) ([[Char]] -> [[Char]])
-> (Action n -> [[Char]]) -> Action n -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
  ActionTypeCheck Term n
term TermT n
ty ->
    [ [Char]
"typechecking"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU Term n
term
    , [Char]
"against type"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
ty) ]

  ActionUnify TermT n
term TermT n
expected TermT n
actual ->
    [ [Char]
"unifying expected type"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
expected)
    , [Char]
"with actual type"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
actual)
    , [Char]
"for term"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
term) ]

  ActionUnifyTerms TermT n
expected TermT n
actual ->
    [ [Char]
"unifying term (expected)"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> TermT n -> [Char]
ppTyped TermT n
expected
    , [Char]
"with term (actual)"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> TermT n -> [Char]
ppTyped TermT n
actual ]

  ActionInfer Term n
term ->
    [ [Char]
"inferring type for term"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU Term n
term ]

  ActionContextEntailedBy [TermT n]
topes TermT n
term ->
    [ [Char]
"checking if local context"
    , [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ((TermT n -> [Char]) -> [TermT n] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (([Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<>) ([Char] -> [Char]) -> (TermT n -> [Char]) -> TermT n -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term n -> [Char]
ppU (Term n -> [Char]) -> (TermT n -> Term n) -> TermT n -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped) [TermT n]
topes)
    , [Char]
"includes (is entailed by) restriction tope"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
term) ]

  ActionContextEntails [TermT n]
topes TermT n
term ->
    [ [Char]
"checking if local context"
    , [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ((TermT n -> [Char]) -> [TermT n] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (([Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<>) ([Char] -> [Char]) -> (TermT n -> [Char]) -> TermT n -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term n -> [Char]
ppU (Term n -> [Char]) -> (TermT n -> Term n) -> TermT n -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped) [TermT n]
topes)
    , [Char]
"is included in (entails) the tope"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
term) ]

  ActionContextEntailsUnion [TermT n]
topes [TermT n]
terms ->
    [ [Char]
"checking if local context"
    , [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ((TermT n -> [Char]) -> [TermT n] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (([Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<>) ([Char] -> [Char]) -> (TermT n -> [Char]) -> TermT n -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term n -> [Char]
ppU (Term n -> [Char]) -> (TermT n -> Term n) -> TermT n -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped) [TermT n]
topes)
    , [Char]
"is included in (entails) the union of the topes"
    , [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ((TermT n -> [Char]) -> [TermT n] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (([Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<>) ([Char] -> [Char]) -> (TermT n -> [Char]) -> TermT n -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term n -> [Char]
ppU (Term n -> [Char]) -> (TermT n -> Term n) -> TermT n -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped) [TermT n]
terms) ]

  ActionWHNF TermT n
term ->
    [ [Char]
"computing WHNF for term"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> TermT n -> [Char]
ppTyped TermT n
term ]

  ActionNF TermT n
term ->
    [ [Char]
"computing normal form for term"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
term) ]

  ActionCheckCoherence (TermT n
ltope, TermT n
lterm) (TermT n
rtope, TermT n
rterm) ->
    [ [Char]
"checking coherence for"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
ltope)
    , [Char]
"  |-> " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
lterm)
    , [Char]
"and"
    , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
rtope)
    , [Char]
"  |-> " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
rterm) ]

  ActionCloseSection Maybe SectionName
Nothing ->
    [ [Char]
"closing the file"
    , [Char]
"and collecting assumptions (variables)" ]
  ActionCloseSection (Just SectionName
sectionName) ->
    [ [Char]
"closing #section " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> SectionName -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree SectionName
sectionName
    , [Char]
"and collecting assumptions (variables)"]

  ActionCheckLetValue Maybe VarIdent
orig ->
    [ [Char]
"checking the local definition "
        [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char] -> (VarIdent -> [Char]) -> Maybe VarIdent -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
"_" (VarIdent' RzkPosition -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree (VarIdent' RzkPosition -> [Char])
-> (VarIdent -> VarIdent' RzkPosition) -> VarIdent -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarIdent -> VarIdent' RzkPosition
getVarIdent) Maybe VarIdent
orig ]
  where
    ppU :: Term n -> [Char]
ppU = Naming n -> Term n -> [Char]
forall (n :: S). Naming n -> Term n -> [Char]
ppTerm Naming n
naming
    ppTyped :: TermT n -> [Char]
ppTyped = Naming n -> TermT n -> [Char]
forall (n :: S). Naming n -> TermT n -> [Char]
ppTermT Naming n
naming

-- | The context an error was raised in: where it happened, what was being
-- checked, the tope context, the stack of judgements, and the hypotheses.
ppContext :: OutputDirection -> Context n -> String
ppContext :: forall (n :: S). OutputDirection -> Context n -> [Char]
ppContext OutputDirection
dir ctx :: Context n
ctx@Context{Bool
Int
[[ModalTope n]]
[Name n]
[VarIdent]
[SectionInfo n]
[Action n]
[ModalTope n]
Maybe Bool
Maybe Command
Maybe LocationInfo
Maybe RenderBackend
Map VarIdent [VarIdent]
Map VarIdent (Name n)
NameMap n (VarInfo n)
Scope n
MetaPrefixSensitivity
CachedSaturation n
Verbosity
Covariance
ctxScope :: Scope n
ctxVars :: NameMap n (VarInfo n)
ctxNamed :: Map VarIdent (Name n)
ctxBound :: [Name n]
ctxSections :: [SectionInfo n]
ctxDiscreteTopes :: [ModalTope n]
ctxTopes :: [ModalTope n]
ctxTopesNF :: [ModalTope n]
ctxTopesNFUnion :: [[ModalTope n]]
ctxTopesEntailBottom :: Maybe Bool
ctxTopesSaturated :: CachedSaturation n
ctxShadow :: Map VarIdent [VarIdent]
ctxActionStack :: [Action n]
ctxActionStackDepth :: Int
ctxCurrentCommand :: Maybe Command
ctxLocation :: Maybe LocationInfo
ctxVerbosity :: Verbosity
ctxCovariance :: Covariance
ctxRenderBackend :: Maybe RenderBackend
ctxRenderHideTerm :: Bool
ctxHolesAreErrors :: Bool
ctxDeferHoleMismatches :: Bool
ctxHintLemmas :: [VarIdent]
ctxWarnOverhang :: Bool
ctxMetaPrefixSensitivity :: MetaPrefixSensitivity
ctxMetaPrefixSensitivity :: forall (n :: S). Context n -> MetaPrefixSensitivity
ctxWarnOverhang :: forall (n :: S). Context n -> Bool
ctxHintLemmas :: forall (n :: S). Context n -> [VarIdent]
ctxDeferHoleMismatches :: forall (n :: S). Context n -> Bool
ctxHolesAreErrors :: forall (n :: S). Context n -> Bool
ctxRenderHideTerm :: forall (n :: S). Context n -> Bool
ctxRenderBackend :: forall (n :: S). Context n -> Maybe RenderBackend
ctxCovariance :: forall (n :: S). Context n -> Covariance
ctxVerbosity :: forall (n :: S). Context n -> Verbosity
ctxLocation :: forall (n :: S). Context n -> Maybe LocationInfo
ctxCurrentCommand :: forall (n :: S). Context n -> Maybe Command
ctxActionStackDepth :: forall (n :: S). Context n -> Int
ctxActionStack :: forall (n :: S). Context n -> [Action n]
ctxShadow :: forall (n :: S). Context n -> Map VarIdent [VarIdent]
ctxTopesSaturated :: forall (n :: S). Context n -> CachedSaturation n
ctxTopesEntailBottom :: forall (n :: S). Context n -> Maybe Bool
ctxTopesNFUnion :: forall (n :: S). Context n -> [[ModalTope n]]
ctxTopesNF :: forall (n :: S). Context n -> [ModalTope n]
ctxTopes :: forall (n :: S). Context n -> [ModalTope n]
ctxDiscreteTopes :: forall (n :: S). Context n -> [ModalTope n]
ctxSections :: forall (n :: S). Context n -> [SectionInfo n]
ctxBound :: forall (n :: S). Context n -> [Name n]
ctxNamed :: forall (n :: S). Context n -> Map VarIdent (Name n)
ctxVars :: forall (n :: S). Context n -> NameMap n (VarInfo n)
ctxScope :: forall (n :: S). Context n -> Scope n
..} = OutputDirection -> [[Char]] -> [Char]
block OutputDirection
dir ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ ([Char] -> Bool) -> [[Char]] -> [[Char]]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null
  [ OutputDirection -> [[Char]] -> [Char]
block OutputDirection
TopDown
    [ case Maybe LocationInfo
ctxLocation of
        Maybe LocationInfo
_ | OutputDirection
dir OutputDirection -> OutputDirection -> Bool
forall a. Eq a => a -> a -> Bool
== OutputDirection
TopDown -> [Char]
"" -- FIXME
        Just (LocationInfo (Just [Char]
path) (Just Int
lineNo) (Just Int
col)) ->
          [Char]
path [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" (line " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
lineNo [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
", column " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
col [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"):"
        Just (LocationInfo (Just [Char]
path) (Just Int
lineNo) Maybe Int
Nothing) ->
          [Char]
path [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" (line " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
lineNo [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"):"
        Just (LocationInfo (Just [Char]
path) Maybe Int
_ Maybe Int
_) ->
          [Char]
path [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
":"
        Maybe LocationInfo
_  -> [Char]
""
    , case Maybe Command
ctxCurrentCommand of
        Just (Rzk.CommandDefine BNFC'Position
_loc VarIdent' BNFC'Position
name DeclUsedVars' BNFC'Position
_vars [Param' BNFC'Position]
_params Term' BNFC'Position
_ty Term' BNFC'Position
_term) ->
          [Char]
"  Error occurred when checking\n    #define " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> VarIdent' BNFC'Position -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree VarIdent' BNFC'Position
name
        Just (Rzk.CommandPostulate BNFC'Position
_loc VarIdent' BNFC'Position
name DeclUsedVars' BNFC'Position
_vars [Param' BNFC'Position]
_params Term' BNFC'Position
_ty ) ->
          [Char]
"  Error occurred when checking\n    #postulate " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> VarIdent' BNFC'Position -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree VarIdent' BNFC'Position
name
        Just (Rzk.CommandData BNFC'Position
_loc VarIdent' BNFC'Position
name DeclUsedVars' BNFC'Position
_vars [Param' BNFC'Position]
_params DataSort' BNFC'Position
_sort DataBody' BNFC'Position
_body) ->
          [Char]
"  Error occurred when checking\n    #data " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> VarIdent' BNFC'Position -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree VarIdent' BNFC'Position
name
        Just (Rzk.CommandCheck BNFC'Position
_loc Term' BNFC'Position
term Term' BNFC'Position
ty) ->
          [Char]
"  Error occurred when checking\n    " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term' BNFC'Position -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree Term' BNFC'Position
term [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" : " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term' BNFC'Position -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree Term' BNFC'Position
ty
        Just (Rzk.CommandCompute BNFC'Position
_loc Term' BNFC'Position
term) ->
          [Char]
"  Error occurred when computing\n    " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term' BNFC'Position -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree Term' BNFC'Position
term
        Just (Rzk.CommandComputeNF BNFC'Position
_loc Term' BNFC'Position
term) ->
          [Char]
"  Error occurred when computing NF for\n    " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term' BNFC'Position -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree Term' BNFC'Position
term
        Just (Rzk.CommandComputeWHNF BNFC'Position
_loc Term' BNFC'Position
term) ->
          [Char]
"  Error occurred when computing WHNF for\n    " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term' BNFC'Position -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree Term' BNFC'Position
term
        Just (Rzk.CommandSetOption BNFC'Position
_loc [Char]
optionName [Char]
_optionValue) ->
          [Char]
"  Error occurred when trying to set option\n    #set-option " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
optionName
        Just command :: Command
command@Rzk.CommandUnsetOption{} ->
          [Char]
"  Error occurred when trying to unset option\n    " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Command -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree Command
command
        Just command :: Command
command@Rzk.CommandAssume{} ->
          [Char]
"  Error occurred when checking assumption\n    " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Command -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree Command
command
        Just (Rzk.CommandSection BNFC'Position
_loc SectionName
name) ->
          [Char]
"  Error occurred when checking\n    #section " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> SectionName -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree SectionName
name
        Just (Rzk.CommandSectionEnd BNFC'Position
_loc SectionName
name) ->
          [Char]
"  Error occurred when checking\n    #end " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> SectionName -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree SectionName
name
        Maybe Command
Nothing -> [Char]
"  Error occurred outside of any command!"
    ]
  , [Char]
""
  , case (AST NameBinder (AnnSig TypeInfo TermSig) n -> Bool)
-> [AST NameBinder (AnnSig TypeInfo TermSig) n]
-> [AST NameBinder (AnnSig TypeInfo TermSig) n]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (AST NameBinder (AnnSig TypeInfo TermSig) n -> Bool)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AST NameBinder (AnnSig TypeInfo TermSig) n -> Bool
forall {binder :: S -> S -> *} {ann :: * -> *} {n :: S}.
AST binder (AnnSig ann TermSig) n -> Bool
isTopeTop) (Context n -> [AST NameBinder (AnnSig TypeInfo TermSig) n]
forall (n :: S). Context n -> [TermT n]
availableTopes Context n
ctx) of
      [] -> [Char]
"Local tope context is unrestricted (⊤)."
      [AST NameBinder (AnnSig TypeInfo TermSig) n]
topes -> OutputDirection -> [Char] -> [[Char]] -> [Char]
namedBlock OutputDirection
TopDown [Char]
"Local tope context:"
        [ [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (AST NameBinder (AnnSig TypeInfo TermSig) n -> Term n
forall (n :: S). TermT n -> Term n
untyped AST NameBinder (AnnSig TypeInfo TermSig) n
tope)
        | AST NameBinder (AnnSig TypeInfo TermSig) n
tope <- [AST NameBinder (AnnSig TypeInfo TermSig) n]
topes ]
  , [Char]
""
  , OutputDirection -> [[Char]] -> [Char]
block OutputDirection
dir
    [ [Char]
"when " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Naming n -> Int -> Action n -> [Char]
forall (n :: S). Naming n -> Int -> Action n -> [Char]
ppAction Naming n
naming Int
0 Action n
action
    | Action n
action <- [Action n]
ctxActionStack ]
  , OutputDirection -> [Char] -> [[Char]] -> [Char]
namedBlock OutputDirection
TopDown [Char]
"Definitions in context:"
    [ OutputDirection -> [[Char]] -> [Char]
block OutputDirection
dir
      [ Naming n -> Name n -> [Char]
forall (n :: S). Naming n -> Name n -> [Char]
ppName Naming n
naming Name n
name [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" : " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Term n -> [Char]
ppU (AST NameBinder (AnnSig TypeInfo TermSig) n -> Term n
forall (n :: S). TermT n -> Term n
untyped (VarInfo n -> AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). VarInfo n -> TermT n
varType VarInfo n
info))
      | (Name n
name, VarInfo n
info) <- [(Name n, VarInfo n)] -> [(Name n, VarInfo n)]
forall a. [a] -> [a]
reverse (Context n -> [(Name n, VarInfo n)]
forall (n :: S). Context n -> [(Name n, VarInfo n)]
varsInScope Context n
ctx) ] ]
  ]
  where
    naming :: Naming n
naming = Context n -> Naming n
forall (n :: S). Context n -> Naming n
namingOfContext Context n
ctx
    ppU :: Term n -> [Char]
ppU = Naming n -> Term n -> [Char]
forall (n :: S). Naming n -> Term n -> [Char]
ppTerm Naming n
naming
    isTopeTop :: AST binder (AnnSig ann TermSig) n -> Bool
isTopeTop TopeTopT{} = Bool
True
    isTopeTop AST binder (AnnSig ann TermSig) n
_          = Bool
False

-- | An error, with the context it was raised in.
ppTypeErrorInScopedContext :: OutputDirection -> TypeErrorInScopedContext -> String
ppTypeErrorInScopedContext :: OutputDirection -> TypeErrorInScopedContext -> [Char]
ppTypeErrorInScopedContext OutputDirection
dir (TypeErrorInScopedContext Context n
ctx TypeError n
err) = OutputDirection -> [[Char]] -> [Char]
block OutputDirection
dir
  [ Naming n -> TypeError n -> [Char]
forall (n :: S). Naming n -> TypeError n -> [Char]
ppTypeError (Context n -> Naming n
forall (n :: S). Context n -> Naming n
namingOfContext Context n
ctx) TypeError n
err
  , [Char]
""
  , OutputDirection -> Context n -> [Char]
forall (n :: S). OutputDirection -> Context n -> [Char]
ppContext OutputDirection
dir Context n
ctx
  ]