@@ -39,17 +39,15 @@ import Util.Pretty (text, char, vsep, (<>), Doc, annotate)
3939
4040searchByType :: [String] -> PTerm -> Idris ()
4141searchByType pkgs pterm = do
42− orig <- getIState -- save original
42+ i <- getIState -- save original
4343 when (not (null pkgs)) $
4444 iputStrLn $ "Searching packages: " ++ showSep ", " pkgs
4545
4646 mapM_ loadPkgIndex pkgs
4747 pterm' <- addUsingConstraints syn emptyFC pterm
4848 pterm'' <- implicit toplevel syn name pterm'
49− i <- getIState
5049 let pterm''' = addImpl i pterm''
5150 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'
52− putIState i -- don't actually make any changes
5351 let names = searchUsing searchPred i ty
5452 let names' = take numLimit names
5553 let docs =
@@ -60,7 +58,7 @@ searchByType pkgs pterm = do
6058 RawOutput _ -> do mapM_ iRenderOutput docs
6159 iPrintResult ""
6260 IdeSlave _ _ -> iRenderResult (vsep docs)
63− putIState orig
61+ putIState i -- don't actually make any changes
6462 where
6563 numLimit = 50
6664 syn = defaultSyntax { implicitAllowed = True } -- syntax
@@ -85,7 +83,7 @@ searchUsing pred istate ty = pred istate nty . concat . M.elems $
8583 || n `elem` map T.pack ["believe_me", "really_believe_me"]
8684 special _ = False
8785
88−-- Our default search predicate.
86+-- | Our default search predicate.
8987searchPred :: IState -> Type -> [(Name, Type)] -> [(Name, Score)]
9088searchPred istate ty1 = matcher where
9189 maxScore = 100
@@ -174,10 +172,12 @@ sided f (Sided l r) = f l r
174172both :: (a -> b) -> Sided a -> Sided b
175173both f (Sided l r) = Sided (f l) (f r)
176174
175+-- | Keeps a record of the modifications made to match one type
176+-- signature with another
177177data Score = Score
178− { transposition :: !Int
179− , equalityFlips :: !Int
180− , asymMods :: !(Sided AsymMods)
178+ { transposition :: !Int -- ^ transposition of arguments
179+ , equalityFlips :: !Int -- ^ application of symmetry of equality
180+ , asymMods :: !(Sided AsymMods) -- ^ "directional" modifications
181181 } deriving (Eq, Show)
182182
183183displayScore :: Score -> Doc OutputAnnotation
@@ -190,6 +190,9 @@ displayScore score = case both noMods (asymMods score) of
190190 annotated ordr = annotate (AnnSearchResult ordr) . text
191191 noMods (Mods app tcApp tcIntro) = app + tcApp + tcIntro == 0
192192
193+-- | This allows the search to stop expanding on a certain state if its
194+-- score is already too high. Returns 'True' if the algorithm should keep
195+-- exploring from this state, and 'False' otherwise.
193196scoreCriterion :: Score -> Bool
194197scoreCriterion (Score _ _ amods) = not
195198 ( sided (&&) (both ((> 0) . argApp) amods)
@@ -197,6 +200,8 @@ scoreCriterion (Score _ _ amods) = not
197200 || sided (||) (both (\(Mods _ tcApp tcIntro) -> tcApp > 3 || tcIntro > 3) amods)
198201 )
199202
203+-- | Convert a 'Score' to an 'Int' to provide an order for search results.
204+-- Lower scores are better.
200205defaultScoreFunction :: Score -> Int
201206defaultScoreFunction (Score trans eqFlip amods) =
202207 trans + eqFlip + linearPenalty + upAndDowncastPenalty
@@ -208,6 +213,10 @@ defaultScoreFunction (Score trans eqFlip amods) =
208213 upAndDowncastPenalty = 100 *
209214 sided (*) (both (\(Mods app tcApp tcIntro) -> 2 * app + tcApp + tcIntro) amods)
210215
216+instance Ord Score where
217+ compare = comparing defaultScoreFunction
218+
219+
211220instance Monoid a => Monoid (Sided a) where
212221 mempty = Sided mempty mempty
213222 (Sided l1 r1) `mappend` (Sided l2 r2) = Sided (l1 `mappend` l2) (r1 `mappend` r2)
@@ -278,9 +287,6 @@ isTypeClassArg classInfo ty = not (null (getClassName clss >>= flip lookupCtxt c
278287 getClassName _ = []
279288
280289
281−instance Ord Score where
282− compare = comparing defaultScoreFunction
283−
284290-- | Compute the power set
285291subsets :: [a] -> [[a]]
286292subsets [] = [[]]
@@ -429,17 +435,17 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
429435 getClassName (P (TCon _ _) className _) = [className]
430436 getClassName _ = []
431437
432− -- Just if the computation hasn't totally failed yet, Nothing if it has
433− -- Left if we haven't found a terminal state, Right if we have
438+ -- 'Just' if the computation hasn't totally failed yet, 'Nothing' if it has
439+ -- 'Left' if we haven't found a terminal state, 'Right' if we have
434440 nextStepsQueue :: Q.PQueue Score State -> Maybe (Either (Q.PQueue Score State) Score)
435441 nextStepsQueue queue = do
436442 ((nextScore, next), rest) <- Q.minViewWithKey queue
437− if isFinal next
438− then Just $ Right nextScore
443+ Just $ if isFinal next
444+ then Right nextScore
439445 else let additions = if scoreCriterion nextScore
440446 then Q.fromList [ (score state, state) | state <- nextSteps next ]
441447 else Q.empty in
442− Just $ Left (Q.union rest additions)
448+ Left (Q.union rest additions)
443449 where
444450 isFinal (State [] (Sided ([], []) ([], [])) _ _) = True
445451 isFinal _ = False