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# how many times Word.mul.go's result wrapped past 2^n: each step adds the# carry of acc + b (on a 1 bit) and, for every later bit of a, the top bit# that shl pushed out of bdef mulq(+n: Nat, m: Nat, a: Word(m), +b: Word(n), +acc: Word(n)) -> Nat:  match m:    case 0n:      0n    case 1n++mp:      match a:        case WCon{False{}, +at}:          Nat.add(mulq(n, mp, at, Word.shl(n, b), acc), Nat.mul(Word.to_nat(mp, at), b2n(top(n, False{}, b))))        case WCon{True{}, +at}:          Nat.add(mulq(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), Nat.add(Nat.mul(Word.to_nat(mp, at), b2n(top(n, False{}, b))), b2n(carry(n, acc, b, False{}))))