0 | module Idris.REPL.FuzzySearch
  1 |
  2 | import Core.Metadata
  3 |
  4 | import Idris.Doc.String
  5 | import Idris.Pretty
  6 | import Idris.Syntax
  7 |
  8 | import public Idris.REPL.Common
  9 |
 10 | import Data.String
 11 | import Libraries.Data.List.Extra
 12 | import Libraries.Data.WithDefault
 13 |
 14 | %default covering
 15 |
 16 | export
 17 | fuzzySearch : {auto c : Ref Ctxt Defs}
 18 |            -> {auto s : Ref Syn SyntaxInfo}
 19 |            -> {auto o : Ref ROpts REPLOpts}
 20 |            -> PTerm
 21 |            -> Core REPLResult
 22 | fuzzySearch expr = do
 23 |   let Just (neg, pos) = parseExpr expr
 24 |     | _ => pure (REPLError ("Bad expression, expected"
 25 |                        <++> code "B"
 26 |                        <++> "or"
 27 |                        <++> code "A -> _"
 28 |                        <++> "or"
 29 |                        <++> code "A -> B"
 30 |                        <+> ", where"
 31 |                        <++> code "A"
 32 |                        <++> "and"
 33 |                        <++> code "B"
 34 |                        <++> "are spines of global names"))
 35 |   defs <- branch
 36 |   let curr = currentNS defs
 37 |   let ctxt = gamma defs
 38 |   filteredDefs <-
 39 |     do names   <- allNames ctxt
 40 |        defs    <- traverse (flip lookupCtxtExact ctxt) names
 41 |        let defs = flip mapMaybe defs $ \ md =>
 42 |                       do d <- md
 43 |                          guard (visibleIn curr (fullname d) (collapseDefault $ visibility d))
 44 |                          guard (isJust $ userNameRoot (fullname d))
 45 |                          pure d
 46 |        allDefs <- traverse (resolved ctxt) defs
 47 |        filterM (predicate neg pos) allDefs
 48 |   put Ctxt defs
 49 |   doc <- traverse (docsOrSignature EmptyFC) $ fullname <$> filteredDefs
 50 |   pure $ PrintedDoc $ vsep doc
 51 |  where
 52 |
 53 |   data NameOrConst = AName Name
 54 |                    | APrimType PrimType
 55 |                    | AType
 56 |
 57 |   eqConst : (x, y : NameOrConst) -> Bool
 58 |   eqConst (APrimType x) (APrimType y) = x == y
 59 |   eqConst AType         AType         = True
 60 |   eqConst _             _             = False -- names equality is irrelevant
 61 |
 62 |   parseNameOrConst : PTerm -> Maybe NameOrConst
 63 |   parseNameOrConst (PRef _ n)               = Just (AName n)
 64 |   parseNameOrConst (PPrimVal _ $ PrT t)     = Just (APrimType t)
 65 |   parseNameOrConst (PType _)                = Just AType
 66 |   parseNameOrConst _                        = Nothing
 67 |
 68 |   parseExpr' : PTerm -> Maybe (List NameOrConst)
 69 |   parseExpr' (PApp _ f x) =
 70 |     [| parseNameOrConst x :: parseExpr' f |]
 71 |   parseExpr' x = (:: []) <$> parseNameOrConst x
 72 |
 73 |   parseExpr : PTerm -> Maybe (List NameOrConst, List NameOrConst)
 74 |   parseExpr (PPi _ _ _ _ a (PImplicit _)) = do
 75 |     a' <- parseExpr' a
 76 |     pure (a', [])
 77 |   parseExpr (PPi _ _ _ _ a b) = do
 78 |     a' <- parseExpr' a
 79 |     b' <- parseExpr' b
 80 |     pure (a', b')
 81 |   parseExpr b = do
 82 |     b' <- parseExpr' b
 83 |     pure ([], b')
 84 |
 85 |   isApproximationOf : (given : Name)
 86 |                    -> (candidate : Name)
 87 |                    -> Bool
 88 |   isApproximationOf (NS ns n) (NS ns' n') =
 89 |     n == n' && Namespace.isApproximationOf ns ns'
 90 |   isApproximationOf (UN n) (NS ns' (UN n')) =
 91 |     n == n'
 92 |   isApproximationOf (NS ns n) _ =
 93 |     False
 94 |   isApproximationOf (UN n) (UN n') =
 95 |     n == n'
 96 |   isApproximationOf _ _ =
 97 |     False
 98 |
 99 |   isApproximationOf' : (given : NameOrConst)
100 |                     -> (candidate : NameOrConst)
101 |                     -> Bool
102 |   isApproximationOf' (AName x) (AName y) =
103 |     isApproximationOf x y
104 |   isApproximationOf' a b = eqConst a b
105 |
106 |   ||| Find all name and type literal occurrences.
107 |   export
108 |   doFind : List NameOrConst -> Term vars -> List NameOrConst
109 |   doFind ns (Local fc x idx y) = ns
110 |   doFind ns (Ref fc x name) = AName name :: ns
111 |   doFind ns (Meta fc n i xs)
112 |       = foldl doFind ns xs
113 |   doFind ns (Bind fc x (Let _ c val ty) scope)
114 |       = doFind (doFind (doFind ns val) ty) scope
115 |   doFind ns (Bind fc x b scope)
116 |       = doFind (doFind ns (binderType b)) scope
117 |   doFind ns (App fc fn arg)
118 |       = doFind (doFind ns fn) arg
119 |   doFind ns (As fc s as tm) = doFind ns tm
120 |   doFind ns (TDelayed fc x y) = doFind ns y
121 |   doFind ns (TDelay fc x t y)
122 |       = doFind (doFind ns t) y
123 |   doFind ns (TForce fc r x) = doFind ns x
124 |   doFind ns (PrimVal fc c) =
125 |     fromMaybe [] ((:: []) <$> parseNameOrConst (PPrimVal fc c)) ++ ns
126 |   doFind ns (Erased fc i) = ns
127 |   doFind ns (TType fc _) = AType :: ns
128 |
129 |   toFullNames' : NameOrConst -> Core NameOrConst
130 |   toFullNames' (AName x) = AName <$> toFullNames x
131 |   toFullNames' x = pure x
132 |
133 |   fuzzyMatch : (neg : List NameOrConst)
134 |             -> (pos : List NameOrConst)
135 |             -> Term vars
136 |             -> Core Bool
137 |   fuzzyMatch neg pos (Bind _ _ b sc) = do
138 |     let refsB = doFind [] (binderType b)
139 |     refsB <- traverse toFullNames' refsB
140 |     let neg' = diffBy isApproximationOf' neg refsB
141 |     fuzzyMatch neg' pos sc
142 |   fuzzyMatch (_ :: _) pos tm = pure False
143 |   fuzzyMatch [] pos tm = do
144 |     let refsB = doFind [] tm
145 |     refsB <- traverse toFullNames' refsB
146 |     pure (isNil $ diffBy isApproximationOf' pos refsB)
147 |
148 |   predicate :  (neg : List NameOrConst)
149 |             -> (pos : List NameOrConst)
150 |             -> GlobalDef
151 |             -> Core Bool
152 |   predicate neg pos def = case definition def of
153 |     Hole {} => pure False
154 |     _ => fuzzyMatch neg pos def.type
155 |