{-# LANGUAGE CPP, PatternGuards #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module Idris.Delaborate (
annName, bugaddr, delab, delabWithEnv, delabDirect, delab', delabMV, delabSugared
, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab
, pprintDelabTy', pprintDelabTy, pprintErr, resugar
) where
import Idris.AbsSyntax
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Docstrings (overview, renderDocTerm, renderDocstring)
import Idris.ErrReverse
import Util.Pretty
#if (MIN_VERSION_base(4,11,0))
import Prelude hiding ((<$>), (<>))
#else
import Prelude hiding ((<$>))
#endif
import Control.Applicative (Alternative((<|>)))
import Control.Monad.State
import Data.Generics.Uniplate.Data (transform)
import Data.List (nub)
import Data.Maybe (mapMaybe)
import qualified Data.Text as T
bugaddr :: String
bugaddr = String
"https://github.com/idris-lang/Idris-dev/issues"
resugar :: IState -> PTerm -> PTerm
resugar :: IState -> PTerm -> PTerm
resugar IState
ist = (PTerm -> PTerm) -> PTerm -> PTerm
forall on. Uniplate on => (on -> on) -> on -> on
transform PTerm -> PTerm
flattenDoLet (PTerm -> PTerm) -> (PTerm -> PTerm) -> PTerm -> PTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PTerm -> PTerm) -> PTerm -> PTerm
forall on. Uniplate on => (on -> on) -> on -> on
transform PTerm -> PTerm
resugarApp
where
resugarApp :: PTerm -> PTerm
resugarApp (PApp FC
fc (PRef FC
_ [FC]
_ Name
n) [PArg]
args)
| [PTerm
c, PTerm
t, PTerm
f] <- (PArg -> Maybe PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PArg -> Maybe PTerm
forall {a}. PArg' a -> Maybe a
explicitTerm [PArg]
args
, Name -> Name
basename Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"ifThenElse"
= FC -> PTerm -> PTerm -> PTerm -> PTerm
PIfThenElse FC
fc PTerm
c (PTerm -> PTerm
dedelay PTerm
t) (PTerm -> PTerm
dedelay PTerm
f)
resugarApp (PApp FC
fc (PRef FC
_ [FC]
_ Name
n) [PArg]
args)
| [PTerm
v, PLam FC
_ Name
bn FC
_ PTerm
_ PTerm
next] <- (PArg -> Maybe PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PArg -> Maybe PTerm
forall {a}. PArg' a -> Maybe a
explicitTerm [PArg]
args
, Name -> Name
basename Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
">>="
= let step :: PDo' PTerm
step = if Name
bn Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Name, PTerm)] -> IState -> PTerm -> [Name]
namesIn [] IState
ist PTerm
next
then FC -> Name -> FC -> PTerm -> PDo' PTerm
forall t. FC -> Name -> FC -> t -> PDo' t
DoBind FC
fc Name
bn FC
NoFC PTerm
v
else FC -> PTerm -> PDo' PTerm
forall t. FC -> t -> PDo' t
DoExp FC
NoFC PTerm
v
in case PTerm -> PTerm
resugarApp PTerm
next of
PDoBlock [PDo' PTerm]
dos -> [PDo' PTerm] -> PTerm
PDoBlock (PDo' PTerm
step PDo' PTerm -> [PDo' PTerm] -> [PDo' PTerm]
forall a. a -> [a] -> [a]
: [PDo' PTerm]
dos)
PTerm
expr -> [PDo' PTerm] -> PTerm
PDoBlock [PDo' PTerm
step, FC -> PTerm -> PDo' PTerm
forall t. FC -> t -> PDo' t
DoExp FC
NoFC PTerm
expr]
resugarApp (PApp FC
fc (PRef FC
_ [FC]
_ Name
n) [PArg]
args)
| [PConstant FC
fc (BI Integer
i)] <- (PArg -> Maybe PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PArg -> Maybe PTerm
forall {a}. PArg' a -> Maybe a
explicitTerm [PArg]
args
, Name -> Name
basename Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"fromInteger"
= FC -> Const -> PTerm
PConstant FC
fc (Integer -> Const
BI Integer
i)
resugarApp PTerm
tm = PTerm
tm
flattenDoLet :: PTerm -> PTerm
flattenDoLet (PLet FC
_ RigCount
rc Name
ln FC
_ PTerm
ty PTerm
v PTerm
bdy)
| PDoBlock [PDo' PTerm]
dos <- PTerm -> PTerm
flattenDoLet PTerm
bdy
= [PDo' PTerm] -> PTerm
PDoBlock (FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PDo' PTerm
forall t. FC -> RigCount -> Name -> FC -> t -> t -> PDo' t
DoLet FC
NoFC RigCount
rc Name
ln FC
NoFC PTerm
ty PTerm
v PDo' PTerm -> [PDo' PTerm] -> [PDo' PTerm]
forall a. a -> [a] -> [a]
: [PDo' PTerm]
dos)
flattenDoLet (PDoBlock [PDo' PTerm]
dos) =
[PDo' PTerm] -> PTerm
PDoBlock ([PDo' PTerm] -> PTerm) -> [PDo' PTerm] -> PTerm
forall a b. (a -> b) -> a -> b
$ (PDo' PTerm -> [PDo' PTerm]) -> [PDo' PTerm] -> [PDo' PTerm]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDo' PTerm -> [PDo' PTerm]
fixExp [PDo' PTerm]
dos
where fixExp :: PDo' PTerm -> [PDo' PTerm]
fixExp (DoExp FC
_ (PLet FC
_ RigCount
rc Name
ln FC
_ PTerm
ty PTerm
v PTerm
bdy)) =
FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PDo' PTerm
forall t. FC -> RigCount -> Name -> FC -> t -> t -> PDo' t
DoLet FC
NoFC RigCount
rc Name
ln FC
NoFC PTerm
ty PTerm
v PDo' PTerm -> [PDo' PTerm] -> [PDo' PTerm]
forall a. a -> [a] -> [a]
: PDo' PTerm -> [PDo' PTerm]
fixExp (FC -> PTerm -> PDo' PTerm
forall t. FC -> t -> PDo' t
DoExp FC
NoFC PTerm
bdy)
fixExp PDo' PTerm
d = [PDo' PTerm
d]
flattenDoLet PTerm
tm = PTerm
tm
dedelay :: PTerm -> PTerm
dedelay (PApp FC
_ (PRef FC
_ [FC]
_ Name
delay) [PArg
_, PArg
_, PArg
obj])
| Name
delay Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"Delay" = PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
obj
dedelay PTerm
x = PTerm
x
explicitTerm :: PArg' a -> Maybe a
explicitTerm (PExp {getTm :: forall t. PArg' t -> t
getTm = a
tm}) = a -> Maybe a
forall a. a -> Maybe a
Just a
tm
explicitTerm PArg' a
_ = Maybe a
forall a. Maybe a
Nothing
delabSugared :: IState -> Term -> PTerm
delabSugared :: IState -> Term -> PTerm
delabSugared IState
ist Term
tm = IState -> PTerm -> PTerm
resugar IState
ist (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ IState -> Term -> PTerm
delab IState
ist Term
tm
delab :: IState -> Term -> PTerm
delab :: IState -> Term -> PTerm
delab IState
i Term
tm = IState -> Term -> Bool -> Bool -> PTerm
delab' IState
i Term
tm Bool
False Bool
False
delabWithEnv :: IState -> [(Name, Type)] -> Term -> PTerm
delabWithEnv :: IState -> [(Name, Term)] -> Term -> PTerm
delabWithEnv IState
i [(Name, Term)]
tys Term
tm = IState -> [(Name, Term)] -> Term -> Bool -> Bool -> PTerm
delabWithEnv' IState
i [(Name, Term)]
tys Term
tm Bool
False Bool
False
delabMV :: IState -> Term -> PTerm
delabMV :: IState -> Term -> PTerm
delabMV IState
i Term
tm = IState -> Term -> Bool -> Bool -> PTerm
delab' IState
i Term
tm Bool
False Bool
True
delabDirect :: IState -> Term -> PTerm
delabDirect :: IState -> Term -> PTerm
delabDirect IState
i Term
tm = IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [] [] Term
tm Bool
False Bool
False Bool
False
delabTy :: IState -> Name -> PTerm
delabTy :: IState -> Name -> PTerm
delabTy IState
i Name
n
= case Name -> Context -> [Term]
lookupTy Name
n (IState -> Context
tt_ctxt IState
i) of
(Term
ty:[Term]
_) -> case Name -> Ctxt [PArg] -> [[PArg]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
([PArg]
imps:[[PArg]]
_) -> IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [PArg]
imps [] Term
ty Bool
False Bool
False Bool
True
[[PArg]]
_ -> IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [] [] Term
ty Bool
False Bool
False Bool
True
[] -> String -> PTerm
forall a. HasCallStack => String -> a
error String
"delabTy: got non-existing name"
delab' :: IState -> Term -> Bool -> Bool -> PTerm
delab' :: IState -> Term -> Bool -> Bool -> PTerm
delab' IState
i Term
t Bool
f Bool
mvs = IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [] [] Term
t Bool
f Bool
mvs Bool
True
delabWithEnv' :: IState -> [(Name, Type)] -> Term -> Bool -> Bool -> PTerm
delabWithEnv' :: IState -> [(Name, Term)] -> Term -> Bool -> Bool -> PTerm
delabWithEnv' IState
i [(Name, Term)]
tys Term
t Bool
f Bool
mvs = IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [] [(Name, Term)]
tys Term
t Bool
f Bool
mvs Bool
True
delabTy' :: IState -> [PArg]
-> [(Name, Type)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' :: IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
ist [PArg]
imps [(Name, Term)]
genv Term
tm Bool
fullname Bool
mvs Bool
docases = [(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
genv [] [PArg]
imps Term
tm
where
un :: FC
un = String -> FC
fileFC String
"(val)"
de :: [(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
imps Term
sc
| Bool
docases
, Term -> Bool
isCaseApp Term
sc
, (P NameType
_ Name
cOp Term
_, args :: [Term]
args@(Term
_:[Term]
_)) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
sc
, Just PTerm
caseblock <- [(Name, Term)]
-> [(Name, Name)]
-> [PArg]
-> Term
-> Name
-> [Term]
-> Maybe PTerm
delabCase [(Name, Term)]
tys [(Name, Name)]
env [PArg]
imps ([Term] -> Term
forall a. HasCallStack => [a] -> a
last [Term]
args) Name
cOp [Term]
args
= PTerm
caseblock
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (App AppStatus Name
_ Term
f Term
a) = [(Name, Term)] -> [(Name, Name)] -> Term -> [Term] -> PTerm
deFn [(Name, Term)]
tys [(Name, Name)]
env Term
f [Term
a]
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (V Int
i) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [(Name, Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Name)]
env = FC -> [FC] -> Name -> PTerm
PRef FC
un [] ((Name, Name) -> Name
forall a b. (a, b) -> b
snd ([(Name, Name)]
env[(Name, Name)] -> Int -> (Name, Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
i))
| Bool
otherwise = FC -> [FC] -> Name -> PTerm
PRef FC
un [] (String -> Name
sUN (String
"v" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
""))
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (P NameType
_ Name
n Term
_) | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
unitTy = FC -> PunInfo -> PTerm
PTrue FC
un PunInfo
IsType
| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
unitCon = FC -> PunInfo -> PTerm
PTrue FC
un PunInfo
IsTerm
| Just Name
n' <- Name -> [(Name, Name)] -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Name)]
env = FC -> [FC] -> Name -> PTerm
PRef FC
un [] Name
n'
| Bool
otherwise
= case Name
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> Maybe (Maybe Name, Int, [Name], Bool, Bool)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist) of
Just (Just Name
_, Int
mi, [Name]
_, Bool
_, Bool
_) -> Name -> [PTerm] -> PTerm
mkMVApp Name
n []
Maybe (Maybe Name, Int, [Name], Bool, Bool)
_ -> FC -> [FC] -> Name -> PTerm
PRef FC
un [] Name
n
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (Bind Name
n (Lam RigCount
_ Term
ty) Term
sc)
= FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
un Name
n FC
NoFC ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [] Term
sc)
de [(Name, Term)]
tys [(Name, Name)]
env (PArg
_ : [PArg]
is) (Bind Name
n (Pi RigCount
rig (Just ImplicitInfo
impl) Term
ty Term
_) Term
sc)
| ImplicitInfo -> Bool
toplevel_imp ImplicitInfo
impl
= Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ([ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [] Static
Dynamic Bool
False (ImplicitInfo -> Maybe ImplicitInfo
forall a. a -> Maybe a
Just ImplicitInfo
impl) Bool
False RigCount
rig) Name
n FC
NoFC
([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [PArg]
is Term
sc)
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
is (Bind Name
n (Pi RigCount
rig (Just ImplicitInfo
impl) Term
ty Term
_) Term
sc)
| ImplicitInfo -> Bool
tcimplementation ImplicitInfo
impl
= Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
constraint Name
n FC
NoFC ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty)
([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [PArg]
is Term
sc)
| Bool
otherwise
= Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ([ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [] Static
Dynamic Bool
False (ImplicitInfo -> Maybe ImplicitInfo
forall a. a -> Maybe a
Just ImplicitInfo
impl) Bool
False RigCount
rig) Name
n FC
NoFC ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [PArg]
is Term
sc)
de [(Name, Term)]
tys [(Name, Name)]
env ((PImp { argopts :: forall t. PArg' t -> [ArgOpt]
argopts = [ArgOpt]
opts }):[PArg]
is) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc)
= Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ([ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [ArgOpt]
opts Static
Dynamic Bool
False Maybe ImplicitInfo
forall a. Maybe a
Nothing Bool
False RigCount
rig) Name
n FC
NoFC
([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [PArg]
is Term
sc)
de [(Name, Term)]
tys [(Name, Name)]
env (PConstraint Int
_ [ArgOpt]
_ Name
_ PTerm
_:[PArg]
is) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc)
= Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
constraint { pcount = rig}) Name
n FC
NoFC
([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [PArg]
is Term
sc)
de [(Name, Term)]
tys [(Name, Name)]
env (PTacImplicit Int
_ [ArgOpt]
_ Name
_ PTerm
tac PTerm
_:[PArg]
is) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc)
= Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ((PTerm -> Plicity
tacimpl PTerm
tac) { pcount = rig }) Name
n FC
NoFC
([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [PArg]
is Term
sc)
de [(Name, Term)]
tys [(Name, Name)]
env (PArg
plic:[PArg]
is) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc)
= Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity
Exp (PArg -> [ArgOpt]
forall t. PArg' t -> [ArgOpt]
argopts PArg
plic) Static
Dynamic Bool
False RigCount
rig)
Name
n FC
NoFC
([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty)
([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [PArg]
is Term
sc)
de [(Name, Term)]
tys [(Name, Name)]
env [] (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc)
= Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
expl { pcount = rig }) Name
n FC
NoFC ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty)
([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [] Term
sc)
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
imps (Bind Name
n (Let RigCount
rc Term
ty Term
val) Term
sc)
| Bool
docases
, Term -> Bool
isCaseApp Term
sc
, (P NameType
_ Name
cOp Term
_, [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
sc
, Just PTerm
caseblock <- [(Name, Term)]
-> [(Name, Name)]
-> [PArg]
-> Term
-> Name
-> [Term]
-> Maybe PTerm
delabCase [(Name, Term)]
tys [(Name, Name)]
env [PArg]
imps Term
val Name
cOp [Term]
args = PTerm
caseblock
| Bool
otherwise =
FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
un RigCount
rc Name
n FC
NoFC ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty)
([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
val) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [] Term
sc)
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (Bind Name
n (Hole Term
ty) Term
sc) = [(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n, String -> Name
sUN String
"[__]")(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [] Term
sc
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (Bind Name
n (Guess Term
ty Term
val) Term
sc) = [(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Term
ty) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n, String -> Name
sUN String
"[__]")(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [] Term
sc
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
plic (Bind Name
n Binder Term
bb Term
sc) = [(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de ((Name
n, Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
bb) (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)]
tys) ((Name
n,Name
n)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [] Term
sc
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (Constant Const
i) = FC -> Const -> PTerm
PConstant FC
NoFC Const
i
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (Proj Term
_ Int
_) = String -> PTerm
forall a. HasCallStack => String -> a
error String
"Delaboration got run-time-only Proj!"
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ Term
Erased = PTerm
Placeholder
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ Term
Impossible = PTerm
Placeholder
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (Inferred Term
t) = PTerm
Placeholder
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (TType UExp
i) = FC -> PTerm
PType FC
un
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
_ (UType Universe
u) = FC -> Universe -> PTerm
PUniverse FC
un Universe
u
deFn :: [(Name, Term)] -> [(Name, Name)] -> Term -> [Term] -> PTerm
deFn [(Name, Term)]
tys [(Name, Name)]
env (App AppStatus Name
_ Term
f Term
a) [Term]
args = [(Name, Term)] -> [(Name, Name)] -> Term -> [Term] -> PTerm
deFn [(Name, Term)]
tys [(Name, Name)]
env Term
f (Term
aTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
args)
deFn [(Name, Term)]
tys [(Name, Name)]
env (P NameType
_ Name
n Term
_) [Term
l,Term
r]
| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
pairTy = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
un [] PunInfo
IsType ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
l) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
r)
deFn [(Name, Term)]
tys [(Name, Name)]
env (P NameType
_ Name
n Term
_) [Term
ty, Bind Name
x (Lam RigCount
_ Term
_) Term
r]
| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
sigmaTy
= FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
un [] PunInfo
IsType (FC -> [FC] -> Name -> PTerm
PRef FC
un [] Name
x) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
ty)
([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys ((Name
x,Name
x)(Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
:[(Name, Name)]
env) [] (Term -> Term -> Term
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
ty) Term
r))
deFn [(Name, Term)]
tys [(Name, Name)]
env (P NameType
_ Name
n Term
_) [Term
lt,Term
rt,Term
l,Term
r]
| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
pairCon = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
un [] PunInfo
IsTerm ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
l) ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
r)
| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
sigmaCon = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
un [] PunInfo
IsTerm ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
l) PTerm
Placeholder
([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
r)
deFn [(Name, Term)]
tys [(Name, Name)]
env (P NameType
_ Name
n Term
_) [Term]
args
| Bool -> Bool
not Bool
mvs = case Name
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> Maybe (Maybe Name, Int, [Name], Bool, Bool)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist) of
Just (Just Name
_, Int
mi, [Name]
_, Bool
_, Bool
_) ->
Name -> [PTerm] -> PTerm
mkMVApp Name
n (Int -> [PTerm] -> [PTerm]
forall a. Int -> [a] -> [a]
drop Int
mi ((Term -> PTerm) -> [Term] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env []) [Term]
args))
Maybe (Maybe Name, Int, [Name], Bool, Bool)
_ -> [(Name, Term)] -> Name -> [PTerm] -> PTerm
mkPApp [(Name, Term)]
tys Name
n ((Term -> PTerm) -> [Term] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env []) [Term]
args)
| Bool
otherwise = [(Name, Term)] -> Name -> [PTerm] -> PTerm
mkPApp [(Name, Term)]
tys Name
n ((Term -> PTerm) -> [Term] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env []) [Term]
args)
deFn [(Name, Term)]
tys [(Name, Name)]
env (V Int
i) [Term]
args
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [(Name, Name)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Name)]
env = [(Name, Term)] -> Name -> [PTerm] -> PTerm
mkPApp [(Name, Term)]
tys ((Name, Name) -> Name
forall a b. (a, b) -> a
fst ([(Name, Name)]
env[(Name, Name)] -> Int -> (Name, Name)
forall a. HasCallStack => [a] -> Int -> a
!!Int
i)) ((Term -> PTerm) -> [Term] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env []) [Term]
args)
deFn [(Name, Term)]
tys [(Name, Name)]
env Term
f [Term]
args = FC -> PTerm -> [PArg] -> PTerm
PApp FC
un ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [] Term
f) ((PTerm -> PArg) -> [PTerm] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PArg
forall {t}. t -> PArg' t
pexp ((Term -> PTerm) -> [Term] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env []) [Term]
args))
mkMVApp :: Name -> [PTerm] -> PTerm
mkMVApp Name
n []
= FC -> Name -> PTerm
PMetavar FC
NoFC Name
n
mkMVApp Name
n [PTerm]
args
= FC -> PTerm -> [PArg] -> PTerm
PApp FC
un (FC -> Name -> PTerm
PMetavar FC
NoFC Name
n) ((PTerm -> PArg) -> [PTerm] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PArg
forall {t}. t -> PArg' t
pexp [PTerm]
args)
mkPApp :: [(Name, Term)] -> Name -> [PTerm] -> PTerm
mkPApp [(Name, Term)]
tys Name
n [PTerm]
args
| Just Term
ty <- Name -> [(Name, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Term)]
tys
= let imps :: [PArg]
imps = Term -> [PArg]
findImp Term
ty in
FC -> PTerm -> [PArg] -> PTerm
PApp FC
un (FC -> [FC] -> Name -> PTerm
PRef FC
un [] Name
n) ((PArg -> PTerm -> PArg) -> [PArg] -> [PTerm] -> [PArg]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith PArg -> PTerm -> PArg
forall {t}. PArg' t -> t -> PArg' t
imp ([PArg]
imps [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++ PArg -> [PArg]
forall a. a -> [a]
repeat (PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
forall a. HasCallStack => a
undefined)) [PTerm]
args)
| Just [PArg]
imps <- Name -> Ctxt [PArg] -> Maybe [PArg]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [PArg]
idris_implicits IState
ist)
= FC -> PTerm -> [PArg] -> PTerm
PApp FC
un (FC -> [FC] -> Name -> PTerm
PRef FC
un [] Name
n) ((PArg -> PTerm -> PArg) -> [PArg] -> [PTerm] -> [PArg]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith PArg -> PTerm -> PArg
forall {t}. PArg' t -> t -> PArg' t
imp ([PArg]
imps [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++ PArg -> [PArg]
forall a. a -> [a]
repeat (PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
forall a. HasCallStack => a
undefined)) [PTerm]
args)
| Bool
otherwise = FC -> PTerm -> [PArg] -> PTerm
PApp FC
un (FC -> [FC] -> Name -> PTerm
PRef FC
un [] Name
n) ((PTerm -> PArg) -> [PTerm] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PArg
forall {t}. t -> PArg' t
pexp [PTerm]
args)
where
findImp :: Term -> [PArg]
findImp (Bind Name
n (Pi RigCount
_ im :: Maybe ImplicitInfo
im@(Just ImplicitInfo
i) Term
_ Term
_) Term
sc)
= Name -> PTerm -> Bool -> PArg
forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n PTerm
Placeholder Bool
True PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: Term -> [PArg]
findImp Term
sc
findImp (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Term
_ Term
_) Term
sc)
= PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
Placeholder PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: Term -> [PArg]
findImp Term
sc
findImp Term
_ = []
imp :: PArg' t -> t -> PArg' t
imp (PImp Int
p Bool
m [ArgOpt]
l Name
n t
_) t
arg = Int -> Bool -> [ArgOpt] -> Name -> t -> PArg' t
forall t. Int -> Bool -> [ArgOpt] -> Name -> t -> PArg' t
PImp Int
p Bool
m [ArgOpt]
l Name
n t
arg
imp (PExp Int
p [ArgOpt]
l Name
n t
_) t
arg = Int -> [ArgOpt] -> Name -> t -> PArg' t
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp Int
p [ArgOpt]
l Name
n t
arg
imp (PConstraint Int
p [ArgOpt]
l Name
n t
_) t
arg = Int -> [ArgOpt] -> Name -> t -> PArg' t
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PConstraint Int
p [ArgOpt]
l Name
n t
arg
imp (PTacImplicit Int
p [ArgOpt]
l Name
n t
sc t
_) t
arg = Int -> [ArgOpt] -> Name -> t -> t -> PArg' t
forall t. Int -> [ArgOpt] -> Name -> t -> t -> PArg' t
PTacImplicit Int
p [ArgOpt]
l Name
n t
sc t
arg
isCaseApp :: Term -> Bool
isCaseApp Term
tm | P NameType
_ Name
n Term
_ <- (Term, [Term]) -> Term
forall a b. (a, b) -> a
fst (Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm) = Name -> Bool
isCN Name
n
| Bool
otherwise = Bool
False
where isCN :: Name -> Bool
isCN (NS Name
n [Text]
_) = Name -> Bool
isCN Name
n
isCN (SN (CaseN FC'
_ Name
_)) = Bool
True
isCN Name
_ = Bool
False
delabCase :: [(Name, Type)] -> [(Name, Name)] -> [PArg] -> Term -> Name -> [Term] -> Maybe PTerm
delabCase :: [(Name, Term)]
-> [(Name, Name)]
-> [PArg]
-> Term
-> Name
-> [Term]
-> Maybe PTerm
delabCase [(Name, Term)]
tys [(Name, Name)]
env [PArg]
imps Term
scrutinee Name
caseName [Term]
caseArgs =
do [([(Name, Term)], Term, Term)]
cases <- case Name
-> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
-> [([([(Name, Term)], Term, Term)], [PTerm])]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
caseName (IState -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs IState
ist) of
[([([(Name, Term)], Term, Term)]
cases, [PTerm]
_)] -> [([(Name, Term)], Term, Term)]
-> Maybe [([(Name, Term)], Term, Term)]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [([(Name, Term)], Term, Term)]
cases
[([([(Name, Term)], Term, Term)], [PTerm])]
_ -> Maybe [([(Name, Term)], Term, Term)]
forall a. Maybe a
Nothing
PTerm -> Maybe PTerm
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> Maybe PTerm) -> PTerm -> Maybe PTerm
forall a b. (a -> b) -> a -> b
$ FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
un ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys [(Name, Name)]
env [PArg]
imps Term
scrutinee)
[ ([(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys ([(Name, Name)]
env [(Name, Name)] -> [(Name, Name)] -> [(Name, Name)]
forall a. [a] -> [a] -> [a]
++ ((Name, Term) -> (Name, Name)) -> [(Name, Term)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, Term
_) -> (Name
n, Name
n)) [(Name, Term)]
vars) [PArg]
imps (Term -> Term
forall {n}. TT n -> TT n
splitArg Term
lhs),
[(Name, Term)] -> [(Name, Name)] -> [PArg] -> Term -> PTerm
de [(Name, Term)]
tys ([(Name, Name)]
env [(Name, Name)] -> [(Name, Name)] -> [(Name, Name)]
forall a. [a] -> [a] -> [a]
++ ((Name, Term) -> (Name, Name)) -> [(Name, Term)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, Term
_) -> (Name
n, Name
n)) [(Name, Term)]
vars) [PArg]
imps Term
rhs)
| ([(Name, Term)]
vars, Term
lhs, Term
rhs) <- [([(Name, Term)], Term, Term)]
cases
]
where splitArg :: TT n -> TT n
splitArg TT n
tm | (TT n
_, [TT n]
args) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
tm = [TT n] -> TT n
forall {n}. [TT n] -> TT n
nonVar ([TT n] -> [TT n]
forall a. [a] -> [a]
reverse [TT n]
args)
| Bool
otherwise = TT n
tm
nonVar :: [TT n] -> TT n
nonVar [] = String -> TT n
forall a. HasCallStack => String -> a
error String
"Tried to delaborate empty case list"
nonVar [TT n
x] = TT n
x
nonVar (x :: TT n
x@(App AppStatus n
_ TT n
_ TT n
_) : [TT n]
_) = TT n
x
nonVar (x :: TT n
x@(P (DCon Int
_ Int
_ Bool
_) n
_ TT n
_) : [TT n]
_) = TT n
x
nonVar (TT n
x:[TT n]
xs) = [TT n] -> TT n
nonVar [TT n]
xs
errorIndent :: Int
errorIndent :: Int
errorIndent = Int
8
indented :: Doc a -> Doc a
indented :: forall a. Doc a -> Doc a
indented = Int -> Doc a -> Doc a
forall a. Int -> Doc a -> Doc a
nest Int
errorIndent (Doc a -> Doc a) -> (Doc a -> Doc a) -> Doc a -> Doc a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc a
forall a. Doc a
line Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<>)
pprintDelab :: IState -> Term -> Doc OutputAnnotation
pprintDelab :: IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist Term
tm = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm [] Term
tm)
(IState -> PTerm -> Doc OutputAnnotation
prettyIst IState
ist (IState -> Term -> PTerm
delabSugared IState
ist Term
tm))
pprintNoDelab :: IState -> Term -> Doc OutputAnnotation
pprintNoDelab :: IState -> Term -> Doc OutputAnnotation
pprintNoDelab IState
ist Term
tm = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm [] Term
tm)
(IState -> PTerm -> Doc OutputAnnotation
prettyIst IState
ist (IState -> Term -> PTerm
delab IState
ist Term
tm))
pprintDelabTy' :: IState -> Name -> Term -> Doc OutputAnnotation
pprintDelabTy' :: IState -> Name -> Term -> Doc OutputAnnotation
pprintDelabTy' IState
i Name
n Term
ty
= OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm [] Term
ty) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (PTerm -> Doc OutputAnnotation) -> PTerm -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IState -> PTerm -> Doc OutputAnnotation
prettyIst IState
i (PTerm -> Doc OutputAnnotation) -> PTerm -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$
case Name -> Ctxt [PArg] -> [[PArg]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
([PArg]
imps:[[PArg]]
_) -> IState -> PTerm -> PTerm
resugar IState
i (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [PArg]
imps [] Term
ty Bool
False Bool
False Bool
True
[[PArg]]
_ -> IState -> PTerm -> PTerm
resugar IState
i (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ IState
-> [PArg]
-> [(Name, Term)]
-> Term
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
i [] [] Term
ty Bool
False Bool
False Bool
True
pprintDelabTy :: IState -> Name -> Doc OutputAnnotation
pprintDelabTy :: IState -> Name -> Doc OutputAnnotation
pprintDelabTy IState
i Name
n
= case Name -> Context -> [Term]
lookupTy Name
n (IState -> Context
tt_ctxt IState
i) of
(Term
ty:[Term]
_) -> IState -> Name -> Term -> Doc OutputAnnotation
pprintDelabTy' IState
i Name
n Term
ty
[] -> String -> Doc OutputAnnotation
forall a. HasCallStack => String -> a
error String
"pprintDelabTy got a name that doesn't exist"
pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
ist = IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
ist []
pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
ist [(Name, Bool)]
bnd PTerm
tm = PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm (IState -> PPOption
ppOptionIst IState
ist) [(Name, Bool)]
bnd [] (IState -> [FixDecl]
idris_infixes IState
ist) PTerm
tm
pprintProv :: IState -> [(Name, Term)] -> Provenance -> Doc OutputAnnotation
pprintProv :: IState -> [(Name, Term)] -> Provenance -> Doc OutputAnnotation
pprintProv IState
i [(Name, Term)]
e Provenance
ExpectedType = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Expected type"
pprintProv IState
i [(Name, Term)]
e Provenance
InferredVal = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Inferred value"
pprintProv IState
i [(Name, Term)]
e Provenance
GivenVal = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Given value"
pprintProv IState
i [(Name, Term)]
e (SourceTerm Term
tm)
= String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Type of " Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm ([Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
e) (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)) Term
tm)
(IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i ([Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
e) (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)) (IState -> Term -> PTerm
delabSugared IState
i Term
tm))
pprintProv IState
i [(Name, Term)]
e (TooManyArgs Term
tm)
= String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Is " Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm ([Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
e) (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)) Term
tm)
(IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i ([Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
e) (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)) (IState -> Term -> PTerm
delabSugared IState
i Term
tm))
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
" applied to too many arguments?"
pprintErr :: IState -> Err -> Doc OutputAnnotation
pprintErr :: IState -> Err -> Doc OutputAnnotation
pprintErr IState
i Err
err = IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i ((Term -> Term) -> Err -> Err
forall a b. (a -> b) -> Err' a -> Err' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Term -> Term
errReverse IState
i) Err
err)
pprintErr' :: IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i (Msg String
s) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
s
pprintErr' IState
i (InternalMsg String
s) =
[Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep [ String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"INTERNAL ERROR:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
s,
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"This is probably a bug, or a missing error message.",
String -> Doc OutputAnnotation
forall a. String -> Doc a
text (String
"Please consider reporting at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bugaddr)
]
pprintErr' IState
i (CantUnify Bool
_ (Term
x_in, Maybe Provenance
xprov) (Term
y_in, Maybe Provenance
yprov) Err
e [(Name, Term)]
sc Int
s) =
let (Term
x_ns, Term
y_ns, [Name]
nms) = Term -> Term -> (Term, Term, [Name])
renameMNs Term
x_in Term
y_in
(PTerm
x, PTerm
y) = PTerm -> PTerm -> (PTerm, PTerm)
addImplicitDiffs (IState -> Term -> PTerm
delabSugared IState
i Term
x_ns) (IState -> Term -> PTerm
delabSugared IState
i Term
y_ns) in
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Type mismatch between" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
x_ns
(IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i (((Name, Term) -> (Name, Bool)) -> [(Name, Term)] -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
b) -> (Name
n, Bool
False)) [(Name, Term)]
sc
[(Name, Bool)] -> [(Name, Bool)] -> [(Name, Bool)]
forall a. [a] -> [a] -> [a]
++ [Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
nms (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)) PTerm
x))
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> case Maybe Provenance
xprov of
Maybe Provenance
Nothing -> Doc OutputAnnotation
forall a. Doc a
empty
Just Provenance
t -> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
" (" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> [(Name, Term)] -> Provenance -> Doc OutputAnnotation
pprintProv IState
i [(Name, Term)]
sc Provenance
t Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
")"
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"and" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
y_ns
(IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i (((Name, Term) -> (Name, Bool)) -> [(Name, Term)] -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
b) -> (Name
n, Bool
False)) [(Name, Term)]
sc
[(Name, Bool)] -> [(Name, Bool)] -> [(Name, Bool)]
forall a. [a] -> [a] -> [a]
++ [Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
nms (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)) PTerm
y))
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> case Maybe Provenance
yprov of
Maybe Provenance
Nothing -> Doc OutputAnnotation
forall a. Doc a
empty
Just Provenance
t -> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
" (" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> [(Name, Term)] -> Provenance -> Doc OutputAnnotation
pprintProv IState
i [(Name, Term)]
sc Provenance
t Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
")"
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
case Err
e of
Msg String
"" -> Doc OutputAnnotation
forall a. Doc a
empty
CantUnify Bool
_ (Term
x_in', Maybe Provenance
_) (Term
y_in',Maybe Provenance
_) Err
_ [(Name, Term)]
_ Int
_ | Term
x_in Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
x_in' Bool -> Bool -> Bool
&& Term
y_in Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
y_in' -> Doc OutputAnnotation
forall a. Doc a
empty
Err
_ -> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Specifically:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
if (IOption -> Bool
opt_errContext (IState -> IOption
idris_options IState
i))
then String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Unification failure" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc IState
i [(Name, Term)]
sc
else Doc OutputAnnotation
forall a. Doc a
empty
pprintErr' IState
i (CantConvert Term
x_in Term
y_in [(Name, Term)]
env) =
let (Term
x_ns, Term
y_ns, [Name]
_) = Term -> Term -> (Term, Term, [Name])
renameMNs Term
x_in Term
y_in
(PTerm
x, PTerm
y) = PTerm -> PTerm -> (PTerm, PTerm)
addImplicitDiffs (IState -> Term -> PTerm
delabSugared IState
i (Term -> Term
flagUnique Term
x_ns))
(IState -> Term -> PTerm
delabSugared IState
i (Term -> Term
flagUnique Term
y_ns)) in
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Type mismatch between" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
x_ns (IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i (((Name, Term) -> (Name, Bool)) -> [(Name, Term)] -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
b) -> (Name
n, Bool
False)) [(Name, Term)]
env)
PTerm
x)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"and" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
y_ns (IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i (((Name, Term) -> (Name, Bool)) -> [(Name, Term)] -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
b) -> (Name
n, Bool
False)) [(Name, Term)]
env)
PTerm
y)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
if (IOption -> Bool
opt_errContext (IState -> IOption
idris_options IState
i)) then Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Conversion failure" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc IState
i [(Name, Term)]
env else Doc OutputAnnotation
forall a. Doc a
empty
where flagUnique :: Term -> Term
flagUnique (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
i Term
t k :: Term
k@(UType Universe
u)) Term
sc)
= AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN (Universe -> String
forall a. Show a => a -> String
show Universe
u)) Term
forall n. TT n
Erased)
(Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i (Term -> Term
flagUnique Term
t) Term
k) (Term -> Term
flagUnique Term
sc))
flagUnique (App AppStatus Name
s Term
f Term
a) = AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s (Term -> Term
flagUnique Term
f) (Term -> Term
flagUnique Term
a)
flagUnique (Bind Name
n Binder Term
b Term
sc) = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n ((Term -> Term) -> Binder Term -> Binder Term
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
flagUnique Binder Term
b) (Term -> Term
flagUnique Term
sc)
flagUnique Term
t = Term
t
pprintErr' IState
i (CantSolveGoal Term
x [(Name, Term)]
env) =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't find a value of type " Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
x (IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i (((Name, Term) -> (Name, Bool)) -> [(Name, Term)] -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
b) -> (Name
n, Bool
False)) [(Name, Term)]
env) (IState -> Term -> PTerm
delabSugared IState
i Term
x))) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
if (IOption -> Bool
opt_errContext (IState -> IOption
idris_options IState
i)) then Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc IState
i [(Name, Term)]
env else Doc OutputAnnotation
forall a. Doc a
empty
pprintErr' IState
i (UnifyScope Name
n Name
out Term
tm [(Name, Term)]
env) =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't unify" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Name -> Doc OutputAnnotation
annName Name
n) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"with" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
tm (IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i (((Name, Term) -> (Name, Bool)) -> [(Name, Term)] -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
b) -> (Name
n, Bool
False)) [(Name, Term)]
env) (IState -> Term -> PTerm
delabSugared IState
i Term
tm))) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"as" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Name -> Doc OutputAnnotation
annName Name
out) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"is not in scope" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
if (IOption -> Bool
opt_errContext (IState -> IOption
idris_options IState
i)) then Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc IState
i [(Name, Term)]
env else Doc OutputAnnotation
forall a. Doc a
empty
pprintErr' IState
i (CantInferType String
t) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't infer type for" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
t
pprintErr' IState
i (NonFunctionType Term
f Term
ty) =
Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
f (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
f)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"does not have a function type" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
parens (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
ty))
pprintErr' IState
i (NotEquality Term
tm Term
ty) =
Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
tm (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
tm)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"does not have an equality type" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
ty (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
parens (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
ty)))
pprintErr' IState
i (TooManyArguments Name
f) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Too many arguments for" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc OutputAnnotation
annName Name
f
pprintErr' IState
i (CantIntroduce Term
ty) =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't use lambda here: type is" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
ty (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
ty))
pprintErr' IState
i (InfiniteUnify Name
x Term
tm [(Name, Term)]
env) =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Unifying" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> String -> Doc OutputAnnotation
annName' Name
x (Name -> String
showbasic Name
x) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"and" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
tm (IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i (((Name, Term) -> (Name, Bool)) -> [(Name, Term)] -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
b) -> (Name
n, Bool
False)) [(Name, Term)]
env) (IState -> Term -> PTerm
delabSugared IState
i Term
tm)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"would lead to infinite value" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
if (IOption -> Bool
opt_errContext (IState -> IOption
idris_options IState
i)) then Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc IState
i [(Name, Term)]
env else Doc OutputAnnotation
forall a. Doc a
empty
pprintErr' IState
i (NotInjective Term
p Term
x Term
y) =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't verify injectivity of" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
p (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
p)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
" when unifying" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
x (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
x)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"and" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
y (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
y))
pprintErr' IState
i (CantResolve Bool
_ Term
c Err
e)
= String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't find implementation for" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
c)
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
case Err
e of
Msg String
"" -> Doc OutputAnnotation
forall a. Doc a
empty
Err
_ -> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Possible cause:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e)
pprintErr' IState
i (InvalidTCArg Name
n Term
t)
= Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
t (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
t)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
" cannot be a parameter of "
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Name -> Doc OutputAnnotation
annName Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"(Implementation arguments must be type or data constructors)"
pprintErr' IState
i (CantResolveAlts [Name]
as) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't disambiguate name:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
cat (Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. Doc a -> [Doc a] -> [Doc a]
punctuate (Doc OutputAnnotation
forall a. Doc a
comma Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
space) ((Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map ((OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
i Bool
True) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Name -> Doc OutputAnnotation) -> Name -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc OutputAnnotation
annName) [Name]
as)))
pprintErr' IState
i (NoValidAlts [Name]
as) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't disambiguate since no name has a suitable type:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
cat (Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. Doc a -> [Doc a] -> [Doc a]
punctuate (Doc OutputAnnotation
forall a. Doc a
comma Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
space) ((Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map ((OutputAnnotation -> OutputAnnotation)
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
i Bool
True) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (Name -> Doc OutputAnnotation) -> Name -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc OutputAnnotation
annName) [Name]
as))))
pprintErr' IState
i (NoTypeDecl Name
n) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"No type declaration for" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc OutputAnnotation
annName Name
n
pprintErr' IState
i (NoSuchVariable Name
n) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"No such variable" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc OutputAnnotation
annName Name
n
pprintErr' IState
i (WithFnType Term
ty) =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't match on a function: type is" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
ty (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
ty))
pprintErr' IState
i (CantMatch Term
t) =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't match on" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
t (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
t))
pprintErr' IState
i (IncompleteTerm Term
t)
= let missing :: [(Term, Name)]
missing = [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [] [] Term
t in
case [(Term, Name)]
missing of
[] -> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Incomplete term" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
t (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
t))
[(Term, Name)]
_ -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
cat (Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. Doc a -> [Doc a] -> [Doc a]
punctuate (Doc OutputAnnotation
forall a. Doc a
comma Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
space)
(((Term, Name) -> Doc OutputAnnotation)
-> [(Term, Name)] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (Term, Name) -> Doc OutputAnnotation
pprintIncomplete ([(Term, Name)] -> [(Term, Name)]
forall a. Eq a => [a] -> [a]
nub ([(Term, Name)] -> [(Term, Name)])
-> [(Term, Name)] -> [(Term, Name)]
forall a b. (a -> b) -> a -> b
$ [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [] [] Term
t))))
where
pprintIncomplete :: (Term, Name) -> Doc OutputAnnotation
pprintIncomplete (Term
tm, Name
arg)
| Name -> Bool
expname Name
arg
= String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't infer explicit argument to" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
tm (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
tm))
| Bool
otherwise
= String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't infer argument" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc OutputAnnotation
annName Name
arg Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"to" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
tm (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
tm))
expname :: Name -> Bool
expname (UN Text
n) = case Text -> String
str Text
n of
(Char
'_':String
_) -> Bool
True
String
_ -> Bool
False
expname (MN Int
_ Text
n) = case Text -> String
str Text
n of
(Char
'_':String
_) -> Bool
True
String
_ -> Bool
False
expname Name
_ = Bool
False
getMissing :: [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing :: [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs [Name]
env (Bind Name
n (Hole Term
ty) Term
sc)
= [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
hs) (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) Term
sc
getMissing [Name]
hs [Name]
env (Bind Name
n (Guess Term
_ Term
_) Term
sc)
= [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
hs) (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) Term
sc
getMissing [Name]
hs [Name]
env (Bind Name
n (Let RigCount
rc Term
t Term
v) Term
sc)
= [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs [Name]
env Term
t [(Term, Name)] -> [(Term, Name)] -> [(Term, Name)]
forall a. [a] -> [a] -> [a]
++
[Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs [Name]
env Term
v [(Term, Name)] -> [(Term, Name)] -> [(Term, Name)]
forall a. [a] -> [a] -> [a]
++
[Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) Term
sc
getMissing [Name]
hs [Name]
env (Bind Name
n Binder Term
b Term
sc)
= [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs [Name]
env (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b) [(Term, Name)] -> [(Term, Name)] -> [(Term, Name)]
forall a. [a] -> [a] -> [a]
++
[Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) Term
sc
getMissing [Name]
hs [Name]
env ap :: Term
ap@(App AppStatus Name
_ Term
_ Term
_)
| (fn :: Term
fn@(P NameType
_ Name
n Term
_), [Term]
args) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap = Term -> [Term] -> [(Term, Name)]
getMissingArgs Term
fn [Term]
args
where
getMissingArgs :: Term -> [Term] -> [(Term, Name)]
getMissingArgs Term
n [] = []
getMissingArgs Term
n (V Int
i : [Term]
as)
| [Name]
env[Name] -> Int -> Name
forall a. HasCallStack => [a] -> Int -> a
!!Int
i Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs = (Term
n, [Name]
env[Name] -> Int -> Name
forall a. HasCallStack => [a] -> Int -> a
!!Int
i) (Term, Name) -> [(Term, Name)] -> [(Term, Name)]
forall a. a -> [a] -> [a]
: Term -> [Term] -> [(Term, Name)]
getMissingArgs Term
n [Term]
as
getMissingArgs Term
n (P NameType
_ Name
a Term
_ : [Term]
as)
| Name
a Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs = (Term
n, Name
a) (Term, Name) -> [(Term, Name)] -> [(Term, Name)]
forall a. a -> [a] -> [a]
: Term -> [Term] -> [(Term, Name)]
getMissingArgs Term
n [Term]
as
getMissingArgs Term
n (Term
a : [Term]
as) = [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs [Name]
env Term
a [(Term, Name)] -> [(Term, Name)] -> [(Term, Name)]
forall a. [a] -> [a] -> [a]
++ Term -> [Term] -> [(Term, Name)]
getMissingArgs Term
n [Term]
as
getMissing [Name]
hs [Name]
env (App AppStatus Name
_ Term
f Term
a)
= [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs [Name]
env Term
f [(Term, Name)] -> [(Term, Name)] -> [(Term, Name)]
forall a. [a] -> [a] -> [a]
++ [Name] -> [Name] -> Term -> [(Term, Name)]
getMissing [Name]
hs [Name]
env Term
a
getMissing [Name]
hs [Name]
env Term
_ = []
pprintErr' IState
i (UniverseError FC
fc UExp
uexp (Int, Int)
old (Int, Int)
new [ConstraintFC]
suspects) =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Universe inconsistency." Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
(Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Doc OutputAnnotation -> Doc OutputAnnotation)
-> ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep) [ String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Working on:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text (UExp -> String
forall a. Show a => a -> String
show UExp
uexp)
, String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Old domain:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text ((Int, Int) -> String
forall a. Show a => a -> String
show (Int, Int)
old)
, String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"New domain:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text ((Int, Int) -> String
forall a. Show a => a -> String
show (Int, Int)
new)
, String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Involved constraints:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
(Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Doc OutputAnnotation -> Doc OutputAnnotation)
-> ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep) ((ConstraintFC -> Doc OutputAnnotation)
-> [ConstraintFC] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc OutputAnnotation
forall a. String -> Doc a
text (String -> Doc OutputAnnotation)
-> (ConstraintFC -> String) -> ConstraintFC -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstraintFC -> String
forall a. Show a => a -> String
show) [ConstraintFC]
suspects)
]
pprintErr' IState
i (UniqueError Universe
NullType Name
n)
= String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Borrowed name" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> String -> Doc OutputAnnotation
annName' Name
n (Name -> String
showbasic Name
n)
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"must not be used on RHS"
pprintErr' IState
i (UniqueError Universe
_ Name
n) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Unique name" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> String -> Doc OutputAnnotation
annName' Name
n (Name -> String
showbasic Name
n)
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"is used more than once"
pprintErr' IState
i (UniqueKindError Universe
k Name
n) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Constructor" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> String -> Doc OutputAnnotation
annName' Name
n (Name -> String
showbasic Name
n)
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text (String
"has a " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Universe -> String
forall a. Show a => a -> String
show Universe
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
",")
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"but the data type does not"
pprintErr' IState
i Err
ProgramLineComment = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Program line next to comment"
pprintErr' IState
i (Inaccessible Name
n) = Name -> Doc OutputAnnotation
annName Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"is not an accessible pattern variable"
pprintErr' IState
i (UnknownImplicit Name
n Name
f) = Name -> Doc OutputAnnotation
annName Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"is not an implicit argument of" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc OutputAnnotation
annName Name
f
pprintErr' IState
i (NonCollapsiblePostulate Name
n) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"The return type of postulate" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Name -> Doc OutputAnnotation
annName Name
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"is not collapsible"
pprintErr' IState
i (AlreadyDefined Name
n) = Name -> Doc OutputAnnotation
annName Name
nDoc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"is already defined"
pprintErr' IState
i (ProofSearchFail Err
e) = IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e
pprintErr' IState
i (NoRewriting Term
l Term
r Term
tm) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"rewriting" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
l (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
l)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"to" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
r (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
r)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"did not change type" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
tm (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
tm))
pprintErr' IState
i (At FC
f Err
e) = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (FC -> OutputAnnotation
AnnFC FC
f) (String -> Doc OutputAnnotation
forall a. String -> Doc a
text (FC -> String
forall a. Show a => a -> String
show FC
f)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e
pprintErr' IState
i (Elaborating String
s Name
n Maybe Term
ty Err
e) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"When checking" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
s Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Name -> String -> Doc OutputAnnotation
annName' Name
n (IState -> Name -> String
showqual IState
i Name
n) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Maybe Term -> Doc OutputAnnotation
pprintTy Maybe Term
ty Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e
where pprintTy :: Maybe Term -> Doc OutputAnnotation
pprintTy Maybe Term
Nothing = Doc OutputAnnotation
forall a. Doc a
colon
pprintTy (Just Term
ty) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
" with expected type" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
ty (IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
i (IState -> Term -> PTerm
delabSugared IState
i Term
ty)))
Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line
pprintErr' IState
i (ElaboratingArg Name
f Name
x [(Name, Name)]
_ Err
e)
| Name -> Bool
isInternal Name
f = IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e
| Name -> Bool
isUN Name
x =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"When checking argument" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (Name -> Bool -> OutputAnnotation
AnnBoundName Name
x Bool
False) (String -> Doc OutputAnnotation
forall a. String -> Doc a
text (Name -> String
showbasic Name
x)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"to" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
whatIsName Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Name -> Doc OutputAnnotation
annName Name
f Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e)
| Bool
otherwise =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"When checking an application of" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
whatIsName Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Name -> Doc OutputAnnotation
annName Name
f Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e)
where whatIsName :: Doc a
whatIsName = let ctxt :: Context
ctxt = IState -> Context
tt_ctxt IState
i
in if Name -> Context -> Bool
isTConName Name
f Context
ctxt
then String -> Doc a
forall a. String -> Doc a
text String
"type constructor" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<> Doc a
forall a. Doc a
space
else if Name -> Context -> Bool
isDConName Name
f Context
ctxt
then String -> Doc a
forall a. String -> Doc a
text String
"constructor" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<> Doc a
forall a. Doc a
space
else if Name -> Context -> Bool
isFnName Name
f Context
ctxt
then String -> Doc a
forall a. String -> Doc a
text String
"function" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<> Doc a
forall a. Doc a
space
else Doc a
forall a. Doc a
empty
isInternal :: Name -> Bool
isInternal (MN Int
_ Text
_) = Bool
True
isInternal (UN Text
n) = Text -> Text -> Bool
T.isPrefixOf (String -> Text
T.pack String
"__") Text
n
isInternal (NS Name
n [Text]
_) = Name -> Bool
isInternal Name
n
isInternal Name
_ = Bool
True
pprintErr' IState
i (ProviderError String
msg) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text (String
"Type provider error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg)
pprintErr' IState
i (LoadingFailed String
fn Err
e) = String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Loading" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
fn Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"failed:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e
pprintErr' IState
i (ReflectionError [[ErrorReportPart]]
parts Err
orig) =
let parts' :: [Doc OutputAnnotation]
parts' = ([ErrorReportPart] -> Doc OutputAnnotation)
-> [[ErrorReportPart]] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
fillSep ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> ([ErrorReportPart] -> [Doc OutputAnnotation])
-> [ErrorReportPart]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ErrorReportPart -> Doc OutputAnnotation)
-> [ErrorReportPart] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> ErrorReportPart -> Doc OutputAnnotation
showPart IState
i)) [[ErrorReportPart]]
parts in
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
fillSep [Doc OutputAnnotation]
parts') Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
if (IOption -> Bool
opt_origerr (IState -> IOption
idris_options IState
i))
then Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Original error:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
orig)
else Doc OutputAnnotation
forall a. Doc a
empty
pprintErr' IState
i (ReflectionFailed String
msg Err
err) =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"When attempting to perform error reflection, the following internal error occurred:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
err) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
msg Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text (String
"This is probably a bug. Please consider reporting it at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bugaddr)
pprintErr' IState
i (ElabScriptDebug [ErrorReportPart]
msg Term
tm [(Name, Term, [(Name, Binder Term)])]
holes) =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Elaboration halted." Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (Doc OutputAnnotation -> Doc OutputAnnotation)
-> ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
hsep ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ (ErrorReportPart -> Doc OutputAnnotation)
-> [ErrorReportPart] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> ErrorReportPart -> Doc OutputAnnotation
showPart IState
i) [ErrorReportPart]
msg) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Holes:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep (((Name, Term, [(Name, Binder Term)]) -> Doc OutputAnnotation)
-> [(Name, Term, [(Name, Binder Term)])] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term, [(Name, Binder Term)]) -> Doc OutputAnnotation
ppHole [(Name, Term, [(Name, Binder Term)])]
holes)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Term: " Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented ([Name] -> Term -> Doc OutputAnnotation
pprintTT [] Term
tm)
where ppHole :: (Name, Type, [(Name, Binder Type)]) -> Doc OutputAnnotation
ppHole :: (Name, Term, [(Name, Binder Term)]) -> Doc OutputAnnotation
ppHole (Name
hn, Term
goal, [(Name, Binder Term)]
env) =
[Name] -> [(Name, Binder Term)] -> Doc OutputAnnotation
ppAssumptions [] ([(Name, Binder Term)] -> [(Name, Binder Term)]
forall a. [a] -> [a]
reverse [(Name, Binder Term)]
env) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"----------------------------------" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Name -> Bool -> Doc OutputAnnotation
bindingOf Name
hn Bool
False Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
":" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
[Name] -> Term -> Doc OutputAnnotation
pprintTT (((Name, Binder Term) -> Name) -> [(Name, Binder Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Binder Term) -> Name
forall a b. (a, b) -> a
fst ([(Name, Binder Term)] -> [(Name, Binder Term)]
forall a. [a] -> [a]
reverse [(Name, Binder Term)]
env)) Term
goal Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line
ppAssumptions :: [Name] -> [(Name, Binder Type)] -> Doc OutputAnnotation
ppAssumptions :: [Name] -> [(Name, Binder Term)] -> Doc OutputAnnotation
ppAssumptions [Name]
ns [] = Doc OutputAnnotation
forall a. Doc a
empty
ppAssumptions [Name]
ns ((Name
n, Binder Term
b) : [(Name, Binder Term)]
rest) =
Name -> Bool -> Doc OutputAnnotation
bindingOf Name
n Bool
False Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
":" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
[Name] -> Term -> Doc OutputAnnotation
pprintTT [Name]
ns (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
[Name] -> [(Name, Binder Term)] -> Doc OutputAnnotation
ppAssumptions (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
ns) [(Name, Binder Term)]
rest
pprintErr' IState
i (ElabScriptStuck Term
tm) =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't run" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Name] -> Term -> Doc OutputAnnotation
pprintTT [] Term
tm Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"as an elaborator script." Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Is it a stuck term?"
pprintErr' IState
i (RunningElabScript Err
e) =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"While running an elaboration script, the following error occurred" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$> IState -> Err -> Doc OutputAnnotation
pprintErr' IState
i Err
e
pprintErr' IState
i (ElabScriptStaging Name
n) =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Can't run elaboration script because it contains pattern matching that has not yet been elaborated." Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Try lifting the script to a top-level definition." Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"In particular, the problem is caused by:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc OutputAnnotation
annName Name
n
pprintErr' IState
i (FancyMsg [ErrorReportPart]
parts) =
[Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
fillSep ((ErrorReportPart -> Doc OutputAnnotation)
-> [ErrorReportPart] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> ErrorReportPart -> Doc OutputAnnotation
showPart IState
i) [ErrorReportPart]
parts)
showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation
showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation
showPart IState
ist (TextPart String
str) = [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
fillSep ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> (String -> [Doc OutputAnnotation])
-> String
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Doc OutputAnnotation)
-> [String] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc OutputAnnotation
forall a. String -> Doc a
text ([String] -> [Doc OutputAnnotation])
-> (String -> [String]) -> String -> [Doc OutputAnnotation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
words (String -> Doc OutputAnnotation) -> String -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ String
str
showPart IState
ist (NamePart Name
n) = Name -> Doc OutputAnnotation
annName Name
n
showPart IState
ist (TermPart Term
tm) = IState -> PTerm -> Doc OutputAnnotation
pprintTerm IState
ist (IState -> Term -> PTerm
delabSugared IState
ist Term
tm)
showPart IState
ist (RawPart Raw
tm) = [Name] -> Raw -> Doc OutputAnnotation
pprintRaw [] Raw
tm
showPart IState
ist (SubReport [ErrorReportPart]
rs) = Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented (Doc OutputAnnotation -> Doc OutputAnnotation)
-> ([ErrorReportPart] -> Doc OutputAnnotation)
-> [ErrorReportPart]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
hsep ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> ([ErrorReportPart] -> [Doc OutputAnnotation])
-> [ErrorReportPart]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ErrorReportPart -> Doc OutputAnnotation)
-> [ErrorReportPart] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> ErrorReportPart -> Doc OutputAnnotation
showPart IState
ist) ([ErrorReportPart] -> Doc OutputAnnotation)
-> [ErrorReportPart] -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ [ErrorReportPart]
rs
renameMNs :: Term -> Term -> (Term, Term, [Name])
renameMNs :: Term -> Term -> (Term, Term, [Name])
renameMNs Term
x Term
y = let ns :: [Name]
ns = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Term -> [Name]
forall n. Eq n => TT n -> [n]
allTTNames Term
x [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
forall n. Eq n => TT n -> [n]
allTTNames Term
y
newnames :: [(Name, Name)]
newnames = State Int [(Name, Name)] -> Int -> [(Name, Name)]
forall s a. State s a -> s -> a
evalState ([(Name, Name)] -> [Name] -> State Int [(Name, Name)]
getRenames [] [Name]
ns) Int
1 in
([(Name, Name)] -> Term -> Term
rename [(Name, Name)]
newnames Term
x, [(Name, Name)] -> Term -> Term
rename [(Name, Name)]
newnames Term
y, ((Name, Name) -> Name) -> [(Name, Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Name) -> Name
forall a b. (a, b) -> b
snd [(Name, Name)]
newnames)
where
getRenames :: [(Name, Name)] -> [Name] -> State Int [(Name, Name)]
getRenames :: [(Name, Name)] -> [Name] -> State Int [(Name, Name)]
getRenames [(Name, Name)]
acc [] = [(Name, Name)] -> State Int [(Name, Name)]
forall a. a -> StateT Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, Name)]
acc
getRenames [(Name, Name)]
acc (n :: Name
n@(MN Int
i Text
x) : [Name]
xs) | Text -> [Name] -> Bool
rpt Text
x [Name]
xs
= do Int
idx <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
idx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
let x' :: Name
x' = String -> Name
sUN (Text -> String
str Text
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
idx)
[(Name, Name)] -> [Name] -> State Int [(Name, Name)]
getRenames ((Name
n, Name
x') (Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
: [(Name, Name)]
acc) [Name]
xs
getRenames [(Name, Name)]
acc (n :: Name
n@(UN Text
x) : [Name]
xs) | Text -> [Name] -> Bool
rpt Text
x [Name]
xs
= do Int
idx <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
idx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
let x' :: Name
x' = String -> Name
sUN (Text -> String
str Text
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
idx)
[(Name, Name)] -> [Name] -> State Int [(Name, Name)]
getRenames ((Name
n, Name
x') (Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
: [(Name, Name)]
acc) [Name]
xs
getRenames [(Name, Name)]
acc (Name
x : [Name]
xs) = [(Name, Name)] -> [Name] -> State Int [(Name, Name)]
getRenames [(Name, Name)]
acc [Name]
xs
rpt :: Text -> [Name] -> Bool
rpt Text
x [] = Bool
False
rpt Text
x (UN Text
y : [Name]
xs) | Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
y = Bool
True
rpt Text
x (MN Int
i Text
y : [Name]
xs) | Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
y = Bool
True
rpt Text
x (Name
_ : [Name]
xs) = Text -> [Name] -> Bool
rpt Text
x [Name]
xs
rename :: [(Name, Name)] -> Term -> Term
rename :: [(Name, Name)] -> Term -> Term
rename [(Name, Name)]
ns (P NameType
nt Name
x Term
t) | Just Name
x' <- Name -> [(Name, Name)] -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x [(Name, Name)]
ns = NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
nt Name
x' Term
t
rename [(Name, Name)]
ns (App AppStatus Name
s Term
f Term
a) = AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s ([(Name, Name)] -> Term -> Term
rename [(Name, Name)]
ns Term
f) ([(Name, Name)] -> Term -> Term
rename [(Name, Name)]
ns Term
a)
rename [(Name, Name)]
ns (Bind Name
x Binder Term
b Term
sc)
= let b' :: Binder Term
b' = (Term -> Term) -> Binder Term -> Binder Term
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, Name)] -> Term -> Term
rename [(Name, Name)]
ns) Binder Term
b
sc' :: Term
sc' = [(Name, Name)] -> Term -> Term
rename [(Name, Name)]
ns Term
sc in
case Name -> [(Name, Name)] -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x [(Name, Name)]
ns of
Just Name
x' -> Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x' Binder Term
b' Term
sc'
Maybe Name
Nothing -> Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x Binder Term
b' Term
sc'
rename [(Name, Name)]
ns Term
x = Term
x
addImplicitDiffs :: PTerm -> PTerm -> (PTerm, PTerm)
addImplicitDiffs :: PTerm -> PTerm -> (PTerm, PTerm)
addImplicitDiffs PTerm
x PTerm
y
= if (PTerm
x PTerm -> PTerm -> Bool
`expLike` PTerm
y) then PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
x PTerm
y else (PTerm
x, PTerm
y)
where
addI :: PTerm -> PTerm -> (PTerm, PTerm)
addI :: PTerm -> PTerm -> (PTerm, PTerm)
addI (PApp FC
fc PTerm
f [PArg]
as) (PApp FC
gc PTerm
g [PArg]
bs)
= let ([PArg]
as', [PArg]
bs') = [PArg] -> [PArg] -> ([PArg], [PArg])
addShows [PArg]
as [PArg]
bs in
(FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f [PArg]
as', FC -> PTerm -> [PArg] -> PTerm
PApp FC
gc PTerm
g [PArg]
bs')
where addShows :: [PArg] -> [PArg] -> ([PArg], [PArg])
addShows [] [] = ([], [])
addShows (PArg
a:[PArg]
as) (PArg
b:[PArg]
bs)
= let ([PArg]
as', [PArg]
bs') = [PArg] -> [PArg] -> ([PArg], [PArg])
addShows [PArg]
as [PArg]
bs
(PTerm
a', PTerm
b') = PTerm -> PTerm -> (PTerm, PTerm)
addI (PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
a) (PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
b) in
if (Bool -> Bool
not (PTerm
a' PTerm -> PTerm -> Bool
`expLike` PTerm
b'))
then (PArg
a { argopts = AlwaysShow : argopts a,
getTm = a' } PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
as',
PArg
b { argopts = AlwaysShow : argopts b,
getTm = b' } PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
bs')
else (PArg
a { getTm = a' } PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
as',
PArg
b { getTm = b' } PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
bs')
addShows [PArg]
xs [PArg]
ys = ([PArg]
xs, [PArg]
ys)
addI (PLam FC
fc Name
n FC
nfc PTerm
a PTerm
b) (PLam FC
fc' Name
n' FC
nfc' PTerm
c PTerm
d)
= let (PTerm
a', PTerm
c') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
a PTerm
c
(PTerm
b', PTerm
d') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
b PTerm
d in
(FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
n FC
nfc PTerm
a' PTerm
b', FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc' Name
n' FC
nfc' PTerm
c' PTerm
d')
addI (PPi Plicity
p Name
n FC
fc PTerm
a PTerm
b) (PPi Plicity
p' Name
n' FC
fc' PTerm
c PTerm
d)
= let (PTerm
a', PTerm
c') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
a PTerm
c
(PTerm
b', PTerm
d') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
b PTerm
d in
(Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p Name
n FC
fc PTerm
a' PTerm
b', Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p' Name
n' FC
fc' PTerm
c' PTerm
d')
addI (PPair FC
fc [FC]
hls PunInfo
pi PTerm
a PTerm
b) (PPair FC
fc' [FC]
hls' PunInfo
pi' PTerm
c PTerm
d)
= let (PTerm
a', PTerm
c') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
a PTerm
c
(PTerm
b', PTerm
d') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
b PTerm
d in
(FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
fc [FC]
hls PunInfo
pi PTerm
a' PTerm
b', FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
fc' [FC]
hls' PunInfo
pi' PTerm
c' PTerm
d')
addI (PDPair FC
fc [FC]
hls PunInfo
pi PTerm
a PTerm
t PTerm
b) (PDPair FC
fc' [FC]
hls' PunInfo
pi' PTerm
c PTerm
u PTerm
d)
= let (PTerm
a', PTerm
c') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
a PTerm
c
(PTerm
t', PTerm
u') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
t PTerm
u
(PTerm
b', PTerm
d') = PTerm -> PTerm -> (PTerm, PTerm)
addI PTerm
b PTerm
d in
(FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
fc [FC]
hls PunInfo
pi PTerm
a' PTerm
t' PTerm
b', FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
fc' [FC]
hls' PunInfo
pi' PTerm
c' PTerm
u' PTerm
d')
addI PTerm
x PTerm
y = (PTerm
x, PTerm
y)
expLike :: PTerm -> PTerm -> Bool
expLike (PRef FC
_ [FC]
_ Name
n) (PRef FC
_ [FC]
_ Name
n') = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n'
expLike (PApp FC
_ PTerm
f [PArg]
as) (PApp FC
_ PTerm
f' [PArg]
as')
= PTerm -> PTerm -> Bool
expLike PTerm
f PTerm
f' Bool -> Bool -> Bool
&& [PArg] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PArg]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [PArg] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PArg]
as' Bool -> Bool -> Bool
&&
[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((PTerm -> PTerm -> Bool) -> [PTerm] -> [PTerm] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith PTerm -> PTerm -> Bool
expLike ([PArg] -> [PTerm]
getExps [PArg]
as) ([PArg] -> [PTerm]
getExps [PArg]
as'))
expLike (PPi Plicity
_ Name
n FC
fc PTerm
s PTerm
t) (PPi Plicity
_ Name
n' FC
fc' PTerm
s' PTerm
t')
= Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
expLike PTerm
s PTerm
s' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
expLike PTerm
t PTerm
t'
expLike (PLam FC
_ Name
n FC
_ PTerm
s PTerm
t) (PLam FC
_ Name
n' FC
_ PTerm
s' PTerm
t')
= Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
expLike PTerm
s PTerm
s' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
expLike PTerm
t PTerm
t'
expLike (PPair FC
_ [FC]
_ PunInfo
_ PTerm
x PTerm
y) (PPair FC
_ [FC]
_ PunInfo
_ PTerm
x' PTerm
y') = PTerm -> PTerm -> Bool
expLike PTerm
x PTerm
x' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
expLike PTerm
y PTerm
y'
expLike (PDPair FC
_ [FC]
_ PunInfo
_ PTerm
x PTerm
_ PTerm
y) (PDPair FC
_ [FC]
_ PunInfo
_ PTerm
x' PTerm
_ PTerm
y') = PTerm -> PTerm -> Bool
expLike PTerm
x PTerm
x' Bool -> Bool -> Bool
&& PTerm -> PTerm -> Bool
expLike PTerm
y PTerm
y'
expLike PTerm
x PTerm
y = PTerm
x PTerm -> PTerm -> Bool
forall a. Eq a => a -> a -> Bool
== PTerm
y
isUN :: Name -> Bool
isUN :: Name -> Bool
isUN (UN Text
n) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Text -> Text -> Bool
T.isPrefixOf (String -> Text
T.pack String
"__") Text
n
isUN (NS Name
n [Text]
_) = Name -> Bool
isUN Name
n
isUN Name
_ = Bool
False
annName :: Name -> Doc OutputAnnotation
annName :: Name -> Doc OutputAnnotation
annName Name
n = Name -> String -> Doc OutputAnnotation
annName' Name
n (Name -> String
showbasic Name
n)
annName' :: Name -> String -> Doc OutputAnnotation
annName' :: Name -> String -> Doc OutputAnnotation
annName' Name
n String
str = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate (Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing) (String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
str)
annTm :: Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm :: Term -> Doc OutputAnnotation -> Doc OutputAnnotation
annTm Term
tm = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm [] Term
tm)
fancifyAnnots :: IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots :: IState -> Bool -> OutputAnnotation -> OutputAnnotation
fancifyAnnots IState
ist Bool
meta annot :: OutputAnnotation
annot@(AnnName Name
n Maybe NameOutput
nt Maybe String
_ Maybe String
_) =
do let ctxt :: Context
ctxt = IState -> Context
tt_ctxt IState
ist
docs :: Maybe String
docs = IState -> Name -> Maybe String
docOverview IState
ist Name
n
ty :: Maybe String
ty = String -> Maybe String
forall a. a -> Maybe a
Just (IState -> Name -> String
getTy IState
ist Name
n)
case () of
()
_ | Name -> Context -> Bool
isDConName Name
n Context
ctxt -> Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
DataOutput) Maybe String
docs Maybe String
ty
()
_ | Name -> Context -> Bool
isFnName Name
n Context
ctxt -> Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
FunOutput) Maybe String
docs Maybe String
ty
()
_ | Name -> Context -> Bool
isTConName Name
n Context
ctxt -> Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
TypeOutput) Maybe String
docs Maybe String
ty
()
_ | Name -> IState -> Bool
isMetavarName Name
n IState
ist -> if Bool
meta
then Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
MetavarOutput) Maybe String
docs Maybe String
ty
else Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
FunOutput) Maybe String
docs Maybe String
ty
()
_ | Name -> IState -> Bool
isPostulateName Name
n IState
ist -> Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n (Maybe NameOutput
nt Maybe NameOutput -> Maybe NameOutput -> Maybe NameOutput
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
PostulateOutput) Maybe String
docs Maybe String
ty
()
_ | Bool
otherwise -> OutputAnnotation
annot
where docOverview :: IState -> Name -> Maybe String
docOverview :: IState -> Name -> Maybe String
docOverview IState
ist Name
n = do (Docstring DocTerm, [(Name, Docstring DocTerm)])
docs <- Name
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Maybe (Docstring DocTerm, [(Name, Docstring DocTerm)])
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
ist)
let o :: Docstring DocTerm
o = Docstring DocTerm -> Docstring DocTerm
forall a. Docstring a -> Docstring a
overview ((Docstring DocTerm, [(Name, Docstring DocTerm)])
-> Docstring DocTerm
forall a b. (a, b) -> a
fst (Docstring DocTerm, [(Name, Docstring DocTerm)])
docs)
norm :: Term -> Term
norm = Context -> Env -> Term -> Term
normaliseAll (IState -> Context
tt_ctxt IState
ist) []
out :: String -> String
out = SimpleDoc OutputAnnotation -> String -> String
forall a. SimpleDoc a -> String -> String
displayS (SimpleDoc OutputAnnotation -> String -> String)
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> String
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
1.0 Int
50 (Doc OutputAnnotation -> String -> String)
-> Doc OutputAnnotation -> String -> String
forall a b. (a -> b) -> a -> b
$
(DocTerm -> String -> Doc OutputAnnotation)
-> Docstring DocTerm -> Doc OutputAnnotation
forall a.
(a -> String -> Doc OutputAnnotation)
-> Docstring a -> Doc OutputAnnotation
renderDocstring ((Term -> Doc OutputAnnotation)
-> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation
renderDocTerm (IState -> Term -> Doc OutputAnnotation
pprintDelab IState
ist)
Term -> Term
norm) Docstring DocTerm
o
String -> Maybe String
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> String
out String
"")
getTy :: IState -> Name -> String
getTy :: IState -> Name -> String
getTy IState
ist Name
n = let theTy :: Doc OutputAnnotation
theTy = PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm (IState -> PPOption
ppOptionIst IState
ist) [] [] (IState -> [FixDecl]
idris_infixes IState
ist) (PTerm -> Doc OutputAnnotation) -> PTerm -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$
IState -> PTerm -> PTerm
resugar IState
ist (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ IState -> Name -> PTerm
delabTy IState
ist Name
n
in (SimpleDoc OutputAnnotation -> String -> String
forall a. SimpleDoc a -> String -> String
displayS (SimpleDoc OutputAnnotation -> String -> String)
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> String
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
1.0 Int
50 (Doc OutputAnnotation -> String -> String)
-> Doc OutputAnnotation -> String -> String
forall a b. (a -> b) -> a -> b
$ Doc OutputAnnotation
theTy) String
""
fancifyAnnots IState
_ Bool
_ OutputAnnotation
annot = OutputAnnotation
annot
showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation
showSc IState
i [] = Doc OutputAnnotation
forall a. Doc a
empty
showSc IState
i [(Name, Term)]
xs = Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"In context:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
indented ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep ([Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. [a] -> [a]
reverse ([(Name, Bool)] -> [(Name, Term)] -> [Doc OutputAnnotation]
showSc' [] [(Name, Term)]
xs)))
where showSc' :: [(Name, Bool)] -> [(Name, Term)] -> [Doc OutputAnnotation]
showSc' [(Name, Bool)]
bnd [] = []
showSc' [(Name, Bool)]
bnd ((Name
n, Term
ty):[(Name, Term)]
ctxt) =
let this :: Doc OutputAnnotation
this = Name -> Bool -> Doc OutputAnnotation
bindingOf Name
n Bool
False Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
pprintTerm' IState
i [(Name, Bool)]
bnd (IState -> Term -> PTerm
delabSugared IState
i Term
ty)
in Doc OutputAnnotation
this Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. a -> [a] -> [a]
: [(Name, Bool)] -> [(Name, Term)] -> [Doc OutputAnnotation]
showSc' ((Name
n,Bool
False)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) [(Name, Term)]
ctxt
showqual :: IState -> Name -> String
showqual :: IState -> Name -> String
showqual IState
i Name
n = Maybe IState
-> [(Name, Bool)] -> PPOption -> Bool -> Name -> String
showName (IState -> Maybe IState
forall a. a -> Maybe a
Just IState
i) [] (IState -> PPOption
ppOptionIst IState
i) { ppopt_impl = False } Bool
False (Name -> Name
dens Name
n)
where
dens :: Name -> Name
dens ns :: Name
ns@(NS Name
n [Text]
_) = case Name -> Ctxt [PArg] -> [[PArg]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
[[PArg]
_] -> Name
n
[[PArg]]
_ -> Name
ns
dens Name
n = Name
n
showbasic :: Name -> String
showbasic :: Name -> String
showbasic n :: Name
n@(UN Text
_) = Name -> String
forall a. Show a => a -> String
show Name
n
showbasic (MN Int
_ Text
s) = Text -> String
str Text
s
showbasic (NS Name
n [Text]
s) = String -> [String] -> String
showSep String
"." ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
str ([Text] -> [Text]
forall a. [a] -> [a]
reverse [Text]
s)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"." String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
showbasic Name
n
showbasic (SN SpecialName
s) = SpecialName -> String
forall a. Show a => a -> String
show SpecialName
s
showbasic Name
n = Name -> String
forall a. Show a => a -> String
show Name
n