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