{-|
Module      : Idris.Elab.Interface
Description : Code to elaborate interfaces.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# 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
$cshowsPrec :: Int -> MArgTy -> ShowS
showsPrec :: Int -> MArgTy -> ShowS
$cshow :: MArgTy -> String
show :: MArgTy -> String
$cshowList :: [MArgTy] -> ShowS
showList :: [MArgTy] -> ShowS
Show

elabInterface :: ElabInfo
              -> SyntaxInfo
              -> Docstring (Either Err PTerm)
              -> ElabWhat
              -> FC
              -> [(Name, PTerm)] -- ^ Superclass constraints
              -> Name
              -> FC
              -> [(Name, FC, PTerm)] -- ^ Parameters
              -> [(Name, Docstring (Either Err PTerm))]
              -> [(Name, FC)]                 -- ^ determining params
              -> [PDecl]                      -- ^ interface body
              -> Maybe (Name, FC)             -- ^ implementation ctor name and location
              -> Docstring (Either Err PTerm) -- ^ implementation ctor docs
              -> 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 = 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 b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FC -> [FC] -> Name -> PTerm
PRef FC
fc []) (((Name, FC, PTerm) -> Name) -> [(Name, FC, PTerm)] -> [Name]
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 = addToUsing (using syn_in)
                                 [(pn, pt) | (pn, _, pt) <- ps]
                     }

         -- Calculate implicit parameters
         ist <- Idris IState
getIState
         let 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 (\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 (\ (Name
_,FC
_,PTerm
x) -> PTerm
x) [(Name, FC, PTerm)]
ps)
         let impps = ((Name, FC, PTerm) -> Bool)
-> [(Name, FC, PTerm)] -> [(Name, FC, PTerm)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n, FC
_, PTerm
_) ->
                               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 (\ (Name
n, FC
_, PTerm
_) -> Name
n) [(Name, FC, PTerm)]
ps)) [(Name, FC, PTerm)]
impps_ns

         let tty = [(Name, PTerm)] -> PTerm -> PTerm
impbind (((Name, FC, PTerm) -> (Name, PTerm))
-> [(Name, FC, PTerm)] -> [(Name, PTerm)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, FC
_, 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 (\(Name
n, FC
_, PTerm
ty) -> (Name
n, PTerm
ty)) [(Name, FC, PTerm)]
ps) (FC -> PTerm
PType FC
fc)

         logElab 5 $ "Implicit parameters are " ++ show impps
         logElab 5 $ "Interface type is " ++ showTmImpls tty

         -- build data declaration
         let mdecls = (PDecl -> Bool) -> [PDecl] -> [PDecl]
forall a. (a -> Bool) -> [a] -> [a]
filter PDecl -> Bool
forall {t}. PDecl' t -> Bool
tydecl [PDecl]
ds -- method declarations
         let idecls = (PDecl -> Bool) -> [PDecl] -> [PDecl]
forall a. (a -> Bool) -> [a] -> [a]
filter PDecl -> Bool
forall {t}. PDecl' t -> Bool
impldecl [PDecl]
ds -- default super interface implementation declarations
         mapM_ checkDefaultSuperInterfaceImplementation idecls
         let 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 = (PDecl -> Name) -> [PDecl] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map PDecl -> Name
forall {t}. PDecl' t -> Name
getFullMName [PDecl]
mdecls
         ist <- getIState
         let 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)

         mapM_ (checkConstraintName (map (\(Name
x, FC
_, PTerm
_) -> Name
x) ps)) constraintNames

         let pre_ddecl = Name -> FC -> PTerm -> PData' PTerm
forall t. Name -> FC -> t -> PData' t
PLaterdecl Name
tn FC
NoFC PTerm
tty
         -- Elaborate the interface header, as long as we haven't done it
         -- in an earlier pass
         when (what /= EDefns) $
            elabData info (syn { no_imp = no_imp syn ++ mnames,
                                 imp_methods = mnames }) doc pDocs fc [] pre_ddecl
         -- Continue only if we're not in the first pass of a mutual block
         when (what /= ETypes) $ do
             dets <- findDets tn (map fst fds)

             logElab 3 $ "Building methods " ++ show fullmnames
             ims <- mapM (tdecl impps mnames) mdecls
             defs <- mapM (defdecl (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) ims) constraint)
                          (filter clause ds)
             let 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 (\ ((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), [PDecl])) -> (Name, (Name, PDecl)))
