From 643fc9c4c722d098a599be4531247d385b0de413 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Wed, 28 Aug 2019 15:30:13 +0200 Subject: [PATCH] provide Version command in ide-mode --- Makefile | 2 +- src/Idris/CommandLine.idr | 15 +++-- src/Idris/IDEMode/Commands.idr | 21 +++++++ src/Idris/IDEMode/REPL.idr | 3 + src/Idris/REPL.idr | 95 ++++++++++++++++++------------- src/Idris/Syntax.idr | 1 + src/Idris/Version.idr | 2 +- tests/ideMode/ideMode002/expected | 3 + tests/ideMode/ideMode002/input | 1 + tests/ideMode/ideMode002/run | 3 + 10 files changed, 95 insertions(+), 51 deletions(-) create mode 100644 tests/ideMode/ideMode002/expected create mode 100644 tests/ideMode/ideMode002/input create mode 100755 tests/ideMode/ideMode002/run diff --git a/Makefile b/Makefile index df0d144..21621d9 100644 --- a/Makefile +++ b/Makefile @@ -18,7 +18,7 @@ idris2: src/YafflePaths.idr check_version idris --build idris2.ipkg src/YafflePaths.idr: - @echo 'module YafflePaths; export yprefix : String; yprefix = "${PREFIX}"; export yversion : ((Nat,Nat,Nat), String); yversion = ((2,0,0), "alpha")' > src/YafflePaths.idr + @echo 'module YafflePaths; export yprefix : String; yprefix = "${PREFIX}"; export yversion : ((Nat,Nat,Nat), String); yversion = ((0,0,0), "")' > src/YafflePaths.idr prelude: make -C libs/prelude IDRIS2=../../idris2 diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index ea6157a..8959813 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -1,5 +1,9 @@ module Idris.CommandLine +import Data.String +import Idris.Version +import YafflePaths + %default total public export @@ -48,7 +52,7 @@ data CLOpt ||| Whether or not to run in IdeMode (easily parsable for other tools) IdeMode | ||| Whether or not to run IdeMode (using a socket instead of stdin/stdout) - IdeModeSocket | + IdeModeSocket | ||| Run as a checker for the core language TTImp Yaffle String | Timing | @@ -82,7 +86,7 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly] MkOpt ["--ide-mode"] [] [IdeMode] (Just "Run the REPL with machine-readable syntax"), - + MkOpt ["--ide-mode-socket"] [] [IdeModeSocket] (Just "Run the ide socket mode"), @@ -124,13 +128,9 @@ optUsage d showSep sep [x] = x showSep sep (x :: xs) = x ++ sep ++ showSep sep xs -export -version : String -version = "0.0" - export versionMsg : String -versionMsg = "Idris 2, version " ++ version +versionMsg = "Idris 2, version " ++ showVersion version export usage : String @@ -182,4 +182,3 @@ getCmdOpts : IO (Either String (List CLOpt)) getCmdOpts = do (_ :: opts) <- getArgs | pure (Left "Invalid command line") pure $ getOpts opts - diff --git a/src/Idris/IDEMode/Commands.idr b/src/Idris/IDEMode/Commands.idr index b65430a..11adaa8 100644 --- a/src/Idris/IDEMode/Commands.idr +++ b/src/Idris/IDEMode/Commands.idr @@ -75,8 +75,29 @@ getIDECommand (SExpList [SymbolAtom "make-case", IntegerAtom l, StringAtom n]) = Just $ MakeCase l n getIDECommand (SExpList [SymbolAtom "make-with", IntegerAtom l, StringAtom n]) = Just $ MakeWith l n +getIDECommand (SymbolAtom "version") = Just Version getIDECommand _ = Nothing +export +putIDECommand : IDECommand -> SExp +putIDECommand (Interpret cmd) = (SExpList [SymbolAtom "interpret", StringAtom cmd]) +putIDECommand (LoadFile fname Nothing) = (SExpList [SymbolAtom "load-file", StringAtom fname]) +putIDECommand (LoadFile fname (Just line)) = (SExpList [SymbolAtom "load-file", StringAtom fname, IntegerAtom line]) +putIDECommand (TypeOf cmd Nothing) = (SExpList [SymbolAtom "type-of", StringAtom cmd]) +putIDECommand (TypeOf cmd (Just (line, col))) = (SExpList [SymbolAtom "type-of", StringAtom cmd, IntegerAtom line, IntegerAtom col]) +putIDECommand (CaseSplit line col n) = (SExpList [SymbolAtom "case-split", IntegerAtom line, IntegerAtom col, StringAtom n]) +putIDECommand (AddClause line n) = (SExpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n]) +putIDECommand (ExprSearch line n exprs mode) = (SExpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom n, SExpList $ map StringAtom exprs, getMode mode]) + where + getMode : Bool -> SExp + getMode True = SymbolAtom "all" + getMode False = SymbolAtom "other" +putIDECommand (GenerateDef line n) = (SExpList [SymbolAtom "generate-def", IntegerAtom line, StringAtom n]) +putIDECommand (MakeLemma line n) = (SExpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom n]) +putIDECommand (MakeCase line n) = (SExpList [SymbolAtom "make-case", IntegerAtom line, StringAtom n]) +putIDECommand (MakeWith line n) = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n]) +putIDECommand Version = SymbolAtom "version" + export getMsg : SExp -> Maybe (IDECommand, Integer) getMsg (SExpList [cmdexp, IntegerAtom num]) diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 124bd6d..008fbbc 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -185,6 +185,9 @@ process (MakeCase l n) process (MakeWith l n) = do Idris.REPL.process (Editing (MakeWith (fromInteger l) (UN n))) pure () +process Version + = do Idris.REPL.process ShowVersion + pure () processCatch : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 75ad180..0e0a3d5 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -29,6 +29,7 @@ import Idris.Parser import Idris.Resugar import public Idris.REPLCommon import Idris.Syntax +import Idris.Version import TTImp.Elab import TTImp.Elab.Check @@ -48,17 +49,17 @@ import System showInfo : {auto c : Ref Ctxt Defs} -> (Name, Int, GlobalDef) -> Core () -showInfo (n, idx, d) - = do coreLift $ putStrLn (show (fullname d) ++ " ==> " ++ +showInfo (n, idx, d) + = do coreLift $ putStrLn (show (fullname d) ++ " ==> " ++ show !(toFullNames (definition d))) coreLift $ putStrLn (show (multiplicity d)) case compexpr d of Nothing => pure () Just expr => coreLift $ putStrLn ("Compiled: " ++ show expr) - coreLift $ putStrLn ("Refers to: " ++ + coreLift $ putStrLn ("Refers to: " ++ show !(traverse getFullName (keys (refersTo d)))) - when (not (isNil (sizeChange d))) $ - let scinfo = map (\s => show (fnCall s) ++ ": " ++ + when (not (isNil (sizeChange d))) $ + let scinfo = map (\s => show (fnCall s) ++ ": " ++ show (fnArgs s)) !(traverse toFullNames (sizeChange d)) in coreLift $ putStrLn $ "Size change: " ++ showSep ", " scinfo @@ -68,7 +69,7 @@ isHole def = case definition def of Hole locs _ => Just locs _ => Nothing - + showCount : RigCount -> String showCount Rig0 = " 0 " showCount Rig1 = " 1 " @@ -89,14 +90,14 @@ tidy n = show n showEnv : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - Defs -> Env Term vars -> Name -> Nat -> Term vars -> + 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 showCount (multiplicity b) ++ + then showCount (multiplicity b) ++ impBracket (implicitBind b) (tidy x ++ " : " ++ show ity) ++ "\n" else "" (envstr, ret) <- showEnv defs (b :: env) fn args sc @@ -115,12 +116,12 @@ showEnv defs env fn args ty showHole : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - Defs -> Env Term vars -> Name -> Nat -> Term vars -> + 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 + let envs' = if showImplicits pp then envs else dropShadows envs pure (concat (map snd envs') ++ ret) @@ -134,9 +135,9 @@ showHole gam env fn args ty displayType : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - Defs -> (Name, Int, GlobalDef) -> + Defs -> (Name, Int, GlobalDef) -> Core String -displayType defs (n, i, gdef) +displayType defs (n, i, gdef) = maybe (do tm <- resugar [] !(normaliseHoles defs [] (type gdef)) pure (show (fullname gdef) ++ " : " ++ show tm)) (\num => showHole defs [] n num (type gdef)) @@ -152,7 +153,7 @@ getEnvTerm _ env tm = (_ ** (env, tm)) displayTerm : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - Defs -> ClosedTerm -> + Defs -> ClosedTerm -> Core String displayTerm defs tm = do ptm <- resugar [] !(normaliseHoles defs [] tm) @@ -160,7 +161,7 @@ displayTerm defs tm displayPatTerm : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - Defs -> ClosedTerm -> + Defs -> ClosedTerm -> Core String displayPatTerm defs tm = do ptm <- resugarNoPatvars [] !(normaliseHoles defs [] tm) @@ -168,7 +169,7 @@ displayPatTerm defs tm displayClause : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - Defs -> (vs ** (Env Term vs, Term vs, Term vs)) -> + Defs -> (vs ** (Env Term vs, Term vs, Term vs)) -> Core String displayClause defs (vs ** (env, lhs, rhs)) = do lhstm <- resugar env !(normaliseHoles defs env lhs) @@ -177,7 +178,7 @@ displayClause defs (vs ** (env, lhs, rhs)) displayPats : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - Defs -> (Name, Int, GlobalDef) -> + Defs -> (Name, Int, GlobalDef) -> Core String displayPats defs (n, idx, gdef) = case definition gdef of @@ -190,16 +191,16 @@ displayPats defs (n, idx, gdef) setOpt : {auto c : Ref Ctxt Defs} -> {auto o : Ref ROpts REPLOpts} -> REPLOpt -> Core () -setOpt (ShowImplicits t) +setOpt (ShowImplicits t) = do pp <- getPPrint setPPrint (record { showImplicits = t } pp) -setOpt (ShowNamespace t) +setOpt (ShowNamespace t) = do pp <- getPPrint setPPrint (record { fullNamespace = t } pp) -setOpt (ShowTypes t) +setOpt (ShowTypes t) = do opts <- get ROpts put ROpts (record { showTypes = t } opts) -setOpt (EvalMode m) +setOpt (EvalMode m) = do opts <- get ROpts put ROpts (record { evalMode = m } opts) setOpt (Editor e) @@ -211,7 +212,7 @@ setOpt (CG e) Nothing => coreLift $ putStrLn "No such code generator available" findCG : {auto c : Ref Ctxt Defs} -> Core Codegen -findCG +findCG = do defs <- get Ctxt case codegen (session (options defs)) of Chez => pure codegenChez @@ -247,9 +248,9 @@ execExp ctm inidx <- resolveName (UN "[input]") (tm, ty) <- elabTerm inidx InExpr [] (MkNested []) [] ttimp Nothing - tm_erased <- linearCheck replFC Rig1 True [] tm + tm_erased <- linearCheck replFC Rig1 True [] tm execute !findCG tm_erased - + anyAt : (FC -> Bool) -> FC -> a -> Bool anyAt p loc y = p loc @@ -271,7 +272,7 @@ printClause i (ImpossibleClause _ lhsraw) = do lhs <- pterm lhsraw pure (pack (replicate i ' ') ++ show lhs ++ " impossible") -lookupDefTyName : Name -> Context -> +lookupDefTyName : Name -> Context -> Core (List (Name, Int, (Def, ClosedTerm))) lookupDefTyName = lookupNameBy (\g => (definition g, type g)) @@ -294,7 +295,7 @@ processEdit (TypeAt line col name) else printResult res if res == "" then printResult !(showHole defs [] n num t) - else printResult (res ++ "\n\n" ++ "Locally:\n" ++ + else printResult (res ++ "\n\n" ++ "Locally:\n" ++ !(showHole defs [] n num t)) processEdit (CaseSplit line col name) = do let find = if col > 0 @@ -317,25 +318,25 @@ processEdit (ExprSearch line name hints all) do tms <- exprSearch replFC name [] defs <- get Ctxt restms <- traverse (normaliseHoles defs []) tms - itms <- the (Core (List PTerm)) - (traverse (\tm => + itms <- the (Core (List PTerm)) + (traverse (\tm => do let (_ ** (env, tm')) = dropLams locs [] tm resugar env tm') restms) if all then printResult $ showSep "\n" (map show itms) else case itms of [] => printError "No search results" - (x :: xs) => printResult - (show (if brack + (x :: xs) => printResult + (show (if brack then addBracket replFC x else x)) [] => printError $ "Unknown name " ++ show name _ => printError "Not a searchable hole" where - dropLams : Nat -> Env Term vars -> Term vars -> + dropLams : Nat -> Env Term vars -> Term vars -> (vars' ** (Env Term vars', Term vars')) dropLams Z env tm = (_ ** (env, tm)) - dropLams (S k) env (Bind _ _ b sc) = dropLams k (b :: env) sc + dropLams (S k) env (Bind _ _ b sc) = dropLams k (b :: env) sc dropLams _ env tm = (_ ** (env, tm)) processEdit (GenerateDef line name) = do defs <- get Ctxt @@ -343,7 +344,7 @@ processEdit (GenerateDef line name) | Nothing => printError ("Can't find declaration for " ++ show name ++ " on line " ++ show line) case !(lookupDefExact n' (gamma defs)) of Just None => - catch + catch (do Just (fc, cs) <- makeDef (\p, n => onLine line p) n' | Nothing => processEdit (AddClause line name) ls <- traverse (printClause (cast (snd (startPos fc)))) cs @@ -367,7 +368,7 @@ processEdit (MakeLemma line name) case idemode opts of REPL _ => printResult (show name ++ " : " ++ show pty ++ "\n" ++ pappstr) IDEMode i _ f => - send f (SExpList [SymbolAtom "return", + send f (SExpList [SymbolAtom "return", SExpList [SymbolAtom "ok", SExpList [SymbolAtom "metavariable-lemma", SExpList [SymbolAtom "replace-metavariable", @@ -410,7 +411,7 @@ process (Eval itm) = do opts <- get ROpts case evalMode opts of Execute => do execExp itm; pure True - _ => + _ => do ttimp <- desugar AnyExpr [] itm inidx <- resolveName (UN "[input]") (tm, gty) <- elabTerm inidx (emode (evalMode opts)) [] (MkNested []) @@ -500,24 +501,24 @@ process (ProofSearch n_in) coreLift (putStrLn (show itm)) pure True process (Missing n) - = do defs <- get Ctxt + = do defs <- get Ctxt case !(lookupCtxtName n (gamma defs)) of [] => throw (UndefinedName replFC n) ts => do traverse (\fn => do tot <- getTotality replFC fn the (Core ()) $ case isCovering tot of - MissingCases cs => + MissingCases cs => do tms <- traverse (displayPatTerm defs) cs printResult (show fn ++ ":\n" ++ showSep "\n" tms) NonCoveringCall ns_in => do ns <- traverse getFullName ns_in - printResult - (show fn ++ ": Calls non covering function" + printResult + (show fn ++ ": Calls non covering function" ++ case ns of [fn] => " " ++ show fn _ => "s: " ++ showSep ", " (map show ns)) - _ => iputStrLn (show fn ++ ": All cases covered")) + _ => iputStrLn (show fn ++ ": All cases covered")) (map fst ts) pure True process (Total n) @@ -527,7 +528,7 @@ process (Total n) ts => do traverse (\fn => do checkTotal replFC fn tot <- getTotality replFC fn - iputStrLn (show fn ++ " is " ++ show !(toFullNames tot))) + iputStrLn (show fn ++ " is " ++ show !(toFullNames tot))) (map fst ts) pure True process (DebugInfo n) @@ -558,11 +559,23 @@ process (Editing cmd) processEdit cmd setPPrint ppopts pure True -process Quit +process Quit = do iputStrLn "Bye for now!" pure False process NOP = pure True +process ShowVersion + = do opts <- get ROpts + case idemode opts of + REPL _ => iputStrLn $ showVersion version + IDEMode i _ f => do + let MkVersion (maj, min, patch) t = version + send f (SExpList [SymbolAtom "return", + SExpList [SymbolAtom "ok", + SExpList [SExpList (map (IntegerAtom . cast) [maj, min, patch]), + SExpList [ StringAtom $ fromMaybe "" t ]]], + toSExp i]) + pure False processCatch : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index bf2b597..3f8ea7c 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -279,6 +279,7 @@ data REPLCmd : Type where SetLog : Nat -> REPLCmd Metavars : REPLCmd Editing : EditCmd -> REPLCmd + ShowVersion : REPLCmd Quit : REPLCmd NOP : REPLCmd diff --git a/src/Idris/Version.idr b/src/Idris/Version.idr index 3cead36..6cb4945 100644 --- a/src/Idris/Version.idr +++ b/src/Idris/Version.idr @@ -1,4 +1,4 @@ -||| Sets and display version of Idris 2 +||| Sets and display version of Idris. module Idris.Version import YafflePaths diff --git a/tests/ideMode/ideMode002/expected b/tests/ideMode/ideMode002/expected new file mode 100644 index 0000000..8ca347a --- /dev/null +++ b/tests/ideMode/ideMode002/expected @@ -0,0 +1,3 @@ +000018(:protocol-version 2 0) +000021(:return (:ok ((0 0 0) (""))) 1) +Alas the file is done, aborting diff --git a/tests/ideMode/ideMode002/input b/tests/ideMode/ideMode002/input new file mode 100644 index 0000000..47043bb --- /dev/null +++ b/tests/ideMode/ideMode002/input @@ -0,0 +1 @@ +00000c(:version 1) diff --git a/tests/ideMode/ideMode002/run b/tests/ideMode/ideMode002/run new file mode 100755 index 0000000..86bdf71 --- /dev/null +++ b/tests/ideMode/ideMode002/run @@ -0,0 +1,3 @@ +$1 --ide-mode < input + +rm -rf build