diff options
Diffstat (limited to '')
| -rw-r--r-- | lux-mode/lux-mode.el | 5 | ||||
| -rw-r--r-- | stdlib/source/documentation/lux/control/concatenative.lux | 88 | ||||
| -rw-r--r-- | stdlib/source/library/lux/control/concatenative.lux | 195 | ||||
| -rw-r--r-- | stdlib/source/library/lux/data/format/css/value.lux | 126 | ||||
| -rw-r--r-- | stdlib/source/test/lux/control/concatenative.lux | 323 |
5 files changed, 339 insertions, 398 deletions
diff --git a/lux-mode/lux-mode.el b/lux-mode/lux-mode.el index bf840e44e..7d9f18203 100644 --- a/lux-mode/lux-mode.el +++ b/lux-mode/lux-mode.el @@ -5,7 +5,7 @@ ;; Authors: Eduardo Julian <eduardoejp@gmail.com> ;; URL: https://github.com/LuxLang/lux/tree/master/lux-mode ;; Keywords: languages lisp lux -;; Version: 0.6.0 +;; Version: 0.6.6 ;; Package-Requires: ((emacs "24.1")) ;; This file is not part of GNU Emacs. @@ -393,13 +393,12 @@ Called by `imenu--generic-function'." (alternative-format (altRE "char" "bin" "oct" "hex")) (documentation (altRE "comment" "documentation:")) (function-application (altRE "|>" "<|" "left" "right" "all")) - (function-definition (altRE "function" "|>>" "<<|" "||>")) + (function-definition (altRE "function" "|>>" "<<|")) (remember (altRE "remember" "to_do" "fix_me")) (definition (altRE "\\.using" "def:" "type:" "program:" "inline:" "macro" "syntax" "exception:" - "word:" "analysis" "synthesis" "generation" "directive"))) (let ((control (altRE control//flow control//pattern-matching 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 |