{-|
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 Name -> Ctxt InterfaceInfo -> [(Name, InterfaceInfo)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
                  [(Name, InterfaceInfo)
c] -> (Name, InterfaceInfo)
-> StateT IState (ExceptT Err IO) (Name, InterfaceInfo)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name, InterfaceInfo)
c
                  [] -> String -> StateT IState (ExceptT Err IO) (Name, InterfaceInfo)
forall a. String -> Idris a
ifail (String -> StateT IState (ExceptT Err IO) (Name, InterfaceInfo))
-> String -> StateT IState (ExceptT Err IO) (Name, InterfaceInfo)
forall a b. (a -> b) -> a -> b
$ FC -> String
forall a. Show a => a -> String
show FC
fc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not an interface"
                  [(Name, InterfaceInfo)]
cs -> TC (Name, InterfaceInfo)
-> StateT IState (ExceptT Err IO) (Name, InterfaceInfo)
forall a. TC a -> Idris a
tclift (TC (Name, InterfaceInfo)
 -> StateT IState (ExceptT Err IO) (Name, InterfaceInfo))
-> TC (Name, InterfaceInfo)
-> StateT IState (ExceptT Err IO) (Name, InterfaceInfo)
forall a b. (a -> b) -> a -> b
$ Err -> TC (Name, InterfaceInfo)
forall a. Err -> TC a
tfail (Err -> TC (Name, InterfaceInfo))
-> Err -> TC (Name, InterfaceInfo)
forall a b. (a -> b) -> a -> b
$ FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc
                           ([Name] -> Err
forall t. [Name] -> Err' t
CantResolveAlts (((Name, InterfaceInfo) -> Name)
-> [(Name, InterfaceInfo)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, InterfaceInfo) -> Name
forall a b. (a, b) -> a
fst [(Name, InterfaceInfo)]
cs))
    let iname :: Name
iname = Name -> [String] -> [PTerm] -> Maybe Name -> Name
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 = addDef iname acc (hide_list ist) })
    IState
ist <- Idris IState
getIState

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

    let emptyinterface :: Bool
emptyinterface = [(Name, (Bool, FnOpts, PTerm))] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci)
    Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ElabWhat
