This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Ok, modules loaded: Main, Language.Coatl.Abstract, Language.Coatl.Parser.Expression, Language.Coatl.Parser.Declaration, Language.Coatl.Graph, Language.Coatl.Check, Language.Coatl.Check.Types. | |
*Main> main | |
Language.Coatl.Parser.Expression | |
expression | |
- parses names | |
- parses operators | |
- parses infix operators | |
- parses lambdas | |
- parses the type of the identity function |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- | Some functions on directed graphs. | |
module Language.Coatl.Graph where | |
-- base | |
import Data.Maybe | |
-- containers | |
import Data.Map (Map) | |
import qualified Data.Map as M | |
import Data.Set (Set) | |
import qualified Data.Set as S | |
-- mtl |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
[ import = [ internal ] | |
, module = small-example | |
, pragma = no-prelude | |
, doc = "A small example module!" | |
] | |
id _ x = x | |
[ doc = "The identity function" | |
, type = dependent type (\a -> function a a) | |
] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Control.Applicative.Recipes where | |
-- base | |
import Control.Applicative | |
import Data.Foldable | |
import Data.Traversable | |
import Data.Monoid | |
-- containers | |
import Data.Set | |
data Recipe k v m a = Recipe |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
def bit_iter(bits, n): | |
"Iterate over the bits of an integer, padding it to `n` digits." | |
return ((bits >> i) & 1 for i in xrange(n - 1, -1, -1)) | |
def unsigned_bin(x, n=32): | |
"Print the unsigned binary representation of an integer." | |
return "".join(repr(y) for y in bit_iter(x, n)) | |
print unsigned_bin(0b101, 8) # '00000101' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import Sheets | |
import Control.Applicative | |
import Control.Monad.State | |
import Data.Text (Text) | |
import qualified Data.Text as T | |
import qualified Data.Text.IO as T | |
simple :: [T.Text] -> Table (State Int) Text | |
simple = Table [counter id, see] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
data MaybeT : (Type -> Type) -> Type where | |
MT : {m : Type -> Type} -> m (Maybe a) -> MaybeT m a |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
def multidecorator(fn): | |
class _MultiDecorator(object): | |
class __metaclass__(type): | |
def __new__(cls, name, bases, dict): | |
# No magic on the first class with this metaclass | |
if bases == (object,): | |
return type.__new__(cls, fn.__name__, bases, dict) | |
else: | |
return fn(**dict) | |
return _MultiDecorator |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
\begin{diagram} | |
\named{a} \box \box \\ | |
\box \box \named{b} \\ | |
\box \box \empty | |
\end{diagram} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Elaborating {__Infer0} | |
builtin:0 | |
---> Type a | |
builtin:0:Constructor {__infer0} : {{A0} : Type} -> ({a0} : {A0}) -> {__Infer0} | |
Rechecking ({A0} : Type 0) -> {A0} -> {__Infer0} | |
---> {__infer0} : ({A0} : Type c) -> {A0} -> {__Infer0} | |
Forced: {__infer0} [] | |
from ({A0} : Type c) -> {A0} -> {__Infer0} | |
Elaborating {__Unit0} | |
builtin:0 |