{-|
Module      : Idris.Delaborate
Description : Convert core TT back into high level syntax, primarily for display purposes.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE CPP, PatternGuards #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module Idris.Delaborate (
    annName, bugaddr, delab, delabWithEnv, delabDirect, delab', delabMV, delabSugared
  , delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab
  , pprintDelabTy', pprintDelabTy, pprintErr, resugar
  ) where

import Idris.AbsSyntax
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Docstrings (overview, renderDocTerm, renderDocstring)
import Idris.ErrReverse

import Util.Pretty

#if (MIN_VERSION_base(4,11,0))
import Prelude hiding ((<$>), (<>))
#else
import Prelude hiding ((<$>))
#endif

import Control.Applicative (Alternative((<|>)))
import Control.Monad.State
import Data.Generics.Uniplate.Data (transform)
import Data.List (nub)
import Data.Maybe (mapMaybe)
import qualified Data.Text as T

bugaddr :: String
bugaddr = String
"https://github.com/idris-lang/Idris-dev/issues"

-- | Re-add syntactic sugar in a term
resugar :: IState -> PTerm -> PTerm
resugar :: IState -> PTerm -> PTerm
resugar IState
ist = (PTerm -> PTerm) -> PTerm -> PTerm
forall on. Uniplate on => (on -> on) -> on -> on
transform PTerm -> PTerm
flattenDoLet (PTerm -> PTerm) -> (PTerm -> PTerm) -> PTerm -> PTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PTerm -> PTerm) -> PTerm -> PTerm
forall on. Uniplate on => (on -> on) -> on -> on
transform PTerm -> PTerm
resugarApp
  where
    resugarApp :: PTerm -> PTerm
resugarApp (PApp FC
fc (PRef FC
_ [FC]
_ Name
n) [PArg]
args)
      | [PTerm
c, PTerm
t, PTerm
f] <- (PArg -> Maybe PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PArg -> Maybe PTerm
forall {a}. PArg' a -> Maybe a
explicitTerm [PArg]
args
      , Name -> Name
basename Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"ifThenElse"
      = FC -> PTerm -> PTerm -> PTerm -> PTerm
PIfThenElse FC
fc PTerm
c (PTerm -> PTerm
dedelay PTerm
t) (PTerm -> PTerm
dedelay PTerm
f)
    resugarApp (PApp FC
fc (PRef FC
_ [FC]
_ Name
n) [PArg]
args)
      | [PTerm
v, PLam FC
_ Name
bn FC
_ PTerm
_ PTerm
next] <- (PArg -> Maybe PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PArg -> Maybe PTerm
forall {a}. PArg' a -> Maybe a
explicitTerm [PArg]
args
      , Name -> Name
basename Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
">>="
      = let step :: PDo' PTerm
step = if Name
bn Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Name, PTerm)] -> IState -> PTerm -> [Name]
namesIn [] IState
ist PTerm
next
                      then FC -> Name -> FC -> PTerm -> PDo' PTerm
forall t. FC -> Name -> FC -> t -> PDo' t
DoBind FC
fc Name
bn FC
NoFC PTerm
v
                      else FC -> PTerm -> PDo' PTerm
forall t. FC -> t -> PDo' t
DoExp FC
NoFC PTerm
v
        in case PTerm -> PTerm
resugarApp PTerm
next of
             PDoBlock [PDo' PTerm]
dos -> [PDo' PTerm] -> PTerm
PDoBlock (PDo' PTerm
step PDo' PTerm -> [PDo' PTerm] -> [PDo' PTerm]
forall a. a -> [a] -> [a]
: [PDo' PTerm]
dos)
             PTerm
expr -> [PDo' PTerm] -> PTerm
PDoBlock [PDo' PTerm
step, FC -> PTerm -> PDo' PTerm
forall t. FC -> t -> PDo' t
DoExp FC
NoFC PTerm
expr]
    resugarApp (PApp FC
fc (PRef FC
_ [FC]
_ Name
n) [PArg]
args)
      | [PConstant FC
fc (BI Integer
i)] <- (PArg -> Maybe PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PArg -> Maybe PTerm
forall {a}. PArg' a -> Maybe a
explicitTerm [PArg]
args
      , Name -> Name
basename Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"fromInteger"
      = FC -> Const -> PTerm
PConstant FC
fc (Integer -> Const
BI Integer
i)
    resugarApp PTerm
tm = PTerm
tm

    flattenDoLet :: PTerm -> PTerm
flattenDoLet (PLet FC
_ RigCount
rc Name
ln FC
_ PTerm
ty PTerm
v PTerm
bdy)
      | PDoBlock [PDo' PTerm]
dos <- PTerm -> PTerm
flattenDoLet PTerm
bdy
      = [PDo' PTerm] -> PTerm
PDoBlock (FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PDo' PTerm
forall t. FC -> RigCount -> Name -> FC -> t -> t -> PDo' t
DoLet FC
NoFC RigCount
rc Name
ln FC
NoFC PTerm
ty PTerm
v PDo' PTerm -> [PDo' PTerm] -> [PDo' PTerm]
forall a. a -> [a] -> [a]
: [PDo' PTerm]
dos)
    flattenDoLet (PDoBlock [PDo' PTerm]
dos) =
      [PDo' PTerm] -> PTerm
PDoBlock ([PDo' PTerm] -> PTerm) -> [PDo' PTerm] -> PTerm
forall a b. (a -> b) -> a -> b
$ (PDo' PTerm -> [PDo' PTerm]) -> [PDo' PTerm] -> [PDo' PTerm]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDo' PTerm -> [PDo' PTerm]
fixExp [PDo' PTerm]
dos
        where fixExp :: PDo' PTerm -> [PDo' PTerm]
fixExp (DoExp FC
_ (PLet FC
_ RigCount
rc Name
ln FC
_ PTerm
ty PTerm
v PTerm
bdy)) =
                FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PDo' PTerm
forall t. FC -> RigCount -> Name -> FC -> t -> t -> PDo' t
DoLet FC
NoFC RigCount
rc Name
ln FC
NoFC PTerm
ty PTerm
v PDo' PTerm -> [PDo' PTerm] -> [PDo' PTerm]
forall a. a -> [a] -> [a]
: PDo' PTerm -> [PDo' PTerm]
fixExp (FC -> PTerm -> PDo' PTerm
forall t. FC -> t -> PDo' t
DoExp FC
NoFC PTerm
bdy)
              fixExp PDo' PTerm
d = [PDo' PTerm
d]
    flattenDoLet PTerm
tm = PTerm
tm

    dedelay :: PTerm -> PTerm
dedelay (PApp FC
_ (PRef FC
_ [FC]
_ Name
delay) [PArg
_, PArg
_, PArg
obj])
      | Name
delay Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"Delay" = PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
obj
    dedelay PTerm
x = PTerm
x

    explicitTerm :: PArg' a -> Maybe a
explicitTerm (PExp {getTm :: forall t. PArg' t -> t
getTm = a
tm}) = a -> Maybe a
forall a. a -> Maybe a
Just a
tm
    explicitTerm PArg' a
_ = Maybe a
forall a. Maybe a
Nothing


-- | Delaborate and resugar a term
delabSugared :: IState -> Term -> PTerm
delabSugared :: IState -> Term -> PTerm
delabSugared IState
ist Term
tm = IState -> PTerm -> PTerm
resugar IState
ist (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ IState -> Term -> PTerm
delab IState
ist Term
tm

-- | Delaborate a term without resugaring
delab :: IState -> Term -> PTerm
delab :: IState -> Term -> PTerm
delab IState
i Term
tm = IState -> Term -> Bool -> Bool -> PTerm
delab' IState
i Term
tm Bool
False Bool
False

delabWithEnv :: IState -> [(Name, Type)] -> Term -> PTerm
delabWithEnv :: IState -> [(Name, Term)] -> Term -> PTerm
delabWithEnv IState
i [(Name, Term)]
tys Term
tm = IState -> [(Name, Term)] -> Term -> Bool -> Bool -> PTerm
delabWithEnv' IState
i [(Name, Term)]
tys Term
tm Bool
False Bool
False

delabMV :: IState -> Term -> PTerm
delabMV :: IState -> Term -> PTerm
delabMV IState
i Term
tm = IState -> Term -> Bool -> Bool -> PTerm
delab' IState
i Term
tm Bool
False Bool
True

-- | Delaborate a term directly, leaving case applications as they are.
-- We need this for interactive case splitting, where we need access to the
-- underlying function in a delaborated form, to generate the right patterns
delabDirect :: IState -> Term -> PTerm
delabDirect :: IState -> Term -> PTerm
delabDirect IState
i Term
tm = IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [] [] Term
tm Bool
False Bool
False Bool
False

delabTy :: IState -> Name -> PTerm
delabTy :: IState -> Name -> PTerm
delabTy IState
i Name
n
    = case Name -> Context -> [Term]
lookupTy Name
n (IState -> Context
tt_ctxt IState
i) of
           (Term
ty:[Term]
_) -> case Name -> Ctxt [PArg] -> [[PArg]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
                         ([PArg]
imps:[[PArg]]
_) -> IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [PArg]
imps [] Term
ty Bool
False Bool
False Bool
True
                         [[PArg]]
_ -> IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [] [] Term
ty Bool
False Bool
False Bool
True
           [] -> String -> PTerm
forall a. HasCallStack => String -> a
error String
"delabTy: got non-existing name"

delab' :: IState -> Term -> Bool -> Bool -> PTerm
delab' :: IState -> Term -> Bool -> Bool -> PTerm
delab' IState
i Term
t Bool
f Bool
mvs = IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [] [] Term
t Bool
f Bool
mvs Bool
True

delabWithEnv' :: IState -> [(Name, Type)] -> Term -> Bool -> Bool -> PTerm
delabWithEnv' :: IState -> [(Name, Term)] -> Term -> Bool -> Bool -> PTerm
delabWithEnv' IState
i [(Name, Term)]
tys Term
t Bool
f Bool
mvs = IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [] [(Name, Term)]
tys Term
t Bool
f Bool
mvs Bool
True

delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any
          -> [(Name, Type)] -- ^ Names and types in environment
                            -- (for properly hiding scoped implicits)
          -> Term
          -> Bool -- ^ use full names
          -> Bool -- ^ Don't treat metavariables specially
          -> Bool -- ^ resugar cases
          -> PTerm
delabTy' :: IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
ist [PArg]
imps [(Name, Term)]
genv Term
tm Bool
fullname Bool
mvs Bool
docases = [(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
genv [] [PArg]
imps Term
tm
  where
    un :: FC
un = String -> FC
fileFC String
"(val)"

    -- Special case for spotting applications of case functions
    -- (Normally the scrutinee is let-bound, but hole types get normalised,
    -- so they could appear in this form. The scrutinee is always added as
    -- the last argument,
    -- although that's not always the thing that gets pattern matched
    -- in the elaborated block)
    de :: [(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
imps Term
sc
          | Bool
docases
          , Term -> Bool
isCaseApp Term
sc
          , (P NameType
_ Name
cOp Term
_, args :: [Term]
args@(Term
_:[Term]
_)) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
sc
          , Just PTerm
caseblock <- [(Name, Term)]
-> [(Name, Name)]
-> [PArg]
-> Term
-> Name
-> [Term]
-> Maybe PTerm
delabCase [(Name, Term)]
tys [(Name, Name)]
env [PArg]
imps ([Term] -> Term
forall a. HasCallStack => [a] -> a
last [Term]
args) Name
cOp [Term]
args
                 = PTerm
caseblock

    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (App AppStatus Name
_ Term
f Term
a) = [(Name, Term)] -> [(Name, Name)] -> Term -> [Term] -> PTerm
deFn [(Name, Term)]
tys [(Name, Name)]
env Term
f [Term
a]
    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (V Int
i) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [(Name, Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Name)]
env = FC -> [FC] -> Name -> PTerm
PRef FC
un [] ((Name, Name) -> Name
forall a b. (a, b) -> b
snd ([(Name, Name)]
env[(Name, Name)] -> Int -> (Name, Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
i))
                       | Bool
otherwise = FC -> [FC] -> Name -> PTerm
PRef FC
un [] (String -> Name
sUN (String
"v" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
""))
    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (P NameType
_ Name
n Term
_) | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
unitTy = FC -> PunInfo -> PTerm
PTrue FC
un PunInfo
IsType
                           | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
unitCon = FC -> PunInfo -> PTerm
PTrue FC
un PunInfo
IsTerm
                           | Just Name
n' <- Name -> [(Name, Name)] -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Name)]
env = FC -> [FC] -> Name -> PTerm
PRef FC
un [] Name
n'
                           | Bool
otherwise
                                = case Name
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> Maybe (Maybe Name, Int, [Name], Bool, Bool)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist) of
                                      Just (Just Name
_, Int
mi, [Name]
_, Bool
_, Bool
_) -> Name -> [PTerm] -> PTerm
mkMVApp Name
n []
                                      Maybe (Maybe Name, Int, [Name], Bool, Bool)
_ -> FC -> [FC] -> Name -> PTerm
PRef FC
un [] Name
n
    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (Bind Name
n (Lam RigCount
_ Term
ty) Term
sc)
          = FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
un Name
n FC
NoFC ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [] Term
sc)
    de [(Name, Term)]
tys [(Name, Name)]
env (PArg
_ : [PArg]
is) (Bind Name
n (Pi RigCount
rig (Just ImplicitInfo
impl) Term
ty Term
_) Term
sc)
       | ImplicitInfo -> Bool
toplevel_imp ImplicitInfo
impl -- information in 'imps' repeated
          = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ([ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [] Static
Dynamic Bool
False (ImplicitInfo -> Maybe ImplicitInfo
forall a. a -> Maybe a
Just ImplicitInfo
impl) Bool
False RigCount
rig) Name
n FC
NoFC
                ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [PArg]
is Term
sc)
    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
is (Bind Name
n (Pi RigCount
rig (Just ImplicitInfo
impl) Term
ty Term
_) Term
sc)
       | ImplicitInfo -> Bool
tcimplementation ImplicitInfo
impl
          = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
constraint Name
n FC
NoFC ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty)
                ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [PArg]
is Term
sc)
       | Bool
otherwise
          = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ([ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [] Static
Dynamic Bool
False (ImplicitInfo -> Maybe ImplicitInfo
forall a. a -> Maybe a
Just ImplicitInfo
impl) Bool
False RigCount
rig) Name
n FC
NoFC ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [PArg]
is Term
sc)
    de [(Name, Term)]
tys [(Name, Name)]
env ((PImp { argopts :: forall t. PArg' t -> [ArgOpt]
argopts = [ArgOpt]
opts }):[PArg]
is) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc)
          = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ([ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [ArgOpt]
opts Static
Dynamic Bool
False Maybe ImplicitInfo
forall a. Maybe a
Nothing Bool
False RigCount
rig) Name
n FC
NoFC
                ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [PArg]
is Term
sc)
    de [(Name, Term)]
tys [(Name, Name)]
env (PConstraint Int
_ [ArgOpt]
_ Name
_ PTerm
_:[PArg]
is) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc)
          = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
constraint { pcount = rig}) Name
n FC
NoFC
                ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [PArg]
is Term
sc)
    de [(Name, Term)]
tys [(Name, Name)]
env (PTacImplicit Int
_ [ArgOpt]
_ Name
_ PTerm
tac PTerm
_:[PArg]
is) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc)
          = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ((PTerm -> Plicity
tacimpl PTerm
tac) { pcount = rig }) Name
n FC
NoFC
                ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [PArg]
is Term
sc)
    de [(Name, Term)]
tys [(Name, Name)]
env (PArg
plic:[PArg]
is) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc)
          = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity
Exp (PArg -> [ArgOpt]
forall t. PArg' t -> [ArgOpt]
argopts PArg
plic) Static
Dynamic Bool
False RigCount
rig)
                Name
n FC
NoFC
                ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty)
                ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [PArg]
is Term
sc)
    de [(Name, Term)]
tys [(Name, Name)]
env [] (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc)
          = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
expl { pcount = rig }) Name
n FC
NoFC ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty)
                ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [] Term
