{-|
Module      : Idris.Elab.Implementation
Description : Code to elaborate instances.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE PatternGuards #-}
module Idris.Elab.Implementation(elabImplementation) where

import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate
import Idris.Docstrings
import Idris.Elab.Term
import Idris.Elab.Type
import Idris.Elab.Utils
import Idris.Error
import Idris.Output (iWarn, sendHighlighting)

import Util.Pretty (text)

import Prelude hiding (id, (.))

import Control.Category
import Control.Monad
import Data.List
import Data.Maybe
import qualified Data.Text as T

elabImplementation :: ElabInfo
                   -> SyntaxInfo
                   -> Docstring (Either Err PTerm)
                   -> [(Name, Docstring (Either Err PTerm))]
                   -> ElabWhat        -- ^ phase
                   -> FC
                   -> [(Name, PTerm)] -- ^ constraints
                   -> [Name]          -- ^ parent dictionary names (optionally)
                   -> Accessibility
                   -> FnOpts
                   -> Name            -- ^ the interface
                   -> FC              -- ^ precise location of interface name
                   -> [PTerm]         -- ^ interface parameters (i.e. implementation)
                   -> [(Name, PTerm)] -- ^ Extra arguments in scope (e.g. implementation in where block)
                   -> PTerm           -- ^ full implementation type
                   -> Maybe Name      -- ^ explicit name
                   -> [PDecl]
                   -> Idris ()
elabImplementation :: ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> ElabWhat
-> FC
-> [(Name, PTerm)]
-> [Name]
-> Accessibility
-> FnOpts
-> Name
-> FC
-> [PTerm]
-> [(Name, PTerm)]
-> PTerm
-> Maybe Name
-> [PDecl]
-> Idris ()
elabImplementation ElabInfo
info SyntaxInfo
syn Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs ElabWhat
what FC
fc [(Name, PTerm)]
cs [Name]
parents Accessibility
acc FnOpts
opts Name
n FC
nfc [PTerm]
ps [(Name, PTerm)]
pextra PTerm
t Maybe Name
expn [PDecl]
ds = do
    IState
ist <- Idris IState
getIState
    (Name
n, InterfaceInfo
ci) <- case forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
                  [(Name, InterfaceInfo)
c] -> forall (m :: * -> *) a. Monad m => a -> m a
return (Name, InterfaceInfo)
c
                  [] -> forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show FC
fc forall a. [a] -> [a] -> [a]
++ String
":" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" is not an interface"
                  [(Name, InterfaceInfo)]
cs -> forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail forall a b. (a -> b) -> a -> b
$ forall t. FC -> Err' t -> Err' t
At FC
fc
                           (forall t. [Name] -> Err' t
CantResolveAlts (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, InterfaceInfo)]
cs))
    let iname :: Name
iname = forall {a}. Show a => Name -> [String] -> [a] -> Maybe Name -> Name
mkiname Name
n (ElabInfo -> [String]
namespace ElabInfo
info) [PTerm]
ps Maybe Name
expn
    IState -> Idris ()
putIState (IState
ist { hide_list :: Ctxt Accessibility
hide_list = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
iname Accessibility
acc (IState -> Ctxt Accessibility
hide_list IState
ist) })
    IState
ist <- Idris IState
getIState

    let totopts :: FnOpts
totopts = FnOpt
Dictionary forall a. a -> [a] -> [a]
: FnOpt
Inlinable forall a. a -> [a] -> [a]
: FnOpts
opts

    let emptyinterface :: Bool
emptyinterface = forall (t :: * -> *) a. Foldable t => t a -> Bool
null (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci)
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ElabWhat
what forall a. Eq a => a -> a -> Bool
/= ElabWhat
EDefns) forall a b. (a -> b) -> a -> b
$ do
         Type
nty <- Bool
-> ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> Idris Type
elabType' Bool
True ElabInfo
info SyntaxInfo
syn Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs FC
fc FnOpts
totopts Name
iname FC
NoFC
                          (Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
piBindp Plicity
expl_param [(Name, PTerm)]
pextra PTerm
t)
         -- if the implementation type matches any of the implementations we have already,
         -- and it's not a named implementation, then it's overlapping, so report an error
         case Maybe Name
expn of
            Maybe Name
Nothing
               | FnOpt