-> [(Name, ((Name, PDecl), [PDecl]))] -> [(Name, (Name, PDecl))]
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

             addInterface tn (CI cn (map nodoc imethods) defaults idecls
                                  (map (\(Name
n, FC
_, PTerm
_) -> Name
n) impps)
                                  (map (\(Name
n, FC
_, PTerm
_) -> Name
n) ps)
                                  (map snd constraints)
                                  [] dets)

             -- for each constraint, build a top level function to chase it
             -- elaborate types now, bodies later (after we've done the constructor
             -- of the interface)
             cfns <- mapM (cfun cn constraint syn (map fst imethods)) constraints
             let (cfnTyDecls, cfnDefs) = unzip cfns
             mapM_ (rec_elabDecl info EAll info) cfnTyDecls

             -- for each method, build a top level function
             -- 'tfun' builds appropriate implicits for the constructor
             -- declaration
             fns <- mapM (tfun cn constraint (syn { imp_methods = mnames }) -- mnames })
                               (map fst imethods)) imethods
             let (fnTyDecls, fnDefs) = unzip fns
             mapM_ (rec_elabDecl info EAll info) fnTyDecls

             elabMethTys <- mapM getElabMethTy fullmnames

             logElab 3 $ "Method types:\n" ++ showSep "\n" (map showTmImpls elabMethTys)

             let cpos = ((Name, PTerm) -> (Name, Int)) -> [(Name, PTerm)] -> [(Name, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, 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)
             logElab 5 $ "Constraint pos: " ++ show cpos

             -- Method types to store in the IState, taken from the elaborated
             -- types with the parameter removed
             let 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)
             updateIMethods tn storemeths

             -- build implementation constructor type
             let cty = [(Name, PTerm)] -> PTerm -> PTerm
impbind [(Name
pn, PTerm
pt) | (Name
pn, FC
_, 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
             logElab 3 $ "Constraint constructor type: " ++ showTmImpls cty

             let 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 = 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

             logElab 10 $ "Interface " ++ show (showDImp verbosePPOption ddecl)


             -- Elaborate the data declaration
             elabData info (syn { no_imp = no_imp syn ++ mnames,
                                  imp_methods = [] }) doc pDocs fc [] ddecl


             logElab 5 $ "Function types " ++ show fnTyDecls
             logElab 5 $ "Method types now: " ++ show imethods

             -- Elaborate the the top level constraint chasers
             -- (Types elaborated earlier)
             mapM_ (rec_elabDecl info EAll info) cfnDefs
             -- Elaborate the the top level method bodies
             mapM_ (rec_elabDecl info EAll info) fnDefs

             -- Flag all the top level data declarations as injective
             mapM_ (\Name
n -> do Name -> Bool -> Idris ()
setInjectivity Name
n Bool
True
                             IBCWrite -> Idris ()
addIBC (Name -> Bool -> IBCWrite
IBCInjective Name
n Bool
True))
                   (map fst (filter (\(Name
_, (Bool
inj, FC
_, Docstring (Either Err PTerm)
_, FnOpts
_, PTerm
_)) -> Bool
inj) imethods))

             -- add the default definitions
             mapM_ (rec_elabDecl info EAll info) (concatMap (snd.snd) defs)
             addIBC (IBCInterface tn)

             sendHighlighting $ S.fromList $
               [(FC' tnfc, AnnName tn Nothing Nothing Nothing)] ++
               [(FC' pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++
               [(FC' fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++
               maybe [] (\(Name
conN, 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)]) mcn

  where
    info :: ElabInfo
info = ElabInfo
info_in { noCaseLift = tn : noCaseLift info_in }

    getElabMethTy :: Name -> Idris PTerm
    getElabMethTy :: Name -> StateT IState (ExceptT Err IO) PTerm
getElabMethTy Name
n = do ist <- Idris IState
getIState
                         let 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 [PArg]
i -> [PArg]
i
                                          Maybe [PArg]
Nothing -> []
                         case lookupTyExact n (tt_ctxt ist) of
                              Just Type
ty -> PTerm -> StateT IState (ExceptT Err IO) PTerm
forall a. a -> StateT IState (ExceptT Err IO) a
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 -> 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 String
"Can't happen, elabMethTy"))

    -- Find the argument position of the current interface in a method type
    -- (we'll use this to update the elaborated top level method types before
    -- building a data declaration
    findConstraint :: PTerm -> Int
    findConstraint :: PTerm -> Int
findConstraint = Int -> PTerm -> Int
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 Name -> Name -> Bool
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 Name -> Name -> Bool
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 t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) PTerm
sc
        findPos t
i PTerm
_ = -t
1 -- Can't happen!

    -- Make the method component of the constructor type by taking the
    -- elaborated top level method and removing the implicits/constraint
    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, 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 Int
i -> Int
i Int -> Int -> Int
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 t -> t -> Bool
forall a. Ord a => a -> a -> Bool
> t
0 = t -> PTerm -> PTerm
dropPis (t
n t -> t -> t
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 <- 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
+ Int
1) [PArg]
args))
        dropImp (PApp FC
fc PTerm
f [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 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))

    -- To make sure the type constructor of the interface is in the appropriate
    -- uniqueness hierarchy
    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 (Universe -> Universe -> Universe
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

    -- TODO: probably should normalise
    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 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 a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, PTerm)]
cs) (Idris () -> Idris ()) -> (TC () -> Idris ()) -> TC () -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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
"Default super interface implementations can't have constraints."))
             i <- Idris IState
