Shows where Formality runtime fusion breaks down when attempting to add two bytes

ByteFusion.fm

// USES OLDER VERSION OF FORMALITY
// 
// npm i -g [email protected]
// fm -t ByteFusion/main; fm -o ByteFusion/main

T Bit
| z
| o

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

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

byte_one : Byte
  byte(o, z, z, z, z, z, z, z)
  
// The byte_add_primitive functions below do not actually
// perform addition on bytes
// but showcase what happens when one tries the first step of
// the most primitive method of performing addition

byte_add_primitive3(byte0: Byte, byte1: Byte) : Byte
  new(Byte) (P; bytef) =>
  	case byte0
  	| byte =>
  		case byte1
  		| byte =>
  			case byte0.b0
  			+ bytef : (b0: Bit, b1: Bit, b2: Bit, b3: Bit, b4: Bit, b5: Bit, b6: Bit, b7: Bit) ->
      			P(byte(b0, b1, b2, b3, b4, b5, b6, b7))
      	+ byte1.b0 : Bit
  			| z => bytef(z,z,z,z,z,z,z,z)
  			| o => bytef(z,z,z,z,z,z,z,z)
  			
        : P(byte_add_primitive3(
          	byte(byte0.b0, byte0.b1, byte0.b2, byte0.b3, byte0.b4, byte0.b5, byte0.b6, byte0.b7),
          	byte(byte1.b0, byte1.b1, byte1.b2, byte1.b3, byte1.b4, byte1.b5, byte1.b6, byte1.b7)))
          	
      : P(byte_add_primitive3(byte(byte0.b0, byte0.b1, byte0.b2, byte0.b3, byte0.b4, byte0.b5, byte0.b6, byte0.b7), byte1))
    : P(byte_add_primitive3(byte0, byte1))
    
byte_add_primitive4(byte0: Byte, byte1: Byte) : Byte
  new(Byte) (P; bytef) =>
  	case byte0
  	| byte =>
  		case byte1
  		| byte =>
  			case byte0.b0
  			+ bytef : (b0: Bit, b1: Bit, b2: Bit, b3: Bit, b4: Bit, b5: Bit, b6: Bit, b7: Bit) ->
      			P(byte(b0, b1, b2, b3, b4, b5, b6, b7))
      	+ byte1.b0 : Bit
  			| z => 
  				case byte1.b0
	  			+ bytef : (b0: Bit, b1: Bit, b2: Bit, b3: Bit, b4: Bit, b5: Bit, b6: Bit, b7: Bit) ->
      			P(byte(b0, b1, b2, b3, b4, b5, b6, b7))
  				| z => bytef(z,z,z,z,z,z,z,z)
  				| o => bytef(z,z,z,z,z,z,z,z)
          : P(byte_add_primitive4(
            	byte(z, byte0.b1, byte0.b2, byte0.b3, byte0.b4, byte0.b5, byte0.b6, byte0.b7),
            	byte(byte1.b0, byte1.b1, byte1.b2, byte1.b3, byte1.b4, byte1.b5, byte1.b6, byte1.b7)))
  			| o =>
  				case byte1.b0
	  			+ bytef : (b0: Bit, b1: Bit, b2: Bit, b3: Bit, b4: Bit, b5: Bit, b6: Bit, b7: Bit) ->
      			P(byte(b0, b1, b2, b3, b4, b5, b6, b7))
  				| z => bytef(z,z,z,z,z,z,z,z)
  				| o => bytef(z,z,z,z,z,z,z,z)
          : P(byte_add_primitive4(
            	byte(z, byte0.b1, byte0.b2, byte0.b3, byte0.b4, byte0.b5, byte0.b6, byte0.b7),
            	byte(byte1.b0, byte1.b1, byte1.b2, byte1.b3, byte1.b4, byte1.b5, byte1.b6, byte1.b7)))
  			
        : P(byte_add_primitive4(
          	byte(byte0.b0, byte0.b1, byte0.b2, byte0.b3, byte0.b4, byte0.b5, byte0.b6, byte0.b7),
          	byte(byte1.b0, byte1.b1, byte1.b2, byte1.b3, byte1.b4, byte1.b5, byte1.b6, byte1.b7)))
          	
      : P(byte_add_primitive4(byte(byte0.b0, byte0.b1, byte0.b2, byte0.b3, byte0.b4, byte0.b5, byte0.b6, byte0.b7), byte1))
    : P(byte_add_primitive4(byte0, byte1))

// 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) =>
  dup izero = izero
  dup isucc = isucc
  dup irest = (use(r))((x) => P(x); #izero, #isucc)
  # isucc(r; irest)

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

// Doubles an INat.
imul2(n: INat) : INat
  new(INat) (P; b, s) =>
  dup b = b
  dup 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
  dup s = s
  (use(n))((x) => P; z, #(i;) => s)

main : ! Byte
  // fusion works before case splitting on bit values
  
  // recurse(128N, Byte; #byte_zero, #byte_add_primitive3(byte_one))
  // recurse(2048N, Byte; #byte_zero, #byte_add_primitive3(byte_one))
  

  // fusion stops working after case splitting on bit values
  
  recurse(128N, Byte; #byte_zero, #byte_add_primitive4(byte_one))
  // recurse(2048N, Byte; #byte_zero, #byte_add_primitive4(byte_one))



// Below is another method that was attempted, without successful fusion
// T Byte
// | byte(b0: ! Bit, b1: ! Bit, b2: ! Bit, b3: ! Bit, b4: ! Bit, b5: ! Bit, b6: ! Bit, b7: ! Bit)

// 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_add_carry(o, b1))
//     : P(bit_add_carry(b0, b1))
  
// bit_add(b0: ! Bit, b1: ! Bit, bc: ! Bit) : [:!Bit, !Bit]
//   dup d_b0 = b0
//   dup d_b1 = b1
//   dup d_bc = bc
	
//   let r0 = bit_xor(d_b0, d_b1)
//   let r1 = bit_xor(r0, d_bc)
  
//   let r2 = bit_and(d_b0, d_b1)
//   let r3 = bit_xor(r2, d_bc)

//   [#r1, #r3]


// byte_add1(byte0: ! Byte, byte1: ! Byte) : ! Byte
//   byte0
  

// byte_add(byte0: Byte, byte1: Byte) : Byte
//   new(Byte) (P; bytef) =>
//   case byte0
//   | byte =>
//     case byte1
//     | byte =>
// 			get [b0_sum, b0_carry] = bit_add(byte0.b0, byte1.b0, #z)
//     	get [b1_sum, b1_carry] = bit_add(byte0.b1, byte1.b1, b0_carry)
//     	get [b2_sum, b2_carry] = bit_add(byte0.b2, byte1.b2, b1_carry)
//     	get [b3_sum, b3_carry] = bit_add(byte0.b3, byte1.b3, b2_carry)
//     	get [b4_sum, b4_carry] = bit_add(byte0.b4, byte1.b4, b3_carry)
//     	get [b5_sum, b5_carry] = bit_add(byte0.b5, byte1.b5, b4_carry)
//     	get [b6_sum, b6_carry] = bit_add(byte0.b6, byte1.b6, b5_carry)
//     	get [b7_sum, b7_carry] = bit_add(byte0.b7, byte1.b7, b6_carry)
    	
//       bytef(b0_sum, b1_sum, b2_sum, b3_sum, b4_sum, b5_sum, b6_sum, b7_sum)
      
//     : 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))