word.bend source

word.bend on the hub · documented module

# word.bend: the vocabulary wordlib's laws are stated in.import Base# a bit as a Natdef b2n(b: Bool) -> Nat:  match b:    case False{}:      0n    case True{}:      1n# p if k, else 0ndef scale(k: Bool, p: Nat) -> Nat:  match k:    case False{}:      0n    case True{}:      pdef pow2(n: Nat) -> Nat:  match n:    case 0n:      1n    case 1n+p:      Nat.double(pow2(p))# majority of three bits: a full adder's carry outdef maj(a: Bool, b: Bool, c: Bool) -> Bool:  match a b c:    case False{} False{} _:      False{}    case True{} True{} _:      True{}    case False{} True{} _:      c    case True{} False{} _:      c# the carry out of Word.adc's add: the bit an n-bit sum overflows intodef carry(n: Nat, a: Word(n), b: Word(n), c: Bool) -> Bool:  match n:    case 0n:      c    case 1n+p:      match a b:        case WCon{ab, at} WCon{bb, bt}:          carry(p, at, bt, maj(ab, bb, c))# the bit Word.shl.put(n, c, w) shifts out: w's top bit, or c when n is 0def top(n: Nat, c: Bool, w: Word(n)) -> Bool:  match n:    case 0n:      c    case 1n+p:      match w:        case WCon{b, t}:          top(p, b, t)# the lowest bit (False for the empty word)def lsb(n: Nat, w: Word(n)) -> Bool:  match n:    case 0n:      False{}    case 1n+p:      match w:        case WCon{b, t}:          b