Merge pull request #10 from mikhailmints/mixed_match

Implement mixed/irreversible match as a primitive
mikhailmints · Sep 13, 2024 · 8594bdb · 8594bdb
2 parents 89e4f4a + 5d525d0
commit 8594bdb
Show file tree

Hide file tree

Showing 31 changed files with 846 additions and 321 deletions.
diff --git a/bin/driver_util.ml b/bin/driver_util.ml
@@ -6,7 +6,7 @@ open Typechecking
 open Semantics
 
 let execute_expr (e : expr) : unit =
-  match mixed_type_check StringMap.empty e with
+  match mixed_type_check StringMap.empty StringMap.empty e with
   | NoneE err -> Printf.printf "Typechecking error: %s\n\n" err
   | SomeE tp -> begin
       Printf.printf "Expression type: %s\n%!"

diff --git a/bin/qunity_compile_qasm.ml b/bin/qunity_compile_qasm.ml
@@ -125,7 +125,7 @@ let compile_file (prog_filename : string) (out_filename : string) : unit =
         Printf.printf "%s\n" err;
         exit 1
     | SomeE e -> begin
-        match mixed_type_check StringMap.empty e with
+        match mixed_type_check StringMap.empty StringMap.empty e with
         | NoneE err ->
             Printf.printf "Typechecking error: %s\n" err;
             exit 1

