119956a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1271 from bmsherman/typeSearch

119956aEdwin Brady12 years ago

src/Idris/AbsSyntaxTree.hs+5

compare with master

unifiedsplit

@@ -1421,6 +1421,11 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1421 getFixity :: String -> Maybe Fixity

1422 getFixity = flip M.lookup fixities

1423

1424+prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation

1425+prettyDocumentedIst ist (name, ty, docs) =

1426+ prettyName True [] name <+> colon <+> align (prettyIst ist ty) <$>

1427+ fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

1428+

1424-- | Pretty-printer helper for the binding site of a name

1429-- | Pretty-printer helper for the binding site of a name

1425bindingOf :: Name -- ^^ the bound name

1430bindingOf :: Name -- ^^ the bound name

1426 -> Bool -- ^^ whether the name is implicit

1431 -> Bool -- ^^ whether the name is implicit

src/Idris/Help.hs+1

@@ -33,6 +33,7 @@ help =

33 ([":doc"], NameArg, "Show internal documentation"),

34 ([":mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"),

35 ([":apropos"], NoArg, "Search names, types, and documentation"),

36+ ([":search", ":s"], ExprArg, "Search for values by type"),

36 ([":whocalls", ":wc"], NameArg, "List the callers of some name"),

37 ([":whocalls", ":wc"], NameArg, "List the callers of some name"),

37 ([":callswho", ":cw"], NameArg, "List the callees of some name"),

38 ([":callswho", ":cw"], NameArg, "List the callees of some name"),

38 ([":total"], NameArg, "Check the totality of a name"),

39 ([":total"], NameArg, "Check the totality of a name"),

src/Idris/Output.hs+56−56

@@ -16,6 +16,7 @@ import Debug.Trace

16import System.IO (stdout, Handle, hPutStrLn)

18import Data.List (nub)

19+import Data.Maybe (fromMaybe)

20pshow :: IState -> Err -> String

21pshow :: IState -> Err -> String

21pshow ist err = displayDecorated (consoleDecorate ist) .

22pshow ist err = displayDecorated (consoleDecorate ist) .

@@ -53,16 +54,6 @@ iRender d = do w <- getWidth

53 | otherwise -> do width <- runIO getScreenWidth

54 | otherwise -> do width <- runIO getScreenWidth

54 return $ renderPretty 0.8 width d

55 return $ renderPretty 0.8 width d

56−ihPrintResult :: Handle -> String -> Idris ()

57−ihPrintResult h s = do i <- getIState

58− case idris_outputmode i of

59− RawOutput -> case s of

60− "" -> return ()

61− s -> runIO $ hPutStrLn h s

62− IdeSlave n ->

63− let good = SexpList [SymbolAtom "ok", toSExp s] in

64− runIO $ hPutStrLn h $ convSExp "return" good n

65−

66-- | Write a pretty-printed term to the console with semantic coloring

57-- | Write a pretty-printed term to the console with semantic coloring

67consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

58consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

68consoleDisplayAnnotated h output = do ist <- getIState

59consoleDisplayAnnotated h output = do ist <- getIState

@@ -71,23 +62,8 @@ consoleDisplayAnnotated h output = do ist <- getIState

71 displayDecorated (consoleDecorate ist) $

62 displayDecorated (consoleDecorate ist) $

72 rendered

63 rendered

74−

75−-- | Write pretty-printed output to IDESlave with semantic annotations

76−ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

77−ideSlaveReturnAnnotated n h out = do ist <- getIState

78− (str, spans) <- fmap displaySpans .

79− iRender .

80− fmap (fancifyAnnots ist) $

81− out

82− let good = [SymbolAtom "ok", toSExp str, toSExp spans]

83− runIO . hPutStrLn h $ convSExp "return" good n

84−

85ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

65ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

86−ihPrintTermWithType h tm ty = do ist <- getIState

66+ihPrintTermWithType h tm ty = ihRenderResult h (tm <+> colon <+> align ty)

87− let output = tm <+> colon <+> align ty

88− case idris_outputmode ist of

89− RawOutput -> consoleDisplayAnnotated h output

90− IdeSlave n -> ideSlaveReturnAnnotated n h output

92-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

68-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

93ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

69ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

@@ -96,9 +72,7 @@ ihPrintFunTypes h bnd n overloads = do ist <- getIState

96 let ppo = ppOptionIst ist

72 let ppo = ppOptionIst ist

97 let infixes = idris_infixes ist

73 let infixes = idris_infixes ist

98 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

74 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

99− case idris_outputmode ist of

75+ ihRenderResult h output

100− RawOutput -> consoleDisplayAnnotated h output

101− IdeSlave n -> ideSlaveReturnAnnotated n h output

102 where fullName n = prettyName True bnd n

76 where fullName n = prettyName True bnd n

103 ppOverload ppo infixes n tm =

77 ppOverload ppo infixes n tm =

104 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

78 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

@@ -109,18 +83,20 @@ ihRenderResult h d = do ist <- getIState

109 RawOutput -> consoleDisplayAnnotated h d

83 RawOutput -> consoleDisplayAnnotated h d

110 IdeSlave n -> ideSlaveReturnAnnotated n h d

84 IdeSlave n -> ideSlaveReturnAnnotated n h d

111

112−fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

86+makeAnnName :: IState -> Name -> Maybe OutputAnnotation

113−fancifyAnnots ist annot@(AnnName n _ _ _) =

87+makeAnnName ist n

114− do let ctxt = tt_ctxt ist

115− docs = docOverview ist n

116− ty = Just (getTy ist n)

117− case () of

118− _ | isDConName n ctxt -> AnnName n (Just DataOutput) docs ty

88+ | isDConName n ctxt = annName DataOutput

119− _ | isFnName n ctxt -> AnnName n (Just FunOutput) docs ty

89+ | isFnName n ctxt = annName FunOutput

120− _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty

90+ | isTConName n ctxt = annName TypeOutput

121− _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty

91+ | isMetavarName n ist = annName MetavarOutput

122− _ | otherwise -> annot

92+ | otherwise = Nothing

93+ where ctxt = tt_ctxt ist

94+ docs = docOverview ist n

95+ ty = Just (getTy ist n)

96+

97+ annName :: NameOutput -> Maybe OutputAnnotation

98+ annName nameType = Just (AnnName n (Just nameType) docs ty)

123− where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

99+ docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

124 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

100 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

125 let o = overview (fst docs)

101 let o = overview (fst docs)

126 -- TODO make width configurable

102 -- TODO make width configurable

@@ -130,30 +106,54 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

130 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

106 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

131 delabTy ist n

107 delabTy ist n

132 in (displayS . renderPretty 1.0 50 $ theTy) ""

108 in (displayS . renderPretty 1.0 50 $ theTy) ""

109+

110+

111+fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

112+fancifyAnnots ist annot@(AnnName n _ _ _) = case makeAnnName ist n of

113+ Just fancyAnnot -> fancyAnnot

114+ Nothing -> annot

133fancifyAnnots _ annot = annot

115fancifyAnnots _ annot = annot

134

116

117+

118+ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

119+ideSlaveReturnWithStatus status n h out = do

120+ ist <- getIState

121+ (str, spans) <- fmap displaySpans .

122+ iRender .

123+ fmap (fancifyAnnots ist) $

124+ out

125+ let good = [SymbolAtom status, toSExp str, toSExp spans]

126+ runIO . hPutStrLn h $ convSExp "return" good n

127+

128+

129+-- | Write pretty-printed output to IDESlave with semantic annotations

130+ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

131+ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"

132+

135-- | Show an error with semantic highlighting

133-- | Show an error with semantic highlighting

136ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

134ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

137ihRenderError h e = do ist <- getIState

135ihRenderError h e = do ist <- getIState

138 case idris_outputmode ist of

136 case idris_outputmode ist of

139 RawOutput -> consoleDisplayAnnotated h e

137 RawOutput -> consoleDisplayAnnotated h e

140− IdeSlave n -> do

138+ IdeSlave n -> ideSlaveReturnWithStatus "error" n h e

141− (str, spans) <- fmap displaySpans .

139+

142− iRender .

140+ihPrintWithStatus :: String -> Handle -> String -> Idris ()

143− fmap (fancifyAnnots ist) $

141+ihPrintWithStatus status h s = do

144− e

142+ i <- getIState

143+ case idris_outputmode i of

144+ RawOutput -> case s of

145+ "" -> return ()

146+ s -> runIO $ hPutStrLn h s

147+ IdeSlave n ->

145− let good = [SymbolAtom "error", toSExp str, toSExp spans]

148+ let good = SexpList [SymbolAtom status, toSExp s] in

146− runIO . hPutStrLn h $ convSExp "return" good n

149+ runIO $ hPutStrLn h $ convSExp "return" good n

150+

151+

152+ihPrintResult :: Handle -> String -> Idris ()

153+ihPrintResult = ihPrintWithStatus "ok"

147

154

148ihPrintError :: Handle -> String -> Idris ()

155ihPrintError :: Handle -> String -> Idris ()

149−ihPrintError h s = do i <- getIState

156+ihPrintError = ihPrintWithStatus "error"

150− case idris_outputmode i of

151− RawOutput -> case s of

152− "" -> return ()

153− s -> runIO $ hPutStrLn h s

154− IdeSlave n ->

155− let good = SexpList [SymbolAtom "error", toSExp s] in

156− runIO . hPutStrLn h $ convSExp "return" good n

157

158ihputStrLn :: Handle -> String -> Idris ()

159ihputStrLn h s = do i <- getIState

src/Idris/REPL.hs+7−12

@@ -32,7 +32,7 @@ import Idris.DeepSeq

32import Idris.Output

33import Idris.Interactive

34import Idris.WhoCalls

35−import Idris.TypeSearch (searchByType, searchPred, defaultScoreFunction)

35+import Idris.TypeSearch (searchByType)

37import Paths_idris

38import Version_idris (gitHash)

@@ -708,8 +708,7 @@ process h fn (DebugInfo n)

708 iputStrLn $ "Size change: " ++ show sc

709 when (not (null cg')) $ do iputStrLn "Call graph:\n"

710 iputStrLn (show cg')

711−process h fn (Search t) = searchByType h (searchPred defaultScoreFunction) scoreLimit t where

711+process h fn (Search t) = searchByType h t

712− scoreLimit = 100

713process h fn (CaseSplitAt updatefile l n)

712process h fn (CaseSplitAt updatefile l n)

714 = caseSplitAt h fn updatefile l n

713 = caseSplitAt h fn updatefile l n

715process h fn (AddClauseFrom updatefile l n)

714process h fn (AddClauseFrom updatefile l n)

@@ -905,10 +904,9 @@ process h fn ColourOff

905 putIState $ ist { idris_colourRepl = False }

904 putIState $ ist { idris_colourRepl = False }

906process h fn ListErrorHandlers =

905process h fn ListErrorHandlers =

907 do ist <- getIState

906 do ist <- getIState

908− case idris_errorhandlers ist of

907+ iPrintResult $ case idris_errorhandlers ist of

909− [] -> iPrintResult "No registered error handlers"

908+ [] -> "No registered error handlers"

910− handlers ->

911− iPrintResult $ "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers

909+ handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers

912process h fn (SetConsoleWidth w) = setWidth w

910process h fn (SetConsoleWidth w) = setWidth w

913

911

914process h fn (Apropos a) =

912process h fn (Apropos a) =

@@ -918,11 +916,8 @@ process h fn (Apropos a) =

918 delabTy ist n,

916 delabTy ist n,

919 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

917 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

920 | n <- sort names, isUN n ]

918 | n <- sort names, isUN n ]

921− ihRenderResult h $ vsep (map (renderApropos ist) aproposInfo)

919+ ihRenderResult h $ vsep (map (prettyDocumentedIst ist) aproposInfo)

922− where renderApropos ist (name, ty, docs) =

923− prettyName True [] name <+> colon <+> align (prettyIst ist ty) <$>

924− fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

925− isUN (UN _) = True

920+ where isUN (UN _) = True

926 isUN (NS n _) = isUN n

921 isUN (NS n _) = isUN n

927 isUN _ = False

922 isUN _ = False

928

923

src/Idris/TypeSearch.hs+51−38

@@ -7,7 +7,8 @@ import Control.Arrow (first, second, (&&&))

7import Control.Monad (forM_, guard)

9import Data.Function (on)

10−import Data.List (find, sortBy, (\\))

10+import Data.List (find, minimumBy, sortBy, (\\))

11+import Data.Map (Map)

11import qualified Data.Map as M

12import qualified Data.Map as M

12import Data.Maybe (catMaybes, fromMaybe, isJust)

13import Data.Maybe (catMaybes, fromMaybe, isJust)

13import Data.Monoid (Monoid (mempty, mappend))

14import Data.Monoid (Monoid (mempty, mappend))

@@ -16,39 +17,43 @@ import qualified Data.Set as S

17import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)

18import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)

