{-# 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
-> FC
-> [(Name, PTerm)]
-> [Name]
-> Accessibility
-> FnOpts
-> Name
-> FC
-> [PTerm]
-> [(Name, PTerm)]
-> PTerm
-> Maybe 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)
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
[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
_ -> []
[[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
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
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
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
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)
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
[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
_ = []
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
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
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
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