{-# LANGUAGE PatternGuards #-}
{-# OPTIONS_GHC -fwarn-missing-signatures #-}
module Idris.Elab.Interface(elabInterface) where
import Idris.AbsSyntax
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate
import Idris.Docstrings
import Idris.Elab.Data
import Idris.Elab.Utils
import Idris.Error
import Idris.Output (sendHighlighting)
import Prelude hiding (id, (.))
import Control.Category
import Control.Monad
import Data.Generics.Uniplate.Data (transform)
import Data.List
import Data.Maybe
import qualified Data.Set as S
data MArgTy = IA Name | EA Name | CA deriving Int -> MArgTy -> ShowS
[MArgTy] -> ShowS
MArgTy -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MArgTy] -> ShowS
$cshowList :: [MArgTy] -> ShowS
show :: MArgTy -> String
$cshow :: MArgTy -> String
showsPrec :: Int -> MArgTy -> ShowS
$cshowsPrec :: Int -> MArgTy -> ShowS
Show
elabInterface :: ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> ElabWhat
-> FC
-> [(Name, PTerm)]
-> Name
-> FC
-> [(Name, FC, PTerm)]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Name, FC)]
-> [PDecl]
-> Maybe (Name, FC)
-> Docstring (Either Err PTerm)
-> Idris ()
elabInterface :: ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> ElabWhat
-> FC
-> [(Name, PTerm)]
-> Name
-> FC
-> [(Name, FC, PTerm)]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Name, FC)]
-> [PDecl]
-> Maybe (Name, FC)
-> Docstring (Either Err PTerm)
-> Idris ()
elabInterface ElabInfo
info_in SyntaxInfo
syn_in Docstring (Either Err PTerm)
doc ElabWhat
what FC
fc [(Name, PTerm)]
constraints Name
tn FC
tnfc [(Name, FC, PTerm)]
ps [(Name, Docstring (Either Err PTerm))]
pDocs [(Name, FC)]
fds [PDecl]
ds Maybe (Name, FC)
mcn Docstring (Either Err PTerm)
cd
= do let cn :: Name
cn = forall a. a -> Maybe a -> a
fromMaybe (SpecialName -> Name
SN (Name -> SpecialName
ImplementationCtorN Name
tn)) (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Name, FC)
mcn)
let constraint :: PTerm
constraint = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
tn)
(forall a b. (a -> b) -> [a] -> [b]
map (forall {t}. t -> PArg' t
pexp forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FC -> [FC] -> Name -> PTerm
PRef FC
fc []) (forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, FC
_, PTerm
_) -> Name
n) [(Name, FC, PTerm)]
ps))
let syn :: SyntaxInfo
syn =
SyntaxInfo
syn_in { using :: [Using]
using = [Using] -> [(Name, PTerm)] -> [Using]
addToUsing (SyntaxInfo -> [Using]
using SyntaxInfo
syn_in)
[(Name
pn, PTerm
pt) | (Name
pn, FC
_, PTerm
pt) <- [(Name, FC, PTerm)]
ps]
}
IState
ist <- Idris IState
getIState
let impps_ns :: [(Name, FC, PTerm)]
impps_ns = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, FC
emptyFC, PTerm
Placeholder)) forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Name] -> IState -> PTerm -> [Name]
implicitNamesIn [] IState
ist)
(forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
_,FC
_,PTerm
x) -> PTerm
x) [(Name, FC, PTerm)]
ps)
let impps :: [(Name, FC, PTerm)]
impps = forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n, FC
_, PTerm
_) ->
Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, FC
_, PTerm
_) -> Name
n) [(Name, FC, PTerm)]
ps)) [(Name, FC, PTerm)]
impps_ns
let tty :: PTerm
tty = [(Name, PTerm)] -> PTerm -> PTerm
impbind (forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, FC
_, PTerm
ty) -> (Name
n, PTerm
ty)) [(Name, FC, PTerm)]
impps) forall a b. (a -> b) -> a -> b
$
[(Name, PTerm)] -> PTerm -> PTerm
pibind (forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, FC
_, PTerm
ty) -> (Name
n, PTerm
ty)) [(Name, FC, PTerm)]
ps) (FC -> PTerm
PType FC
fc)
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Implicit parameters are " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, FC, PTerm)]
impps
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Interface type is " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
tty
let mdecls :: [PDecl]
mdecls = forall a. (a -> Bool) -> [a] -> [a]
filter forall {t}. PDecl' t -> Bool
tydecl [PDecl]
ds
let idecls :: [PDecl]
idecls = forall a. (a -> Bool) -> [a] -> [a]
filter forall {t}. PDecl' t -> Bool
impldecl [PDecl]
ds
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ PDecl -> Idris ()
checkDefaultSuperInterfaceImplementation [PDecl]
idecls
let mnames :: [Name]
mnames = forall a b. (a -> b) -> [a] -> [b]
map forall {t}. PDecl' t -> Name
getMName [PDecl]
mdecls
let fullmnames :: [Name]
fullmnames = forall a b. (a -> b) -> [a] -> [b]
map forall {t}. PDecl' t -> Name
getFullMName [PDecl]
mdecls
IState
ist <- Idris IState
getIState
let constraintNames :: [Name]
constraintNames = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([(Name, PTerm)] -> IState -> PTerm -> [Name]
namesIn [] IState
ist) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Name, PTerm)]
constraints)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Name] -> Name -> Idris ()
checkConstraintName (forall a b. (a -> b) -> [a] -> [b]
map (\(Name
x, FC
_, PTerm
_) -> Name
x) [(Name, FC, PTerm)]
ps)) [Name]
constraintNames
let pre_ddecl :: PData' PTerm
pre_ddecl = forall t. Name -> FC -> t -> PData' t
PLaterdecl Name
tn FC
NoFC PTerm
tty
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ElabWhat
what forall a. Eq a => a -> a -> Bool
/= ElabWhat
EDefns) forall a b. (a -> b) -> a -> b
$
ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> DataOpts
-> PData' PTerm
-> Idris ()
elabData ElabInfo
info (SyntaxInfo
syn { no_imp :: [Name]
no_imp = SyntaxInfo -> [Name]
no_imp SyntaxInfo
syn forall a. [a] -> [a] -> [a]
++ [Name]
mnames,
imp_methods :: [Name]
imp_methods = [Name]
mnames }) Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
pDocs FC
fc [] PData' PTerm
pre_ddecl
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ElabWhat
what forall a. Eq a => a -> a -> Bool
/= ElabWhat
ETypes) forall a b. (a -> b) -> a -> b
$ do
[Int]
dets <- Name -> [Name] -> Idris [Int]
findDets Name
tn (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, FC)]
fds)
Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"Building methods " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name]
fullmnames
[((Name, PTerm),
(Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm)),
(Name, (FC, SyntaxInfo, FnOpts, PTerm)))]
ims <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([(Name, FC, PTerm)]
-> [Name]
-> PDecl
-> StateT
IState
(ExceptT Err IO)
((Name, PTerm),
(Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm)),
(Name, (FC, SyntaxInfo, FnOpts, PTerm)))
tdecl [(Name, FC, PTerm)]
impps [Name]
mnames) [PDecl]
mdecls
[(Name, ((Name, PDecl), [PDecl]))]
defs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([(Name, (FC, SyntaxInfo, FnOpts, PTerm))]
-> PTerm
-> PDecl
-> StateT IState (ExceptT Err IO) (Name, ((Name, PDecl), [PDecl]))
defdecl (forall a b. (a -> b) -> [a] -> [b]
map (\ ((Name, PTerm)
x,(Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))
y,(Name, (FC, SyntaxInfo, FnOpts, PTerm))
z) -> (Name, (FC, SyntaxInfo, FnOpts, PTerm))
z) [((Name, PTerm),
(Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm)),
(Name, (FC, SyntaxInfo, FnOpts, PTerm)))]
ims) PTerm
constraint)
(forall a. (a -> Bool) -> [a] -> [a]
filter forall {t}. PDecl' t -> Bool
clause [PDecl]
ds)
let imethods :: [(Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))]
imethods = forall a b. (a -> b) -> [a] -> [b]
map (\ ((Name, PTerm)
x, (Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))
y, (Name, (FC, SyntaxInfo, FnOpts, PTerm))
z) -> (Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))
y) [((Name, PTerm),
(Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm)),
(Name, (FC, SyntaxInfo, FnOpts, PTerm)))]
ims
let defaults :: [(Name, (Name, PDecl))]
defaults = forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
x, ((Name, PDecl)
y, [PDecl]
z)) -> (Name
x,(Name, PDecl)
y)) [(Name, ((Name, PDecl), [PDecl]))]
defs
Name -> InterfaceInfo -> Idris ()
addInterface Name
tn (Name
-> [(Name, (Bool, FnOpts, PTerm))]
-> [(Name, (Name, PDecl))]
-> [PDecl]
-> [Name]
-> [Name]
-> [PTerm]
-> [(Name, Bool)]
-> [Int]
-> InterfaceInfo
CI Name
cn (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a} {b} {c} {b} {c}.
(a, (a, b, c, b, c)) -> (a, (a, b, c))
nodoc [(Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))]
imethods) [(Name, (Name, PDecl))]
defaults [PDecl]
idecls
(forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, FC
_, PTerm
_) -> Name
n) [(Name, FC, PTerm)]
impps)
(forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, FC
_, PTerm
_) -> Name
n) [(Name, FC, PTerm)]
ps)
(forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Name, PTerm)]
constraints)
[] [Int]
dets)
[(PDecl, PDecl)]
cfns <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a.
Name
-> PTerm
-> SyntaxInfo
-> [a]
-> (Name, PTerm)
-> Idris (PDecl, PDecl)
cfun Name
cn PTerm
constraint SyntaxInfo
syn (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))]
imethods)) [(Name, PTerm)]
constraints
let ([PDecl]
cfnTyDecls, [PDecl]
cfnDefs) = forall a b. [(a, b)] -> ([a], [b])
unzip [(PDecl, PDecl)]
cfns
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]
cfnTyDecls
[(PDecl, PDecl)]
fns <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name
-> PTerm
-> SyntaxInfo
-> [Name]
-> (Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))
-> Idris (PDecl, PDecl)
tfun Name
cn PTerm
constraint (SyntaxInfo
syn { imp_methods :: [Name]
imp_methods = [Name]
mnames })
(forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))]
imethods)) [(Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))]
imethods
let ([PDecl]
fnTyDecls, [PDecl]
fnDefs) = forall a b. [(a, b)] -> ([a], [b])
unzip [(PDecl, PDecl)]
fns
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]
fnTyDecls
[PTerm]
elabMethTys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> Idris PTerm
getElabMethTy [Name]
fullmnames
Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"Method types:\n" forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n" (forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
elabMethTys)
let cpos :: [(Name, Int)]
cpos = forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, PTerm
ty) -> (Name
n, PTerm -> Int
findConstraint PTerm
ty))
(forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
fullmnames [PTerm]
elabMethTys)
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Constraint pos: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, Int)]
cpos
let storemeths :: [(Name, PTerm)]
storemeths = forall a b. (a -> b) -> [a] -> [b]
map (Bool -> [(Name, Int)] -> (Name, PTerm) -> (Name, PTerm)
mkMethTy Bool
True [(Name, Int)]
cpos) (forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
fullmnames [PTerm]
elabMethTys)
Name -> [(Name, PTerm)] -> Idris ()
updateIMethods Name
tn [(Name, PTerm)]
storemeths
let cty :: PTerm
cty = [(Name, PTerm)] -> PTerm -> PTerm
impbind [(Name
pn, PTerm
pt) | (Name
pn, FC
_, PTerm
pt) <- [(Name, FC, PTerm)]
impps forall a. [a] -> [a] -> [a]
++ [(Name, FC, PTerm)]
ps] forall a b. (a -> b) -> a -> b
$
[(Name, PTerm)] -> PTerm -> PTerm
conbind [(Name, PTerm)]
constraints forall a b. (a -> b) -> a -> b
$
[(Name, PTerm)] -> PTerm -> PTerm
pibind (forall a b. (a -> b) -> [a] -> [b]
map (Bool -> [(Name, Int)] -> (Name, PTerm) -> (Name, PTerm)
mkMethTy Bool
False [(Name, Int)]
cpos) (forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
fullmnames [PTerm]
elabMethTys))
PTerm
constraint
Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"Constraint constructor type: " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
cty
let cons :: [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [a])]
cons = [(Docstring (Either Err PTerm)
cd, [(Name, Docstring (Either Err PTerm))]
pDocs forall a. [a] -> [a] -> [a]
++ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PDecl -> Maybe (Name, Docstring (Either Err PTerm))
memberDocs [PDecl]
ds, Name
cn, FC
NoFC, PTerm
cty, FC
fc, [])]
let ddecl :: PData' PTerm
ddecl = forall t.
Name
-> FC
-> t
-> [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]
-> PData' t
PDatadecl Name
tn FC
NoFC PTerm
tty forall {a}.
[(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [a])]
cons
Int -> String -> Idris ()
logElab Int
10 forall a b. (a -> b) -> a -> b
$ String
"Interface " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (PPOption -> PData' PTerm -> Doc OutputAnnotation
showDImp PPOption
verbosePPOption PData' PTerm
ddecl)
ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> DataOpts
-> PData' PTerm
-> Idris ()
elabData ElabInfo
info (SyntaxInfo
syn { no_imp :: [Name]
no_imp = SyntaxInfo -> [Name]
no_imp SyntaxInfo
syn forall a. [a] -> [a] -> [a]
++ [Name]
mnames,
imp_methods :: [Name]
imp_methods = [] }) Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
pDocs FC
fc [] PData' PTerm
ddecl
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Function types " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [PDecl]
fnTyDecls
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Method types now: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))]
imethods
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]
cfnDefs
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]
fnDefs
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Name
n -> do Name -> Bool -> Idris ()
setInjectivity Name
n Bool
True
IBCWrite -> Idris ()
addIBC (Name -> Bool -> IBCWrite
IBCInjective Name
n Bool
True))
(forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
_, (Bool
inj, FC
_, Docstring (Either Err PTerm)
_, FnOpts
_, PTerm
_)) -> Bool
inj) [(Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))]
imethods))
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
info) (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a b. (a, b) -> b
sndforall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.forall a b. (a, b) -> b
snd) [(Name, ((Name, PDecl), [PDecl]))]
defs)
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCInterface Name
tn)
Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$
[(FC -> FC'
FC' FC
tnfc, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
tn forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. Maybe a
Nothing)] forall a. [a] -> [a] -> [a]
++
[(FC -> FC'
FC' FC
pnfc, Name -> Bool -> OutputAnnotation
AnnBoundName Name
pn Bool
False) | (Name
pn, FC
pnfc, PTerm
_) <- [(Name, FC, PTerm)]
ps] forall a. [a] -> [a] -> [a]
++
[(FC -> FC'
FC' FC
fdfc, Name -> Bool -> OutputAnnotation
AnnBoundName Name
fc Bool
False) | (Name
fc, FC
fdfc) <- [(Name, FC)]
fds] forall a. [a] -> [a] -> [a]
++
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\(Name
conN, FC
conNFC) -> [(FC -> FC'
FC' FC
conNFC, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
conN forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. Maybe a
Nothing)]) Maybe (Name, FC)
mcn
where
info :: ElabInfo
info = ElabInfo
info_in { noCaseLift :: [Name]
noCaseLift = Name
tn forall a. a -> [a] -> [a]
: ElabInfo -> [Name]
noCaseLift ElabInfo
info_in }
getElabMethTy :: Name -> Idris PTerm
getElabMethTy :: Name -> Idris PTerm
getElabMethTy Name
n = do IState
ist <- Idris IState
getIState
let impls :: [PArg]
impls = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [PArg]
idris_implicits IState
ist) of
Just [PArg]
i -> [PArg]
i
Maybe [PArg]
Nothing -> []
case Name -> Context -> Maybe Type
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
ist) of
Just Type
ty -> forall (m :: * -> *) a. Monad m => a -> m a
return (IState
-> [PArg]
-> [(Name, Type)]
-> Type
-> Bool
-> Bool
-> Bool
-> PTerm
delabTy' IState
ist [PArg]
impls [] Type
ty Bool
False Bool
False Bool
False)
Maybe Type
Nothing -> forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Err' t
InternalMsg String
"Can't happen, elabMethTy"))
findConstraint :: PTerm -> Int
findConstraint :: PTerm -> Int
findConstraint = forall {t}. Num t => t -> PTerm -> t
findPos Int
0
where
findPos :: t -> PTerm -> t
findPos t
i (PPi Plicity
_ Name
_ FC
_ (PRef FC
_ [FC]
_ Name
n) PTerm
sc)
| Name
n forall a. Eq a => a -> a -> Bool
== Name
tn = t
i
findPos t
i (PPi Plicity
_ Name
_ FC
_ (PApp FC
_ (PRef FC
_ [FC]
_ Name
n) [PArg]
_) PTerm
sc)
| Name
n forall a. Eq a => a -> a -> Bool
== Name
tn = t
i
findPos t
i (PPi Plicity
_ Name
_ FC
_ PTerm
ty PTerm
sc) = t -> PTerm -> t
findPos (t
i forall a. Num a => a -> a -> a
+ t
1) PTerm
sc
findPos t
i PTerm
_ = -t
1
mkMethTy :: Bool -> [(Name, Int)] -> (Name, PTerm) -> (Name, PTerm)
mkMethTy :: Bool -> [(Name, Int)] -> (Name, PTerm) -> (Name, PTerm)
mkMethTy Bool
keepns [(Name, Int)]
cpos (Name
n, PTerm
tm)
= (if Bool
keepns then Name
n else Name -> Name
nsroot Name
n, forall {t}. (Ord t, Num t) => t -> PTerm -> PTerm
dropPis Int
num ((PTerm -> PTerm) -> PTerm -> PTerm
mapPT PTerm -> PTerm
dropImp PTerm
tm))
where
num :: Int
num = case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Int)]
cpos of
Just Int
i -> Int
i forall a. Num a => a -> a -> a
+ Int
1
Maybe Int
Nothing -> Int
0
dropPis :: t -> PTerm -> PTerm
dropPis t
n (PPi Plicity
_ Name
_ FC
_ PTerm
_ PTerm
sc) | t
n forall a. Ord a => a -> a -> Bool
> t
0 = t -> PTerm -> PTerm
dropPis (t
n forall a. Num a => a -> a -> a
- t
1) PTerm
sc
dropPis t
_ PTerm
tm = PTerm
tm
dropImp :: PTerm -> PTerm
dropImp (PApp FC
fc (PRef FC
fcr [FC]
fcs Name
n) [PArg]
args)
| Just Int
pos <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Int)]
cpos
= FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fcr [FC]
fcs (Name -> Name
nsroot Name
n))
(forall a. (a -> Bool) -> [a] -> [a]
filter forall {t}. PArg' t -> Bool
notConstr (forall a. Int -> [a] -> [a]
drop (Int
pos forall a. Num a => a -> a -> a
+ Int
1) [PArg]
args))
dropImp (PApp FC
fc PTerm
f [PArg]
args)
= FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f (forall a. (a -> Bool) -> [a] -> [a]
filter forall {t}. PArg' t -> Bool
notConstr [PArg]
args)
dropImp PTerm
tm = PTerm
tm
notConstr :: PArg' t -> Bool
notConstr (PConstraint {}) = Bool
False
notConstr PArg' t
_ = Bool
True
nodoc :: (a, (a, b, c, b, c)) -> (a, (a, b, c))
nodoc (a
n, (a
inj, b
_, c
_, b
o, c
t)) = (a
n, (a
inj, b
o, c
t))
pibind :: [(Name, PTerm)] -> PTerm -> PTerm
pibind [] PTerm
x = PTerm
x
pibind ((Name
n, PTerm
ty): [(Name, PTerm)]
ns) PTerm
x = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
expl Name
n FC
NoFC PTerm
ty ([(Name, PTerm)] -> PTerm -> PTerm
pibind [(Name, PTerm)]
ns (PTerm -> PTerm -> PTerm
chkUniq PTerm
ty PTerm
x))
chkUniq :: PTerm -> PTerm -> PTerm
chkUniq u :: PTerm
u@(PUniverse FC
_ Universe
_) (PType FC
_) = PTerm
u
chkUniq (PUniverse FC
_ Universe
l) (PUniverse FC
_ Universe
r) = FC -> Universe -> PTerm
PUniverse FC
NoFC (forall a. Ord a => a -> a -> a
min Universe
l Universe
r)
chkUniq (PPi Plicity
_ Name
_ FC
_ PTerm
_ PTerm
sc) PTerm
t = PTerm -> PTerm -> PTerm
chkUniq PTerm
sc PTerm
t
chkUniq PTerm
_ PTerm
t = PTerm
t
checkDefaultSuperInterfaceImplementation :: PDecl -> Idris ()
checkDefaultSuperInterfaceImplementation :: PDecl -> Idris ()
checkDefaultSuperInterfaceImplementation (PImplementation Docstring (Either Err PTerm)
_ [(Name, Docstring (Either Err PTerm))]
_ SyntaxInfo
_ FC
fc [(Name, PTerm)]
cs [Name]
_ Accessibility
_ FnOpts
_ Name
n FC
_ [PTerm]
ps [(Name, PTerm)]
_ PTerm
_ Maybe Name
_ [PDecl]
_)
= do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, PTerm)]
cs) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a. TC a -> Idris a
tclift
forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Err' t
Msg String
"Default super interface implementations can't have constraints."))
IState
i <- Idris IState
getIState
let isConstrained :: Bool
isConstrained = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (IState -> Name -> [PArg] -> PTerm -> Bool
checkConstrained IState
i Name
n (forall a b. (a -> b) -> [a] -> [b]
map forall {t}. t -> PArg' t
pexp [PTerm]
ps)) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Name, PTerm)]
constraints)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
isConstrained) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a. TC a -> Idris a
tclift
forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Err' t
Msg String
"Default implementations must be for a super interface constraint on the containing interface."))
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
checkConstrained :: IState -> Name -> [PArg] -> PTerm -> Bool
checkConstrained IState
i Name
n [PArg]
args PTerm
constraint =
if (Name
n forall a. Eq a => a -> a -> Bool
== Name
cn Bool -> Bool -> Bool
&& [PArg]
args forall a. Eq a => a -> a -> Bool
== [PArg]
cargs)
then Bool
True
else forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (forall a b. (a -> b) -> [a] -> [b]
map (IState -> Name -> [PArg] -> PTerm -> Bool
checkConstrained IState
i Name
n [PArg]
args) [PTerm]
parentConstraints)
where
PApp FC
_ (PRef FC
_ [FC]
_ Name
cn) [PArg]
cargs = PTerm
constraint
parentConstraints :: [PTerm]
parentConstraints = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap InterfaceInfo -> [PTerm]
interface_constraints (forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
cn (IState -> Ctxt InterfaceInfo
idris_interfaces IState
i))
checkConstraintName :: [Name] -> Name -> Idris ()
checkConstraintName :: [Name] -> Name -> Idris ()
checkConstraintName [Name]
bound Name
cname
| Name
cname forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
bound
= forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ String
"Name " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
cname forall a. [a] -> [a] -> [a]
++
String
" is not bound in interface " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
tn
forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
" " (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Name]
bound)))
| Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return ()
impbind :: [(Name, PTerm)] -> PTerm -> PTerm
impbind :: [(Name, PTerm)] -> PTerm -> PTerm
impbind [] PTerm
x = PTerm
x
impbind ((Name
n, PTerm
ty): [(Name, PTerm)]
ns) PTerm
x = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
impl Name
n FC
NoFC PTerm
ty ([(Name, PTerm)] -> PTerm -> PTerm
impbind [(Name, PTerm)]
ns PTerm
x)
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
getMName :: PDecl' t -> Name
getMName (PTy Docstring (Either Err t)
_ [(Name, Docstring (Either Err t))]
_ SyntaxInfo
_ FC
_ FnOpts
_ Name
n FC
nfc t
_) = Name -> Name
nsroot Name
n
getMName (PData Docstring (Either Err t)
_ [(Name, Docstring (Either Err t))]
_ SyntaxInfo
_ FC
_ DataOpts
_ (PLaterdecl Name
n FC
nfc t
_)) = Name -> Name
nsroot Name
n
getFullMName :: PDecl' t -> Name
getFullMName (PTy Docstring (Either Err t)
_ [(Name, Docstring (Either Err t))]
_ SyntaxInfo
_ FC
_ FnOpts
_ Name
n FC
nfc t
_) = Name
n
getFullMName (PData Docstring (Either Err t)
_ [(Name, Docstring (Either Err t))]
_ SyntaxInfo
_ FC
_ DataOpts
_ (PLaterdecl Name
n FC
nfc t
_)) = Name
n
tdecl :: [(Name, FC, PTerm)]
-> [Name]
-> PDecl
-> StateT
IState
(ExceptT Err IO)
((Name, PTerm),
(Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm)),
(Name, (FC, SyntaxInfo, FnOpts, PTerm)))
tdecl [(Name, FC, PTerm)]
impps [Name]
allmeths (PTy Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
_ SyntaxInfo
syn FC
_ FnOpts
o Name
n FC
nfc PTerm
t)
= do PTerm
t' <- ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
implicit' ElabInfo
info SyntaxInfo
syn (forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, FC
_, PTerm
_) -> Name
n) ([(Name, FC, PTerm)]
impps forall a. [a] -> [a] -> [a]
++ [(Name, FC, PTerm)]
ps) forall a. [a] -> [a] -> [a]
++ [Name]
allmeths) Name
n PTerm
t
Int -> String -> Idris ()
logElab Int
1 forall a b. (a -> b) -> a -> b
$ String
"Method " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" : " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
t'
forall (m :: * -> *) a. Monad m => a -> m a
return ( (Name
n, (forall {t :: * -> *}.
Foldable t =>
t Name
-> ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity)
-> PTerm
-> PTerm
toExp (forall a b. (a -> b) -> [a] -> [b]
map (\(Name
pn, FC
_, PTerm
_) -> Name
pn) [(Name, FC, PTerm)]
ps) [ArgOpt] -> Static -> Bool -> RigCount -> Plicity
Exp PTerm
t')),
(Name
n, (Bool
False, FC
nfc, Docstring (Either Err PTerm)
doc, FnOpts
o, (forall {t :: * -> *}.
Foldable t =>
t Name
-> ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity)
-> PTerm
-> PTerm
toExp (forall a b. (a -> b) -> [a] -> [b]
map (\(Name
pn, FC
_, PTerm
_) -> Name
pn) [(Name, FC, PTerm)]
ps)
(\ [ArgOpt]
l Static
s Bool
p RigCount
r -> [ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [ArgOpt]
l Static
s Bool
p forall a. Maybe a
Nothing Bool
True RigCount
r) PTerm
t'))),
(Name
n, (FC
nfc, SyntaxInfo
syn, FnOpts
o, PTerm
t) ) )
tdecl [(Name, FC, PTerm)]
impps [Name]
allmeths (PData Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
_ SyntaxInfo
syn FC
_ DataOpts
_ (PLaterdecl Name
n FC
nfc PTerm
t))
= do let o :: [a]
o = []
PTerm
t' <- ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
implicit' ElabInfo
info SyntaxInfo
syn (forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, FC
_, PTerm
_) -> Name
n) [(Name, FC, PTerm)]
ps forall a. [a] -> [a] -> [a]
++ [Name]
allmeths) Name
n PTerm
t
Int -> String -> Idris ()
logElab Int
2 forall a b. (a -> b) -> a -> b
$ String
"Data method " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" : " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
t'
forall (m :: * -> *) a. Monad m => a -> m a
return ( (Name
n, (forall {t :: * -> *}.
Foldable t =>
t Name
-> ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity)
-> PTerm
-> PTerm
toExp (forall a b. (a -> b) -> [a] -> [b]
map (\(Name
pn, FC
_, PTerm
_) -> Name
pn) [(Name, FC, PTerm)]
ps) [ArgOpt] -> Static -> Bool -> RigCount -> Plicity
Exp PTerm
t')),
(Name
n, (Bool
True, FC
nfc, Docstring (Either Err PTerm)
doc, forall a. [a]
o, (forall {t :: * -> *}.
Foldable t =>
t Name
-> ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity)
-> PTerm
-> PTerm
toExp (forall a b. (a -> b) -> [a] -> [b]
map (\(Name
pn, FC
_, PTerm
_) -> Name
pn) [(Name, FC, PTerm)]
ps)
(\ [ArgOpt]
l Static
s Bool
p RigCount
r -> [ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [ArgOpt]
l Static
s Bool
p forall a. Maybe a
Nothing Bool
True RigCount
r) PTerm
t'))),
(Name
n, (FC
nfc, SyntaxInfo
syn, forall a. [a]
o, PTerm
t) ) )
tdecl [(Name, FC, PTerm)]
impps [Name]
allmeths (PData Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
_ SyntaxInfo
syn FC
_ DataOpts
_ PData' PTerm
_)
= forall a. Err -> Idris a
ierror forall a b. (a -> b) -> a -> b
$ forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Err' t
Msg String
"Data definitions not allowed in an interface declaration")
tdecl [(Name, FC, PTerm)]
_ [Name]
_ PDecl
_ = forall a. Err -> Idris a
ierror forall a b. (a -> b) -> a -> b
$ forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Err' t
Msg String
"Not allowed in an interface declaration")
defdecl :: [(Name, (FC, SyntaxInfo, FnOpts, PTerm))]
-> PTerm
-> PDecl
-> StateT IState (ExceptT Err IO) (Name, ((Name, PDecl), [PDecl]))
defdecl [(Name, (FC, SyntaxInfo, FnOpts, PTerm))]
mtys PTerm
c d :: PDecl
d@(PClauses FC
fc FnOpts
opts Name
n [PClause' PTerm]
cs) =
case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, (FC, SyntaxInfo, FnOpts, PTerm))]
mtys of
Just (FC
nfc, SyntaxInfo
syn, FnOpts
o, PTerm
ty) ->
do let ty' :: PTerm
ty' = PTerm -> [Name] -> PTerm -> PTerm
insertConstraint PTerm
c (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, (FC, SyntaxInfo, FnOpts, PTerm))]
mtys) PTerm
ty
let ds :: [PDecl]
ds = forall a b. (a -> b) -> [a] -> [b]
map ((Name -> Name) -> PDecl -> PDecl
decorateid Name -> Name
defaultdec)
[forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> t
-> PDecl' t
PTy forall a. Docstring a
emptyDocstring [] SyntaxInfo
syn FC
fc [] Name
n FC
nfc PTerm
ty',
forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc (FnOpts
o forall a. [a] -> [a] -> [a]
++ FnOpts
opts) Name
n [PClause' PTerm]
cs]
Int -> String -> Idris ()
logElab Int
1 (forall a. Show a => a -> String
show [PDecl]
ds)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, ((Name -> Name
defaultdec Name
n, [PDecl]
dsforall a. [a] -> Int -> a
!!Int
1), [PDecl]
ds))
Maybe (FC, SyntaxInfo, FnOpts, PTerm)
_ -> forall a. Err -> Idris a
ierror forall a b. (a -> b) -> a -> b
$ forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Err' t
Msg (forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" is not a method"))
defdecl [(Name, (FC, SyntaxInfo, FnOpts, PTerm))]
_ PTerm
_ PDecl
_ = forall a. String -> Idris a
ifail String
"Can't happen (defdecl)"
defaultdec :: Name -> Name
defaultdec (UN Text
n) = String -> Name
sUN (String
"default#" forall a. [a] -> [a] -> [a]
++ Text -> String
str Text
n)
defaultdec (NS Name
n [Text]
ns) = Name -> [Text] -> Name
NS (Name -> Name
defaultdec Name
n) [Text]
ns
tydecl :: PDecl' t -> Bool
tydecl (PTy{}) = Bool
True
tydecl (PData Docstring (Either Err t)
_ [(Name, Docstring (Either Err t))]
_ SyntaxInfo
_ FC
_ DataOpts
_ PData' t
_) = Bool
True
tydecl PDecl' t
_ = Bool
False
impldecl :: PDecl' t -> Bool
impldecl (PImplementation{}) = Bool
True
impldecl PDecl' t
_ = Bool
False
clause :: PDecl' t -> Bool
clause (PClauses{}) = Bool
True
clause PDecl' t
_ = Bool
False
cfun :: Name -> PTerm -> SyntaxInfo -> [a] -> (Name, PTerm) -> Idris (PDecl, PDecl)
cfun :: forall a.
Name
-> PTerm
-> SyntaxInfo
-> [a]
-> (Name, PTerm)
-> Idris (PDecl, PDecl)
cfun Name
cn PTerm
c SyntaxInfo
syn [a]
all (Name
cnm, PTerm
con)
= do let cfn :: Name
cfn = SpecialName -> Name
SN (Name -> Text -> SpecialName
ParentN Name
cn (String -> Text
txt (forall a. Show a => a -> String
show PTerm
con)))
let mnames :: [Name]
mnames = forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
all) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\Int
x -> Int -> String -> Name
sMN Int
x String
"meth") [Int
0..]
let capp :: PTerm
capp = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
cn) (forall a b. (a -> b) -> [a] -> [b]
map (forall {t}. t -> PArg' t
pexp forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FC -> [FC] -> Name -> PTerm
PRef FC
fc []) [Name]
mnames)
let lhs :: PTerm
lhs = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
cfn) [forall {t}. t -> PArg' t
pconst PTerm
capp]
let rhs :: PTerm
rhs = FC -> PTerm
PResolveTC (String -> FC
fileFC String
"HACK")
let ty :: PTerm
ty = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
constraint Name
cnm FC
NoFC PTerm
c PTerm
con
Int -> String -> Idris ()
logElab Int
2 (String
"Dictionary constraint: " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
ty)
Int -> String -> Idris ()
logElab Int
2 (PTerm -> String
showTmImpls PTerm
lhs forall a. [a] -> [a] -> [a]
++ String
" = " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
rhs)
IState
i <- Idris IState
getIState
let conn :: Name
conn = case PTerm
con of
PRef FC
_ [FC]
_ Name
n -> Name
n
PApp FC
_ (PRef FC
_ [FC]
_ Name
n) [PArg]
_ -> Name
n
let conn' :: Name
conn' = case forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
conn (IState -> Ctxt InterfaceInfo
idris_interfaces IState
i) of
[(Name
n, InterfaceInfo
_)] -> Name
n
[(Name, InterfaceInfo)]
_ -> Name
conn
Bool -> Bool -> Name -> Name -> Idris ()
addImplementation Bool
False Bool
True Name
conn' Name
cfn
IBCWrite -> Idris ()
addIBC (Bool -> Bool -> Name -> Name -> IBCWrite
IBCImplementation Bool
False Bool
True Name
conn' Name
cfn)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> t
-> PDecl' t
PTy forall a. Docstring a
emptyDocstring [] SyntaxInfo
syn FC
fc [] Name
cfn FC
NoFC PTerm
ty,
forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc [FnOpt
Inlinable, FnOpt
Dictionary] Name
cfn [forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
cfn PTerm
lhs [] PTerm
rhs []])
tfun :: Name
-> PTerm
-> SyntaxInfo -> [Name]
-> (Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))
-> Idris (PDecl, PDecl)
tfun :: Name
-> PTerm
-> SyntaxInfo
-> [Name]
-> (Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))
-> Idris (PDecl, PDecl)
tfun Name
cn PTerm
c SyntaxInfo
syn [Name]
all (Name
m, (Bool
isdata, FC
mfc, Docstring (Either Err PTerm)
doc, FnOpts
o, PTerm
ty))
= do let ty' :: PTerm
ty' = SyntaxInfo -> PTerm -> PTerm
expandMethNS SyntaxInfo
syn (PTerm -> [Name] -> PTerm -> PTerm
insertConstraint PTerm
c [Name]
all PTerm
ty)
let mnames :: [Name]
mnames = forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
all) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\Int
x -> Int -> String -> Name
sMN Int
x String
"meth") [Int
0..]
let capp :: PTerm
capp = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
cn) (forall a b. (a -> b) -> [a] -> [b]
map (forall {t}. t -> PArg' t
pexp forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FC -> [FC] -> Name -> PTerm
PRef FC
fc []) [Name]
mnames)
let margs :: [MArgTy]
margs = PTerm -> [MArgTy]
getMArgs PTerm
ty
let anames :: [Name]
anames = forall a b. (a -> b) -> [a] -> [b]
map (\Int
x -> Int -> String -> Name
sMN Int
x String
"arg") [Int
0..]
let lhs :: PTerm
lhs = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
m) (forall {t}. t -> PArg' t
pconst PTerm
capp forall a. a -> [a] -> [a]
: forall {a}. [MArgTy] -> [a] -> [PArg]
lhsArgs [MArgTy]
margs [Name]
anames)
let rhs :: PTerm
rhs = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc ([Name] -> [Name] -> Name -> PTerm
getMeth [Name]
mnames [Name]
all Name
m) (forall {a}. [MArgTy] -> [a] -> [PArg]
rhsArgs [MArgTy]
margs [Name]
anames)
Int -> String -> Idris ()
logElab Int
2 (String
"Top level type: " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
ty')
Int -> String -> Idris ()
logElab Int
1 (forall a. Show a => a -> String
show (Name
m, PTerm
ty', PTerm
capp, [MArgTy]
margs))
Int -> String -> Idris ()
logElab Int
2 (String
"Definition: " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs forall a. [a] -> [a] -> [a]
++ String
" = " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
rhs)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> t
-> PDecl' t
PTy Docstring (Either Err PTerm)
doc [] SyntaxInfo
syn FC
fc FnOpts
o Name
m FC
mfc PTerm
ty',
forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc [FnOpt
Inlinable] Name
m [forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
m PTerm
lhs [] PTerm
rhs []])
getMArgs :: PTerm -> [MArgTy]
getMArgs (PPi (Imp [ArgOpt]
_ Static
_ Bool
_ Maybe ImplicitInfo
_ Bool
_ RigCount
_) Name
n FC
_ PTerm
ty PTerm
sc) = Name -> MArgTy
IA Name
n forall a. a -> [a] -> [a]
: PTerm -> [MArgTy]
getMArgs PTerm
sc
getMArgs (PPi (Exp [ArgOpt]
_ Static
_ Bool
_ RigCount
_) Name
n FC
_ PTerm
ty PTerm
sc) = Name -> MArgTy
EA Name
n forall a. a -> [a] -> [a]
: PTerm -> [MArgTy]
getMArgs PTerm
sc
getMArgs (PPi (Constraint [ArgOpt]
_ Static
_ RigCount
_) Name
n FC
_ PTerm
ty PTerm
sc) = MArgTy
CA forall a. a -> [a] -> [a]
: PTerm -> [MArgTy]
getMArgs PTerm
sc
getMArgs PTerm
_ = []
getMeth :: [Name] -> [Name] -> Name -> PTerm
getMeth :: [Name] -> [Name] -> Name -> PTerm
getMeth (Name
m:[Name]
ms) (Name
a:[Name]
as) Name
x | Name
x forall a. Eq a => a -> a -> Bool
== Name
a = FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
m
| Bool
otherwise = [Name] -> [Name] -> Name -> PTerm
getMeth [Name]
ms [Name]
as Name
x
lhsArgs :: [MArgTy] -> [a] -> [PArg]
lhsArgs (EA Name
_ : [MArgTy]
xs) (a
n : [a]
ns) = []
lhsArgs (IA Name
n : [MArgTy]
xs) [a]
ns = forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) Bool
False forall a. a -> [a] -> [a]
: [MArgTy] -> [a] -> [PArg]
lhsArgs [MArgTy]
xs [a]
ns
lhsArgs (MArgTy
CA : [MArgTy]
xs) [a]
ns = [MArgTy] -> [a] -> [PArg]
lhsArgs [MArgTy]
xs [a]
ns
lhsArgs [] [a]
_ = []
rhsArgs :: [MArgTy] -> [a] -> [PArg]
rhsArgs (EA Name
_ : [MArgTy]
xs) (a
n : [a]
ns) = []
rhsArgs (IA Name
n : [MArgTy]
xs) [a]
ns = forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) forall a. a -> [a] -> [a]
: [MArgTy] -> [a] -> [PArg]
rhsArgs [MArgTy]
xs [a]
ns
rhsArgs (MArgTy
CA : [MArgTy]
xs) [a]
ns = forall {t}. t -> PArg' t
pconst (FC -> PTerm
PResolveTC FC
fc) forall a. a -> [a] -> [a]
: [MArgTy] -> [a] -> [PArg]
rhsArgs [MArgTy]
xs [a]
ns
rhsArgs [] [a]
_ = []
insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm
insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm
insertConstraint PTerm
c [Name]
all PTerm
sc
= let dictN :: Name
dictN = Int -> String -> Name
sMN Int
0 String
"__interface" in
Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
constraint { pstatic :: Static
pstatic = Static
Static })
Name
dictN FC
NoFC PTerm
c
([Name] -> Name -> PTerm -> PTerm
constrainMeths (forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
basename [Name]
all)
Name
dictN PTerm
sc)
where
constrainMeths :: [Name] -> Name -> PTerm -> PTerm
constrainMeths :: [Name] -> Name -> PTerm -> PTerm
constrainMeths [Name]
allM Name
dictN PTerm
tm = forall on. Uniplate on => (on -> on) -> on -> on
transform (forall {t :: * -> *}.
Foldable t =>
t Name -> Name -> PTerm -> PTerm
addC [Name]
allM Name
dictN) PTerm
tm
addC :: t Name -> Name -> PTerm -> PTerm
addC t Name
allM Name
dictN m :: PTerm
m@(PRef FC
fc [FC]
hls Name
n)
| Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
allM = FC -> PTerm -> [PArg] -> PTerm
PApp FC
NoFC PTerm
m [forall {t}. t -> PArg' t
pconst (FC -> [FC] -> Name -> PTerm
PRef FC
NoFC [FC]
hls Name
dictN)]
| Bool
otherwise = PTerm
m
addC t Name
_ Name
_ PTerm
tm = PTerm
tm
toExp :: t Name
-> ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity)
-> PTerm
-> PTerm
toExp t Name
ns [ArgOpt] -> Static -> Bool -> RigCount -> Plicity
e (PPi (Imp [ArgOpt]
l Static
s Bool
p Maybe ImplicitInfo
_ Bool
_ RigCount
r) Name
n FC
fc PTerm
ty PTerm
sc)
| Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
ns = t Name
-> ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity)
-> PTerm
-> PTerm
toExp t Name
ns [ArgOpt] -> Static -> Bool -> RigCount -> Plicity
e PTerm
sc
| Bool
otherwise = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity
e [ArgOpt]
l Static
s Bool
p RigCount
r) Name
n FC
fc PTerm
ty (t Name
-> ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity)
-> PTerm
-> PTerm
toExp t Name
ns [ArgOpt] -> Static -> Bool -> RigCount -> Plicity
e PTerm
sc)
toExp t Name
ns [ArgOpt] -> Static -> Bool -> RigCount -> Plicity
e (PPi Plicity
p Name
n FC
fc PTerm
ty PTerm
sc) = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p Name
n FC
fc PTerm
ty (t Name
-> ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity)
-> PTerm
-> PTerm
toExp t Name
ns [ArgOpt] -> Static -> Bool -> RigCount -> Plicity
e PTerm
sc)
toExp t Name
ns [ArgOpt] -> Static -> Bool -> RigCount -> Plicity
e PTerm
sc = PTerm
sc
memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))
memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))
memberDocs (PTy Docstring (Either Err PTerm)
d [(Name, Docstring (Either Err PTerm))]
_ SyntaxInfo
_ FC
_ FnOpts
_ Name
n FC
_ PTerm
_) = forall a. a -> Maybe a
Just (Name -> Name
basename Name
n, Docstring (Either Err PTerm)
d)
memberDocs (PPostulate Bool
_ Docstring (Either Err PTerm)
d SyntaxInfo
_ FC
_ FC
_ FnOpts
_ Name
n PTerm
_) = forall a. a -> Maybe a
Just (Name -> Name
basename Name
n, Docstring (Either Err PTerm)
d)
memberDocs (PData Docstring (Either Err PTerm)
d [(Name, Docstring (Either Err PTerm))]
_ SyntaxInfo
_ FC
_ DataOpts
_ PData' PTerm
pdata) = forall a. a -> Maybe a
Just (Name -> Name
basename forall a b. (a -> b) -> a -> b
$ forall t. PData' t -> Name
d_name PData' PTerm
pdata, Docstring (Either Err PTerm)
d)
memberDocs (PRecord Docstring (Either Err PTerm)
d SyntaxInfo
_ FC
_ DataOpts
_ Name
n FC
_ [(Name, FC, Plicity, PTerm)]
_ [(Name, Docstring (Either Err PTerm))]
_ [(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
_ Maybe (Name, FC)
_ Docstring (Either Err PTerm)
_ SyntaxInfo
_ ) = forall a. a -> Maybe a
Just (Name -> Name
basename Name
n, Docstring (Either Err PTerm)
d)
memberDocs (PInterface Docstring (Either Err PTerm)
d SyntaxInfo
_ FC
_ [(Name, PTerm)]
_ Name
n FC
_ [(Name, FC, PTerm)]
_ [(Name, Docstring (Either Err PTerm))]
_ [(Name, FC)]
_ [PDecl]
_ Maybe (Name, FC)
_ Docstring (Either Err PTerm)
_) = forall a. a -> Maybe a
Just (Name -> Name
basename Name
n, Docstring (Either Err PTerm)
d)
memberDocs PDecl
_ = forall a. Maybe a
Nothing
expandMethNS :: SyntaxInfo
-> PTerm -> PTerm
expandMethNS :: SyntaxInfo -> PTerm -> PTerm
expandMethNS SyntaxInfo
syn = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT PTerm -> PTerm
expand
where
expand :: PTerm -> PTerm
expand (PRef FC
fc [FC]
hls Name
n) | Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` SyntaxInfo -> [Name]
imp_methods SyntaxInfo
syn = FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC]
hls forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n
expand PTerm
t = PTerm
t
findDets :: Name -> [Name] -> Idris [Int]
findDets :: Name -> [Name] -> Idris [Int]
findDets Name
n [Name]
ns =
do IState
i <- Idris IState
getIState
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Name -> Context -> Maybe Type
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
i) of
Just Type
ty -> forall {t :: * -> *} {a} {t}.
(Foldable t, Eq a, Num t) =>
t -> t a -> TT a -> [t]
getDetPos Int
0 [Name]
ns Type
ty
Maybe Type
Nothing -> []
where
getDetPos :: t -> t a -> TT a -> [t]
getDetPos t
i t a
ns (Bind a
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT a
_ TT a
_) TT a
sc)
| a
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
ns = t
i forall a. a -> [a] -> [a]
: t -> t a -> TT a -> [t]
getDetPos (t
i forall a. Num a => a -> a -> a
+ t
1) t a
ns TT a
sc
| Bool
otherwise = t -> t a -> TT a -> [t]
getDetPos (t
i forall a. Num a => a -> a -> a
+ t
1) t a
ns TT a
sc
getDetPos t
_ t a
_ TT a
_ = []