OverlappingDictionary forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` FnOpts
opts ->
                       do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall {a} {a}. Show a => a -> Idris a
overlapping forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {t :: * -> *} {a}.
(Foldable t, Eq a, Num a, Enum a) =>
IState -> t a -> PTerm -> Name -> Maybe PTerm
findOverlapping IState
ist (InterfaceInfo -> [Int]
interface_determiners InterfaceInfo
ci) (IState -> Type -> PTerm
delab IState
ist Type
nty))
                                (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ InterfaceInfo -> [(Name, Bool)]
interface_implementations InterfaceInfo
ci)
                          Bool -> Bool -> Name -> Name -> Idris ()
addImplementation Bool
intImpl Bool
True Name
n Name
iname
            Maybe Name
_ -> Bool -> Bool -> Name -> Name -> Idris ()
addImplementation Bool
intImpl Bool
False Name
n Name
iname

    IState
ist <- Idris IState
getIState
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Maybe a -> Bool
isNothing Maybe Name
expn) forall a b. (a -> b) -> a -> b
$
      FC -> Name -> [Int] -> Maybe Type -> Idris ()
checkInjectiveArgs FC
fc Name
n (InterfaceInfo -> [Int]
interface_determiners InterfaceInfo
ci) (Name -> Context -> Maybe Type
lookupTyExact Name
iname (IState -> Context
tt_ctxt IState
ist))

    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ElabWhat
what forall a. Eq a => a -> a -> Bool
/= ElabWhat
ETypes Bool -> Bool -> Bool
&& (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PDecl]
ds Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
emptyinterface))) forall a b. (a -> b) -> a -> b
$ do
         -- Add the parent implementation names to the privileged set
         [Name]
oldOpen <- [Name] -> Idris [Name]
addOpenImpl [Name]
parents

         let ips :: [(Name, PTerm)]
ips = forall a b. [a] -> [b] -> [(a, b)]
zip (InterfaceInfo -> [Name]
interface_params InterfaceInfo
ci) [PTerm]
ps
         let ns :: [Text]
ns = case Name
n of
                    NS Name
n [Text]
ns' -> [Text]
ns'
                    Name
_ -> []
         -- get the implicit parameters that need passing through to the
         -- where block
         [[PArg' PTerm]]
wparams <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\PTerm
p -> case PTerm
p of
                                  PApp FC
_ PTerm
_ [PArg' PTerm]
args -> [PTerm] -> StateT IState (ExceptT Err IO) [PArg' PTerm]
getWParams (forall a b. (a -> b) -> [a] -> [b]
map forall t. PArg' t -> t
getTm [PArg' PTerm]
args)
                                  a :: PTerm
a@(PRef FC
fc [FC]
_ Name
f) -> [PTerm] -> StateT IState (ExceptT Err IO) [PArg' PTerm]
getWParams [PTerm
a]
                                  PTerm
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []) [PTerm]
ps
         IState
ist <- Idris IState
getIState
         let pnames :: [Name]
pnames = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t. PArg' t -> Name
pname (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a. Eq a => [a] -> [a]
nub [[PArg' PTerm]]
wparams)) forall a. [a] -> [a] -> [a]
++
                          forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([(Name, PTerm)] -> IState -> PTerm -> [Name]
namesIn [] IState
ist) [PTerm]
ps

         let superInterfaceImplementations :: [PDecl]
superInterfaceImplementations = forall a b. (a -> b) -> [a] -> [b]
map ([(Name, PTerm)] -> [Name] -> PDecl -> PDecl
substImplementation [(Name, PTerm)]
ips [Name]
pnames) (InterfaceInfo -> [PDecl]
interface_default_super_interfaces InterfaceInfo
ci)
         [PDecl]
undefinedSuperInterfaceImplementations <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IState -> PDecl -> StateT IState (ExceptT Err IO) Bool
isOverlapping IState
ist) [PDecl]
superInterfaceImplementations
         forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
info) [PDecl]
undefinedSuperInterfaceImplementations

         IState
ist <- Idris IState
getIState
         -- Bring variables in implementation head into scope when building the
         -- dictionary
         let headVars :: [Name]
headVars = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PTerm -> [Name]
getHeadVars [PTerm]
ps
         let ([(Name, PTerm)]
headVarTypes, Type
ty)
                = case Name -> Context -> Maybe Type
lookupTyExact Name
iname (IState -> Context
tt_ctxt IState
ist) of
                              Just Type
ty -> (forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, IState -> Name -> Type -> PTerm
getTypeIn IState
ist Name
n Type
ty)) [Name]
headVars, Type
ty)
                              Maybe Type
_ -> (forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
headVars (forall a. a -> [a]
repeat PTerm
Placeholder), forall n. TT n
Erased)

         let impps :: [PTerm]
impps = forall {a}. IState -> [a] -> [Type] -> [PTerm]
getImpParams IState
ist (InterfaceInfo -> [Name]
interface_impparams InterfaceInfo
ci)
                          (forall a b. (a, b) -> b
snd (forall n. TT n -> (TT n, [TT n])
unApply (forall n. TT n -> TT n
substRetTy Type
ty)))
         let iimpps :: [(Name, PTerm)]
iimpps = forall a b. [a] -> [b] -> [(a, b)]
zip (InterfaceInfo -> [Name]
interface_impparams InterfaceInfo
ci) [PTerm]
impps

         Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"ImpPS: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [PTerm]
impps forall a. [a] -> [a] -> [a]
++ String
" --- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, PTerm)]
iimpps
         Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Head var types " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, PTerm)]
headVarTypes forall a. [a] -> [a] -> [a]
++ String
" from " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
ty

         let all_meths :: [Name]
all_meths = forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name
nsroot forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (a, b) -> a
fst) (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci)
         let mtys :: [(Name, FnOpts, PTerm, PTerm)]
mtys = forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, (Bool
inj, FnOpts
op, PTerm
t)) ->
                   let t_in :: PTerm
t_in = [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
substMatchesShadow ([(Name, PTerm)]
iimpps forall a. [a] -> [a] -> [a]
++ [(Name, PTerm)]
ips) [Name]
pnames PTerm
t
                       mnamemap :: [(Name, PTerm)]
mnamemap =
                          forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, FC -> PTerm -> [PArg' PTerm] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] ([Text] -> Name -> Name -> Name
decorate [Text]
ns Name
iname Name
n))
                                              (forall a b. (a -> b) -> [a] -> [b]
map (FC -> Name -> PArg' PTerm
toImp FC
fc) [Name]
headVars)))
                                      [Name]
all_meths
                       t' :: PTerm
t' = [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
substMatchesShadow [(Name, PTerm)]
mnamemap [Name]
pnames PTerm
t_in in
                       ([Text] -> Name -> Name -> Name
decorate [Text]
ns Name
iname Name
n,
                           FnOpts
op, [(Name, PTerm)] -> [(Name, PTerm)] -> PTerm -> PTerm
coninsert [(Name, PTerm)]
cs [(Name, PTerm)]
pextra PTerm
t', PTerm
t'))
              (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci)

         Int -> String -> Idris ()
logElab Int
5 (forall a. Show a => a -> String
show ([(Name, FnOpts, PTerm, PTerm)]
mtys, ([(Name, PTerm)]
iimpps forall a. [a] -> [a] -> [a]
++ [(Name, PTerm)]
ips)))
         Int -> String -> Idris ()
logElab Int
5 (String
"Before defaults: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [PDecl]
ds forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci)))
         let ds_defs :: [PDecl]
ds_defs = IState
-> Name -> [(Name, (Name, PDecl))] -> [Text] -> [PDecl] -> [PDecl]
insertDefaults IState
ist Name
iname (InterfaceInfo -> [(Name, (Name, PDecl))]
interface_defaults InterfaceInfo
ci) [Text]
ns [PDecl]
ds
         Int -> String -> Idris ()
logElab Int
3 (String
"After defaults: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [PDecl]
ds_defs forall a. [a] -> [a] -> [a]
++ String
"\n")

         let ds' :: [PDecl]
ds' = [Name] -> [PDecl] -> [PDecl]
reorderDefs (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci)) [PDecl]
ds_defs
         Int -> String -> Idris ()
logElab Int
1 (String
"Reordered: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [PDecl]
ds' forall a. [a] -> [a] -> [a]
++ String
"\n")

         forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall {t :: * -> *} {t}.
Foldable t =>
t (PDecl' t) -> [Text] -> Name -> Name -> Idris ()
warnMissing [PDecl]
ds' [Text]
ns Name
iname) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci))
         forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall {t :: * -> *}. Foldable t => t Name -> Name -> Idris ()
checkInInterface (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci))) (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl -> [Name]
defined [PDecl]
ds')
         let wbTys :: [PDecl]
wbTys = forall a b. (a -> b) -> [a] -> [b]
map forall {d}. (Name, FnOpts, PTerm, d) -> PDecl
mkTyDecl [(Name, FnOpts, PTerm, PTerm)]
mtys
         let wbVals_orig :: [PDecl]
wbVals_orig = forall a b. (a -> b) -> [a] -> [b]
map ((Name -> Name) -> PDecl -> PDecl
decorateid ([Text] -> Name -> Name -> Name
decorate [Text]
ns Name
iname)) [PDecl]
ds'
         IState
ist <- Idris IState
getIState
         let wbVals :: [PDecl]
wbVals = forall a b. (a -> b) -> [a] -> [b]
map (Bool
-> IState
-> (Name -> Name)
-> [(Name, PTerm)]
-> [Name]
-> PDecl
-> PDecl
expandParamsD Bool
False IState
ist forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [(Name, PTerm)]
pextra (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c} {d}. (a, b, c, d) -> a
methName [(Name, FnOpts, PTerm, PTerm)]
mtys)) [PDecl]
wbVals_orig

         Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"Method types " forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n" (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => a -> String
show forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. PPOption -> PDecl -> Doc OutputAnnotation
showDeclImp PPOption
verbosePPOption forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {d}. (Name, FnOpts, PTerm, d) -> PDecl
mkTyDecl) [(Name, FnOpts, PTerm, PTerm)]
mtys)
         Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"Implementation is " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [PTerm]
ps forall a. [a] -> [a] -> [a]
++ String
" implicits " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a. Eq a => [a] -> [a]
nub [[PArg' PTerm]]
wparams))

         let lhsImps :: [PArg' PTerm]
lhsImps = forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) Bool
True) [Name]
headVars

         let lhs :: PTerm
lhs = FC -> PTerm -> [PArg' PTerm] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
iname) ([PArg' PTerm]
lhsImps forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (Name -> PArg' PTerm
toExp forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.forall a b. (a, b) -> a
fst) [(Name, PTerm)]
pextra)
         let rhs :: PTerm
rhs = FC -> PTerm -> [PArg' PTerm] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (InterfaceInfo -> Name
implementationCtorName InterfaceInfo
ci))
                           (forall a b. (a -> b) -> [a] -> [b]
map (forall {t}. t -> PArg' t
pexp forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (forall {b} {c}. [PArg' PTerm] -> (Name, b, c, PTerm) -> PTerm
mkMethApp [PArg' PTerm]
lhsImps)) [(Name, FnOpts, PTerm, PTerm)]
mtys)

         Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Implementation LHS " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show FnOpts
totopts forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name]
headVars
         Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Implementation RHS " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PTerm
rhs

         Name -> Bool -> Idris ()
push_estack Name
iname Bool
True
         Int -> String -> Idris ()
logElab Int
3 (String
"Method types: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [PDecl]
wbTys)
         Int -> String -> Idris ()
logElab Int
3 (String
"Method bodies (before params): " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [PDecl]
wbVals_orig)
         Int -> String -> Idris ()
logElab Int
3 (String
"Method bodies: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [PDecl]
wbVals)

         let idecls :: [PDecl]
idecls = [forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc FnOpts
totopts Name
iname
                              [forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
iname PTerm
lhs [] PTerm
rhs []]]

         forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
info) (forall a b. (a -> b) -> [a] -> [b]
map ([(Name, PTerm)] -> PDecl -> PDecl
impBind [(Name, PTerm)]
headVarTypes) [PDecl]
wbTys)
         forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
info) [PDecl]
idecls

         Context
ctxt <- Idris Context
getContext
         let ifn_ty :: Type
ifn_ty = case Name -> Context -> Maybe Type
lookupTyExact Name
iname Context
ctxt of
                           Just Type
t -> Type
t
                           Maybe Type
Nothing -> forall a. HasCallStack => String -> a
error String
"Can't happen (interface constructor)"
         let ifn_is :: [PArg' PTerm]
ifn_is = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
iname (IState -> Ctxt [PArg' PTerm]
idris_implicits IState
ist) of
                           Just [PArg' PTerm]
t -> [PArg' PTerm]
t
                           Maybe [PArg' PTerm]
Nothing -> []
         let prop_params :: [Name]
prop_params = IState -> [Name] -> [PArg' PTerm] -> Type -> [Name]
getParamsInType IState
ist [] [PArg' PTerm]
ifn_is Type
ifn_ty

         Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"Propagating parameters to methods: "
                           forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Name
iname, [Name]
prop_params)

         let wbVals' :: [PDecl]
wbVals' = forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> PDecl -> PDecl
addParams [Name]
prop_params) [PDecl]
wbVals

         Int -> String -> Idris ()
logElab Int
5 (String
"Elaborating method bodies: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [PDecl]
wbVals')
         forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
info) [PDecl]
wbVals'

         forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC -> [(Name, (Bool, FnOpts, PTerm))] -> (PDecl, PDecl) -> Idris ()
checkInjectiveDef FC
fc (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci)) (forall a b. [a] -> [b] -> [(a, b)]
zip [PDecl]
ds' [PDecl]
wbVals')

         Idris ()
pop_estack

         [Name] -> Idris ()
setOpenImpl [Name]
oldOpen
--          totalityCheckBlock

         IBCWrite -> Idris ()
addIBC (Bool -> Bool -> Name -> Name -> IBCWrite
IBCImplementation Bool
intImpl (forall a. Maybe a -> Bool
isNothing Maybe Name
expn) Name
n Name
iname)

  where
    getImpParams :: IState -> [a] -> [Type] -> [PTerm]
getImpParams IState
ist = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\a
n Type
tm -> IState -> Type -> PTerm
delab IState
ist Type
tm)

    intImpl :: Bool
intImpl = case [PTerm]
ps of
                [PConstant FC
NoFC (AType (ATInt IntTy
ITNative))] -> Bool
True
                [PTerm]
_ -> Bool
False

    mkiname :: Name -> [String] -> [a] -> Maybe Name -> Name
mkiname Name
n' [String]
ns [a]
ps' Maybe Name
expn' =
        case Maybe Name
expn' of
          Maybe Name
Nothing -> case [String]
ns of
                          [] -> SpecialName -> Name
SN (Name -> [String] -> SpecialName
sImplementationN Name
n' (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [a]
ps'))
                          [String]
m -> Name -> [String] -> Name
sNS (SpecialName -> Name
SN (Name -> [String] -> SpecialName
sImplementationN Name
n' (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [a]
ps'))) [String]
m
          Just Name
nm -> Name
nm

    substImplementation :: [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
substImplementation [(Name, PTerm)]
ips [Name]
pnames (PImplementation Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
syn FC
_ [(Name, PTerm)]
cs [Name]
parents Accessibility
acc FnOpts
opts Name
n FC
nfc [PTerm]
ps [(Name, PTerm)]
pextra PTerm
t Maybe Name
expn [PDecl]
ds)
        = forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [(Name, t)]
-> [Name]
-> Accessibility
-> FnOpts
-> Name
-> FC
-> [t]
-> [(Name, t)]
-> t
-> Maybe Name
-> [PDecl' t]
-> PDecl' t
PImplementation Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
syn FC
fc [(Name, PTerm)]
cs [Name]
parents Accessibility
acc FnOpts
opts Name
n FC
nfc
                     (forall a b. (a -> b) -> [a] -> [b]
map ([(Name, PTerm)] -> [Name] -> PTerm -> PTerm
substMatchesShadow [(Name, PTerm)]
ips [Name]
pnames) [PTerm]
ps)
                     [(Name, PTerm)]
pextra
                     ([(Name, PTerm)] -> [Name] -> PTerm -> PTerm
substMatchesShadow [(Name, PTerm)]
ips [Name]
pnames PTerm
t) Maybe Name
expn [PDecl]
ds

    isOverlapping :: IState -> PDecl -> StateT IState (ExceptT Err IO) Bool
isOverlapping IState
i (PImplementation Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
syn FC
_ [(Name, PTerm)]
_ [Name]
_ Accessibility
_ FnOpts
_ Name
n FC
nfc [PTerm]
ps [(Name, PTerm)]
pextra PTerm
t Maybe Name
expn [PDecl]
_)
        = case forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt InterfaceInfo
idris_interfaces IState
i) of
            [(Name
n, InterfaceInfo
ci)] -> let iname :: Name
iname = (forall {a}. Show a => Name -> [String] -> [a] -> Maybe Name -> Name
mkiname Name
n (ElabInfo -> [String]
namespace ElabInfo
info) [PTerm]
ps Maybe Name
expn) in
                            case Name -> Context -> [Type]
lookupTy Name
iname (IState -> Context
tt_ctxt IState
i) of
                              [] -> IState
-> InterfaceInfo
-> Name
-> SyntaxInfo
-> PTerm
-> StateT IState (ExceptT Err IO) Bool
elabFindOverlapping IState
i InterfaceInfo
ci Name
iname SyntaxInfo
syn PTerm
t
                              (Type
_:[Type]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
            [(Name, InterfaceInfo)]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False -- couldn't find interface, just let elabImplementation fail later

    elabFindOverlapping :: IState
-> InterfaceInfo
-> Name
-> SyntaxInfo
-> PTerm
-> StateT IState (ExceptT Err IO) Bool
elabFindOverlapping IState
i InterfaceInfo
ci Name
iname SyntaxInfo
syn PTerm
t
        = do PTerm
ty' <- SyntaxInfo -> FC -> PTerm -> Idris PTerm
addUsingConstraints SyntaxInfo
syn FC
fc PTerm
t
             -- TODO think: something more in info?
             PTerm
ty' <- ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
implicit ElabInfo
info SyntaxInfo
syn Name
iname PTerm
ty'
             let ty :: PTerm
ty = [Name] -> IState -> PTerm -> PTerm
addImpl [] IState
i PTerm
ty'
             Context
ctxt <- Idris Context
getContext
             (ElabResult Type
tyT [(Name, (Int, Maybe Name, Type, [Name]))]
_ [PDecl]
_ Context
ctxt' [RDeclInstructions]
newDecls Set (FC', OutputAnnotation)
highlights Int
newGName, String
_) <-
                forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) Name
iname (forall n. UExp -> TT n
TType (Int -> UExp
UVal Int
0)) EState
initEState
                         (forall aux a.
String -> Name -> Maybe Type -> Elab' aux a -> Elab' aux a
errAt String
"type of " Name
iname forall a. Maybe a
Nothing (forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> PTerm
-> ElabD ElabResult
build IState
i ElabInfo
info ElabMode
ERHS [] Name
iname PTerm
ty)))
             Context -> Idris ()
setContext Context
ctxt'
             ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
info [RDeclInstructions]
newDecls
             Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights
             (IState -> IState) -> Idris ()
updateIState forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }

             Context
ctxt <- Idris Context
getContext
             (Type
cty, Type
_) <- String
-> FC
-> (Err -> Err)
-> Env
-> Type
-> StateT IState (ExceptT Err IO) (Type, Type)
recheckC (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] Type
tyT
             let nty :: Type
nty = Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
cty
             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Maybe a -> Bool
isJust forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {t :: * -> *} {a}.
(Foldable t, Eq a, Num a, Enum a) =>
IState -> t a -> PTerm -> Name -> Maybe PTerm
findOverlapping IState
i (InterfaceInfo -> [Int]
interface_determiners InterfaceInfo
ci) (IState -> Type -> PTerm
delab IState
i Type
nty)) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ InterfaceInfo -> [(Name, Bool)]
interface_implementations InterfaceInfo
ci)

    findOverlapping :: IState -> t a -> PTerm -> Name -> Maybe PTerm
findOverlapping IState
i t a
dets PTerm
t Name
n
     | SN (ParentN Name
_ Text
_) <- Name
n = forall a. Maybe a
Nothing
     | Just FnOpts
opts <- forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt FnOpts
idris_flags IState
i),
       FnOpt
OverlappingDictionary forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts = forall a. Maybe a
Nothing
     | Bool
otherwise
        = case Name -> Context -> [Type]
lookupTy Name
n (IState -> Context
tt_ctxt IState
i) of
            [Type
t'] -> let tret :: PTerm
tret = PTerm -> PTerm
getRetType PTerm
t
                        tret' :: PTerm
tret' = PTerm -> PTerm
getRetType (IState -> Type -> PTerm
delab IState
i Type
t') in
                        case forall {t :: * -> *} {a}.
(Foldable t, Eq a, Num a, Enum a) =>
IState
-> t a -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchArgs IState
i t a
dets PTerm
tret' PTerm
tret of
                           Right [(Name, PTerm)]
_ -> forall a. a -> Maybe a
Just PTerm
tret'
                           Left (PTerm, PTerm)
_ -> case forall {t :: * -> *} {a}.
(Foldable t, Eq a, Num a, Enum a) =>
IState
-> t a -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchArgs IState
i t a
dets PTerm
tret PTerm
tret' of
                                       Right [(Name, PTerm)]
_ -> forall a. a -> Maybe a
Just PTerm
tret'
                                       Left (PTerm, PTerm)
_ -> forall a. Maybe a
Nothing
            [Type]
_ -> forall a. Maybe a
Nothing
    overlapping :: a -> Idris a
overlapping a
t' = forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
                          String
"Overlapping implementation: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
t' forall a. [a] -> [a] -> [a]
++ String
" already defined"))
    getRetType :: PTerm -> PTerm
getRetType (PPi Plicity
_ Name
_ FC
_ PTerm
_ PTerm
sc) = PTerm -> PTerm
getRetType PTerm
sc
    getRetType PTerm
t = PTerm
t

    matchArgs :: IState
-> t a -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchArgs IState
i t a
dets PTerm
x PTerm
y =
        let x' :: PTerm
x' = forall {t :: * -> *} {a}.
(Foldable t, Eq a, Num a, Enum a) =>
t a -> PTerm -> PTerm
keepDets t a
dets PTerm
x
            y' :: PTerm
y' = forall {t :: * -> *} {a}.
(Foldable t, Eq a, Num a, Enum a) =>
t a -> PTerm -> PTerm
keepDets t a
dets PTerm
y in
            IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchClause IState
i PTerm
x' PTerm
y'

    keepDets :: t a -> PTerm -> PTerm
keepDets t a
dets (PApp FC
fc PTerm
f [PArg' PTerm]
args)
        = FC -> PTerm -> [PArg' PTerm] -> PTerm
PApp FC
fc PTerm
f forall a b. (a -> b) -> a -> b
$ let a' :: [(a, PArg' PTerm)]
a' = forall a b. [a] -> [b] -> [(a, b)]
zip [a
0..] [PArg' PTerm]
args in
              forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (forall a. (a -> Bool) -> [a] -> [a]
filter (\(a
i, PArg' PTerm
_) -> a
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
dets) [(a, PArg' PTerm)]
a')
    keepDets t a
dets PTerm
t = PTerm
t

    methName :: (a, b, c, d) -> a
methName (a
n, b
_, c
_, d
_) = a
n
    toExp :: Name -> PArg' PTerm
toExp Name
n = forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n)

    mkMethApp :: [PArg' PTerm] -> (Name, b, c, PTerm) -> PTerm
mkMethApp [PArg' PTerm]
ps (Name
n, b
_, c
_, PTerm
ty)
              = Int -> PTerm -> PTerm -> PTerm
lamBind Int
0 PTerm
ty (FC -> PTerm -> [PArg' PTerm] -> PTerm
papp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n)
                     ([PArg' PTerm]
ps forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (Name -> PArg' PTerm
toExp forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (a, b) -> a
fst) [(Name, PTerm)]
pextra forall a. [a] -> [a] -> [a]
++ Int -> PTerm -> [PArg' PTerm]
methArgs Int
0 PTerm
ty))

    lamBind :: Int -> PTerm -> PTerm -> PTerm
lamBind Int
i (PPi (Constraint [ArgOpt]
_ Static
_ RigCount
_) Name
_ FC
_ PTerm
_ PTerm
sc) PTerm
sc'
          = FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> String -> Name
sMN Int
i String
"meth") FC
NoFC PTerm
Placeholder (Int -> PTerm -> PTerm -> PTerm
lamBind (Int
iforall a. Num a => a -> a -> a
+Int
1) PTerm
sc PTerm
sc')
    lamBind Int
i (PPi Plicity
_ Name
n FC
_ PTerm
ty PTerm
sc) PTerm
sc'
          = FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> String -> Name
sMN Int
i String
"meth") FC
NoFC PTerm
Placeholder (Int -> PTerm -> PTerm -> PTerm
lamBind (Int
iforall a. Num a => a -> a -> a
+Int
1) PTerm
sc PTerm
sc')
    lamBind Int
i PTerm
_ PTerm
sc = PTerm
sc
    methArgs :: Int -> PTerm -> [PArg' PTerm]
methArgs Int
i (PPi (Imp [ArgOpt]
_ Static
_ Bool
_ Maybe ImplicitInfo
_ Bool
_ RigCount
_) Name
n FC
_ PTerm
ty PTerm
sc)
        = forall t. Int -> Bool -> [ArgOpt] -> Name -> t -> PArg' t
PImp Int
0 Bool
True [] Name
n (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> String -> Name
sMN Int
i String
"meth")) forall a. a -> [a] -> [a]
: Int -> PTerm -> [PArg' PTerm]
methArgs (Int
iforall a. Num a => a -> a -> a
+Int
1) PTerm
sc
    methArgs Int
i (PPi (Exp [ArgOpt]
_ Static
_ Bool
_ RigCount
_) Name
n FC
_ PTerm
ty PTerm
sc)
        = forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp Int
0 [] (Int -> String -> Name
sMN Int
0 String
"marg") (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> String -> Name
sMN Int
i String
"meth")) forall a. a -> [a] -> [a]
: Int -> PTerm -> [PArg' PTerm]
methArgs (Int
iforall a. Num a => a -> a -> a
+Int
1) PTerm
sc
    methArgs Int
i (PPi (Constraint [ArgOpt]
_ Static
_ RigCount
_) Name
n FC
_ PTerm
ty PTerm
sc)
        = forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PConstraint Int
0 [] (Int -> String -> Name
sMN Int
0 String
"marg") (FC -> PTerm
PResolveTC FC
fc) forall a. a -> [a] -> [a]
: Int -> PTerm -> [PArg' PTerm]
methArgs (Int
iforall a. Num a => a -> a -> a
+Int
1) PTerm
sc
    methArgs Int
i PTerm
_ = []

    papp :: FC -> PTerm -> [PArg' PTerm] -> PTerm
papp FC
fc PTerm
f [] = PTerm
f
    papp FC
fc PTerm
f [PArg' PTerm]
as = FC -> PTerm -> [PArg' PTerm] -> PTerm
PApp FC
fc PTerm
f [PArg' PTerm]
as

    getWParams :: [PTerm] -> StateT IState (ExceptT Err IO) [PArg' PTerm]
getWParams [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
    getWParams (PTerm
p : [PTerm]
ps)
      | PRef FC
_ [FC]
_ Name
n <- PTerm
p
        = do [PArg' PTerm]
ps' <- [PTerm] -> StateT IState (ExceptT Err IO) [PArg' PTerm]
getWParams [PTerm]
ps
             Context
ctxt <- Idris Context
getContext
             case Name -> Context -> [Type]
lookupP Name
n Context
ctxt of
                [] -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) Bool
True forall a. a -> [a] -> [a]
: [PArg' PTerm]
ps')
                [Type]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return [PArg' PTerm]
ps'
    getWParams (PTerm
_ : [PTerm]
ps) = [PTerm] -> StateT IState (ExceptT Err IO) [PArg' PTerm]
getWParams [PTerm]
ps

    decorate :: [Text] -> Name -> Name -> Name
decorate [Text]
ns Name
iname (NS (UN Text
nm) [Text]
s)
         = Name -> [Text] -> Name
NS (SpecialName -> Name
SN (Int -> Name -> Name -> SpecialName
WhereN Int
0 Name
iname (SpecialName -> Name
SN (Name -> SpecialName
MethodN (Text -> Name
UN Text
nm))))) [Text]
ns
    decorate [Text]
ns Name
iname Name
nm
         = Name -> [Text] -> Name
NS (SpecialName -> Name
SN (Int -> Name -> Name -> SpecialName
WhereN Int
0 Name
iname (SpecialName -> Name
SN (Name -> SpecialName
MethodN Name
nm)))) [Text]
ns

    mkTyDecl :: (Name, FnOpts, PTerm, d) -> PDecl
mkTyDecl (Name
n, FnOpts
op, PTerm
t, d
_)
        = forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> t
-> PDecl' t
PTy forall a. Docstring a
emptyDocstring [] SyntaxInfo
syn FC
fc FnOpts
op Name
n FC
NoFC
               ([Name] -> [(Name, Name)] -> PTerm -> PTerm
mkUniqueNames [] [] PTerm
t)

    conbind :: [(Name, PTerm)] -> PTerm -> PTerm
    conbind :: [(Name, PTerm)] -> PTerm -> PTerm
conbind ((Name
c,PTerm
ty) : [(Name, PTerm)]
ns) PTerm
x = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
constraint Name
c FC
NoFC PTerm
ty ([(Name, PTerm)] -> PTerm -> PTerm
conbind [(Name, PTerm)]
ns PTerm
x)
    conbind [] PTerm
x = PTerm
x

    extrabind :: [(Name, PTerm)] -> PTerm -> PTerm
    extrabind :: [(Name, PTerm)] -> PTerm -> PTerm
extrabind ((Name
c,PTerm
ty) : [(Name, PTerm)]
ns) PTerm
x = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
expl Name
c FC
NoFC PTerm
ty ([(Name, PTerm)] -> PTerm -> PTerm
extrabind [(Name, PTerm)]
ns PTerm
x)
    extrabind [] PTerm
x = PTerm
x

    coninsert :: [(Name, PTerm)] -> [(Name, PTerm)] -> PTerm -> PTerm
    coninsert :: [(Name, PTerm)] -> [(Name, PTerm)] -> PTerm -> PTerm
coninsert [(Name, PTerm)]
cs [(Name, PTerm)]
ex (PPi p :: Plicity
p@(Imp [ArgOpt]
_ Static
_ Bool
_ Maybe ImplicitInfo
_ Bool
_ RigCount
_) Name
n FC
fc PTerm
t PTerm
sc) = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p Name
n FC
fc PTerm
t ([(Name, PTerm)] -> [(Name, PTerm)] -> PTerm -> PTerm
coninsert [(Name, PTerm)]
cs [(Name, PTerm)]
ex PTerm
sc)
    coninsert [(Name, PTerm)]
cs [(Name, PTerm)]
ex PTerm
sc = [(Name, PTerm)] -> PTerm -> PTerm
conbind [(Name, PTerm)]
cs ([(Name, PTerm)] -> PTerm -> PTerm
extrabind [(Name, PTerm)]
ex PTerm
sc)

    -- Reorder declarations to be in the same order as defined in the
    -- interface declaration (important so that we insert default definitions
    -- in the right place, and so that dependencies between methods are
    -- respected)
    reorderDefs :: [Name] -> [PDecl] -> [PDecl]
    reorderDefs :: [Name] -> [PDecl] -> [PDecl]
reorderDefs [Name]
ns [] = []
    reorderDefs [] [PDecl]
ds = [PDecl]
ds
    reorderDefs (Name
n : [Name]
ns) [PDecl]
ds = case forall {t}.
Name -> [PDecl' t] -> [PDecl' t] -> Maybe (PDecl' t, [PDecl' t])
pick Name
n [] [PDecl]
ds of
                                  Just (PDecl
def, [PDecl]
ds') -> PDecl
def forall a. a -> [a] -> [a]
: [Name] -> [PDecl] -> [PDecl]
reorderDefs [Name]
ns [PDecl]
ds'
                                  Maybe (PDecl, [PDecl])
Nothing -> [Name] -> [PDecl] -> [PDecl]
reorderDefs [Name]
ns [PDecl]
ds

    pick :: Name -> [PDecl' t] -> [PDecl' t] -> Maybe (PDecl' t, [PDecl' t])
pick Name
n [PDecl' t]
acc [] = forall a. Maybe a
Nothing
    pick Name
n [PDecl' t]
acc (def :: PDecl' t
def@(PClauses FC
_ FnOpts
_ Name
cn [PClause' t]
cs) : [PDecl' t]
ds)
         | Name -> Name
nsroot Name
n forall a. Eq a => a -> a -> Bool
== Name -> Name
nsroot Name
cn = forall a. a -> Maybe a
Just (PDecl' t
def, [PDecl' t]
acc forall a. [a] -> [a] -> [a]
++ [PDecl' t]
ds)
    pick Name
n [PDecl' t]
acc (PDecl' t
d : [PDecl' t]
ds) = Name -> [PDecl' t] -> [PDecl' t] -> Maybe (PDecl' t, [PDecl' t])
pick Name
n ([PDecl' t]
acc forall a. [a] -> [a] -> [a]
++ [PDecl' t
d]) [PDecl' t]
ds

    insertDefaults :: IState -> Name ->
                      [(Name, (Name, PDecl))] -> [T.Text] ->
                      [PDecl] -> [PDecl]
    insertDefaults :: IState
-> Name -> [(Name, (Name, PDecl))] -> [Text] -> [PDecl] -> [PDecl]
insertDefaults IState
i Name
iname [] [Text]
ns [PDecl]
ds = [PDecl]
ds
    insertDefaults IState
i Name
iname ((Name
n,(Name
dn, PDecl
clauses)) : [(Name, (Name, PDecl))]
defs) [Text]
ns [PDecl]
ds
       = IState
-> Name -> [(Name, (Name, PDecl))] -> [Text] -> [PDecl] -> [PDecl]
insertDefaults IState
i Name
iname [(Name, (Name, PDecl))]
defs [Text]
ns (IState
-> Name -> Name -> PDecl -> [Text] -> Name -> [PDecl] -> [PDecl]
insertDef IState
i Name
n Name
dn PDecl
clauses [Text]
ns Name
iname [PDecl]
ds)

    insertDef :: IState
-> Name -> Name -> PDecl -> [Text] -> Name -> [PDecl] -> [PDecl]
insertDef IState
i Name
meth Name
def PDecl
clauses [Text]
ns Name
iname [PDecl]
decls
        | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall {t}. Name -> Name -> [Text] -> PDecl' t -> Bool
clauseFor Name
meth Name
iname [Text]
ns) [PDecl]
decls
            = let newd :: PDecl
newd = Bool
-> IState
-> (Name -> Name)
-> [(Name, PTerm)]
-> [Name]
-> PDecl
-> PDecl
expandParamsD Bool
False IState
i (\Name
n -> Name
meth) [] [Name
def] PDecl
clauses in
                  -- trace (show newd) $
                  [PDecl]
decls forall a. [a] -> [a] -> [a]
++ [PDecl
newd]
        | Bool
otherwise = [PDecl]
decls

    warnMissing :: t (PDecl' t) -> [Text] -> Name -> Name -> Idris ()
warnMissing t (PDecl' t)
decls [Text]
ns Name
iname Name
meth
        | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall {t}. Name -> Name -> [Text] -> PDecl' t -> Bool
clauseFor Name
meth Name
iname [Text]
ns) t (PDecl' t)
decls
            = FC -> Doc OutputAnnotation -> Idris ()
iWarn FC
fc forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a. String -> Doc a
text forall a b. (a -> b) -> a -> b
$ String
"method " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
meth forall a. [a] -> [a] -> [a]
++ String
" not defined"
        | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return ()

    checkInInterface :: t Name -> Name -> Idris ()
checkInInterface t Name
ns Name
meth
        | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> Name -> Bool
eqRoot Name
meth) t Name
ns = forall (m :: * -> *) a. Monad m => a -> m a
return ()
        | Bool
otherwise = forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
                                forall a. Show a => a -> String
show Name
meth forall a. [a] -> [a] -> [a]
++ String
" not a method of interface " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n))

    eqRoot :: Name -> Name -> Bool
eqRoot Name
x Name
y = Name -> Name
nsroot Name
x forall a. Eq a => a -> a -> Bool
== Name -> Name
nsroot Name
y

    clauseFor :: Name -> Name -> [Text] -> PDecl' t -> Bool
clauseFor Name
m Name
iname [Text]
ns (PClauses FC
_ FnOpts
_ Name
m' [PClause' t]
_)
       = [Text] -> Name -> Name -> Name
decorate [Text]
ns Name
iname Name
m forall a. Eq a => a -> a -> Bool
== [Text] -> Name -> Name -> Name
decorate [Text]
ns Name
iname Name
m'
    clauseFor Name
m Name
iname [Text]
ns PDecl' t
_ = Bool
False

getHeadVars :: PTerm -> [Name]
getHeadVars :: PTerm -> [Name]
getHeadVars (PRef FC
_ [FC]
_ Name
n) | Name -> Bool
implicitable Name
n = [Name
n]
getHeadVars (PApp FC
_ PTerm
_ [PArg' PTerm]
args) = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PTerm -> [Name]
getHeadVars (forall a b. (a -> b) -> [a] -> [b]
map forall t. PArg' t -> t
getTm [PArg' PTerm]
args)
getHeadVars (PPair FC
_ [FC]
_ PunInfo
_ PTerm
l PTerm
r) = PTerm -> [Name]
getHeadVars PTerm
l forall a. [a] -> [a] -> [a]
++ PTerm -> [Name]
getHeadVars PTerm
r
getHeadVars (PDPair FC
_ [FC]
_ PunInfo
_ PTerm
l PTerm
t PTerm
r) = PTerm -> [Name]
getHeadVars PTerm
l forall a. [a] -> [a] -> [a]
++ PTerm -> [Name]
getHeadVars PTerm
t forall a. [a] -> [a] -> [a]
++ PTerm -> [Name]
getHeadVars PTerm
t
getHeadVars PTerm
_ = []

-- | Implicitly bind variables from the implementation head in method types
impBind :: [(Name, PTerm)] -> PDecl -> PDecl
impBind :: [(Name, PTerm)] -> PDecl -> PDecl
impBind [(Name, PTerm)]
vs (PTy Docstring (Either Err PTerm)
d [(Name, Docstring (Either Err PTerm))]
ds SyntaxInfo
syn FC
fc FnOpts
opts Name
n FC
fc' PTerm
t)
     = forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> t
-> PDecl' t
PTy Docstring (Either Err PTerm)
d [(Name, Docstring (Either Err PTerm))]
ds SyntaxInfo
syn FC
fc FnOpts
opts Name
n FC
fc'
          ([(Name, PTerm)] -> PTerm -> PTerm
doImpBind (forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n, PTerm
ty) -> Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` PTerm -> [Name]
boundIn PTerm
t) [(Name, PTerm)]
vs) PTerm
t)
  where
    doImpBind :: [(Name, PTerm)] -> PTerm -> PTerm