sc)

    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
imps (Bind Name
n (Let RigCount
rc Term
ty Term
val) Term
sc)
          | Bool
docases
          , Term -> Bool
isCaseApp Term
sc
          , (P NameType
_ Name
cOp Term
_, [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
sc
          , Just PTerm
caseblock    <- [(Name, Term)]
-> [(Name, Name)]
-> [PArg]
-> Term
-> Name
-> [Term]
-> Maybe PTerm
delabCase [(Name, Term)]
tys [(Name, Name)]
env [PArg]
imps Term
val Name
cOp [Term]
args = PTerm
caseblock
          | Bool
otherwise    =
              FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
un RigCount
rc Name
n FC
NoFC ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty)
                   ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
val) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [] Term
sc)
    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (Bind Name
n (Hole Term
ty) Term
sc) = [(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n, String -> Name
sUN String
"[__]")(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [] Term
sc
    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (Bind Name
n (Guess Term
ty Term
val) Term
sc) = [(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n, String -> Name
sUN String
"[__]")(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [] Term
sc
    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
plic (Bind Name
n Binder Term
bb Term
sc) = [(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
bb) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [] Term
sc
    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (Constant Const
i) = FC -> Const -> PTerm
PConstant FC
NoFC Const
i
    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (Proj Term
_ Int
_) = String -> PTerm
forall a. HasCallStack => String -> a
error String
"Delaboration got run-time-only Proj!"
    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ Term
Erased = PTerm
Placeholder
    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ Term
Impossible = PTerm
Placeholder
    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (Inferred Term
t) = PTerm
Placeholder
    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (TType UExp
i) = FC -> PTerm
PType FC
un
    de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (UType Universe
u) = FC -> Universe -> PTerm
PUniverse FC
un Universe
u

    deFn :: [(Name, Term)] -> [(Name, Name)] -> Term -> [Term] -> PTerm
deFn [(Name, Term)]
tys [(Name, Name)]
env (App AppStatus Name
_ Term
f Term
a) [Term]
args = [(Name, Term)] -> [(Name, Name)] -> Term -> [Term] -> PTerm
deFn [(Name, Term)]
tys [(Name, Name)]
env Term
f (Term
aTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
args)
    deFn [(Name, Term)]
tys [(Name, Name)]
env (P NameType
_ Name
n Term
_) [Term
l,Term
r]
         | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
pairTy    = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
un [] PunInfo
IsType ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
l) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
r)
    deFn [(Name, Term)]
tys [(Name, Name)]
env (P NameType
_ Name
n Term
_) [Term
ty, Bind Name
x (Lam RigCount
_ Term
_) Term
r]
         | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
sigmaTy
               = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
un [] PunInfo
IsType (FC -> [FC] -> Name -> PTerm
PRef FC
un [] Name
x) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty)
                           ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys ((Name
x,Name
x)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [] (Term -> Term -> Term
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
ty) Term
r))
    deFn [(Name, Term)]
tys [(Name, Name)]
env (P NameType
_ Name
n Term
_) [Term
lt,Term
rt,Term
l,Term
r]
         | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
pairCon = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
un [] PunInfo
IsTerm ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
l) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
r)
         | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
sigmaCon = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
un [] PunInfo
IsTerm ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
l) PTerm
Placeholder
                                                ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
r)
--     deFn tys env f@(P _ n _) args
--          | n `elem` map snd env
--               = PApp un (de tys env [] f) (map pexp (map (de tys env []) args))
    deFn [(Name, Term)]
tys [(Name, Name)]
env (P NameType
_ Name
n Term
_) [Term]
args
         | Bool -> Bool
not Bool
mvs = case Name
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> Maybe (Maybe Name, Int, [Name], Bool, Bool)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist) of
                        Just (Just Name
_, Int
mi, [Name]
_, Bool
_, Bool
_) ->
                            Name -> [PTerm] -> PTerm
