idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 04:33:45 +03:00
Code Issues Projects Releases Wiki Activity

Fix REPL execExp and fix "it" (#908)

Browse Source
This commit is contained in:
Michael Messer 2021-01-27 17:14:41 -06:00 committed by GitHub
parent b81b390f20
commit 05c9029b35
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 115 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

77
src/Idris/REPL.idr
View File

@ -7,6 +7,7 @@ import Compiler.ES.Node
import Compiler.ES.Javascript
import Compiler.Common
import Compiler.RefC.RefC
import Compiler.Inline
import Core.AutoSearch
import Core.CaseTree
@ -43,6 +44,7 @@ import Idris.Version
import TTImp.Elab
import TTImp.Elab.Check
import TTImp.Elab.Local
import TTImp.Interactive.CaseSplit
import TTImp.Interactive.ExprSearch
import TTImp.Interactive.GenerateDef
@ -540,6 +542,44 @@ data REPLResult : Type where
Exited : REPLResult
Edited : EditResult -> REPLResult
getItDecls :
{auto o : Ref ROpts REPLOpts} ->
Core (List ImpDecl)
getItDecls
= do opts <- get ROpts
case evalResultName opts of
Nothing => pure []
Just n => pure [ IClaim replFC top Private [] (MkImpTy replFC (UN "it") (Implicit replFC False)), IDef replFC (UN "it") [PatClause replFC (IVar replFC (UN "it")) (IVar replFC n)]]
prepareExp :
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} ->
PTerm -> Core ClosedTerm
prepareExp ctm
= do ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm)
let ttimpWithIt = ILocal replFC !getItDecls ttimp
inidx <- resolveName (UN "[input]")
(tm, ty) <- elabTerm inidx InExpr [] (MkNested [])
[] ttimpWithIt Nothing
tm_erased <- linearCheck replFC linear True [] tm
compileAndInlineAll
pure tm_erased
processLocal : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
{auto e : Ref EST (EState vars)} ->
List ElabOpt ->
NestedNames vars -> Env Term vars ->
List ImpDecl -> (scope : List ImpDecl) ->
Core ()
processLocal {vars} eopts nest env nestdecls_in scope
= localHelper nest env nestdecls_in $ \nest' => traverse_ (processDecl eopts nest' env) scope
export
execExp : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
@ -548,11 +588,7 @@ execExp : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
PTerm -> Core REPLResult
execExp ctm
= do ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm)
inidx <- resolveName (UN "[input]")
(tm, ty) <- elabTerm inidx InExpr [] (MkNested [])
[] ttimp Nothing
tm_erased <- linearCheck replFC linear True [] tm
= do tm_erased <- prepareExp ctm
execute !findCG tm_erased
pure $ Executed ctm
@ -561,6 +597,7 @@ execDecls : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} ->
List PDecl -> Core REPLResult
execDecls decls = do
traverse_ execDecl decls
@ -569,7 +606,9 @@ execDecls decls = do
execDecl : PDecl -> Core ()
execDecl decl = do
i <- desugarDecl [] decl
traverse_ (processDecl [] (MkNested []) []) i
inidx <- resolveName (UN "[defs]")
newRef EST (initEStateSub inidx [] SubRefl)
processLocal [] (MkNested []) [] !getItDecls i
export
compileExp : {auto c : Ref Ctxt Defs} ->
@ -579,11 +618,7 @@ compileExp : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
PTerm -> String -> Core REPLResult
compileExp ctm outfile
= do inidx <- resolveName (UN "[input]")
ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm)
(tm, gty) <- elabTerm inidx InExpr [] (MkNested [])
[] ttimp Nothing
tm_erased <- linearCheck replFC linear True [] tm
= do tm_erased <- prepareExp ctm
ok <- compile !findCG tm_erased outfile
maybe (pure CompilationFailed)
(pure . Compiled)
@ -597,7 +632,9 @@ loadMainFile : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
String -> Core REPLResult
loadMainFile f
= do resetContext
= do opts <- get ROpts
put ROpts (record { evalResultName = Nothing } opts)
resetContext
Right res <- coreLift (readFile f)
| Left err => do setSource ""
pure (ErrorLoadingFile f err)
@ -660,6 +697,7 @@ process (Eval itm)
Execute => do execExp itm; pure (Executed itm)
_ =>
do ttimp <- desugar AnyExpr [] itm
let ttimpWithIt = ILocal replFC !getItDecls ttimp
inidx <- resolveName (UN "[input]")
-- a TMP HACK to prioritise list syntax for List: hide
-- foreign argument lists. TODO: once the new FFI is fully
@ -669,7 +707,7 @@ process (Eval itm)
hide replFC (NS primIONS (UN "Nil")))
(\err => pure ())
(tm, gty) <- elabTerm inidx (emode (evalMode opts)) [] (MkNested [])
[] ttimp Nothing
[] ttimpWithIt Nothing
logTerm "repl.eval" 10 "Elaborated input" tm
defs <- get Ctxt
opts <- get ROpts
@ -678,7 +716,10 @@ process (Eval itm)
logTermNF "repl.eval" 5 "Normalised" [] ntm
itm <- resugar [] ntm
ty <- getTerm gty
addDef (UN "it") (newDef emptyFC (UN "it") top [] ty Private (PMDef defaultPI [] (STerm 0 ntm) (STerm 0 ntm) []))
evalResultName <- DN "it" <$> genName "evalResult"
addDef evalResultName (newDef replFC evalResultName top [] ty Private (PMDef defaultPI [] (STerm 0 ntm) (STerm 0 ntm) []))
addToSave evalResultName
put ROpts (record { evalResultName = Just evalResultName } opts)
if showTypes opts
then do ity <- resugar [] !(norm defs [] ty)
pure (Evaluated itm (Just ity))
@ -692,6 +733,11 @@ process (Eval itm)
REPLEval -> Defs -> Env Term vs -> Term vs -> Core (Term vs)
nfun NormaliseAll = normaliseAll
nfun _ = normalise
process (Check (PRef fc (UN "it")))
= do opts <- get ROpts
case evalResultName opts of
Nothing => throw (UndefinedName fc (UN "it"))
Just n => process (Check (PRef fc n))
process (Check (PRef fc fn))
= do defs <- get Ctxt
case !(lookupCtxtName fn (gamma defs)) of
@ -701,8 +747,9 @@ process (Check (PRef fc fn))
process (Check itm)
= do inidx <- resolveName (UN "[input]")
ttimp <- desugar AnyExpr [] itm
let ttimpWithIt = ILocal replFC !getItDecls ttimp
(tm, gty) <- elabTerm inidx InExpr [] (MkNested [])
[] ttimp Nothing
[] ttimpWithIt Nothing
defs <- get Ctxt
itm <- resugar [] !(normaliseHoles defs [] tm)
ty <- getTerm gty

