package jazz.circuit.expr;

//////////////////////////////////////////////////////////////////////////////
//
//  Imperative construction of circuits using boolean expressions
//
//  Author: Francois.Bourdoncle@ensmp.fr
//
//////////////////////////////////////////////////////////////////////////////

import jazz.unsafe.Hashtable;
import jazz.unsafe.Counter;

var defs = Hashtable.create();
var inids = Hashtable.create();
var dummy = new _VarExpr(id = 0);
var ids = Counter.create(1);

BoolExpr.constant(v) = new BoolExpr(e = new _CstExpr(v = v));
BoolExpr.newLocal() = new BoolExpr(e = new _VarExpr(id = ids.next()));
BoolExpr.newInput(n) = ( inids.put(id, n)
                       ; new BoolExpr(e = new _VarExpr(id = id)))
{
  id = ids.next();
}

// Sets or update the definition of boolean variables
setEq@BoolExpr(x) = (e.setEq(x.e) ; this);
setEq@_BoolExpr(e) = error("setEq@_BoolExpr");
setEq@_VarExpr(e) = defs.put(id, e);

setOr@BoolExpr(x) = (e.setOr(x.e) ; this);
setOr@_BoolExpr(e) = error("setOr@_BoolExpr");
setOr@_VarExpr(e) = defs.put(id, setOr(e, defs.get(id, dummy)))
{
  // Ignore "dummy" in the or
  fun setOr(e1: _BoolExpr, e2: _BoolExpr): _BoolExpr;
  setOr(e1, e2) = new _OrExpr(e1 = e1, e2 = e2);
  setOr(e1, e2@_VarExpr) = e2.id == 0 ? e1 : new _OrExpr(e1 = e1, e2 = e2);
}

setAnd@BoolExpr(x) = (e.setAnd(x.e) ; this);
setAnd@_BoolExpr(e) = error("setAnd@_BoolExpr");
setAnd@_VarExpr(e) = defs.put(id, setAnd(e, defs.get(id, dummy)))
{
  // Ignore "dummy" in the and
  fun setAnd(e1: _BoolExpr, e2: _BoolExpr): _BoolExpr;
  setAnd(e1, e2) = new _AndExpr(e1 = e1, e2 = e2);
  setAnd(e1, e2@_VarExpr) = e2.id == 0 ? e1 : new _AndExpr(e1 = e1, e2 = e2);
}

setXor@BoolExpr(x) = (e.setXor(x.e) ; this);
setXor@_BoolExpr(e) = error("setXor@_BoolExpr");
setXor@_VarExpr(e) = defs.put(id, setXor(e, defs.get(id, dummy)))
{
  // Ignore "dummy" in the xor
  fun setXor(e1: _BoolExpr, e2: _BoolExpr): _BoolExpr;
  setXor(e1, e2) = new _XorExpr(e1 = e1, e2 = e2);
  setXor(e1, e2@_VarExpr) = e2.id == 0 ? e1 : new _XorExpr(e1 = e1, e2 = e2);
}

// Returns the definition of a boolean expression
getDefinition@BoolExpr() = new BoolExpr(e = e.getDefinition());
getDefinition@_BoolExpr() = this;
getDefinition@_VarExpr() =
  defs.get(id, error("unassigned variable: %a", this));

// We create the lazy array "vars" of all boolean variables by a single
// equation involving the two hashtables containing the input variables (vars)
// and the definition of local variables (defs). This is the only way to
// instanciate a circuit. If the circuit contains loops (without registers)
// then the Jazz runtime will fail with unassigned variables (this is a bug in
// the generated circuit, not in the code that follows).
BoolExpr.instanciate(outputs)(inputs, reg, constant) =
  [i -> outputs[i].e.getValue(vars, reg, constant)]
{
  // The "vars" array is the array of all the variables in the circuit
  vars = [id -> val(id)];

  fun val(id) = (inids.containsKey(id) ?
                 inputs[inids.get(id, error("internal error"))] :
                 def(id).getValue(vars, reg, constant));
             
  fun def(id) = (_BoolExpr) defs.get(id, error("undefined variable: $%d", id));
}

getValue@_VarExpr(vars, reg, constant) = vars[id];
  
getValue@_CstExpr(vars, reg, constant) = constant(v);

getValue@_NotExpr(vars, reg, constant) = ~e.getValue(vars, reg, constant);

getValue@_RegExpr(vars, reg, constant) = reg(e.getValue(vars, reg, constant));

getValue@_AndExpr(vars, reg, constant) =
  e1.getValue(vars, reg, constant) & e2.getValue(vars, reg, constant);

getValue@_OrExpr(vars, reg, constant) =
  e1.getValue(vars, reg, constant) | e2.getValue(vars, reg, constant);

getValue@_XorExpr(vars, reg, constant) =
  e1.getValue(vars, reg, constant) ^ e2.getValue(vars, reg, constant);

getValue@_MuxExpr(vars, reg, constant) = cond(e0.getValue(vars, reg, constant),
                                         e1.getValue(vars, reg, constant),
                                         e2.getValue(vars, reg, constant));