Fix polarities in StellarCircuits

ocaml/Circuits.ml

@@ -12,24 +12,28 @@ type op =
   | CAnd | COr | CNeg
 
 type input = id
-type gate = input list * op * id
+type output = id
+type gate = input list * op * output list
 type circuit = gate list
 
 (* _________ Getters _________ *)
 
-let get_node_info circ node =
-    let (ins, op, i) =
-      List.hd (List.filter (fun (_, _, i) -> i = node) circ)
-  in (ins, op)
+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 (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
+  let (_, op, _) = get_node_info circ node in op
 
 (* extracts the two first inputs in a list of inputs *)
-let extract_bin_ins = function
+let twinhd = function
   | [] -> failwith "Error extract_bin_ins: no input."
   | h1::h2::t -> (h1, h2)
   | _ -> failwith "Error extract_bin_ins: inputs do not match." 
@@ -44,12 +48,12 @@ let rec value circ concl =
       let x = List.hd (get_inputs circ concl) in
       value circ x
   | CAnd ->
-    let (x, y) = extract_bin_ins (get_inputs circ concl) in
+      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) = extract_bin_ins (get_inputs circ concl) in
+      let (x, y) = twinhd (get_inputs circ concl) in
       let vx = value circ x in
       let vy = value circ y in
       max vx vy
@@ -61,38 +65,43 @@ let rec value circ concl =
 let rec eval (circ : circuit) : int =
   let (_, _, concl) =
     List.hd (List.filter (fun (_, o, _) -> o = COut) circ)
-  in value circ concl
+  in value circ (List.hd concl)
 
 (* _________ Examples _________ *)
 
-let make_gate ins op id : gate = (ins, op, id)
-let make_input value id : gate = ([], CIn value, id)
+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
+  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
+  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
+  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;
-  make_gate [1] CNeg 2;
-  make_gate [1;2] COr 3;
-  make_gate [3] COut 4
+  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]

ocaml/Resolution.ml

@@ -107,17 +107,20 @@ let print_dgraph dg =
   in print_string (aux dg);;
 
 (* _________ Examples _________ *)
+let make_const_pol pol c = Func (c, pol, [])
+let make_const c = make_const_pol Npol c
+
 let y = Var("y")
 let x = Var("x")
 let z = Var("z")
 let r = Var("r")
-let zero = Func("0", Npol, [])
+let zero = make_const "0"
 let s x = Func("s", Npol, [x])
 let add p x y z = Func("add", p, [x;y;z])
 
 (* Convert int to term *)
 let rec enat i = 
-  if i = 0 then Func("0", Npol, []) else s (enat (i-1))
+  if i = 0 then zero else s (enat (i-1))
 
 (* makes the constellation corresponding to an addition *)
 let make_const_add n m = 

ocaml/StellarCircuits.ml

@@ -0,0 +1,56 @@
+open Circuits
+open Resolution
+
+(* ============================================
+               Stellar Circuits
+   ============================================ *)
+
+let port pol i v = Func ("c"^(string_of_int i), pol, v)
+let inport i x = port Neg i [Var x]
+let outport i x = port Pos i [Var x]
+
+let call_cneg pol arg res = Func ("neg", pol, [arg; res])
+let call_cand pol arg1 arg2 res = Func ("and", pol, [arg1; arg2; res])
+let call_cor pol arg1 arg2 res = Func ("or", pol, [arg1; arg2; res])
+
+let star_of_gate circ (ins, op, outs) =
+  match op with
+  | CIn i -> [port Pos (List.hd outs) [make_const (string_of_int i)]]
+  | COut -> [inport (List.hd ins) "r"; Var "r"]
+  | CShare -> 
+      let (o1, o2) = twinhd outs in
+      [inport (List.hd ins) "x"; outport o1 "x"; outport o2 "x"] 
+  | CNeg -> [
+      inport (List.hd ins) "x";
+      call_cneg Neg (Var "x") (Var "r");
+      outport (List.hd outs) "r" 
+    ]
+  | CAnd ->
+      let (i1, i2) = twinhd ins in [
+        inport i1 "x";
+        inport i2 "y";
+        call_cand Neg (Var "x") (Var "y") (Var "r");
+        outport (List.hd outs) "r" 
+      ]
+  | COr ->
+      let (i1, i2) = twinhd ins in [
+        inport i1 "x";
+        inport i2 "y";
+        call_cor Neg (Var "x") (Var "y") (Var "r");
+        outport (List.hd outs) "r" 
+      ]
+
+let const_of_circuit (circ : circuit) = List.map (star_of_gate circ) circ
+
+let prop_logic : constellation = [
+  [call_cneg Pos (make_const "0") (make_const "1")];
+  [call_cneg Pos (make_const "1") (make_const "0")];
+  [call_cand Pos (make_const "0") (make_const "0") (make_const "0")];
+  [call_cand Pos (make_const "0") (make_const "1") (make_const "0")];
+  [call_cand Pos (make_const "1") (make_const "0") (make_const "0")];
+  [call_cand Pos (make_const "1") (make_const "1") (make_const "1")];
+  [call_cor Pos (make_const "0") (make_const "0") (make_const "0")];
+  [call_cor Pos (make_const "0") (make_const "1") (make_const "1")];
+  [call_cor Pos (make_const "1") (make_const "0") (make_const "1")];
+  [call_cor Pos (make_const "1") (make_const "1") (make_const "1")]
+]

ocaml/StellarFSA.ml

@@ -0,0 +1,15 @@
+open Resolution
+open FSA
+
+(* ============================================
+              Stellar Automata
+   ============================================ *)
+
+let dot x y = Func ("·", Npol, [x; y])
+
+let const_of_word (w : char list) =
+  let rec aux = function
+    | [] -> Func ("", Npol, [])
+    | c::w ->
+        dot (Func (String.make 1 c, Npol, [])) (aux w)
+  in [Func ("i", Pos, [aux w])]