data Stream (s a : Data) where MkStream : (s -> Step s a) -> s -> Stream s a data Step (s a : Data) where Yield : a -> s -> Step s a Skip : s -> Step s a Done : Step s a -- | Apply a function to every element of a stream. smap (f : a -> b) (ss : Stream s a) : Stream s b = case ss of MkStream stepA sA0 -> let stepB q = case stepA q of Yield x sA1 -> Yield (f x) sA1 Skip sA2 -> Skip sA2 Done -> Done in MkStream stepB sA0 -- | Take the given number of elements from the front of a stream. stake (n : Nat) (ss : Stream s a) : Stream (Tup2 s Nat) a = case ss of MkStream fA sA0 -> let stepB q = case q of T2 sA ix -> if ix >= n then Done else case fA sA of Yield x sA2 -> Yield x (T2 sA2 (ix + 1)) Skip sA3 -> Skip (T2 sA3 ix) Done -> Done in MkStream stepB (T2 sA0 0)As we can see, work on larger demos is starting to be hampered by the lack of pattern matching sugar in the source language, so I'm going to add that next. After adding pattern matching, I'm going to spend a couple of weeks bug fixing, and should get the DDC 0.5 release out in early February 2015.
More info at the The Disciplined Disciple Compiler (DDC) Development Wiki.
Easy tickets to get started with: on the trac.
Tuesday, December 30, 2014
Work on DDC progresses, though recently it's been straightforward compiler engineering rather than anything novel, so I haven't been blogging. DDC now drops interface files when compiling modules, multi-module compilation works, and the front-end supports unicode string literals. I've also implemented a lambda lifter and support for higher order functions. This part is well baked enough to implement simple stream functions, as used in the Haskell Data.Vector library, though the compiler doesn't do the associated fusion yet. For example:
Posted by Ben Lippmeier at 4:40 PM