// This program shows how to use BDD synthesis to produce the function
// producing the mapping from Net[4] -> Net[7] needed to display integer values
// in the range 0..15 on a 7-segment display.

import jazz.circuit.*;
import jazz.circuit.bdd.*;

// Segments for the first 16 digits: 0123456789abcdef
var segments = [#1111110, #0001100, #0110111, #0011111, #1001101, #1011011,
                #1111011, #0001110, #1111111, #1011111, #1101111, #1111001,
                #1110010, #0111101, #1110011, #1100011];
 
// Function boolean[4] -> boolean such that "segment(k)([a, b, c, d])" is
// true iff the display of the binary number "#abcd" requires segment k.
fun segment(k)(b: boolean[4]) = segments[s(0) + s(1) + s(2) + s(3)].bit(k) == 1
{
  fun s(i) = b[i] ? 1 << i : 0;
}

// Create 4 bdd variables
var vars = Bdd.newVars(4)(["d0", "d1", "d2", "d3"]);

// Compute the array of the seven bdds computing segment(0) ... segment(6)
var bdds = [k -> Bdd.fromFunction(4)(vars)(segment(k))];

// Create a decoder generator "decoder" that, when applied to the "zero" and
// "one" values of a boolean algebra "A", produces the decoder A[4] -> A[7].
var decoder = Bdd.toFunction(4)(vars)(7)(bdds);

// Decoder device
device Decoder {
  input digit: Net[4];
  output segments: Net[7];

  // Instanciate the decoder for nets
  var zero = Net.constant(#(0));
  var one = Net.constant(#(1));

  // Apply the decoder to compute the segments
  segments = decoder(zero, one)(digit);
}

// Export the device
export Decoder();

// Instanciate the decoder for booleans
var booleanDecoder = decoder(false, true);
  
// Display digit "n" using the decoder
fun display(n: int) = ()
{
  var s = booleanDecoder([i -> n.bit(i) == 1]);
  @ (print("%s%s%s\n",
           s[0] || s[5] ? "@" : " ",
           s[5] ? "@@" : "  ",
           s[4] || s[5] ? "@" : " ")
     ; print("%s  %s\n", s[0] ? "@" : " ", s[4] ? "@" : " ")
     ; print("%s  %s\n", s[0] ? "@" : " ", s[4] ? "@" : " ")
     ; print("%s%s%s\n",
             s[0] || s[1] || s[6] ? "@" : " ",
             s[6] ? "@@" : "  ",
             s[3] || s[4] || s[6] ? "@" : " ")
     ; print("%s  %s\n", s[1] ? "@" : " ", s[3] ? "@" : " ")
     ; print("%s  %s\n", s[1] ? "@" : " ", s[3] ? "@" : " ")
     ; print("%s%s%s\n\n",
             s[1] || s[2] ? "@" : " ",
             s[2] ? "@@" : "  ",
             s[2] || s[3] ? "@" : " "));
}
  
// Test the decoder exhaustively by displaying the segments of all the digits
for (n < 16) {
  @ display(n);
}