mkMVApp Name
n (Int -> [PTerm] -> [PTerm]
forall a. Int -> [a] -> [a]
drop Int
mi ((Term -> PTerm) -> [Term] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env []) [Term]
args))
                        Maybe (Maybe Name, Int, [Name], Bool, Bool)
_ -> [(Name, Term)] -> Name -> [PTerm] -> PTerm
mkPApp [(Name, Term)]
tys Name
n ((Term -> PTerm) -> [Term] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env []) [Term]
args)
         | Bool
otherwise = [(Name, Term)] -> Name -> [PTerm] -> PTerm
mkPApp [(Name, Term)]
tys Name
n ((Term -> PTerm) -> [Term] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env []) [Term]
args)
    deFn [(Name, Term)]
tys [(Name, Name)]
env (V Int
i) [Term]
args
         | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [(Name, Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Name)]
env = [(Name, Term)] -> Name -> [PTerm] -> PTerm
mkPApp [(Name, Term)]
tys ((Name, Name) -> Name
forall a b. (a, b) -> a
fst ([(Name, Name)]
env[(Name, Name)] -> Int -> (Name, Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
i)) ((Term -> PTerm) -> [Term] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env []) [Term]
args)
    deFn [(Name, Term)]
tys [(Name, Name)]
env Term
f [Term]
args = FC -> PTerm -> [PArg] -> PTerm
PApp FC
un ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
f) ((PTerm -> PArg) -> [PTerm] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PArg
forall {t}. t -> PArg' t
pexp ((Term -> PTerm) -> [Term] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env []) [Term]
args))

    mkMVApp :: Name -> [PTerm] -> PTerm
mkMVApp Name
n []
            = FC -> Name -> PTerm
PMetavar FC
NoFC Name
n
    mkMVApp Name
n [PTerm]
args
            = FC -> PTerm -> [PArg] -> PTerm
PApp FC
un (FC -> Name -> PTerm
PMetavar FC
NoFC Name
n) ((PTerm -> PArg) -> [PTerm] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PArg
forall {t}. t -> PArg' t
pexp [PTerm]
args)

    mkPApp :: [(Name, Term)] -> Name -> [PTerm] -> PTerm
mkPApp [(Name, Term)]
tys Name
n [PTerm]
args
        | Just Term
ty <- Name -> [(Name, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Term)]
tys
            = let imps :: [PArg]
imps = Term -> [PArg]
findImp Term
ty in
                  FC -> PTerm -> [PArg] -> PTerm
PApp FC
un (FC -> [FC] -> Name -> PTerm
PRef FC
un [] Name
n) ((PArg -> PTerm -> PArg) -> [PArg] -> [PTerm] -> [PArg]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith PArg -> PTerm -> PArg
forall {t}. PArg' t -> t -> PArg' t
imp ([PArg]
imps [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++ PArg -> [PArg]
forall a. a -> [a]
repeat (PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
forall a. HasCallStack => a
undefined)) [PTerm]
args)
        | Just [PArg]
imps <- Name -> Ctxt [PArg] -> Maybe [PArg]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [PArg]
idris_implicits IState
ist)
            = FC -> PTerm -> [PArg] -> PTerm
PApp FC
un (FC -> [FC] -> Name -> PTerm
PRef FC
un [] Name
n) ((PArg -> PTerm -> PArg) -> [PArg] -> [PTerm] -> [PArg]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith PArg -> PTerm -> PArg
forall {t}. PArg' t -> t -> PArg' t
imp ([PArg]
imps [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++ PArg -> [PArg]
forall a. a -> [a]
repeat (PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
forall a. HasCallStack => a
undefined)) [PTerm]
args)
        | Bool
otherwise = FC -> PTerm -> [PArg] -> PTerm
PApp FC
un (FC -> [FC] -> Name -> PTerm
PRef FC
un [] Name
n) ((PTerm -> PArg) -> [PTerm] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PArg
forall {t}. t -> PArg' t
pexp [PTerm]
args)
      where
        findImp :: Term -> [PArg]
findImp (Bind Name
n (Pi RigCount
_ im :: Maybe ImplicitInfo
im@(Just ImplicitInfo
i) Term
_ Term
_) Term
sc)
             = Name -> PTerm -> Bool -> PArg
forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n PTerm
Placeholder Bool
True PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: Term -> [PArg]
findImp Term
sc
        findImp (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Term
_ Term
_) Term
sc)
             = PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
Placeholder PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: Term -> [PArg]
findImp Term
sc
        findImp Term
_ = []
    imp :: PArg' t -> t -> PArg' t
imp (PImp Int
p Bool
m [ArgOpt]
l Name
n t
_) t
arg = Int -> Bool -> [ArgOpt] -> Name -> t -> PArg' t
forall t. Int -> Bool -> [ArgOpt] -> Name -> t -> PArg' t
PImp Int
p Bool
m [ArgOpt]
l Name
n t
arg
    imp (PExp Int
p [ArgOpt]
l Name
n t
_)   t
arg = Int -> [ArgOpt] -> Name -> t -> PArg' t
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp Int
p [ArgOpt]
l Name
n t
arg
    imp (PConstraint Int
p [ArgOpt]
l Name
n t
_) t
arg = Int -> [ArgOpt] -> Name -> t -> PArg' t
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PConstraint Int
p [ArgOpt]
l Name
n t
arg
    imp (PTacImplicit Int
p [ArgOpt]
l Name
n t
sc t
_) t
arg = Int -> [ArgOpt] -> Name -> t -> t -> PArg' t
forall t. Int -> [ArgOpt] -> Name -> t -> t -> PArg' t
PTacImplicit Int
p [ArgOpt]
l Name
n t
sc t
arg

    isCaseApp :: Term -> Bool
isCaseApp Term
tm | P NameType
_ Name
n Term
_ <- (Term, [Term]) -> Term
forall a b. (a, b) -> a
fst (Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm) = Name -> Bool
isCN Name
n
                 | Bool
otherwise = Bool
False
      where isCN :: Name -> Bool
isCN (NS Name
n [Text]
_) = Name -> Bool
isCN Name
n
            isCN (SN (CaseN FC'
_ Name
_)) = Bool
True
            isCN Name
_ = Bool
False

    delabCase :: [(Name, Type)] -> [(Name, Name)] -> [PArg] -> Term -> Name -> [Term] -> Maybe PTerm
    delabCase :: [(Name, Term)]
-> [(Name, Name)]
-> [PArg]
-> Term
-> Name
-> [Term]
-> Maybe PTerm
delabCase [(Name, Term)]
tys [(Name, Name)]
env [PArg]
imps Term
scrutinee Name
caseName [Term]
caseArgs =
      do [([(Name, Term)], Term, Term)]
cases <- case Name
-> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
-> [([([(Name, Term)], Term, Term)], [PTerm])]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
caseName (IState -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs IState
ist) of
                    [([([(Name, Term)], Term, Term)]
cases, [PTerm]
_)] -> [([(Name, Term)], Term, Term)]
-> Maybe [([(Name, Term)], Term, Term)]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [([(Name, Term)], Term, Term)]
cases
                    [([([(Name, Term)], Term, Term)], [PTerm])]
_ -> Maybe [([(Name, Term)], Term, Term)]
forall a. Maybe a
Nothing
         PTerm -> Maybe PTerm
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> Maybe PTerm) -> PTerm -> Maybe PTerm
forall a b. (a -> b) -> a -> b
$ FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
un ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
imps Term
scrutinee)
                    [ ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys ([(Name, Name)]
env [(Name, Name)] -> [(Name, Name)] -> [(Name, Name)]
forall a. [a] -> [a] -> [a]
++ ((Name, Term) -> (Name, Name)) -> [(Name, Term)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, Term
_) -> (Name
n, Name
n)) [(Name, Term)]
vars) [PArg]
imps (Term -> Term
forall {n}. TT n -> TT n
splitArg Term
lhs),
                       [(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys ([(Name, Name)]
env [(Name, Name)] -> [(Name, Name)] -> [(Name, Name)]
forall a. [a] -> [a] -> [a]
++ ((Name, Term) -> (Name, Name)) -> [(Name, Term)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, Term
_) -> (Name
n, Name
n)) [(Name, Term)]
vars) [PArg]
imps Term
rhs)
                    | ([(Name, Term)]
vars, Term
lhs, Term
rhs) <- [([(Name, Term)], Term, Term)]
cases
                    ]
      where splitArg :: TT n -> TT n
splitArg TT n
tm | (TT n
_, [TT n]
args) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
tm = [TT n] -> TT n
forall {n}. [TT n] -> TT n
nonVar ([TT n] -> [TT n]
forall a. [a] -> [a]
reverse [TT n]
args)
                        | Bool
otherwise = TT n
tm
            nonVar :: [TT n] -> TT n
nonVar [] = String -> TT n
forall a. HasCallStack => String -> a
error String
"Tried to delaborate empty case list"
            nonVar [TT n
x] = TT n
x
            nonVar (x :: TT n
x@(App AppStatus n
_ TT n
_ TT n
_) : [TT n]
_) = TT n
x
            nonVar (x :: TT n
x@(P (DCon Int
_ Int
_ Bool
_) n
_ TT n
_) : [TT n]
_) = TT n
x
            nonVar (TT n
x:[TT n]
xs) = [TT n] -> TT n
nonVar [TT n]
xs
-- | How far to indent sub-errors
errorIndent :: Int
errorIndent :: Int
errorIndent = Int
8

-- | Actually indent a sub-error - no line at end because a newline can end
-- multiple layers of indent
indented :: Doc a -> Doc a
indented :: forall a. Doc a -> Doc a
indented = Int -> Doc a -> Doc a
forall a. Int -> Doc a -> Doc a
nest Int
errorIndent (Doc a -> Doc a) -> (Doc a -> Doc a) -> Doc a -> Doc a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc a
forall a. Doc a
line Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<>)

