Add simple REPL for TTImp

src/Core/Context.idr

@@ -472,18 +472,31 @@ addToSave n
 
 -- Specific lookup functions
 export
-lookupDefExact : Name -> Context GlobalDef -> Core (Maybe Def)
-lookupDefExact n gam
+lookupExactBy : (GlobalDef -> a) -> Name -> Context GlobalDef -> 
+                Core (Maybe a)
+lookupExactBy fn n gam
     = do Just gdef <- lookupCtxtExact n gam
               | Nothing => pure Nothing
-         pure (Just (definition gdef))
+         pure (Just (fn gdef))
+
+export
+lookupNameBy : (GlobalDef -> a) -> Name -> Context GlobalDef -> 
+               Core (List (Name, Int, a))
+lookupNameBy fn n gam
+    = do gdef <- lookupCtxtName n gam
+         pure (map (\ (n, i, gd) => (n, i, fn gd)) gdef)
+
+export
+lookupDefExact : Name -> Context GlobalDef -> Core (Maybe Def)
+lookupDefExact = lookupExactBy definition
+
+export
+lookupDefName : Name -> Context GlobalDef -> Core (List (Name, Int, Def))
+lookupDefName = lookupNameBy definition 
 
 export
 lookupTyExact : Name -> Context GlobalDef -> Core (Maybe ClosedTerm)
-lookupTyExact n gam
-    = do Just gdef <- lookupCtxtExact n gam
-              | Nothing => pure Nothing
-         pure (Just (type gdef))
+lookupTyExact = lookupExactBy type 
 
 -- Set the default namespace for new definitions
 export
@@ -557,13 +570,6 @@ inCurrentNS n@(MN _ _)
          pure (NS (currentNS defs) n)
 inCurrentNS n = pure n
 
-export
-lookupTypeExact : Name -> Context GlobalDef -> Core (Maybe ClosedTerm)
-lookupTypeExact n ctxt
-    = do Just gdef <- lookupCtxtExact n ctxt
-              | Nothing => pure Nothing
-         pure (Just (type gdef))
-
 -- Get the next entry id in the context (this is for recording where to go
 -- back to when backtracking in the elaborator)
 export

src/TTImp/Parser.idr

@@ -358,8 +358,27 @@ collectDefs (INamespace loc ns nds :: ds)
 collectDefs (d :: ds)
     = d :: collectDefs ds
 
+-- full programs
 export
 prog : FileName -> Rule (List ImpDecl)
 prog fname
     = do ds <- nonEmptyBlock (topDecl fname)
          pure (collectDefs ds)
+
+-- TTImp REPL commands
+export
+command : Rule ImpREPL
+command
+    = do symbol ":"; exactIdent "t"
+         tm <- expr "(repl)" init
+         pure (Check tm)
+  <|> do symbol ":"; exactIdent "s"
+         n <- name
+         pure (ProofSearch n)
+  <|> do symbol ":"; exactIdent "di"
+         n <- name
+         pure (DebugInfo n)
+  <|> do symbol ":"; exactIdent "q"
+         pure Quit
+  <|> do tm <- expr "(repl)" init
+         pure (Eval tm)

src/TTImp/TTImp.idr

@@ -129,6 +129,15 @@ mutual
     show (IData _ _ d) = show d
     show (IDef _ n cs) = "(%def " ++ show n ++ " " ++ show cs ++ ")"
 
+-- REPL commands for TTImp interaction
+public export
+data ImpREPL : Type where
+     Eval : RawImp -> ImpREPL
+     Check : RawImp -> ImpREPL
+     ProofSearch : Name -> ImpREPL
+     DebugInfo : Name -> ImpREPL
+     Quit : ImpREPL
+
 export
 lhsInCurrentNS : {auto c : Ref Ctxt Defs} ->
                  RawImp -> Core RawImp

src/Yaffle/Main.idr

@@ -12,9 +12,11 @@ import Core.Options
 import Core.TT
 import Core.UnifyState
 
-import TTImp.TTImp
 import TTImp.Parser
 import TTImp.ProcessDecls
+import TTImp.TTImp
+
+import Yaffle.REPL
 
 import System
 
@@ -35,10 +37,7 @@ coreMain fname
                          do makeBuildDirectory (pathToNS (working_dir d) fname)
                             writeToTTC () !(getTTCFileName fname ".ttc")
                             coreLift $ putStrLn "Written TTC"
-
-         defs <- get Ctxt
-         res <- normalise defs [] (Ref emptyFC Func (NS ["Main"] (UN "main")))
-         coreLift $ printLn !(toFullNames res)
+         repl {c} {u}
 
 main : IO ()
 main

src/Yaffle/REPL.idr

@@ -0,0 +1,81 @@
+module Yaffle.REPL
+
+import Core.Context
+import Core.Core
+import Core.Env
+import Core.FC
+import Core.Normalise
+import Core.TT
+import Core.Unify
+
+import TTImp.Elab
+import TTImp.Elab.Check
+import TTImp.Parser
+import TTImp.ProcessDecls
+import TTImp.TTImp
+
+import Parser.Support
+
+import Control.Catchable
+
+%default covering
+
+showInfo : (Name, Int, Def) -> Core ()
+showInfo (n, d) = coreLift $ putStrLn (show n ++ " ==> " ++ show d)
+
+-- Returns 'True' if the REPL should continue
+process : {auto c : Ref Ctxt Defs} ->
+          {auto u : Ref UST UState} ->
+          ImpREPL -> Core Bool
+process (Eval ttimp)
+    = do (tm, _) <- elabTerm (UN "[input]") InExpr [] ttimp Nothing
+         defs <- get Ctxt
+         tmnf <- normalise defs [] tm
+         coreLift (printLn !(toFullNames tmnf))
+         pure True
+process (Check ttimp)
+    = do (tm, gty) <- elabTerm (UN "[input]") InExpr [] ttimp Nothing
+         defs <- get Ctxt
+         tyh <- getTerm gty
+         ty <- normaliseHoles defs [] tyh
+         coreLift (printLn !(toFullNames ty))
+         pure True
+process (ProofSearch n)
+    = do throw (InternalError "Not implemented")
+--          tm <- search () False 1000 [] (UN "(interactive)") Nothing n
+--          gam <- get Ctxt
+--          coreLift (putStrLn (show (normalise gam [] tm)))
+--          dumpConstraints 0 True
+--          pure True
+process (DebugInfo n)
+    = do defs <- get Ctxt
+         traverse showInfo !(lookupDefName n (gamma defs))
+         pure True
+process Quit 
+    = do coreLift $ putStrLn "Bye for now!"
+         pure False
+
+processCatch : {auto c : Ref Ctxt Defs} ->
+               {auto u : Ref UST UState} ->
+               ImpREPL -> Core Bool
+processCatch cmd
+    = catch (process cmd) 
+            (\err => do coreLift (putStrLn (show err))
+                        pure True)
+
+export
+repl : {auto c : Ref Ctxt Defs} ->
+       {auto u : Ref UST UState} ->
+       Core ()
+repl
+    = do coreLift (putStr "Yaffle> ")
+         inp <- coreLift getLine
+         case runParser inp command of
+              Left err => do coreLift (printLn err)
+                             repl
+              Right cmd =>
+                  do if !(processCatch cmd)
+                        then repl
+                        else pure ()
+
+

yaffle.ipkg

@@ -51,7 +51,9 @@ modules =
     TTImp.ProcessType,
     TTImp.TTImp,
 
-    Utils.Binary
+    Utils.Binary,
+
+    Yaffle.REPL
 
 sourcedir = src
 executable = yaffle