Refactor hole information extracting functions into a new submodule

Introduce a new data structure for IDE-related hole data

Separate hole printing from informationextraction

idris2.ipkg

@@ -70,6 +70,7 @@ modules =
     Idris.IDEMode.Parser,
     Idris.IDEMode.REPL,
     Idris.IDEMode.TokenLine,
+    Idris.IDEMode.Holes,
     Idris.ModTree,
     Idris.Package,
     Idris.Parser,

src/Idris/IDEMode/Holes.idr

@@ -0,0 +1,123 @@
+module Idris.IDEMode.Holes
+
+import Core.Env
+
+import Idris.Resugar
+import Idris.Syntax
+
+record HolePremise where
+  constructor MkHolePremise
+  name         : Name
+  type         : PTerm
+  multiplicity : RigCount  
+  isImplicit   : Bool
+  
+
+record HoleData where
+  constructor MkHoleData
+  name : Name
+  type : PTerm
+  context : List HolePremise
+
+||| If input is a hole, return number of locals in scope at binding
+||| point
+export  
+isHole : GlobalDef -> Maybe Nat
+isHole def
+    = case definition def of
+           Hole locs _ => Just locs
+           PMDef pi _ _ _ _ =>
+                 case holeInfo pi of
+                      NotHole => Nothing
+                      SolvedHole n => Just n
+           _ => Nothing
+
+
+
+-- Bring these back into REPL.idr
+showName : Name -> Bool
+showName (UN "_") = False
+showName (MN _ _) = False
+showName _ = True
+
+showCount : RigCount -> String
+showCount = elimSemi
+                 " 0 "
+                 " 1 "
+                 (const "   ")
+
+impBracket : Bool -> String -> String
+impBracket False str = str
+impBracket True str = "{" ++ str ++ "}"
+
+tidy : Name -> String
+tidy (MN n _) = n
+tidy n = show n
+
+export
+extractHoleData : {vars : _} ->
+          {auto c : Ref Ctxt Defs} ->
+          {auto s : Ref Syn SyntaxInfo} ->
+          Defs -> Env Term vars -> Name -> Nat -> Term vars ->
+          Core HoleData
+extractHoleData defs env fn (S args) (Bind fc x (Let c val ty) sc) 
+  = extractHoleData defs env fn args (subst val sc)
+extractHoleData defs env fn (S args) (Bind fc x b sc)
+  = do rest <- extractHoleData defs (b :: env) fn args sc
+       let True = showName x
+         | False => pure rest
+       ity <- resugar env !(normalise defs env (binderType b))
+       let premise = MkHolePremise x ity (multiplicity b) (implicitBind b)
+       pure $ record { context $= (premise ::)  } rest
+  where
+    implicitBind : Binder (Term vars) -> Bool
+    implicitBind (Pi _ Explicit _) = False
+    implicitBind (Pi _ _ _) = True
+    implicitBind (Lam _ Explicit _) = False
+    implicitBind (Lam _ _ _) = True
+    implicitBind _ = False
+   
+extractHoleData defs env fn args ty
+  = do ity <- resugar env !(normalise defs env ty)
+       pure $ MkHoleData fn ity []
+
+
+export
+holeData : {vars : _} ->
+           {auto c : Ref Ctxt Defs} ->
+           {auto s : Ref Syn SyntaxInfo} ->
+           Defs -> Env Term vars -> Name -> Nat -> Term vars ->
+           Core HoleData
+
+holeData gam env fn args ty
+  = do hdata <- extractHoleData gam env fn args ty
+       pp <- getPPrint
+       pure $ if showImplicits pp
+              then record { context $= dropShadows } hdata
+              else hdata
+  where
+    dropShadows : List HolePremise -> List HolePremise
+    dropShadows [] = []
+    dropShadows (premise :: rest)
+        = if premise.name `elem` map name rest
+             then            dropShadows rest
+             else premise :: dropShadows rest
+       
+
+export
+showHole : {vars : _} ->
+          {auto c : Ref Ctxt Defs} ->
+          {auto s : Ref Syn SyntaxInfo} ->
+          Defs -> Env Term vars -> Name -> Nat -> Term vars ->
+          Core String
+showHole defs env fn args ty
+    = do hdata <- holeData defs env fn args ty
+         pure $ concat 
+              (map (\hole => showCount hole.multiplicity
+                             ++ (impBracket hole.isImplicit $
+                                 tidy hole.name ++ " : " ++ (show hole.type) ++ "\n" )
+                   ) hdata.context)
+              ++ "-------------------------------------\n"
+              ++ nameRoot (hdata.name) ++ " : " ++ show hdata.type
+
+

src/Idris/IDEMode/REPL.idr

@@ -261,9 +261,6 @@ SExpable REPLOpt where
   toSExp (CG str) = SExpList [ SymbolAtom "cg", toSExp str ]
 
 