what ElabWhat -> ElabWhat -> Bool
forall a. Eq a => a -> a -> Bool
/= ElabWhat
EDefns) (Idris () -> Idris ()) -> Idris () -> Idris ()
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 FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` FnOpts
opts ->
                       do (Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Idris () -> (PTerm -> Idris ()) -> Maybe PTerm -> Idris ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) PTerm -> Idris ()
forall {a} {a}. Show a => a -> Idris a
overlapping (Maybe PTerm -> Idris ())
-> (Name -> Maybe PTerm) -> Name -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IState -> [Int] -> PTerm -> Name -> Maybe PTerm
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))
                                (((Name, Bool) -> Name) -> [(Name, Bool)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Bool) -> Name
forall a b. (a, b) -> a
fst ([(Name, Bool)] -> [Name]) -> [(Name, Bool)] -> [Name]
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
    Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe Name -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Name
expn) (Idris () -> Idris ()) -> Idris () -> Idris ()
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))

    Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ElabWhat
what ElabWhat -> ElabWhat -> Bool
forall a. Eq a => a -> a -> Bool
/= ElabWhat
ETypes Bool -> Bool -> Bool
&& (Bool -> Bool
not ([PDecl] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PDecl]
ds Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
emptyinterface))) (Idris () -> Idris ()) -> Idris () -> Idris ()
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 = [Name] -> [PTerm] -> [(Name, PTerm)]
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 <- (PTerm -> StateT IState (ExceptT Err IO) [PArg' PTerm])
-> [PTerm] -> StateT IState (ExceptT Err IO) [[PArg' PTerm]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\PTerm
p -> case PTerm
p of
                                  PApp FC
_ PTerm
_ [PArg' PTerm]
args -> [PTerm] -> StateT IState (ExceptT Err IO) [PArg' PTerm]
getWParams ((PArg' PTerm -> PTerm) -> [PArg' PTerm] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PArg' PTerm -> PTerm
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
_ -> [PArg' PTerm] -> StateT IState (ExceptT Err IO) [PArg' PTerm]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []) [PTerm]
ps
         IState
ist <- Idris IState
getIState
         let pnames :: [Name]
pnames = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ (PArg' PTerm -> Name) -> [PArg' PTerm] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map PArg' PTerm -> Name
forall t. PArg' t -> Name
pname ([[PArg' PTerm]] -> [PArg' PTerm]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[PArg' PTerm]] -> [[PArg' PTerm]]
forall a. Eq a => [a] -> [a]
nub [[PArg' PTerm]]
wparams)) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
                          (PTerm -> [Name]) -> [PTerm] -> [Name]
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 = (PDecl -> PDecl) -> [PDecl] -> [PDecl]
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 <- (PDecl -> StateT IState (ExceptT Err IO) Bool)
-> [PDecl] -> StateT IState (ExceptT Err IO) [PDecl]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((Bool -> Bool)
-> StateT IState (ExceptT Err IO) Bool
-> StateT IState (ExceptT Err IO) Bool
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not (StateT IState (ExceptT Err IO) Bool
 -> StateT IState (ExceptT Err IO) Bool)
-> (PDecl -> StateT IState (ExceptT Err IO) Bool)
-> PDecl
-> StateT IState (ExceptT Err IO) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
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
         (PDecl -> Idris ()) -> [PDecl] -> Idris ()
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 = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ (PTerm -> [Name]) -> [PTerm] -> [Name]
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 -> ((Name -> (Name, PTerm)) -> [Name] -> [(Name, PTerm)]
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
_ -> ([Name] -> [PTerm] -> [(Name, PTerm)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
headVars (PTerm -> [PTerm]
forall a. a -> [a]
repeat PTerm
Placeholder), Type
forall n. TT n
Erased)

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

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

         let all_meths :: [Name]
all_meths = ((Name, (Bool, FnOpts, PTerm)) -> Name)
-> [(Name, (Bool, FnOpts, PTerm))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name
nsroot (Name -> Name)
-> ((Name, (Bool, FnOpts, PTerm)) -> Name)
-> (Name, (Bool, FnOpts, PTerm))
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Name, (Bool, FnOpts, PTerm)) -> Name
forall a b. (a, b) -> a
fst) (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci)
         let mtys :: [(Name, FnOpts, PTerm, PTerm)]
mtys = ((Name, (Bool, FnOpts, PTerm)) -> (Name, FnOpts, PTerm, PTerm))
-> [(Name, (Bool, FnOpts, PTerm))]
-> [(Name, FnOpts, PTerm, PTerm)]
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 [(Name, PTerm)] -> [(Name, PTerm)] -> [(Name, PTerm)]
forall a. [a] -> [a] -> [a]
++ [(Name, PTerm)]
ips) [Name]
pnames PTerm
t
                       mnamemap :: [(Name, PTerm)]
mnamemap =
                          (Name -> (Name, PTerm)) -> [Name] -> [(Name, PTerm)]
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))
                                              ((Name -> PArg' PTerm) -> [Name] -> [PArg' PTerm]
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 (([(Name, FnOpts, PTerm, PTerm)], [(Name, PTerm)]) -> String
forall a. Show a => a -> String
show ([(Name, FnOpts, PTerm, PTerm)]
mtys, ([(Name, PTerm)]
iimpps [(Name, PTerm)] -> [(Name, PTerm)] -> [(Name, PTerm)]
forall a. [a] -> [a] -> [a]
++ [(Name, PTerm)]
ips)))
         Int -> String -> Idris ()
logElab Int
5 (String
"Before defaults: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [PDecl] -> String
forall a. Show a => a -> String
show [PDecl]
ds String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (((Name, (Bool, FnOpts, PTerm)) -> Name)
-> [(Name, (Bool, FnOpts, PTerm))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Bool, FnOpts, PTerm)) -> Name
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: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [PDecl] -> String
forall a. Show a => a -> String
show [PDecl]
ds_defs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n")

         let ds' :: [PDecl]
ds' = [Name] -> [PDecl] -> [PDecl]
reorderDefs (((Name, (Bool, FnOpts, PTerm)) -> Name)
-> [(Name, (Bool, FnOpts, PTerm))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Bool, FnOpts, PTerm)) -> Name
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: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [PDecl] -> String
forall a. Show a => a -> String
show [PDecl]
ds' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n")

         (Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([PDecl] -> [Text] -> Name -> Name -> Idris ()
forall {t :: * -> *} {t}.
Foldable t =>
t (PDecl' t) -> [Text] -> Name -> Name -> Idris ()
warnMissing [PDecl]
ds' [Text]
ns Name
iname) (((Name, (Bool, FnOpts, PTerm)) -> Name)
-> [(Name, (Bool, FnOpts, PTerm))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Bool, FnOpts, PTerm)) -> Name
forall a b. (a, b) -> a
fst (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci))
         (Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Name] -> Name -> Idris ()
forall {t :: * -> *}. Foldable t => t Name -> Name -> Idris ()
checkInInterface (((Name, (Bool, FnOpts, PTerm)) -> Name)
-> [(Name, (Bool, FnOpts, PTerm))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Bool, FnOpts, PTerm)) -> Name
forall a b. (a, b) -> a
fst (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci))) ((PDecl -> [Name]) -> [PDecl] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl -> [Name]
defined [PDecl]
ds')
         let wbTys :: [PDecl]
wbTys = ((Name, FnOpts, PTerm, PTerm) -> PDecl)
-> [(Name, FnOpts, PTerm, PTerm)] -> [PDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Name, FnOpts, PTerm, PTerm) -> PDecl
forall {d}. (Name, FnOpts, PTerm, d) -> PDecl
mkTyDecl [(Name, FnOpts, PTerm, PTerm)]
mtys
         let wbVals_orig :: [PDecl]
wbVals_orig = (PDecl -> PDecl) -> [PDecl] -> [PDecl]
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 = (PDecl -> PDecl) -> [PDecl] -> [PDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
-> IState
-> (Name -> Name)
-> [(Name, PTerm)]
-> [Name]
-> PDecl
-> PDecl
expandParamsD Bool
False IState
ist Name -> Name
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [(Name, PTerm)]
pextra (((Name, FnOpts, PTerm, PTerm) -> Name)
-> [(Name, FnOpts, PTerm, PTerm)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, FnOpts, PTerm, PTerm) -> Name
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 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Method types " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n" (((Name, FnOpts, PTerm, PTerm) -> String)
-> [(Name, FnOpts, PTerm, PTerm)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Doc OutputAnnotation -> String
forall a. Show a => a -> String
show (Doc OutputAnnotation -> String)
-> ((Name, FnOpts, PTerm, PTerm) -> Doc OutputAnnotation)
-> (Name, FnOpts, PTerm, PTerm)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
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 (PDecl -> Doc OutputAnnotation)
-> ((Name, FnOpts, PTerm, PTerm) -> PDecl)
-> (Name, FnOpts, PTerm, PTerm)
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Name, FnOpts, PTerm, PTerm) -> PDecl
forall {d}. (Name, FnOpts, PTerm, d) -> PDecl
mkTyDecl) [(Name, FnOpts, PTerm, PTerm)]
mtys)
         Int -> String -> Idris ()
logElab Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Implementation is " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [PTerm] -> String
forall a. Show a => a -> String
show [PTerm]
ps String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" implicits " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [PArg' PTerm] -> String
forall a. Show a => a -> String
show ([[PArg' PTerm]] -> [PArg' PTerm]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[PArg' PTerm]] -> [[PArg' PTerm]]
forall a. Eq a => [a] -> [a]
nub [[PArg' PTerm]]
wparams))

         let lhsImps :: [PArg' PTerm]
lhsImps = (Name -> PArg' PTerm) -> [Name] -> [PArg' PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> Name -> PTerm -> Bool -> PArg' PTerm
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 [PArg' PTerm] -> [PArg' PTerm] -> [PArg' PTerm]
forall a. [a] -> [a] -> [a]
++ ((Name, PTerm) -> PArg' PTerm) -> [(Name, PTerm)] -> [PArg' PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> PArg' PTerm
toExp (Name -> PArg' PTerm)
-> ((Name, PTerm) -> Name) -> (Name, PTerm) -> PArg' PTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.(Name, PTerm) -> Name
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))
                           (((Name, FnOpts, PTerm, PTerm) -> PArg' PTerm)
-> [(Name, FnOpts, PTerm, PTerm)] -> [PArg' PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (PTerm -> PArg' PTerm
forall {t}. t -> PArg' t
pexp (PTerm -> PArg' PTerm)
-> ((Name, FnOpts, PTerm, PTerm) -> PTerm)
-> (Name, FnOpts, PTerm, PTerm)
-> PArg' PTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ([PArg' PTerm] -> (Name, FnOpts, PTerm, PTerm) -> PTerm
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 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Implementation LHS " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FnOpts -> String
forall a. Show a => a -> String
show FnOpts
totopts String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
headVars
         Int -> String -> Idris ()
logElab Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Implementation RHS " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
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: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [PDecl] -> String
forall a. Show a => a -> String
show [PDecl]
wbTys)
         Int -> String -> Idris ()
logElab Int
3 (String
"Method bodies (before params): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [PDecl] -> String
forall a. Show a => a -> String
show [PDecl]
wbVals_orig)
         Int -> String -> Idris ()
logElab Int
3 (String
"Method bodies: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [PDecl] -> String
forall a. Show a => a -> String
show [PDecl]
wbVals)

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

         (PDecl -> Idris ()) -> [PDecl] -> Idris ()
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 -> PDecl) -> [PDecl] -> [PDecl]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, PTerm)] -> PDecl -> PDecl
impBind [(Name, PTerm)]
headVarTypes) [PDecl]
wbTys)
         (PDecl -> Idris ()) -> [PDecl] -> Idris ()
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 -> String -> Type
forall a. HasCallStack => String -> a
error String
"Can't happen (interface constructor)"
         let ifn_is :: [PArg' PTerm]
ifn_is = case Name -> Ctxt [PArg' PTerm] -> Maybe [PArg' PTerm]
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 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Propagating parameters to methods: "
                           String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Name, [Name]) -> String
forall a. Show a => a -> String
show (Name
iname, [Name]
prop_params)

         let wbVals' :: [PDecl]
wbVals' = (PDecl -> PDecl) -> [PDecl] -> [PDecl]
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: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [PDecl] -> String
forall a. Show a => a -> String
show [PDecl]
wbVals')
         (PDecl -> Idris ()) -> [PDecl] -> Idris ()
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'

         ((PDecl, PDecl) -> Idris ()) -> [(PDecl, PDecl)] -> Idris ()
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)) ([PDecl] -> [PDecl] -> [(PDecl, PDecl)]
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 (Maybe Name -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Name
expn) Name
n Name
iname)

  where
    getImpParams :: IState -> [a] -> [Type] -> [PTerm]
getImpParams IState
ist = (a -> Type -> PTerm) -> [a] -> [Type] -> [PTerm]
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' ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show [a]
ps'))
                          [String]
m -> Name -> [String] -> Name
sNS (SpecialName -> Name
SN (Name -> [String] -> SpecialName
sImplementationN Name
n' ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
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)
        = Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> [(Name, PTerm)]
-> [Name]
-> Accessibility
-> FnOpts
-> Name
-> FC
-> [PTerm]
-> [(Name, PTerm)]
-> PTerm
-> Maybe Name
-> [PDecl]
-> PDecl
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
                     ((PTerm -> PTerm) -> [PTerm] -> [PTerm]
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 Name -> Ctxt InterfaceInfo -> [(Name, InterfaceInfo)]
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 = (Name -> [String] -> [PTerm] -> Maybe Name -> Name
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]
_) -> Bool -> StateT IState (ExceptT Err IO) Bool
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
            [(Name, InterfaceInfo)]
_ -> Bool -> StateT IState (ExceptT Err IO) Bool
forall a. a -> StateT IState (ExceptT Err IO) a
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
_) <-
                TC (ElabResult, String) -> Idris (ElabResult, String)
forall a. TC a -> Idris a
tclift (TC (ElabResult, String) -> Idris (ElabResult, String))
-> TC (ElabResult, String) -> Idris (ElabResult, String)
forall a b. (a -> b) -> a -> b
$ String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> EState
-> Elab' EState ElabResult
-> TC (ElabResult, String)
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 (UExp -> Type
forall n. UExp -> TT n
TType (Int -> UExp
UVal Int
0)) EState
initEState
                         (String
-> Name
-> Maybe Type
-> Elab' EState ElabResult
-> Elab' EState ElabResult
forall aux a.
String -> Name -> Maybe Type -> Elab' aux a -> Elab' aux a
errAt String
"type of " Name
iname Maybe Type
forall a. Maybe a
Nothing (FC -> Elab' EState ElabResult -> Elab' EState ElabResult
forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> PTerm
-> Elab' EState 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 ((IState -> IState) -> Idris ()) -> (IState -> IState) -> Idris ()
forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i { idris_name = 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 Err -> Err
forall a. a -> a
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
             Bool -> StateT IState (ExceptT Err IO) Bool
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> StateT IState (ExceptT Err IO) Bool)
-> Bool -> StateT IState (ExceptT Err IO) Bool
forall a b. (a -> b) -> a -> b
$ (Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe PTerm -> Bool
forall a. Maybe a -> Bool
isJust (Maybe PTerm -> Bool) -> (Name -> Maybe PTerm) -> Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IState -> [Int] -> PTerm -> Name -> Maybe PTerm
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)) (((Name, Bool) -> Name) -> [(Name, Bool)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Bool) -> Name
forall a b. (a, b) -> a
fst ([(Name, Bool)] -> [Name]) -> [(Name, Bool)] -> [Name]
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 = Maybe PTerm
forall a. Maybe a
Nothing
     | Just FnOpts
opts <- Name -> Ctxt FnOpts -> Maybe FnOpts
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt FnOpts
idris_flags IState
i),
       FnOpt
OverlappingDictionary FnOpt -> FnOpts -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts = Maybe PTerm
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 IState
-> t a -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
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)]
_ -> PTerm -> Maybe PTerm
forall a. a -> Maybe a
Just PTerm
tret'
                           Left (PTerm, PTerm)
_ -> case IState
-> t a -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
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)]
_ -> PTerm -> Maybe PTerm
forall a. a -> Maybe a
Just PTerm
tret'
                                       Left (PTerm, PTerm)
_ -> Maybe PTerm
forall a. Maybe a
Nothing
            [Type]
_ -> Maybe PTerm
forall a. Maybe a
Nothing
    overlapping :: a -> Idris a
overlapping a
t' = TC a -> Idris a
forall a. TC a -> Idris a
tclift (TC a -> Idris a) -> TC a -> Idris a
forall a b. (a -> b) -> a -> b
$ Err -> TC a
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Err
forall t. String -> Err' t
Msg (String -> Err) -> String -> Err
forall a b. (a -> b) -> a -> b
$
                          String
"Overlapping implementation: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
t' String -> String -> String
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' = t a -> PTerm -> PTerm
forall {t :: * -> *} {a}.
(Foldable t, Eq a, Num a, Enum a) =>
t a -> PTerm -> PTerm
keepDets t a
dets PTerm
x
            y' :: PTerm
y' = t a -> PTerm -> PTerm
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 ([PArg' PTerm] -> PTerm) -> [PArg' PTerm] -> PTerm
forall a b. (a -> b) -> a -> b
$ let a' :: [(a, PArg' PTerm)]
a' = [a] -> [PArg' PTerm] -> [(a, PArg' PTerm)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a
0..] [PArg' PTerm]
args in
              ((a, PArg' PTerm) -> PArg' PTerm)
-> [(a, PArg' PTerm)] -> [PArg' PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (a, PArg' PTerm) -> PArg' PTerm
forall a b. (a, b) -> b
snd (((a, PArg' PTerm) -> Bool)
-> [(a, PArg' PTerm)] -> [(a, PArg' PTerm)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(a
i, PArg' PTerm
_) -> a
i a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
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 = PTerm -> PArg' PTerm
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 [PArg' PTerm] -> [PArg' PTerm] -> [PArg' PTerm]
forall a. [a] -> [a] -> [a]
++ ((Name, PTerm) -> PArg' PTerm) -> [(Name, PTerm)] -> [PArg' PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> PArg' PTerm
toExp (Name -> PArg' PTerm)
-> ((Name, PTerm) -> Name) -> (Name, PTerm) -> PArg' PTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Name, PTerm) -> Name
forall a b. (a, b) -> a
fst) [(Name, PTerm)]
pextra [PArg' PTerm] -> [PArg' PTerm] -> [PArg' PTerm]
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
iInt -> Int -> Int
forall 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
iInt -> Int -> Int
forall 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)
        = Int -> Bool -> [ArgOpt] -> Name -> PTerm -> PArg' PTerm
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")) PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: Int -> PTerm -> [PArg' PTerm]
methArgs (Int
iInt -> Int -> Int
forall 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)
        = Int -> [ArgOpt] -> Name -> PTerm -> PArg' PTerm
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")) PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: Int -> PTerm -> [PArg' PTerm]
methArgs (Int
iInt -> Int -> Int
forall 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)
        = Int -> [ArgOpt] -> Name -> PTerm -> PArg' PTerm
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PConstraint Int
0 [] (Int -> String -> Name
sMN Int
0 String
"marg") (FC -> PTerm
PResolveTC FC
fc) PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: Int -> PTerm -> [PArg' PTerm]
methArgs (Int
iInt -> Int -> Int
forall 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 [] = [PArg' PTerm] -> StateT IState (ExceptT Err IO) [PArg' PTerm]
forall a. a -> StateT IState (ExceptT Err IO) a
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
                [] -> [PArg' PTerm] -> StateT IState (ExceptT Err IO) [PArg' PTerm]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> PTerm -> Bool -> PArg' PTerm
forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) Bool
True PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: [PArg' PTerm]
ps')
                [Type]
_ -> [PArg' PTerm] -> StateT IState (ExceptT Err IO) [PArg' PTerm]
forall a. a -> StateT IState (ExceptT Err IO) a
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
_)
        = Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> PDecl
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> t
-> PDecl' t
PTy Docstring (Either Err PTerm)
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 Name -> [PDecl] -> [PDecl] -> Maybe (PDecl, [PDecl])
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 PDecl -> [PDecl] -> [PDecl]
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 [] = Maybe (PDecl' t, [PDecl' t])
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Name
nsroot Name
cn = (PDecl' t, [PDecl' t]) -> Maybe (PDecl' t, [PDecl' t])
forall a. a -> Maybe a
Just (PDecl' t
def, [PDecl' t]
acc [PDecl' t] -> [PDecl' t] -> [PDecl' t]
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 [PDecl' t] -> [PDecl' t] -> [PDecl' t]
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 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (PDecl -> Bool) -> [PDecl] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> Name -> [Text] -> PDecl -> Bool
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 [PDecl] -> [PDecl] -> [PDecl]
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 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (PDecl' t -> Bool) -> t (PDecl' t) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> Name -> [Text] -> PDecl' t -> Bool
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 (Doc OutputAnnotation -> Idris ())
-> (String -> Doc OutputAnnotation) -> String -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> Doc OutputAnnotation
forall a. String -> Doc a
text (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"method " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
meth String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" not defined"
        | Bool
otherwise = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

    eqRoot :: Name -> Name -> Bool
eqRoot Name
x Name
y = Name -> Name
nsroot Name
x Name -> Name -> Bool
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 Name -> Name -> Bool
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) = (PTerm -> [Name]) -> [PTerm] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PTerm -> [Name]
getHeadVars ((PArg' PTerm -> PTerm) -> [PArg' PTerm] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PArg' PTerm -> PTerm
forall t. PArg' t -> t
getTm [PArg' PTerm]
args)
getHeadVars (PPair FC
_ [FC]
_ PunInfo
_ PTerm
l PTerm
r) = PTerm -> [Name]
getHeadVars PTerm
l [Name] -> [Name] -> [Name]
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 [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ PTerm -> [Name]
getHeadVars PTerm
t [Name] -> [Name] -> [Name]
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)
     = Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> PDecl
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 (((Name, PTerm) -> Bool) -> [(Name, PTerm)] -> [(Name, PTerm)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n, PTerm
ty) -> Name
n Name -> [Name] -> Bool
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 Name -> [Name] -> [Name]
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = IState -> Type -> PTerm
delab IState
ist (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b)
    | Bool
otherwise = IState -> Name -> Type -> PTerm
getTypeIn IState
ist Name
n (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
x Type
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 = Name -> PTerm -> Bool -> PArg' PTerm
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) = FC -> FnOpts -> Name -> [PClause' PTerm] -> PDecl
forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc FnOpts
opts Name
n ((PClause' PTerm -> PClause' PTerm)
-> [PClause' PTerm] -> [PClause' PTerm]
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)
        = FC
-> Name -> PTerm -> [PTerm] -> PTerm -> [PDecl] -> PClause' PTerm
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)
        = FC
-> Name
-> PTerm
-> [PTerm]
-> PTerm
-> Maybe (Name, FC)
-> [PDecl]
-> PClause' PTerm
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
                      ((PDecl -> PDecl) -> [PDecl] -> [PDecl]
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) ((Name -> PArg' PTerm) -> [Name] -> [PArg' PTerm]
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 ([PArg' PTerm] -> [PArg' PTerm] -> [PArg' PTerm]
forall {t}. [PArg' t] -> [PArg' t] -> [PArg' t]
mergePs ((Name -> PArg' PTerm) -> [Name] -> [PArg' PTerm]
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
         | PArg' t -> Bool
forall {t}. PArg' t -> Bool
isImplicit PArg' t
p,
           PArg' t -> Name
forall t. PArg' t -> Name
pname PArg' t
p Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (PArg' t -> Name) -> [PArg' t] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map PArg' t -> Name
forall t. PArg' t -> Name
pname [PArg' t]
args
               = PArg' t
p PArg' t -> [PArg' t] -> [PArg' t]
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 = (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Name
x -> Name
x Name -> [Name] -> Bool
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
_) <- Name
-> [(Name, (Bool, FnOpts, PTerm))] -> Maybe (Bool, 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 (([Name], SC' Type) -> SC' Type
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 ((Type, [Type]) -> Type
forall a b. (a, b) -> a
fst (Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
tm))
    checkInjectiveCase IState
_ SC' Type
_ = Idris ()
forall {a}. Idris a
notifail

    checkInjectiveApp :: IState -> Type -> Idris ()
checkInjectiveApp IState
ist (P (TCon Int
_ Int
_) Name
n Type
_) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    checkInjectiveApp IState
ist (P (DCon Int
_ Int
_ Bool
_) Name
n Type
_) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    checkInjectiveApp IState
ist (P NameType
Ref Name
n Type
_) = Idris ()
forall {a}. Idris a
notifail
    checkInjectiveApp IState
_ Type
_ = Idris ()
forall {a}. Idris a
notifail

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

    clookup :: Name -> [(Name, a)] -> Maybe a
clookup Name
n [] = Maybe a
forall a. Maybe a
Nothing
    clookup Name
n ((Name
n', a
d) : [(Name, a)]
ds) | Name -> Name
nsroot Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Name
nsroot Name
n' = a -> Maybe a
forall a. a -> Maybe a
Just a
d
                             | Bool
otherwise = Maybe a
forall a. Maybe a
Nothing
checkInjectiveDef FC
fc [(Name, (Bool, FnOpts, PTerm))]
ns (PDecl, PDecl)
_ = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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 = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
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 Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) IState
ist [Type]
as
            else TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Name -> Type -> Err
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) IState
ist [Type]
as
    ci Int
i IState
ist [] = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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 (Binder Type -> Type
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)
       = TT n -> TT n -> TT n
forall n. TT n -> TT n -> TT n
substV (NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
n TT n
forall n. TT n
Erased) (TT n -> TT n
instantiateRetTy TT n
sc)
    instantiateRetTy TT n
t = TT n
t