18import Idris.AbsSyntaxTree (class_instances, defaultSyntax, Idris,

19import Idris.AbsSyntaxTree (class_instances, defaultSyntax, Idris,

19− IState (idris_classes, tt_ctxt),

20+ IState (idris_classes, idris_docstrings, tt_ctxt),

20− implicitAllowed, prettyIst, PTerm, toplevel)

21+ implicitAllowed, prettyDocumentedIst, prettyIst, PTerm, toplevel)

21import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

22import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

22import Idris.Core.TT

23import Idris.Core.TT

23import Idris.Core.Unify (match_unify)

24import Idris.Core.Unify (match_unify)

24import Idris.Delaborate (delab, delabTy)

25import Idris.Delaborate (delab, delabTy)

25−import Idris.Docstrings (noDocs)

26+import Idris.Docstrings (noDocs, overview)

26import Idris.ElabDecls (elabType')

27import Idris.ElabDecls (elabType')

27import Idris.Output (ihRenderResult, ihPrintResult, ihPrintFunTypes)

28import Idris.Output (ihRenderResult, ihPrintResult, ihPrintFunTypes)

29import System.IO (Handle)

30import System.IO (Handle)

32+import Util.Pretty (text, vsep, char, (<>), Doc)

32−searchByType :: (Ord a, Show a) => Handle -> (IState -> Type -> Type -> Maybe a) -> a -> PTerm -> Idris ()

34+searchByType :: Handle -> PTerm -> Idris ()

33−searchByType h pred scoreLimit pterm = do

35+searchByType h pterm = do

34 pterm' <- addUsingConstraints syn emptyFC pterm

36 pterm' <- addUsingConstraints syn emptyFC pterm

35 pterm'' <- implicit toplevel syn n pterm'

37 pterm'' <- implicit toplevel syn n pterm'

36 i <- getIState

38 i <- getIState

37 let pterm''' = addImpl i pterm''

39 let pterm''' = addImpl i pterm''

38 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'

40 ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'

39 putIState i -- don't actually make any changes

41 putIState i -- don't actually make any changes

40− ihRenderResult h (prettyIst i pterm)

41− let names = searchUsing pred i ty

42+ let names = searchUsing searchPred i ty

42− let names' = take numLimit . takeWhile ((< scoreLimit) . snd . snd) $

43+ let names' = take numLimit . takeWhile ((< scoreLimit) . getScore) $

43− sortBy (compare `on` (snd . snd)) names

44+ sortBy (compare `on` getScore) names

44− forM_ names' $ \(name, (typ, val)) -> do

45+ let docs =

45− ihPrintFunTypes h [] name [(name, delabTy i name)]

46+ [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in

46− ihPrintResult h ("\tScore: " ++ show val ++ "\n")

47+ displayScore score <> char ' ' <> prettyDocumentedIst i docInfo

48+ | (n, (_,score)) <- names']

49+ ihRenderResult h $ vsep docs

47 where

50 where

51+ getScore = defaultScoreFunction . snd . snd

48 numLimit = 50

52 numLimit = 50

53+ scoreLimit = 100

49 syn = defaultSyntax { implicitAllowed = True } -- syntax

54 syn = defaultSyntax { implicitAllowed = True } -- syntax

50 n = sMN 0 "searchType" -- name

55 n = sMN 0 "searchType" -- name

51−

56+

53searchUsing :: (IState -> Type -> Type -> Maybe a) -> IState -> Type -> [(Name, (Type, a))]

58searchUsing :: (IState -> Type -> Type -> Maybe a) -> IState -> Type -> [(Name, (Type, a))]

54searchUsing pred istate ty =

59searchUsing pred istate ty =

@@ -82,10 +87,10 @@ tcToMaybe (Error _) = Nothing

85−searchPred :: (Score -> Int) -> IState -> Type -> Type -> Maybe Int

90+searchPred :: IState -> Type -> Type -> Maybe Score

86−searchPred scoref istate ty1 = \ty2 -> case matcher ty2 of

91+searchPred istate ty1 = \ty2 -> case matcher ty2 of

87 Nothing -> Nothing

92 Nothing -> Nothing

88− Just xs -> guard (not (null xs)) >> return (minimum (map scoref xs))

93+ Just xs -> guard (not (null xs)) >> return (minimumBy (compare `on` defaultScoreFunction) xs)

89 where

94 where

90 matcher = unifyWithHoles True istate ty1

95 matcher = unifyWithHoles True istate ty1

@@ -102,7 +107,7 @@ reverseDag xs = map f xs where

102computeDagP :: Ord n => TT n -> ([((n, TT n), Set n)], TT n)

107computeDagP :: Ord n => TT n -> ([((n, TT n), Set n)], TT n)

103computeDagP t = (reverse (map f args), retTy) where

108computeDagP t = (reverse (map f args), retTy) where

104

109

105− f (n, t) = ((n, t), usedVars t)

110+ f (n, t) = ((n, t), M.keysSet (usedVars t))

106

111

107 (numArgs, args, retTy) = go 0 [] t

112 (numArgs, args, retTy) = go 0 [] t

108

113

@@ -110,17 +115,17 @@ computeDagP t = (reverse (map f args), retTy) where

110 go k args (Bind n (Pi t) sc) = go (succ k) ( (n, t) : args ) sc

115 go k args (Bind n (Pi t) sc) = go (succ k) ( (n, t) : args ) sc

111 go k args retTy = (k, args, retTy)

116 go k args retTy = (k, args, retTy)

112

117

113− usedVars :: Ord n => TT n -> Set n

114− usedVars (V j) = error "unexpected! run vToP first"

115− usedVars (P Bound n t) = S.singleton n `S.union` usedVars t

116− usedVars (Bind n binder t2) = (S.delete n (usedVars t2) `S.union`) $ case binder of

117− Let t v -> usedVars t `S.union` usedVars v

118− Guess t v -> usedVars t `S.union` usedVars v

119− b -> usedVars (binderTy b)

120− usedVars (App t1 t2) = usedVars t1 `S.union` usedVars t2

121− usedVars (Proj t _) = usedVars t

122− usedVars _ = S.empty

123

118

119+usedVars :: Ord n => TT n -> Map n (TT n)

120+usedVars (V j) = error "unexpected! run vToP first"

121+usedVars (P Bound n t) = M.singleton n t `M.union` usedVars t

122+usedVars (Bind n binder t2) = (M.delete n (usedVars t2) `M.union`) $ case binder of

123+ Let t v -> usedVars t `M.union` usedVars v

124+ Guess t v -> usedVars t `M.union` usedVars v

125+ b -> usedVars (binderTy b)

126+usedVars (App t1 t2) = usedVars t1 `M.union` usedVars t2

127+usedVars (Proj t _) = usedVars t

128+usedVars _ = M.empty

124

129

125deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]

130deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]

126deleteFromDag name [] = []

131deleteFromDag name [] = []

@@ -136,6 +141,15 @@ data Score = Score

136 , leftTypeClass :: Int

141 , leftTypeClass :: Int

137 , rightTypeClass :: Int } deriving (Eq, Show)

