packages feed

ddc-code 0.4.2.1 → 0.4.3.1

raw patch · 27 files changed

+1638/−546 lines, 27 filesdep ~base

Dependency ranges changed: base

Files

LICENSE view
@@ -1,7 +1,7 @@ -------------------------------------------------------------------------------- The Disciplined Disciple Compiler License (MIT style) -Copyrite (K) 2007-2014 The Disciplined Disciple Compiler Strike Force+Copyrite (K) 2007-2016 The Disciplined Disciple Compiler Strike Force All rights reversed.  Permission is hereby granted, free of charge, to any person obtaining a copy
ddc-code.cabal view
@@ -1,5 +1,5 @@ Name:           ddc-code-Version:        0.4.2.1+Version:        0.4.3.1 License:        MIT License-file:   LICENSE Author:         The Disciplined Disciple Compiler Strike Force@@ -28,11 +28,28 @@         sea/primitive/Primitive.h         sea/runtime/Runtime.h +        tetra/base/Class/Applicative.ds+        tetra/base/Class/Functor.ds+        tetra/base/Class/Monad.ds+        tetra/base/Class/Ord.ds+        tetra/base/Class/Show.ds++        tetra/base/Control/Parsec.ds+         tetra/base/Data/Numeric/Bool.ds         tetra/base/Data/Numeric/Nat.ds+        tetra/base/Data/Numeric/Word.ds++        tetra/base/data/Text/Base.ds+        tetra/base/data/Text/Char.ds+        tetra/base/data/Text/List.ds+        tetra/base/data/Text/Operator.ds+        tetra/base/data/Text/Show.ds+         tetra/base/Data/Array.ds         tetra/base/Data/Function.ds         tetra/base/Data/List.ds+        tetra/base/Data/Map.ds         tetra/base/Data/Maybe.ds         tetra/base/Data/Ref.ds         tetra/base/Data/Stream.ds@@ -46,7 +63,7 @@  Library   build-depends:-        base            >= 4.6  &&  < 4.9,+        base            >= 4.6  &&  < 4.10,         filepath        >= 1.3  &&  < 1.5    exposed-modules:
salt/runtime64/debug/Trace.dcs view
@@ -65,7 +65,7 @@                   -- Some format that we don't handle yet,                   -- or the header is trashed.-                 _      -> do   primPutString "Unknown\n"+                 _      -> do   primPutString "Unknown\n"#                                 0#  @@ -78,17 +78,17 @@         format  = band# header 0x0fw32#         tag     = shr#  header 8w32# -        primPutString   "Thunk\n"-        fieldAddr       "{   ptr     = " (takePtr# obj)-        fieldWord32     "    format  = " format-        fieldWord32     "    tag     = " tag-        fieldNat        "    params  = " (paramsThunk obj)-        fieldNat        "    boxes   = " (boxesThunk  obj)-        fieldNat        "    args    = " (argsThunk   obj)-        fieldNat        "    runs    = " (runsThunk   obj)-        fieldAddr       "    fun     = " (funThunk    obj)+        primPutString   "Thunk\n"#+        fieldAddr       "{   ptr     = "# (takePtr# obj)+        fieldWord32     "    format  = "# format+        fieldWord32     "    tag     = "# tag+        fieldNat        "    params  = "# (paramsThunk obj)+        fieldNat        "    boxes   = "# (boxesThunk  obj)+        fieldNat        "    args    = "# (argsThunk   obj)+        fieldNat        "    runs    = "# (runsThunk   obj)+        fieldAddr       "    fun     = "# (funThunk    obj)         traceThunkPtrs obj 0#-        primPutString   "}\n"+        primPutString   "}\n"#          case trace of          True#  -> traceThunkPtrss obj 0#@@ -104,11 +104,11 @@           False#            -> do addr    = takePtr# (getThunk obj i)-                primPutString "    arg "+                primPutString "    arg "#                 primPutString (primShowNat i)-                primPutString "   = "+                primPutString "   = "#                 primPutString (primShowAddr addr)-                primPutString ";\n"+                primPutString ";\n"#                 traceThunkPtrs obj (add# i 1#)  @@ -134,13 +134,13 @@         tag     = shr#  header 8w32#         arity   = peek# ptr 4# -        primPutString   "Boxed\n"-        fieldAddr       "{   ptr     = " (takePtr# obj)-        fieldWord32     "    format  = " format-        fieldWord32     "    tag     = " tag-        fieldNat        "    arity   = " (promote# arity)+        primPutString   "Boxed\n"#+        fieldAddr       "{   ptr     = "# (takePtr# obj)+        fieldWord32     "    format  = "# format+        fieldWord32     "    tag     = "# tag+        fieldNat        "    arity   = "# (promote# arity)         traceBoxedPtrs obj (promote# arity) 0#-        primPutString   "}\n"+        primPutString   "}\n"#          case trace of          True#  -> traceBoxedPtrss obj (promote# arity) 0#@@ -156,11 +156,11 @@          False#            -> do addr     = takePtr# (getBoxed obj i) -                primPutString "    arg "+                primPutString "    arg "#                 primPutString (primShowNat i)-                primPutString "   = "+                primPutString "   = "#                 primPutString (primShowAddr addr)-                primPutString ";\n"+                primPutString ";\n"#                 traceBoxedPtrs obj n (add# i 1#)  @@ -185,12 +185,12 @@         tag     = shr#  header 8w32#         size    = peek# ptr 4# -        primPutString   "Raw\n"-        fieldAddr       "{   ptr     = " (takePtr# obj)-        fieldWord32     "    format  = " format-        fieldWord32     "    tag     = " tag-        fieldWord32     "    size    = " size-        primPutString   "}\n"+        primPutString   "Raw\n"#+        fieldAddr       "{   ptr     = "# (takePtr# obj)+        fieldWord32     "    format  = "# format+        fieldWord32     "    tag     = "# tag+        fieldWord32     "    size    = "# size+        primPutString   "}\n"#         0#  @@ -203,11 +203,11 @@         format  =             band# header 0x0fw32#         size    = shr# 4w32# (band# header 0xf0w32#) -        primPutString   "Small\n"-        fieldAddr       "{   ptr     = " (takePtr# obj)-        fieldWord32     "    format  = " format-        fieldWord32     "    size    = " size-        primPutString   "}\n"+        primPutString   "Small\n"#+        fieldAddr       "{   ptr     = "# (takePtr# obj)+        fieldWord32     "    format  = "# format+        fieldWord32     "    size    = "# size+        primPutString   "}\n"#         0#  @@ -216,20 +216,20 @@ fieldAddr (name: TextLit#) (val: Addr#): Void#  = do   primPutString name         primPutString (primShowAddr val)-        primPutString ";\n"+        primPutString ";\n"#   -- | Print a Nat# field to stdout. fieldNat (name: TextLit#) (val: Nat#): Void#  = do   primPutString name         primPutString (primShowNat val)-        primPutString ";\n"+        primPutString ";\n"#   -- | Print a Word32# field to stdout. fieldWord32 (name: TextLit#) (val: Word32#): Void#  = do   primPutString name         primPutString (primShowWord32 val)-        primPutString ";\n"+        primPutString ";\n"#
sea/primitive/Primitive.c view
@@ -80,6 +80,11 @@ }  +// Print a text literal to stdout.+void primPutTextLit (string_t* str)+{       fputs(str, stdout);+}+ // Print a text vector to stdout. void primPutVector (Obj* obj) {       string_t* str = (string_t*) _payloadRaw(obj);
sea/primitive/Primitive.h view
@@ -113,7 +113,8 @@  // Other primitives ----------------------------------------------------------- // These are defined in C land and linked into the runtime library.-extern string_t* primShowInt   (int   i);-extern string_t* primShowNat   (nat_t i);-extern void      primPutString (string_t* str);+extern string_t* primShowInt    (int   i);+extern string_t* primShowNat    (nat_t i);+extern void      primPutTextLit (string_t* str);+extern void      primPutString  (string_t* str);
+ tetra/base/Class/Applicative.ds view
@@ -0,0 +1,61 @@++module Class.Applicative+export  +{       dFunctorOfApplicative;+        pure; ap;+        liftA; liftA2; liftA3+}+import Class.Functor+where+++-- A functor with application.+data Applicative (f: Data -> Data) where+        Applicative+         :  Functor f +         -> ([a: Data].   a -> f a)                     -- pure+         -> ([a b: Data]. f (a -> b) -> f a -> f b)     -- ap+         -> Applicative f+++-- | Take the Functor dictionary from an Applicative dictionary.+dFunctorOfApplicative +        : [f: Data -> Data]+        . Applicative f -> Functor f++dFunctorOfApplicative (Applicative dFunctor _ _)+ = dFunctor+++-- | Return a value in the carrier.+pure    : [f: Data -> Data]. [a: Data]+        . Applicative f -> a -> f a++pure    (Applicative _ pure' _) x+ = pure' x+++-- | Apply a function in the carrier its argument in another carrier.+ap      : [f: Data -> Data]. [a b: Data]+        . Applicative f -> f (a -> b) -> f a -> f b++ap      (Applicative _ _ ap') xfab xfa+ = ap' xfab xfa+++-- Lifting functions.+liftA   (dapp: Applicative f) (f: a -> b) (xa: f a): f b+ = ap dapp (pure dapp f) xa+++liftA2  (dapp: Applicative f)+        (f: a -> b -> c) (xa: f a) (xb: f b): f c+ = let  dfun    = dFunctorOfApplicative dapp+   in   ap dapp (fmap dfun f xa) xb+++liftA3  (dapp: Applicative f) +        (f: a -> b -> c -> d) (xa: f a) (xb: f b) (xc: f c): f d+ = let  dfun    = dFunctorOfApplicative dapp+   in   ap dapp (ap dapp (fmap dfun f xa) xb) xc+
+ tetra/base/Class/Functor.ds view
@@ -0,0 +1,19 @@++module  Class.Functor +export  fmap+where+++-- | Class of collection types that can be mapped over.+data Functor (f: Data -> Data) where+        Functor+         :  ([a b: Data]. (a -> b) -> f a -> f b)       -- fmap+         -> Functor f+++-- | Apply a function to values of type 'a' in the input collection.+fmap    : [f: Data -> Data]. [a b: Data]+        . Functor f -> (a -> b) -> f a -> f b++fmap (Functor fmap') = fmap'+
+ tetra/base/Class/Monad.ds view
@@ -0,0 +1,54 @@++module Class.Monad+export  +{       dFunctorOfMonad; dApplicativeOfMonad;+        return; bind+}+import Class.Functor+import Class.Applicative+where+++-- | Class of types that support associative sequencing.+data Monad (m: Data -> Data) where+        Monad+         :  Applicative m+         -> ([a: Data].   a   -> m a)                   -- return+         -> ([a b: Data]. m a -> (a -> m b) -> m b)     -- bind+         -> Monad m+++-- | Take the Functor dictionary from a Monad dictionary.+dFunctorOfMonad +        : [m: Data -> Data]+        . Monad m -> Functor m++dFunctorOfMonad dMonad+        = dFunctorOfApplicative (dApplicativeOfMonad dMonad)+++-- | Take the Applicative dictionary from a Monad dictionary.+dApplicativeOfMonad+        : [m: Data -> Data]+        . Monad m -> Applicative m++dApplicativeOfMonad (Monad dApplicative _ _)+        = dApplicative+++-- | Return a value in a monad.+return  : [m: Data -> Data]. [a: Data]+        . Monad m -> a -> m a++return (Monad _ return' _) x+ = return' x+++-- | Evaluate a monadic compuation and pass the result to +--   a function that produces a new monadic computation.+bind    : [m: Data -> Data]. [a b: Data]+        . Monad m -> m a -> (a -> m b) -> m b++bind    (Monad _ _ bind') ma mf + = bind' ma mf+
+ tetra/base/Class/Ord.ds view
@@ -0,0 +1,14 @@++module Class.Ord+where+++data Ordering where+        LT      : Ordering+        GT      : Ordering+        EQ      : Ordering+++data Ord (k: Data) where+        Ord     : (k -> k -> Ordering) -> Ord k+
+ tetra/base/Class/Show.ds view
@@ -0,0 +1,48 @@++module Class.Show+export+{       show; show_bool; show_nat;+        show_text;+        show_tup2;+        show_list;+}+import Data.Text+import Data.List+where+++-- | Class dictionary for Show.+data Show (a: Data) where+        Show    : (a -> Text) -> Show a++show ((Show sh): Show a) (x: a): Text+ = sh x+++-------------------------------------------------------------------------------+-- Instances for basic types.+-- We define these in this module to avoid making it recursive+-- with the modules that define basic data types.+show_bool       = Show showBool+show_nat        = Show showNat+++-- ISSUE: #381: Escape non-printable characters in base Show library.+show_text: Show Text+ = Show sh+ where  sh tx           = "\"" % tx % "\""+++show_tup2 ((Show sh_a): Show a) ((Show sh_b): Show b)+        : Show (Tup2 a b)+ = Show sh+ where  +        sh (T2 x y)     = parens $ "T2" %% sh_a x %% sh_b y+++show_list ((Show sh_a): Show a): Show (List a)+ = Show sh+ where  +        sh Nil          = "Nil"+        sh (Cons x xs)  = parens $ "Cons" %% sh_a x %% sh xs+
+ tetra/base/Control/Parsec.ds view
@@ -0,0 +1,166 @@++module Control.Parsec+export  +{       parse; zero; item; satisfies;+        from; alt;+        monad_Parser;+        some; many;+}+import Class.Monad+import Data.List+import Data.Tuple+import Data.Maybe+where++data Parser (t a: Data) where+        Parser: (List t → List (Tup2 a (List t))) → Parser t a+++-- | Apply a parser to a list of input tokens.+parse ((Parser p): Parser t a) (ts: List t): List (Tup2 a (List t))+ = p ts+++-- Functor --------------------------------------------------------------------+functor_Parser [t: Data]: Functor (Parser t)+ = Functor parser_fmap++ where  parser_fmap [t a b: Data] (f: a → b) (parserA: Parser t a): Parser t b+         = Parser $ λts+         → for (parse parserA ts) $ λ(T2 resultA ts2)+         → T2  (f resultA) ts2+++-- Applicative ----------------------------------------------------------------+applicative_Parser [t: Data]: Applicative (Parser t)+ = Applicative +        functor_Parser+        parser_pure+        parser_ap++ where  parser_pure (x: a): Parser t' a+         = Parser $ λts → Cons (T2 x ts) Nil++        parser_ap   (parserF: Parser t' (a → b))+                    (parserA: Parser t' a)+                    : Parser t' b+         = Parser $ λts → concat+         $ for (parse parserF ts)  $ λ(T2 resultF ts2)+         → for (parse parserA ts2) $ λ(T2 resultA ts3)+         → T2 (resultF resultA) ts3+++-- Monad ----------------------------------------------------------------------+monad_Parser [t: Data]: Monad (Parser t)+ = Monad applicative_Parser+         parser_return+         parser_bind++ where  parser_return (x: a): Parser t' a+         = Parser $ λts → Cons (T2 x ts) Nil++        parser_bind+                (parserA:   Parser t' a)+                (mkParserB: a → Parser t' b)+                : Parser t' b+         = Parser $ λts → concat  +         $ for (parse parserA ts)              $ λ(T2 resultA ts2)+         → for (parse (mkParserB resultA) ts2) $ λ(T2 resultB ts3)+         → T2 resultB ts3+++-------------------------------------------------------------------------------+-- | Always fail, producing no possible parses.+zero: Parser t a+ = Parser $ λ_ → Nil+++-- | Consume the first input token, failing if there aren't any.+item: Parser t t+ = Parser $ λts+ → case ts of+        Nil             → Nil+        Cons t ts'      → Cons (T2 t ts) Nil+++-- | A parser that accepts a single token that satisfies the given predicate,+--   producing the given value if it matches.+satisfies (pred: t → Bool): Parser t t+ = Parser $ λts+ → case ts of+        Nil            → Nil+        Cons t ts+         | pred t      → Cons (T2 t ts) Nil+         | otherwise   → Nil+++-- | Use the given function to check whether to accept the next token,+--   returning the result that it produces.+from (accept: t → Maybe a): Parser t a+ = Parser $ λts+ → case ts of+        Nil            → Nil+        Cons t ts'+         → case accept t of+               Nothing → Nil+               Just x  → Cons (T2 x ts') Nil+++-- | Combine two argument parsers, producing a new one that accepts+--   strings parsed by either of the argument parsers.+plus (parserA parserB: Parser t a): Parser t a+ = Parser $ λts + → append (parse parserA ts) (parse parserB ts)+++-- | Combine two argument parsers, producing a new one that accepts+--   strings parser by either of the argument parser, but not both.+--   We prefer result produced by the first parser over the second.+alt (parserA parserB: Parser t a): Parser t a+ = Parser $ λts+ → case parse parserA ts of+        Nil    → parse parserB ts+        res    → res+++-- | Combine a list of argument parsers, producing a new one that+--   gives the result produced by the first matching argument parser.+alts (parsers: List (Parser t a)): Parser t a+ = case parsers of+        Nil             → zero+        Cons p ps       → alt p (alts ps)+++-- | Like `alts`, accept use the given default parser if no +--   parser from the first list succeeds.+altss (parsers: List (Parser t a)) (def: Parser t a): Parser t a+ = case parsers of+        Nil             → def+        Cons p ps       → alt p (altss ps def)+++-- | Apply a parser followed by another parser,+--   producing a tuple that contains both results.+follows (parserA: Parser t a) (parserB: Parser t b): Parser t (Tup2 a b)+ = Parser $ λts → concat+ $ for (parse parserA ts)  $ λ(T2 resultA ts2)+ → for (parse parserB ts2) $ λ(T2 resultB ts3)+ → T2 (T2 resultA resultB) ts3+++-- | Parse zero or more things, yielding a list of those things.+some (parserA: Parser t a): Parser t (List a)+ = alt  (bind   monad_Parser parserA        $ λx  → +         bind   monad_Parser (some parserA) $ λxs →+         return monad_Parser (Cons x xs))+        (return monad_Parser Nil)+++-- | Parse one or more things, yielding a list of those things.+many [a t: Data] (parserA: Parser t a): Parser t (List a)+ = alt  (bind   monad_Parser parserA        $ λx  →+         bind   monad_Parser (some parserA) $ λxs →+         return monad_Parser (Cons x xs))+        (bind   monad_Parser parserA        $ λx  →+         return monad_Parser (Cons x Nil))+
tetra/base/Data/Array.ds view
@@ -1,11 +1,17 @@  module Data.Array-export { allocArray; readArray; writeArray }+export { allocArray; readArray; writeArray; }+import Data.Numeric.Nat  import foreign boxed type  Array : Region ~> Data ~> Data  import foreign c value+ -- ISSUE #377: Use type equations during Tetra to Salt transform.+ -- The Tetra to Salt transform isn't looking through type equations,+ -- so types of primitives that use type synonyms break. Eg if we use+ -- 'Nat' here instead of 'Nat#' the transform won't know these primtives+ -- accept unboxed values.  allocArray : [r: Region]. [a: Data]. Nat# -> a -> S (Alloc r) (Array r a)  readArray  : [r: Region]. [a: Data]. Array r a -> Nat# -> S (Read r) a  writeArray : [r: Region]. [a: Data]. Array r a -> Nat# -> a -> S (Write r) Void#
tetra/base/Data/Function.ds view
@@ -1,6 +1,6 @@  module  Data.Function-export  { id; apply; compose }+export  { id; apply; compose; } where  @@ -18,5 +18,5 @@ -- | Compose two functions. --   The operator '∘' is desugared to applications of this function. compose [a b c: Data] (f: b -> c) (g: a -> b): a -> c- = λx : a. f (g x)+ = λ(x : a) -> f (g x)
tetra/base/Data/List.ds view
@@ -1,22 +1,30 @@  module Data.List -export  { singleton;    replicate-        ; enumFromTo-        ; append-        ; length-        ; head-        ; tail; tail1-        ; last; index-        ; reverse -        ; map;    mapS-        ; forS-        ; zipWith; zipWithS-        ; foldl;  foldlS;       sum;    prod-        ; foldr;  foldrS-        ; scanl-        ; filter; filterS-        ; any }+export+{       singleton;  replicate;+        enumFromTo; append; concat;+        length;+        head;+        tail; tail1;+        last; index;+        lookupBy; find;+        reverse;+        map; mapS; for;+        forS;+        zipWith; zipWithS;+        foldl;  foldlS;       sum;    prod;+        foldr;  foldrS;+        scanl;+        filter; filterS;+        any;+} import  Data.Numeric.Nat+import  Data.Numeric.Bool+import  Data.Tuple+import  Data.Maybe+import  Data.Function+import  Class.Functor+import  Class.Monad where  -- | Standard Cons-lists.@@ -33,13 +41,13 @@  -- | Construct a list of the given length where all elements are' --   the same value.-replicate (n: Nat#) (x: a): List a+replicate (n: Nat) (x: a): List a  | n == 0       = Nil  | otherwise    = Cons x (replicate (n - 1) x)   -- | Construct a range of values.-enumFromTo (start: Nat#) (end: Nat#): List Nat#+enumFromTo (start: Nat) (end: Nat): List Nat  | start >= end = singleton start  | otherwise    = Cons start (enumFromTo (start + 1) end) @@ -51,9 +59,35 @@         Cons x xs       -> Cons x (append xs yy)  +-- | Concatenate a list of lists.+concat (xss0: List (List a)): List a+ = case xss0 of+        Nil             -> Nil+        Cons xs xss1    -> go xs xss1+ where+        go Nil         Nil              = Nil+        go Nil         (Cons xs' xss')  = go xs' xss'+        go (Cons x xs) xss              = Cons x (go xs xss)+++-- | Generate a list of the given length by repeatedly +--   applying a stateful function.+unfold   (s0: s) (f: s -> Maybe (Tup2 a s)): List a+ = case f s0 of+        Nothing         -> Nil+        Just (T2 a s1)  -> Cons a (unfold s1 f)+++generate (len: Nat) (f: Nat -> a): List a+ = unfold 0+ $ (\ix -> if ix >= len +                then Nothing+                else Just (T2 (f ix) (ix + 1)))++ -- Projections ---------------------------------------------------------------- -- | Take the length of a list.-length (xx: List a): Nat#+length (xx: List a): Nat  = case xx of         Nil             -> 0         Cons x xs       -> 1 + length xs@@ -77,23 +111,19 @@ tail1   (def: a) (xx: List a): List a  = case xx of         Nil             -> singleton def-        Cons x xs        -         -> case xs of-                Nil     -> singleton x-                _       -> xs+        Cons x Nil      -> singleton x+        Cons _ xs       -> xs   -- | Take the last element of a list, if there is one. last (def: a) (xx: List a): a  = case xx of         Nil                     -> def-        Cons x xs-         -> case xs of-                Nil             -> x-                Cons y ys       -> last def xs+        Cons x Nil              -> x+        Cons x (Cons y ys)      -> last def (Cons y ys)  -index (def: a) (n: Nat#) (xx: List a): a+index (def: a) (n: Nat) (xx: List a): a  = case xx of            Nil     -> def         Cons x xs @@ -102,6 +132,26 @@                 _       -> index def (n - 1) xs  +-- Searches -------------------------------------------------------------------+-- | Given a list of key value pairs, lookup the first+--   value whose key is selected by the given predicate.+lookupBy (f: a -> Bool) (xx: List (Tup2 a b)): Maybe b+ = case xx of+        Nil             -> Nothing+        Cons (T2 x y) xs+         | f x          -> Just y+         | otherwise    -> lookupBy f xs+++-- | Find the first element in a list that matches the given predicate.+find (f: a -> Bool) (xx: List a): Maybe a+ = case xx of+        Nil             -> Nothing+        Cons x xs+         | f x          -> Just x+         | otherwise    -> find f xs++ -- Transforms ----------------------------------------------------------------- -- | Reverse the elements of a list. --   This is a naive O(n^2) version for testing purposes.@@ -119,6 +169,18 @@         Cons x xs       -> Cons (f x) (map f xs)  +-- | Like `map`, but with the arguments swapped.+for     (xx: List a) (f: a -> b): List b+ = case xx of+        Nil             -> Nil+        Cons x xs       -> Cons (f x) (for xs f)+++-- | Functor instance for List.+functor_list + = Functor map++ -- | Apply a stateful worker function to every element of a list, --   yielding a new list.  --   The worker is applied to the source elements left-to-right.@@ -137,29 +199,37 @@                 forS xs f  --- Zips ------------------------------------------------------------------------zipWith (f: a -> b -> c) -        (xx: List a) (yy: List b): List c+-- | Monadic map.+mapM    (dMonad: Monad m) +        (f: a -> m b) (xx: List a): m (List b)  = case xx of-        Nil     -> Nil+        Nil    +         -> return dMonad Nil+         Cons x xs-         -> case yy of-                Cons y ys-                 -> Cons (f x y) (zipWith f xs ys)+         -> bind   dMonad (f x)              $ λx'+         -> bind   dMonad (mapM dMonad f xs) $ λxs'+         -> return dMonad (Cons x' xs') -                Nil -> Nil +-- Zips -----------------------------------------------------------------------+zipWith (f: a -> b -> c) +        (xx: List a) (yy: List b): List c+ = case T2 xx yy of+        T2 Nil _                -> Nil+        T2 (Cons x xs) Nil      -> Nil+        T2 (Cons x xs) (Cons y ys)+         -> Cons (f x y) (zipWith f xs ys) ++-- | Stateful zipWith. zipWithS (f: a -> b -> S e c)           (xx: List a) (yy: List b): S e (List c)- = case xx of-        Nil     -> Nil-        Cons x xs-         -> case yy of-                Cons y ys-                 -> Cons (f x y) (zipWithS f xs ys)--                Nil -> Nil+ = case T2 xx yy of+        T2 Nil _                -> Nil+        T2 (Cons x xs) Nil      -> Nil+        T2 (Cons x xs) (Cons y ys)+         -> Cons (f x y) (zipWithS f xs ys)   -- Folds ----------------------------------------------------------------------@@ -196,15 +266,20 @@   -- | Take the sum of a list of Nats.-sum (xs: List Nat#): Nat#+sum (xs: List Nat): Nat  = foldl (+) 0 xs   -- | Take the product of a list of Nats.-prod (xs: List Nat#): Nat#+prod (xs: List Nat): Nat  = foldl (*) 1 xs  +-- | Monadic sequence.+sequence (dMonad: Monad m) (xs: List (m a)): m (List a)+ = mapM dMonad id xs++ -- Scans ---------------------------------------------------------------------- scanl (f: b -> a -> b) (acc: b) (xx: List a): List b  = case xx of@@ -218,31 +293,28 @@  -- Filters -------------------------------------------------------------------- -- | Keep only those elements that match the given predicate.-filter (p: a -> Bool#) (xx: List a): List a+filter (p: a -> Bool) (xx: List a): List a  = case xx of         Nil             -> Nil         Cons x xs  -         -> if p x -                then Cons x (filter p xs)-                else filter p xs+         | p x          -> Cons x (filter p xs)+         | otherwise    -> filter p xs   -- | Keep only those elements that match the given stateful predicate. --   The predicate is applied to the list elements from left to right.-filterS (p: a -> S e Bool#) (xx: List a): S e (List a)+filterS (p: a -> S e Bool) (xx: List a): S e (List a)  = case xx of         Nil             -> Nil         Cons x xs  -         -> if p x -                then Cons x (filterS p xs)-                else filterS p xs+         | p x          -> Cons x (filterS p xs)+         | otherwise    -> filterS p xs   -- | Check if any of the members of the list match the given predicate.-any (p: a -> Bool#) (xx: List a): Bool#+any (p: a -> Bool) (xx: List a): Bool  = case xx of-        Nil-         -> False+        Nil             -> False          Cons x xs           | p x          -> True
+ tetra/base/Data/Map.ds view
@@ -0,0 +1,325 @@++module Data.Map+export  +{       map_empty;  map_singleton;+        map_null;   map_size;+        map_lookup; map_member;+        map_insert; map_insertWithKey;+        map_foldr;  map_foldrWithKey; map_foldlWithKey;+        map_fromList;+        map_toList; map_toAscList; map_toDescList;+        show_map;+}+import Data.Numeric.Nat+import Data.Numeric.Bool+import Data.Text+import Data.Maybe+import Data.List+import Data.Tuple+import Class.Ord+import Class.Show+where+++-- | A map from keys @k@ to values @a@.+data Map (k a: Data) where+        Bin : Size -> k -> a -> Map k a -> Map k a -> Map k a+        Tip : Map k a+++type Size = Nat+++show_map (show_k: Show k) (show_a: Show a): Show (Map k a)+ = Show sh+ where  +        sh (Bin s k a l r)+         = parens $ "Bin"+                %% show show_nat s+                %% show show_k   k+                %% show show_a   a+                %% show (show_map show_k show_a) l+                %% show (show_map show_k show_a) r++        sh Tip+         = "Tip"+++-- Construction -----------------------------------------------------------------------------------+-- | O(1). The empty map.+map_empty : Map k a+ = Tip+++-- | O(1). A map with a single element.+map_singleton (k: k) (x: a) : Map k a+ = Bin 1 k x Tip Tip+++-- Query ------------------------------------------------------------------------------------------+-- | /O(1)/. Is the map empty?+--+-- > Data.Map.null (empty)           == True+-- > Data.Map.null (singleton 1 'a') == False+map_null (mp: Map k a): Bool+ = case mp of+        Tip             -> True+        Bin _ _ _ _ _   -> False+++-- | /O(1)/. The number of elements in the map.+--+-- > size empty                                   == 0+-- > size (singleton 1 'a')                       == 1+-- > size (fromList([(1,'a'), (2,'c'), (3,'b')])) == 3+map_size (mp: Map k a): Size+ = case mp of+        Tip             -> 0+        Bin sz _ _ _ _  -> sz+  ++-- | /O(log n)/. Lookup the value at a key in the map.+--+-- The function will return the corresponding value as @('Just' value)@,+-- or 'Nothing' if the key isn't in the map.+map_lookup ((Ord compare): Ord k) (kx: k) (mp: Map k a): Maybe a+ = go kx mp+ where  +        go _ Tip +         = Nothing [a]++        go k (Bin _ kx x l r)+         = case compare k kx of+                LT -> go k l+                GT -> go k r+                EQ -> Just x+++-- | /O(log n)/. Is the key a member of the map?+--+-- > member 5 (fromList [(5,'a'), (3,'b')]) == True+-- > member 1 (fromList [(5,'a'), (3,'b')]) == False+--+map_member ((Ord compare): Ord k) (kx: k) (mp: Map k a): Bool+ = go kx mp+ where  +        go _ Tip +         = False++        go k (Bin _ kx _ l r)+         = case compare k kx of+                LT -> go k l+                GT -> go k r+                EQ -> True+++-- Insertion --------------------------------------------------------------------------------------+-- | /O(log n)/. Insert a new key and value in the map.+--   If the key is already present in the map, the associated value is+--   replaced with the supplied value. 'insert' is equivalent to+--   @'insertWith' 'const'@.+--+-- > insert 5 'x' (fromList [(5,'a'), (3,'b')]) == fromList [(3, 'b'), (5, 'x')]+-- > insert 7 'x' (fromList [(5,'a'), (3,'b')]) == fromList [(3, 'b'), (5, 'a'), (7, 'x')]+-- > insert 5 'x' empty                         == singleton 5 'x'+--+map_insert+        ((Ord compare): Ord k) +        (kx0: k) (x0: a) (mp: Map k a): Map k a+ = go kx0 x0 mp+ where+        go kx x Tip +         = map_singleton kx x++        go kx x (Bin sz ky y l r)+         = case compare kx ky of+                LT -> map_balance ky y (go kx x l) r+                GT -> map_balance ky y l (go kx x r)+                EQ -> Bin sz kx x l r+++-- | /O(log n)/. Insert with a function, combining new value and old value.+--   @'insertWith' f key value mp@+--   will insert the pair (key, value) into @mp@ if key does+--   not exist in the map. If the key does exist, the function will+--   insert the pair @(key, f new_value old_value)@.+--+map_insertWith+        (ord: Ord k)+        (f: a -> a -> a)+        (kx: k) (x: a) (mp: Map k a)+        : Map k a+ = map_insertWithKey ord+        (\_ x' y' -> f x' y')+        kx x mp+++-- | /O(log n)/. Insert with a function, combining key, new value and old value.+--   @'insertWithKey' f key value mp@+--   will insert the pair (key, value) into @mp@ if key does+--   not exist in the map. If the key does exist, the function will+--   insert the pair @(key,f key new_value old_value)@.+--   Note that the key passed to f is the same key passed to 'insertWithKey'.+--+map_insertWithKey+        ((Ord compare): Ord k)+        (f: k -> a -> a -> a)+        (kx: k) (x: a) (mp: Map k a)+        : Map k a+ = go kx x mp+ where+        go kx x Tip+         = map_singleton kx x++        go kx x (Bin sy ky y l r)+         = case compare kx ky of+                LT -> map_balance ky y (go kx x l) r+                GT -> map_balance ky y l (go kx x r)+                EQ -> Bin sy kx (f kx x y) l r+++-- Folds ------------------------------------------------------------------------------------------+-- | /O(n)/. Fold the values in the map using the given right-associative+--   binary operator.+--+map_foldr (f: a -> b -> b) (z: b) (mp: Map k a): b+ = go z mp+ where+        go z' Tip             = z'+        go z' (Bin _ _ x l r) = go (f x (go z' r)) l+++-- | /O(n)/. Fold the keys and values in the map using the given right-associative+--   binary operator..+--+map_foldrWithKey (f: k -> a -> b -> b) (z: b) (mp: Map k a): b+ = go z mp+ where+        go z' Tip              = z'+        go z' (Bin _ kx x l r) = go (f kx x (go z' r)) l+++-- | /O(n)/. Fold the keys and values in the map using the given left-associative+-- binary operator.+map_foldlWithKey (f: a -> k -> b -> a) (z: a) (mp: Map k b): a+ = go z mp+ where  go z' Tip              = z'+        go z' (Bin _ kx x l r) = go (f (go z' l) kx x) r+++-- Conversion -------------------------------------------------------------------------------------+map_fromList +        (ord: Ord k)+        (xx: List (Tup2 k a))+        : Map k a+ = foldl (λ  mp tp+          -> case tp of+                 T2 kx x -> map_insert ord kx x mp)+         map_empty xx+++-- | /O(n)/. Convert the map to a list of key\/value pairs. +map_toList (mp: Map k a): List (Tup2 k a)+        = map_toAscList mp+++-- | /O(n)/. Convert the map to a list of key\/value pairs where the+--   keys are in ascending order. +map_toAscList (mp: Map k a): List (Tup2 k a)+        = map_foldrWithKey (λk x xs -> Cons (T2 k x) xs) Nil mp+++-- | /O(n)/. Convert the map to a list of key\/value pairs where the+--   keys are in descending order.+map_toDescList (mp: Map k a): List (Tup2 k a)+        = map_foldlWithKey (λxs k x -> Cons (T2 k x) xs) Nil mp+++---------------------------------------------------------------------------------------------------+-- [balance l x r] balances two trees with value x.+--  The sizes of the trees should balance after decreasing the+--  size of one of them. (a rotation).+--+--  [delta] is the maximal relative difference between the sizes of+--          two trees, it corresponds with the [w] in Adams' paper.+--+--  [ratio] is the ratio between an outer and inner sibling of the+--          heavier subtree in an unbalanced setting. It determines+--          whether a double or single rotation should be performed+--          to restore balance. It is corresponds with the inverse+--          of $\alpha$ in Adam's article.+--+--  Note that according to the Adam's paper:+--  - [delta] should be larger than 4.646 with a [ratio] of 2.+--  - [delta] should be larger than 3.745 with a [ratio] of 1.534.+--+--  But the Adam's paper is erroneous:+--  - It can be proved that for delta=2 and delta>=5 there does+--    not exist any ratio that would work.+--  - Delta=4.5 and ratio=2 does not work.+--+--  That leaves two reasonable variants, delta=3 and delta=4,+--  both with ratio=2.+--+--  - A lower [delta] leads to a more 'perfectly' balanced tree.+--  - A higher [delta] performs less rebalancing.+--+--  In the benchmarks, delta=3 is faster on insert operations,+--  and delta=4 has slightly better deletes. As the insert speedup+--  is larger, we currently use delta=3.+--+--  NOTE: The Haskell implementation from the containers package+--  contains an unfolded version of balance to optimise pattern +--  matching, but there is no point using that until we have the+--  same sort of pattern matching compiler optimisations as GHC.+-- +delta   = 2+ratio   = 5+++map_balance (k: k) (x: a) (l: Map k a) (r: Map k a): Map k a+ = let  sizeL = map_size l in+   let  sizeR = map_size r in+   let  sizeX = sizeL + sizeR + 1 +   in   match+         | sizeL + sizeR <= 1    = Bin sizeX k x l r+         | sizeR > delta*sizeL   = rotateL k x l r+         | sizeL > delta*sizeR   = rotateR k x l r+         | otherwise             = Bin sizeX k x l r+++rotateL (k: k) (x: a)+        (l: Map k a) (r@(Bin _ _ _ ly ry): Map k a)+        : Map k a+ | map_size ly < ratio*map_size ry = singleL k x l r+ | otherwise                       = doubleL k x l r+++rotateR (k: k) (x: a)+        (l@(Bin _ _ _ ly ry): Map k a) (r: Map k a)+        : Map k a+ | map_size ry < ratio*map_size ly = singleR k x l r+ | otherwise                       = doubleR k x l r+++singleL (k1: k) (x1: a) (t1: Map k a) (tR: Map k a): Map k a+ | Bin _ k2 x2 t2 t3 <- tR+ = bin k2 x2 (bin k1 x1 t1 t2) t3++singleR (k1: k) (x1: a) (tL: Map k a) (t3: Map k a): Map k a+ | Bin _ k2 x2 t1 t2 <- tL+ = bin k2 x2 t1 (bin k1 x1 t2 t3)++doubleL (k1: k) (x1: a) (t1: Map k a) (tR: Map k a): Map k a+ | Bin _ k2 x2 (Bin _ k3 x3 t2 t3) t4 <- tR+ = bin k3 x3 (bin k1 x1 t1 t2) (bin k2 x2 t3 t4)++doubleR (k1: k) (x1: a) (tL: Map k a) (t4: Map k a): Map k a+ | Bin _ k2 x2 t1 (Bin _ k3 x3 t2 t3) <- tL+ = bin k3 x3 (bin k2 x2 t1 t2) (bin k1 x1 t3 t4)+++-- | The bin constructor maintains the size of the tree+bin (k: k) (x: a) (l: Map k a) (r: Map k a): Map k a+ = Bin (map_size l + map_size r + 1) k x l r+
tetra/base/Data/Maybe.ds view
@@ -1,6 +1,10 @@  module Data.Maybe export  { isNothing; isJust; fromMaybe }+import Class.Functor+import Class.Applicative+import Class.Monad+import Data.Numeric.Bool where  @@ -10,20 +14,73 @@         Just    : a -> Maybe a  +-- Functor --------------------------------------------------------------------+functor_maybe+ = Functor +        maybe_fmap+ where +        maybe_fmap : [a b: Data]. (a -> b) -> Maybe a -> Maybe b+        maybe_fmap f xx +         = case xx of+               Nothing -> Nothing+               Just x  -> Just (f x)+++-- Applicative ----------------------------------------------------------------+applicative_maybe+ = Applicative +        functor_maybe +        maybe_pure+        maybe_ap+ where+        maybe_pure : [a: Data]. a -> Maybe a+        maybe_pure x+         = Just x++        maybe_ap   : [a b: Data]. Maybe (a -> b) -> Maybe a -> Maybe b+        maybe_ap mf ma+         | Just xf      <- mf+         , Just xa      <- ma+         = Just (xf xa)++         | otherwise+         = Nothing+++-- Monad ----------------------------------------------------------------------+monad_maybe+ = Monad+        applicative_maybe+        maybe_return+        maybe_bind+ where  +        maybe_return : [a: Data]. a -> Maybe a+        maybe_return x+         = Just x++        maybe_bind   : [a b: Data]. Maybe a -> (a -> Maybe b) -> Maybe b+        maybe_bind ma f         +         = case ma of+                Nothing -> Nothing+                Just xa -> f xa+++-- Predicates ----------------------------------------------------------------- -- | Check if the given value is a `Nothing`.-isNothing (m: Maybe a): Bool#+isNothing (m: Maybe a): Bool  = case m of         Nothing -> True         Just x  -> False   -- | Check if the given value is a `Just`.-isJust (m: Maybe a): Bool#+isJust (m: Maybe a): Bool  = case m of         Nothing -> False         Just x  -> True  +-- Destructors ---------------------------------------------------------------- -- | Take the value from a `Just`, or return a default value. fromMaybe (def: a) (m: Maybe a): a  = case m of@@ -36,3 +93,4 @@  = case m of         Nothing -> def         Just x  -> f x+
tetra/base/Data/Numeric/Bool.ds view
@@ -1,23 +1,24 @@  module Data.Numeric.Bool-export  { not; and; or }+export { not; and; or; } where +type Bool = Bool#  -- | Boolean NOT.-not (x: Bool#): Bool#+not (x: Bool): Bool  = if x then False           else True   -- | Boolean AND.-and (x y: Bool#): Bool#+and (x y: Bool): Bool  = if x then y          else False   -- | Boolean OR.-or (x y: Bool#): Bool#+or (x y: Bool): Bool  = if x then True          else y
tetra/base/Data/Numeric/Nat.ds view
@@ -1,12 +1,18 @@  module Data.Numeric.Nat-export  { add; sub;  mul; div; rem-        ; eq;  neq; lt;   le;  gt;  ge-        ; shl; shr; band; bor; bxor-        ; divMod }+export  +{       add; sub;  mul; div; rem;+        eq;  neq; lt;   le;  gt;  ge;+        shl; shr; band; bor; bxor;+        divMod;+        ord_nat;+} import Data.Tuple+import Class.Ord where +type Nat = Nat#+ ------------------------------------------------------------------------------- -- Names used by the Source Tetra desugarer to implement infix operators. add x y         = add# [Nat#] x y@@ -37,7 +43,16 @@ bxor x y        = bxor# [Nat#] x y   -divMod (n m: Nat#): Tup2 Nat# Nat#+divMod (n m: Nat): Tup2 Nat Nat  = T2 (div n m) (rem n m) ++-------------------------------------------------------------------------------+-- Type class instances.+nat_compare n1 n2+ | n1 > n2      = GT+ | n1 < n2      = LT+ | otherwise    = EQ++ord_nat         = Ord nat_compare
+ tetra/base/Data/Numeric/Word.ds view
@@ -0,0 +1,9 @@++module Data.Numeric.Word+where++type Word8      = Word8#+type Word16     = Word16#+type Word32     = Word32#+type Word64     = Word64#+
tetra/base/Data/Stream.ds view
@@ -1,10 +1,13 @@  module Data.Stream-export  { streamOfList; listOfStream-        ; sgenerate; senumFrom; srepeat; scons-        ; smap; smapacc-        ; sfold; sany-        ; stake; stakeWhile; sfilter }+export  +{       streamOfList; listOfStream;+        sgenerate; senumFrom; srepeat; scons;+        smap; smapacc;+        sfold; sany;+        stake; stakeWhile; +        sfilter;+} import Data.Numeric.Nat import Data.List import Data.Maybe@@ -15,6 +18,7 @@ where  +------------------------------------------------------------------------------- -- | Unbounded streams,  --   wraps a function that produces elements on demand. data Stream (s a: Data) where@@ -26,31 +30,30 @@         Done    : Step s a  --- Conversions ------------------------------------------------------------------------------------+-- Conversions ---------------------------------------------------------------- -- | Convert a list to a stream. streamOfList (xx: List a): Stream (List a) a- = let  step (s1: List a)+ = MkStream step xx+ where  +        step (s1: List a)          = case s1 of                 Nil       -> Done                 Cons x xs -> Yield x xs-   in   MkStream step xx   -- | Convert a stream to a list.-listOfStream  (ss: Stream s a): List a- = case ss of-        MkStream f s0-         -> case f s0 of-                Yield x s1      -> Cons x (listOfStream (MkStream f s1))-                Skip  s1        -> listOfStream (MkStream f s1)-                Done            -> Nil+listOfStream (ss: Stream s a): List a+ | MkStream f s0 <- ss+ = case f s0 of+        Yield x s1      -> Cons x (listOfStream (MkStream f s1))+        Skip  s1        -> listOfStream (MkStream f s1)+        Done            -> Nil   -- | Load the given number of elements from a stream and write them --   into a freshly allocated array. arrayOfStream -        [r1: Region] -        (n: Nat#)        -- ^ Length of result array.+        (n: Nat)         -- ^ Length of result array.         (d: a)           -- ^ Default element value.         (ss: Stream s a) -- ^ Stream to evaluate.         : S (Alloc r1) (Array r1 a)@@ -68,94 +71,101 @@  -- | Unstream all available elements into the given array. unstreamToArray-        [r: Region] -        (ss: Stream s a) (arr: Array r a) (ix: Nat#)+        (ss: Stream s a) (arr: Array r a) (ix: Nat)         : S (Write r) Unit- = case ss of-        MkStream f s0-         -> case f s0 of+ | MkStream f s0  <- ss+ = go s0 0+ where  +        go (s: s) (ix: Nat): S (Write r) Unit+         = case f s of                 Yield x s1                  -> do  writeArray arr ix x-                        unstreamToArray (MkStream f s1) arr (ix + 1)+                        go s1 (ix + 1)                  Skip s1-                 ->     unstreamToArray (MkStream f s1)  arr ix+                 ->     go s1 ix                   Done                  ->     ()  --- Constructors -----------------------------------------------------------------------------------+-- Constructors --------------------------------------------------------------- -- | Generate a stream, given a starting value and a stepper function. sgenerate (x: s) (step: s -> Tup2 s a): Stream s a- = let  step' sA+ = MkStream step' x+ where  +        step' sA          = case step sA of                 T2 s' x -> Yield x s'-   in   MkStream step' x -senumFrom (x: Nat#): Stream Nat# Nat#- = sgenerate x (λs: Nat#. T2 (s + 1) s)+senumFrom (x: Nat): Stream Nat Nat+ = sgenerate x (λ(s: Nat) -> T2 (s + 1) s)   -- | Create a stream that returns copies of the same value. srepeat (x: a): Stream a a- = sgenerate x (λs: a. T2 s s)+ = sgenerate x (λ(s: a) -> T2 s s)   -- | Cons an element to the front of a stream.-scons (x: a) (ss: Stream s a): Stream (Tup2 s Bool#) a- = case ss of-        MkStream stepA sA0-         -> let stepA2 q-                 = case q of-                        T2 sA1 b-                         -> case b of-                                True    -> Yield x (T2 sA1 False)-                                False   -> case stepA sA1 of-                                                Yield y sA2 -> Yield y (T2 sA2 False)-                                                Skip  sA2   -> Skip    (T2 sA2 False)-                                                Done        -> Done-            in  MkStream stepA2 (T2 sA0 True)+scons   (x: a) (ss: Stream s a)+        : Stream (Tup2 s Bool) a+ | MkStream stepA  sA0 <- ss+ = MkStream stepA2 (T2 sA0 True)+ where  +        stepA2 (T2 sA1 True)+         = Yield x (T2 sA1 False) +        stepA2 (T2 sA1 False)+         = case stepA sA1 of+                Yield y sA2 -> Yield y (T2 sA2 False)+                Skip  sA2   -> Skip    (T2 sA2 False)+                Done        -> Done --- Maps -------------------------------------------------------------------------------------------++-- Maps ----------------------------------------------------------------------- -- | 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+smap    (f: a -> b) +        (ss: Stream s a)+        : Stream s b+ | MkStream stepA sA0 <- ss+ = MkStream stepB sA0+ where+        stepB q +         = case stepA q of+                Yield x sA1     -> Yield (f x) sA1+                Skip sA2        -> Skip sA2+                Done            -> Done  --- Scans ------------------------------------------------------------------------------------------+-- Scans ---------------------------------------------------------------------- -- | Like `smap`, but keep a running accumulator as we walk along the stream.-smapacc (f: a -> b -> Tup2 a c) (z: a) -        (ss: Stream s b): Stream (Tup2 s a) c- = case ss of-        MkStream fB sB0-         -> let stepC q-                 = case q of-                        T2 sB1 xA1-                         -> case fB sB1 of-                                Yield xB1 sB2 -                                 -> case f xA1 xB1 of-                                        T2 xA2 xC2-                                         -> Yield xC2 (T2 sB2 xA2)-                                Skip sB2 -> Skip      (T2 sB2 xA1)-                                Done     -> Done-            in  MkStream stepC (T2 sB0 z)+smapacc :  [a b c s: Data]+        .  (a -> b -> Tup2 a c)+        -> a+        -> Stream s b+        -> Stream (Tup2 s a) c +smapacc f z (MkStream fB sB0)+ = MkStream stepC (T2 sB0 z)+ where+        stepC (T2 sB1 xA1)+         = case fB sB1 of+                Yield xB1 sB2 +                 -> case f xA1 xB1 of+                        T2 xA2 xC2+                         -> Yield xC2 (T2 sB2 xA2)+                Skip sB2 -> Skip      (T2 sB2 xA1)+                Done     -> Done --- Folds ------------------------------------------------------------------------------------------++-- Folds ---------------------------------------------------------------------- -- | Fold all the elements from a stream.-sfold    (f: a -> b -> a) (acc: a) (ss: Stream s b): a- = case ss of-        MkStream step s0 -         -> sconsume f acc step s0+sfold   (f: a -> b -> a) +        (acc: a) +        ((MkStream step s0): Stream s b)+        : a+ = sconsume f acc step s0   sconsume (f:    a -> b -> a)   (acc:   a) @@ -168,54 +178,57 @@  -- | Check if any of the elements of this stream are true, --   demanding only the prefix of non-true elements from the stream.-sany [s: Data] (ss: Stream s Bool#): Bool#+sany [s: Data] (ss: Stream s Bool): Bool  = sfold or False $ stakeWhile id ss  --- Projections ------------------------------------------------------------------------------------+-- Projections ---------------------------------------------------------------- -- | Take the given number of elements from 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 -                         | ix >= n   -> Done-                         | otherwise -                         -> 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)+stake   (n: Nat)+        ((MkStream fA sA0): Stream s a)+        : Stream (Tup2 s Nat) a + = MkStream stepB (T2 sA0 0)+ where  +        stepB (T2 sA ix)+         | ix >= n   = Done+         | otherwise +         = case fA sA of+                Yield x sA2 -> Yield x (T2 sA2 (ix + 1))+                Skip sA3    -> Skip  (T2 sA3 ix)+                Done        -> Done --- | Take elements from a strem while they match the given predicate.-stakeWhile (p: a -> Bool#) (ss: Stream s a): Stream s a- = case ss of-        MkStream stepA sA0-         -> let stepB q-                 = case stepA q of-                        Yield x sA1     -                         | p x          -> Yield x sA1-                         | otherwise    -> Done [s] [a] -                        Skip sA1        -> Skip    sA1-                        Done            -> Done+-- | Take elements from a stream while they match the given predicate.+stakeWhile +        (p: a -> Bool) +        ((MkStream stepA sA0): Stream s a)+        : Stream s a -            in  MkStream stepB sA0+ = MkStream stepB sA0+ where  +        stepB (q: s)+         = case stepA q of+                Yield x sA1     +                 | p x          -> Yield x sA1+                 | otherwise    -> Done +                Skip sA1        -> Skip    sA1+                Done            -> Done + -- | Take elements from a stream that match the given predicate.-sfilter (p: a -> Bool#) (ss: Stream s a): Stream s a- = case ss of-        MkStream stepA sA0-         -> let stepB q-                 = case stepA q of-                        Yield x sA1     -                         | p x          -> Yield x sA1-                         | otherwise    -> Skip    sA1+sfilter (p: a -> Bool)+        ((MkStream stepA sA0): Stream s a)+        : Stream s a+ = MkStream stepB sA0+ where+        stepB (q: s)+         = case stepA q of+                Yield x sA1     +                 | p x          -> Yield x sA1+                 | otherwise    -> Skip sA1 -                        Skip sA1        -> Skip    sA1-                        Done            -> Done+                Skip sA1        -> Skip sA1+                Done            -> Done  -            in  MkStream stepB sA0
tetra/base/Data/Text.ds view
@@ -1,308 +1,6 @@  module Data.Text -export  -{       -- * Construction-        textLit; textOfVector; vectorOfText;-        paste; pastes;--        -- * Projections-        sizeOfText;--        -- * Conversions-        copyTextToVector;-        copyTextLitToVector;-        copyTextVecToVector;--        -- * Operators-        textOfWord8;--        -- * Showing-        showBool;-        showNat; showBinaryNat; showDecimalNat; showHexNat; showBaseNat;-        digitBinary; digitDecimal; digitHex;-}-import Data.Numeric.Nat-import Data.Numeric.Bool-import Data.Function-import Data.List----- | The TextLit type is define in the runtime system and contains---   a pointer to the literal utf-8 text data in static memory.-import foreign boxed type-        TextLit         : Data----- | Runtime functions for dealing with unboxed text literals.-import foreign c value--        -- | Box a text literal.-        makeTextLit     : TextLit# -> TextLit--        -- | Get the size of a boxed text literal.-        sizeOfTextLit   : TextLit  -> Nat#--        -- | Get a single byte from a boxed text literal.-        indexTextLit    : TextLit  -> Nat# -> Word8#----- | Top level region containing text vectors.-import foreign abstract type-        RegionText      : Region----- | Capabilities to allocate and read top-level text vectors.-import foreign abstract capability-        capTopTextAlloc : Alloc RegionText-        capTopTextRead  : Read  RegionText--where------------------------------------------------------------------------------------- Names used by the Source Tetra desugarer to implement string literals.-textLit (x : TextLit#) : Text- = TextLit (makeTextLit x)--paste  (x y : Text) : Text- = TextApp x y--pastes (x y : Text) : Text- = x % " " % y-----------------------------------------------------------------------------------data Text where-        TextLit : TextLit                   -> Text-        TextVec : Vector# RegionText Word8# -> Text-        TextApp : Text -> Text              -> Text----- Construction ------------------------------------------------------------------ | O(1). Wrap a vector of utf8 data into a text object.-textOfVector (vec: Vector# RegionText Word8#): Text- = TextVec vec----- | Copy a Text object into a flat vector of utf-8 bytes.-vectorOfText [r1: Region] (tt: Text)-        : S (Alloc r1) (Vector# r1 Word8#)- = extend r1 using r2 with { Alloc r2; Write r2 } in-   do   -        -- Allocate a vector to hold all the data, -        -- including an extra null terminator byte.-        vec     = vectorAlloc# [r2] [Word8#] (add (sizeOfText tt) 1)--        -- Copy the text data into the vector.-        iEnd    = copyTextToVector tt vec 0--        -- Write the null terminator.-        vectorWrite# vec iEnd 0w8--        vec----- | Wrap a single 8-bit character into a text object.----textOfWord8 (w8: Word8#): Text- = TextVec-  (extend RegionText using r1 with { Alloc r1; Write r1 } in-   do   -- Allocate the vector to hold the data,-        -- including an extra null terminator byte.-        vec     = vectorAlloc# [r1] [Word8#] 2--        -- Write the character.-        vectorWrite# vec 0 w8--        -- Write the null terminator.-        vectorWrite# vec 1 0w8--        vec)----- Projections ------------------------------------------------------------------- | Get the size of the utf8 data in a Text object, in bytes.------   * This is NOT the same as the length of the text string in characters,---     as single characters can be encoded using multiple bytes.----sizeOfText (tt: Text): Nat#- = case tt of-        TextLit lit-         -> sizeOfTextLit lit--        -- The size of a text vector is the vector size minus-        -- the null terminator byte.-        TextVec vec     -         -> vectorLength# vec - 1--        TextApp t1 t2-         -> sizeOfText t1 + sizeOfText t2----- Conversions ------------------------------------------------------------------- | Copy a text literal to a mutable vector of utf-8 bytes.-copyTextToVector -        [r: Region] (tt: Text) (vec: Vector# r Word8#) (i0: Nat#)-        : S (Write r) Nat#- = case tt of-        TextLit lit-         -> copyTextLitToVector lit  vec i0 0 (sizeOfTextLit lit)--        TextVec vec2-         -> copyTextVecToVector vec2 vec i0 0 (vectorLength# vec2)--        TextApp t1 t2-         -> do  i1 = copyTextToVector t1 vec i0-                i2 = copyTextToVector t2 vec i1-                i2----- | Copy a text literal to a mutable vector of utf-8 bytes.-copyTextLitToVector -        [r: Region] (tt: TextLit) (vec: Vector# r Word8#) -        (iDst iSrc nSrc: Nat#)-        : S (Write r) Nat#- = case iSrc >= nSrc of-        True  -> iDst-        False -         -> do  vectorWrite# vec iDst (indexTextLit tt iSrc)--                copyTextLitToVector -                        tt vec (iDst + 1) (iSrc + 1) nSrc----- | Copy a text source vector to a mutable destination of utf-8 bytes.-copyTextVecToVector -        [r1 r2: Region] -        (vecSrc: Vector# r1 Word8#) (vecDst: Vector# r2 Word8#)-        (iDst iSrc nSrc: Nat#)-        : S (Read r1 + Write r2) Nat#- = case iSrc >= nSrc of-        True    -> iDst--        False   -> do-                vectorWrite# vecDst iDst (vectorRead# vecSrc iSrc)--                copyTextVecToVector -                        vecSrc vecDst (iDst + 1) (iSrc + 1) nSrc----- Operators --------------------------------------------------------------------- | If this text is not already in flat form then flatten it.------   This allocates a new contiguous vector for the text object and---   allows the program to release space for intermediate append nodes.----flattenText (tt: Text): Text- = case tt of-        -- Single text literals are already flat.-        TextLit lit     -> tt--        -- Single text vectors are already flat.-        TextVec vec     -> tt--        -- Text has an outer append-node, -        -- so flatten the whole thing.-        TextApp _ _     -> textOfVector (run vectorOfText [RegionText] tt)----- Showing ----------------------------------------------------------------------- | Convert a Bool to a String.-showBool (x : Bool#) : Text- = if x then "True" -        else "False"----- | Show a natural number.-showNat (x: Nat#): Text- = showBaseNat 10 digitDecimal 0 "X" x------------------------------------------------------------------------------------- | Show a natural number, in binary.-showBinaryNat (x: Nat#): Text- = showBaseNat 2 digitBinary 0 "X" x--digitBinary (n: Nat#): Text- = case n of-        0       -> "0"-        1       -> "1"-        _       -> "X"----- | Show a natural number in decimal.-showDecimalNat (x: Nat#): Text- = showBaseNat 10 digitDecimal 0 "X" x--digitDecimal (n: Nat#): Text- = case n of-        0       -> "0"-        1       -> "1"-        2       -> "2"-        3       -> "3"-        4       -> "4"-        5       -> "5"-        6       -> "6"-        7       -> "7"-        8       -> "8"-        9       -> "9"-        _       -> "X"----- | Show a natural number in hex.-showHexNat (x: Nat#): Text- = showBaseNat    16 digitHex 0 "X" x--digitHex (n: Nat#): Text- = case n of-        0       -> "0"-        1       -> "1"-        2       -> "2"-        3       -> "3"-        4       -> "4"-        5       -> "5"-        6       -> "6"-        7       -> "7"-        8       -> "8"-        9       -> "9"-        10      -> "a"-        11      -> "b"-        12      -> "c"-        13      -> "d"-        14      -> "e"-        15      -> "f"-        _       -> "X"------------------------------------------------------------------------------------- | Show a natural number using an arbitrary base encoding.-showBaseNat -        (base:  Nat#)           -- ^ Base of encoding.-        (digit: Nat# -> Text)   -- ^ Show a digit in this base.-        (width: Nat#)           -- ^ Width of output, or 0 to not pad.-        (pad:   Text)           -- ^ Character to pad output with.-        (x:     Nat#)           -- ^ Number to print.-        : Text-- = do   s       = showBaseNat' base digit width pad True x-        if x < 0 -         then "-" % s -         else s--showBaseNat' base digit width pad first x- | and (x == 0) first- = showBaseNat' base digit (width - 1) pad False x- % "0"-- | and (x == 0) (width > 0)- = showBaseNat' base digit (width - 1) pad False x- % pad-- | x == 0- = ""-- | otherwise- = showBaseNat' base digit (width - 1) pad False (div x base) - % digit (rem x base) -+import Data.Text.Base+import Data.Text.List+import Data.Text.Operator+import Data.Text.Show
+ tetra/base/Data/Text/Base.ds view
@@ -0,0 +1,244 @@++-- | Basic types and operators on Text objects.+module Data.Text.Base+export+{       -- Runtime operators.+        makeTextLit;+        sizeOfTextLit;+        indexTextLit;++        -- Construction.+        textOfChar;+        textOfWord8;+        textOfVector;++        -- Conversion.+        vectorOfText;++        -- Projections.+        sizeOfText;+        indexText;++        -- Operators.+        eqText;+}+import Data.Text.Char+import Data.Numeric.Nat+import Data.Numeric.Word+import Data.Maybe+++-------------------------------------------------------------------------------+-- Foreign imports.++-- | A TextLit is a boxed object that contains a pointer to literal+--   UTF-8 data in static memory.  +import foreign boxed type+        TextLit         : Data+++-- | Runtime operators for working with unboxed text literals.+import foreign c value++        -- | Make a text literal.+        --   The TextLit# type is a pointer to literal UTF-8 data in +        --   static memory, which we pack into a boxed object.+        makeTextLit     : TextLit# -> TextLit++        -- | Get the size of a boxed text literal.+        sizeOfTextLit   : TextLit  -> Nat#++        -- | Get a single byte from a boxed text literal.+        --   This is a byte rather than a character,+        --   as UTF-8 encoded characters can consist of multiple bytes.+        indexTextLit    : TextLit  -> Nat# -> Word8#+++-- | Top level region containing text vectors.+--   All our dynamic character data is in this region.+import foreign abstract type+        RegionText      : Region+++-- | Capabilities to allocate and read top-level text vectors.+import foreign abstract capability+        capTopTextAlloc : Alloc RegionText+        capTopTextRead  : Read  RegionText++where+++-- Text -----------------------------------------------------------------------+data Text where+        -- | Wrap a text literal into a text object.+        --   The characterdata is stored in static memory.+        TextLit : TextLit                   -> Text++        -- | Wrap some character data into a text object.+        --   The character data is stored on the heap.+        TextVec : Vector# RegionText Word8# -> Text++        -- | Append two text objects.+        TextApp : Text -> Text              -> Text+++-- Construction ---------------------------------------------------------------+-- | O(1). Wrap a single character into a text object.+--   We're only taking the lowest 8 bit bytes,+--   rather than doing proper UTF-8 encoding.+textOfChar (c: Word32): Text+ = textOfWord8 (truncate# c)+++-- | O(1). Wrap a single byte into a text object.+textOfWord8 (w8: Word8): Text+ = TextVec+ $ extend RegionText using r1 with { Alloc r1; Write r1 } in+   do   -- Allocate the vector to hold the data,+        -- including an extra null terminator byte.+        vec     = vectorAlloc# [r1] 2++        -- Write the character.+        vectorWrite# vec 0 w8++        -- Write the null terminator.+        vectorWrite# vec 1 0w8++        vec+++-- | O(1). Wrap a vector of UTF-8 data into a text object.+textOfVector (vec: Vector# RegionText Word8): Text+ = TextVec vec+++-- Conversion -----------------------------------------------------------------+-- | Copy a Text object into a flat vector of UTF-8 data.+vectorOfText+        [r1: Region] (tt: Text)+        : S (Alloc r1) (Vector# r1 Word8)+ = extend r1 using r2 with { Alloc r2; Write r2 } in+   do   +        -- Allocate a vector to hold all the data, +        -- including an extra null terminator byte.+        vec     = vectorAlloc# [r2] (add (sizeOfText tt) 1)++        -- Copy the text data into the vector.+        iEnd    = copyTextToVector tt vec 0++        -- Write the null terminator.+        vectorWrite# vec iEnd 0w8++        vec+++-- | Copy a text object to a mutable vector of UTF-8 data.+copyTextToVector +        [r: Region] (tt: Text) (vec: Vector# r Word8) (i0: Nat)+        : S (Write r) Nat+ = case tt of+        TextLit lit+         -> copyTextLitToVector lit  vec i0 0 (sizeOfTextLit lit)++        TextVec vec2+         -> copyTextVecToVector vec2 vec i0 0 (vectorLength# vec2 - 1)++        TextApp t1 t2+         -> do  i1 = copyTextToVector t1 vec i0+                i2 = copyTextToVector t2 vec i1+                i2+++-- | Copy a text literal to a mutable vector of UTF-8 data.+copyTextLitToVector +        [r: Region] (tt: TextLit) (vec: Vector# r Word8) +        (iDst iSrc nSrc: Nat)+        : S (Write r) Nat+ | iSrc >= nSrc = iDst+ | otherwise+ = do   vectorWrite# vec iDst (indexTextLit tt iSrc)+        copyTextLitToVector +                tt vec (iDst + 1) (iSrc + 1) nSrc+++-- | Copy a text source vector to a mutable vector of UTF-8 data.+copyTextVecToVector +        [r1 r2: Region] +        (vecSrc: Vector# r1 Word8) (vecDst: Vector# r2 Word8)+        (iDst iSrc nSrc: Nat)+        : S (Read r1 + Write r2) Nat+ | iSrc >= nSrc = iDst+ | otherwise+ = do   vectorWrite# vecDst iDst (vectorRead# vecSrc iSrc)+        copyTextVecToVector +                vecSrc vecDst (iDst + 1) (iSrc + 1) nSrc+++-- Projections ----------------------------------------------------------------+-- | Get the size of the utf8 data in a Text object, in bytes.+--+--   * This is NOT the same as the length of the text string in characters,+--     as single characters can be encoded using multiple bytes.+--+sizeOfText (tt: Text): Nat+ = case tt of+        TextLit lit+         -> sizeOfTextLit lit++        -- The size of a text vector is the vector size minus+        -- the null terminator byte.+        TextVec vec     +         -> vectorLength# vec - 1++        TextApp t1 t2+         -> sizeOfText t1 + sizeOfText t2+++-- | Get a single word8 character from a Text object.+indexText (tt: Text) (ix: Nat): Maybe Word8+ = case tt of+        TextLit lit+         | ix >= sizeOfTextLit lit      -> Nothing+         | otherwise                    -> Just (indexTextLit lit ix)++        TextVec vec+         | ix >= vectorLength# vec - 1  -> Nothing+         | otherwise                    -> Just (vectorRead# vec ix)++        TextApp t1 t2+         -> case indexText t1 ix of+                Just x                  -> Just x+                Nothing                 -> indexText t2 (ix - sizeOfText t1)+++-- Comparison -----------------------------------------------------------------+-- | O(max len1 len2).+--   Check if two text objects represent the same characters.+eqText (tx1 tx2: Text): Bool+ = private r with {Read r; Alloc r} in+   do   +        -- We copy both strings into new vectors before doing the comparison.+        -- It would be better to do it in-place.+        vec1    = vectorOfText  [r] tx1 +        len1    = vectorLength# vec1++        vec2    = vectorOfText  [r] tx2+        len2    = vectorLength# vec2++        match+         | len1 /= len2 = False+         | len1 == 0    = True+         | otherwise    = go vec1 vec2 len1 0++ where+        go (vec1 vec2: Vector# r Word8)+           (len: Nat) (ix: Nat): S (Read r) Bool+         | ix >= (len - 1)+         = True++         | not (eq# (vectorRead# vec1 ix) (vectorRead# vec2 ix))+         = False++         | otherwise+         = go vec1 vec2 len (ix + 1)+
+ tetra/base/Data/Text/Char.ds view
@@ -0,0 +1,28 @@++module Data.Text.Char+export+{       isDigit;+        isUpper;+        isLower;+}+import Data.Numeric.Bool+where++-- Character literals are special syntax for a unicode codepoint+-- represented as a 32-bit word.+type Char = Word32#+++-- | Check if a character is a digit.+isDigit (c: Char): Bool+ = ge# c 0x030w32 ∧ le# c 0x039w32+++-- | Check if a character is an upper-case letter.+isUpper (c: Char): Bool+ = ge# c 65w32    ∧ le# c 90w32+++-- | Check if a character is a lower-case letter.+isLower (c: Char): Bool+ = ge# c 97w32    ∧ le# c 122w32
+ tetra/base/Data/Text/List.ds view
@@ -0,0 +1,66 @@++-- | Conversions between Text and Lists.+module Data.Text.List+export +{       textOfCharList;+        charListOfText;+}+import Data.Numeric.Word+import Data.Text.Base+import Data.Text.Char+import Data.List+where+++-- | Convert a list of characters to a Text object.+textOfCharList (xx: List Char): Text+ = TextVec+ $ extend RegionText using r with { Alloc r; Read r; Write r }+   in  vectorOfCharList [r] xx+++-- | O(n). Convert a text object to a list of characters.+charListOfText (tx: Text): List Char+ = case tx of+        TextVec vec -> charListOfTextVec vec+        _           -> charListOfTextVec (vectorOfText [RegionText] tx)+++-- | Unpack a list of characters from a vector.+charListOfTextVec+        (vec: Vector# r Word8)+        : S (Read r) (List Char)+ = go 0+ where  +        go (ix: Nat): S (Read r) (List Char)+         | ix >= (vectorLength# vec - 1)+         = Nil++         | otherwise               +         = do   txChar = promote# (vectorRead# vec ix)+                Cons txChar (go (ix + 1))+++-- | Pack a list of characters into a mutable vector.+vectorOfCharList+        [r: Region]+        (xx: List Char)+        : S (Alloc r + Write r) (Vector# r Word8)+ = do+        len     = length xx+        vec     = vectorAlloc# [r] (len + 1)++        fill (ix: Nat) (xx: List Char): S (Write r) Unit+         = case xx of+                Nil     -> ()+                Cons x xs+                 -> do  vectorWrite# vec ix (truncate# x)+                        fill (ix + 1) xs++                 | otherwise+                 -> do  fill (ix + 1) xs+        fill 0 xx++        vectorWrite# vec len 0w8+        vec+
+ tetra/base/Data/Text/Operator.ds view
@@ -0,0 +1,54 @@++-- | Useful operators on text objects.+module Data.Text.Operator+export+{       -- * Desugaring+        textLit; paste; pastes;++        -- * Optimizations+        flattenText;++        -- * Pretty Printing+        parens;+}+import Data.Text.Base+where+++-- Desuguaring -----------------------------------------------------------------+-- Names used by the Source Tetra desugarer to implement string literals.+textLit (x : TextLit#) : Text+ = TextLit (makeTextLit x)++paste  (x y : Text) : Text+ = TextApp x y++pastes (x y : Text) : Text+ = x % " " % y+++-- Optimizations --------------------------------------------------------------+-- | If this text is not already in flat form then flatten it.+--+--   This allocates a new contiguous vector for the text object and+--   allows the program to release space for intermediate append nodes.+--+flattenText (tt: Text): Text+ = case tt of+        -- Single text literals are already flat.+        TextLit lit     -> tt++        -- Single text vectors are already flat.+        TextVec vec     -> tt++        -- Text has an outer append-node, +        -- so flatten the whole thing.+        TextApp _ _     -> textOfVector (run vectorOfText [RegionText] tt)+++-- Pretty Printing ------------------------------------------------------------+-- | Wrap a some text in parenthesis.+parens (tx: Text): Text+ = "(" % tx % ")"++
+ tetra/base/Data/Text/Show.ds view
@@ -0,0 +1,119 @@++-- | Showing various data types as text.+module Data.Text.Show+export+{       showBool;++        showNat;+        showBinaryNat;  digitBinary;+        showDecimalNat; digitDecimal;+        showHexNat;     digitHex;+        showBaseNat;+}+import Data.Numeric.Word+import Data.Text.Base+import Data.Text.Char+import Data.Text.Operator+where+++-------------------------------------------------------------------------------+-- | Convert a Bool to a String.+showBool (x : Bool): Text+ = if x then "True" +        else "False"+++-- | Show a natural number.+showNat (x: Nat): Text+ = showBaseNat 10 digitDecimal 0 'X' x+++-------------------------------------------------------------------------------+-- | Show a natural number, in binary.+showBinaryNat (x: Nat): Text+ = showBaseNat 2 digitBinary 0 'X' x++digitBinary (n: Nat): Char+ = case n of+        0       -> '0'+        1       -> '1'+        _       -> 'X'+++-------------------------------------------------------------------------------+-- | Show a natural number in decimal.+showDecimalNat (x: Nat): Text+ = showBaseNat 10 digitDecimal 0 'X' x++digitDecimal (n: Nat): Word32+ = case n of+        0       -> '0'+        1       -> '1'+        2       -> '2'+        3       -> '3'+        4       -> '4'+        5       -> '5'+        6       -> '6'+        7       -> '7'+        8       -> '8'+        9       -> '9'+        _       -> 'X'+++-------------------------------------------------------------------------------+-- | Show a natural number in hex.+showHexNat (x: Nat): Text+ = showBaseNat 16 digitHex 0 'X' x++digitHex (n: Nat): Char+ = case n of+        0       -> '0'+        1       -> '1'+        2       -> '2'+        3       -> '3'+        4       -> '4'+        5       -> '5'+        6       -> '6'+        7       -> '7'+        8       -> '8'+        9       -> '9'+        10      -> 'a'+        11      -> 'b'+        12      -> 'c'+        13      -> 'd'+        14      -> 'e'+        15      -> 'f'+        _       -> 'X'+++-------------------------------------------------------------------------------+-- | Show a natural number using an arbitrary base encoding.+showBaseNat +        (base:  Nat)            -- ^ Base of encoding.+        (digit: Nat -> Char)    -- ^ Show a digit in this base.+        (width: Nat)            -- ^ Width of output, or 0 to not pad.+        (pad:   Char)           -- ^ Character to pad output with.+        (x:     Nat)            -- ^ Number to print.+        : Text+ = do   s       = showBaseNat' base digit width pad True x+        if x < 0 +         then "-" % s +         else s++showBaseNat' base digit width pad first x+ | and (x == 0) first+ = showBaseNat' base digit (width - 1) pad False x +        % "0"++ | and (x == 0) (width > 0)+ = showBaseNat' base digit (width - 1) pad False x+        % textOfChar pad++ | x == 0  + = ""++ | otherwise+ = showBaseNat' base digit (width - 1) pad False (div x base) +        % textOfChar (digit (rem x base))+
tetra/base/Math/Combinations.ds view
@@ -6,37 +6,36 @@ import Data.List where + -- | Compute the factorial of a number. -- --   factorial n is the number of possible permutations --   of a sequence of n things. ---factorial (n: Nat#): Nat#- = if n == 0-        then 1-        else n * factorial (n - 1)+factorial (n: Nat): Nat+ | n == 0       = 1+ | otherwise    = n * factorial (n - 1)  --- | Compute the number of was of choosing r things from n things.+-- | Compute the number of ways of choosing r things from n things. --- --   Note that the textbook definition of this is, --     div (factorial n) ( factorial (n - 1) * factorial r ) --   but we factor out the (factorial (n - 1)) term beforehand to  --   make it easier to compute. ---choose (n r: Nat#): Nat#- = if r > n -        then 0-        else div (prodRange n (n - (r - 1))) (factorial r)+choose (n r: Nat): Nat+ | r > n        = 0+ | otherwise    = div (prodRange n (n - (r - 1))) (factorial r) + -- | Compute the product of the range [n, n-1 .. m] inclusive.-prodRange (n m: Nat#): Nat#- = if n == m-        then n-        else n * prodRange (n - 1) m+prodRange (n m: Nat): Nat+ | n == m       = n+ | otherwise    = n * prodRange (n - 1) m   -- | Compute the number of ways of choosing collections of things --   of sizes rs from n things.-chooseMany (n: Nat#) (rs: List Nat#): Nat#+chooseMany (n: Nat) (rs: List Nat): Nat  = div (factorial n) (prod (map factorial rs))