From 6d473014fd24fdde262f1dc38e4b047138e366aa Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Fri, 26 Apr 2019 10:16:23 +0100 Subject: [PATCH] Add simple REPL for TTImp --- src/Core/Context.idr | 34 +++++++++++-------- src/TTImp/Parser.idr | 19 +++++++++++ src/TTImp/TTImp.idr | 9 +++++ src/Yaffle/Main.idr | 9 +++-- src/Yaffle/REPL.idr | 81 ++++++++++++++++++++++++++++++++++++++++++++ yaffle.ipkg | 4 ++- 6 files changed, 136 insertions(+), 20 deletions(-) create mode 100644 src/Yaffle/REPL.idr diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 4cecd04..48a1b81 100644 --- a/src/Core/Context.idr +++ b/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 diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index cb0f313..a915eb2 100644 --- a/src/TTImp/Parser.idr +++ b/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) diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 40754e6..a23e7b0 100644 --- a/src/TTImp/TTImp.idr +++ b/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 diff --git a/src/Yaffle/Main.idr b/src/Yaffle/Main.idr index ee387ce..c60cd62 100644 --- a/src/Yaffle/Main.idr +++ b/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 diff --git a/src/Yaffle/REPL.idr b/src/Yaffle/REPL.idr new file mode 100644 index 0000000..c679bcf --- /dev/null +++ b/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 () + + diff --git a/yaffle.ipkg b/yaffle.ipkg index 04aa4d7..3295a78 100644 --- a/yaffle.ipkg +++ b/yaffle.ipkg @@ -51,7 +51,9 @@ modules = TTImp.ProcessType, TTImp.TTImp, - Utils.Binary + Utils.Binary, + + Yaffle.REPL sourcedir = src executable = yaffle