@@ -10,14 +10,14 @@ import Data.Function (on)
1010import Data.List (find, minimumBy, partition, sortBy, (\\))
1111import Data.Map (Map)
1212import qualified Data.Map as M
13−import Data.Maybe (catMaybes, fromMaybe, isJust)
13+import Data.Maybe (catMaybes, fromMaybe, isJust, maybeToList)
1414import Data.Monoid (Monoid (mempty, mappend))
1515import Data.Set (Set)
1616import qualified Data.Set as S
1717import qualified Data.Text as T (pack, isPrefixOf)
1818
1919import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)
20−import Idris.AbsSyntaxTree (class_instances, defaultSyntax, Idris,
20+import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, Idris,
2121 IState (idris_classes, idris_docstrings, tt_ctxt),
2222 implicitAllowed, prettyDocumentedIst, prettyIst, PTerm, toplevel)
2323import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
@@ -218,6 +218,25 @@ inArgTys :: (Type -> Type) -> ArgsDAG -> ArgsDAG
218218inArgTys = map . first . second
219219
220220
221+typeclassUnify :: Ctxt ClassInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]
222+typeclassUnify classInfo ctxt ty tyTry = do
223+ res <- tcToMaybe $ match_unify ctxt [] ty retTy [] holes []
224+ guard $ null (holes \\ map fst res)
225+ let argTys' = map (second $ foldr (.) id [ subst n t | (n, t) <- res ]) tcArgs
226+ return argTys'
227+ where
228+ tyTry' = vToP tyTry
229+ holes = map fst nonTcArgs
230+ retTy = getRetTy tyTry'
231+ (tcArgs, nonTcArgs) = partition (isTypeClassArg classInfo . snd) $ getArgTys tyTry'
232+
233+isTypeClassArg :: Ctxt ClassInfo -> Type -> Bool
234+isTypeClassArg classInfo ty = not (null (getClassName clss >>= flip lookupCtxt classInfo)) where
235+ (clss, args) = unApply ty
236+ getClassName (P (TCon _ _) className _) = [className]
237+ getClassName _ = []
238+
239+
221240--DONT run vToP first!
222241-- | Try to match two types together in a unification-like procedure.
223242-- Returns a list of possible scores representing ways in which the two
@@ -238,16 +257,11 @@ unifyWithHoles istate type1 = \type2 -> let
238257 ctxt = tt_ctxt istate
239258 classInfo = idris_classes istate
240259
241− isTypeClassArg :: Type -> Bool
242− isTypeClassArg ty = not (null (getClassName clss >>= flip lookupCtxt classInfo)) where
243− (clss, args) = unApply ty
244− getClassName (P (TCon _ _) className _) = [className]
245− getClassName _ = []
246−
247260 (dag1, typeClassArgs1, retTy1) = makeDag type1
248261 argNames1 = map (fst . fst) dag1
249262 makeDag :: Type -> (ArgsDAG, [(Name, Type)], Type)
250− makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) . computeDagP isTypeClassArg . vToP
263+ makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) .
264+ computeDagP (isTypeClassArg classInfo) . vToP
251265 first3 f (a,b,c) = (f a, b, c)
252266
253267 -- update our state with the unification resolutions
@@ -278,9 +292,13 @@ unifyWithHoles istate type1 = \type2 -> let
278292 (Nothing, Nothing) -> nextStep
279293 _ -> error ("Shouldn't happen. Watch the alpha conversion!\n" ++ show args1 ++ "\n\n" ++ show args2)
280294 where
295+ varsInTy = map fst $ M.toList (usedVars term) --[]
296+ toDelete = name : varsInTy
297+ deleteMany = foldr (.) id $ [ deleteLeft t . deleteRight t | t <- toDelete ]
298+
281299 inScore f state = state { score = f (score state) }
282− state' = modifyTypes (subst name term) . deleteLeft name . deleteRight name $
283− state { holes = holes \\ [name]}
300+ state' = modifyTypes (subst name term) . deleteMany $
301+ state { holes = holes \\ toDelete }
284302 nextStep = resolveUnis xs state'
285303
286304
@@ -288,12 +306,13 @@ unifyWithHoles istate type1 = \type2 -> let
288306 unifyQueue :: State -> [(Type, Type)] -> Maybe State
289307 unifyQueue state [] = return state
290308 unifyQueue state ((ty1, ty2) : queue) = do
309+ --trace ("go: \n" ++ show state) True `seq` return ()
291310 res <- tcToMaybe $ match_unify ctxt [] ty1 ty2 [] (holes state) []
292311 (state', queueAdditions) <- resolveUnis res state
293312 guard $ scoreCriterion (score state')
294313 unifyQueue state' (queue ++ queueAdditions)
295314
296− possClassInstances :: [Name] -> Type -> [([(Name, Type)], Type)]
315+ possClassInstances :: [Name] -> Type -> [Type]
297316 possClassInstances usedNames ty = do
298317 className <- getClassName clss
299318 classDef <- lookupCtxt className classInfo
@@ -301,57 +320,61 @@ unifyWithHoles istate type1 = \type2 -> let
301320 def <- lookupCtxt n (definitions ctxt)
302321 ty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])
303322 let ty' = vToP (uniqueBinders usedNames ty)
304− return (getArgTys ty', getRetTy ty')
323+ return ty'
305324 where
306− (clss, args) = unApply ty
325+ (clss, _) = unApply ty
307326 getClassName (P (TCon _ _) className _) = [className]
308327 getClassName _ = []
309328
329+
330+ collect :: [State] -> [Score]
331+ collect states = concat [ possibleMatches state | state <- states, scoreCriterion (score state) ]
332+
310333 -- | Find all possible matches starting from a given state.
334+ -- We go in stages rather than concatenating all three results in hopes of narrowing
335+ -- the search tree. Once we advance in a phase, there should be no going back.
311336 possibleMatches :: State -> [Score]
337+
338+ -- Stage 3 - we're done!
312339 possibleMatches (State [] [] [] [] [] scoreAcc _) = [scoreAcc]
313− possibleMatches (State holes dag1 dag2 c1 c2 scoreAcc usedNames) =
314− concat [ possibleMatches state | state <- results, scoreCriterion (score state) ] where
340+
341+ -- Stage 2 - match typeclasses
342+ possibleMatches (State [] [] [] c1 c2 scoreAcc usedNames) =
343+ collect (if null results2 then results3 else results2)
344+ where
345+ -- try to match a typeclass argument from the left with a typeclass argument from the right
346+ results2 =
347+ catMaybes [ unifyQueue (State [] [] []
348+ (deleteFromArgList n1 c1) (map (second subst2for1) (deleteFromArgList n2 c2)) scoreAcc usedNames) [(ty1, ty2)]
349+ | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]
350+
351+ -- try to hunt match a typeclass constraint by replacing it with an instance
352+ results3 = results3A ++ results3B
353+ typeClassArgs classes = [ ((n, ty), inst) | (n, ty) <- classes, inst <- possClassInstances usedNames ty ]
354+ results3A = [ State [] [] []
355+ (deleteFromArgList n c1 ++ newClassArgs) c2
356+ (scoreAcc `mappend` (mempty { leftTypeClass = 1 }))
357+ (usedNames ++ newHoles)
358+ | ((n, ty), inst) <- typeClassArgs c1
359+ , newClassArgs <- maybeToList $ typeclassUnify classInfo ctxt ty inst
360+ , let newHoles = map fst newClassArgs ]
361+ results3B = [ State [] [] []
362+ c1 (deleteFromArgList n c2 ++ newClassArgs)
363+ (scoreAcc `mappend` (mempty { rightTypeClass = 1 }))
364+ (usedNames ++ newHoles)
365+ | ((n, ty), inst) <- typeClassArgs c2
366+ , newClassArgs <- maybeToList $ typeclassUnify classInfo ctxt ty inst
367+ , let newHoles = map fst newClassArgs ]
368+
369+ -- Stage 1 - match arguments
370+ possibleMatches (State holes dag1 dag2 c1 c2 scoreAcc usedNames) = collect results1 where
315371
316372 -- we only try to match arguments whose names don't appear in the types
317373 -- of any other arguments
318374 canBeFirst :: ArgsDAG -> [(Name, Type)]
319375 canBeFirst = map fst . filter (S.null . snd . snd)
320376
321− -- this is done rather than concatenating all three results in hopes of narrowing
322− -- the search tree
323− results = fromMaybe [] $ find (not . null) [results1, results2, results3]
324−
325377 -- try to match an argument from the left with an argument from the right
326378 results1 = catMaybes [ unifyQueue (State (holes \\ [n1, n2]) (deleteFromDag n1 dag1)
327379 ((inArgTys subst2for1) $ deleteFromDag n2 dag2) c1 (map (second subst2for1) c2) scoreAcc usedNames) [(ty1, ty2)]
328380 | (n1, ty1) <- canBeFirst dag1, (n2, ty2) <- canBeFirst dag2, let subst2for1 = psubst n2 (P Bound n1 ty1)]
329−
330− -- try to match a typeclass argument from the left with a typeclass argument from the right
331− results2 = catMaybes [ unifyQueue (State (holes \\ [n1, n2]) dag1 (inArgTys subst2for1 dag2)
332− (deleteFromArgList n1 c1) (map (second subst2for1) (deleteFromArgList n2 c2)) scoreAcc usedNames) [(ty1, ty2)]
333− | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]
334−
335− -- try to hunt match a typeclass constraint by replacing it with an instance
336− results3 = if null dag1 || null dag2 then catMaybes (results3A ++ results3B) else []
337− typeClassArgs classes = [ ((n, ty), inst) | (n, ty) <- classes, inst <- possClassInstances usedNames ty ]
338− noDeps (n, ty) = ((n, ty), (0, S.empty))
339− results3A = [ unifyQueue
340− (State ((holes \\ [n]) ++ newHoles) (dag1 ++ map noDeps newNonClassArgs) dag2
341− (deleteFromArgList n c1 ++ newClassArgs) c2
342− (scoreAcc `mappend` (mempty { leftTypeClass = 1 }))
343− (usedNames ++ newHoles)
344− )
345− [(ty, inst)]
346− | ((n, ty), (newArgs, inst)) <- typeClassArgs c1, let newHoles = map fst newArgs
347− , let (newClassArgs, newNonClassArgs) = partition (isTypeClassArg . snd) newArgs ]
348− results3B = [ unifyQueue
349− (State ((holes \\ [n]) ++ newHoles) dag1 (dag2 ++ map noDeps newNonClassArgs)
350− c1 (deleteFromArgList n c2 ++ newClassArgs)
351− (scoreAcc `mappend` (mempty { rightTypeClass = 1 }))
352− (usedNames ++ newHoles)
353− )
354− [(ty, inst)]
355− | ((n, ty), (newArgs, inst)) <- typeClassArgs c2, let newHoles = map fst newArgs
356− , let (newClassArgs, newNonClassArgs) = partition (isTypeClassArg . snd) newArgs ]
357−