-- | Pretty-print a core term using delaboration
pprintDelab :: IState -> Term -> Doc OutputAnnotation
pprintDelab :: IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist Term
tm = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm [] Term
tm)
                              (IState -> PTerm -> Doc OutputAnnotation
prettyIst IState
ist (IState -> Term -> PTerm
delabSugared IState
ist Term
tm))

pprintNoDelab :: IState -> Term -> Doc OutputAnnotation
pprintNoDelab :: IState -> Term -> Doc OutputAnnotation
pprintNoDelab IState
ist Term
tm = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm [] Term
tm)
                              (IState -> PTerm -> Doc OutputAnnotation
prettyIst IState
ist (IState -> Term -> PTerm
delab IState
ist Term
tm))

pprintDelabTy' :: IState -> Name -> Term -> Doc OutputAnnotation
pprintDelabTy' :: IState -> Name -> Term -> Doc OutputAnnotation
pprintDelabTy' IState
i Name
n Term
ty
    = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm [] Term
ty) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (PTerm -> Doc OutputAnnotation) -> PTerm -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IState -> PTerm -> Doc OutputAnnotation
prettyIst IState
i (PTerm -> Doc OutputAnnotation) -> PTerm -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$
      case Name -> Ctxt [PArg] -> [[PArg]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
           ([PArg]
imps:[[PArg]]
_) -> IState -> PTerm -> PTerm
resugar IState
i (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [PArg]
imps [] Term
ty Bool
False Bool
False Bool
True
           [[PArg]]
_ -> IState -> PTerm -> PTerm
resugar IState
i (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [] [] Term
ty Bool
False Bool
False Bool
True

-- | Pretty-print the type of some name
pprintDelabTy :: IState -> Name -> Doc OutputAnnotation
pprintDelabTy :: IState -> Name -> Doc OutputAnnotation
pprintDelabTy IState
i Name
n
    = case Name -> Context -> [Term]
lookupTy Name
n (IState -> Context
tt_ctxt IState
i) of
           (Term
ty:[Term]
_) -> IState -> Name -> Term -> Doc OutputAnnotation
pprintDelabTy' IState
i Name
n Term
ty
           [] -> String -> Doc OutputAnnotation
forall a. HasCallStack => String -> a
error String
"pprintDelabTy got a name that doesn't exist"

pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
ist = IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
ist []

pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
ist [(Name, Bool)]
bnd PTerm
tm = PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm (IState -> PPOption
ppOptionIst IState
ist) [(Name, Bool)]
bnd [] (IState -> [FixDecl]
idris_infixes IState
ist) PTerm
tm

pprintProv :: IState -> [(Name, Term)] -> Provenance -> Doc OutputAnnotation
pprintProv :: IState -> [(Name, Term)] -> Provenance -> Doc OutputAnnotation
pprintProv IState
i [(Name, Term)]
e Provenance
ExpectedType = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Expected type"
pprintProv IState
i [(Name, Term)]
e Provenance
InferredVal = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Inferred value"
pprintProv IState
i [(Name, Term)]
e Provenance
GivenVal = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Given value"
pprintProv IState
i [(Name, Term)]
e (SourceTerm Term
tm)
  = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Type of " Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
    OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm ([Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
e) (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)) Term
tm)
             (IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i ([Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
e) (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)) (IState -> Term -> PTerm
delabSugared IState
i Term
tm))
pprintProv IState
i [(Name, Term)]
e (TooManyArgs Term
tm)
  = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Is " Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
      OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm ([Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
e) (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)) Term
tm)
               (IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i ([Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
e) (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)) (IState -> Term -> PTerm
delabSugared IState
i Term
tm))
       Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
" applied to too many arguments?"

pprintErr :: IState -> Err -> Doc OutputAnnotation
pprintErr :: IState -> Err -> Doc OutputAnnotation
pprintErr IState
i Err
err = IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i ((Term -> Term) -> Err -> Err
forall a b. (a -> b) -> Err' a -> Err' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Term -> Term
errReverse IState
i) Err
err)

pprintErr' :: IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i (Msg String
s) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
s
pprintErr' IState
i (InternalMsg String
s) =
  [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep [ String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"INTERNAL ERROR:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
s,
         String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"This is probably a bug, or a missing error message.",
         String -> Doc OutputAnnotation
forall a. String -> Doc a
text (String
"Please consider reporting at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bugaddr)
       ]
pprintErr' IState
i (CantUnify Bool
_ (Term
x_in, Maybe Provenance
xprov) (Term
y_in, Maybe Provenance
yprov) Err
e [(Name, Term)]
sc Int
s) =
  let (Term
x_ns, Term
y_ns, [Name]
nms) = Term -> Term -> (Term, Term, [Name])
renameMNs Term
x_in Term
y_in
      (PTerm
x, PTerm
y) = PTerm -> PTerm -> (PTerm, PTerm)
addImplicitDiffs (IState -> Term -> PTerm
delabSugared IState
i Term
x_ns) (IState -> Term -> PTerm
delabSugared IState
i Term
y_ns) in
    String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Type mismatch between" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
x_ns
                      (IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i (((Name, Term) -> (Name, Bool)) -> [(Name, Term)] -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
b) -> (Name
n, Bool
False)) [(Name, Term)]
sc
                                        [(Name, Bool)] -> [(Name, Bool)] -> [(Name, Bool)]
forall a. [a] -> [a] -> [a]
++ [Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
nms (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)) PTerm
x))
        Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> case Maybe Provenance
xprov of
                Maybe Provenance
Nothing -> Doc OutputAnnotation
forall a. Doc a
empty
                Just Provenance
t -> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
" (" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> [(Name, Term)] -> Provenance -> Doc OutputAnnotation
pprintProv IState
i [(Name, Term)]
sc Provenance
t Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
")"
        Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
    String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"and" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
y_ns
                      (IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i (((Name, Term) -> (Name, Bool)) -> [(Name, Term)] -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
b) -> (Name
n, Bool
False)) [(Name, Term)]
sc
                                        [(Name, Bool)] -> [(Name, Bool)] -> [(Name, Bool)]
forall a. [a] -> [a] -> [a]
++ [Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
nms (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)) PTerm
y))
        Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> case Maybe Provenance
yprov of
                Maybe Provenance
Nothing -> Doc OutputAnnotation
forall a. Doc a
empty
                Just Provenance
t -> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
" (" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> [(Name, Term)] -> Provenance -> Doc OutputAnnotation
pprintProv IState
i [(Name, Term)]
sc Provenance
t Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
")"
        Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
    case Err
e of
      Msg String
"" -> Doc OutputAnnotation
forall a. Doc a
empty
        -- if the specific error is the same as the one we just printed,
        -- there's no need to print it
      CantUnify Bool
_ (Term
x_in', Maybe Provenance
_) (Term
y_in',Maybe Provenance
_) Err
_ [(Name, Term)]
_ Int
_ | Term
x_in Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
x_in' Bool -> Bool -> Bool
&& Term
y_in Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
y_in' -> Doc OutputAnnotation
forall a. Doc a
empty
      Err
_ -> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Specifically:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
           Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
           if (IOption -> Bool
opt_errContext (IState -> IOption
idris_options IState
i))
             then String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Unification failure" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc IState
i [(Name, Term)]
sc
             else Doc OutputAnnotation
forall a. Doc a
empty
pprintErr' IState
i (CantConvert Term
x_in Term
y_in [(Name, Term)]
env) =
 let (Term
x_ns, Term
y_ns, [Name]
_) = Term -> Term -> (Term, Term, [Name])
renameMNs Term
x_in Term
y_in
     (PTerm
x, PTerm
y) = PTerm -> PTerm -> (PTerm, PTerm)
addImplicitDiffs (IState -> Term -> PTerm
delabSugared IState
i (Term -> Term
flagUnique Term
x_ns))
                               (IState -> Term -> PTerm
delabSugared IState
i (Term -> Term
flagUnique Term
y_ns)) in
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Type mismatch between" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
  Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
x_ns (IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i (((Name, Term) -> (Name, Bool)) -> [(Name, Term)] -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
b) -> (Name
n, Bool
False)) [(Name, Term)]
env)
               PTerm
x)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"and" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
  Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
y_ns (IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i (((Name, Term) -> (Name, Bool)) -> [(Name, Term)] -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
b) -> (Name
n, Bool
False)) [(Name, Term)]
env)
               PTerm
y)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
  if (IOption -> Bool
opt_errContext (IState -> IOption
idris_options IState
i)) then Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Conversion failure" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>  IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc IState
i [(Name, Term)]
env else Doc OutputAnnotation
forall a. Doc a
empty
    where flagUnique :: Term -> Term
flagUnique (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
i Term
t k :: Term
k@(UType Universe
u)) Term
sc)
              = AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN (Universe -> String
forall a. Show a => a -> String
show Universe
u)) Term
forall n. TT n
Erased)
                    (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i (Term -> Term
flagUnique Term
t) Term
k) (Term -> Term
flagUnique Term
sc))
          flagUnique (App AppStatus Name
s Term
f Term
a) = AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s (Term -> Term
flagUnique Term
f) (Term -> Term
flagUnique Term
a)
          flagUnique (Bind Name
n Binder Term
b Term
sc) = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n ((Term -> Term) -> Binder Term -> Binder Term
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
flagUnique Binder Term
b) (Term -> Term
flagUnique Term
sc)
          flagUnique Term
t = Term
t
pprintErr' IState
i (CantSolveGoal Term
x [(Name, Term)]
env) =
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't find a value of type " Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
  Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
x (IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i (((Name, Term) -> (Name, Bool)) -> [(Name, Term)] -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
b) -> (Name
n, Bool
False)) [(Name, Term)]
env) (IState -> Term -> PTerm
delabSugared IState
i Term
x))) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
  if (IOption -> Bool
opt_errContext (IState -> IOption
idris_options IState
i)) then Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc IState
i [(Name, Term)]
env else Doc OutputAnnotation
forall a. Doc a
empty
pprintErr' IState
i (UnifyScope Name
n Name
out Term
tm [(Name, Term)]
env) =
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't unify" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Name -> Doc OutputAnnotation
annName Name
n) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"with" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
tm (IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i (((Name, Term) -> (Name, Bool)) -> [(Name, Term)] -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
b) -> (Name
n, Bool
False)) [(Name, Term)]
env) (IState -> Term -> PTerm
delabSugared IState
i Term
tm))) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
 String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"as" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Name -> Doc OutputAnnotation
