Refactor FoundHoles : REPLResult to carry more structured information about holes

src/Idris/IDEMode/Holes.idr

@@ -5,6 +5,7 @@ import Core.Env
 import Idris.Resugar
 import Idris.Syntax
 
+public export
 record HolePremise where
   constructor MkHolePremise
   name         : Name
@@ -13,6 +14,7 @@ record HolePremise where
   isImplicit   : Bool
   
 
+public export
 record HoleData where
   constructor MkHoleData
   name : Name
@@ -30,6 +32,7 @@ isHole def
                  case holeInfo pi of
                       NotHole => Nothing
                       SolvedHole n => Just n
+           None => Just 0
            _ => Nothing
 
 
@@ -78,7 +81,7 @@ extractHoleData defs env fn (S args) (Bind fc x b sc)
     implicitBind _ = False
    
 extractHoleData defs env fn args ty
-  = do ity <- resugar env !(normalise defs env ty)
+  = do ity <- resugar env !(normaliseHoles defs env ty)
        pure $ MkHoleData fn ity []
 
 
@@ -112,7 +115,9 @@ showHole : {vars : _} ->
           Core String
 showHole defs env fn args ty
     = do hdata <- holeData defs env fn args ty
-         pure $ concat 
+         case hdata.context of
+           [] => pure $ show (hdata.name) ++ " : " ++ show hdata.type
+           _  => pure $ concat 
               (map (\hole => showCount hole.multiplicity
                              ++ (impBracket hole.isImplicit $
                                  tidy hole.name ++ " : " ++ (show hole.type) ++ "\n" )

src/Idris/IDEMode/REPL.idr

@@ -320,10 +320,10 @@ displayIDEResult outf i  (REPL $ FoundHoles xs)
   = printIDEResult outf i $ !holesSexp
   where
     sexpName : 
-      Name -> Core SExp
+      HoleData -> Core SExp
     sexpName n = do
       pure $ SExpList 
-        [ StringAtom (show  n)
+        [ StringAtom (show  n.name)
         , SExpList []  -- Premises
         , SExpList [ StringAtom "?"   -- Conclusion
                    , SExpList[]]    -- TODO: Highlighting information

src/Idris/REPL.idr

@@ -422,7 +422,7 @@ data REPLResult : Type where
   ProofFound : PTerm -> REPLResult
   Missed : List MissedResult -> REPLResult
   CheckedTotal : List (Name, Totality) -> REPLResult
-  FoundHoles : List Name -> REPLResult
+  FoundHoles : List HoleData -> REPLResult
   OptionsSet : List REPLOpt -> REPLResult
   LogLevelSet : Nat -> REPLResult
   VersionIs : Version -> REPLResult
@@ -630,8 +630,21 @@ process (SetLog lvl)
     = do setLogLevel lvl
          pure $ LogLevelSet lvl
 process Metavars
-    = do ms <- getUserHoles
-         pure $ FoundHoles ms
+    = do defs <- get Ctxt
+         let ctxt = gamma defs
+         ms  <- getUserHoles
+         let globs = concat !(traverse (\n => lookupCtxtName n ctxt) ms)
+         let holesWithArgs = mapMaybe (\(n, i, gdef) => do args <- isHole gdef
+                                                           pure (n, gdef, args))
+                                      globs
+         hData <- the (Core $ List HoleData) $
+             traverse (\n_gdef_args => 
+                        -- Inference can't deal with this for now :/
+                        let (n, gdef, args) = the (Name, GlobalDef, Nat) n_gdef_args in
+                        holeData defs [] n args (type gdef))
+                      holesWithArgs 
+         pure $ FoundHoles hData
+
 process (Editing cmd)
     = do ppopts <- getPPrint
          -- Since we're working in a local environment, don't do the usual
@@ -788,9 +801,9 @@ mutual
   displayResult  (Missed cases) = printResult $ showSep "\n" $ map handleMissing cases
   displayResult  (CheckedTotal xs) = printResult $ showSep "\n" $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs
   displayResult  (FoundHoles []) = printResult $ "No holes"
-  displayResult  (FoundHoles [x]) = printResult $ "1 hole: " ++ show x
+  displayResult  (FoundHoles [x]) = printResult $ "1 hole: " ++ show x.name
   displayResult  (FoundHoles xs) = printResult $ show (length xs) ++ " holes: " ++
-                                   showSep ", " (map show xs)
+                                   showSep ", " (map (show . name) xs)
   displayResult  (LogLevelSet k) = printResult $ "Set loglevel to " ++ show k
   displayResult  (VersionIs x) = printResult $ showVersion True x
   displayResult  (RequestedHelp) = printResult displayHelp

tests/typedd-book/chapter01/expected

@@ -3,6 +3,5 @@
 3/5: Building HelloHole (HelloHole.idr)
 4/5: Building HoleFix (HoleFix.idr)
 5/5: Building All (All.idr)
-Main> -------------------------------------
-convert : Char -> String
+Main> Main.convert : Char -> String
 Main> Bye for now!