doImpBind [] PTerm
ty = PTerm
ty
    doImpBind ((Name
n, PTerm
argty) : [(Name, PTerm)]
ns) PTerm
ty
       = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
impl Name
n FC
NoFC PTerm
argty ([(Name, PTerm)] -> PTerm -> PTerm
doImpBind [(Name, PTerm)]
ns PTerm
ty)

    boundIn :: PTerm -> [Name]
boundIn (PPi Plicity
_ Name
n FC
_ PTerm
_ PTerm
sc) = Name
n forall a. a -> [a] -> [a]
: PTerm -> [Name]
boundIn PTerm
sc
    boundIn PTerm
_ = []

getTypeIn :: IState -> Name -> Type -> PTerm
getTypeIn :: IState -> Name -> Type -> PTerm
getTypeIn IState
ist Name
n (Bind Name
x Binder Type
b Type
sc)
    | Name
n forall a. Eq a => a -> a -> Bool
== Name
x = IState -> Type -> PTerm
delab IState
ist (forall b. Binder b -> b
binderTy Binder Type
b)
    | Bool
otherwise = IState -> Name -> Type -> PTerm
getTypeIn IState
ist Name
n (forall n. TT n -> TT n -> TT n
substV (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
x forall n. TT n
Erased) Type
sc)
getTypeIn IState
ist Name
n Type
tm = PTerm
Placeholder

