aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--stdlib/source/documentation/lux/control/concatenative.lux88
-rw-r--r--stdlib/source/library/lux/control/concatenative.lux195
-rw-r--r--stdlib/source/library/lux/data/format/css/value.lux126
-rw-r--r--stdlib/source/test/lux/control/concatenative.lux323
4 files changed, 337 insertions, 395 deletions
diff --git a/stdlib/source/documentation/lux/control/concatenative.lux b/stdlib/source/documentation/lux/control/concatenative.lux
index 6b71f6ecd..7fa084004 100644
--- a/stdlib/source/documentation/lux/control/concatenative.lux
+++ b/stdlib/source/documentation/lux/control/concatenative.lux
@@ -1,6 +1,6 @@
(.using
[library
- [lux (.except if loop)
+ [lux (.except if loop left right)
["$" documentation (.only documentation:)]
[data
[text
@@ -30,22 +30,6 @@
else (=> ,,,0 ,,,1)]
,,,0 [Bit then else] ,,,1))])
-(documentation: /.||>
- "A self-contained sequence of concatenative instructions."
- [(same? value
- (||> (push sample)))]
- [(||> (push 123)
- dup
- n/=)])
-
-(documentation: /.word:
- "A named concatenative function."
- [(word: square
- (=> [Nat] [Nat])
-
- dup
- (apply_2 n.*))])
-
(documentation: /.apply
"A generator for functions that turn arity N functions into arity N concatenative functions."
[(is (=> [Nat] [Nat])
@@ -77,19 +61,19 @@
(documentation: /.swap
"Swaps the 2 topmost stack values.")
-(documentation: /.rotL
+(documentation: /.left_rotation
"Rotes the 3 topmost stack values to the left.")
-(documentation: /.rotR
+(documentation: /.right_rotation
"Rotes the 3 topmost stack values to the right.")
(documentation: /.&&
"Groups the 2 topmost stack values as a 2-tuple.")
-(documentation: /.||L
+(documentation: /.left
"Left-injects the top into sum.")
-(documentation: /.||R
+(documentation: /.right
"Right-injects the top into sum.")
(with_template [<input> <word> <func>]
@@ -144,10 +128,10 @@
(documentation: /.if
"If expression."
[(same? "then"
- (||> (push true)
- (push "then")
- (push "else")
- if))])
+ (/.value (|>> (push true)
+ (push "then")
+ (push "else")
+ if)))])
(documentation: /.call
"Executes an anonymous block on the stack.")
@@ -164,38 +148,38 @@
(documentation: /.do
"Do-while loop expression."
[(n.= (++ sample)
- (||> (push sample)
- (push (push false))
- (push (|>> (push 1) n/+))
- do while))])
+ (/.value (|>> (push sample)
+ (push (push false))
+ (push (|>> (push 1) n/+))
+ do while)))])
(documentation: /.while
"While loop expression."
[(n.= (n.+ distance start)
- (||> (push start)
- (push (|>> dup
- (push start) n/-
- (push distance) n/<))
- (push (|>> (push 1) n/+))
- while))])
+ (/.value (|>> (push start)
+ (push (|>> dup
+ (push start) n/-
+ (push distance) n/<))
+ (push (|>> (push 1) n/+))
+ while)))])
(documentation: /.compose
"Function composition."
[(n.= (n.+ 2 sample)
- (||> (push sample)
- (push (|>> (push 1) n/+))
- (push (|>> (push 1) n/+))
- compose
- call))])
+ (/.value (|>> (push sample)
+ (push (|>> (push 1) n/+))
+ (push (|>> (push 1) n/+))
+ compose
+ call)))])
(documentation: /.partial
"Partial application."
[(n.= (n.+ sample sample)
- (||> (push sample)
- (push sample)
- (push n/+)
- partial
- call))])
+ (/.value (|>> (push sample)
+ (push sample)
+ (push n/+)
+ partial
+ call)))])
(documentation: /.when
"Only execute the block when #1.")
@@ -208,8 +192,6 @@
($.module /._
""
[..=>
- ..||>
- ..word:
..apply
..apply_1
..apply_2
@@ -224,11 +206,11 @@
..nip
..dup
..swap
- ..rotL
- ..rotR
+ ..left_rotation
+ ..right_rotation
..&&
- ..||L
- ..||R
+ ..left
+ ..right
..if
..call
..loop
@@ -280,5 +262,7 @@
..f/<
..f/<=
..f/>
- ..f/>=]
+ ..f/>=
+
+ ($.default /.value)]
[]))
diff --git a/stdlib/source/library/lux/control/concatenative.lux b/stdlib/source/library/lux/control/concatenative.lux
index 9bd9d2355..4661a546e 100644
--- a/stdlib/source/library/lux/control/concatenative.lux
+++ b/stdlib/source/library/lux/control/concatenative.lux
@@ -1,21 +1,22 @@
(.using
[library
- [lux (.except Alias if loop)
+ [lux (.except Alias if loop left right)
["[0]" meta]
+ ["[0]" type]
[abstract
["[0]" monad]]
[control
["[0]" maybe (.open: "[1]#[0]" monad)]]
[data
+ ["[0]" product]
["[0]" text (.only)
["%" \\format (.only format)]]
[collection
["[0]" list (.open: "[1]#[0]" mix functor)]]]
["[0]" macro (.only with_symbols)
+ [syntax (.only syntax)]
["[0]" code]
- ["[0]" template]
- [syntax (.only syntax)
- ["|[0]|" export]]]
+ ["[0]" template]]
[math
[number
["n" nat]
@@ -26,111 +27,55 @@
["<>" parser (.open: "[1]#[0]" monad)
["<[0]>" code (.only Parser)]]])
-(type: Alias
- [Text Code])
-
(type: Stack
(Record
[#bottom (Maybe Code)
#top (List Code)]))
-(def: aliases^
- (Parser (List Alias))
- (|> (<>.and <code>.local <code>.any)
- <>.some
- <code>.tuple))
-
-(def: top^
+(def: top
(Parser (List Code))
(<code>.tuple (<>.some <code>.any)))
-(def: bottom^
+(def: bottom
(Parser Code)
- (<code>.not ..top^))
+ (<code>.not ..top))
-(def: stack^
+(def: stack
(Parser Stack)
- (<>.either (<>.and (<>.maybe bottom^)
- ..top^)
- (<>.and (<>#each (|>> {.#Some}) bottom^)
+ (<>.either (<>.and (<>.maybe bottom)
+ ..top)
+ (<>.and (<>#each (|>> {.#Some}) bottom)
(<>#in (list)))))
-(def: (stack_mix tops bottom)
+(def: (stack_type tops bottom)
(-> (List Code) Code Code)
(list#mix (function (_ top bottom)
(` [(~ bottom) (~ top)]))
bottom
tops))
-(def: (singleton expander)
- (-> (Meta (List Code)) (Meta Code))
- (monad.do meta.monad
- [expansion expander]
- (case expansion
- {.#Item singleton {.#End}}
- (in singleton)
-
- _
- (meta.failure (format "Cannot expand to more than a single AST/Code node:" text.new_line
- (|> expansion (list#each %.code) (text.interposed " ")))))))
-
-(def: signature^
- (Parser [(List Alias) Stack Stack])
- (<>.either (all <>.and aliases^ stack^ stack^)
- (all <>.and (<>#in (list)) stack^ stack^)))
-
(def: .public =>
- (syntax (_ [[aliases inputs outputs] signature^])
- (let [de_alias (function (_ aliased)
- (list#mix (function (_ [from to] pre)
- (code.replaced (code.local from) to pre))
- aliased
- aliases))]
- (case [(the #bottom inputs)
- (the #bottom outputs)]
- [{.#Some bottomI} {.#Some bottomO}]
- (monad.do meta.monad
- [inputC (singleton (macro.full_expansion (stack_mix (the #top inputs) bottomI)))
- outputC (singleton (macro.full_expansion (stack_mix (the #top outputs) bottomO)))]
- (in (list (` (-> (~ (de_alias inputC))
- (~ (de_alias outputC)))))))
-
- [?bottomI ?bottomO]
- (with_symbols [g!stack]
- (monad.do meta.monad
- [inputC (singleton (macro.full_expansion (stack_mix (the #top inputs) (maybe.else g!stack ?bottomI))))
- outputC (singleton (macro.full_expansion (stack_mix (the #top outputs) (maybe.else g!stack ?bottomO))))]
- (with_symbols [g!_]
- (in (list (` (All ((~ g!_) (~ g!stack))
- (-> (~ (de_alias inputC))
- (~ (de_alias outputC))))))))))))))
-
-(def: beginning
- Any
- [])
-
-(def: end
- (All (_ a) (-> [Any a] a))
- (function (_ [_ top])
- top))
-
-(def: .public ||>
- (syntax (_ [commands (<>.some <code>.any)])
- (in (list (` (|> (~! ..beginning) (~+ commands) ((~! ..end))))))))
-
-(def: word
- (Parser [Code Text Code (List Code)])
- (|export|.parser
- (all <>.and
- <code>.local
- <code>.any
- (<>.many <code>.any))))
-
-(def: .public word:
- (syntax (_ [[export_policy name type commands] ..word])
- (in (list (` (def: (~ export_policy) (~ (code.local name))
- (~ type)
- (|>> (~+ commands))))))))
+ (syntax (_ [inputs stack
+ outputs stack])
+ (with_symbols [g!_ common_bottom]
+ (let [input_bottom (maybe.else common_bottom (the #bottom inputs))
+ output_bottom (maybe.else common_bottom (the #bottom outputs))
+ input_stack (stack_type (the #top inputs) input_bottom)
+ output_stack (stack_type (the #top outputs) output_bottom)]
+ (in (list (.if (or (same? common_bottom input_bottom)
+ (same? common_bottom output_bottom))
+ (` (All ((~ g!_) (~ common_bottom))
+ (-> (~ input_stack)
+ (~ output_stack))))
+ (` (-> (~ input_stack)
+ (~ output_stack))))))))))
+
+(def: .public (value it)
+ (All (_ ,,, a)
+ (-> (=> []
+ ,,, [a])
+ a))
+ (|> [] it product.right))
(def: .public apply
(syntax (_ [arity (<>.only (n.> 0) <code>.nat)])
@@ -141,7 +86,7 @@
(-> (-> (~+ g!inputs) (~ g!output))
(=> [(~+ g!inputs)] [(~ g!output)])))
(function ((~ g!_) (~ g!func))
- (function ((~ g!_) (~ (stack_mix g!inputs g!stack)))
+ (function ((~ g!_) (~ (stack_type g!inputs g!stack)))
[(~ g!stack) ((~ g!func) (~+ g!inputs))]))))))))))
(with_template [<arity>]
@@ -177,12 +122,12 @@
(function (_ [[stack l] r])
[[stack r] l]))
-(def: .public rotL
+(def: .public left_rotation
(All (_ a b c) (=> [a b c] [b c a]))
(function (_ [[[stack a] b] c])
[[[stack b] c] a]))
-(def: .public rotR
+(def: .public right_rotation
(All (_ a b c) (=> [a b c] [c a b]))
(function (_ [[[stack a] b] c])
[[[stack c] a] b]))
@@ -192,12 +137,12 @@
(function (_ [[stack l] r])
[stack [l r]]))
-(def: .public ||L
+(def: .public left
(All (_ a b) (=> [a] [(Or a b)]))
(function (_ [stack l])
[stack {0 #0 l}]))
-(def: .public ||R
+(def: .public right
(All (_ a b) (=> [b] [(Or a b)]))
(function (_ [stack r])
[stack {0 #1 r}]))
@@ -255,9 +200,10 @@
(def: .public if
(All (_ ,,,0 ,,,1)
- (=> [then (=> ,,,0 ,,,1)
- else (=> ,,,0 ,,,1)]
- ,,,0 [Bit then else] ,,,1))
+ (type.let [then (=> ,,,0 ,,,1)
+ else (=> ,,,0 ,,,1)]
+ (=> ,,,0 [Bit then else]
+ ,,,1)))
(function (_ [[[stack test] then] else])
(.if test
(then stack)
@@ -265,15 +211,18 @@
(def: .public call
(All (_ ,,,0 ,,,1)
- (=> [quote (=> ,,,0 ,,,1)]
- ,,,0 [quote] ,,,1))
+ (type.let [quote (=> ,,,0 ,,,1)]
+ (=> ,,,0 [quote]
+ ,,,1)))
(function (_ [stack quote])
(quote stack)))
(def: .public loop
(All (_ ,,,)
- (=> [test (=> ,,, ,,, [Bit])]
- ,,, [test] ,,,))
+ (type.let [test (=> ,,,
+ ,,, [Bit])]
+ (=> ,,, [test]
+ ,,,)))
(function (loop [stack pred])
(let [[stack' verdict] (pred stack)]
(.if verdict
@@ -296,19 +245,19 @@
(def: .public do
(All (_ ,,,0 ,,,1)
- (=> [body (=> ,,,0 ,,,1)
- pred (=> ,,,1 ,,,0 [Bit])]
- ,,,0 [pred body]
- ,,,1 [pred body]))
+ (type.let [body (=> ,,,0 ,,,1)
+ pred (=> ,,,1 ,,,0 [Bit])]
+ (=> ,,,0 [pred body]
+ ,,,1 [pred body])))
(function (_ [[stack pred] body])
[[(body stack) pred] body]))
(def: .public while
(All (_ ,,,0 ,,,1)
- (=> [body (=> ,,,1 ,,,0)
- pred (=> ,,,0 ,,,1 [Bit])]
- ,,,0 [pred body]
- ,,,1))
+ (type.let [body (=> ,,,1 ,,,0)
+ pred (=> ,,,0 ,,,1 [Bit])]
+ (=> ,,,0 [pred body]
+ ,,,1)))
(function (while [[stack pred] body])
(let [[stack' verdict] (pred stack)]
(.if verdict
@@ -329,20 +278,20 @@
(function (_ [[stack arg] quote])
[stack (|>> (push arg) quote)]))
-(word: .public when
+(def: .public when
(All (_ ,,,)
- (=> [body (=> ,,, ,,,)]
- ,,, [Bit body]
- ,,,))
- swap
- (push ..call)
- (push ..drop)
- if)
-
-(word: .public ?
+ (type.let [body (=> ,,, ,,,)]
+ (=> ,,, [Bit body]
+ ,,,)))
+ (|>> swap
+ (push ..call)
+ (push ..drop)
+ if))
+
+(def: .public ?
(All (_ a)
(=> [Bit a a] [a]))
- rotL
- (push ..drop)
- (push ..nip)
- if)
+ (|>> left_rotation
+ (push ..drop)
+ (push ..nip)
+ if))
diff --git a/stdlib/source/library/lux/data/format/css/value.lux b/stdlib/source/library/lux/data/format/css/value.lux
index ad27c40b7..79636d63a 100644
--- a/stdlib/source/library/lux/data/format/css/value.lux
+++ b/stdlib/source/library/lux/data/format/css/value.lux
@@ -33,8 +33,8 @@
(syntax (_ [symbol <code>.text])
(in (list (code.local (text.replaced "-" "_" symbol))))))
-(def: enumeration:
- (template (enumeration: <abstraction> <representation> <out> <sample>+ <definition>+)
+(def: enumeration
+ (template (_ <abstraction> <representation> <out> <sample>+ <definition>+)
[(primitive: .public <abstraction>
<representation>
@@ -793,11 +793,13 @@
(format name)
abstraction))
- (enumeration: Step Text
- step
- [[start "start"]
- [end "end"]]
- [])
+ (enumeration
+ Step
+ Text
+ step
+ [[start "start"]
+ [end "end"]]
+ [])
(def: .public (steps intervals step)
(-> Nat Step (Value Timing))
@@ -1055,19 +1057,23 @@
(list)
(..apply "url")))
- (enumeration: Shape Text
- shape
- [[ellipse_shape "ellipse"]
- [circle_shape "circle"]]
- [])
-
- (enumeration: Extent Text
- extent
- [[closest_side "closest-side"]
- [closest_corner "closest-corner"]
- [farthest_side "farthest-side"]
- [farthest_corner "farthest-corner"]]
- [])
+ (enumeration
+ Shape
+ Text
+ shape
+ [[ellipse_shape "ellipse"]
+ [circle_shape "circle"]]
+ [])
+
+ (enumeration
+ Extent
+ Text
+ extent
+ [[closest_side "closest-side"]
+ [closest_corner "closest-corner"]
+ [farthest_side "farthest-side"]
+ [farthest_corner "farthest-corner"]]
+ [])
(with_template [<name> <function>]
[(def: .public (<name> shape extent location start next)
@@ -1142,28 +1148,30 @@
(-> URL (Value Content))
(|>> (list) (..apply "url")))
- (enumeration: Font Text
- font_name
- [[serif "serif"]
- [sans_serif "sans-serif"]
- [cursive "cursive"]
- [fantasy "fantasy"]
- [monospace "monospace"]]
- [(def: .public font
- (-> Text Font)
- (|>> %.text abstraction))
-
- (def: .public (font_family options)
- (-> (List Font) (Value Font))
- (case options
- {.#Item _}
- (|> options
- (list#each ..font_name)
- (text.interposed ",")
- (abstraction Value))
-
- {.#End}
- ..initial))])
+ (enumeration
+ Font
+ Text
+ font_name
+ [[serif "serif"]
+ [sans_serif "sans-serif"]
+ [cursive "cursive"]
+ [fantasy "fantasy"]
+ [monospace "monospace"]]
+ [(def: .public font
+ (-> Text Font)
+ (|>> %.text abstraction))
+
+ (def: .public (font_family options)
+ (-> (List Font) (Value Font))
+ (case options
+ {.#Item _}
+ (|> options
+ (list#each ..font_name)
+ (text.interposed ",")
+ (abstraction Value))
+
+ {.#End}
+ ..initial))])
(def: .public font_size
(-> (Value Length) (Value Font_Size))
@@ -1212,22 +1220,24 @@
(-> Nat Nat (Value Ratio))
(abstraction (format (%.nat numerator) "/" (%.nat denominator))))
- (enumeration: Quote Text
- quote_text
- [[double_quote "\0022"]
- [single_quote "\0027"]
- [single_left_angle_quote "\2039"]
- [single_right_angle_quote "\203A"]
- [double_left_angle_quote "\00AB"]
- [double_right_angle_quote "\00BB"]
- [single_left_quote "\2018"]
- [single_right_quote "\2019"]
- [double_left_quote "\201C"]
- [double_right_quote "\201D"]
- [low_double_quote "\201E"]]
- [(def: .public quote
- (-> Text Quote)
- (|>> abstraction))])
+ (enumeration
+ Quote
+ Text
+ quote_text
+ [[double_quote "\0022"]
+ [single_quote "\0027"]
+ [single_left_angle_quote "\2039"]
+ [single_right_angle_quote "\203A"]
+ [double_left_angle_quote "\00AB"]
+ [double_right_angle_quote "\00BB"]
+ [single_left_quote "\2018"]
+ [single_right_quote "\2019"]
+ [double_left_quote "\201C"]
+ [double_right_quote "\201D"]
+ [low_double_quote "\201E"]]
+ [(def: .public quote
+ (-> Text Quote)
+ (|>> abstraction))])
(def: quote_separator " ")
diff --git a/stdlib/source/test/lux/control/concatenative.lux b/stdlib/source/test/lux/control/concatenative.lux
index 354cc744a..4092dbd0d 100644
--- a/stdlib/source/test/lux/control/concatenative.lux
+++ b/stdlib/source/test/lux/control/concatenative.lux
@@ -17,7 +17,7 @@
["r" rev]
["f" frac]]]]]
[\\library
- ["[0]" / (.only word: => ||>)]])
+ ["[0]" / (.only =>)]])
(def: stack_shuffling
Test
@@ -27,68 +27,68 @@
(`` (all _.and
(_.coverage [/.push]
(n.= sample
- (||> (/.push sample))))
+ (/.value (/.push sample))))
(_.coverage [/.drop]
(n.= sample
- (||> (/.push sample)
- (/.push dummy)
- /.drop)))
+ (/.value (|>> (/.push sample)
+ (/.push dummy)
+ /.drop))))
(_.coverage [/.nip]
(n.= sample
- (||> (/.push dummy)
- (/.push sample)
- /.nip)))
+ (/.value (|>> (/.push dummy)
+ (/.push sample)
+ /.nip))))
(_.coverage [/.dup]
- (||> (/.push sample)
- /.dup
- /.n/=))
+ (/.value (|>> (/.push sample)
+ /.dup
+ /.n/=)))
(_.coverage [/.swap]
(n.= sample
- (||> (/.push sample)
- (/.push dummy)
- /.swap)))
- (_.coverage [/.rotL]
+ (/.value (|>> (/.push sample)
+ (/.push dummy)
+ /.swap))))
+ (_.coverage [/.left_rotation]
(n.= sample
- (||> (/.push sample)
- (/.push dummy)
- (/.push dummy)
- /.rotL)))
- (_.coverage [/.rotR]
+ (/.value (|>> (/.push sample)
+ (/.push dummy)
+ (/.push dummy)
+ /.left_rotation))))
+ (_.coverage [/.right_rotation]
(n.= sample
- (||> (/.push dummy)
- (/.push sample)
- (/.push dummy)
- /.rotR)))
+ (/.value (|>> (/.push dummy)
+ (/.push sample)
+ (/.push dummy)
+ /.right_rotation))))
(_.coverage [/.&&]
- (let [[left right] (||> (/.push sample)
- (/.push dummy)
- /.&&)]
+ (let [[left right] (/.value (|>> (/.push sample)
+ (/.push dummy)
+ /.&&))]
(and (n.= sample left)
(n.= dummy right))))
(~~ (with_template [<function> <tag>]
[(_.coverage [<function>]
((sum.equivalence n.= n.=)
{<tag> sample}
- (||> (/.push sample)
- <function>)))]
+ (/.value (|>> (/.push sample)
+ <function>))))]
- [/.||L .#Left]
- [/.||R .#Right]))
+ [/.left .#Left]
+ [/.right .#Right]))
(_.coverage [/.dip]
(n.= (++ sample)
- (||> (/.push sample)
- (/.push dummy)
- (/.push (/.apply_1 ++))
- /.dip
- /.drop)))
+ (/.value (|>> (/.push sample)
+ (/.push dummy)
+ (/.push (/.apply_1 ++))
+ /.dip
+ /.drop))))
(_.coverage [/.dip_2]
(n.= (++ sample)
- (||> (/.push sample)
- (/.push dummy)
- (/.push dummy)
- (/.push (/.apply_1 ++))
- /.dip_2
- /.drop /.drop)))
+ (/.value (|>> (/.push sample)
+ (/.push dummy)
+ (/.push dummy)
+ (/.push (/.apply_1 ++))
+ /.dip_2
+ /.drop /.drop))))
))))
(def: !numerical
@@ -103,17 +103,17 @@
(~~ (with_template [<concatenative> <functional>]
[(_.coverage [<concatenative>]
(<=> (<functional> parameter subject)
- (||> (/.push subject)
- (/.push parameter)
- <concatenative>)))]
+ (/.value (|>> (/.push subject)
+ (/.push parameter)
+ <concatenative>))))]
<arithmetic>'))
(~~ (with_template [<concatenative> <functional>]
[(_.coverage [<concatenative>]
(bit#= (<functional> parameter subject)
- (||> (/.push subject)
- (/.push parameter)
- <concatenative>)))]
+ (/.value (|>> (/.push subject)
+ (/.push parameter)
+ <concatenative>))))]
<order>'))
)))))]))
@@ -149,167 +149,166 @@
(all _.and
(_.coverage [/.call /.apply_1]
(n.= (++ sample)
- (||> (/.push sample)
- (/.push (/.apply_1 ++))
- /.call)))
+ (/.value (|>> (/.push sample)
+ (/.push (/.apply_1 ++))
+ /.call))))
(_.coverage [/.apply_2]
(n.= (n.+ sample sample)
- (||> (/.push sample)
- (/.push sample)
- (/.push (/.apply_2 n.+))
- /.call)))
+ (/.value (|>> (/.push sample)
+ (/.push sample)
+ (/.push (/.apply_2 n.+))
+ /.call))))
(_.coverage [/.apply_3]
(n.= (all n.+ sample sample sample)
- (||> (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push (/.apply_3 (function (_ i0 i1 i2)
- (all n.+ i0 i1 i2))))
- /.call)))
+ (/.value (|>> (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push (/.apply_3 (function (_ i0 i1 i2)
+ (all n.+ i0 i1 i2))))
+ /.call))))
(_.coverage [/.apply_4]
(n.= (all n.+ sample sample sample sample)
- (||> (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push (/.apply_4 (function (_ i0 i1 i2 i3)
- (all n.+ i0 i1 i2 i3))))
- /.call)))
+ (/.value (|>> (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push (/.apply_4 (function (_ i0 i1 i2 i3)
+ (all n.+ i0 i1 i2 i3))))
+ /.call))))
(_.coverage [/.apply_5]
(n.= (all n.+ sample sample sample sample sample)
- (||> (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push (/.apply_5 (function (_ i0 i1 i2 i3 i4)
- (all n.+ i0 i1 i2 i3 i4))))
- /.call)))
+ (/.value (|>> (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push (/.apply_5 (function (_ i0 i1 i2 i3 i4)
+ (all n.+ i0 i1 i2 i3 i4))))
+ /.call))))
(_.coverage [/.apply_6]
(n.= (all n.+ sample sample sample sample sample sample)
- (||> (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push (/.apply_6 (function (_ i0 i1 i2 i3 i4 i5)
- (all n.+ i0 i1 i2 i3 i4 i5))))
- /.call)))
+ (/.value (|>> (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push (/.apply_6 (function (_ i0 i1 i2 i3 i4 i5)
+ (all n.+ i0 i1 i2 i3 i4 i5))))
+ /.call))))
(_.coverage [/.apply_7]
(n.= (all n.+ sample sample sample sample sample sample sample)
- (||> (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push (/.apply_7 (function (_ i0 i1 i2 i3 i4 i5 i6)
- (all n.+ i0 i1 i2 i3 i4 i5 i6))))
- /.call)))
+ (/.value (|>> (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push (/.apply_7 (function (_ i0 i1 i2 i3 i4 i5 i6)
+ (all n.+ i0 i1 i2 i3 i4 i5 i6))))
+ /.call))))
(_.coverage [/.apply_8]
(n.= (all n.+ sample sample sample sample sample sample sample sample)
- (||> (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push (/.apply_8 (function (_ i0 i1 i2 i3 i4 i5 i6 i7)
- (all n.+ i0 i1 i2 i3 i4 i5 i6 i7))))
- /.call)))
+ (/.value (|>> (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push (/.apply_8 (function (_ i0 i1 i2 i3 i4 i5 i6 i7)
+ (all n.+ i0 i1 i2 i3 i4 i5 i6 i7))))
+ /.call))))
(_.coverage [/.apply]
(n.= (all n.+ sample sample sample sample sample sample sample sample sample)
- (||> (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push sample)
- (/.push ((/.apply 9) (function (_ i0 i1 i2 i3 i4 i5 i6 i7 i8)
- (all n.+ i0 i1 i2 i3 i4 i5 i6 i7 i8))))
- /.call)))
+ (/.value (|>> (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push sample)
+ (/.push ((/.apply 9) (function (_ i0 i1 i2 i3 i4 i5 i6 i7 i8)
+ (all n.+ i0 i1 i2 i3 i4 i5 i6 i7 i8))))
+ /.call))))
(_.coverage [/.if]
(n.= (if choice
(++ sample)
(-- sample))
- (||> (/.push sample)
- (/.push choice)
- (/.push (/.apply_1 ++))
- (/.push (/.apply_1 --))
- /.if)))
+ (/.value (|>> (/.push sample)
+ (/.push choice)
+ (/.push (/.apply_1 ++))
+ (/.push (/.apply_1 --))
+ /.if))))
(_.coverage [/.loop]
(n.= (n.+ distance start)
- (||> (/.push start)
- (/.push (is (/.=> [Nat] [Nat Bit])
- (|>> |++| /.dup |test|)))
- /.loop)))
+ (/.value (|>> (/.push start)
+ (/.push (is (/.=> [Nat] [Nat Bit])
+ (|>> |++| /.dup |test|)))
+ /.loop))))
(_.coverage [/.while]
(n.= (n.+ distance start)
- (||> (/.push start)
- (/.push (is (/.=> [Nat] [Nat Bit])
- (|>> /.dup |test|)))
- (/.push |++|)
- /.while)))
+ (/.value (|>> (/.push start)
+ (/.push (is (/.=> [Nat] [Nat Bit])
+ (|>> /.dup |test|)))
+ (/.push |++|)
+ /.while))))
(_.coverage [/.do]
(n.= (++ sample)
- (||> (/.push sample)
- (/.push (is (/.=> [] [Bit])
- (|>> (/.push false))))
- (/.push |++|)
- /.do /.while)))
+ (/.value (|>> (/.push sample)
+ (/.push (is (/.=> [] [Bit])
+ (|>> (/.push false))))
+ (/.push |++|)
+ /.do /.while))))
(_.coverage [/.compose]
(n.= (++ (++ sample))
- (||> (/.push sample)
- (/.push |++|)
- (/.push |++|)
- /.compose
- /.call)))
+ (/.value (|>> (/.push sample)
+ (/.push |++|)
+ (/.push |++|)
+ /.compose
+ /.call))))
(_.coverage [/.partial]
(n.= (n.+ sample sample)
- (||> (/.push sample)
- (/.push sample)
- (/.push (/.apply_2 n.+))
- /.partial
- /.call)))
+ (/.value (|>> (/.push sample)
+ (/.push sample)
+ (/.push (/.apply_2 n.+))
+ /.partial
+ /.call))))
(_.coverage [/.when]
(n.= (if choice
(++ sample)
sample)
- (||> (/.push sample)
- (/.push choice)
- (/.push (/.apply_1 ++))
- /.when)))
+ (/.value (|>> (/.push sample)
+ (/.push choice)
+ (/.push (/.apply_1 ++))
+ /.when))))
(_.coverage [/.?]
(n.= (if choice
(++ sample)
(-- sample))
- (||> (/.push choice)
- (/.push (++ sample))
- (/.push (-- sample))
- /.?)))
+ (/.value (|>> (/.push choice)
+ (/.push (++ sample))
+ (/.push (-- sample))
+ /.?))))
)))
-(word: square
+(def: square
(=> [Nat] [Nat])
-
- /.dup
- (/.apply_2 n.*))
+ (|>> /.dup
+ (/.apply_2 n.*)))
(def: definition
Test
(do random.monad
[sample random.nat]
- (_.coverage [/.word: /.=> /.||>]
+ (_.coverage [/.=> /.value]
(n.= (n.* sample sample)
- (||> (/.push sample)
- ..square)))))
+ (/.value (|>> (/.push sample)
+ ..square))))))
(def: .public test
Test
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 12:01:16 +0000