142 , rightTypeClass :: Int } deriving (Eq, Show)

138

143

144+displayScore :: Score -> Doc a

145+displayScore (Score trans lapp rapp lclass rclass) = text $ case (lt, gt) of

146+ (True , True ) -> "="

147+ (True , False) -> "<"

148+ (False, True ) -> ">"

149+ (False, False) -> " "

150+ where lt = lapp + lclass == 0

151+ gt = rapp + rclass == 0

152+

139

153

140scoreCriterion :: Score -> Bool

154scoreCriterion :: Score -> Bool

141scoreCriterion (Score a b c d e) = True {- not

155scoreCriterion (Score a b c d e) = True {- not

@@ -205,18 +219,17 @@ unifyWithHoles debugParam istate type1 = \type2 -> let

205 mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs

219 mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs

206

220

207 updateDags ((name, term) : xs) (holes, args1, args2) = case (mgetType name args1, mgetType name args2) of

221 updateDags ((name, term) : xs) (holes, args1, args2) = case (mgetType name args1, mgetType name args2) of

208− (Just _, Nothing) -> thrd (\score -> score { leftApplied = succ (leftApplied score) }) <$>

222+ (Just (_,ix), Nothing) -> thrd (\score -> score { leftApplied = succ (leftApplied score) }) <$> nextStep

209− updateDags xs (holes', updatef args1, args2)

210− (Nothing, Just _) -> thrd (\score -> score { rightApplied = succ (rightApplied score) }) <$>

223+ (Nothing, Just (_, ix)) -> thrd (\score -> score { rightApplied = succ (rightApplied score) }) <$> nextStep

211− updateDags xs (holes', args1, updatef args2)

224+ (Nothing, Nothing) -> nextStep

212− _ -> error "Shouldn't happen. Watch the alpha conversion!"

225+ _ -> error ("Shouldn't happen. Watch the alpha conversion!\n" ++ show args1 ++ "\n\n" ++ show args2)

213 where

226 where

227+ varsInTy = map fst $ M.toList (usedVars term)

228+ deleteMany = foldr (.) id $ map deleteFromDag (name : varsInTy)

214 thrd f (a,b,c) = (a,b,f c)

229 thrd f (a,b,c) = (a,b,f c)

215− holes' = holes \\ [name]

230+ nextStep = updateDags xs (holes \\ [name], updatef args1, updatef args2 )

216− updatef = map (first . second $ subst name term) . deleteFromDag name

217− args1' = deleteFromDag name args1

218− args1'' = map (first . second $ subst name term) args1'

231+ updatef = map (first . second $ subst name term) . deleteMany

219− mgetType name xs = fmap (snd . fst) . find ((name ==) . fst . fst) $ xs

232+ mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs

220

233

221

234

222 go :: State -> [(Type, Type)] -> Maybe State

235 go :: State -> [(Type, Type)] -> Maybe State