Merge pull request #153 from ohad/ide-protocol-holes

Ide protocol holes

idris2.ipkg

@@ -71,6 +71,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,146 @@
+module Idris.IDEMode.Holes
+
+import Core.Env
+
+import Idris.Resugar
+import Idris.Syntax
+
+import Idris.IDEMode.Commands
+
+public export
+record HolePremise where
+  constructor MkHolePremise
+  name         : Name
+  type         : PTerm
+  multiplicity : RigCount  
+  isImplicit   : Bool
+  
+
+public export
+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
+           None => Just 0
+           _ => 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 !(normaliseHoles 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 hdata
+              else record { context $= dropShadows } 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
+         case hdata.context of
+           [] => pure $ show (hdata.name) ++ " : " ++ show hdata.type
+           _  => pure $ concat 
+              (map (\premise => showCount premise.multiplicity
+                             ++ (impBracket premise.isImplicit $
+                                 tidy premise.name ++ " : " ++ (show premise.type) ++ "\n" )
+                   ) hdata.context)
+              ++ "-------------------------------------\n"
+              ++ nameRoot (hdata.name) ++ " : " ++ show hdata.type
+
+sexpPremise : HolePremise -> SExp
+sexpPremise premise = 
+  SExpList [StringAtom $ showCount premise.multiplicity 
+                       ++ (impBracket premise.isImplicit $
+                           tidy premise.name)
+           ,StringAtom $ show premise.type
+           ,SExpList [] -- TODO: metadata
+           ]
+
+export
+sexpHole : HoleData -> SExp
+sexpHole hole = SExpList 
+  [ StringAtom (show  hole.name)
+  , SExpList $ map sexpPremise hole.context  -- Premises
+  , SExpList [ StringAtom $ show hole.type   -- Conclusion
+             , SExpList[]]    -- TODO: Highlighting information
+  ]

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} ->
@@ -317,14 +314,8 @@ displayIDEResult outf i  (REPL $ CheckedTotal xs)
   = printIDEResult outf i 
   $ StringAtom $ showSep "\n" 
   $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs
-displayIDEResult outf i  (REPL $ FoundHoles []) 
+displayIDEResult outf i  (REPL $ FoundHoles holes) 
-  = printIDEResult outf i $ SExpList []
+  = printIDEResult outf i $ SExpList $ map sexpHole holes
-displayIDEResult outf i  (REPL $ FoundHoles xs) 
-  = printIDEResult outf i $ holesSexp
-  where
-    holesSexp : SExp
-    holesSexp = SExpList $ map sexpName xs
-
 displayIDEResult outf i  (REPL $ LogLevelSet k) 
   = printIDEResult outf i 
   $ StringAtom $ "Set loglevel to " ++ show k

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,82 +77,6 @@ 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
-
 displayType : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->
               Defs -> (Name, Int, GlobalDef) ->
@@ -494,7 +419,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
@@ -702,8 +627,21 @@ process (SetLog lvl)
     = do setLogLevel lvl
          pure $ LogLevelSet lvl
 process Metavars
-    = do ms <- getUserHoles
+    = do defs <- get Ctxt
-         pure $ FoundHoles ms
+         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
@@ -860,9 +798,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> -------------------------------------
+Main> Main.convert : Char -> String
-convert : Char -> String
 Main> Bye for now!