@@ -39,17 +39,15 @@ import Util.Pretty (text, char, vsep, (<>), Doc, annotate)
40searchByType :: [String] -> PTerm -> Idris ()
40searchByType :: [String] -> PTerm -> Idris ()
41searchByType pkgs pterm = do
41searchByType pkgs pterm = do
42− orig <- getIState -- save original
42+ i <- getIState -- save original
43 when (not (null pkgs)) $
43 when (not (null pkgs)) $
44 iputStrLn $ "Searching packages: " ++ showSep ", " pkgs
44 iputStrLn $ "Searching packages: " ++ showSep ", " pkgs
46 mapM_ loadPkgIndex pkgs
46 mapM_ loadPkgIndex pkgs
47 pterm' <- addUsingConstraints syn emptyFC pterm
47 pterm' <- addUsingConstraints syn emptyFC pterm
48 pterm'' <- implicit toplevel syn name pterm'
48 pterm'' <- implicit toplevel syn name pterm'
50 let pterm''' = addImpl i pterm''
49 let pterm''' = addImpl i pterm''
51 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'
50 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'
52− putIState i -- don't actually make any changes
53 let names = searchUsing searchPred i ty
51 let names = searchUsing searchPred i ty
54 let names' = take numLimit names
52 let names' = take numLimit names
55 let docs =
53 let docs =
@@ -60,7 +58,7 @@ searchByType pkgs pterm = do
60 RawOutput _ -> do mapM_ iRenderOutput docs
58 RawOutput _ -> do mapM_ iRenderOutput docs
61 iPrintResult ""
59 iPrintResult ""
62 IdeSlave _ _ -> iRenderResult (vsep docs)
60 IdeSlave _ _ -> iRenderResult (vsep docs)
63− putIState orig
61+ putIState i -- don't actually make any changes
65 numLimit = 50
63 numLimit = 50
66 syn = defaultSyntax { implicitAllowed = True } -- syntax
64 syn = defaultSyntax { implicitAllowed = True } -- syntax
@@ -85,7 +83,7 @@ searchUsing pred istate ty = pred istate nty . concat . M.elems $
85 || n `elem` map T.pack ["believe_me", "really_believe_me"]
83 || n `elem` map T.pack ["believe_me", "really_believe_me"]
86 special _ = False
84 special _ = False
88−-- Our default search predicate.
86+-- | Our default search predicate.
89searchPred :: IState -> Type -> [(Name, Type)] -> [(Name, Score)]
87searchPred :: IState -> Type -> [(Name, Type)] -> [(Name, Score)]
90searchPred istate ty1 = matcher where
88searchPred istate ty1 = matcher where
91 maxScore = 100
89 maxScore = 100
@@ -174,10 +172,12 @@ sided f (Sided l r) = f l r
174both :: (a -> b) -> Sided a -> Sided b
172both :: (a -> b) -> Sided a -> Sided b
175both f (Sided l r) = Sided (f l) (f r)
173both f (Sided l r) = Sided (f l) (f r)
175+-- | Keeps a record of the modifications made to match one type
176+-- signature with another
177data Score = Score
177data Score = Score
178− { transposition :: !Int
178+ { transposition :: !Int -- ^ transposition of arguments
179− , equalityFlips :: !Int
179+ , equalityFlips :: !Int -- ^ application of symmetry of equality
180− , asymMods :: !(Sided AsymMods)
180+ , asymMods :: !(Sided AsymMods) -- ^ "directional" modifications
181 } deriving (Eq, Show)
181 } deriving (Eq, Show)
183displayScore :: Score -> Doc OutputAnnotation
183displayScore :: Score -> Doc OutputAnnotation
@@ -190,6 +190,9 @@ displayScore score = case both noMods (asymMods score) of
190 annotated ordr = annotate (AnnSearchResult ordr) . text
190 annotated ordr = annotate (AnnSearchResult ordr) . text
191 noMods (Mods app tcApp tcIntro) = app + tcApp + tcIntro == 0
191 noMods (Mods app tcApp tcIntro) = app + tcApp + tcIntro == 0
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.
193scoreCriterion :: Score -> Bool
196scoreCriterion :: Score -> Bool
194scoreCriterion (Score _ _ amods) = not
197scoreCriterion (Score _ _ amods) = not
195 ( sided (&&) (both ((> 0) . argApp) amods)
198 ( sided (&&) (both ((> 0) . argApp) amods)
@@ -197,6 +200,8 @@ scoreCriterion (Score _ _ amods) = not
197 || sided (||) (both (\(Mods _ tcApp tcIntro) -> tcApp > 3 || tcIntro > 3) amods)
200 || sided (||) (both (\(Mods _ tcApp tcIntro) -> tcApp > 3 || tcIntro > 3) amods)
203+-- | Convert a 'Score' to an 'Int' to provide an order for search results.
204+-- Lower scores are better.
200defaultScoreFunction :: Score -> Int
205defaultScoreFunction :: Score -> Int
201defaultScoreFunction (Score trans eqFlip amods) =
206defaultScoreFunction (Score trans eqFlip amods) =
202 trans + eqFlip + linearPenalty + upAndDowncastPenalty
207 trans + eqFlip + linearPenalty + upAndDowncastPenalty
@@ -208,6 +213,10 @@ defaultScoreFunction (Score trans eqFlip amods) =
208 upAndDowncastPenalty = 100 *
213 upAndDowncastPenalty = 100 *
209 sided (*) (both (\(Mods app tcApp tcIntro) -> 2 * app + tcApp + tcIntro) amods)
214 sided (*) (both (\(Mods app tcApp tcIntro) -> 2 * app + tcApp + tcIntro) amods)
216+instance Ord Score where
217+ compare = comparing defaultScoreFunction
211instance Monoid a => Monoid (Sided a) where
220instance Monoid a => Monoid (Sided a) where
212 mempty = Sided mempty mempty
221 mempty = Sided mempty mempty
213 (Sided l1 r1) `mappend` (Sided l2 r2) = Sided (l1 `mappend` l2) (r1 `mappend` r2)
222 (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
278 getClassName _ = []
287 getClassName _ = []
281−instance Ord Score where
282− compare = comparing defaultScoreFunction
284-- | Compute the power set
290-- | Compute the power set
285subsets :: [a] -> [[a]]
291subsets :: [a] -> [[a]]
286subsets [] = [[]]
292subsets [] = [[]]
@@ -429,17 +435,17 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
429 getClassName (P (TCon _ _) className _) = [className]
435 getClassName (P (TCon _ _) className _) = [className]
430 getClassName _ = []
436 getClassName _ = []
432− -- Just if the computation hasn't totally failed yet, Nothing if it has
438+ -- '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
439+ -- 'Left' if we haven't found a terminal state, 'Right' if we have
434 nextStepsQueue :: Q.PQueue Score State -> Maybe (Either (Q.PQueue Score State) Score)
440 nextStepsQueue :: Q.PQueue Score State -> Maybe (Either (Q.PQueue Score State) Score)
435 nextStepsQueue queue = do
441 nextStepsQueue queue = do
436 ((nextScore, next), rest) <- Q.minViewWithKey queue
442 ((nextScore, next), rest) <- Q.minViewWithKey queue
437− if isFinal next
443+ Just $ if isFinal next
438− then Just $ Right nextScore
444+ then Right nextScore
439 else let additions = if scoreCriterion nextScore
445 else let additions = if scoreCriterion nextScore
440 then Q.fromList [ (score state, state) | state <- nextSteps next ]
446 then Q.fromList [ (score state, state) | state <- nextSteps next ]
441 else Q.empty in
447 else Q.empty in
442− Just $ Left (Q.union rest additions)
448+ Left (Q.union rest additions)
444 isFinal (State [] (Sided ([], []) ([], [])) _ _) = True
450 isFinal (State [] (Sided ([], []) ([], [])) _ _) = True
445 isFinal _ = False
451 isFinal _ = False