annName Name
out) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"is not in scope" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
  if (IOption -> Bool
opt_errContext (IState -> IOption
idris_options IState
i)) then Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc IState
i [(Name, Term)]
env else Doc OutputAnnotation
forall a. Doc a
empty
pprintErr' IState
i (CantInferType String
t) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't infer type for" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
t
pprintErr' IState
i (NonFunctionType Term
f Term
ty) =
  Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
f (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
f)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"does not have a function type" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
  Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
parens (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
ty))
pprintErr' IState
i (NotEquality Term
tm Term
ty) =
  Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
tm (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
tm)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"does not have an equality type" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
  Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
ty (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
parens (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
ty)))
pprintErr' IState
i (TooManyArguments Name
f) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Too many arguments for" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc OutputAnnotation
annName Name
f
pprintErr' IState
i (CantIntroduce Term
ty) =
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't use lambda here: type is" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
ty (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
ty))
pprintErr' IState
i (InfiniteUnify Name
x Term
tm [(Name, Term)]
env) =
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Unifying" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> String -> Doc OutputAnnotation
annName' Name
x (Name -> String
showbasic Name
x) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"and" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
  Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
tm (IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i (((Name, Term) -> (Name, Bool)) -> [(Name, Term)] -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
b) -> (Name
n, Bool
False)) [(Name, Term)]
env) (IState -> Term -> PTerm
delabSugared IState
i Term
tm)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"would lead to infinite value" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
  if (IOption -> Bool
opt_errContext (IState -> IOption
idris_options IState
i)) then Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc IState
i [(Name, Term)]
env else Doc OutputAnnotation
forall a. Doc a
empty
pprintErr' IState
i (NotInjective Term
p Term
x Term
y) =
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't verify injectivity of" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
p (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
p)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
" when unifying" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
x (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
x)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"and" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
  Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
y (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
y))
pprintErr' IState
i (CantResolve Bool
_ Term
c Err
e)
  = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't find implementation for" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
c)
        Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
    case Err
e of
      Msg String
"" -> Doc OutputAnnotation
forall a. Doc a
empty
      Err
_ -> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Possible cause:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
           Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e)
pprintErr' IState
i (InvalidTCArg Name
n Term
t)
   = Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
t (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
t)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
" cannot be a parameter of "
        Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Name -> Doc OutputAnnotation
annName Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
        String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"(Implementation arguments must be type or data constructors)"
pprintErr' IState
i (CantResolveAlts [Name]
as) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't disambiguate name:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
                                    Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
cat (Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. Doc a -> [Doc a] -> [Doc a]
punctuate (Doc OutputAnnotation
forall a. Doc a
comma Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
space) ((Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map ((OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
i Bool
True) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Name -> Doc OutputAnnotation) -> Name -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc OutputAnnotation
annName) [Name]
as)))
pprintErr' IState
i (NoValidAlts [Name]
as) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't disambiguate since no name has a suitable type:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
                                    Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
cat (Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. Doc a -> [Doc a] -> [Doc a]
punctuate (Doc OutputAnnotation
forall a. Doc a
comma Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
space) ((Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map ((OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
i Bool
True) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Name -> Doc OutputAnnotation) -> Name -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc OutputAnnotation
annName) [Name]
as))))
pprintErr' IState
i (NoTypeDecl Name
n) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"No type declaration for" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc OutputAnnotation
annName Name
n
pprintErr' IState
i (NoSuchVariable Name
n) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"No such variable" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc OutputAnnotation
annName Name
n
pprintErr' IState
i (WithFnType Term
ty) =
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't match on a function: type is" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
ty (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
ty))
pprintErr' IState
i (CantMatch Term
t) =
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't match on" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
t (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
t))
pprintErr' IState
i (IncompleteTerm Term
t)
    = let missing :: [(Term, Name)]
missing = [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [] [] Term
t in
          case [(Term, Name)]
missing of
            [] -> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Incomplete term" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
t (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
t))
            [(Term, Name)]
_ -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
cat (Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. Doc a -> [Doc a] -> [Doc a]
punctuate (Doc OutputAnnotation
forall a. Doc a
comma Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
space)
                       (((Term, Name) -> Doc OutputAnnotation)
-> [(Term, Name)] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (Term, Name) -> Doc OutputAnnotation
pprintIncomplete ([(Term, Name)] -> [(Term, Name)]
forall a. Eq a => [a] -> [a]
nub ([(Term, Name)] -> [(Term, Name)])
-> [(Term, Name)] -> [(Term, Name)]
forall a b. (a -> b) -> a -> b
$ [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [] [] Term
t))))
 where
   pprintIncomplete :: (Term, Name) -> Doc OutputAnnotation
pprintIncomplete (Term
tm, Name
arg)
    | Name -> Bool
expname Name
arg
      = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't infer explicit argument to" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
                   Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
tm (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
tm))
    | Bool
otherwise
      = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't infer argument" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc OutputAnnotation
annName Name
arg Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"to" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
                   Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
tm (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
tm))

   expname :: Name -> Bool
expname (UN Text
n) = case Text -> String
str Text
n of
                         (Char
'_':String
_) -> Bool
True
                         String
_ -> Bool
False
   expname (MN Int
_ Text
n) = case Text -> String
str Text
n of
                         (Char
'_':String
_) -> Bool
True
                         String
_ -> Bool
False
   expname Name
