git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/src/Idris/TypeSearch.hs
552 lines 24 kB history raw
1{-|
2Module : Idris.TypeSearch
3Description : A Hoogle for Idris.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE ScopedTypeVariables #-}
10module Idris.TypeSearch (
11 searchByType
12 , searchPred
13 , defaultScoreFunction
14 ) where
16import Idris.AbsSyntax (addImpl, addUsingConstraints, getIState, implicit,
17 logLvl, putIState)
18import Idris.AbsSyntaxTree (IState(idris_docstrings, idris_interfaces, idris_outputmode, tt_ctxt),
19 Idris, InterfaceInfo, OutputMode(..), PTerm,
20 defaultSyntax, eqTy, implicitAllowed,
21 interface_implementations, toplevel)
22import Idris.Core.Evaluate (Context(definitions), Def(CaseOp, Function, TyDecl),
23 normaliseC)
24import Idris.Core.TT hiding (score)
25import Idris.Core.Unify (match_unify)
26import Idris.Delaborate (delabTy)
27import Idris.Docstrings (noDocs, overview)
28import Idris.Elab.Type (elabType)
29import Idris.IBC
30import Idris.Output (iPrintResult, iRenderError, iRenderOutput, iRenderResult,
31 iputStrLn, prettyDocumentedIst)
33import Util.Pretty (Doc, annotate, char, text, vsep, (<>))
35import Prelude hiding (pred)
37import Control.Applicative (Applicative(..), (<$>), (<*>), (<|>))
38import Control.Arrow (first, second, (&&&), (***))
39import Control.Monad (guard, when)
40import Data.List (find, partition, (\\))
41import Data.Map (Map)
42import qualified Data.Map as M
43import Data.Maybe (catMaybes, fromMaybe, isJust, mapMaybe, maybeToList)
44import Data.Monoid (Monoid(mappend, mempty))
45import Data.Ord (comparing)
46import qualified Data.PriorityQueue.FingerTree as Q
47import Data.Set (Set)
48import qualified Data.Set as S
49import qualified Data.Text as T (isPrefixOf, pack)
50import Data.Traversable (traverse)
52searchByType :: [String] -> PTerm -> Idris ()
53searchByType pkgs pterm = do
54 i <- getIState -- save original
55 when (not (null pkgs)) $
56 iputStrLn $ "Searching packages: " ++ showSep ", " pkgs
58 mapM_ loadPkgIndex pkgs
59 pterm' <- addUsingConstraints syn emptyFC pterm
60 pterm'' <- implicit toplevel syn name pterm'
61 let pterm''' = addImpl [] i pterm''
62 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name NoFC pterm'
63 let names = searchUsing searchPred i ty
64 let names' = take numLimit names
65 let docs =
66 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in
67 displayScore theScore <> char ' ' <> prettyDocumentedIst i docInfo
68 | (n, theScore) <- names']
69 if (not (null docs))
70 then case idris_outputmode i of
71 RawOutput _ -> do mapM_ iRenderOutput docs
72 iPrintResult ""
73 IdeMode _ _ -> iRenderResult (vsep docs)
74 else iRenderError $ text "No results found"
75 putIState i -- don't actually make any changes
76 where
77 numLimit = 50
78 syn = defaultSyntax { implicitAllowed = True } -- syntax
79 name = sMN 0 "searchType" -- name
81-- | Conduct a type-directed search using a given match predicate
82searchUsing :: (IState -> Type -> [(Name, Type)] -> [(Name, a)])
83 -> IState -> Type -> [(Name, a)]
84searchUsing pred istate ty = pred istate nty . concat . M.elems $
85 M.mapWithKey (\key -> M.toAscList . M.mapMaybe (f key)) (definitions ctxt)
86 where
87 nty = normaliseC ctxt [] ty
88 ctxt = tt_ctxt istate
89 f k x = do
90 guard $ not (special k)
91 type2 <- typeFromDef x
92 return $ normaliseC ctxt [] type2
93 special :: Name -> Bool
94 special (NS n _) = special n
95 special (SN _) = True
96 special (UN n) = T.pack "default#" `T.isPrefixOf` n
97 || n `elem` map T.pack ["believe_me", "really_believe_me"]
98 special _ = False
100-- | Our default search predicate.
101searchPred :: IState -> Type -> [(Name, Type)] -> [(Name, Score)]
102searchPred istate ty1 = matcher where
103 maxScore = 100
104 matcher = matchTypesBulk istate maxScore ty1
107typeFromDef :: (Def, r, i, b, c, d) -> Maybe Type
108typeFromDef (def, _, _, _, _, _) = get def where
109 get :: Def -> Maybe Type
110 get (Function ty _) = Just ty
111 get (TyDecl _ ty) = Just ty
112 -- get (Operator ty _ _) = Just ty
113 get (CaseOp _ ty _ _ _ _) = Just ty
114 get _ = Nothing
116-- Replace all occurences of `Delayed s t` with `t` in a type
117unLazy :: Type -> Type
118unLazy typ = case typ of
119 App _ (App _ (P _ lazy _) _) ty | lazy == sUN "Delayed" -> unLazy ty
120 Bind name binder ty -> Bind name (fmap unLazy binder) (unLazy ty)
121 App s t1 t2 -> App s (unLazy t1) (unLazy t2)
122 Proj ty i -> Proj (unLazy ty) i
123 _ -> typ
125-- | reverse the edges for a directed acyclic graph
126reverseDag :: Ord k => [((k, a), Set k)] -> [((k, a), Set k)]
127reverseDag xs = map f xs where
128 f ((k, v), _) = ((k, v), S.fromList . map (fst . fst) $ filter (S.member k . snd) xs)
130-- run vToP first!
131-- | Compute a directed acyclic graph corresponding to the
132-- arguments of a function.
133-- returns [(the name and type of the bound variable
134-- the names in the type of the bound variable)]
135computeDagP :: Ord n
136 => (TT n -> Bool) -- ^ filter to remove some arguments
137 -> TT n
138 -> ([((n, TT n), Set n)], [(n, TT n)], TT n)
139computeDagP removePred t = (reverse (map f arguments), reverse theRemovedArgs , retTy) where
140 f (n, ty) = ((n, ty), M.keysSet (usedVars ty))
142 (arguments, theRemovedArgs, retTy) = go [] [] t
144 -- NOTE : args are in reverse order
145 go args removedArgs (Bind n (Pi _ _ ty _) sc) = let arg = (n, ty) in
146 if removePred ty
147 then go args (arg : removedArgs) sc
148 else go (arg : args) removedArgs sc
149 go args removedArgs sc = (args, removedArgs, sc)
151-- | Collect the names and types of all the free variables
152-- The Boolean indicates those variables which are determined due to injectivity
153-- I have not given nearly enough thought to know whether this is correct
154usedVars :: Ord n => TT n -> Map n (TT n, Bool)
155usedVars = f True where
156 f b (P Bound n t) = M.singleton n (t, b) `M.union` f b t
157 f b (Bind n binder t2) = (M.delete n (f b t2) `M.union`) $ case binder of
158 Let t v -> f b t `M.union` f b v
159 Guess t v -> f b t `M.union` f b v
160 bind -> f b (binderTy bind)
161 f b (App _ t1 t2) = f b t1 `M.union` f (b && isInjective t1) t2
162 f b (Proj t _) = f b t
163 f _ (V _) = error "unexpected! run vToP first"
164 f _ _ = M.empty
166-- | Remove a node from a directed acyclic graph
167deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]
168deleteFromDag name [] = []
169deleteFromDag name (((name2, ty), (ix, set)) : xs) = (if name == name2
170 then id
171 else (((name2, ty) , (ix, S.delete name set)) :) ) (deleteFromDag name xs)
173deleteFromArgList :: Ord n => n -> [(n, TT n)] -> [(n, TT n)]
174deleteFromArgList n = filter ((/= n) . fst)
176-- | Asymmetric modifications to keep track of
177data AsymMods = Mods
178 { argApp :: !Int
179 , interfaceApp :: !Int
180 , interfaceIntro :: !Int
181 } deriving (Eq, Show)
184-- | Homogenous tuples
185data Sided a = Sided
186 { left :: !a
187 , right :: !a
188 } deriving (Eq, Show)
190sided :: (a -> a -> b) -> Sided a -> b
191sided f (Sided l r) = f l r
193-- | Could be a functor instance, but let's avoid name overloading
194both :: (a -> b) -> Sided a -> Sided b
195both f (Sided l r) = Sided (f l) (f r)
197-- | Keeps a record of the modifications made to match one type
198-- signature with another
199data Score = Score
200 { transposition :: !Int -- ^ transposition of arguments
201 , equalityFlips :: !Int -- ^ application of symmetry of equality
202 , asymMods :: !(Sided AsymMods) -- ^ "directional" modifications
203 } deriving (Eq, Show)
205displayScore :: Score -> Doc OutputAnnotation
206displayScore score = case both noMods (asymMods score) of
207 Sided True True -> annotated EQ "=" -- types are isomorphic
208 Sided True False -> annotated LT "<" -- found type is more general than searched type
209 Sided False True -> annotated GT ">" -- searched type is more general than found type
210 Sided False False -> text "_"
211 where
212 annotated ordr = annotate (AnnSearchResult ordr) . text
213 noMods (Mods app tcApp tcIntro) = app + tcApp + tcIntro == 0
215-- | This allows the search to stop expanding on a certain state if its
216-- score is already too high. Returns 'True' if the algorithm should keep
217-- exploring from this state, and 'False' otherwise.
218scoreCriterion :: Score -> Bool
219scoreCriterion (Score _ _ amods) = not
220 ( sided (&&) (both ((> 0) . argApp) amods)
221 || sided (+) (both argApp amods) > 4
222 || sided (||) (both (\(Mods _ tcApp tcIntro) -> tcApp > 3 || tcIntro > 3) amods)
223 )
225-- | Convert a 'Score' to an 'Int' to provide an order for search results.
226-- Lower scores are better.
227defaultScoreFunction :: Score -> Int
228defaultScoreFunction (Score trans eqFlip amods) =
229 trans + eqFlip + linearPenalty + upAndDowncastPenalty
230 where
231 -- prefer finding a more general type to a less general type
232 linearPenalty = (\(Sided l r) -> 3 * l + r)
233 (both (\(Mods app tcApp tcIntro) -> 3 * app + 4 * tcApp + 2 * tcIntro) amods)
234 -- it's very bad to have *both* upcasting and downcasting
235 upAndDowncastPenalty = 100 *
236 sided (*) (both (\(Mods app tcApp tcIntro) -> 2 * app + tcApp + tcIntro) amods)
238instance Ord Score where
239 compare = comparing defaultScoreFunction
242instance Monoid a => Monoid (Sided a) where
243 mempty = Sided mempty mempty
244 (Sided l1 r1) `mappend` (Sided l2 r2) = Sided (l1 `mappend` l2) (r1 `mappend` r2)
246instance Monoid AsymMods where
247 mempty = Mods 0 0 0
248 (Mods a b c) `mappend` (Mods a' b' c') = Mods (a + a') (b + b') (c + c')
250instance Monoid Score where
251 mempty = Score 0 0 mempty
252 (Score t e mods) `mappend` (Score t' e' mods') = Score (t + t') (e + e') (mods `mappend` mods')
254-- | A directed acyclic graph representing the arguments to a function
255-- The 'Int' represents the position of the argument (1st argument, 2nd, etc.)
256type ArgsDAG = [((Name, Type), (Int, Set Name))]
258-- | A list of interface constraints
259type Interfaces = [(Name, Type)]
261-- | The state corresponding to an attempted match of two types.
262data State = State
263 { holes :: ![(Name, Type)] -- ^ names which have yet to be resolved
264 , argsAndInterfaces :: !(Sided (ArgsDAG, Interfaces))
265 -- ^ arguments and interface constraints for each type which have yet to be resolved
266 , score :: !Score -- ^ the score so far
267 , usedNames :: ![Name] -- ^ all names that have been used
268 } deriving Show
270modifyTypes :: (Type -> Type) -> (ArgsDAG, Interfaces) -> (ArgsDAG, Interfaces)
271modifyTypes f = modifyDag *** modifyList
272 where
273 modifyDag = map (first (second f))
274 modifyList = map (second f)
276findNameInArgsDAG :: Name -> ArgsDAG -> Maybe (Type, Maybe Int)
277findNameInArgsDAG name = fmap ((snd . fst) &&& (Just . fst . snd)) . find ((name ==) . fst . fst)
279findName :: Name -> (ArgsDAG, Interfaces) -> Maybe (Type, Maybe Int)
280findName n (args, interfaces) = findNameInArgsDAG n args <|> ((,) <$> lookup n interfaces <*> Nothing)
282deleteName :: Name -> (ArgsDAG, Interfaces) -> (ArgsDAG, Interfaces)
283deleteName n (args, interfaces) = (deleteFromDag n args, filter ((/= n) . fst) interfaces)
285tcToMaybe :: TC a -> Maybe a
286tcToMaybe (OK x) = Just x
287tcToMaybe (Error _) = Nothing
289inArgTys :: (Type -> Type) -> ArgsDAG -> ArgsDAG
290inArgTys = map . first . second
293interfaceUnify :: Ctxt InterfaceInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]
294interfaceUnify interfaceInfo ctxt ty tyTry = do
295 res <- tcToMaybe $ match_unify ctxt [] (ty, Nothing) (retTy, Nothing) [] theHoles []
296 guard $ null (theHoles \\ map fst res)
297 let argTys' = map (second $ foldr (.) id [ subst n t | (n, t) <- res ]) tcArgs
298 return argTys'
299 where
300 tyTry' = vToP tyTry
301 theHoles = map fst nonTcArgs
302 retTy = getRetTy tyTry'
303 (tcArgs, nonTcArgs) = partition (isInterfaceArg interfaceInfo . snd) $ getArgTys tyTry'
305isInterfaceArg :: Ctxt InterfaceInfo -> Type -> Bool
306isInterfaceArg interfaceInfo ty = not (null (getInterfaceName clss >>= flip lookupCtxt interfaceInfo)) where
307 (clss, args) = unApply ty
308 getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName]
309 getInterfaceName _ = []
312-- | Compute the power set
313subsets :: [a] -> [[a]]
314subsets [] = [[]]
315subsets (x : xs) = let ss = subsets xs in map (x :) ss ++ ss
318-- not recursive (i.e., doesn't flip iterated identities) at the moment
319-- recalls the number of flips that have been made
320flipEqualities :: Type -> [(Int, Type)]
321flipEqualities t = case t of
322 eq1@(App _ (App _ (App _ (App _ eq@(P _ eqty _) tyL) tyR) valL) valR) | eqty == eqTy ->
323 [(0, eq1), (1, app (app (app (app eq tyR) tyL) valR) valL)]
324 Bind n binder sc -> (\bind' (j, sc') -> (fst (binderTy bind') + j, Bind n (fmap snd bind') sc'))
325 <$> traverse flipEqualities binder <*> flipEqualities sc
326 App _ f x -> (\(i, f') (j, x') -> (i + j, app f' x'))
327 <$> flipEqualities f <*> flipEqualities x
328 t' -> [(0, t')]
329 where app = App Complete
331--DONT run vToP first!
332-- | Try to match two types together in a unification-like procedure.
333-- Returns a list of types and their minimum scores, sorted in order
334-- of increasing score.
335matchTypesBulk :: forall info. IState -> Int -> Type -> [(info, Type)] -> [(info, Score)]
336matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues where
337 getStartQueues :: (info, Type) -> Maybe (Score, (info, Q.PQueue Score State))
338 getStartQueues nty@(info, type2) = case mapMaybe startStates ty2s of
339 [] -> Nothing
340 xs -> Just (minimum (map fst xs), (info, Q.fromList xs))
341 where
342 ty2s = (\(i, dag) (j, retTy) -> (i + j, dag, retTy))
343 <$> flipEqualitiesDag dag2 <*> flipEqualities retTy2
344 flipEqualitiesDag dag = case dag of
345 [] -> [(0, [])]
346 ((n, ty), (pos, deps)) : xs ->
347 (\(i, ty') (j, xs') -> (i + j , ((n, ty'), (pos, deps)) : xs'))
348 <$> flipEqualities ty <*> flipEqualitiesDag xs
349 startStates (numEqFlips, sndDag, sndRetTy) = do
350 state <- unifyQueue (State startingHoles
351 (Sided (dag1, interfaceArgs1) (sndDag, interfaceArgs2))
352 (mempty { equalityFlips = numEqFlips }) usedns) [(retTy1, sndRetTy)]
353 return (score state, state)
356 (dag2, interfaceArgs2, retTy2) = makeDag (uniqueBinders (map fst argNames1) type2)
357 argNames2 = map fst dag2
358 usedns = map fst startingHoles
359 startingHoles = argNames1 ++ argNames2
361 startingTypes = [(retTy1, retTy2)]
364 startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)
365 startQueueOfQueues = Q.fromList $ mapMaybe getStartQueues types
367 getAllResults :: Q.PQueue Score (info, Q.PQueue Score State) -> [(info, Score)]
368 getAllResults q = case Q.minViewWithKey q of
369 Nothing -> []
370 Just ((nextScore, (info, stateQ)), q') ->
371 if defaultScoreFunction nextScore <= maxScore
372 then case nextStepsQueue stateQ of
373 Nothing -> getAllResults q'
374 Just (Left stateQ') -> case Q.minViewWithKey stateQ' of
375 Nothing -> getAllResults q'
376 Just ((newQscore,_), _) -> getAllResults (Q.add newQscore (info, stateQ') q')
377 Just (Right theScore) -> (info, theScore) : getAllResults q'
378 else []
381 ctxt = tt_ctxt istate
382 interfaceInfo = idris_interfaces istate
384 (dag1, interfaceArgs1, retTy1) = makeDag type1
385 argNames1 = map fst dag1
386 makeDag :: Type -> (ArgsDAG, Interfaces, Type)
387 makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) .
388 computeDagP (isInterfaceArg interfaceInfo) . vToP . unLazy
389 first3 f (a,b,c) = (f a, b, c)
391 -- update our state with the unification resolutions
392 resolveUnis :: [(Name, Type)] -> State -> Maybe (State, [(Type, Type)])
393 resolveUnis [] state = Just (state, [])
394 resolveUnis ((name, term@(P Bound name2 _)) : xs)
395 state | isJust findArgs = do
396 ((ty1, ix1), (ty2, ix2)) <- findArgs
398 (state'', queue) <- resolveUnis xs state'
399 let transScore = fromMaybe 0 (abs <$> ((-) <$> ix1 <*> ix2))
400 return (inScore (\s -> s { transposition = transposition s + transScore }) state'', (ty1, ty2) : queue)
401 where
402 unresolved = argsAndInterfaces state
403 inScore f stat = stat { score = f (score stat) }
404 findArgs = ((,) <$> findName name (left unresolved) <*> findName name2 (right unresolved)) <|>
405 ((,) <$> findName name2 (left unresolved) <*> findName name (right unresolved))
406 matchnames = [name, name2]
407 deleteArgs = deleteName name . deleteName name2
408 state' = state { holes = filter (not . (`elem` matchnames) . fst) (holes state)
409 , argsAndInterfaces = both (modifyTypes (subst name term) . deleteArgs) unresolved}
411 resolveUnis ((name, term) : xs)
412 state@(State hs unresolved _ _) = case both (findName name) unresolved of
413 Sided Nothing Nothing -> Nothing
414 Sided (Just _) (Just _) -> error "Idris internal error: TypeSearch.resolveUnis"
415 oneOfEach -> first (addScore (both scoreFor oneOfEach)) <$> nextStep
416 where
417 scoreFor (Just _) = mempty { argApp = 1 }
418 scoreFor Nothing = mempty { argApp = otherApplied }
419 -- find variables which are determined uniquely by the type
420 -- due to injectivity
421 matchedVarMap = usedVars term
422 bothT f (x, y) = (f x, f y)
423 (injUsedVars, notInjUsedVars) = bothT M.keys . M.partition id . M.filterWithKey (\k _-> k `elem` map fst hs) $ M.map snd matchedVarMap
424 varsInTy = injUsedVars ++ notInjUsedVars
425 toDelete = name : varsInTy
426 deleteMany = foldr (.) id (map deleteName toDelete)
428 otherApplied = length notInjUsedVars
430 addScore additions theState = theState { score = let s = score theState in
431 s { asymMods = asymMods s `mappend` additions } }
432 state' = state { holes = filter (not . (`elem` toDelete) . fst) hs
433 , argsAndInterfaces = both (modifyTypes (subst name term) . deleteMany) (argsAndInterfaces state) }
434 nextStep = resolveUnis xs state'
437 -- | resolve a queue of unification constraints
438 unifyQueue :: State -> [(Type, Type)] -> Maybe State
439 unifyQueue state [] = return state
440 unifyQueue state ((ty1, ty2) : queue) = do
441 --trace ("go: \n" ++ show state) True `seq` return ()
442 res <- tcToMaybe $ match_unify ctxt [ (n, RigW, Pi RigW Nothing ty (TType (UVar [] 0))) | (n, ty) <- holes state]
443 (ty1, Nothing)
444 (ty2, Nothing) [] (map fst $ holes state) []
445 (state', queueAdditions) <- resolveUnis res state
446 guard $ scoreCriterion (score state')
447 unifyQueue state' (queue ++ queueAdditions)
449 possInterfaceImplementations :: [Name] -> Type -> [Type]
450 possInterfaceImplementations usedns ty = do
451 interfaceName <- getInterfaceName clss
452 interfaceDef <- lookupCtxt interfaceName interfaceInfo
453 n <- interface_implementations interfaceDef
454 def <- lookupCtxt (fst n) (definitions ctxt)
455 nty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])
456 let ty' = vToP (uniqueBinders usedns nty)
457 return ty'
458 where
459 (clss, _) = unApply ty
460 getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName]
461 getInterfaceName _ = []
463 -- 'Just' if the computation hasn't totally failed yet, 'Nothing' if it has
464 -- 'Left' if we haven't found a terminal state, 'Right' if we have
465 nextStepsQueue :: Q.PQueue Score State -> Maybe (Either (Q.PQueue Score State) Score)
466 nextStepsQueue queue = do
467 ((nextScore, next), rest) <- Q.minViewWithKey queue
468 Just $ if isFinal next
469 then Right nextScore
470 else let additions = if scoreCriterion nextScore
471 then Q.fromList [ (score state, state) | state <- nextSteps next ]
472 else Q.empty in
473 Left (Q.union rest additions)
474 where
475 isFinal (State [] (Sided ([], []) ([], [])) _ _) = True
476 isFinal _ = False
478 -- | Find all possible matches starting from a given state.
479 -- We go in stages rather than concatenating all three results in hopes of narrowing
480 -- the search tree. Once we advance in a phase, there should be no going back.
481 nextSteps :: State -> [State]
483 -- Stage 3 - match interfaces
484 nextSteps (State [] unresolved@(Sided ([], c1) ([], c2)) scoreAcc usedns) =
485 if null results3 then results4 else results3
486 where
487 -- try to match an interface argument from the left with an interface argument from the right
488 results3 =
489 catMaybes [ unifyQueue (State []
490 (Sided ([], deleteFromArgList n1 c1)
491 ([], map (second subst2for1) (deleteFromArgList n2 c2)))
492 scoreAcc usedns) [(ty1, ty2)]
493 | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]
495 -- try to hunt match an interface constraint by replacing it with an implementation
496 results4 = [ State [] (both (\(cs, _, _) -> ([], cs)) sds)
497 (scoreAcc `mappend` Score 0 0 (both (\(_, amods, _) -> amods) sds))
498 (usedns ++ sided (++) (both (\(_, _, hs) -> hs) sds))
499 | sds <- allMods ]
500 where
501 allMods = parallel defMod mods
502 mods :: Sided [( Interfaces, AsymMods, [Name] )]
503 mods = both (implementationMods . snd) unresolved
504 defMod :: Sided (Interfaces, AsymMods, [Name])
505 defMod = both (\(_, cs) -> (cs, mempty , [])) unresolved
506 parallel :: Sided a -> Sided [a] -> [Sided a]
507 parallel (Sided l r) (Sided ls rs) = map (flip Sided r) ls ++ map (Sided l) rs
508 implementationMods :: Interfaces -> [( Interfaces , AsymMods, [Name] )]
509 implementationMods interfaces = [ ( newInterfaceArgs, mempty { interfaceApp = 1 }, newHoles )
510 | (_, ty) <- interfaces
511 , impl <- possInterfaceImplementations usedns ty
512 , newInterfaceArgs <- maybeToList $ interfaceUnify interfaceInfo ctxt ty impl
513 , let newHoles = map fst newInterfaceArgs ]
516 -- Stage 1 - match arguments
517 nextSteps (State hs (Sided (dagL, c1) (dagR, c2)) scoreAcc usedns) = results where
519 results = concatMap takeSomeInterfaces results1
521 -- we only try to match arguments whose names don't appear in the types
522 -- of any other arguments
523 canBeFirst :: ArgsDAG -> [(Name, Type)]
524 canBeFirst = map fst . filter (S.null . snd . snd)
526 -- try to match an argument from the left with an argument from the right
527 results1 = catMaybes [ unifyQueue (State (filter (not . (`elem` [n1,n2]) . fst) hs)
528 (Sided (deleteFromDag n1 dagL, c1)
529 (inArgTys subst2for1 $ deleteFromDag n2 dagR, map (second subst2for1) c2))
530 scoreAcc usedns) [(ty1, ty2)]
531 | (n1, ty1) <- canBeFirst dagL, (n2, ty2) <- canBeFirst dagR
532 , let subst2for1 = psubst n2 (P Bound n1 ty1)]
536 -- Stage 2 - simply introduce a subset of the interfaces
537 -- we've finished, so take some interfaces
538 takeSomeInterfaces (State [] unresolved@(Sided ([], _) ([], _)) scoreAcc usedns) =
539 map statesFromMods . prod $ both (interfaceMods . snd) unresolved
540 where
541 swap (Sided l r) = Sided r l
542 statesFromMods :: Sided (Interfaces, AsymMods) -> State
543 statesFromMods sides = let interfaces = both (\(c, _) -> ([], c)) sides
544 mods = swap (both snd sides) in
545 State [] interfaces (scoreAcc `mappend` (mempty { asymMods = mods })) usedns
546 interfaceMods :: Interfaces -> [(Interfaces, AsymMods)]
547 interfaceMods cs = let lcs = length cs in
548 [ (cs', mempty { interfaceIntro = lcs - length cs' }) | cs' <- subsets cs ]
549 prod :: Sided [a] -> [Sided a]
550 prod (Sided ls rs) = [Sided l r | l <- ls, r <- rs]
551 -- still have arguments to match, so just be the identity
552 takeSomeInterfaces s = [s]