diff --git a/diagrams/circuits/bogosort.png b/diagrams/circuits/bogosort.png
diff --git a/diagrams/circuits/ctrl_nested1.png b/diagrams/circuits/ctrl_nested1.png
diff --git a/diagrams/circuits/ctrl_on_match.png b/diagrams/circuits/ctrl_on_match.png
diff --git a/diagrams/circuits/mixed_match.png b/diagrams/circuits/mixed_match.png
diff --git a/diagrams/circuits/share_discard_many.png b/diagrams/circuits/share_discard_many.png
diff --git a/diagrams/circuits/walk_1d.png b/diagrams/circuits/walk_1d.png
diff --git a/diagrams/circuits/walk_1d_alt.png b/diagrams/circuits/walk_1d_alt.png
diff --git a/diagrams/circuits/walk_1d_alt1.png b/diagrams/circuits/walk_1d_alt1.png
diff --git a/diagrams/sim_results/bogosort_sim_results.png b/diagrams/sim_results/bogosort_sim_results.png
diff --git a/diagrams/sim_results/ctrl_nested1_sim_results.png b/diagrams/sim_results/ctrl_nested1_sim_results.png
diff --git a/diagrams/sim_results/ctrl_on_match_sim_results.png b/diagrams/sim_results/ctrl_on_match_sim_results.png
diff --git a/diagrams/sim_results/mixed_match_sim_results.png b/diagrams/sim_results/mixed_match_sim_results.png
diff --git a/diagrams/sim_results/walk_1d_alt1_sim_results.png b/diagrams/sim_results/walk_1d_alt1_sim_results.png
diff --git a/diagrams/sim_results/walk_1d_alt_sim_results.png b/diagrams/sim_results/walk_1d_alt_sim_results.png
diff --git a/diagrams/sim_results/walk_1d_sim_results.png b/diagrams/sim_results/walk_1d_sim_results.png
diff --git a/examples/bogosort.qunity b/examples/bogosort.qunity
@@ -0,0 +1,89 @@
+def Split <N, T, I> :=
+    if I = [0] then
+        lambda x {NTensorT <N, T>} -> ((), x)
+    else
+        lambda (x, x') {NTensorT <N, T>} ->
+            let (x, (x0, x1)) {T * (NTensorT <[I - 1], T> * NTensorT <[N - I], T>)} =
+                (x, Split <[N - 1], T, [I - 1]> of x') in
+            ((x, x0), x1)
+    endif
+end
+
+def Swap <N, T, I> :=
+    if I = [0] then
+        Qid <NTensorT <N, T>>
+    else
+        lambda (x, x') {NTensorT <N, T>} ->
+            let (x, (x0, (xi, x1))) {T * (NTensorT <[I - 1], T> * NTensorT <[N - I], T>)} =
+                (x, Split <[N - 1], T, [I - 1]> of x') in
+            (xi, Concat <[I - 1], [N - I], T> of (x0, (x, x1)))
+    endif
+end
+
+def RandomizePassIter <N, T, I> :=
+    if I = N then
+        Qid <NTensorT <N, T>>
+    else
+        lambda x {NTensorT <N, T>} ->
+            match {Bit, NTensorT <N, T>} BitPlus [
+                Bit0 -> x |> Swap <N, T, I>;
+                Bit1 -> x
+            ] |> RandomizePassIter <N, T, [I + 1]>
+    endif
+end
+
+def RandomizePass <N, T> :=
+    if N = [0] then
+        Qid <qunit>
+    else
+        lambda (x, x') {NTensorT <N, T>} ->
+            let (x, x') {NTensorT <N, T>} = RandomizePassIter <N, T, [1]> of (x, x') in
+            (x, RandomizePass <[N - 1], T> of x')
+    endif
+end
+
+def RandomizeIter <N, T, Niter> :=
+    if Niter = [0] then
+        Qid <NTensorT <N, T>>
+    else
+        lambda x {NTensorT <N, T>} ->
+            x |> RandomizePass <N, T> |> RandomizeIter <N, T, [Niter - 1]>
+    endif
+end
+
+def Randomize <N, T> :=
+    RandomizeIter <N, T, N>
+end
+
+def IsSorted <N, T, Compare> :=
+    if N = [0] then
+        lambda () {qunit} -> Bit1
+    else
+        if N = [1] then
+            lambda (x, ()) {T * qunit} -> Bit1
+        else
+            lambda (x0, (x1, x')) {NTensorT <N, T>} ->
+                match {Bit, Bit} (Compare of (x0, x1)) [
+                    Bit0 -> Bit0;
+                    Bit1 -> IsSorted <[N - 1], T, Compare> of (x1, x')
+                ]
+        endif
+    endif
+end
+
+def BitCompare :=
+    lambda (a, b) {Bit * Bit} -> match {Bit * Bit, Bit} (a, b) [
+        (Bit1, Bit0) -> Bit0;
+        else -> Bit1
+    ]
+end
+
+def Bogosort <N, T, Compare> :=
+    lambda x {NTensorT <N, T>} ->
+        let x' {NTensorT <N, T>} = Randomize <N, T> of x in
+        match {Bit, NTensorT <N, T>} (IsSorted <N, T, Compare> of x') [
+            Bit1 -> x'
+        ]
+end
+
+Bogosort <[4], Bit, BitCompare> of (Bit0, (Bit1, (Bit0, (Bit1, ()))))
diff --git a/examples/ctrl_nested1.qunity b/examples/ctrl_nested1.qunity
@@ -0,0 +1,3 @@
+(BitPlus, BitPlus) |> lambda (a, b) {Bit * Bit} -> ctrl {Bit * Bit, Bit * Bit} (a, b) [
+    (Bit0, x) -> (a, ctrl {Bit, Bit} x [Bit0 -> b])
+]
diff --git a/examples/ctrl_on_match.qunity b/examples/ctrl_on_match.qunity
@@ -0,0 +1,5 @@
+(BitPlus, BitPlus) |> lambda (
+ctrl {Bit, Bit * Bit} (match {Bit, Bit} x [Bit0 -> BitPlus; Bit1 -> BitMinus]) [
+    Bit0 -> (x, Bit1);
+    Bit1 -> (x, Bit0);
+]) {Bit * Bit} -> x
diff --git a/examples/mixed_match.qunity b/examples/mixed_match.qunity
@@ -0,0 +1,5 @@
+BitPlus |> lambda x {Bit} -> (x, x)
+|> lambda (x, y) {Bit * Bit} -> match {Bit, Bit} x [
+    Bit0 -> y;
+    Bit1 -> try y |> lambda BitPlus {Bit} -> BitPlus catch Bit1 
+]
diff --git a/examples/walk_1d.qunity b/examples/walk_1d.qunity
@@ -1,9 +1,9 @@
 def Step <N> :=
     lambda (x, velocity) {NTensorT <N, Bit> * Bit} ->
     match {NTensorT <N, Bit> * Bit, NTensorT <N, Bit> * Bit} (x, velocity) [
-        (NTensorE <N, Bit0>, Bit0) -> (IncrementLE <N> of NTensorE <N, Bit0>, Bit1);
-        (NTensorE <N, Bit1>, Bit1) -> (DecrementLE <N> of NTensorE <N, Bit1>, Bit0);
-        else -> ctrl {Bit, NTensorT <N, Bit> * Bit} velocity [
+        (NTensorE <N, Bit0>, Bit0) -> (IncrementLE <N> of x, Qnot of velocity);
+        (NTensorE <N, Bit1>, Bit1) -> (DecrementLE <N> of x, Qnot of velocity);
+        else -> match {Bit, NTensorT <N, Bit> * Bit} velocity [
             Bit0 -> (DecrementLE <N> of x, velocity);
             Bit1 -> (IncrementLE <N> of x, velocity)
         ]