_ = Bool
False

   getMissing :: [Name] -> [Name] -> Term -> [(Term, Name)]
   getMissing :: [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs [Name]
env (Bind Name
n (Hole Term
ty) Term
sc)
       = [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
hs) (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) Term
sc
   getMissing [Name]
hs [Name]
env (Bind Name
n (Guess Term
_ Term
_) Term
sc)
       = [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
hs) (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) Term
sc
   getMissing [Name]
hs [Name]
env (Bind Name
n (Let RigCount
rc Term
t Term
v) Term
sc)
       = [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs [Name]
env Term
t [(Term, Name)] -> [(Term, Name)] -> [(Term, Name)]
forall a. [a] -> [a] -> [a]
++
         [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs [Name]
env Term
v [(Term, Name)] -> [(Term, Name)] -> [(Term, Name)]
forall a. [a] -> [a] -> [a]
++
         [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) Term
sc
   getMissing [Name]
hs [Name]
env (Bind Name
n Binder Term
b Term
sc)
       = [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs [Name]
env (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b) [(Term, Name)] -> [(Term, Name)] -> [(Term, Name)]
forall a. [a] -> [a] -> [a]
++
         [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) Term
sc
   getMissing [Name]
hs [Name]
env ap :: Term
ap@(App AppStatus Name
_ Term
_ Term
_)
       | (fn :: Term
fn@(P NameType
_ Name
n Term
_), [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap = Term -> [Term] -> [(Term, Name)]
getMissingArgs Term
fn [Term]
args
     where
       getMissingArgs :: Term -> [Term] -> [(Term, Name)]
getMissingArgs Term
n [] = []
       getMissingArgs Term
n (V Int
i : [Term]
as)
          | [Name]
env[Name] -> Int -> Name
forall a. HasCallStack => [a] -> Int -> a
!!Int
i Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs = (Term
n, [Name]
env[Name] -> Int -> Name
forall a. HasCallStack => [a] -> Int -> a
!!Int
i) (Term, Name) -> [(Term, Name)] -> [(Term, Name)]
forall a. a -> [a] -> [a]
: Term -> [Term] -> [(Term, Name)]
getMissingArgs Term
n [Term]
as
       getMissingArgs Term
n (P NameType
_ Name
a Term
_ : [Term]
as)
          | Name
a Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs = (Term
n, Name
a) (Term, Name) -> [(Term, Name)] -> [(Term, Name)]
forall a. a -> [a] -> [a]
: Term -> [Term] -> [(Term, Name)]
getMissingArgs Term
n [Term]
as
       getMissingArgs Term
n (Term
a : [Term]
as) = [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs [Name]
env Term
a [(Term, Name)] -> [(Term, Name)] -> [(Term, Name)]
forall a. [a] -> [a] -> [a]
++ Term -> [Term] -> [(Term, Name)]
getMissingArgs Term
n [Term]
as
   getMissing [Name]
hs [Name]
env (App AppStatus Name
_ Term
f Term
a)
       = [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs [Name]
env Term
f [(Term, Name)] -> [(Term, Name)] -> [(Term, Name)]
forall a. [a] -> [a] -> [a]
++ [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs [Name]
env Term
a
   getMissing [Name]
hs [Name]
env Term
_ = []
pprintErr' IState
i (UniverseError FC
fc UExp
uexp (Int, Int)
old (Int, Int)
new [ConstraintFC]
suspects) =
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Universe inconsistency." Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
  (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Doc OutputAnnotation -> Doc OutputAnnotation)
-> ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep) [ String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Working on:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text (UExp -> String
forall a. Show a => a -> String
show UExp
uexp)
                    , String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Old domain:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text ((Int, Int) -> String
forall a. Show a => a -> String
show (Int, Int)
old)
                    , String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"New domain:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text ((Int, Int) -> String
forall a. Show a => a -> String
show (Int, Int)
new)
                    , String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Involved constraints:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
                      (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Doc OutputAnnotation -> Doc OutputAnnotation)
-> ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep) ((ConstraintFC -> Doc OutputAnnotation)
-> [ConstraintFC] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc OutputAnnotation
forall a. String -> Doc a
text (String -> Doc OutputAnnotation)
-> (ConstraintFC -> String) -> ConstraintFC -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstraintFC -> String
forall a. Show a => a -> String
show) [ConstraintFC]
suspects)
                    ]
pprintErr' IState
i (UniqueError Universe
NullType Name
n)
           = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Borrowed name" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> String -> Doc OutputAnnotation
annName' Name
n (Name -> String
showbasic Name
n)
                  Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"must not be used on RHS"
pprintErr' IState
i (UniqueError Universe
_ Name
n) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Unique name" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> String -> Doc OutputAnnotation
annName' Name
n (Name -> String
showbasic Name
n)
                                  Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"is used more than once"
pprintErr' IState
i (UniqueKindError Universe
k Name
n) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Constructor" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> String -> Doc OutputAnnotation
annName' Name
n (Name -> String
showbasic Name
n)
                                   Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text (String
"has a " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Universe -> String
forall a. Show a => a -> String
show Universe
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
",")
                                   Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"but the data type does not"
pprintErr' IState
i Err
ProgramLineComment = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Program line next to comment"
pprintErr' IState
i (Inaccessible Name
n) = Name -> Doc OutputAnnotation
annName Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"is not an accessible pattern variable"
pprintErr' IState
i (UnknownImplicit Name
n Name
f) = Name -> Doc OutputAnnotation
annName Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"is not an implicit argument of" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc OutputAnnotation
annName Name
f
pprintErr' IState
i (NonCollapsiblePostulate Name
n) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"The return type of postulate" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
                                           Name -> Doc OutputAnnotation
annName Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"is not collapsible"
pprintErr' IState
i (AlreadyDefined Name
n) = Name -> Doc OutputAnnotation
annName Name
nDoc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
                                  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"is already defined"
pprintErr' IState
i (ProofSearchFail Err
e) = IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e
pprintErr' IState
i (NoRewriting Term
l Term
r Term
tm) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"rewriting" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
l (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
l)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"to" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
r (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
r)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"did not change type" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
tm (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
tm))
pprintErr' IState
i (At FC
f Err
e) = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (FC -> OutputAnnotation
AnnFC FC
f) (String -> Doc OutputAnnotation
forall a. String -> Doc a
text (FC -> String
forall a. Show a => a -> String
show FC
f)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e
pprintErr' IState
i (Elaborating String
s Name
n Maybe Term
ty Err
e) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"When checking" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
s Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
                                      Name -> String -> Doc OutputAnnotation
annName' Name
n (IState -> Name -> String
showqual IState
i Name
n) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
                                      Maybe Term -> Doc OutputAnnotation
pprintTy Maybe Term
ty Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
                                      IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e
    where pprintTy :: Maybe Term -> Doc OutputAnnotation
pprintTy Maybe Term
Nothing = Doc OutputAnnotation
forall a. Doc a
colon
          pprintTy (Just Term
ty) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
" with expected type" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
                               Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
ty (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
ty)))
                               Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line
pprintErr' IState
i (ElaboratingArg Name
f Name
x [(Name, Name)]
_ Err
e)
  | Name -> Bool
isInternal Name
f = IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e
  | Name -> Bool
isUN Name
x =
     String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"When checking argument" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
     OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (Name -> Bool -> OutputAnnotation
AnnBoundName Name
x Bool
False) (String -> Doc OutputAnnotation
forall a. String -> Doc a
text (Name -> String
showbasic Name
x)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> -- TODO check plicity
     -- Issue #1591 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1591
     String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"to" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
whatIsName Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Name -> Doc OutputAnnotation
annName Name
f Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
     Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e)
  | Bool
otherwise =
     String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"When checking an application of" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
whatIsName Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
     Name -> Doc OutputAnnotation
annName Name
f Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e)
  where whatIsName :: Doc a
whatIsName = let ctxt :: Context
ctxt = IState -> Context
tt_ctxt IState
i
                     in if Name -> Context -> Bool
isTConName Name
f Context
ctxt
                           then String -> Doc a
forall a. String -> Doc a
text String
"type constructor" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<> Doc a
forall a. Doc a
space
                           else if Name -> Context -> Bool
isDConName Name
f Context
ctxt
                                   then String -> Doc a
forall a. String -> Doc a
text String
"constructor" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<> Doc a
forall a. Doc a
space
                                   else if Name -> Context -> Bool
isFnName Name
f Context
ctxt
                                           then String -> Doc a
forall a. String -> Doc a
text String
"function" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<> Doc a
forall a. Doc a
space
                                           else Doc a
forall a. Doc a
empty
        isInternal :: Name -> Bool
isInternal (MN Int
_ Text
_) = Bool
True
        isInternal (UN Text
n) = Text -> Text -> Bool
T.isPrefixOf (String -> Text
T.pack String
"__") Text
n
        isInternal (NS Name
n [Text]
_) = Name -> Bool
isInternal Name
n
        isInternal Name
_ = Bool
True

pprintErr' IState
i (ProviderError String
msg) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text (String
"Type provider error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg)
pprintErr' IState
i (LoadingFailed String
fn Err
e) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Loading" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
fn Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"failed:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>  IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e
pprintErr' IState
i (ReflectionError [[ErrorReportPart]]
parts Err
orig) =
  let parts' :: [Doc OutputAnnotation]
parts' = ([ErrorReportPart] -> Doc OutputAnnotation)
-> [[ErrorReportPart]] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
fillSep ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> ([ErrorReportPart] -> [Doc OutputAnnotation])
-> [ErrorReportPart]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ErrorReportPart -> Doc OutputAnnotation)
-> [ErrorReportPart] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> ErrorReportPart -> Doc OutputAnnotation
showPart IState
i)) [[ErrorReportPart]]
parts in
  Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
fillSep [Doc OutputAnnotation]
parts') Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
  if (IOption -> Bool
opt_origerr (IState -> IOption
idris_options IState
i))
    then Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Original error:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
orig)
    else Doc OutputAnnotation
forall a. Doc a
empty
pprintErr' IState
i (ReflectionFailed String
msg Err
err) =
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"When attempting to perform error reflection, the following internal error occurred:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
  Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
err) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
msg Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text (String
"This is probably a bug. Please consider reporting it at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bugaddr)
pprintErr' IState
i (ElabScriptDebug [ErrorReportPart]
msg Term
tm [(Name, Term, [(Name, Binder Term)])]
holes) =
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Elaboration halted." Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
  Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (Doc OutputAnnotation -> Doc OutputAnnotation)
-> ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
hsep ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ (ErrorReportPart -> Doc OutputAnnotation)
-> [ErrorReportPart] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> ErrorReportPart -> Doc OutputAnnotation
showPart IState
i) [ErrorReportPart]
msg) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
  Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Holes:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
  Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep (((Name, Term, [(Name, Binder Term)]) -> Doc OutputAnnotation)
-> [(Name, Term, [(Name, Binder Term)])] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term, [(Name, Binder Term)]) -> Doc OutputAnnotation
ppHole [(Name, Term, [(Name, Binder Term)])]
holes)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Term: " Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented ([Name] -> Term -> Doc OutputAnnotation
pprintTT [] Term
tm)

  where ppHole :: (Name, Type, [(Name, Binder Type)]) -> Doc OutputAnnotation
        ppHole :: (Name, Term, [(Name, Binder Term)]) -> Doc OutputAnnotation
ppHole (Name
hn, Term
goal, [(Name, Binder Term)]
env) =
          [Name] -> [(Name, Binder Term)] -> Doc OutputAnnotation
ppAssumptions [] ([(Name, Binder Term)] -> [(Name, Binder Term)]
forall a. [a] -> [a]
reverse [(Name, Binder Term)]
env) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
          String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"----------------------------------" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
          Name -> Bool -> Doc OutputAnnotation
bindingOf Name
hn Bool
False Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
":" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
          [Name] -> Term -> Doc OutputAnnotation
pprintTT (((Name, Binder Term) -> Name) -> [(Name, Binder Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Binder Term) -> Name
forall a b. (a, b) -> a
fst ([(Name, Binder Term)] -> [(Name, Binder Term)]
forall a. [a] -> [a]
reverse [(Name, Binder Term)]
env)) Term
goal Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line
        ppAssumptions :: [Name] -> [(Name, Binder Type)] -> Doc OutputAnnotation
        ppAssumptions :: [Name] -> [(Name, Binder Term)] -> Doc OutputAnnotation
ppAssumptions [Name]
ns [] = Doc OutputAnnotation
forall a. Doc a
empty
        ppAssumptions [Name]
ns ((Name
n, Binder Term
b) : [(Name, Binder Term)]
rest) =
          Name -> Bool -> Doc OutputAnnotation
bindingOf Name
n Bool
False Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
          String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
":" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
          [Name] -> Term -> Doc OutputAnnotation
pprintTT [Name]
ns (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
          Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
          [Name] -> [(Name, Binder Term)] -> Doc OutputAnnotation
ppAssumptions (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
ns) [(Name, Binder Term)]
rest
pprintErr' IState
i (ElabScriptStuck Term
tm) =
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't run" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Name] -> Term -> Doc OutputAnnotation
pprintTT [] Term
tm Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"as an elaborator script." Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Is it a stuck term?"
pprintErr' IState
i (RunningElabScript Err
e) =
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"While running an elaboration script, the following error occurred" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e
pprintErr' IState
i (ElabScriptStaging Name
n) =
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't run elaboration script because it contains pattern matching that has not yet been elaborated." Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Try lifting the script to a top-level definition." Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
  String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"In particular, the problem is caused by:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc OutputAnnotation
annName Name
n
pprintErr' IState
i (FancyMsg [ErrorReportPart]
parts) =
  [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
fillSep ((ErrorReportPart -> Doc OutputAnnotation)
-> [ErrorReportPart] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> ErrorReportPart -> Doc OutputAnnotation
showPart IState
i) [ErrorReportPart]
parts)

showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation
showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation
showPart IState
ist (TextPart String
str) = [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
fillSep ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> (String -> [Doc OutputAnnotation])
-> String
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Doc OutputAnnotation)
-> [String] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc OutputAnnotation
forall a. String -> Doc a
text ([String] -> [Doc OutputAnnotation])
-> (String -> [String]) -> String -> [Doc OutputAnnotation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
words (String -> Doc OutputAnnotation) -> String -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ String
str
showPart IState
ist (NamePart Name
n)   = Name -> Doc OutputAnnotation
annName Name
n
showPart IState
ist (TermPart Term
tm)  = IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
ist (IState -> Term -> PTerm
delabSugared IState
ist Term
tm)
showPart IState
ist (RawPart Raw
tm)   = [Name] -> Raw -> Doc OutputAnnotation
pprintRaw [] Raw
tm
showPart IState
ist (SubReport [ErrorReportPart]
rs) = Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Doc OutputAnnotation -> Doc OutputAnnotation)
-> ([ErrorReportPart] -> Doc OutputAnnotation)
-> [ErrorReportPart]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
hsep ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> ([ErrorReportPart] -> [Doc OutputAnnotation])
-> [ErrorReportPart]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ErrorReportPart -> Doc OutputAnnotation)
-> [ErrorReportPart] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> ErrorReportPart -> Doc OutputAnnotation
showPart IState
ist) ([ErrorReportPart] -> Doc OutputAnnotation)
-> [ErrorReportPart] -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ [ErrorReportPart]
rs