toImp :: FC -> Name -> PArg' PTerm
toImp FC
fc Name
n = forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) Bool
True

-- | Propagate interface parameters to method bodies, if they're not
-- already there, and they are needed (i.e. appear in method's type)
addParams :: [Name] -> PDecl -> PDecl
addParams :: [Name] -> PDecl -> PDecl
addParams [Name]
ps (PClauses FC
fc FnOpts
opts Name
n [PClause' PTerm]
cs) = forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc FnOpts
opts Name
n (forall a b. (a -> b) -> [a] -> [b]
map PClause' PTerm -> PClause' PTerm
addCParams [PClause' PTerm]
cs)
  where
    addCParams :: PClause' PTerm -> PClause' PTerm
addCParams (PClause FC
fc Name
n PTerm
lhs [PTerm]
ws PTerm
rhs [PDecl]
wb)
        = forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
n ([Name] -> PTerm -> PTerm
addTmParams ([Name] -> [Name] -> [Name]
dropPs (PTerm -> [Name]
allNamesIn PTerm
lhs) [Name]
ps) PTerm
lhs) [PTerm]
ws PTerm
rhs [PDecl]
wb
    addCParams (PWith FC
fc Name
n PTerm
lhs [PTerm]
ws PTerm
sc Maybe (Name, FC)
pn [PDecl]
ds)
        = forall t.
FC
-> Name
-> t
-> [t]
-> t
-> Maybe (Name, FC)
-> [PDecl' t]
-> PClause' t
PWith FC
fc Name
n ([Name] -> PTerm -> PTerm
addTmParams ([Name] -> [Name] -> [Name]
dropPs (PTerm -> [Name]
allNamesIn PTerm
lhs) [Name]
ps) PTerm
lhs) [PTerm]
ws PTerm
sc Maybe (Name, FC)
pn
                      (forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> PDecl -> PDecl
addParams [Name]
ps) [PDecl]
ds)
    addCParams PClause' PTerm
c = PClause' PTerm
c

    addTmParams :: [Name] -> PTerm -> PTerm
addTmParams [Name]
ps (PRef FC
fc [FC]
hls Name
n)
        = FC -> PTerm -> [PArg' PTerm] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC]
hls Name
n) (forall a b. (a -> b) -> [a] -> [b]
map (FC -> Name -> PArg' PTerm
toImp FC
fc) [Name]
ps)
    addTmParams [Name]
ps (PApp FC
fc ap :: PTerm
ap@(PRef FC
fc' [FC]
hls Name
n) [PArg' PTerm]
args)
        = FC -> PTerm -> [PArg' PTerm] -> PTerm
PApp FC
fc PTerm
ap (forall {t}. [PArg' t] -> [PArg' t] -> [PArg' t]
mergePs (forall a b. (a -> b) -> [a] -> [b]
map (FC -> Name -> PArg' PTerm
toImp FC
fc) [Name]
ps) [PArg' PTerm]
args)
    addTmParams [Name]
ps PTerm
tm = PTerm
tm

    mergePs :: [PArg' t] -> [PArg' t] -> [PArg' t]
mergePs [] [PArg' t]
args = [PArg' t]
args
    mergePs (PArg' t
p : [PArg' t]
ps) [PArg' t]
args
         | forall {t}. PArg' t -> Bool
isImplicit PArg' t
p,
           forall t. PArg' t -> Name
pname PArg' t
p forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall a b. (a -> b) -> [a] -> [b]
map forall t. PArg' t -> Name
pname [PArg' t]
args
               = PArg' t
p forall a. a -> [a] -> [a]
: [PArg' t] -> [PArg' t] -> [PArg' t]
mergePs [PArg' t]
ps [PArg' t]
args
       where
         isImplicit :: PArg' t -> Bool
isImplicit (PExp{}) = Bool
False
         isImplicit PArg' t
_ = Bool
True
    mergePs (PArg' t
p : [PArg' t]
ps) [PArg' t]
args
         = [PArg' t] -> [PArg' t] -> [PArg' t]
mergePs [PArg' t]
ps [PArg' t]
args

    -- Don't propagate a parameter if the name is rebound explicitly
    dropPs :: [Name] -> [Name] -> [Name]
    dropPs :: [Name] -> [Name] -> [Name]
dropPs [Name]
ns = forall a. (a -> Bool) -> [a] -> [a]
filter (\Name
x -> Name
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
ns)

addParams [Name]
ps PDecl
d = PDecl
d

-- | Check a given method definition is injective, if the interface info
-- says it needs to be.  Takes originally written decl and the one
-- with name decoration, so we know which name to look up.
checkInjectiveDef :: FC -> [(Name, (Bool, FnOpts, PTerm))] ->
                           (PDecl, PDecl) -> Idris ()
checkInjectiveDef :: FC -> [(Name, (Bool, FnOpts, PTerm))] -> (PDecl, PDecl) -> Idris ()
checkInjectiveDef FC
fc [(Name, (Bool, FnOpts, PTerm))]
ns (PClauses FC
_ FnOpts
_ Name
n [PClause' PTerm]
cs, PClauses FC
_ FnOpts
_ Name
elabn [PClause' PTerm]
_)
   | Just (Bool
True, FnOpts
_, PTerm
_) <- forall {a}. Name -> [(Name, a)] -> Maybe a
clookup Name
n [(Name, (Bool, FnOpts, PTerm))]
ns
          = do IState
ist <- Idris IState
getIState
               case Name -> Context -> Maybe Def
lookupDefExact Name
elabn (IState -> Context
tt_ctxt IState
ist) of
                    Just (CaseOp CaseInfo
_ Type
_ [(Type, Bool)]
_ [Either Type (Type, Type)]
_ [([Name], Type, Type)]
_ CaseDefs
cdefs) ->
                       IState -> SC' Type -> Idris ()
checkInjectiveCase IState
ist (forall a b. (a, b) -> b
snd (CaseDefs -> ([Name], SC' Type)
cases_compiletime CaseDefs
cdefs))
  where
    checkInjectiveCase :: IState -> SC' Type -> Idris ()
checkInjectiveCase IState
ist (STerm Type
tm)
         = IState -> Type -> Idris ()
checkInjectiveApp IState
ist (forall a b. (a, b) -> a
fst (forall n. TT n -> (TT n, [TT n])
unApply Type
tm))
    checkInjectiveCase IState
_ SC' Type
_ = forall {a}. Idris a
notifail

    checkInjectiveApp :: IState -> Type -> Idris ()
checkInjectiveApp IState
ist (P (TCon Int
_ Int
_) Name
n Type
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
    checkInjectiveApp IState
ist (P (DCon Int
_ Int
_ Bool
_) Name
n Type
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
    checkInjectiveApp IState
ist (P NameType
Ref Name
n Type
_)
        | Just Bool
True <- Name -> Context -> Maybe Bool
lookupInjectiveExact Name
n (IState -> Context
tt_ctxt IState
ist) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
    checkInjectiveApp IState
ist (P NameType
Ref Name
n Type
_) = forall {a}. Idris a
notifail
    checkInjectiveApp IState
_ Type
_ = forall {a}. Idris a
notifail

    notifail :: Idris a
notifail = forall a. Err -> Idris a
ierror forall a b. (a -> b) -> a -> b
$ forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Err' t
Msg (forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" must be defined by a type or data constructor"))

    clookup :: Name -> [(Name, a)] -> Maybe a
clookup Name
n [] = forall a. Maybe a
Nothing
    clookup Name
n ((Name
n', a
d) : [(Name, a)]
ds) | Name -> Name
nsroot Name
n forall a. Eq a => a -> a -> Bool
== Name -> Name
nsroot Name
n' = forall a. a -> Maybe a
Just a
d
                             | Bool
otherwise = forall a. Maybe a
Nothing
checkInjectiveDef FC
fc [(Name, (Bool, FnOpts, PTerm))]
ns (PDecl, PDecl)
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()

checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()
checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()
checkInjectiveArgs FC
fc Name
n [Int]
ds Maybe Type
Nothing = forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkInjectiveArgs FC
fc Name
n [Int]
ds (Just Type
ty)
   = do IState
ist <- Idris IState
getIState
        let (Type
_, [Type]
args) = forall n. TT n -> (TT n, [TT n])
unApply (forall n. TT n -> TT n
instantiateRetTy Type
ty)
        Int -> IState -> [Type] -> Idris ()
ci Int
0 IState
ist [Type]
args
  where
    ci :: Int -> IState -> [Type] -> Idris ()
ci Int
i IState
ist (Type
a : [Type]
as) | Int
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
ds
       = if IState -> Type -> Bool
isInj IState
ist Type
a then Int -> IState -> [Type] -> Idris ()
ci (Int
i forall a. Num a => a -> a -> a
+ Int
1) IState
ist [Type]
as
            else forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. Name -> t -> Err' t
InvalidTCArg Name
n Type
a))
    ci Int
i IState
ist (Type
a : [Type]
as) = Int -> IState -> [Type] -> Idris ()
ci (Int
i forall a. Num a => a -> a -> a
+ Int
1) IState
ist [Type]
as
    ci Int
i IState
ist [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()

    isInj :: IState -> Type -> Bool
isInj IState
i (P NameType
Bound Name
n Type
_) = Bool
True
    isInj IState
i (P NameType
_ Name
n Type
_) = Name -> Context -> Bool
isConName Name
n (IState -> Context
tt_ctxt IState
i)
    isInj IState
i (App AppStatus Name
_ Type
f Type
a) = IState -> Type -> Bool
isInj IState
i Type
f Bool -> Bool -> Bool
&& IState -> Type -> Bool
isInj IState
i Type
a
    isInj IState
i (V Int
_) = Bool
True
    isInj IState
i (Bind Name
n b :: Binder Type
b@(Pi{}) Type
sc) = IState -> Type -> Bool
isInj IState
i (forall b. Binder b -> b
binderTy Binder Type
b) Bool -> Bool -> Bool
&& IState -> Type -> Bool
isInj IState
i Type
sc
    isInj IState
i (Bind Name
n Binder Type
b Type
sc) = Bool
False
    isInj IState
_ Type
_ = Bool
True

    instantiateRetTy :: TT n -> TT n
instantiateRetTy (Bind n
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT n
_ TT n
_) TT n
sc)
       = forall n. TT n -> TT n -> TT n
substV (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
n forall n. TT n
Erased) (TT n -> TT n
instantiateRetTy TT n
sc)
    instantiateRetTy TT n
t = TT n
t