git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1525 from bmsherman/searchAnnotation

Add annotations for :search result classification

commit29b4d1a37f5aec3dc62c01103590596dcd091892 authorDavid Christiansen <david@davidchristiansen.dk> dateTue 16 Sep 2014, 18:34 (12 years ago) parent0ffc92a7ce4d90
4 files changed+16−7
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+1 src/Idris/Core/TT.hs+1 src/Idris/IdeSlave.hs+6 src/Idris/TypeSearch.hs+8−7
src/Idris/AbsSyntaxTree.hs+1
@@ -1207,6 +1207,7 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
12071207 colour UnderlineText = IdrisColour Nothing True True False False
12081208 colour ItalicText = IdrisColour Nothing True False False True
12091209consoleDecorate ist (AnnTerm _ _) = id
1210+consoleDecorate ist (AnnSearchResult _) = id
12101211
12111212isPostulateName :: Name -> IState -> Bool
12121213isPostulateName n ist = S.member n (idris_postulates ist)
src/Idris/Core/TT.hs+1
@@ -102,6 +102,7 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St
102102 | AnnFC FC
103103 | AnnTextFmt TextFormatting
104104 | AnnTerm [(Name, Bool)] (TT Name) -- ^ pprint bound vars, original term
105+ | AnnSearchResult Ordering -- ^ more general, isomorphic, or more specific
105106
106107-- | Used for error reflection
107108data ErrorReportPart = TextPart String
src/Idris/IdeSlave.hs+6
@@ -145,6 +145,12 @@ instance SExpable OutputAnnotation where
145145 ItalicText -> "italic"
146146 UnderlineText -> "underline"
147147 toSExp (AnnTerm bnd tm) = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm bnd tm))]
148+ toSExp (AnnSearchResult ordr) = toSExp [(SymbolAtom "doc-overview",
149+ StringAtom ("Result type is " ++ descr))]
150+ where descr = case ordr of
151+ EQ -> "isomorphic"
152+ LT -> "more general than searched type"
153+ GT -> "more specific than searched type"
148154
149155encodeTerm :: [(Name, Bool)] -> Term -> String
150156encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $
src/Idris/TypeSearch.hs+8−7
@@ -34,7 +34,7 @@ import Idris.Output (iRenderOutput, iPrintResult, iRenderResult)
3434
3535import Prelude hiding (pred)
3636
37−import Util.Pretty (text, char, vsep, (<>), Doc)
37+import Util.Pretty (text, char, vsep, (<>), Doc, annotate)
3838
3939searchByType :: PTerm -> Idris ()
4040searchByType pterm = do
@@ -173,13 +173,14 @@ data Score = Score
173173 , asymMods :: !(Sided AsymMods)
174174 } deriving (Eq, Show)
175175
176−displayScore :: Score -> Doc a
177−displayScore score = text $ case both noMods (asymMods score) of
178− Sided True True -> "=" -- types are isomorphic
179− Sided True False -> "<" -- found type is more general than searched type
180− Sided False True -> ">" -- searched type is more general than found type
181− Sided False False -> "_"
176+displayScore :: Score -> Doc OutputAnnotation
177+displayScore score = case both noMods (asymMods score) of
178+ Sided True True -> annotated EQ "=" -- types are isomorphic
179+ Sided True False -> annotated LT "<" -- found type is more general than searched type
180+ Sided False True -> annotated GT ">" -- searched type is more general than found type
181+ Sided False False -> text "_"
182182 where
183+ annotated ordr = annotate (AnnSearchResult ordr) . text
183184 noMods (Mods app tcApp tcIntro) = app + tcApp + tcIntro == 0
184185
185186scoreCriterion :: Score -> Bool