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