-sexpName :  Name -> SExp
-sexpName n = SExpList [ StringAtom (show  n), SExpList [], SExpList [StringAtom "?", SExpList[]]]
-
 displayIDEResult : {auto c : Ref Ctxt Defs} ->
        {auto u : Ref UST UState} ->
        {auto s : Ref Syn SyntaxInfo} ->
@@ -320,10 +317,21 @@ displayIDEResult outf i  (REPL $ CheckedTotal xs)
 displayIDEResult outf i  (REPL $ FoundHoles []) 
   = printIDEResult outf i $ SExpList []
 displayIDEResult outf i  (REPL $ FoundHoles xs) 
-  = printIDEResult outf i $ holesSexp
+  = printIDEResult outf i $ !holesSexp
   where
-    holesSexp : SExp
-    holesSexp = SExpList $ map sexpName xs
+    sexpName : 
+      Name -> Core SExp
+    sexpName n = do
+      pure $ SExpList 
+        [ StringAtom (show  n)
+        , SExpList []  -- Premises
+        , SExpList [ StringAtom "?"   -- Conclusion
+                   , SExpList[]]    -- TODO: Highlighting information
+        ]
+  
+    holesSexp : Core SExp
+    holesSexp = pure $ SExpList !( traverse sexpName xs )
+
 
 displayIDEResult outf i  (REPL $ LogLevelSet k) 
   = printIDEResult outf i 

src/Idris/REPL.idr

@@ -26,6 +26,7 @@ import Idris.Error
 import Idris.IDEMode.CaseSplit
 import Idris.IDEMode.Commands
 import Idris.IDEMode.MakeClause
+import Idris.IDEMode.Holes
 import Idris.ModTree
 import Idris.Parser
 import Idris.Resugar
@@ -76,81 +77,8 @@ showInfo (n, idx, d)
                 coreLift $ putStrLn $
                         "Size change: " ++ showSep ", " scinfo
 
-isHole : GlobalDef -> Maybe Nat
-isHole def
-    = case definition def of
-           Hole locs _ => Just locs
-           PMDef pi _ _ _ _ =>
-                 case holeInfo pi of
-                      NotHole => Nothing
-                      SolvedHole n => Just n
-           _ => Nothing
 
-showCount : RigCount -> String
-showCount = elimSemi
-                 " 0 "
-                 " 1 "
-                 (const "   ")
-
-impBracket : Bool -> String -> String
-impBracket False str = str
-impBracket True str = "{" ++ str ++ "}"
-
-showName : Name -> Bool
-showName (UN "_") = False
-showName (MN _ _) = False
-showName _ = True
-
-tidy : Name -> String
-tidy (MN n _) = n
-tidy n = show n
-
-showEnv : {vars : _} ->
-          {auto c : Ref Ctxt Defs} ->
-          {auto s : Ref Syn SyntaxInfo} ->
-          Defs -> Env Term vars -> Name -> Nat -> Term vars ->
-          Core (List (Name, String), String)
-showEnv defs env fn (S args) (Bind fc x (Let c val ty) sc)
-    = showEnv defs env fn args (subst val sc)
-showEnv defs env fn (S args) (Bind fc x b sc)
-    = do ity <- resugar env !(normalise defs env (binderType b))
-         let pre = if showName x
-                      then REPL.showCount (multiplicity b) ++
-                           impBracket (implicitBind b) (tidy x ++ " : " ++ show ity) ++ "\n"
-                      else ""
-         (envstr, ret) <- showEnv defs (b :: env) fn args sc
-         pure ((x, pre) :: envstr, ret)
-  where
-    implicitBind : Binder (Term vars) -> Bool
-    implicitBind (Pi _ Explicit _) = False
-    implicitBind (Pi _ _ _) = True
-    implicitBind (Lam _ Explicit _) = False
-    implicitBind (Lam _ _ _) = True
-    implicitBind _ = False
-showEnv defs env fn args ty
-    = do ity <- resugar env !(normalise defs env ty)
-         pure ([], "-------------------------------------\n" ++
-                    nameRoot fn ++ " : " ++ show ity)
-
-showHole : {vars : _} ->
-           {auto c : Ref Ctxt Defs} ->
-           {auto s : Ref Syn SyntaxInfo} ->
-           Defs -> Env Term vars -> Name -> Nat -> Term vars ->
-           Core String
-showHole gam env fn args ty
-    = do (envs, ret) <- showEnv gam env fn args ty
-         pp <- getPPrint
-         let envs' = if showImplicits pp
-                        then envs
-                        else dropShadows envs
-         pure (concat (map snd envs') ++ ret)
-  where
-    dropShadows : List (Name, a) -> List (Name, a)
-    dropShadows [] = []
-    dropShadows ((n, ty) :: ns)
-        = if n `elem` map fst ns
-             then dropShadows ns
-             else (n, ty) :: dropShadows ns
+-- Put the printing of holes back here
 
 displayType : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->