{-|
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, 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 :: [Char]
bugaddr = "https://github.com/idris-lang/Idris-dev/issues"

-- | Re-add syntactic sugar in a term
resugar :: IState -> PTerm -> PTerm
resugar :: IState -> PTerm -> PTerm
resugar ist :: 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
fc (PRef _ _ n :: Name
n) args :: [PArg]
args)
      | [c :: PTerm
c, t :: PTerm
t, f :: 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
== [Char] -> Name
sUN "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
fc (PRef _ _ n :: Name
n) args :: [PArg]
args)
      | [v :: PTerm
v, PLam _ bn :: Name
bn _ _ next :: 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
== [Char] -> Name
sUN ">>="
      = let step :: PDo' PTerm
step = if Name
bn Name -> [Name] -> 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 dos :: [PDo' PTerm]
dos -> [PDo' PTerm] -> PTerm
PDoBlock (PDo' PTerm
step PDo' PTerm -> [PDo' PTerm] -> [PDo' PTerm]
forall a. a -> [a] -> [a]
: [PDo' PTerm]
dos)
             expr :: 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
fc (PRef _ _ n :: Name
n) args :: [PArg]
args)
      | [PConstant fc :: FC
fc (BI i :: 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
== [Char] -> Name
sUN "fromInteger"
      = FC -> Const -> PTerm
PConstant FC
fc (Integer -> Const
BI Integer
i)
    resugarApp tm :: PTerm
tm = PTerm
tm

    flattenDoLet :: PTerm -> PTerm
flattenDoLet (PLet _ rc :: RigCount
rc ln :: Name
ln _ ty :: PTerm
ty v :: PTerm
v bdy :: PTerm
bdy)
      | PDoBlock dos :: [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 dos :: [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 _ (PLet _ rc :: RigCount
rc ln :: Name
ln _ ty :: PTerm
ty v :: PTerm
v bdy :: 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 d :: PDo' PTerm
d = [PDo' PTerm
d]
    flattenDoLet tm :: PTerm
tm = PTerm
tm

    dedelay :: PTerm -> PTerm
dedelay (PApp _ (PRef _ _ delay :: Name
delay) [_, _, obj :: PArg
obj])
      | Name
delay Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Name
sUN "Delay" = PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
obj
    dedelay x :: 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 _ = Maybe a
forall a. Maybe a
Nothing


-- | Delaborate and resugar a term
delabSugared :: IState -> Term -> PTerm
delabSugared :: IState -> Term -> PTerm
delabSugared ist :: IState
ist tm :: 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 i :: IState
i tm :: 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 i :: IState
i tys :: [(Name, Term)]
tys tm :: 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 i :: IState
i tm :: 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 i :: IState
i tm :: 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 i :: IState
i n :: Name
n
    = case Name -> Context -> [Term]
lookupTy Name
n (IState -> Context
tt_ctxt IState
i) of
           (ty :: Term
ty:_) -> case Name -> Ctxt [PArg] -> [[PArg]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
                         (imps :: [PArg]
imps:_) -> IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [PArg]
imps [] Term
ty Bool
False Bool
False Bool
True
                         _ -> IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [] [] Term
ty Bool
False Bool
False Bool
True
           [] -> [Char] -> PTerm
forall a. HasCallStack => [Char] -> a
error "delabTy: got non-existing name"

delab' :: IState -> Term -> Bool -> Bool -> PTerm
delab' :: IState -> Term -> Bool -> Bool -> PTerm
delab' i :: IState
i t :: Term
t f :: Bool
f mvs :: 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' i :: IState
i tys :: [(Name, Term)]
tys t :: Term
t f :: Bool
f mvs :: 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' ist :: IState
ist imps :: [PArg]
imps genv :: [(Name, Term)]
genv tm :: Term
tm fullname :: Bool
fullname mvs :: Bool
mvs docases :: Bool
docases = [(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
genv [] [PArg]
imps Term
tm
  where
    un :: FC
un = [Char] -> FC
fileFC "(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 tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env imps :: [PArg]
imps sc :: Term
sc
          | Bool
docases
          , Term -> Bool
isCaseApp Term
sc
          , (P _ cOp :: Name
cOp _, args :: [Term]
args@(_:_)) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
sc
          , Just caseblock :: 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. [a] -> a
last [Term]
args) Name
cOp [Term]
args
                 = PTerm
caseblock

    de tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env _ (App _ f :: Term
f a :: Term
a) = [(Name, Term)] -> [(Name, Name)] -> Term -> [Term] -> PTerm
deFn [(Name, Term)]
tys [(Name, Name)]
env Term
f [Term
a]
    de tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env _ (V i :: Int
i) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [(Name, Name)] -> 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. [a] -> Int -> a
!!Int
i))
                       | Bool
otherwise = FC -> [FC] -> Name -> PTerm
PRef FC
un [] ([Char] -> Name
sUN ("v" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ""))
    de tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env _ (P _ n :: Name
n _) | 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 n' :: 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 _, mi :: Int
mi, _, _, _) -> Name -> [PTerm] -> PTerm
mkMVApp Name
n []
                                      _ -> FC -> [FC] -> Name -> PTerm
PRef FC
un [] Name
n
    de tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env _ (Bind n :: Name
n (Lam _ ty :: Term
ty) sc :: 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 tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env (_ : is :: [PArg]
is) (Bind n :: Name
n (Pi rig :: RigCount
rig (Just impl :: ImplicitInfo
impl) ty :: Term
ty _) sc :: 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 tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env is :: [PArg]
is (Bind n :: Name
n (Pi rig :: RigCount
rig (Just impl :: ImplicitInfo
impl) ty :: Term
ty _) sc :: 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 tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env ((PImp { argopts :: forall t. PArg' t -> [ArgOpt]
argopts = [ArgOpt]
opts }):is :: [PArg]
is) (Bind n :: Name
n (Pi rig :: RigCount
rig _ ty :: Term
ty _) sc :: 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 tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env (PConstraint _ _ _ _:is :: [PArg]
is) (Bind n :: Name
n (Pi rig :: RigCount
rig _ ty :: Term
ty _) sc :: Term
sc)
          = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
constraint { pcount :: RigCount
pcount = 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 tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env (PTacImplicit _ _ _ tac :: PTerm
tac _:is :: [PArg]
is) (Bind n :: Name
n (Pi rig :: RigCount
rig _ ty :: Term
ty _) sc :: Term
sc)
          = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ((PTerm -> Plicity
tacimpl PTerm
tac) { pcount :: RigCount
pcount = 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 tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env (plic :: PArg
plic:is :: [PArg]
is) (Bind n :: Name
n (Pi rig :: RigCount
rig _ ty :: Term
ty _) sc :: 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 tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env [] (Bind n :: Name
n (Pi rig :: RigCount
rig _ ty :: Term
ty _) sc :: Term
sc)
          = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
expl { pcount :: RigCount
pcount = 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) [] Term
sc)

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

    deFn :: [(Name, Term)] -> [(Name, Name)] -> Term -> [Term] -> PTerm
deFn tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env (App _ f :: Term
f a :: Term
a) args :: [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 tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env (P _ n :: Name
n _) [l :: Term
l,r :: 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 tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env (P _ n :: Name
n _) [ty :: Term
ty, Bind x :: Name
x (Lam _ _) r :: 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 tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env (P _ n :: Name
n _) [lt :: Term
lt,rt :: Term
rt,l :: Term
l,r :: 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 tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env (P _ n :: Name
n _) args :: [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 _, mi :: Int
mi, _, _, _) ->
                            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))
                        _ -> [(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 tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env (V i :: Int
i) args :: [Term]
args
         | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [(Name, Name)] -> 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. [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 tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env f :: Term
f args :: [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 n :: Name
n []
            = FC -> Name -> PTerm
PMetavar FC
NoFC Name
n
    mkMVApp n :: Name
n args :: [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 tys :: [(Name, Term)]
tys n :: Name
n args :: [PTerm]
args
        | Just ty :: 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 imps :: [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 n :: Name
n (Pi _ im :: Maybe ImplicitInfo
im@(Just i :: ImplicitInfo
i) _ _) sc :: 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 n :: Name
n (Pi _ _ _ _) sc :: 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 _ = []
    imp :: PArg' t -> t -> PArg' t
imp (PImp p :: Int
p m :: Bool
m l :: [ArgOpt]
l n :: Name
n _) arg :: 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 p :: Int
p l :: [ArgOpt]
l n :: Name
n _)   arg :: 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 p :: Int
p l :: [ArgOpt]
l n :: Name
n _) arg :: 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 p :: Int
p l :: [ArgOpt]
l n :: Name
n sc :: t
sc _) arg :: 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 tm :: Term
tm | P _ n :: Name
n _ <- (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 n :: Name
n _) = Name -> Bool
isCN Name
n
            isCN (SN (CaseN _ _)) = Bool
True
            isCN _ = 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 tys :: [(Name, Term)]
tys env :: [(Name, Name)]
env imps :: [PArg]
imps scrutinee :: Term
scrutinee caseName :: Name
caseName caseArgs :: [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
                    [(cases :: [([(Name, Term)], Term, Term)]
cases, _)] -> [([(Name, Term)], Term, Term)]
-> Maybe [([(Name, Term)], Term, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [([(Name, Term)], Term, Term)]
cases
                    _ -> Maybe [([(Name, Term)], Term, Term)]
forall a. Maybe a
Nothing
         PTerm -> Maybe PTerm
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 (\(n :: Name
n, _) -> (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 (\(n :: Name
n, _) -> (Name
n, Name
n)) [(Name, Term)]
vars) [PArg]
imps Term
rhs)
                    | (vars :: [(Name, Term)]
vars, lhs :: Term
lhs, rhs :: Term
rhs) <- [([(Name, Term)], Term, Term)]
cases
                    ]
      where splitArg :: TT n -> TT n
splitArg tm :: TT n
tm | (_, args :: [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 [] = [Char] -> TT n
forall a. HasCallStack => [Char] -> a
error "Tried to delaborate empty case list"
            nonVar [x :: TT n
x] = TT n
x
            nonVar (x :: TT n
x@(App _ _ _) : _) = TT n
x
            nonVar (x :: TT n
x@(P (DCon _ _ _) _ _) : _) = TT n
x
            nonVar (x :: TT n
x:xs :: [TT n]
xs) = [TT n] -> TT n
nonVar [TT n]
xs
-- | How far to indent sub-errors
errorIndent :: Int
errorIndent :: Int
errorIndent = 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 :: 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 ist :: IState
ist tm :: 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 ist :: IState
ist tm :: 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))

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

pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
pprintTerm ist :: 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' ist :: IState
ist bnd :: [(Name, Bool)]
bnd tm :: 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 i :: IState
i e :: [(Name, Term)]
e ExpectedType = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "Expected type"
pprintProv i :: IState
i e :: [(Name, Term)]
e InferredVal = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "Inferred value"
pprintProv i :: IState
i e :: [(Name, Term)]
e GivenVal = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "Given value"
pprintProv i :: IState
i e :: [(Name, Term)]
e (SourceTerm tm :: Term
tm)
  = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 i :: IState
i e :: [(Name, Term)]
e (TooManyArgs tm :: Term
tm)
  = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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
<> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text " applied to too many arguments?"

pprintErr :: IState -> Err -> Doc OutputAnnotation
pprintErr :: IState -> Err -> Doc OutputAnnotation
pprintErr i :: IState
i err :: Err
err = IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i ((Term -> Term) -> Err -> Err
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' i :: IState
i (Msg s :: [Char]
s) = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text [Char]
s
pprintErr' i :: IState
i (InternalMsg s :: [Char]
s) =
  [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep [ [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "INTERNAL ERROR:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text [Char]
s,
         [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "This is probably a bug, or a missing error message.",
         [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text ("Please consider reporting at " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
bugaddr)
       ]
pprintErr' i :: IState
i (CantUnify _ (x_in :: Term
x_in, xprov :: Maybe Provenance
xprov) (y_in :: Term
y_in, yprov :: Maybe Provenance
yprov) e :: Err
e sc :: [(Name, Term)]
sc s :: Int
s) =
  let (x_ns :: Term
x_ns, y_ns :: Term
y_ns, nms :: [Name]
nms) = Term -> Term -> (Term, Term, [Name])
renameMNs Term
x_in Term
y_in
      (x :: PTerm
x, y :: 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
    [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 (\ (n :: Name
n, b :: 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
                Nothing -> Doc OutputAnnotation
forall a. Doc a
empty
                Just t :: Provenance
t -> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text " (" 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
<> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text ")"
        Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
    [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 (\ (n :: Name
n, b :: 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
                Nothing -> Doc OutputAnnotation
forall a. Doc a
empty
                Just t :: Provenance
t -> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text " (" 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
<> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text ")"
        Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
    case Err
e of
      Msg "" -> 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 _ (x_in' :: Term
x_in', _) (y_in' :: Term
y_in',_) _ _ _ | 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
      _ -> 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
<> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (CantConvert x_in :: Term
x_in y_in :: Term
y_in env :: [(Name, Term)]
env) =
 let (x_ns :: Term
x_ns, y_ns :: Term
y_ns, _) = Term -> Term -> (Term, Term, [Name])
renameMNs Term
x_in Term
y_in
     (x :: PTerm
x, y :: 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
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 (\ (n :: Name
n, b :: 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
<$>
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 (\ (n :: Name
n, b :: 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
<> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 n :: Name
n (Pi rig :: RigCount
rig i :: Maybe ImplicitInfo
i t :: Term
t k :: Term
k@(UType u :: Universe
u)) sc :: 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 ([Char] -> Name
sUN (Universe -> [Char]
forall a. Show a => a -> [Char]
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 s :: AppStatus Name
s f :: Term
f a :: 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 n :: Name
n b :: Binder Term
b sc :: 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
flagUnique Binder Term
b) (Term -> Term
flagUnique Term
sc)
          flagUnique t :: Term
t = Term
t
pprintErr' i :: IState
i (CantSolveGoal x :: Term
x env :: [(Name, Term)]
env) =
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 (\ (n :: Name
n, b :: 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' i :: IState
i (UnifyScope n :: Name
n out :: Name
out tm :: Term
tm env :: [(Name, Term)]
env) =
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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
<+>
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 (\ (n :: Name
n, b :: 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
<+>
 [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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
<> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (CantInferType t :: [Char]
t) = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "Can't infer type for" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text [Char]
t
pprintErr' i :: IState
i (NonFunctionType f :: Term
f ty :: 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
<+>
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (NotEquality tm :: Term
tm ty :: 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
<+>
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (TooManyArguments f :: Name
f) = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (CantIntroduce ty :: Term
ty) =
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (InfiniteUnify x :: Name
x tm :: Term
tm env :: [(Name, Term)]
env) =
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "Unifying" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> [Char] -> Doc OutputAnnotation
annName' Name
x (Name -> [Char]
showbasic Name
x) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 (\ (n :: Name
n, b :: 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
<+>
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (NotInjective p :: Term
p x :: Term
x y :: Term
y) =
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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
<+>
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text " 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
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (CantResolve _ c :: Term
c e :: Err
e)
  = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 "" -> Doc OutputAnnotation
forall a. Doc a
empty
      _ -> 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
<> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (InvalidTCArg n :: Name
n t :: 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
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text " 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
<$>
        [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "(Implementation arguments must be type or data constructors)"
pprintErr' i :: IState
i (CantResolveAlts as :: [Name]
as) = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 (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' i :: IState
i (NoValidAlts as :: [Name]
as) = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 (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' i :: IState
i (NoTypeDecl n :: Name
n) = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (NoSuchVariable n :: Name
n) = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "No such variable" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc OutputAnnotation
annName Name
n
pprintErr' i :: IState
i (WithFnType ty :: Term
ty) =
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (CantMatch t :: Term
t) =
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (IncompleteTerm t :: Term
t)
    = let missing :: [(Term, Name)]
missing = [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [] [] Term
t in
          case [(Term, Name)]
missing of
            [] -> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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))
            _ -> 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 (tm :: Term
tm, arg :: Name
arg)
    | Name -> Bool
expname Name
arg
      = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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
      = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 n :: Text
n) = case Text -> [Char]
str Text
n of
                         ('_':_) -> Bool
True
                         _ -> Bool
False
   expname (MN _ n :: Text
n) = case Text -> [Char]
str Text
n of
                         ('_':_) -> Bool
True
                         _ -> Bool
False
   expname _ = Bool
False

   getMissing :: [Name] -> [Name] -> Term -> [(Term, Name)]
   getMissing :: [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing hs :: [Name]
hs env :: [Name]
env (Bind n :: Name
n (Hole ty :: Term
ty) sc :: 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 hs :: [Name]
hs env :: [Name]
env (Bind n :: Name
n (Guess _ _) sc :: 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 hs :: [Name]
hs env :: [Name]
env (Bind n :: Name
n (Let rc :: RigCount
rc t :: Term
t v :: Term
v) sc :: 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 hs :: [Name]
hs env :: [Name]
env (Bind n :: Name
n b :: Binder Term
b sc :: 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 hs :: [Name]
hs env :: [Name]
env ap :: Term
ap@(App _ _ _)
       | (fn :: Term
fn@(P _ n :: Name
n _), args :: [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 n :: Term
n [] = []
       getMissingArgs n :: Term
n (V i :: Int
i : as :: [Term]
as)
          | [Name]
env[Name] -> Int -> Name
forall a. [a] -> Int -> a
!!Int
i Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs = (Term
n, [Name]
env[Name] -> Int -> Name
forall a. [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 n :: Term
n (P _ a :: Name
a _ : as :: [Term]
as)
          | Name
a Name -> [Name] -> 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 n :: Term
n (a :: Term
a : as :: [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 hs :: [Name]
hs env :: [Name]
env (App _ f :: Term
f a :: 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 hs :: [Name]
hs env :: [Name]
env _ = []
pprintErr' i :: IState
i (UniverseError fc :: FC
fc uexp :: UExp
uexp old :: (Int, Int)
old new :: (Int, Int)
new suspects :: [ConstraintFC]
suspects) =
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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) [ [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "Working on:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text (UExp -> [Char]
forall a. Show a => a -> [Char]
show UExp
uexp)
                    , [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "Old domain:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text ((Int, Int) -> [Char]
forall a. Show a => a -> [Char]
show (Int, Int)
old)
                    , [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "New domain:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text ((Int, Int) -> [Char]
forall a. Show a => a -> [Char]
show (Int, Int)
new)
                    , [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 ([Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text ([Char] -> Doc OutputAnnotation)
-> (ConstraintFC -> [Char]) -> ConstraintFC -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstraintFC -> [Char]
forall a. Show a => a -> [Char]
show) [ConstraintFC]
suspects)
                    ]
pprintErr' i :: IState
i (UniqueError NullType n :: Name
n)
           = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "Borrowed name" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> [Char] -> Doc OutputAnnotation
annName' Name
n (Name -> [Char]
showbasic Name
n)
                  Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "must not be used on RHS"
pprintErr' i :: IState
i (UniqueError _ n :: Name
n) = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "Unique name" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> [Char] -> Doc OutputAnnotation
annName' Name
n (Name -> [Char]
showbasic Name
n)
                                  Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "is used more than once"
pprintErr' i :: IState
i (UniqueKindError k :: Universe
k n :: Name
n) = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "Constructor" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> [Char] -> Doc OutputAnnotation
annName' Name
n (Name -> [Char]
showbasic Name
n)
                                   Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text ("has a " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Universe -> [Char]
forall a. Show a => a -> [Char]
show Universe
k [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ",")
                                   Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "but the data type does not"
pprintErr' i :: IState
i ProgramLineComment = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "Program line next to comment"
pprintErr' i :: IState
i (Inaccessible n :: Name
n) = Name -> Doc OutputAnnotation
annName Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "is not an accessible pattern variable"
pprintErr' i :: IState
i (UnknownImplicit n :: Name
n f :: Name
f) = Name -> Doc OutputAnnotation
annName Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (NonCollapsiblePostulate n :: Name
n) = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "is not collapsible"
pprintErr' i :: IState
i (AlreadyDefined n :: Name
n) = Name -> Doc OutputAnnotation
annName Name
nDoc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
                                  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "is already defined"
pprintErr' i :: IState
i (ProofSearchFail e :: Err
e) = IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e
pprintErr' i :: IState
i (NoRewriting l :: Term
l r :: Term
r tm :: Term
tm) = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (At f :: FC
f e :: Err
e) = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (FC -> OutputAnnotation
AnnFC FC
f) ([Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text (FC -> [Char]
forall a. Show a => a -> [Char]
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' i :: IState
i (Elaborating s :: [Char]
s n :: Name
n ty :: Maybe Term
ty e :: Err
e) = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "When checking" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text [Char]
s Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
                                      Name -> [Char] -> Doc OutputAnnotation
annName' Name
n (IState -> Name -> [Char]
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 Nothing = Doc OutputAnnotation
forall a. Doc a
colon
          pprintTy (Just ty :: Term
ty) = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text " 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' i :: IState
i (ElaboratingArg f :: Name
f x :: Name
x _ e :: Err
e)
  | Name -> Bool
isInternal Name
f = IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e
  | Name -> Bool
isUN Name
x =
     [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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) ([Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text (Name -> [Char]
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
     [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 =
     [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 [Char] -> Doc a
forall a. [Char] -> Doc a
text "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 [Char] -> Doc a
forall a. [Char] -> Doc a
text "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 [Char] -> Doc a
forall a. [Char] -> Doc a
text "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 _ _) = Bool
True
        isInternal (UN n :: Text
n) = Text -> Text -> Bool
T.isPrefixOf ([Char] -> Text
T.pack "__") Text
n
        isInternal (NS n :: Name
n _) = Name -> Bool
isInternal Name
n
        isInternal _ = Bool
True

pprintErr' i :: IState
i (ProviderError msg :: [Char]
msg) = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text ("Type provider error: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg)
pprintErr' i :: IState
i (LoadingFailed fn :: [Char]
fn e :: Err
e) = [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "Loading" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text [Char]
fn Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (ReflectionError parts :: [[ErrorReportPart]]
parts orig :: 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
<> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (ReflectionFailed msg :: [Char]
msg err :: Err
err) =
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text [Char]
msg Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text ("This is probably a bug. Please consider reporting it at " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
bugaddr)
pprintErr' i :: IState
i (ElabScriptDebug msg :: [ErrorReportPart]
msg tm :: Term
tm holes :: [(Name, Term, [(Name, Binder Term)])]
holes) =
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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
<>
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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
<>
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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 (hn :: Name
hn, goal :: Term
goal, env :: [(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
<>
          [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "----------------------------------" 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
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text ":" 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 ns :: [Name]
ns [] = Doc OutputAnnotation
forall a. Doc a
empty
        ppAssumptions ns :: [Name]
ns ((n :: Name
n, b :: Binder Term
b) : rest :: [(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
<+>
          [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text ":" 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' i :: IState
i (ElabScriptStuck tm :: Term
tm) =
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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
<+> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "as an elaborator script." Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "Is it a stuck term?"
pprintErr' i :: IState
i (RunningElabScript e :: Err
e) =
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (ElabScriptStaging n :: Name
n) =
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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
<$>
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "Try lifting the script to a top-level definition." Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
  [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' i :: IState
i (FancyMsg parts :: [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 ist :: IState
ist (TextPart str :: [Char]
str) = [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
fillSep ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> ([Char] -> [Doc OutputAnnotation])
-> [Char]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> Doc OutputAnnotation)
-> [[Char]] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text ([[Char]] -> [Doc OutputAnnotation])
-> ([Char] -> [[Char]]) -> [Char] -> [Doc OutputAnnotation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[Char]]
words ([Char] -> Doc OutputAnnotation) -> [Char] -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ [Char]
str
showPart ist :: IState
ist (NamePart n :: Name
n)   = Name -> Doc OutputAnnotation
annName Name
n
showPart ist :: IState
ist (TermPart tm :: Term
tm)  = IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
ist (IState -> Term -> PTerm
delabSugared IState
ist Term
tm)
showPart ist :: IState
ist (RawPart tm :: Raw
tm)   = [Name] -> Raw -> Doc OutputAnnotation
pprintRaw [] Raw
tm
showPart ist :: IState
ist (SubReport rs :: [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 x :: Term
x y :: 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) 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 acc :: [(Name, Name)]
acc [] = [(Name, Name)] -> State Int [(Name, Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, Name)]
acc
    getRenames acc :: [(Name, Name)]
acc (n :: Name
n@(MN i :: Int
i x :: Text
x) : xs :: [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
+ 1)
              let x' :: Name
x' = [Char] -> Name
sUN (Text -> [Char]
str Text
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
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 acc :: [(Name, Name)]
acc (n :: Name
n@(UN x :: Text
x) : xs :: [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
+ 1)
              let x' :: Name
x' = [Char] -> Name
sUN (Text -> [Char]
str Text
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
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 acc :: [(Name, Name)]
acc (x :: Name
x : xs :: [Name]
xs) = [(Name, Name)] -> [Name] -> State Int [(Name, Name)]
getRenames [(Name, Name)]
acc [Name]
xs

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

    rename :: [(Name, Name)] -> Term -> Term
    rename :: [(Name, Name)] -> Term -> Term
rename ns :: [(Name, Name)]
ns (P nt :: NameType
nt x :: Name
x t :: Term
t) | Just x' :: 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 ns :: [(Name, Name)]
ns (App s :: AppStatus Name
s f :: Term
f a :: 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 ns :: [(Name, Name)]
ns (Bind x :: Name
x b :: Binder Term
b sc :: Term
sc)
           = let b' :: Binder Term
b' = (Term -> Term) -> Binder Term -> Binder Term
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 x' :: 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'
                      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 ns :: [(Name, Name)]
ns x :: 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 x :: PTerm
x y :: 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
fc f :: PTerm
f as :: [PArg]
as) (PApp gc :: FC
gc g :: PTerm
g bs :: [PArg]
bs)
         = let (as' :: [PArg]
as', bs' :: [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 (a :: PArg
a:as :: [PArg]
as) (b :: PArg
b:bs :: [PArg]
bs)
                = let (as' :: [PArg]
as', bs' :: [PArg]
bs') = [PArg] -> [PArg] -> ([PArg], [PArg])
addShows [PArg]
as [PArg]
bs
                      (a' :: PTerm
a', b' :: 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 :: [ArgOpt]
argopts = ArgOpt
AlwaysShow ArgOpt -> [ArgOpt] -> [ArgOpt]
forall a. a -> [a] -> [a]
: PArg -> [ArgOpt]
forall t. PArg' t -> [ArgOpt]
argopts PArg
a,
                                   getTm :: PTerm
getTm = PTerm
a' } PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
as',
                               PArg
b { argopts :: [ArgOpt]
argopts = ArgOpt
AlwaysShow ArgOpt -> [ArgOpt] -> [ArgOpt]
forall a. a -> [a] -> [a]
: PArg -> [ArgOpt]
forall t. PArg' t -> [ArgOpt]
argopts PArg
b,
                                   getTm :: PTerm
getTm = PTerm
b' } PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
bs')
                         else (PArg
a { getTm :: PTerm
getTm = PTerm
a' } PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
as',
                               PArg
b { getTm :: PTerm
getTm = PTerm
b' } PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
bs')
             addShows xs :: [PArg]
xs ys :: [PArg]
ys = ([PArg]
xs, [PArg]
ys)
    addI (PLam fc :: FC
fc n :: Name
n nfc :: FC
nfc a :: PTerm
a b :: PTerm
b) (PLam fc' :: FC
fc' n' :: Name
n' nfc' :: FC
nfc' c :: PTerm
c d :: PTerm
d)
         = let (a' :: PTerm
a', c' :: PTerm
c') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
a PTerm
c
               (b' :: PTerm
b', d' :: 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 p :: Plicity
p n :: Name
n fc :: FC
fc a :: PTerm
a b :: PTerm
b) (PPi p' :: Plicity
p' n' :: Name
n' fc' :: FC
fc' c :: PTerm
c d :: PTerm
d)
         = let (a' :: PTerm
a', c' :: PTerm
c') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
a PTerm
c
               (b' :: PTerm
b', d' :: 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 :: [FC]
hls pi :: PunInfo
pi a :: PTerm
a b :: PTerm
b) (PPair fc' :: FC
fc' hls' :: [FC]
hls' pi' :: PunInfo
pi' c :: PTerm
c d :: PTerm
d)
         = let (a' :: PTerm
a', c' :: PTerm
c') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
a PTerm
c
               (b' :: PTerm
b', d' :: 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 :: [FC]
hls pi :: PunInfo
pi a :: PTerm
a t :: PTerm
t b :: PTerm
b) (PDPair fc' :: FC
fc' hls' :: [FC]
hls' pi' :: PunInfo
pi' c :: PTerm
c u :: PTerm
u d :: PTerm
d)
         = let (a' :: PTerm
a', c' :: PTerm
c') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
a PTerm
c
               (t' :: PTerm
t', u' :: PTerm
u') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
t PTerm
u
               (b' :: PTerm
b', d' :: 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 x :: PTerm
x y :: PTerm
y = (PTerm
x, PTerm
y)

    -- Just the ones which appear desugared in errors
    expLike :: PTerm -> PTerm -> Bool
expLike (PRef _ _ n :: Name
n) (PRef _ _ n' :: Name
n') = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n'
    expLike (PApp _ f :: PTerm
f as :: [PArg]
as) (PApp _ f' :: PTerm
f' as' :: [PArg]
as')
        = PTerm -> PTerm -> Bool
expLike PTerm
f PTerm
f' Bool -> Bool -> Bool
&& [PArg] -> 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 (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 _ n :: Name
n fc :: FC
fc s :: PTerm
s t :: PTerm
t) (PPi _ n' :: Name
n' fc' :: FC
fc' s' :: PTerm
s' t' :: 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 _ n :: Name
n _ s :: PTerm
s t :: PTerm
t) (PLam _ n' :: Name
n' _ s' :: PTerm
s' t' :: 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 _ _ _ x :: PTerm
x y :: PTerm
y) (PPair _ _ _ x' :: PTerm
x' y' :: PTerm
y') = PTerm -> PTerm -> Bool
expLike PTerm
x PTerm
x' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
expLike PTerm
y PTerm
y'
    expLike (PDPair _ _ _ x :: PTerm
x _ y :: PTerm
y) (PDPair _ _ _ x' :: PTerm
x' _ y' :: PTerm
y') = PTerm -> PTerm -> Bool
expLike PTerm
x PTerm
x' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
expLike PTerm
y PTerm
y'
    expLike x :: PTerm
x y :: 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 n :: Text
n) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Text -> Text -> Bool
T.isPrefixOf ([Char] -> Text
T.pack "__") Text
n -- TODO
isUN (NS n :: Name
n _) = Name -> Bool
isUN Name
n
isUN _ = Bool
False

annName :: Name -> Doc OutputAnnotation
annName :: Name -> Doc OutputAnnotation
annName n :: Name
n = Name -> [Char] -> Doc OutputAnnotation
annName' Name
n (Name -> [Char]
showbasic Name
n)

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

annTm :: Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm :: Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm tm :: 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 ist :: IState
ist meta :: Bool
meta annot :: OutputAnnotation
annot@(AnnName n :: Name
n nt :: Maybe NameOutput
nt _ _) =
  do let ctxt :: Context
ctxt = IState -> Context
tt_ctxt IState
ist
         docs :: Maybe [Char]
docs = IState -> Name -> Maybe [Char]
docOverview IState
ist Name
n
         ty :: Maybe [Char]
ty   = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just (IState -> Name -> [Char]
getTy IState
ist Name
n)
     case () of
       _ | Name -> Context -> Bool
isDConName      Name
n Context
ctxt -> Name
-> Maybe NameOutput
-> Maybe [Char]
-> Maybe [Char]
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
DataOutput) Maybe [Char]
docs Maybe [Char]
ty
       _ | Name -> Context -> Bool
isFnName        Name
n Context
ctxt -> Name
-> Maybe NameOutput
-> Maybe [Char]
-> Maybe [Char]
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
FunOutput) Maybe [Char]
docs Maybe [Char]
ty
       _ | Name -> Context -> Bool
isTConName      Name
n Context
ctxt -> Name
-> Maybe NameOutput
-> Maybe [Char]
-> Maybe [Char]
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
TypeOutput) Maybe [Char]
docs Maybe [Char]
ty
       _ | Name -> IState -> Bool
isMetavarName   Name
n IState
ist  -> if Bool
meta
                                       then Name
-> Maybe NameOutput
-> Maybe [Char]
-> Maybe [Char]
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
MetavarOutput) Maybe [Char]
docs Maybe [Char]
ty
                                       else Name
-> Maybe NameOutput
-> Maybe [Char]
-> Maybe [Char]
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
FunOutput) Maybe [Char]
docs Maybe [Char]
ty
       _ | Name -> IState -> Bool
isPostulateName Name
n IState
ist  -> Name
-> Maybe NameOutput
-> Maybe [Char]
-> Maybe [Char]
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
PostulateOutput) Maybe [Char]
docs Maybe [Char]
ty
       _ | Bool
otherwise              -> OutputAnnotation
annot
  where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs
        docOverview :: IState -> Name -> Maybe [Char]
docOverview ist :: IState
ist n :: 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 :: [Char] -> [Char]
out  = SimpleDoc OutputAnnotation -> [Char] -> [Char]
forall a. SimpleDoc a -> [Char] -> [Char]
displayS (SimpleDoc OutputAnnotation -> [Char] -> [Char])
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> [Char]
-> [Char]
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 1.0 50 (Doc OutputAnnotation -> [Char] -> [Char])
-> Doc OutputAnnotation -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$
                                          (DocTerm -> [Char] -> Doc OutputAnnotation)
-> Docstring DocTerm -> Doc OutputAnnotation
forall a.
(a -> [Char] -> Doc OutputAnnotation)
-> Docstring a -> Doc OutputAnnotation
renderDocstring ((Term -> Doc OutputAnnotation)
-> (Term -> Term) -> DocTerm -> [Char] -> Doc OutputAnnotation
renderDocTerm (IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist)
                                                                         Term -> Term
norm) Docstring DocTerm
o
                               [Char] -> Maybe [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> [Char]
out "")
        getTy :: IState -> Name -> String -- fails if name not already extant!
        getTy :: IState -> Name -> [Char]
getTy ist :: IState
ist n :: 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 -> [Char] -> [Char]
forall a. SimpleDoc a -> [Char] -> [Char]
displayS (SimpleDoc OutputAnnotation -> [Char] -> [Char])
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> [Char]
-> [Char]
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 1.0 50 (Doc OutputAnnotation -> [Char] -> [Char])
-> Doc OutputAnnotation -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Doc OutputAnnotation
theTy) ""
fancifyAnnots _ _ annot :: OutputAnnotation
annot = OutputAnnotation
annot

showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc i :: IState
i [] = Doc OutputAnnotation
forall a. Doc a
empty
showSc i :: IState
i xs :: [(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
<> [Char] -> Doc OutputAnnotation
forall a. [Char] -> Doc a
text "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' bnd :: [(Name, Bool)]
bnd [] = []
           showSc' bnd :: [(Name, Bool)]
bnd ((n :: Name
n, ty :: Term
ty):ctxt :: [(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 -> [Char]
showqual i :: IState
i n :: Name
n = Maybe IState
-> [(Name, Bool)] -> PPOption -> Bool -> Name -> [Char]
showName (IState -> Maybe IState
forall a. a -> Maybe a
Just IState
i) [] (IState -> PPOption
ppOptionIst IState
i) { ppopt_impl :: Bool
ppopt_impl = Bool
False } Bool
False (Name -> Name
dens Name
n)
  where
    dens :: Name -> Name
dens ns :: Name
ns@(NS n :: Name
n _) = case Name -> Ctxt [PArg] -> [[PArg]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
                              [_] -> Name
n -- just one thing
                              _ -> Name
ns
    dens n :: Name
n = Name
n

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