6
src/Idris/REPLOpts.idr
View File

@ -32,6 +32,7 @@ record REPLOpts where
currentElabSource : String
psResult : Maybe (Name, Core (Search RawImp)) -- last proof search continuation (and name)
gdResult : Maybe (Int, Core (Search (FC, List ImpClause))) -- last generate def continuation (and line number)
evalResultName : Maybe Name
-- TODO: Move extraCodegens from here, it doesn't belong, but there's nowhere
-- better to stick it now.
extraCodegens : List (String, Codegen)
@ -57,11 +58,16 @@ defaultOpts fname outmode cgs
, currentElabSource = ""
, psResult = Nothing
, gdResult = Nothing
, evalResultName = Nothing
, extraCodegens = cgs
, consoleWidth = Nothing
, color = True
, synHighlightOn = True
}
where
litStyle : Maybe String -> Maybe LiterateStyle
litStyle Nothing = Nothing
litStyle (Just fn) = isLitFile fn
export
data ROpts : Type where

26
src/TTImp/Elab/Local.idr
View File

@ -21,17 +21,15 @@ import Data.List
%default covering
export
checkLocal : {vars : _} ->
localHelper : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
{auto e : Ref EST (EState vars)} ->
RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars ->
FC -> List ImpDecl -> (scope : RawImp) ->
(expTy : Maybe (Glued vars)) ->
Core (Term vars, Glued vars)
checkLocal {vars} rig elabinfo nest env fc nestdecls_in scope expty
List ImpDecl -> (NestedNames vars -> Core a) ->
Core a
localHelper {vars} nest env nestdecls_in func
= do est <- get EST
let f = defining est
defs <- get Ctxt
@ -64,7 +62,7 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls_in scope expty
ust <- get UST
put UST (record { delayedElab = olddelayed } ust)
defs <- get Ctxt
res <- check rig elabinfo nest' env scope expty
res <- func nest'
defs <- get Ctxt
put Ctxt (record { localHints = oldhints } defs)
pure res
@ -131,6 +129,20 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls_in scope expty
= INamespace fc ps (map setPublic decls)
setPublic d = d
export
checkLocal : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
{auto e : Ref EST (EState vars)} ->
RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars ->
FC -> List ImpDecl -> (scope : RawImp) ->
(expTy : Maybe (Glued vars)) ->
Core (Term vars, Glued vars)
checkLocal {vars} rig elabinfo nest env fc nestdecls_in scope expty
= localHelper nest env nestdecls_in $ \nest' => check rig elabinfo nest' env scope expty
getLocalTerm : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
FC -> Env Term vars -> Term vars -> List Name ->

2
tests/Main.idr
View File

@ -124,7 +124,7 @@ idrisTests = MkTestPool []
"import001", "import002", "import003", "import004", "import005",
-- Miscellaneous REPL
"interpreter001", "interpreter002", "interpreter003", "interpreter004",
"interpreter005", "interpreter006",
"interpreter005", "interpreter006", "interpreter007",
-- Implicit laziness, lazy evaluation
"lazy001",
-- Namespace blocks

6
tests/idris2/interpreter006/expected
View File

@ -3,5 +3,11 @@ Main> 4
Main> 4
Main> "test"
Main> it : String
Main> it ++ it : String
Main> "test"
Main> 1
Main> Main> Main> 2
Main> 2
Main> 2
Main> Refl
Main> Bye for now!

8
tests/idris2/interpreter006/input
View File

@ -3,5 +3,13 @@ it
it
"test"
:t it
:t it ++ it
it
1
:let f : Integer -> Integer
:let f x = x + it
f 1
f 1
2
the (it === 2) Refl
:q

5
tests/idris2/interpreter007/expected Normal file
View File

@ -0,0 +1,5 @@
foo
foo
bar
Main> Main> Main> Main> Main> "bar"
Main> Main> Bye for now!

7
tests/idris2/interpreter007/input Normal file
View File

@ -0,0 +1,7 @@
:let x : String
:let x = "foo"
:exec putStrLn x
:exec putStrLn x
"bar"
:exec putStrLn it
:q

1
tests/idris2/interpreter007/run Executable file
View File

@ -0,0 +1 @@
$1 --no-color --console-width 0 --no-banner < input