module Idris.Elab.Instance(elabInstance) where
import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.DSL
import Idris.Error
import Idris.Delaborate
import Idris.Imports
import Idris.ElabTerm
import Idris.Coverage
import Idris.DataOpts
import Idris.Providers
import Idris.Primitives
import Idris.Inliner
import Idris.PartialEval
import Idris.DeepSeq
import Idris.Output (iputStrLn, pshow, iWarn)
import IRTS.Lang
import Idris.Elab.Type
import Idris.Elab.Data
import Idris.Elab.Utils
import Idris.Core.TT
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.Execute
import Idris.Core.Typecheck
import Idris.Core.CaseTree
import Idris.Docstrings
import Prelude hiding (id, (.))
import Control.Category
import Control.Applicative hiding (Const)
import Control.DeepSeq
import Control.Monad
import Control.Monad.State.Strict as State
import Data.List
import Data.Maybe
import Debug.Trace
import qualified Data.Map as Map
import qualified Data.Set as S
import qualified Data.Text as T
import Data.Char(isLetter, toLower)
import Data.List.Split (splitOn)
import Util.Pretty(pretty, text)
elabInstance :: ElabInfo -> SyntaxInfo ->
ElabWhat ->
FC -> [PTerm] ->
Name ->
[PTerm] ->
PTerm ->
Maybe Name ->
[PDecl] -> Idris ()
elabInstance info syn what fc cs n ps t expn ds = do
i <- getIState
(n, ci) <- case lookupCtxtName n (idris_classes i) of
[c] -> return c
[] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
cs -> tclift $ tfail $ At fc
(CantResolveAlts (map fst cs))
let constraint = PApp fc (PRef fc n) (map pexp ps)
let iname = mkiname n ps expn
let emptyclass = null (class_methods ci)
when (what /= EDefns || (null ds && not emptyclass)) $ do
nty <- elabType' True info syn emptyDocstring [] fc [] iname t
case expn of
Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (delab i nty))
(class_instances ci)
addInstance intInst n iname
Just _ -> addInstance intInst n iname
when (what /= ETypes && (not (null ds && not emptyclass))) $ do
let ips = zip (class_params ci) ps
let ns = case n of
NS n ns' -> ns'
_ -> []
wparams <- mapM (\p -> case p of
PApp _ _ args -> getWParams (map getTm args)
_ -> return []) ps
let pnames = map pname (concat (nub wparams))
let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)
undefinedSuperclassInstances <- filterM (fmap not . isOverlapping i) superclassInstances
mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances
let all_meths = map (nsroot . fst) (class_methods ci)
let mtys = map (\ (n, (op, t)) ->
let t_in = substMatchesShadow ips pnames t
mnamemap = map (\n -> (n, PRef fc (decorate ns iname n)))
all_meths
t' = substMatchesShadow mnamemap pnames t_in in
(decorate ns iname n,
op, coninsert cs t', t'))
(class_methods ci)
logLvl 3 (show (mtys, ips))
let ds' = insertDefaults i iname (class_defaults ci) ns ds
iLOG ("Defaults inserted: " ++ show ds' ++ "\n" ++ show ci)
mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))
mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')
let wbTys = map mkTyDecl mtys
let wbVals = map (decorateid (decorate ns iname)) ds'
let wb = wbTys ++ wbVals
logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)
logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++
show (concat (nub wparams))
ist <- getIState
let headVars = nub $ mapMaybe (\p -> case p of
PRef _ n ->
case lookupTy n (tt_ctxt ist) of
[] -> Just n
_ -> Nothing
_ -> Nothing) ps
let lhs = PApp fc (PRef fc iname)
(map (\n -> pimp n (PRef fc n) True) headVars)
let rhs = PApp fc (PRef fc (instanceName ci))
(map (pexp . mkMethApp) mtys)
logLvl 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars
logLvl 5 $ "Instance RHS " ++ show rhs
let idecls = [PClauses fc [Dictionary] iname
[PClause fc iname lhs [] rhs wb]]
iLOG (show idecls)
mapM_ (rec_elabDecl info EAll info) idecls
addIBC (IBCInstance intInst n iname)
where
intInst = case ps of
[PConstant (AType (ATInt ITNative))] -> True
_ -> False
mkiname n' ps' expn' =
case expn' of
Nothing -> SN (sInstanceN n' (map show ps'))
Just nm -> nm
substInstance ips pnames (PInstance syn _ cs n ps t expn ds)
= PInstance syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds
isOverlapping i (PInstance syn _ _ n ps t expn _)
= case lookupCtxtName n (idris_classes i) of
[(n, ci)] -> let iname = (mkiname n ps expn) in
case lookupTy iname (tt_ctxt i) of
[] -> elabFindOverlapping i ci iname syn t
(_:_) -> return True
_ -> return False
elabFindOverlapping i ci iname syn t
= do ty' <- addUsingConstraints syn fc t
ty' <- implicit info syn iname ty'
let ty = addImpl i ty'
ctxt <- getContext
((tyT, _, _), _) <-
tclift $ elaborate ctxt iname (TType (UVal 0)) []
(errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))
ctxt <- getContext
(cty, _) <- recheckC fc [] tyT
let nty = normalise ctxt [] cty
return $ any (isJust . findOverlapping i (delab i nty)) (class_instances ci)
findOverlapping i t n
| take 2 (show n) == "@@" = Nothing
| otherwise
= case lookupTy n (tt_ctxt i) of
[t'] -> let tret = getRetType t
tret' = getRetType (delab i t') in
case matchClause i tret' tret of
Right ms -> Just tret'
Left _ -> case matchClause i tret tret' of
Right ms -> Just tret'
Left _ -> Nothing
_ -> Nothing
overlapping t' = tclift $ tfail (At fc (Msg $
"Overlapping instance: " ++ show t' ++ " already defined"))
getRetType (PPi _ _ _ sc) = getRetType sc
getRetType t = t
mkMethApp (n, _, _, ty)
= lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
lamBind i (PPi (Constraint _ _) _ _ sc) sc'
= PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
lamBind i (PPi _ n ty sc) sc'
= PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
lamBind i _ sc = sc
methArgs i (PPi (Imp _ _ _) n ty sc)
= PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc
methArgs i (PPi (Exp _ _ _) n ty sc)
= PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc
methArgs i (PPi (Constraint _ _) n ty sc)
= PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc
methArgs i _ = []
papp fc f [] = f
papp fc f as = PApp fc f as
getWParams [] = return []
getWParams (p : ps)
| PRef _ n <- p
= do ps' <- getWParams ps
ctxt <- getContext
case lookupP n ctxt of
[] -> return (pimp n (PRef fc n) True : ps')
_ -> return ps'
getWParams (_ : ps) = getWParams ps
decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t
conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
conbind [] x = x
coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)
coninsert cs sc = conbind cs sc
insertDefaults :: IState -> Name ->
[(Name, (Name, PDecl))] -> [T.Text] ->
[PDecl] -> [PDecl]
insertDefaults i iname [] ns ds = ds
insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds
= insertDefaults i iname defs ns (insertDef i n dn clauses ns iname ds)
insertDef i meth def clauses ns iname decls
| null $ filter (clauseFor meth iname ns) decls
= let newd = expandParamsD False i (\n -> meth) [] [def] clauses in
decls ++ [newd]
| otherwise = decls
warnMissing decls ns iname meth
| null $ filter (clauseFor meth iname ns) decls
= iWarn fc . text $ "method " ++ show meth ++ " not defined"
| otherwise = return ()
checkInClass ns meth
| not (null (filter (eqRoot meth) ns)) = return ()
| otherwise = tclift $ tfail (At fc (Msg $
show meth ++ " not a method of class " ++ show n))
eqRoot x y = nsroot x == nsroot y
clauseFor m iname ns (PClauses _ _ m' _)
= decorate ns iname m == decorate ns iname m'
clauseFor m iname ns _ = False