git.iko.soy/Idris-dev
on master help sign in
Merge remote-tracking branch 'upstream/master'
commit80238b4cc89095c81c3840bcabdcb27683bb0d2b authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 12 Sep 2014, 17:36 (12 years ago) parent0a6feb1aa4702d
6 files changed+72−2
compare with master
unifiedsplit
idris.cabal+4 src/Idris/Core/Execute.hs+6−2 test/interactive005/expected+33 test/interactive005/input+21 test/interactive005/interactive005.idr+3 test/interactive005/run+5
idris.cabal+4
@@ -391,6 +391,10 @@ Extra-source-files:
391391 test/interactive004/input
392392 test/interactive004/*.idr
393393 test/interactive004/expected
394+ test/interactive005/run
395+ test/interactive005/input
396+ test/interactive005/*.idr
397+ test/interactive005/expected
394398
395399 test/io001/run
396400 test/io001/*.idr
src/Idris/Core/Execute.hs+6−2
@@ -60,6 +60,7 @@ data ExecVal = EP NameType Name ExecVal
6060 | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)
6161 | EApp ExecVal ExecVal
6262 | EType UExp
63+ | EUType Universe
6364 | EErased
6465 | EConstant Const
6566 | forall a. EPtr (Ptr a)
@@ -72,6 +73,7 @@ instance Show ExecVal where
7273 show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
7374 show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
7475 show (EType _) = "Type"
76+ show (EUType _) = "UType"
7577 show EErased = "[__]"
7678 show (EConstant c) = show c
7779 show (EPtr p) = "<<ptr " ++ show p ++ ">>"
@@ -102,6 +104,7 @@ toTT (EApp e1 e2) = do e1' <- toTT e1
102104 e2' <- toTT e2
103105 return $ App e1' e2'
104106toTT (EType u) = return $ TType u
107+toTT (EUType u) = return $ UType u
105108toTT EErased = return Erased
106109toTT (EConstant c) = return (Constant c)
107110toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env
@@ -205,6 +208,7 @@ doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
205208doExec env ctxt Erased = return EErased
206209doExec env ctxt Impossible = fail "Tried to execute an impossible case"
207210doExec env ctxt (TType u) = return (EType u)
211+doExec env ctxt (UType u) = return (EUType u)
208212
209213execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
210214execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls
@@ -404,7 +408,7 @@ force = sUN "Force"
404408-- | Look up primitive operations in the global table and transform them into ExecVal functions
405409getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
406410getOp fn [_, _, x] | fn == pbm = Just (return x)
407−getOp fn [EP _ fn' _]
411+getOp fn [EP _ fn' _]
408412 | fn == prs && fn' == pstd =
409413 Just $ do line <- execIO getLine
410414 return (EConstant (Str line))
@@ -548,7 +552,7 @@ foreignFromTT t = case (unApplyV t) of
548552 _ -> trace ("failed to construct ffun") Nothing
549553
550554getFTy :: ExecVal -> Maybe FType
551−getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))
555+getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))
552556 | fi == txt "FIntT" =
553557 case str intTy of
554558 "ITNative" -> Just (FArith (ATInt ITNative))
test/interactive005/expectednew file+33
@@ -0,0 +1,33 @@
1+Type checking ./interactive005.idr
2+3 : Nat
3+Hello, World
4+main : IO ()
5+ This is a docstring
6+
7+Main.main is Total
8+Hello, World
9+Prelude.Basics.id : a -> a
10+Prelude.Basics.id : {a : Type} -> (__pi_arg : a) -> a
11+Prelude.Basics.id : a -> a
12+
13+ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY
14+ EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
15+ IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
16+ PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE
17+ LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
18+ CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
19+ SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
20+ BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
21+ WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
22+ OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
23+ IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
24+
25+main : IO ()
26+ This
27+ is a
28+ docstring
29+
30+main : IO ()
31+ This is a docstring
32+
33+Nat2 : Type
test/interactive005/inputnew file+21
@@ -0,0 +1,21 @@
1+the Nat (1 + 2)
2+:exec
3+:c bytecode hello.bytecode
4+:c c hello
5+:doc main
6+:reload
7+:load interactive005.idr
8+:total main
9+:exec
10+:t id
11+:set showimplicits
12+:t id
13+:unset showimplicits
14+:t id
15+:warranty
16+:consolewidth 10
17+:doc main
18+:consolewidth infinite
19+:doc main
20+:let data Nat2 = Zero | Succ Nat2
21+:t Nat2
test/interactive005/interactive005.idrnew file+3
@@ -0,0 +1,3 @@
1+||| This is a docstring
2+main : IO ()
3+main = putStrLn "Hello, World"
test/interactive005/runnew file+5
@@ -0,0 +1,5 @@
1+#!/usr/bin/env bash
2+idris --quiet interactive005.idr < input
3+rm -f *.ibc
4+rm -f hello.bytecode
5+rm -f hello