getIState
             let 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)
             when (not isConstrained) . tclift
                $ tfail (At fc (Msg "Default implementations must be for a super interface constraint on the containing interface."))
             return ()
            where
                -- First, Check that interface "constraint" has same name & args as default implementation name & args (not checking FC)
                -- If not the case, recursively lookup in context for parent interface & recheck the same with parent constraints
                checkConstrained :: IState -> Name -> [PArg] -> PTerm -> Bool
checkConstrained IState
i Name
n [PArg]
args 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 a. a -> a
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 FC
_ (PRef FC
_ [FC]
_ Name
cn) [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 [Name]
bound 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
$ String
"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]
++
                         String
" 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
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
" " ((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 a. a -> StateT IState (ExceptT Err IO) a
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 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 (\(Name
n, FC
_, PTerm
_) -> 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
                logElab 1 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
                return ( (n, (toExp (map (\(Name
pn, FC
_, PTerm
_) -> Name
pn) ps) Exp t')),
                         (n, (False, nfc, doc, o, (toExp (map (\(Name
pn, FC
_, PTerm
_) -> Name
pn) ps)
                                              (\ [ArgOpt]
l Static
s Bool
p 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) t'))),
                         (n, (nfc, syn, o, 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 = []
                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 (\(Name
n, FC
_, PTerm
_) -> Name
n) [(Name, FC, PTerm)]
ps [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
allmeths) Name
n PTerm
t
                logElab 2 $ "Data method " ++ show n ++ " : " ++ showTmImpls t'
                return ( (n, (toExp (map (\(Name
pn, FC
_, PTerm
_) -> Name
pn) ps) Exp t')),
                         (n, (True, nfc, doc, o, (toExp (map (\(Name
pn, FC
_, PTerm
_) -> Name
pn) ps)
                                              (\ [ArgOpt]
l Static
s Bool
p 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) t'))),
                         (n, (nfc, syn, o, 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
_)
         = 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 String
"Data definitions not allowed in an interface declaration")
    tdecl [(Name, FC, PTerm)]
_ [Name]
_ PDecl
_ = 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 String
"Not allowed in an interface declaration")

    -- Create default definitions
    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 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 (FC
nfc, SyntaxInfo
syn, FnOpts
o, 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 Int
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 a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, ((Name -> Name
defaultdec Name
n, [PDecl]
ds[PDecl] -> Int -> PDecl
forall a. HasCallStack => [a] -> Int -> a
!!Int
1), [PDecl]
ds))
            Maybe (FC, SyntaxInfo, FnOpts, PTerm)
_ -> 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]
++ String
" is not a method"))
    defdecl [(Name, (FC, SyntaxInfo, FnOpts, PTerm))]
_ PTerm
_ PDecl
_ = String
-> StateT IState (ExceptT Err IO) (Name, ((Name, PDecl), [PDecl]))
forall a. String -> Idris a
ifail String
"Can't happen (defdecl)"

    defaultdec :: Name -> Name
defaultdec (UN Text
n) = String -> Name
sUN (String
"default#" String -> ShowS
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

    -- Generate a function for chasing a dictionary constraint
    cfun :: Name -> PTerm -> SyntaxInfo -> [a] -> (Name, PTerm) -> Idris (PDecl, PDecl)
    cfun :: forall a.
Name
-> PTerm
-> SyntaxInfo
-> [a]
-> (Name, PTerm)
-> StateT IState (ExceptT Err IO) (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 (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 a. [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 (\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) ((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 b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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 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: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
ty)
             Int -> String -> Idris ()
logElab Int
2 (PTerm -> String
showTmImpls PTerm
lhs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
rhs)
             i <- Idris IState
getIState
             let conn = case PTerm
con of
                            PRef FC
_ [FC]
_ Name
n -> Name
n
                            PApp FC
_ (PRef FC
_ [FC]
_ Name
n) [PArg]
_ -> Name
n
             let 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
                                [(Name
n, InterfaceInfo
_)] -> Name
n
                                [(Name, InterfaceInfo)]
_ -> Name
conn
             addImplementation False True conn' cfn
             addIBC (IBCImplementation False True conn' cfn)
--              iputStrLn ("Added " ++ show (conn, cfn, ty))
             return (PTy emptyDocstring [] syn fc [] cfn NoFC ty,
                     PClauses fc [Inlinable, Dictionary] cfn [PClause fc cfn lhs [] rhs []])

    -- | Generate a top level function which looks up a method in a given
    -- dictionary (this is inlinable, always)
    tfun :: Name -- ^ The name of the interface
         -> PTerm -- ^ A constraint for the interface, to be inserted under the implicit bindings
         -> SyntaxInfo -> [Name] -- ^ All the method names
         -> (Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))
            -- ^ The present declaration
         -> 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 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 = Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
take ([Name] -> Int
forall a. [a] -> 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 (\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) ((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 b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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 (\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) (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 Int
2 (String
"Top level type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
ty')
             Int -> String -> Idris ()
logElab Int
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 Int
2 (String
"Definition: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
lhs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
rhs)
             (PDecl, PDecl) -> StateT IState (ExceptT Err IO) (PDecl, PDecl)
forall a. a -> StateT IState (ExceptT Err IO) a
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 [ArgOpt]
_ Static
_ Bool
_ Maybe ImplicitInfo
_ Bool
_ RigCount
_) Name
n FC
_ PTerm
ty PTerm
sc) = Name -> MArgTy
IA Name
n MArgTy -> [MArgTy] -> [MArgTy]
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 MArgTy -> [MArgTy] -> [MArgTy]
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 MArgTy -> [MArgTy] -> [MArgTy]
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 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 Name
_ : [MArgTy]
xs) (a
n : [a]
ns) = [] -- pexp (PRef fc n) : lhsArgs xs ns
    lhsArgs (IA Name
n : [MArgTy]
xs) [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 (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) = [] -- pexp (PRef fc n) : rhsArgs xs ns
    rhsArgs (IA Name
n : [MArgTy]
xs) [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 (MArgTy
CA : [MArgTy]
xs) [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 [] [a]
_ = []

    -- Add the top level constraint. Put it first - elaboration will resolve
    -- the order of the implicits if there are dependencies.
    -- Also ensure the dictionary is used for lookup of any methods that
    -- are used in the type
    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 })
                    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
       -- After we insert the constraint into the lookup, we need to
       -- ensure that the same dictionary is used to resolve lookups
       -- to the other methods in the interface
       constrainMeths :: [Name] -> Name -> PTerm -> PTerm
       constrainMeths :: [Name] -> Name -> PTerm -> PTerm
constrainMeths [Name]
allM Name
dictN 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 t Name
allM Name
dictN m :: PTerm
m@(PRef FC
fc [FC]
hls Name
n)
          | Name
n Name -> t Name -> Bool
forall a. Eq a => a -> t a -> 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 t Name
_ Name
_ PTerm
tm = PTerm
tm

    -- make arguments explicit and don't bind interface parameters
    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 Name -> t Name -> Bool
forall a. Eq a => a -> t a -> 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 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

-- | Get the docstring corresponding to a member, if one exists
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
_) = (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 Bool
_ Docstring (Either Err PTerm)
d SyntaxInfo
_ FC
_ FC
_ FnOpts
_ Name
n PTerm
_) = (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 Docstring (Either Err PTerm)
d [(Name, Docstring (Either Err PTerm))]
_ SyntaxInfo
_ FC
_ DataOpts
_ 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 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
_ ) = (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 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)
_) = (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 PDecl
_ = Maybe (Name, Docstring (Either Err PTerm))
forall a. Maybe a
Nothing


-- | In a top level type for a method, expand all the method names' namespaces
-- so that we don't have to disambiguate later
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 Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> 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 PTerm
t = PTerm
t

-- | Find the determining parameter locations
findDets :: Name -> [Name] -> Idris [Int]
findDets :: Name -> [Name] -> Idris [Int]
findDets Name
n [Name]
ns =
    do i <- Idris IState
getIState
       return $ case lookupTyExact n (tt_ctxt i) of
            Just Type
ty -> Int -> [Name] -> Type -> [Int]
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 a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
ns = t
i t -> [t] -> [t]
forall a. a -> [a] -> [a]
: t -> t a -> TT a -> [t]
getDetPos (t
i t -> t -> t
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 t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) t a
ns TT a
sc
    getDetPos t
_ t a
_ TT a
_ = []