edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-24 21:34:36 +03:00
Code Issues Projects Releases Wiki Activity

provide Version command in ide-mode

Browse Source
This commit is contained in:
Arnaud Bailly 2019-08-28 15:30:13 +02:00
parent 558776c4c4
commit 643fc9c4c7
No known key found for this signature in database
GPG Key ID: 389CC2BC5448321E
10 changed files with 95 additions and 51 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile
View File

@ -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

15
src/Idris/CommandLine.idr
View File

@ -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

21
src/Idris/IDEMode/Commands.idr
View File

@ -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])

3
src/Idris/IDEMode/REPL.idr
View File

@ -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} ->

95
src/Idris/REPL.idr
View File

@ -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} ->

1
src/Idris/Syntax.idr
View File

@ -279,6 +279,7 @@ data REPLCmd : Type where
SetLog : Nat -> REPLCmd
Metavars : REPLCmd
Editing : EditCmd -> REPLCmd
ShowVersion : REPLCmd
Quit : REPLCmd
NOP : REPLCmd

2
src/Idris/Version.idr
View File

@ -1,4 +1,4 @@
||| Sets and display version of Idris 2
||| Sets and display version of Idris.
module Idris.Version
import YafflePaths

3
tests/ideMode/ideMode002/expected Normal file
View File

@ -0,0 +1,3 @@
000018(:protocol-version 2 0)
000021(:return (:ok ((0 0 0) (""))) 1)
Alas the file is done, aborting

1
tests/ideMode/ideMode002/input Normal file
View File

@ -0,0 +1 @@
00000c(:version 1)

3
tests/ideMode/ideMode002/run Executable file
View File

@ -0,0 +1,3 @@
$1 --ide-mode < input
rm -rf build