-- | Make sure the machine invented names are shown helpfully to the user, so
-- that any names which differ internally also differ visibly
renameMNs :: Term -> Term -> (Term, Term, [Name])
renameMNs :: Term -> Term -> (Term, Term, [Name])
renameMNs Term
x Term
y = let ns :: [Name]
ns = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Term -> [Name]
forall n. Eq n => TT n -> [n]
allTTNames Term
x [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
forall n. Eq n => TT n -> [n]
allTTNames Term
y
                    newnames :: [(Name, Name)]
newnames = State Int [(Name, Name)] -> Int -> [(Name, Name)]
forall s a. State s a -> s -> a
evalState ([(Name, Name)] -> [Name] -> State Int [(Name, Name)]
getRenames [] [Name]
ns) Int
1 in
                      ([(Name, Name)] -> Term -> Term
rename [(Name, Name)]
newnames Term
x, [(Name, Name)] -> Term -> Term
rename [(Name, Name)]
newnames Term
y, ((Name, Name) -> Name) -> [(Name, Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Name) -> Name
forall a b. (a, b) -> b
snd [(Name, Name)]
newnames)
  where
    getRenames :: [(Name, Name)] -> [Name] -> State Int [(Name, Name)]
    getRenames :: [(Name, Name)] -> [Name] -> State Int [(Name, Name)]
getRenames [(Name, Name)]
acc [] = [(Name, Name)] -> State Int [(Name, Name)]
forall a. a -> StateT Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, Name)]
acc
    getRenames [(Name, Name)]
acc (n :: Name
n@(MN Int
i Text
x) : [Name]
xs) | Text -> [Name] -> Bool
rpt Text
x [Name]
xs
         = do Int
idx <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
              Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
idx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
              let x' :: Name
x' = String -> Name
sUN (Text -> String
str Text
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
idx)
              [(Name, Name)] -> [Name] -> State Int [(Name, Name)]
getRenames ((Name
n, Name
x') (Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
: [(Name, Name)]
acc) [Name]
xs
    getRenames [(Name, Name)]
acc (n :: Name
n@(UN Text
x) : [Name]
xs) | Text -> [Name] -> Bool
rpt Text
x [Name]
xs
         = do Int
idx <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
              Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
idx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
              let x' :: Name
x' = String -> Name
sUN (Text -> String
str Text
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
idx)
              [(Name, Name)] -> [Name] -> State Int [(Name, Name)]
getRenames ((Name
n, Name
x') (Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
: [(Name, Name)]
acc) [Name]
xs
    getRenames [(Name, Name)]
acc (Name
x : [Name]
xs) = [(Name, Name)] -> [Name] -> State Int [(Name, Name)]
getRenames [(Name, Name)]
acc [Name]
xs

    rpt :: Text -> [Name] -> Bool
rpt Text
x [] = Bool
False
    rpt Text
x (UN Text
y : [Name]
xs) | Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
y = Bool
True
    rpt Text
x (MN Int
i Text
y : [Name]
xs) | Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
y = Bool
True
    rpt Text
x (Name
_ : [Name]
xs) = Text -> [Name] -> Bool
rpt Text
x [Name]
xs

    rename :: [(Name, Name)] -> Term -> Term
    rename :: [(Name, Name)] -> Term -> Term
rename [(Name, Name)]
ns (P NameType
nt Name
x Term
t) | Just Name
x' <- Name -> [(Name, Name)] -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x [(Name, Name)]
ns = NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
nt Name
x' Term
t
    rename [(Name, Name)]
ns (App AppStatus Name
s Term
f Term
a) = AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s ([(Name, Name)] -> Term -> Term
rename [(Name, Name)]
ns Term
f) ([(Name, Name)] -> Term -> Term
rename [(Name, Name)]
ns Term
a)
    rename [(Name, Name)]
ns (Bind Name
x Binder Term
b Term
sc)
           = let b' :: Binder Term
b' = (Term -> Term) -> Binder Term -> Binder Term
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, Name)] -> Term -> Term
rename [(Name, Name)]
ns) Binder Term
b
                 sc' :: Term
sc' = [(Name, Name)] -> Term -> Term
rename [(Name, Name)]
ns Term
sc in
                 case Name -> [(Name, Name)] -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x [(Name, Name)]
ns of
                      Just Name
x' -> Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x' Binder Term
b' Term
sc'
                      Maybe Name
Nothing -> Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x Binder Term
b' Term
sc'
    rename [(Name, Name)]
ns Term
x = Term
x

-- If the two terms only differ in their implicits, mark the implicits which
-- differ as AlwaysShow so that they appear in errors
addImplicitDiffs :: PTerm -> PTerm -> (PTerm, PTerm)
addImplicitDiffs :: PTerm -> PTerm -> (PTerm, PTerm)
addImplicitDiffs PTerm
x PTerm
y
    = if (PTerm
x PTerm -> PTerm -> Bool
`expLike` PTerm
y) then PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
x PTerm
y else (PTerm
x, PTerm
y)
  where
    addI :: PTerm -> PTerm -> (PTerm, PTerm)
    addI :: PTerm -> PTerm -> (PTerm, PTerm)
