git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/Elab/Instance.hs
328 lines 14 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 (class_determiners ci) (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 a@(PRef fc f) -> getWParams [a]
92 _ -> return []) ps
93 ist <- getIState
94 let pnames = nub $ map pname (concat (nub wparams)) ++
95 concatMap (namesIn [] ist) ps
96 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)
97 undefinedSuperclassInstances <- filterM (fmap not . isOverlapping i) superclassInstances
98 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances
99 let all_meths = map (nsroot . fst) (class_methods ci)
100 let mtys = map (\ (n, (op, t)) ->
101 let t_in = substMatchesShadow ips pnames t
102 mnamemap = map (\n -> (n, PRef fc (decorate ns iname n)))
103 all_meths
104 t' = substMatchesShadow mnamemap pnames t_in in
105 (decorate ns iname n,
106 op, coninsert cs t', t'))
107 (class_methods ci)
108 logLvl 3 (show (mtys, ips))
109 logLvl 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (class_methods ci)))
110 let ds_defs = insertDefaults i iname (class_defaults ci) ns ds
111 logLvl 3 ("After defaults: " ++ show ds_defs ++ "\n")
112 let ds' = reorderDefs (map fst (class_methods ci)) $ ds_defs
113 iLOG ("Reordered: " ++ show ds' ++ "\n")
114 mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))
115 mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')
116 let wbTys = map mkTyDecl mtys
117 let wbVals = map (decorateid (decorate ns iname)) ds'
118 let wb = wbTys ++ wbVals
119 logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)
120 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++
121 show (concat (nub wparams))
123 -- Bring variables in instance head into scope
124 let headVars = nub $ mapMaybe (\p -> case p of
125 PRef _ n ->
126 case lookupTy n (tt_ctxt ist) of
127 [] -> Just n
128 _ -> Nothing
129 _ -> Nothing) ps
130-- let lhs = PRef fc iname
131 let lhs = PApp fc (PRef fc iname)
132 (map (\n -> pimp n (PRef fc n) True) headVars)
133 let rhs = PApp fc (PRef fc (instanceName ci))
134 (map (pexp . mkMethApp) mtys)
136 logLvl 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars
137 logLvl 5 $ "Instance RHS " ++ show rhs
139 let idecls = [PClauses fc [Dictionary] iname
140 [PClause fc iname lhs [] rhs wb]]
141 iLOG (show idecls)
142 mapM_ (rec_elabDecl info EAll info) idecls
143 ist <- getIState
144 checkInjectiveArgs fc n (class_determiners ci) (lookupTyExact iname (tt_ctxt ist))
145 addIBC (IBCInstance intInst n iname)
147 where
148 intInst = case ps of
149 [PConstant (AType (ATInt ITNative))] -> True
150 _ -> False
152 mkiname n' ns ps' expn' =
153 case expn' of
154 Nothing -> case ns of
155 Nothing -> SN (sInstanceN n' (map show ps'))
156 Just m -> sNS (SN (sInstanceN n' (map show ps'))) m
157 Just nm -> nm
159 substInstance ips pnames (PInstance doc argDocs syn _ cs n ps t expn ds)
160 = PInstance doc argDocs syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds
162 isOverlapping i (PInstance doc argDocs syn _ _ n ps t expn _)
163 = case lookupCtxtName n (idris_classes i) of
164 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in
165 case lookupTy iname (tt_ctxt i) of
166 [] -> elabFindOverlapping i ci iname syn t
167 (_:_) -> return True
168 _ -> return False -- couldn't find class, just let elabInstance fail later
170 -- TODO: largely based upon elabType' - should try to abstract
171 -- Issue #1614 in the issue tracker:
172 -- https://github.com/idris-lang/Idris-dev/issues/1614
173 elabFindOverlapping i ci iname syn t
174 = do ty' <- addUsingConstraints syn fc t
175 -- TODO think: something more in info?
176 ty' <- implicit info syn iname ty'
177 let ty = addImpl [] i ty'
178 ctxt <- getContext
179 (ElabResult tyT _ _ ctxt' newDecls, _) <-
180 tclift $ elaborate ctxt iname (TType (UVal 0)) initEState
181 (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))
182 setContext ctxt'
183 processTacticDecls newDecls
184 ctxt <- getContext
185 (cty, _) <- recheckC fc id [] tyT
186 let nty = normalise ctxt [] cty
187 return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (class_instances ci)
189 findOverlapping i dets t n
190 | take 2 (show n) == "@@" = Nothing
191 | otherwise
192 = case lookupTy n (tt_ctxt i) of
193 [t'] -> let tret = getRetType t
194 tret' = getRetType (delab i t') in
195 case matchArgs i dets tret' tret of
196 Right _ -> Just tret'
197 Left _ -> case matchArgs i dets tret tret' of
198 Right _ -> Just tret'
199 Left _ -> Nothing
200 _ -> Nothing
201 overlapping t' = tclift $ tfail (At fc (Msg $
202 "Overlapping instance: " ++ show t' ++ " already defined"))
203 getRetType (PPi _ _ _ sc) = getRetType sc
204 getRetType t = t
206 matchArgs i dets x y =
207 let x' = keepDets dets x
208 y' = keepDets dets y in
209 matchClause i x' y'
211 keepDets dets (PApp fc f args)
212 = PApp fc f $ let a' = zip [0..] args in
213 map snd (filter (\(i, _) -> i `elem` dets) a')
214 keepDets dets t = t
216 mkMethApp (n, _, _, ty)
217 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
218 lamBind i (PPi (Constraint _ _) _ _ sc) sc'
219 = PLam fc (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
220 lamBind i (PPi _ n ty sc) sc'
221 = PLam fc (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
222 lamBind i _ sc = sc
223 methArgs i (PPi (Imp _ _ _ _) n ty sc)
224 = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc
225 methArgs i (PPi (Exp _ _ _) n ty sc)
226 = PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc
227 methArgs i (PPi (Constraint _ _) n ty sc)
228 = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc
229 methArgs i _ = []
231 papp fc f [] = f
232 papp fc f as = PApp fc f as
234 getWParams [] = return []
235 getWParams (p : ps)
236 | PRef _ n <- p
237 = do ps' <- getWParams ps
238 ctxt <- getContext
239 case lookupP n ctxt of
240 [] -> return (pimp n (PRef fc n) True : ps')
241 _ -> return ps'
242 getWParams (_ : ps) = getWParams ps
244 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
245 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
247 mkTyDecl (n, op, t, _)
248 = PTy emptyDocstring [] syn fc op n
249 (mkUniqueNames [] t)
251 conbind :: [(Name, PTerm)] -> PTerm -> PTerm
252 conbind ((c,ty) : ns) x = PPi constraint c ty (conbind ns x)
253 conbind [] x = x
255 coninsert :: [(Name, PTerm)] -> PTerm -> PTerm
256 coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)
257 coninsert cs sc = conbind cs sc
259 -- Reorder declarations to be in the same order as defined in the
260 -- class declaration (important so that we insert default definitions
261 -- in the right place, and so that dependencies between methods are
262 -- respected)
263 reorderDefs :: [Name] -> [PDecl] -> [PDecl]
264 reorderDefs ns [] = []
265 reorderDefs [] ds = ds
266 reorderDefs (n : ns) ds = case pick n [] ds of
267 Just (def, ds') -> def : reorderDefs ns ds'
268 Nothing -> reorderDefs ns ds
270 pick n acc [] = Nothing
271 pick n acc (def@(PClauses _ _ cn cs) : ds)
272 | nsroot n == nsroot cn = Just (def, acc ++ ds)
273 pick n acc (d : ds) = pick n (acc ++ [d]) ds
275 insertDefaults :: IState -> Name ->
276 [(Name, (Name, PDecl))] -> [T.Text] ->
277 [PDecl] -> [PDecl]
278 insertDefaults i iname [] ns ds = ds
279 insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds
280 = insertDefaults i iname defs ns (insertDef i n dn clauses ns iname ds)
282 insertDef i meth def clauses ns iname decls
283 | null $ filter (clauseFor meth iname ns) decls
284 = let newd = expandParamsD False i (\n -> meth) [] [def] clauses in
285 -- trace (show newd) $
286 decls ++ [newd]
287 | otherwise = decls
289 warnMissing decls ns iname meth
290 | null $ filter (clauseFor meth iname ns) decls
291 = iWarn fc . text $ "method " ++ show meth ++ " not defined"
292 | otherwise = return ()
294 checkInClass ns meth
295 | not (null (filter (eqRoot meth) ns)) = return ()
296 | otherwise = tclift $ tfail (At fc (Msg $
297 show meth ++ " not a method of class " ++ show n))
299 eqRoot x y = nsroot x == nsroot y
301 clauseFor m iname ns (PClauses _ _ m' _)
302 = decorate ns iname m == decorate ns iname m'
303 clauseFor m iname ns _ = False
305checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()
306checkInjectiveArgs fc n ds Nothing = return ()
307checkInjectiveArgs fc n ds (Just ty)
308 = do ist <- getIState
309 let (_, args) = unApply (instantiateRetTy ty)
310 ci 0 ist args
311 where
312 ci i ist (a : as) | i `elem` ds
313 = if isInj ist a then ci (i + 1) ist as
314 else tclift $ tfail (At fc (InvalidTCArg n a))
315 ci i ist (a : as) = ci (i + 1) ist as
316 ci i ist [] = return ()
318 isInj i (P Bound n _) = True
319 isInj i (P _ n _) = isConName n (tt_ctxt i)
320 isInj i (App f a) = isInj i f && isInj i a
321 isInj i (V _) = True
322 isInj i (Bind n b sc) = isInj i sc
323 isInj _ _ = True
325 instantiateRetTy (Bind n (Pi _ _ _) sc)
326 = substV (P Bound n Erased) (instantiateRetTy sc)
327 instantiateRetTy t = t