Binary addition on bytes in Formality - Does not yet fuse

ByteFusion2.fm

// npm i -g [email protected]
// fm -t ByteFusion2/main && fm -o ByteFusion2/main

// INats serve as the base for fused iteration

// The inductive hypothesis on nats. Erases to Church.
INat : Type
  ${self}
  ( P     : INat -> Type;
    izero : P(izero),
    isucc : (r : INat; i : P(r)) -> P(isucc(r))
  ) -> P(self)

// INat successor
isucc(r : INat) : INat
  new(INat) (P; izero, isucc) =>
  let izero = izero
  let isucc = isucc
  let irest = (use(r))((x) => P(x); izero, isucc)
  isucc(r; irest)

// INat zero
izero : INat
  new(INat) (P; izero, isucc) =>
  let izero = izero
  let isucc = isucc
  izero

// Doubles an INat.
imul2(n: INat) : INat
  new(INat) (P; b, s) =>
  let b = b
  let s = s
  let t = (n) => P(imul2(n))
  let s = (n; i) => s(isucc(imul2(n)); s(imul2(n); i))
  (use(n))(t; b, s)
  
// Simple induction is recursion.
recurse(n: INat, P: Type; z: P, s: P -> P) : P
  let s = s
  (use(n))((x) => P; z, (i;) => s)


T Bit
| z
| o

T Byte
| byte(b0: Bit, b1: Bit, b2: Bit, b3: Bit, b4: Bit, b5: Bit, b6: Bit, b7: Bit)

byte_to_num(byte0: Byte) : Number
  case byte0
  | byte =>
  	let n0 = bit_to_num(byte0.b0, 1)
  	let n1 = bit_to_num(byte0.b1, 2)
  	let n2 = bit_to_num(byte0.b2, 4)
  	let n3 = bit_to_num(byte0.b3, 8)
  	let n4 = bit_to_num(byte0.b4, 16)
  	let n5 = bit_to_num(byte0.b5, 32)
  	let n6 = bit_to_num(byte0.b6, 64)
  	let n7 = bit_to_num(byte0.b7, 128)
  	(n0 .+. n1 .+. n2 .+. n3 .+. n4 .+. n5 .+. n6 .+. n7)

bit_to_num(b : Bit, n : Number) : Number
  case b
  | z => 0
  | o => n

byte_zero : Byte
  byte(z, z, z, z, z, z, z, z)

byte_one : Byte
  byte(o, z, z, z, z, z, z, z)

bit_xor(b0: Bit, b1: Bit) : Bit
  new(Bit) (P; zf, of) =>
    case b0
    + of : P(o)
    + zf : P(z)
    + b1 : Bit
    | z =>
    	case b1
    	| z => zf
    	| o => of
    	: P(bit_xor(z, b1))
    | o  =>
    	case b1
    	| z => of
    	| o => zf
    	: P(bit_xor(o, b1))
    : P(bit_xor(b0, b1))

bit_and(b0: Bit, b1: Bit) : Bit
  new(Bit) (P; zf, of) =>
    case b0
    + of : P(o)
    + zf : P(z)
    | z => zf
    | o  =>
    	case b1
    	| z => zf
    	| o => of
    	: P(bit_and(o, b1))
    : P(bit_and(b0, b1))

bit_not_zero(b0: Bit, b1: Bit) : Bit
  new(Bit) (P; zf, of) =>
    case b0
    + of : P(o)
    + zf : P(z)
    | z =>
    	case b1
    	| z => zf
    	| o => of
    	: P(bit_not_zero(z, b1))
    | o => of
    : P(bit_not_zero(b0, b1))
    
bit_sum(b0: Bit, b1: Bit, carry: Bit) : Bit
  bit_xor(carry, bit_xor(b0, b1))

bit_carry(b0: Bit, b1: Bit, carry: Bit) : Bit
  bit_not_zero(bit_and(b0, b1), bit_and(carry, bit_xor(b0, b1)))

byte_add(byte0: Byte, byte1: Byte) : Byte
  new(Byte) (P; bytef) =>
  case byte0
  | byte =>
    case byte1
    | byte =>
      let b0 = bit_sum(byte0.b0, byte1.b0, z)
      let c0 = bit_carry(byte0.b0, byte1.b0, z)

      let b1 = bit_sum(byte0.b1, byte1.b1, c0)
      let c1 = bit_carry(byte0.b1, byte1.b1, c0)

      let b2 = bit_sum(byte0.b2, byte1.b2, c1)
      let c2 = bit_carry(byte0.b2, byte1.b2, c1)

      let b3 = bit_sum(byte0.b3, byte1.b3, c2)
      let c3 = bit_carry(byte0.b3, byte1.b3, c2)

      let b4 = bit_sum(byte0.b4, byte1.b4, c3)
      let c4 = bit_carry(byte0.b4, byte1.b4, c3)

      let b5 = bit_sum(byte0.b5, byte1.b5, c4)
      let c5 = bit_carry(byte0.b5, byte1.b5, c4)

      let b6 = bit_sum(byte0.b6, byte1.b6, c5)
      let c6 = bit_carry(byte0.b6, byte1.b6, c5)

      let b7 = bit_sum(byte0.b7, byte1.b7, c6)
      
      bytef(b0, b1, b2, b3, b4, b5, b6, b7)
      
    : P(byte_add(byte(byte0.b0, byte0.b1, byte0.b2, byte0.b3, byte0.b4, byte0.b5, byte0.b6, byte0.b7), byte1))
  : P(byte_add(byte0, byte1))


// check if fusion works by commenting in a higher number and seeing if the increase of rewrites is logarithmic or linear
main : Number
  let byte0 =
	recurse(128N, Byte; byte_zero, byte_add(byte_one))
  // recurse(2048N, Byte; byte_zero, byte_add(byte_one))
  // recurse(4294967296N, Byte; byte_zero, byte_add(byte_one))
  // recurse(4294967296N, Byte; byte_zero, byte_add(byte_one))

  byte_to_num(byte0)