addI (PApp FC
fc PTerm
f [PArg]
as) (PApp FC
gc PTerm
g [PArg]
bs)
         = let ([PArg]
as', [PArg]
bs') = [PArg] -> [PArg] -> ([PArg], [PArg])
addShows [PArg]
as [PArg]
bs in
               (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f [PArg]
as', FC -> PTerm -> [PArg] -> PTerm
PApp FC
gc PTerm
g [PArg]
bs')
       where addShows :: [PArg] -> [PArg] -> ([PArg], [PArg])
addShows [] [] = ([], [])
             addShows (PArg
a:[PArg]
as) (PArg
b:[PArg]
bs)
                = let ([PArg]
as', [PArg]
bs') = [PArg] -> [PArg] -> ([PArg], [PArg])
addShows [PArg]
as [PArg]
bs
                      (PTerm
a', PTerm
b') = PTerm -> PTerm -> (PTerm, PTerm)
addI (PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
a) (PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
b) in
                      if (Bool -> Bool
not (PTerm
a' PTerm -> PTerm -> Bool
`expLike` PTerm
b'))
                         then (PArg
a { argopts = AlwaysShow : argopts a,
                                   getTm = a' } PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
as',
                               PArg
b { argopts = AlwaysShow : argopts b,
                                   getTm = b' } PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
bs')
                         else (PArg
a { getTm = a' } PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
as',
                               PArg
b { getTm = b' } PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
bs')
             addShows [PArg]
xs [PArg]
ys = ([PArg]
xs, [PArg]
ys)
    addI (PLam FC
fc Name
n FC
nfc PTerm
a PTerm
b) (PLam FC
fc' Name
n' FC
nfc' PTerm
c PTerm
d)
         = let (PTerm
a', PTerm
c') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
a PTerm
c
               (PTerm
b', PTerm
d') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
b PTerm
d in
               (FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
n FC
nfc PTerm
a' PTerm
b', FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc' Name
n' FC
nfc' PTerm
c' PTerm
d')
    addI (PPi Plicity
p Name
n FC
fc PTerm
a PTerm
b) (PPi Plicity
p' Name
n' FC
fc' PTerm
c PTerm
d)
         = let (PTerm
a', PTerm
c') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
a PTerm
c
               (PTerm
b', PTerm
d') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
b PTerm
d in
               (Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p Name
n FC
fc PTerm
a' PTerm
b', Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p' Name
n' FC
fc' PTerm
c' PTerm
d')
    addI (PPair FC
fc [FC]
hls PunInfo
pi PTerm
a PTerm
b) (PPair FC
fc' [FC]
hls' PunInfo
pi' PTerm
c PTerm
d)
         = let (PTerm
a', PTerm
c') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
a PTerm
c
               (PTerm
b', PTerm
d') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
b PTerm
d in
               (FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
fc [FC]
hls PunInfo
pi PTerm
a' PTerm
b', FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
fc' [FC]
hls' PunInfo
pi' PTerm
c' PTerm
d')
    addI (PDPair FC
fc [FC]
hls PunInfo
pi PTerm
a PTerm
t PTerm
b) (PDPair FC
fc' [FC]
hls' PunInfo
pi' PTerm
c PTerm
u PTerm
d)
         = let (PTerm
a', PTerm
c') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
a PTerm
c
               (PTerm
t', PTerm
u') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
t PTerm
u
               (PTerm
b', PTerm
d') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
b PTerm
d in
               (FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
fc [FC]
hls PunInfo
pi PTerm
a' PTerm
t' PTerm
b', FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
fc' [FC]
hls' PunInfo
pi' PTerm
c' PTerm
u' PTerm
d')
    addI PTerm
x PTerm
y = (PTerm
x, PTerm
y)

    -- Just the ones which appear desugared in errors
    expLike :: PTerm -> PTerm -> Bool
expLike (PRef FC
_ [FC]
_ Name
n) (PRef FC
_ [FC]
_ Name
n') = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n'
    expLike (PApp FC
_ PTerm
f [PArg]
as) (PApp FC
_ PTerm
f' [PArg]
as')
        = PTerm -> PTerm -> Bool
expLike PTerm
f PTerm
f' Bool -> Bool -> Bool
&& [PArg] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PArg]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [PArg] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PArg]
as' Bool -> Bool -> Bool
&&
          [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((PTerm -> PTerm -> Bool) -> [PTerm] -> [PTerm] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith PTerm -> PTerm -> Bool
expLike ([PArg] -> [PTerm]
getExps [PArg]
as) ([PArg] -> [PTerm]
getExps [PArg]
as'))
    expLike (PPi Plicity
_ Name
n FC
fc PTerm
s PTerm
t) (PPi Plicity
_ Name
n' FC
fc' PTerm
s' PTerm
t')
        = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
expLike PTerm
s PTerm
s' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
expLike PTerm
t PTerm
t'
    expLike (PLam FC
_ Name
n FC
_ PTerm
s PTerm
t) (PLam FC
_ Name
n' FC
_ PTerm
s' PTerm
t')
        = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
expLike PTerm
s PTerm
s' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
expLike PTerm
t PTerm
t'
    expLike (PPair FC
_ [FC]
_ PunInfo
_ PTerm
x PTerm
y) (PPair FC
_ [FC]
_ PunInfo
_ PTerm
x' PTerm
y') = PTerm -> PTerm -> Bool
expLike PTerm
x PTerm
x' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
expLike PTerm
y PTerm
y'
    expLike (PDPair FC
_ [FC]
_ PunInfo
_ PTerm
x PTerm
_ PTerm
y) (PDPair FC
_ [FC]
_ PunInfo
_ PTerm
x' PTerm
_ PTerm
y') = PTerm -> PTerm -> Bool
expLike PTerm
x PTerm
x' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
expLike PTerm
y PTerm
y'
    expLike PTerm
x PTerm
y = PTerm
x PTerm -> PTerm -> Bool
forall a. Eq a => a -> a -> Bool
== PTerm
y

-- Issue #1589 on the issue tracker
--     https://github.com/idris-lang/Idris-dev/issues/1589
--
-- Figure out why MNs are getting rewritte to UNs for top-level
-- pattern-matching functions
isUN :: Name -> Bool
isUN :: Name -> Bool
isUN (UN Text
n) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Text -> Text -> Bool
T.isPrefixOf (String -> Text
T.pack String
"__") Text
n -- TODO
isUN (NS Name
n [Text]
_) = Name -> Bool
isUN Name
n
isUN Name
_ = Bool
False

annName :: Name -> Doc OutputAnnotation
annName :: Name -> Doc OutputAnnotation
annName Name
n = Name -> String -> Doc OutputAnnotation
annName' Name
n (Name -> String
showbasic Name
n)

annName' :: Name -> String -> Doc OutputAnnotation
annName' :: Name -> String -> Doc OutputAnnotation
annName' Name
n String
str = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing) (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
str)

annTm :: Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm :: Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
tm = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm [] Term
tm)

-- | Add extra metadata to an output annotation, optionally marking metavariables.
fancifyAnnots :: IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots :: IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
meta annot :: OutputAnnotation
annot@(AnnName Name
n Maybe NameOutput
nt Maybe String
_ Maybe String
_) =
  do let ctxt :: Context
ctxt = IState -> Context
tt_ctxt IState
ist
         docs :: Maybe String
docs = IState -> Name -> Maybe String
docOverview IState
ist Name
n
         ty :: Maybe String
ty   = String -> Maybe String
forall a. a -> Maybe a
Just (IState -> Name -> String
getTy IState
ist Name
n)
     case () of
       ()
_ | Name -> Context -> Bool
isDConName      Name
n Context
ctxt -> Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
DataOutput) Maybe String
docs Maybe String
ty
       ()
_ | Name -> Context -> Bool
isFnName        Name
n Context
ctxt -> Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
FunOutput) Maybe String
docs Maybe String
ty
       ()
_ | Name -> Context -> Bool
isTConName      Name
n Context
ctxt -> Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
TypeOutput) Maybe String
docs Maybe String
ty
       ()
_ | Name -> IState -> Bool
isMetavarName   Name
n IState
ist  -> if Bool
meta
                                       then Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
MetavarOutput) Maybe String
docs Maybe String
ty
                                       else Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
FunOutput) Maybe String
docs Maybe String
ty
       ()
_ | Name -> IState -> Bool
isPostulateName Name
n IState
ist  -> Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
PostulateOutput) Maybe String
docs Maybe String
ty
       ()
_ | Bool
otherwise              -> OutputAnnotation
annot
  where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs
        docOverview :: IState -> Name -> Maybe String
docOverview IState
ist Name
n = do (Docstring DocTerm, [(Name, Docstring DocTerm)])
docs <- Name
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
ist)
                               let o :: Docstring DocTerm
o    = Docstring DocTerm -> Docstring DocTerm
forall a. Docstring a -> Docstring a
overview ((Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm
forall a b. (a, b) -> a
fst (Docstring DocTerm, [(Name, Docstring DocTerm)])
docs)
                                   norm :: Term -> Term
norm = Context -> Env -> Term -> Term
normaliseAll (IState -> Context
tt_ctxt IState
ist) []
                                   -- TODO make width configurable
                                   -- Issue #1588 on the Issue Tracker
                                   -- https://github.com/idris-lang/Idris-dev/issues/1588
                                   out :: String -> String
out  = SimpleDoc OutputAnnotation -> String -> String
forall a. SimpleDoc a -> String -> String
displayS (SimpleDoc OutputAnnotation -> String -> String)
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> String
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
1.0 Int
50 (Doc OutputAnnotation -> String -> String)
-> Doc OutputAnnotation -> String -> String
forall a b. (a -> b) -> a -> b
$
                                          (DocTerm -> String -> Doc OutputAnnotation)
-> Docstring DocTerm -> Doc OutputAnnotation
forall a.
(a -> String -> Doc OutputAnnotation)
-> Docstring a -> Doc OutputAnnotation
renderDocstring ((Term -> Doc OutputAnnotation)
-> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation
renderDocTerm (IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist)
                                                                         Term -> Term
norm) Docstring DocTerm
o
                               String -> Maybe String
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> String
out String
"")
        getTy :: IState -> Name -> String -- fails if name not already extant!
        getTy :: IState -> Name -> String
getTy IState
ist Name
n = let theTy :: Doc OutputAnnotation
theTy = PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm (IState -> PPOption
ppOptionIst IState
ist) [] [] (IState -> [FixDecl]
idris_infixes IState
ist) (PTerm -> Doc OutputAnnotation) -> PTerm -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$
                                  IState -> PTerm -> PTerm
resugar IState
ist (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ IState -> Name -> PTerm
delabTy IState
ist Name
n
                      in (SimpleDoc OutputAnnotation -> String -> String
forall a. SimpleDoc a -> String -> String
displayS (SimpleDoc OutputAnnotation -> String -> String)
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> String
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
1.0 Int
50 (Doc OutputAnnotation -> String -> String)
-> Doc OutputAnnotation -> String -> String
forall a b. (a -> b) -> a -> b
$ Doc OutputAnnotation
theTy) String
""
fancifyAnnots IState
_ Bool
_ OutputAnnotation
annot = OutputAnnotation
annot

showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc IState
i [] = Doc OutputAnnotation
forall a. Doc a
empty
showSc IState
i [(Name, Term)]
xs = Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"In context:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
            Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ([Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. [a] -> [a]
reverse ([(Name, Bool)] -> [(Name, Term)] -> [Doc OutputAnnotation]
showSc' [] [(Name, Term)]
xs)))
     where showSc' :: [(Name, Bool)] -> [(Name, Term)] -> [Doc OutputAnnotation]
showSc' [(Name, Bool)]
bnd [] = []
           showSc' [(Name, Bool)]
bnd ((Name
n, Term
ty):[(Name, Term)]
ctxt) =
             let this :: Doc OutputAnnotation
this = Name -> Bool -> Doc OutputAnnotation
bindingOf Name
n Bool
False Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i [(Name, Bool)]
bnd (IState -> Term -> PTerm
delabSugared IState
i Term
ty)
             in Doc OutputAnnotation
this Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. a -> [a] -> [a]
: [(Name, Bool)] -> [(Name, Term)] -> [Doc OutputAnnotation]
showSc' ((Name
n,Bool
False)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) [(Name, Term)]
ctxt


showqual :: IState -> Name -> String
showqual :: IState -> Name -> String
showqual IState
i Name
n = Maybe IState
-> [(Name, Bool)] -> PPOption -> Bool -> Name -> String
showName (IState -> Maybe IState
forall a. a -> Maybe a
Just IState
i) [] (IState -> PPOption
ppOptionIst IState
i) { ppopt_impl = False } Bool
False (Name -> Name
dens Name
n)
  where
    dens :: Name -> Name
dens ns :: Name
ns@(NS Name
n [Text]
_) = case Name -> Ctxt [PArg] -> [[PArg]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
                              [[PArg]
_] -> Name
n -- just one thing
                              [[PArg]]
_ -> Name
ns
    dens Name
n = Name
n

showbasic :: Name -> String
showbasic :: Name -> String
showbasic n :: Name
n@(UN Text
_) = Name -> String
forall a. Show a => a -> String
show Name
n
showbasic (MN Int
_ Text
s) = Text -> String
str Text
s
showbasic (NS Name
n [Text]
s) = String -> [String] -> String
showSep String
"." ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
str ([Text] -> [Text]
forall a. [a] -> [a]
reverse [Text]
s)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"." String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
showbasic Name
n
showbasic (SN SpecialName
s) = SpecialName -> String
forall a. Show a => a -> String
show SpecialName
s
showbasic Name
n = Name -> String
forall a. Show a => a -> String
show Name
n