|
1 | 1 | // -*- rust -*-
|
2 | 2 |
|
3 |
| -/* |
4 |
| -Module: bool |
5 |
| -
|
6 |
| -Classic Boolean logic reified as ADT |
7 |
| -*/ |
| 3 | +#[doc = "Classic Boolean logic reified as ADT"]; |
8 | 4 |
|
9 | 5 | export t;
|
10 | 6 | export not, and, or, xor, implies;
|
11 | 7 | export eq, ne, is_true, is_false;
|
12 | 8 | export from_str, to_str, all_values, to_bit;
|
13 | 9 |
|
14 |
| -/* |
15 |
| -Type: t |
16 |
| -
|
17 |
| -The type of boolean logic values |
18 |
| -*/ |
| 10 | +#[doc = "The type of boolean logic values"] |
19 | 11 | type t = bool;
|
20 | 12 |
|
21 |
| -/* Function: not |
22 |
| -
|
23 |
| -Negation/Inverse |
24 |
| -*/ |
| 13 | +#[doc( |
| 14 | + brief = "Negation/Inverse", |
| 15 | + args(v = "Value to Negate/Invert"), |
| 16 | + return = "Negated/Inverted Value" |
| 17 | +)] |
25 | 18 | pure fn not(v: t) -> t { !v }
|
26 | 19 |
|
27 |
| -/* Function: and |
28 |
| -
|
29 |
| -Conjunction |
30 |
| -*/ |
| 20 | +#[doc( |
| 21 | + brief = "Conjunction", |
| 22 | + args(a = "value `a`", |
| 23 | + b = "value `b`"), |
| 24 | + return = "`a` AND `b`" |
| 25 | +)] |
31 | 26 | pure fn and(a: t, b: t) -> t { a && b }
|
32 | 27 |
|
33 |
| -/* Function: or |
34 |
| -
|
35 |
| -Disjunction |
36 |
| -*/ |
| 28 | +#[doc( |
| 29 | + brief = "Disjunction", |
| 30 | + args(a = "value `a`", |
| 31 | + b = "value `b`"), |
| 32 | + return = "`a` OR `b`" |
| 33 | +)] |
37 | 34 | pure fn or(a: t, b: t) -> t { a || b }
|
38 | 35 |
|
39 |
| -/* |
40 |
| -Function: xor |
41 |
| -
|
42 |
| -Exclusive or, i.e. `or(and(a, not(b)), and(not(a), b))` |
43 |
| -*/ |
| 36 | +#[doc( |
| 37 | + brief = "Exclusive or, i.e. `or(and(a, not(b)), and(not(a), b))`", |
| 38 | + args(a = "value `a`", |
| 39 | + b = "value `b`"), |
| 40 | + return = "`a` XOR `b`" |
| 41 | +)] |
44 | 42 | pure fn xor(a: t, b: t) -> t { (a && !b) || (!a && b) }
|
45 | 43 |
|
46 |
| -/* |
47 |
| -Function: implies |
48 |
| -
|
49 |
| -Implication in the logic, i.e. from `a` follows `b` |
50 |
| -*/ |
| 44 | +#[doc( |
| 45 | + brief = "Implication in the logic, i.e. from `a` follows `b`", |
| 46 | + args(a = "value `a`", |
| 47 | + b = "value `b`"), |
| 48 | + return = "`a` IMPLIES `b`" |
| 49 | +)] |
51 | 50 | pure fn implies(a: t, b: t) -> t { !a || b }
|
52 | 51 |
|
53 |
| -/* |
54 |
| -Predicate: eq |
55 |
| -
|
56 |
| -Returns: |
57 |
| -
|
58 |
| -true if truth values `a` and `b` are indistinguishable in the logic |
59 |
| -*/ |
| 52 | +#[doc( |
| 53 | + brief = "true if truth values `a` and `b` are indistinguishable in the logic", |
| 54 | + args(a = "value `a`", |
| 55 | + b = "value `b`"), |
| 56 | + return = "`a` == `b`" |
| 57 | +)] |
60 | 58 | pure fn eq(a: t, b: t) -> bool { a == b }
|
61 | 59 |
|
62 |
| -/* |
63 |
| -Predicate: ne |
64 |
| -
|
65 |
| -Returns: |
66 |
| -
|
67 |
| -true if truth values `a` and `b` are distinguishable in the logic |
68 |
| -*/ |
| 60 | +#[doc( |
| 61 | + brief = "true if truth values `a` and `b` are distinguishable in the logic", |
| 62 | + args(a = "value `a`", |
| 63 | + b = "value `b`"), |
| 64 | + return = "`a` != `b`" |
| 65 | +)] |
69 | 66 | pure fn ne(a: t, b: t) -> bool { a != b }
|
70 | 67 |
|
71 |
| -/* |
72 |
| -Predicate: is_true |
73 |
| -
|
74 |
| -Returns: |
75 |
| -
|
76 |
| -true if `v` represents truth in the logic |
77 |
| -*/ |
| 68 | +#[doc( |
| 69 | + brief = "true if `v` represents truth in the logic", |
| 70 | + args(v = "value `v`"), |
| 71 | + return = "bool(`v`)" |
| 72 | +)] |
78 | 73 | pure fn is_true(v: t) -> bool { v }
|
79 | 74 |
|
80 |
| -/* |
81 |
| -Predicate: is_false |
82 |
| -
|
83 |
| -Returns: |
84 |
| -
|
85 |
| -true if `v` represents falsehood in the logic |
86 |
| -*/ |
| 75 | +#[doc( |
| 76 | + brief = "true if `v` represents falsehood in the logic", |
| 77 | + args(v = "value `v`"), |
| 78 | + return = "bool(!`v`)" |
| 79 | +)] |
87 | 80 | pure fn is_false(v: t) -> bool { !v }
|
88 | 81 |
|
89 |
| -/* |
90 |
| -Function: from_str |
91 |
| -
|
92 |
| -Parse logic value from `s` |
93 |
| -*/ |
| 82 | +#[doc( |
| 83 | + brief = "Parse logic value from `s`", |
| 84 | + args(v = "string value `s`"), |
| 85 | + return = "true if `s` equals \"true\", else false" |
| 86 | +)] |
94 | 87 | pure fn from_str(s: str) -> t {
|
95 | 88 | alt s {
|
96 | 89 | "true" { true }
|
97 | 90 | "false" { false }
|
98 | 91 | }
|
99 | 92 | }
|
100 | 93 |
|
101 |
| -/* |
102 |
| -Function: to_str |
103 |
| -
|
104 |
| -Convert `v` into a string |
105 |
| -*/ |
| 94 | +#[doc( |
| 95 | + brief = "Convert `v` into a string", |
| 96 | + args(v = "truth value `v`"), |
| 97 | + return = "\"true\" if value `v` is true, else \"false\"" |
| 98 | +)] |
106 | 99 | pure fn to_str(v: t) -> str { if v { "true" } else { "false" } }
|
107 | 100 |
|
108 |
| -/* |
109 |
| -Function: all_values |
110 |
| -
|
111 |
| -Iterates over all truth values by passing them to `blk` |
112 |
| -in an unspecified order |
113 |
| -*/ |
| 101 | +#[doc( |
| 102 | + brief = "Iterates over all truth values by passing them to `blk` in an unspecified order", |
| 103 | + args(v = "block value `v`"), |
| 104 | + return = "Undefined return value" |
| 105 | +)] |
114 | 106 | fn all_values(blk: block(v: t)) {
|
115 | 107 | blk(true);
|
116 | 108 | blk(false);
|
117 | 109 | }
|
118 | 110 |
|
119 |
| -/* |
120 |
| -Function: to_bit |
121 |
| -
|
122 |
| -Returns: |
123 |
| -
|
124 |
| -An u8 whose first bit is set if `if_true(v)` holds |
125 |
| -*/ |
| 111 | +#[doc( |
| 112 | + brief = "converts truth value to an 8 bit byte", |
| 113 | + args(v = "value `v`"), |
| 114 | + return = "returns byte with value 1 if `v` has truth value of true, else 0" |
| 115 | +)] |
126 | 116 | pure fn to_bit(v: t) -> u8 { if v { 1u8 } else { 0u8 } }
|
127 | 117 |
|
128 | 118 | // Local Variables:
|
|
0 commit comments