git.iko.soy/Idris-dev
on 13ebfcf help sign in
Idris-dev/src/Idris/Elab/Instance.hs
266 lines 11 kB history raw
1{-# LANGUAGE PatternGuards #-}
2module Idris.Elab.Instance(elabInstance) where
4import Idris.AbsSyntax
5import Idris.ASTUtils
6import Idris.DSL
7import Idris.Error
8import Idris.Delaborate
9import Idris.Imports
10import Idris.ElabTerm
11import Idris.Coverage
12import Idris.DataOpts
13import Idris.Providers
14import Idris.Primitives
15import Idris.Inliner
16import Idris.PartialEval
17import Idris.DeepSeq
18import Idris.Output (iputStrLn, pshow, iWarn)
19import IRTS.Lang
21import Idris.Elab.Type
22import Idris.Elab.Data
23import Idris.Elab.Utils
25import Idris.Core.TT
26import Idris.Core.Elaborate hiding (Tactic(..))
27import Idris.Core.Evaluate
28import Idris.Core.Execute
29import Idris.Core.Typecheck
30import Idris.Core.CaseTree
32import Idris.Docstrings
34import Prelude hiding (id, (.))
35import Control.Category
37import Control.Applicative hiding (Const)
38import Control.DeepSeq
39import Control.Monad
40import Control.Monad.State.Strict as State
41import Data.List
42import Data.Maybe
43import Debug.Trace
45import qualified Data.Map as Map
46import qualified Data.Set as S
47import qualified Data.Text as T
48import Data.Char(isLetter, toLower)
49import Data.List.Split (splitOn)
51import Util.Pretty(pretty, text)
53elabInstance :: ElabInfo -> SyntaxInfo ->
54 Docstring (Either Err PTerm) ->
55 [(Name, Docstring (Either Err PTerm))] ->
56 ElabWhat -> -- phase
57 FC -> [(Name, PTerm)] -> -- constraints
58 Name -> -- the class
59 [PTerm] -> -- class parameters (i.e. instance)
60 PTerm -> -- full instance type
61 Maybe Name -> -- explicit name
62 [PDecl] -> Idris ()
63elabInstance info syn doc argDocs what fc cs n ps t expn ds = do
64 i <- getIState
65 (n, ci) <- case lookupCtxtName n (idris_classes i) of
66 [c] -> return c
67 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
68 cs -> tclift $ tfail $ At fc
69 (CantResolveAlts (map fst cs))
70 let constraint = PApp fc (PRef fc n) (map pexp ps)
71 let iname = mkiname n (namespace info) ps expn
72 let emptyclass = null (class_methods ci)
73 when (what /= EDefns || (null ds && not emptyclass)) $ do
74 nty <- elabType' True info syn doc argDocs fc [] iname t
75 -- if the instance type matches any of the instances we have already,
76 -- and it's not a named instance, then it's overlapping, so report an error
77 case expn of
78 Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (delab i nty))
79 (class_instances ci)
80 addInstance intInst n iname
81 Just _ -> addInstance intInst n iname
82 when (what /= ETypes && (not (null ds && not emptyclass))) $ do
83 let ips = zip (class_params ci) ps
84 let ns = case n of
85 NS n ns' -> ns'
86 _ -> []
87 -- get the implicit parameters that need passing through to the
88 -- where block
89 wparams <- mapM (\p -> case p of
90 PApp _ _ args -> getWParams (map getTm args)
91 _ -> return []) ps
92 let pnames = map pname (concat (nub wparams))
93 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)
94 undefinedSuperclassInstances <- filterM (fmap not . isOverlapping i) superclassInstances
95 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances
96 let all_meths = map (nsroot . fst) (class_methods ci)
97 let mtys = map (\ (n, (op, t)) ->
98 let t_in = substMatchesShadow ips pnames t
99 mnamemap = map (\n -> (n, PRef fc (decorate ns iname n)))
100 all_meths
101 t' = substMatchesShadow mnamemap pnames t_in in
102 (decorate ns iname n,
103 op, coninsert cs t', t'))
104 (class_methods ci)
105 logLvl 3 (show (mtys, ips))
106 let ds' = insertDefaults i iname (class_defaults ci) ns ds
107 iLOG ("Defaults inserted: " ++ show ds' ++ "\n" ++ show ci)
108 mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))
109 mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')
110 let wbTys = map mkTyDecl mtys
111 let wbVals = map (decorateid (decorate ns iname)) ds'
112 let wb = wbTys ++ wbVals
113 logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)
114 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++
115 show (concat (nub wparams))
117 -- Bring variables in instance head into scope
118 ist <- getIState
119 let headVars = nub $ mapMaybe (\p -> case p of
120 PRef _ n ->
121 case lookupTy n (tt_ctxt ist) of
122 [] -> Just n
123 _ -> Nothing
124 _ -> Nothing) ps
125-- let lhs = PRef fc iname
126 let lhs = PApp fc (PRef fc iname)
127 (map (\n -> pimp n (PRef fc n) True) headVars)
128 let rhs = PApp fc (PRef fc (instanceName ci))
129 (map (pexp . mkMethApp) mtys)
131 logLvl 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars
132 logLvl 5 $ "Instance RHS " ++ show rhs
134 let idecls = [PClauses fc [Dictionary] iname
135 [PClause fc iname lhs [] rhs wb]]
136 iLOG (show idecls)
137 mapM_ (rec_elabDecl info EAll info) idecls
138 addIBC (IBCInstance intInst n iname)
140 where
141 intInst = case ps of
142 [PConstant (AType (ATInt ITNative))] -> True
143 _ -> False
145 mkiname n' ns ps' expn' =
146 case expn' of
147 Nothing -> case ns of
148 Nothing -> SN (sInstanceN n' (map show ps'))
149 Just m -> sNS (SN (sInstanceN n' (map show ps'))) m
150 Just nm -> nm
152 substInstance ips pnames (PInstance doc argDocs syn _ cs n ps t expn ds)
153 = PInstance doc argDocs syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds
155 isOverlapping i (PInstance doc argDocs syn _ _ n ps t expn _)
156 = case lookupCtxtName n (idris_classes i) of
157 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in
158 case lookupTy iname (tt_ctxt i) of
159 [] -> elabFindOverlapping i ci iname syn t
160 (_:_) -> return True
161 _ -> return False -- couldn't find class, just let elabInstance fail later
163 -- TODO: largely based upon elabType' - should try to abstract
164 -- Issue #1614 in the issue tracker:
165 -- https://github.com/idris-lang/Idris-dev/issues/1614
166 elabFindOverlapping i ci iname syn t
167 = do ty' <- addUsingConstraints syn fc t
168 -- TODO think: something more in info?
169 ty' <- implicit info syn iname ty'
170 let ty = addImpl i ty'
171 ctxt <- getContext
172 ((tyT, _, _), _) <-
173 tclift $ elaborate ctxt iname (TType (UVal 0)) initEState
174 (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))
175 ctxt <- getContext
176 (cty, _) <- recheckC fc [] tyT
177 let nty = normalise ctxt [] cty
178 return $ any (isJust . findOverlapping i (delab i nty)) (class_instances ci)
180 findOverlapping i t n
181 | take 2 (show n) == "@@" = Nothing
182 | otherwise
183 = case lookupTy n (tt_ctxt i) of
184 [t'] -> let tret = getRetType t
185 tret' = getRetType (delab i t') in
186 case matchClause i tret' tret of
187 Right ms -> Just tret'
188 Left _ -> case matchClause i tret tret' of
189 Right ms -> Just tret'
190 Left _ -> Nothing
191 _ -> Nothing
192 overlapping t' = tclift $ tfail (At fc (Msg $
193 "Overlapping instance: " ++ show t' ++ " already defined"))
194 getRetType (PPi _ _ _ sc) = getRetType sc
195 getRetType t = t
197 mkMethApp (n, _, _, ty)
198 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
199 lamBind i (PPi (Constraint _ _) _ _ sc) sc'
200 = PLam fc (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
201 lamBind i (PPi _ n ty sc) sc'
202 = PLam fc (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
203 lamBind i _ sc = sc
204 methArgs i (PPi (Imp _ _ _ _) n ty sc)
205 = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc
206 methArgs i (PPi (Exp _ _ _) n ty sc)
207 = PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc
208 methArgs i (PPi (Constraint _ _) n ty sc)
209 = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc
210 methArgs i _ = []
212 papp fc f [] = f
213 papp fc f as = PApp fc f as
215 getWParams [] = return []
216 getWParams (p : ps)
217 | PRef _ n <- p
218 = do ps' <- getWParams ps
219 ctxt <- getContext
220 case lookupP n ctxt of
221 [] -> return (pimp n (PRef fc n) True : ps')
222 _ -> return ps'
223 getWParams (_ : ps) = getWParams ps
225 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
226 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
228 mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t
230 conbind :: [(Name, PTerm)] -> PTerm -> PTerm
231 conbind ((c,ty) : ns) x = PPi constraint c ty (conbind ns x)
232 conbind [] x = x
234 coninsert :: [(Name, PTerm)] -> PTerm -> PTerm
235 coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)
236 coninsert cs sc = conbind cs sc
238 insertDefaults :: IState -> Name ->
239 [(Name, (Name, PDecl))] -> [T.Text] ->
240 [PDecl] -> [PDecl]
241 insertDefaults i iname [] ns ds = ds
242 insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds
243 = insertDefaults i iname defs ns (insertDef i n dn clauses ns iname ds)
245 insertDef i meth def clauses ns iname decls
246 | null $ filter (clauseFor meth iname ns) decls
247 = let newd = expandParamsD False i (\n -> meth) [] [def] clauses in
248 -- trace (show newd) $
249 decls ++ [newd]
250 | otherwise = decls
252 warnMissing decls ns iname meth
253 | null $ filter (clauseFor meth iname ns) decls
254 = iWarn fc . text $ "method " ++ show meth ++ " not defined"
255 | otherwise = return ()
257 checkInClass ns meth
258 | not (null (filter (eqRoot meth) ns)) = return ()
259 | otherwise = tclift $ tfail (At fc (Msg $
260 show meth ++ " not a method of class " ++ show n))
262 eqRoot x y = nsroot x == nsroot y
264 clauseFor m iname ns (PClauses _ _ m' _)
265 = decorate ns iname m == decorate ns iname m'
266 clauseFor m iname ns _ = False