@@ -10,14 +10,15 @@ 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))
15+import qualified Data.PriorityQueue.FingerTree as Q
1516import Data.Set (Set)
1617import qualified Data.Set as S
1718import qualified Data.Text as T (pack, isPrefixOf)
1819
1920import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)
20−import Idris.AbsSyntaxTree (class_instances, defaultSyntax, Idris,
21+import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, Idris,
2122 IState (idris_classes, idris_docstrings, tt_ctxt),
2223 implicitAllowed, prettyDocumentedIst, prettyIst, PTerm, toplevel)
2324import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
@@ -41,7 +42,7 @@ searchByType h pterm = do
4142 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'
4243 putIState i -- don't actually make any changes
4344 let names = searchUsing searchPred i ty
44− let names' = take numLimit . takeWhile ((< scoreLimit) . getScore) $
45+ let names' = take numLimit $
4546 sortBy (compare `on` getScore) names
4647 let docs =
4748 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in
@@ -51,7 +52,6 @@ searchByType h pterm = do
5152 where
5253 getScore = defaultScoreFunction . snd . snd
5354 numLimit = 50
54− scoreLimit = 100
5555 syn = defaultSyntax { implicitAllowed = True } -- syntax
5656 n = sMN 0 "searchType" -- name
5757
@@ -84,10 +84,9 @@ searchUsing pred istate ty =
8484
8585-- Our default search predicate.
8686searchPred :: IState -> Type -> Type -> Maybe Score
87−searchPred istate ty1 = \ty2 -> case matcher ty2 of
88− xs -> guard (not (null xs)) >> return (minimumBy (compare `on` defaultScoreFunction) xs)
89− where
90− matcher = unifyWithHoles istate ty1
87+searchPred istate ty1 = matcher where
88+ maxScore = 100
89+ matcher = unifyWithHoles istate maxScore ty1
9190
9291
9392typeFromDef :: (Def, b, c, d) -> Maybe Type
@@ -218,36 +217,53 @@ inArgTys :: (Type -> Type) -> ArgsDAG -> ArgsDAG
218217inArgTys = map . first . second
219218
220219
220+typeclassUnify :: Ctxt ClassInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]
221+typeclassUnify classInfo ctxt ty tyTry = do
222+ res <- tcToMaybe $ match_unify ctxt [] ty retTy [] holes []
223+ guard $ null (holes \\ map fst res)
224+ let argTys' = map (second $ foldr (.) id [ subst n t | (n, t) <- res ]) tcArgs
225+ return argTys'
226+ where
227+ tyTry' = vToP tyTry
228+ holes = map fst nonTcArgs
229+ retTy = getRetTy tyTry'
230+ (tcArgs, nonTcArgs) = partition (isTypeClassArg classInfo . snd) $ getArgTys tyTry'
231+
232+isTypeClassArg :: Ctxt ClassInfo -> Type -> Bool
233+isTypeClassArg classInfo ty = not (null (getClassName clss >>= flip lookupCtxt classInfo)) where
234+ (clss, args) = unApply ty
235+ getClassName (P (TCon _ _) className _) = [className]
236+ getClassName _ = []
237+
238+
239+instance Ord Score where
240+ compare = compare `on` defaultScoreFunction
241+
221242--DONT run vToP first!
222243-- | Try to match two types together in a unification-like procedure.
223244-- Returns a list of possible scores representing ways in which the two
224245-- types can be matched.
225−unifyWithHoles :: IState -> Type -> Type -> [Score]
226−unifyWithHoles istate type1 = \type2 -> let
246+unifyWithHoles :: IState -> Int -> Type -> Type -> Maybe Score
247+unifyWithHoles istate maxScore type1 = \type2 -> let
227248 (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders argNames1 type2)
228249 argNames2 = map (fst . fst) dag2
229250 startingHoles = argNames1 ++ argNames2
230251
231252 startingTypes = (retTy1, retTy2) : []
232− in case unifyQueue (State startingHoles dag1 dag2
253+ in do
254+ state <- unifyQueue (State startingHoles dag1 dag2
233255 typeClassArgs1 typeClassArgs2
234256 mempty startingHoles) startingTypes
235− of Nothing -> []
236− Just state -> possibleMatches state
257+ getResults (Q.singleton (score state) state)
237258 where
238259 ctxt = tt_ctxt istate
239260 classInfo = idris_classes istate
240261
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−
247262 (dag1, typeClassArgs1, retTy1) = makeDag type1
248263 argNames1 = map (fst . fst) dag1
249264 makeDag :: Type -> (ArgsDAG, [(Name, Type)], Type)
250− makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) . computeDagP isTypeClassArg . vToP
265+ makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) .
266+ computeDagP (isTypeClassArg classInfo) . vToP
251267 first3 f (a,b,c) = (f a, b, c)
252268
253269 -- update our state with the unification resolutions
@@ -278,9 +294,13 @@ unifyWithHoles istate type1 = \type2 -> let
278294 (Nothing, Nothing) -> nextStep
279295 _ -> error ("Shouldn't happen. Watch the alpha conversion!\n" ++ show args1 ++ "\n\n" ++ show args2)
280296 where
297+ varsInTy = map fst $ M.toList (usedVars term) --[]
298+ toDelete = name : varsInTy
299+ deleteMany = foldr (.) id $ [ deleteLeft t . deleteRight t | t <- toDelete ]
300+
281301 inScore f state = state { score = f (score state) }
282− state' = modifyTypes (subst name term) . deleteLeft name . deleteRight name $
283− state { holes = holes \\ [name]}
302+ state' = modifyTypes (subst name term) . deleteMany $
303+ state { holes = holes \\ toDelete }
284304 nextStep = resolveUnis xs state'
285305
286306
@@ -288,12 +308,13 @@ unifyWithHoles istate type1 = \type2 -> let
288308 unifyQueue :: State -> [(Type, Type)] -> Maybe State
289309 unifyQueue state [] = return state
290310 unifyQueue state ((ty1, ty2) : queue) = do
311+ --trace ("go: \n" ++ show state) True `seq` return ()
291312 res <- tcToMaybe $ match_unify ctxt [] ty1 ty2 [] (holes state) []
292313 (state', queueAdditions) <- resolveUnis res state
293314 guard $ scoreCriterion (score state')
294315 unifyQueue state' (queue ++ queueAdditions)
295316
296− possClassInstances :: [Name] -> Type -> [([(Name, Type)], Type)]
317+ possClassInstances :: [Name] -> Type -> [Type]
297318 possClassInstances usedNames ty = do
298319 className <- getClassName clss
299320 classDef <- lookupCtxt className classInfo
@@ -301,57 +322,70 @@ unifyWithHoles istate type1 = \type2 -> let
301322 def <- lookupCtxt n (definitions ctxt)
302323 ty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])
303324 let ty' = vToP (uniqueBinders usedNames ty)
304− return (getArgTys ty', getRetTy ty')
325+ return ty'
305326 where
306− (clss, args) = unApply ty
327+ (clss, _) = unApply ty
307328 getClassName (P (TCon _ _) className _) = [className]
308329 getClassName _ = []
309330
331+
332+ getResults :: Q.PQueue Score State -> Maybe Score
333+ getResults queue = do
334+ ((nextScore, next), rest) <- Q.minViewWithKey queue
335+ if isFinal next
336+ then return nextScore
337+ else do
338+ guard (defaultScoreFunction nextScore <= maxScore)
339+ let additions = if scoreCriterion nextScore
340+ then Q.fromList [ (score state, state) | state <- nextSteps next ]
341+ else Q.empty
342+ getResults (Q.union rest additions)
343+ where
344+ isFinal (State [] [] [] [] [] score _) = True
345+ isFinal _ = False
346+
310347 -- | Find all possible matches starting from a given state.
311− possibleMatches :: State -> [Score]
312− possibleMatches (State [] [] [] [] [] scoreAcc _) = [scoreAcc]
313− possibleMatches (State holes dag1 dag2 c1 c2 scoreAcc usedNames) =
314− concat [ possibleMatches state | state <- results, scoreCriterion (score state) ] where
348+ -- We go in stages rather than concatenating all three results in hopes of narrowing
349+ -- the search tree. Once we advance in a phase, there should be no going back.
350+ nextSteps :: State -> [State]
351+
352+ -- Stage 2 - match typeclasses
353+ nextSteps (State [] [] [] c1 c2 scoreAcc usedNames) =
354+ if null results2 then results3 else results2
355+ where
356+ -- try to match a typeclass argument from the left with a typeclass argument from the right
357+ results2 =
358+ catMaybes [ unifyQueue (State [] [] []
359+ (deleteFromArgList n1 c1) (map (second subst2for1) (deleteFromArgList n2 c2)) scoreAcc usedNames) [(ty1, ty2)]
360+ | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]
361+
362+ -- try to hunt match a typeclass constraint by replacing it with an instance
363+ results3 = results3A ++ results3B
364+ typeClassArgs classes = [ ((n, ty), inst) | (n, ty) <- classes, inst <- possClassInstances usedNames ty ]
365+ results3A = [ State [] [] []
366+ (deleteFromArgList n c1 ++ newClassArgs) c2
367+ (scoreAcc `mappend` (mempty { leftTypeClass = 1 }))
368+ (usedNames ++ newHoles)
369+ | ((n, ty), inst) <- typeClassArgs c1
370+ , newClassArgs <- maybeToList $ typeclassUnify classInfo ctxt ty inst
371+ , let newHoles = map fst newClassArgs ]
372+ results3B = [ State [] [] []
373+ c1 (deleteFromArgList n c2 ++ newClassArgs)
374+ (scoreAcc `mappend` (mempty { rightTypeClass = 1 }))
375+ (usedNames ++ newHoles)
376+ | ((n, ty), inst) <- typeClassArgs c2
377+ , newClassArgs <- maybeToList $ typeclassUnify classInfo ctxt ty inst
378+ , let newHoles = map fst newClassArgs ]
379+
380+ -- Stage 1 - match arguments
381+ nextSteps (State holes dag1 dag2 c1 c2 scoreAcc usedNames) = results1 where
315382
316383 -- we only try to match arguments whose names don't appear in the types
317384 -- of any other arguments
318385 canBeFirst :: ArgsDAG -> [(Name, Type)]
319386 canBeFirst = map fst . filter (S.null . snd . snd)
320387
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−
325388 -- try to match an argument from the left with an argument from the right
326389 results1 = catMaybes [ unifyQueue (State (holes \\ [n1, n2]) (deleteFromDag n1 dag1)
327390 ((inArgTys subst2for1) $ deleteFromDag n2 dag2) c1 (map (second subst2for1) c2) scoreAcc usedNames) [(ty1, ty2)]
328391 | (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−