(* ============================================
               Boolean circuits
   ============================================ *)

(* _________ Types _________ *)

type var = string
type id = int 

type op =
  | CIn of int | COut | CShare
  | CAnd | COr | CNeg

type input = id
type output = id
type gate = input list * op * output list
type circuit = gate list

(* _________ Getters _________ *)

let get_node_info circ target =
  let (ins, op, outs) =
    List.hd (List.filter (fun (_, _, outs) -> List.mem target outs) circ)
  in (ins, op, outs)

let get_inputs circ node =
  let (ins, _, _) = get_node_info circ node in ins
  
let get_outputs circ node =
  let (_, _, outs) = get_node_info circ node in outs

let get_op circ node =
  let (_, op, _) = get_node_info circ node in op

(* extracts the two first inputs in a list of inputs *)
let twinhd = function
  | [] -> failwith "Error extract_bin_ins: no input."
  | h1::h2::t -> (h1, h2)
  | _ -> failwith "Error extract_bin_ins: inputs do not match." 

(* _________ Evaluation _________ *)

(* provides the boolean value of the node 'concl' in a circuit 'circ' *)
let rec value circ concl =
  match get_op circ concl with
  | CIn i -> i
  | CShare | COut ->
      let x = List.hd (get_inputs circ concl) in
      value circ x
  | CAnd ->
      let (x, y) = twinhd (get_inputs circ concl) in
      let vx = value circ x in
      let vy = value circ y in
      min vx vy
  | COr ->
      let (x, y) = twinhd (get_inputs circ concl) in
      let vx = value circ x in
      let vy = value circ y in
      max vx vy
  | CNeg ->
      let x = List.hd (get_inputs circ concl) in
      let vx = value circ x in
      1 - vx

let rec eval (circ : circuit) : int =
  let (_, _, concl) =
    List.hd (List.filter (fun (_, o, _) -> o = COut) circ)
  in value circ (List.hd concl)

(* _________ Examples _________ *)

let make_gate ins op outs : gate = (ins, op, outs)
let make_input value outs : gate = ([], CIn value, outs)

let make_and_circ x y : circuit = [
  make_input x [0];
  make_input y [1];
  make_gate [0;1] CAnd [2];
  make_gate [2] COut [3]
]

let make_or_circ x y : circuit = [
  make_input x [0];
  make_input y [1];
  make_gate [0;1] COr [2];
  make_gate [2] COut [3]
]

let make_neg_circ x : circuit = [
  make_input x [0];
  make_gate [0] CNeg [1];
  make_gate [1] COut [2]
]

(* corresponds to the excluded middle x v ~x *)
let make_em_circ x : circuit = [
  make_input x [0];
  make_gate [0] CShare [1;2];
  make_gate [1] CNeg [3];
  make_gate [3;2] COr [4];
  make_gate [4] COut [5]
]

let c1 = List.map eval [make_and_circ 0 0; make_and_circ 0 1; make_and_circ 1 0; make_and_circ 1 1]
let c2 = List.map eval [make_or_circ 0 0; make_or_circ 0 1; make_or_circ 1 0; make_or_circ 1 1]
let c3 = List.map eval [make_neg_circ 0; make_neg_circ 1]
let c4 = List.map eval [make_em_circ 0; make_em_circ 1]