82190d3 · Idris-dev · git.iko.soy

idris.cabal+1−1

compare with master

unifiedsplit

@@ -71,7 +71,7 @@ source-repository head

71Executable idris

72 Main-is: Main.hs

73 hs-source-dirs: src

74− Other-modules: Core.TT, Core.Evaluate, Core.Typecheck,

74+ Other-modules: Core.TT, Core.Evaluate, Core.Execute, Core.Typecheck,

75 Core.ProofShell, Core.ProofState, Core.CoreParser,

76 Core.ShellParser, Core.Unify, Core.Elaborate,

77 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

2

5

3import Core.TT

6import Core.TT

4import Core.Evaluate

7import Core.Evaluate

5

8

9+import Debug.Trace

10+

6-- | Attempt to perform a side effect. Return either Just the next step in

11-- | Attempt to perform a side effect. Return either Just the next step in

7-- evaluation (after performing the side effect through IO), or Nothing if no

12-- evaluation (after performing the side effect through IO), or Nothing if no

8-- IO was performed.

13-- IO was performed.

9−execute :: TT Name -> Idris (Maybe (TT Name))

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

10−execute tm = Nothing

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

8 | MetaVarArg -- ^ The command takes a metavariable

9 | NoArg -- ^ No completion yet

10

11−

11+-- TODO: Merge the second and fourth elements of the following tuples

12help :: [([String], String, String, CmdArg)]

13help =

14 [ (["<expr>"], "", "Evaluate an expression", NoArg),

@@ -26,6 +26,7 @@ help =

26 ([":rmproof"], "<name>", "Remove proof from proof stack", NameArg),

27 ([":showproof"], "<name>", "Show proof", NameArg),

28 ([":proofs"], "", "Show available proofs", NoArg),

29+ ([":x"], "<expr>", "Execute IO actions resulting from an expression using the interpreter", ExprArg),

29 ([":c",":compile"], "<filename>", "Compile to an executable <filename>", FileArg),

30 ([":c",":compile"], "<filename>", "Compile to an executable <filename>", FileArg),

30 ([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>", FileArg),

31 ([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>", FileArg),

31 ([":exec",":execute"], "", "Compile to an executable and run", NoArg),

32 ([":exec",":execute"], "", "Compile to an executable and run", NoArg),

src/Idris/REPL.hs+12−11

@@ -23,6 +23,7 @@ import Paths_idris

23import Util.System

24

25import Core.Evaluate

26+import Core.Execute (execute)

26import Core.ProofShell

27import Core.ProofShell

27import Core.TT

28import Core.TT

28import Core.Constraints

29import Core.Constraints

@@ -180,17 +181,17 @@ process fn (Eval t)

180 imp <- impShow

181 imp <- impShow

181 iputStrLn (showImp imp (delab ist tm') ++ " : " ++

182 iputStrLn (showImp imp (delab ist tm') ++ " : " ++

182 showImp imp (delab ist ty'))

183 showImp imp (delab ist ty'))

183−process fn (ExecVal t)

184+process fn (ExecVal t)

185+ = do ctxt <- getContext

186+ ist <- getIState

184− = do (tm, ty) <- elabVal toplevel False t

187+ (tm, ty) <- elabVal toplevel False t

185−-- (PApp fc (PRef fc (NS (UN "print") ["Prelude"]))

188+ let tm' = normaliseAll ctxt [] tm

186−-- [pexp t])

189+ let ty' = normaliseAll ctxt [] ty

187− (tmpn, tmph) <- liftIO tempfile

190+ res <- execute tm'

188− liftIO $ hClose tmph

191+ imp <- impShow

189− t <- target

192+ iputStrLn (showImp imp (delab ist res) ++ " : " ++

190− compile t tmpn tm

193+ showImp imp (delab ist ty'))

191− liftIO $ system tmpn

192− return ()

194+ return ()

193− where fc = FC "(input)" 0

194process fn (Check (PRef _ n))

195process fn (Check (PRef _ n))

195 = do ctxt <- getContext

196 = do ctxt <- getContext

196 ist <- getIState

197 ist <- getIState