6db701e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'providers-io-rewrite' of https://github.com/david-christiansen/Idris-dev into david-christiansen-providers-io-rewrite

6db701eEdwin Brady14 years ago

.gitignore+4

compare with master

unifiedsplit

@@ -3,6 +3,9 @@ cabal-dev/

3*.ibc

4*.o

5*.a

6+*.so

7+*.dll

8+*.dylib

6*.swp

9*.swp

7*~

10*~

8custom.mk

11custom.mk

@@ -11,3 +14,4 @@ test/test???/output

11test/reg???/output

14test/reg???/output

12test/test???/*.exe

15test/test???/*.exe

13test/reg???/*.exe

16test/reg???/*.exe

17+

Makefile+2−2

@@ -17,8 +17,8 @@ test:

17 make -C test

19relib:

20− make -C lib IDRIS=../dist/build/idris/idris clean

20+ make -C lib IDRIS=../dist/build/idris/idris RTS=../dist/build/rts/libidris_rts clean

21− make -C effects IDRIS=../dist/build/idris/idris clean

21+ make -C effects IDRIS=../dist/build/idris/idris RTS=../dist/build/rts/libidris_rts DIST=../dist/build clean

22 $(CABAL) install $(CABALFLAGS)

24linecount:

Setup.hs+6−3

@@ -28,8 +28,11 @@ mvn verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation "mv

28(<//>) = (Px.</>)

29idrisCmd local = Px.joinPath $ splitDirectories $

30 ".." <//> buildDir local <//> "idris" <//> "idris"

31+rtsDir local = Px.joinPath $ splitDirectories $

32+ ".." <//> buildDir local <//> "rts" <//> "libidris_rts"

31#else

33#else

32idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"

34idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"

35+rtsDir local = ".." </> buildDir local </> "rts" </> "libidris_rts"

33#endif

36#endif

35cleanStdLib verbosity

38cleanStdLib verbosity

@@ -103,9 +106,9 @@ checkStdLib local withoutEffects verbosity

103 ]

106 ]

104 unless withoutEffects $

107 unless withoutEffects $

105 make verbosity

108 make verbosity

106− [ "-C", "effects", "check"

109+ [ "-C", "effects", "check"

107− , "IDRIS=" ++ icmd

110+ , "IDRIS=" ++ icmd

108− ]

111+ ]

109 make verbosity

112 make verbosity

110 [ "-C", "rts", "check"

113 [ "-C", "rts", "check"

111 , "IDRIS=" ++ icmd

114 , "IDRIS=" ++ icmd

config.mk+26

@@ -7,3 +7,29 @@ CABAL :=cabal

7## Disable building of Effects

8#CABALFLAGS :=-f NoEffects

10+

11+MACHINE := $(shell $(CC) -dumpmachine)

12+ifneq (, $(findstring darwin, $(MACHINE)))

13+ OS :=darwin

14+else

15+ifneq (, $(findstring cygwin, $(MACHINE)))

16+ OS :=windows

17+else

18+ifneq (, $(findstring mingw, $(MACHINE)))

19+ OS :=windows

20+else

21+ OS :=unix

22+endif

23+endif

24+endif

25+

26+ifeq ($(OS),darwin)

27+ SHLIB_SUFFIX :=.dylib

28+else

29+ifeq ($(OS),windows)

30+ SHLIB_SUFFIX :=.DLL

31+else

32+ SHLIB_SUFFIX :=.so

33+endif

34+endif

35+

effects/Makefile+1−1

@@ -4,7 +4,7 @@ check: .PHONY

5recheck: clean check

7−install:

7+install:

8 $(IDRIS) --install effects.ipkg

10clean: .PHONY

lib/Providers.idr+4−3

@@ -1,8 +1,9 @@

1module Providers

3public

4−data Provider a = Provide (IO a) | Error (IO String)

4+data Provider a = Provide a | Error String

6partial public

7−unProv : Provider a -> a

7+unProv : IO (Provider a) -> a

8−unProv (Provide x) = unsafePerformIO x

8+unProv p = case unsafePerformIO p of

9+ Provide x => x

rts/Makefile+4−4

@@ -2,15 +2,15 @@ include ../config.mk

3OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_stdfgn.o idris_bitstring.o idris_opts.o idris_stats.o

4HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_stdfgn.h idris_bitstring.h idris_opts.h idris_stats.h

5−CFLAGS = -O2 -Wall

5+CFLAGS = -O2 -Wall -fPIC

7ifneq ($(GMP_INCLUDE_DIR),)

8− CFLAGS += -isystem $(GMP_INCLUDE_DIR)

8+ CFLAGS += -isystem $(GMP_INCLUDE_DIR)

9endif

11LIBTARGET = libidris_rts.a

13−check : $(LIBTARGET)

13+check : $(LIBTARGET) $(DYLIBTARGET)

15$(LIBTARGET) : $(OBJS)

16 ar r $(LIBTARGET) $(OBJS)

@@ -21,7 +21,7 @@ install : .PHONY

21 install $(LIBTARGET) $(HDRS) $(TARGET)

23clean : .PHONY

24− rm -f $(OBJS) $(LIBTARGET)

24+ rm -f $(OBJS) $(LIBTARGET) $(DYLIBTARGET)

26idris_rts.o: idris_rts.h

rts/idris_stdfgn.h−1

@@ -8,7 +8,6 @@ void putStr(char* str);

9void* fileOpen(char* f, char* mode);

10void fileClose(void* h);

11−//char* freadStr(void* h);

12void fputStr(void*h, char* str);

11void fputStr(void*h, char* str);

14int isNull(void* ptr);

13int isNull(void* ptr);

src/Core/CaseTree.hs+4−4

@@ -14,11 +14,11 @@ import Debug.Trace

14data CaseDef = CaseDef [Name] SC [Term]

15 deriving Show

17−data SC' t = Case Name [CaseAlt' t] -- invariant: lowest tags first

17+data SC' t = Case Name [CaseAlt' t] -- ^ invariant: lowest tags first

18− | ProjCase t [CaseAlt' t] -- special case for projections

18+ | ProjCase t [CaseAlt' t] -- ^ special case for projections

19 | STerm t

20− | UnmatchedCase String -- error message

20+ | UnmatchedCase String -- ^ error message

21− | ImpossibleCase -- already checked to be impossible

21+ | ImpossibleCase -- ^ already checked to be impossible

22 deriving (Eq, Ord, Functor)

23{-!

24deriving instance Binary SC

src/Core/Evaluate.hs+2−2

@@ -9,7 +9,7 @@ module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

9 addDatatype, addCasedef, simplifyCasedef, addOperator,

10 lookupNames, lookupTy, lookupP, lookupDef, lookupVal,

11 lookupTotal, lookupTyEnv, isConName, isFnName,

12− Value(..)) where

12+ Value(..), Quote(..), evalState, initEval) where

14import Debug.Trace

15import Control.Monad.State

@@ -669,7 +669,7 @@ data Context = MkContext {

669 uconstraints :: [UConstraint],

670 next_tvar :: Int,

671 definitions :: Ctxt (Def, Accessibility, Totality)

672− }

672+ } deriving Show

673

674-- | The initial empty context

675initContext = MkContext [] 0 emptyContext

src/Core/Execute.hs+438−76

@@ -1,3 +1,4 @@

1+{-# LANGUAGE PatternGuards, ExistentialQuantification #-}

1module Core.Execute (execute) where

2module Core.Execute (execute) where

3import Idris.AbsSyntax

4import Idris.AbsSyntax

@@ -5,104 +6,456 @@ import Idris.AbsSyntaxTree

6import Core.TT

7import Core.TT

7import Core.Evaluate

8import Core.Evaluate

9+import Core.CaseTree

9import Debug.Trace

11import Debug.Trace

11import Util.DynamicLinker

13import Util.DynamicLinker

14+import Util.System

13import Control.Applicative hiding (Const)

16import Control.Applicative hiding (Const)

14import Control.Monad.Trans

17import Control.Monad.Trans

18+import Control.Monad.Trans.State.Strict

19+import Control.Monad.Trans.Error

15import Control.Monad

20import Control.Monad

16import Data.Maybe

21import Data.Maybe

22+import qualified Data.Map as M

18import Foreign.LibFFI

24import Foreign.LibFFI

19import Foreign.C.String

25import Foreign.C.String

20import Foreign.Marshal.Alloc (free)

26import Foreign.Marshal.Alloc (free)

27+import Foreign.Ptr

28+

29+import System.IO

30+

31+

32+data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show

33+

34+data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs

35+ , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness

36+ , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad

37+ , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad

38+ }

39+

40+data ExecVal = EP NameType Name ExecVal

41+ | EV Int

42+ | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)

43+ | EApp ExecVal ExecVal

44+ | EType UExp

45+ | EErased

46+ | EConstant Const

47+ | forall a. EPtr (Ptr a)

48+ | EThunk Int

49+ | EHandle Handle

50+

51+instance Show ExecVal where

52+ show (EP _ n _) = show n

53+ show (EV i) = "!!V" ++ show i ++ "!!"

54+ show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"

55+ show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"

56+ show (EType _) = "Type"

57+ show EErased = "[__]"

58+ show (EConstant c) = show c

59+ show (EPtr p) = "<<ptr " ++ show p ++ ">>"

60+ show (EThunk i) = "<<thunk " ++ show i ++ ">>"

61+ show (EHandle h) = "<<handle " ++ show h ++ ">>"

62+

63+toTT :: ExecVal -> Exec Term

64+toTT (EP nt n ty) = (P nt n) <$> (toTT ty)

65+toTT (EV i) = return $ V i

66+toTT (EBind n b body) = do body' <- body $ EP Bound n EErased

67+ b' <- fixBinder b

68+ Bind n b' <$> toTT body'

69+ where fixBinder (Lam t) = Lam <$> toTT t

70+ fixBinder (Pi t) = Pi <$> toTT t

71+ fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

72+ fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

73+ fixBinder (Hole t) = Hole <$> toTT t

74+ fixBinder (GHole t) = GHole <$> toTT t

75+ fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2

76+ fixBinder (PVar t) = PVar <$> toTT t

77+ fixBinder (PVTy t) = PVTy <$> toTT t

78+toTT (EApp e1 e2) = do e1' <- toTT e1

79+ e2' <- toTT e2

80+ return $ App e1' e2'

81+toTT (EType u) = return $ TType u

82+toTT EErased = return Erased

83+toTT (EConstant c) = return (Constant c)

84+toTT (EThunk i) = return (P (DCon 0 0) (MN i "THUNK") Erased) --(force i) >>= toTT

85+toTT (EHandle _) = return Erased

86+

87+unApplyV :: ExecVal -> (ExecVal, [ExecVal])

88+unApplyV tm = ua [] tm

89+ where ua args (EApp f a) = ua (a:args) f

90+ ua args t = (t, args)

91+

92+mkEApp :: ExecVal -> [ExecVal] -> ExecVal

93+mkEApp f [] = f

94+mkEApp f (a:args) = mkEApp (EApp f a) args

95+

96+initState :: Idris ExecState

97+initState = do ist <- getIState

98+ return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)

99+

100+type Exec = ErrorT String (StateT ExecState IO)

101+

102+runExec :: Exec a -> ExecState -> IO (Either String a)

103+runExec ex st = fst <$> runStateT (runErrorT ex) st

104+

105+getExecState :: Exec ExecState

106+getExecState = lift get

107+

108+putExecState :: ExecState -> Exec ()

109+putExecState = lift . put

110+

111+execFail :: String -> Exec a

112+execFail = throwError

113+

114+execIO :: IO a -> Exec a

115+execIO = lift . lift

116+

117+delay :: ExecEnv -> Context -> Term -> Exec ExecVal

118+delay env ctxt tm =

119+ do st <- getExecState

120+ let i = exec_next_thunk st

121+ putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)

122+ , exec_next_thunk = exec_next_thunk st + 1

123+ }

124+ return $ EThunk i

125+

126+force :: Int -> Exec ExecVal

127+force i = do st <- getExecState

128+ case M.lookup i (exec_thunks st) of

129+ Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm

130+ case tm' of

131+ EThunk i ->

132+ do res <- force i

133+ update res i

134+ return res

135+ _ -> do update tm' i

136+ return tm'

137+ Just (Forced tm) -> return tm

138+ Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"

139+ where update :: ExecVal -> Int -> Exec ()

140+ update tm i = do est <- getExecState

141+ putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }

142+

143+tryForce :: ExecVal -> Exec ExecVal

144+tryForce (EThunk i) = force i

145+tryForce tm = return tm

146+

147+debugThunks :: Exec ()

148+debugThunks = do st <- getExecState

149+ execIO $ putStrLn (take 4000 (show (exec_thunks st)))

150+

151+execute :: Term -> Idris Term

152+execute tm = do est <- initState

153+ ctxt <- getContext

154+ res <- lift $ flip runExec est $ do res <- doExec [] ctxt tm

155+ toTT res

156+ case res of

157+ Left err -> fail err

158+ Right tm' -> return tm'

159+

160+ioWrap :: ExecVal -> ExecVal

161+ioWrap tm = mkEApp (EP (DCon 0 2) (UN "prim__IO") EErased) [EErased, tm]

162+

163+ioUnit :: ExecVal

164+ioUnit = ioWrap (EP Ref unitCon EErased)

165+

166+type ExecEnv = [(Name, ExecVal)]

167+

168+doExec :: ExecEnv -> Context -> Term -> Exec ExecVal

169+doExec env ctxt p@(P Ref n ty) =

170+ do let val = lookupDef n ctxt

171+ case val of

172+ [Function _ tm] -> doExec env ctxt tm

173+ [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def

174+ [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later

175+ [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun

176+ doExec env ctxt tm

177+ [CaseOp _ _ _ _ _ ns sc _ _] -> return (EP Ref n EErased)

178+ thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined

179+doExec env ctxt p@(P Bound n ty) =

180+ case lookup n env of

181+ Nothing -> execFail "not found"

182+ Just tm -> return tm

183+doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)

184+doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)

185+doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))

186+ | otherwise = execFail "env too small"

187+doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v

188+ doExec ((n, v'):env) ctxt body

189+doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined

190+doExec env ctxt tm@(Bind n b body) = return $

191+ EBind n (fmap (\_->EErased) b)

192+ (\arg -> doExec ((n, arg):env) ctxt body)

193+doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)

194+doExec env ctxt (Constant c) = return (EConstant c)

195+doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in

196+ doExec env ctxt ((x:xs) !! i)

197+doExec env ctxt Erased = return EErased

198+doExec env ctxt Impossible = fail "Tried to execute an impossible case"

199+doExec env ctxt (TType u) = return (EType u)

200+

201+execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal

202+execApp env ctxt (f, args) = do newF <- doExec env ctxt f

203+ laziness <- (++ repeat False) <$> (getLaziness newF)

204+ newArgs <- mapM argExec (zip args laziness)

205+ execApp' env ctxt newF newArgs

206+ where getLaziness (EP _ (UN "lazy") _) = return [False, True]

207+ getLaziness (EP _ n _) = do est <- getExecState

208+ let argInfo = exec_implicits est

209+ case lookupCtxtName n argInfo of

210+ [] -> return (repeat False)

211+ [ps] -> return $ map lazyarg (snd ps)

212+ many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)

213+ getLaziness _ = return (repeat False) -- ok due to zip above

214+ argExec :: (Term, Bool) -> Exec ExecVal

215+ argExec (tm, False) = doExec env ctxt tm

216+ argExec (tm, True) = delay env ctxt tm

217+

218+

219+execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal

220+execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls

221+execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =

222+ execApp' env ctxt v rest

223+

224+execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =

225+ do v'' <- tryForce v'

226+ res <- execApp' env ctxt k [v''] >>= tryForce

227+ execApp' env ctxt res rest

228+execApp' env ctxt con@(EP _ (UN "io_return") _) args@(tp:v:rest) =

229+ do v' <- tryForce v

230+ execApp' env ctxt (mkEApp con [tp, v']) rest

231+

232+-- Special cases arising from not having access to the C RTS in the interpreter

233+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)

234+ | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)

235+ execApp' env ctxt ioUnit rest

236+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

237+ | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do m <- case mode of

238+ "r" -> return ReadMode

239+ "w" -> return WriteMode

240+ "a" -> return AppendMode

241+ "rw" -> return ReadWriteMode

242+ "wr" -> return ReadWriteMode

243+ "r+" -> return ReadWriteMode

244+ _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)

245+ h <- execIO $ openFile f m

246+ execApp' env ctxt (ioWrap (EHandle h)) rest

247+

248+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)

249+ | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do eofp <- execIO $ hIsEOF h

250+ let res = ioWrap (EConstant (I $ if eofp then 1 else 0))

251+ execApp' env ctxt res rest

252+

253+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)

254+ | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do execIO $ hClose h

255+ execApp' env ctxt ioUnit rest

256+

257+

258+execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun _ argTs retT) <- foreignFromTT fn

259+ , length xs >= length argTs =

260+ do res <- stepForeign (ty:fn:take (length argTs) xs)

261+ case res of

262+ Nothing -> fail "Could not call foreign function"

263+ Just r -> return (mkEApp r (drop (length argTs) xs))

264+ | otherwise = return (mkEApp f args)

265+

266+execApp' env ctxt f@(EP _ n _) args =

267+ do let val = lookupDef n ctxt

268+ case val of

269+ [Function _ tm] -> fail "should already have been eval'd"

270+ [TyDecl nt ty] -> return $ mkEApp f args

271+ [Operator tp arity op] ->

272+ if length args >= arity

273+ then do args' <- mapM tryForce $ take arity args

274+ case getOp n args' of

275+ Just res -> do r <- res

276+ execApp' env ctxt r (drop arity args)

277+ Nothing -> return (mkEApp f args)

278+ else return (mkEApp f args)

279+ [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun

280+ do rhs <- doExec env ctxt tm

281+ execApp' env ctxt rhs args

282+ [CaseOp _ _ _ _ _ ns sc _ _] ->

283+ do res <- execCase env ctxt ns sc args

284+ return $ fromMaybe (mkEApp f args) res

285+ thing -> return $ mkEApp f args

286+ where getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

287+ getOp (UN "prim__addInt") [EConstant (I i1), EConstant (I i2)] =

288+ primRes I (i1 + i2)

289+ getOp (UN "prim__charToInt") [EConstant (Ch c)] =

290+ primRes I (fromEnum c)

291+ getOp (UN "prim__concat") [EConstant (Str s1), EConstant (Str s2)] =

292+ primRes Str (s1 ++ s2)

293+ getOp (UN "prim__eqChar") [EConstant (Ch c1), EConstant (Ch c2)] =

294+ primResBool (c1 == c2)

295+ getOp (UN "prim__eqInt") [EConstant (I i1), EConstant (I i2)] =

296+ primResBool (i1 == i2)

297+ getOp (UN "prim__eqString") [EConstant (Str s1), EConstant (Str s2)] =

298+ primResBool (s1 == s2)

299+ getOp (UN "prim__intToFloat") [EConstant (I i)] =

300+ primRes Fl (fromRational (toRational i))

301+ getOp (UN "prim__intToStr") [EConstant (I i)] =

302+ primRes Str (show i)

303+ getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =

304+ primResBool (i1 < i2)

305+ getOp (UN "prim__mulBigInt") [EConstant (BI i1), EConstant (BI i2)] =

306+ primRes BI (i1 * i2)

307+ getOp (UN "prim__mulFloat") [EConstant (Fl i1), EConstant (Fl i2)] =

308+ primRes Fl (i1 * i2)

309+ getOp (UN "prim__mulInt") [EConstant (I i1), EConstant (I i2)] =

310+ primRes I (i1 * i2)

311+ getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =

312+ Just $ do line <- execIO getLine

313+ return (EConstant (Str line))

314+ getOp (UN "prim__readString") [EHandle h] =

315+ Just $ do contents <- execIO $ hGetLine h

316+ return (EConstant (Str contents))

317+ getOp (UN "prim__strCons") [EConstant (Ch c), EConstant (Str s)] =

318+ primRes Str (c:s)

319+ getOp (UN "prim__strHead") [EConstant (Str (c:s))] =

320+ primRes Ch c

321+ getOp (UN "prim__strRev") [EConstant (Str s)] =

322+ primRes Str (reverse s)

323+ getOp (UN "prim__strTail") [EConstant (Str (c:s))] =

324+ primRes Str s

325+ getOp (UN "prim__subFloat") [EConstant (Fl i1), EConstant (Fl i2)] =

326+ primRes Fl (i1 - i2)

327+ getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =

328+ primRes I (i1 - i2)

329+ getOp n args = trace ("No prim " ++ show n ++ " for " ++ take 1000 (show args)) Nothing

330+

331+ primRes :: (a -> Const) -> a -> Maybe (Exec ExecVal)

332+ primRes constr = Just . return . EConstant . constr

333+

334+ primResBool :: Bool -> Maybe (Exec ExecVal)

335+ primResBool b = primRes I (if b then 1 else 0)

336+

337+execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg

338+ let (f', as) = unApplyV ret

339+ execApp' env ctxt f' (as ++ args)

340+execApp' env ctxt (EThunk i) args = do f <- force i

341+ execApp' env ctxt f args

342+execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)

343+execApp' env ctxt f args = return (mkEApp f args)

344+

345+

346+

347+

348+

349+-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,

350+-- evaluates them, then begins the checks for matching cases.

351+execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)

352+execCase env ctxt ns sc args =

353+ let arity = length ns in

354+ if arity <= length args

355+ then do let amap = zip ns args

356+ caseRes <- execCase' env ctxt amap sc

357+ case caseRes of

358+ Just res -> Just <$> execApp' (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)

359+ Nothing -> return Nothing

360+ else return Nothing

361+

362+-- | Take bindings and a case tree and examines them, executing the matching case if possible.

363+execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)

364+execCase' env ctxt amap (UnmatchedCase _) = return Nothing

365+execCase' env ctxt amap (STerm tm) =

366+ Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm

367+execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =

368+ do tm' <- tryForce tm

369+ case chooseAlt tm' alts of

370+ Just (newCase, newBindings) ->

371+ let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

372+ execCase' env ctxt amap' newCase

373+ Nothing -> return Nothing

374+

375+chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])

376+chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])

377+chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])

378+chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm

379+ , cn == n = Just (sc, zip ns args)

380+ | otherwise = chooseAlt tm alts

381+chooseAlt tm (_:alts) = chooseAlt tm alts

382+chooseAlt _ [] = Nothing

383

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

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

24−-- IO was performed.

25−--

26−-- This function is exceedingly generous about what it will accept in order to

27−-- enable convenient testing at the REPL.

28−step :: TT Name -> Idris (Maybe (TT Name))

29−step tm = step' (unApply tm)

30− where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = step arg -- Only step if arg can be stepped

31− step' (P _ (UN "mkForeign") _, args) = stepForeign args

32− step' (P _ (UN "prim__IO") _, [_, arg]) = return (Just arg)

33− step' (P _ (UN "prim__readString") _, [(P _ (UN "prim__stdin") _)]) =

34− do line <- lift $ getLine

35− return . Just . Constant . Str $ line

36− step' _ = return Nothing

37−

38−-- | Perform side effects until no more can be performed, then return the

39−-- resulting term (possibly the argument).

40−execute :: TT Name -> Idris (TT Name)

41−execute tm = case unApply tm of

42− (P _ (UN "unsafePerformIO") _, [_, arg] ) -> execute' arg

43− _ -> return tm

44− where execute' tm = do stepped <- step tm

45− case stepped of

46− Nothing -> return tm

47− Just tm' -> execute' tm'

384

385

386

388

389+idrisType :: FTy -> ExecVal

390+idrisType FUnit = EP Ref unitTy EErased

391+idrisType ft = EConstant (idr ft)

392+ where idr FInt = IType

393+ idr FFloat = FlType

394+ idr FChar = ChType

395+ idr FString = StrType

396+ idr FPtr = PtrType

397+

53data Foreign = FFun String [FTy] FTy deriving Show

398data Foreign = FFun String [FTy] FTy deriving Show

399

400+

55−call :: Foreign -> [TT Name] -> Idris (Maybe (TT Name))

401+call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)

56−call (FFun name argTypes retType) args = do fn <- findForeign name

402+call (FFun name argTypes retType) args =

403+ do fn <- findForeign name

57− case fn of

404+ case fn of

58− Nothing -> return Nothing

405+ Nothing -> return Nothing

59− Just f -> return . Just =<< call' f args retType

406+ Just f -> do res <- call' f args retType

407+ return . Just . ioWrap $ res

60− where call' :: ForeignFun -> [TT Name] -> FTy -> Idris (TT Name)

408+ where call' :: ForeignFun -> [ExecVal] -> FTy -> Exec ExecVal

61− call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)

409+ call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)

62− return (Constant (I (fromIntegral res)))

410+ return (EConstant (I (fromIntegral res)))

63− call' (Fun _ h) args FFloat = do res <- lift $ callFFI h retCDouble (prepArgs args)

411+ call' (Fun _ h) args FFloat = do res <- execIO $ callFFI h retCDouble (prepArgs args)

64− return (Constant (Fl (realToFrac res)))

412+ return (EConstant (Fl (realToFrac res)))

65− call' (Fun _ h) args FChar = do res <- lift $ callFFI h retCChar (prepArgs args)

413+ call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)

66− return (Constant (Ch (castCCharToChar res)))

414+ return (EConstant (Ch (castCCharToChar res)))

67− call' (Fun _ h) args FString = do res <- lift $ callFFI h retCString (prepArgs args)

415+ call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)

68− hStr <- lift $ peekCString res

416+ hStr <- execIO $ peekCString res

69-- lift $ free res

417-- lift $ free res

70− return (Constant (Str hStr))

418+ return (EConstant (Str hStr))

71−-- awaiting Const constructor for pointers

419+

72−-- call' (Fun _ h) args FPtr = do res <- lift $ callFFI h retPtr (prepArgs args)

420+ call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)

73−-- return (Constant (Ch (castCCharToChar res)))

421+ return (EPtr res)

74− call' (Fun _ h) args FUnit = do res <- lift $ callFFI h retVoid (prepArgs args)

422+ call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)

75− return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level

423+ return (EP Ref unitCon EErased)

424+-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)

425+

426

77 prepArgs = map prepArg

427 prepArgs = map prepArg

78− prepArg (Constant (I i)) = argCInt (fromIntegral i)

428+ prepArg (EConstant (I i)) = argCInt (fromIntegral i)

79− prepArg (Constant (Fl f)) = argCDouble (realToFrac f)

429+ prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)

80− prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars

430+ prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars

81− prepArg (Constant (Str s)) = argString s

431+ prepArg (EConstant (Str s)) = argString s

432+ prepArg (EPtr p) = argPtr p

433+ prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined

434

435

436

85−foreignFromTT :: TT Name -> Maybe Foreign

437+foreignFromTT :: ExecVal -> Maybe Foreign

86−foreignFromTT t = case (unApply t) of

438+foreignFromTT t = case (unApplyV t) of

87− (_, [(Constant (Str name)), args, ret]) ->

439+ (_, [(EConstant (Str name)), args, ret]) ->

88− do argTy <- unList args

440+ do argTy <- unEList args

89 argFTy <- sequence $ map getFTy argTy

441 argFTy <- sequence $ map getFTy argTy

90 retFTy <- getFTy ret

442 retFTy <- getFTy ret

91 return $ FFun name argFTy retFTy

443 return $ FFun name argFTy retFTy

92− _ -> Nothing

444+ _ -> trace "failed to construct ffun" Nothing

93−

445+

94−getFTy :: TT Name -> Maybe FTy

446+getFTy :: ExecVal -> Maybe FTy

95−getFTy (P _ (UN t) _) = case t of

447+getFTy (EP _ (UN t) _) =

448+ case t of

96− "FInt" -> Just FInt

449+ "FInt" -> Just FInt

97− "FFloat" -> Just FFloat

450+ "FFloat" -> Just FFloat

98− "FChar" -> Just FChar

451+ "FChar" -> Just FChar

99− "FString" -> Just FString

452+ "FString" -> Just FString

100− "FPtr" -> Just FPtr

453+ "FPtr" -> Just FPtr

101− "FUnit" -> Just FUnit

454+ "FUnit" -> Just FUnit

102− _ -> Nothing

455+ _ -> Nothing

103getFTy _ = Nothing

456getFTy _ = Nothing

104

457

105−unList :: TT Name -> Maybe [TT Name]

458+unList :: Term -> Maybe [Term]

106unList tm = case unApply tm of

459unList tm = case unApply tm of

107 (nil, [_]) -> Just []

460 (nil, [_]) -> Just []

108 (cons, ([_, x, xs])) ->

461 (cons, ([_, x, xs])) ->

@@ -110,11 +463,20 @@ unList tm = case unApply tm of

110 return $ x:rest

463 return $ x:rest

111 (f, args) -> Nothing

464 (f, args) -> Nothing

112

465

466+unEList :: ExecVal -> Maybe [ExecVal]

467+unEList tm = case unApplyV tm of

468+ (nil, [_]) -> Just []

469+ (cons, ([_, x, xs])) ->

470+ do rest <- unEList xs

471+ return $ x:rest

472+ (f, args) -> Nothing

473+

474+

113−toConst :: TT Name -> Maybe Const

475+toConst :: Term -> Maybe Const

114toConst (Constant c) = Just c

476toConst (Constant c) = Just c

115toConst _ = Nothing

477toConst _ = Nothing

116

478

117−stepForeign :: [TT Name] -> Idris (Maybe (TT Name))

479+stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)

118stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn

480stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn

119 f' <- case (call <$> ffun) of

481 f' <- case (call <$> ffun) of

120 Just f -> f args

482 Just f -> f args

@@ -130,15 +492,15 @@ mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs

130 Just x'' -> return (x'':rest)

492 Just x'' -> return (x'':rest)

131 Nothing -> return rest

493 Nothing -> return rest

132

494

133−findForeign :: String -> Idris (Maybe ForeignFun)

495+findForeign :: String -> Exec (Maybe ForeignFun)

134−findForeign fn = do i <- getIState

496+findForeign fn = do est <- getExecState

135− let libs = idris_dynamic_libs i

497+ let libs = exec_dynamic_libs est

136− fns <- mapMaybeM (lift . tryLoadFn fn) libs

498+ fns <- mapMaybeM getFn libs

137 case fns of

499 case fns of

138 [f] -> return (Just f)

500 [f] -> return (Just f)

139− [] -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" not found"

501+ [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"

140 return Nothing

502 return Nothing

141− fs -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++

503+ fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++

142− show (length fs) ++ " occurrences."

504+ show (length fs) ++ " occurrences."

143 return Nothing

505 return Nothing

144−

506+ where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)

src/Core/TT.hs+4−1

@@ -430,7 +430,10 @@ instance Show UConstraint where

430

431type UCs = (Int, [UConstraint])

432

433−data NameType = Bound | Ref | DCon Int Int | TCon Int Int

433+data NameType = Bound

434+ | Ref

435+ | DCon Int Int -- ^ Data constructor; Ints are tag and arity

436+ | TCon Int Int -- ^ Type constructor; Ints are tag and arity

434 deriving (Show, Ord)

437 deriving (Show, Ord)

435{-!

438{-!

436deriving instance Binary NameType

439deriving instance Binary NameType

src/IRTS/CodegenC.hs+1−1

@@ -47,7 +47,7 @@ codegenC defs out exec incs objs libs dbg

47 incFlags <- getIncFlags

48 let gcc = comp ++ " " ++

49 gccDbg dbg ++

50− " -I. " ++ objs ++ " -x c " ++

50+ " -I. " ++ objs ++ " -x c " ++

51 (if (exec == Executable) then "" else " -c ") ++

52 " " ++ tmpn ++

53 " " ++ libFlags ++

src/Idris/ElabDecls.hs+3−3

@@ -223,11 +223,11 @@ elabProvider info syn fc n ty tm

223 " as " ++ show using

224 (e', et) <- elabVal toplevel False using

225 ctxt <- getContext

226− let e'' = normaliseAll ctxt [] e'

226+ let str = show e' in

227− logLvl 1 $ "Term is " ++ show e''

227+ logLvl 1 $ "Term is " ++ if length str > 200 then (take 200 str) ++ "..." else str

228 let et' = normaliseAll ctxt [] et

229 elabType info syn "" fc [] n ty

230− rhs <- execute e''

230+ rhs <- execute e'

231 logLvl 1 $ "Normalized " ++ show n ++ "'s RHS to " ++ show rhs

232 providerError rhs

233 elabClauses info fc [] n [PClause fc n (PRef fc $ n) [] (delab i rhs) []]

src/Idris/Providers.hs+7−13

@@ -1,3 +1,4 @@

1+{-# LANGUAGE PatternGuards #-}

1module Idris.Providers where

2module Idris.Providers where

3import Core.TT

4import Core.TT

@@ -19,16 +20,9 @@ unProv fc tm = PApp fc (PRef fc $ NS (UN "unProv") ["Providers"]) [PExp 0 False

20-- | Handle an error, if the type provider returned an error. Otherwise do nothing.

21-- | Handle an error, if the type provider returned an error. Otherwise do nothing.

21providerError :: TT Name -> Idris ()

22providerError :: TT Name -> Idris ()

22−providerError tm = case unApply tm of

23+providerError tm | (P _ unProv_case _, _:_:tm':_) <- unApply tm

23− (P _ (NS (UN "unProv") ["Providers"]) _, [_, tm']) ->

24− case unApply tm' of

25− (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) ->

24+ , (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) <- unApply tm' =

26− do str <- execute err

27− case (unApply str) of

25+ case err of

28− (Constant (Str msg), []) ->

29− ierror . ProviderError $ msg

30− (P _ (UN "prim__IO") _, [_, (Constant (Str msg))]) ->

31− ierror . ProviderError $ msg

26+ Constant (Str msg) -> ierror . ProviderError $ msg

32− _ -> fail "Error in type provider."

27+ _ -> fail "Error in type provider"

33− _ -> return ()

34− _ -> return ()

28+ | otherwise = return ()

src/Idris/REPL.hs+4−3

@@ -196,9 +196,9 @@ process fn (ExecVal t)

196 = do ctxt <- getContext

197 ist <- getIState

198 (tm, ty) <- elabVal toplevel False t

199− let tm' = normaliseAll ctxt [] tm

199+-- let tm' = normaliseAll ctxt [] tm

200 let ty' = normaliseAll ctxt [] ty

201− res <- execute tm'

201+ res <- execute tm

202 imp <- impShow

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

204 showImp imp (delab ist ty'))

@@ -561,6 +561,7 @@ idrisMain opts =

561 [] -> setIBCSubDir ""

562 (d:_) -> setIBCSubDir d

563 setImportDirs importdirs

564+

564 addPkgDir "base"

565 addPkgDir "base"

565 mapM_ addPkgDir pkgdirs

566 mapM_ addPkgDir pkgdirs

566 elabPrims

567 elabPrims

@@ -645,7 +646,7 @@ getLanguageExt (Extension e) = Just e

645getLanguageExt _ = Nothing

646getLanguageExt _ = Nothing

646

647

647opt :: (Opt -> Maybe a) -> [Opt] -> [a]

648opt :: (Opt -> Maybe a) -> [Opt] -> [a]

648−opt = mapMaybe

649+opt = mapMaybe

649

650

650ver = showVersion version

651ver = showVersion version

651

652

src/Main.hs+3

@@ -29,6 +29,7 @@ import Idris.Imports

29import Idris.Error

31import Util.System ( getLibFlags, getIdrisLibDir, getIncFlags )

32+import Util.DynamicLinker

33import Pkg.Package

34import Pkg.Package

@@ -94,3 +95,5 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

94 "\t--link Show C library directories and exit (for C linking)\n" ++

95 "\t--link Show C library directories and exit (for C linking)\n" ++

95 "\t--include Show C include directories and exit (for C linking)\n" ++

96 "\t--include Show C include directories and exit (for C linking)\n" ++

96 "\t--target [target] Type the target: C, Java, bytecode, javascript, node\n"

97 "\t--target [target] Type the target: C, Java, bytecode, javascript, node\n"

98+

99+

src/Util/System.hs+1−1

@@ -1,7 +1,7 @@

1{-# LANGUAGE CPP #-}

2module Util.System(tempfile,withTempdir,environment,getCC,

3 getLibFlags,getIdrisLibDir,getIncFlags,rmFile,

4− getMvn,getExecutablePom) where

4+ getMvn,getExecutablePom,catchIO) where

6-- System helper functions.

7import Control.Monad (when)

test/README+4

@@ -22,5 +22,9 @@ Tests:

22020: implicit conversions

23021: effects

24022: dynamic C library loading and interpreter IO

25+023: trivial (non-I/O) type providers

26+024: interpreter I/O

27+025: memory effects

28+026: simple file-I/O-based type provider

26regxxx: various regression tests

30regxxx: various regression tests

test/test023/test023.idr+4−4

@@ -7,8 +7,8 @@ import Providers

7%language TypeProviders

9-- Provide the Unit type

10−goodProvider : Provider Type

10+goodProvider : IO (Provider Type)

11−goodProvider = Provide (return (the Type ()))

11+goodProvider = return (Provide (the Type ()))

13%provide (Unit : Type) with goodProvider

@@ -16,8 +16,8 @@ foo : Unit

16foo = ()

18-- Always fail

19−badProvider : Provider Type

19+badProvider : IO (Provider Type)

20−badProvider = Error (return "Always fails")

20+badProvider = return (Error "Always fails")

22%provide (t : Type) with badProvider

test/test024/expectednew file+3

@@ -0,0 +1,3 @@

1+Type checking ./test024.idr

2+testtest

3+() : ()

test/test024/inputnew file+2

@@ -0,0 +1,2 @@

1+:x unsafePerformIO main

2+test

test/test024/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris --quiet test024.idr < input

3+rm -f *.ibc

test/test024/test024.idrnew file+6

@@ -0,0 +1,6 @@

1+module Main

3+main : IO ()

4+main = do l <- getLine

5+ let ll = l ++ l

6+ putStrLn ll

test/test026/expectednew file+3

@@ -0,0 +1,3 @@

1+Type checking ./test026.idr

2+2 : Int

3+2 : Nat

test/test026/inputnew file+2

@@ -0,0 +1,2 @@

1+foo

2+bar

test/test026/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris --quiet test026.idr < input

3+rm -f *.ibc

test/test026/test026.idrnew file+26

@@ -0,0 +1,26 @@

1+module Main

3+-- Simple test case for trivial type providers.

5+import Providers

7+%language TypeProviders

9+strToType : String -> Type

10+strToType "Int" = Int

11+strToType _ = Nat

12+

13+-- If the file contains "Int", provide Int as a type, otherwise provide Nat

14+fromFile : String -> IO (Provider Type)

15+fromFile fname = do str <- readFile fname

16+ return (Provide (strToType str))

17+

18+%provide (T1 : Type) with fromFile "theType"

19+%provide (T2 : Type) with fromFile "theOtherType"

20+

21+foo : T1

22+foo = 2

23+

24+bar : T2

25+bar = 2

26+

test/test026/theOtherTypenew file+1

@@ -0,0 +1 @@

1+Nat

test/test026/theTypenew file+1

@@ -0,0 +1 @@

1+Int