{-# 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"
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
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
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
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]
-> [(Name, Type)]
-> Term
-> Bool
-> Bool
-> Bool
-> 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)"
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
= 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 :: [(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
errorIndent :: Int
errorIndent :: Int
errorIndent = 8
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
<>)
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))
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
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
<+>
[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
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
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)
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
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
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)
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
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) []
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
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
_ -> 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