git.iko.soy/Idris-dev
on master help sign in
Basics of command to execute IO actions in the interpreter
commit82190d338471d61e390886d4d58d2af8bd5c07d9 authorDavid Christiansen <david@davidchristiansen.dk> dateWed 13 Mar 2013, 17:10 (14 years ago) parentab89bf0
4 files changed+40−16
compare with master
unifiedsplit
idris.cabal+1−1 src/Core/Execute.hs+25−3 src/Idris/Help.hs+2−1 src/Idris/REPL.hs+12−11
idris.cabal+1−1
@@ -71,7 +71,7 @@ source-repository head
7171Executable idris
7272 Main-is: Main.hs
7373 hs-source-dirs: src
74− Other-modules: Core.TT, Core.Evaluate, Core.Typecheck,
74+ Other-modules: Core.TT, Core.Evaluate, Core.Execute, Core.Typecheck,
7575 Core.ProofShell, Core.ProofState, Core.CoreParser,
7676 Core.ShellParser, Core.Unify, Core.Elaborate,
7777 Core.CaseTree, Core.Constraints,
src/Core/Execute.hs+25−3
@@ -1,10 +1,32 @@
1−module Core.Execute where
1+module Core.Execute (execute) where
2+
3+import Idris.AbsSyntax
4+import Idris.AbsSyntaxTree
25
36import Core.TT
47import Core.Evaluate
58
9+import Debug.Trace
10+
611-- | Attempt to perform a side effect. Return either Just the next step in
712-- evaluation (after performing the side effect through IO), or Nothing if no
813-- IO was performed.
9−execute :: TT Name -> Idris (Maybe (TT Name))
10−execute tm = Nothing
14+step :: TT Name -> Idris (Maybe (TT Name))
15+step tm = step' (unApply tm)
16+ where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = return $ Just arg
17+ step' (P _ (UN "mkForeign") _, args) = do newTerm <- stepForeign args
18+ return Nothing
19+ step' _ = return Nothing
20+
21+-- | Perform side effects until no more can be performed, then return the
22+-- resulting term (possibly the argument).
23+execute :: TT Name -> Idris (TT Name)
24+execute tm = do stepped <- step tm
25+ case stepped of
26+ Nothing -> return tm
27+ Just tm' -> execute tm'
28+
29+
30+stepForeign :: [TT Name] -> Idris (TT Name)
31+stepForeign args = do iputStrLn $ "FOREIGN CALL" ++ show args
32+ return $ mkApp (P Bound (UN "mkForeign") Erased) args
src/Idris/Help.hs+2−1
@@ -8,7 +8,7 @@ data CmdArg = ExprArg -- ^ The command takes an expression
88 | MetaVarArg -- ^ The command takes a metavariable
99 | NoArg -- ^ No completion yet
1010
11−
11+-- TODO: Merge the second and fourth elements of the following tuples
1212help :: [([String], String, String, CmdArg)]
1313help =
1414 [ (["<expr>"], "", "Evaluate an expression", NoArg),
@@ -26,6 +26,7 @@ help =
2626 ([":rmproof"], "<name>", "Remove proof from proof stack", NameArg),
2727 ([":showproof"], "<name>", "Show proof", NameArg),
2828 ([":proofs"], "", "Show available proofs", NoArg),
29+ ([":x"], "<expr>", "Execute IO actions resulting from an expression using the interpreter", ExprArg),
2930 ([":c",":compile"], "<filename>", "Compile to an executable <filename>", FileArg),
3031 ([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>", FileArg),
3132 ([":exec",":execute"], "", "Compile to an executable and run", NoArg),
src/Idris/REPL.hs+12−11
@@ -23,6 +23,7 @@ import Paths_idris
2323import Util.System
2424
2525import Core.Evaluate
26+import Core.Execute (execute)
2627import Core.ProofShell
2728import Core.TT
2829import Core.Constraints
@@ -180,17 +181,17 @@ process fn (Eval t)
180181 imp <- impShow
181182 iputStrLn (showImp imp (delab ist tm') ++ " : " ++
182183 showImp imp (delab ist ty'))
183−process fn (ExecVal t)
184− = do (tm, ty) <- elabVal toplevel False t
185−-- (PApp fc (PRef fc (NS (UN "print") ["Prelude"]))
186−-- [pexp t])
187− (tmpn, tmph) <- liftIO tempfile
188− liftIO $ hClose tmph
189− t <- target
190− compile t tmpn tm
191− liftIO $ system tmpn
192− return ()
193− where fc = FC "(input)" 0
184+process fn (ExecVal t)
185+ = do ctxt <- getContext
186+ ist <- getIState
187+ (tm, ty) <- elabVal toplevel False t
188+ let tm' = normaliseAll ctxt [] tm
189+ let ty' = normaliseAll ctxt [] ty
190+ res <- execute tm'
191+ imp <- impShow
192+ iputStrLn (showImp imp (delab ist res) ++ " : " ++
193+ showImp imp (delab ist ty'))
194+ return ()
194195process fn (Check (PRef _ n))
195196 = do ctxt <- getContext
196197 ist <- getIState