Preserve original parameter names in residual code

Closes #28.

CHANGELOG.md

@@ -6,14 +6,20 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## unreleased
 
+### Added
+
+ - The `Symbol.freshen` function that generates a fresh symbol according to a given predicate.
+
 ### Changed
 
  - Do not share syntactically equal arguments during postprocessing.
+ - Preserve original parameter names in residual code.
 
 ### Fixed
 
  - Do not simplify _/(x, 0)_ and _%(x, 0)_ to avoid incorrect panic messages (issue https://github.com/mazeppa-dev/mazeppa/issues/25).
  - Hide empty reduction paths in CLI error messages (issue https://github.com/mazeppa-dev/mazeppa/issues/27).
+ - Do not overshadow user-specified symbols during residualization (issue https://github.com/mazeppa-dev/mazeppa/issues/28).
 
 ## 0.4.3 - 2024-11-11
 

README.md

@@ -126,8 +126,8 @@ target
 ```
 main(xs) := f0(xs);
 
-f0(x0) := match x0 {
-    Cons(x1, x2) -> +(*(x1, x1), f0(x2)),
+f0(xs) := match xs {
+    Cons(x0, x1) -> +(*(x0, x0), f0(x1)),
     Nil() -> 0i32
 };
 ```
@@ -251,10 +251,10 @@ By running Mazeppa on the above sample, we can obtain an efficient string matchi
 ```
 main(s) := f0(s);
 
-f0(x0) := match x0 {
-    Cons(x1, x2) -> match =(97u8, x1) {
-        F() -> f1(x2),
-        T() -> f2(x2)
+f0(s) := match s {
+    Cons(x0, x1) -> match =(97u8, x0) {
+        F() -> f1(x1),
+        T() -> f2(x1)
     },
     Nil() -> F()
 };
@@ -562,12 +562,12 @@ Run `dune exec my_compiler` to see the desired residual program:
 
 ```
 [([], "main", ["xs"], (Raw_term.Call ("f0", [(Raw_term.Var "xs")])));
-  ([], "f0", ["x0"],
-   (Raw_term.Match ((Raw_term.Var "x0"),
-      [(("Cons", ["x1"; "x2"]),
+  ([], "f0", ["xs"],
+   (Raw_term.Match ((Raw_term.Var "xs"),
+      [(("Cons", ["x0"; "x1"]),
         (Raw_term.Call ("+",
-           [(Raw_term.Call ("*", [(Raw_term.Var "x1"); (Raw_term.Var "x1")]));
-             (Raw_term.Call ("f0", [(Raw_term.Var "x2")]))]
+           [(Raw_term.Call ("*", [(Raw_term.Var "x0"); (Raw_term.Var "x0")]));
+             (Raw_term.Call ("f0", [(Raw_term.Var "x1")]))]
            )));
         (("Nil", []), (Raw_term.Const (Const.Int (Checked_oint.I32 0))))]
       )))

bin/main.ml

@@ -109,7 +109,7 @@ let supercompile ~(channels : channels) (input : Raw_program.t) : unit =
     (match channels.nodes_oc with
      | Some oc -> Nodes.output ~oc ()
      | None -> ());
-    let t_res, program_res = Residualizer.run graph in
+    let t_res, program_res = Residualizer.run ~unknowns:main_params graph in
     let residue = ([], main_symbol, main_params, t_res) :: program_res in
     Pretty.print_program ~oc:channels.output_oc residue
 ;;

examples/ackermann/target/output.mz

@@ -1,9 +1,9 @@
 main(m, n) := Combine(1u32, 3u32, 7u32, 13u32, f0(m, n));
 
-f0(x0, x1) := match =(x0, 0u32) {
-    F() -> match =(x1, 0u32) {
-        F() -> f0(-(x0, 1u32), f0(x0, -(x1, 1u32))),
-        T() -> f0(-(x0, 1u32), 1u32)
+f0(m, n) := match =(m, 0u32) {
+    F() -> match =(n, 0u32) {
+        F() -> f0(-(m, 1u32), f0(m, -(n, 1u32))),
+        T() -> f0(-(m, 1u32), 1u32)
     },
-    T() -> +(x1, 1u32)
+    T() -> +(n, 1u32)
 };

examples/call-by-value/target/output.mz

@@ -1,3 +1,3 @@
 main(x) := Combine(f0(x), Panic("666"));
 
-f0(x0) := f0(x0);
+f0(x) := f0(x);

examples/church-binary-trees/target/output.mz

@@ -1,13 +1,13 @@
 main(t) := f0(t);
 
-f0(x0) := match x0 {
-    Leaf(x1) -> 0u64,
-    Node(x1, x2) ->
+f0(t) := match t {
+    Leaf(x0) -> 0u64,
+    Node(x0, x1) ->
+    let x2 := f1(x0);
     let x3 := f1(x1);
-    let x4 := f1(x2);
-    +(match >(x3, x4) {
-        F() -> x4,
-        T() -> x3
+    +(match >(x2, x3) {
+        F() -> x3,
+        T() -> x2
     }, 1u64)
 };
 

examples/defunctionalization/target/output.mz

@@ -1,12 +1,12 @@
 main(xs, op1, op2) := f1(op1, op2, xs);
 
-f0(x0, x1) := match x1 {
+f0(x0, op1) := match op1 {
     F() -> +(x0, 5i32),
     G() -> /(x0, 10i32),
     H() -> *(x0, x0)
 };
 
-f1(x0, x1, x2) := match x2 {
-    Cons(x3, x4) -> Cons(f0(f0(x3, x0), x1), f1(x0, x1, x4)),
+f1(op1, op2, xs) := match xs {
+    Cons(x0, x1) -> Cons(f0(f0(x0, op1), op2), f1(op1, op2, x1)),
     Nil() -> Nil()
 };

examples/double-append/target/output.mz

@@ -1,11 +1,11 @@
 main(xs, ys, zs) := f0(xs, ys, zs);
 
-f0(x0, x1, x2) := match x0 {
-    Cons(x3, x4) -> Cons(x3, f0(x4, x1, x2)),
-    Nil() -> f1(x1, x2)
+f0(xs, ys, zs) := match xs {
+    Cons(x0, x1) -> Cons(x0, f0(x1, ys, zs)),
+    Nil() -> f1(ys, zs)
 };
 
-f1(x0, x1) := match x0 {
-    Cons(x2, x3) -> Cons(x2, f1(x3, x1)),
-    Nil() -> x1
+f1(ys, zs) := match ys {
+    Cons(x0, x1) -> Cons(x0, f1(x1, zs)),
+    Nil() -> zs
 };

examples/double-squares/target/output.mz

@@ -1,6 +1,6 @@
 main(xs) := f0(xs);
 
-f0(x0) := match x0 {
-    Cons(x1, x2) -> Cons(*(*(x1, x1), *(x1, x1)), f0(x2)),
+f0(xs) := match xs {
+    Cons(x0, x1) -> Cons(*(*(x0, x0), *(x0, x0)), f0(x1)),
     Nil() -> Nil()
 };

examples/factorial/target/output.mz

@@ -1,6 +1,6 @@
 main(n) := Combine(1u32, 1u32, 2u32, 6u32, 24u32, 120u32, f0(n));
 
-f0(x0) := match =(x0, 0u32) {
-    F() -> *(x0, f0(-(x0, 1u32))),
+f0(n) := match =(n, 0u32) {
+    F() -> *(n, f0(-(n, 1u32))),
     T() -> 1u32
 };

examples/fibonacci/target/output.mz

@@ -1,9 +1,9 @@
 main(n) := Combine(0u32, 1u32, 1u32, 2u32, 3u32, 5u32, 8u32, 13u32, 21u32, 34u32
     , f0(n));
 
-f0(x0) := match =(x0, 0u32) {
-    F() -> match =(x0, 1u32) {
-        F() -> +(f0(-(x0, 1u32)), f0(-(x0, 2u32))),
+f0(n) := match =(n, 0u32) {
+    F() -> match =(n, 1u32) {
+        F() -> +(f0(-(n, 1u32)), f0(-(n, 2u32))),
         T() -> 1u32
     },
     T() -> 0u32

examples/flip-tree/target/output.mz

@@ -1,8 +1,8 @@
 main(xs) := f0(xs);
 
-f0(x0) := match x0 {
-    Branch(x1, x2) -> +(f1(x1), f1(x2)),
-    Leaf(x1) -> x1
+f0(xs) := match xs {
+    Branch(x0, x1) -> +(f1(x0), f1(x1)),
+    Leaf(x0) -> x0
 };
 
 f1(x0) := f0(x0);

examples/kmp-test/target/output.mz

@@ -1,9 +1,9 @@
 main(s) := f0(s);
 
-f0(x0) := match x0 {
-    Cons(x1, x2) -> match =(97u8, x1) {
-        F() -> f1(x2),
-        T() -> f2(x2)
+f0(s) := match s {
+    Cons(x0, x1) -> match =(97u8, x0) {
+        F() -> f1(x1),
+        T() -> f2(x1)
     },
     Nil() -> F()
 };

examples/mc91/target/output.mz

@@ -1,6 +1,6 @@
 main(n) := Combine(91i32, 91i32, 91i32, 91i32, 92i32, 93i32, f0(n));
 
-f0(x0) := match >(x0, 100i32) {
-    F() -> f0(f0(+(x0, 11i32))),
-    T() -> -(x0, 10i32)
+f0(n) := match >(n, 100i32) {
+    F() -> f0(f0(+(n, 11i32))),
+    T() -> -(n, 10i32)
 };

examples/mutual-recursion/target/output.mz

@@ -1,9 +1,9 @@
 main(xs) := f0(xs);
 
-f0(x0) := match x0 {
-    Cons(x1, x2) -> match x2 {
-        Cons(x3, x4) -> +(*(2i32, x1), +(*(3i32, x3), f0(x4))),
-        Nil() -> +(*(2i32, x1), 0i32)
+f0(xs) := match xs {
+    Cons(x0, x1) -> match x1 {
+        Cons(x2, x3) -> +(*(2i32, x0), +(*(3i32, x2), f0(x3))),
+        Nil() -> +(*(2i32, x0), 0i32)
     },
     Nil() -> 0i32
 };

examples/productivity-analysis/target/output.mz

@@ -1,20 +1,20 @@
 main(stmt) := f0(stmt);
 
-f0(x0) := match x0 {
-    If1(x1, x2, x3) -> match x1 {
-        F() -> f1(x3),
-        T() -> f1(x2),
-        Var(x4, x5) -> match f2(x4, x5) {
-            F() -> f1(x3),
-            T() -> f1(x2)
+f0(stmt) := match stmt {
+    If1(x0, x1, x2) -> match x0 {
+        F() -> f1(x2),
+        T() -> f1(x1),
+        Var(x3, x4) -> match f2(x3, x4) {
+            F() -> f1(x2),
+            T() -> f1(x1)
         }
     },
-    If2(x1, x2, x3) -> match x1 {
-        F() -> f1(x3),
-        T() -> f1(x2),
-        Var(x4, x5) -> match f2(x4, x5) {
-            F() -> f1(x3),
-            T() -> f1(x2)
+    If2(x0, x1, x2) -> match x0 {
+        F() -> f1(x2),
+        T() -> f1(x1),
+        Var(x3, x4) -> match f2(x3, x4) {
+            F() -> f1(x2),
+            T() -> f1(x1)
         }
     }
 };

examples/raytracer-loop/target/output.mz

@@ -1,8 +1,8 @@
 main(xs, ys) := f0(xs, ys);
 
-f0(x0, x1) := match x0 {
-    Cons(x2, x3) -> match x1 {
-        Cons(x4, x5) -> +(*(x2, x4), f0(x3, x5)),
+f0(xs, ys) := match xs {
+    Cons(x0, x1) -> match ys {
+        Cons(x2, x3) -> +(*(x0, x2), f0(x1, x3)),
         Nil() -> 0i32
     },
     Nil() -> 0i32

examples/sat-solver/target/output.mz

@@ -10,17 +10,17 @@ f0() := T();
 
 f1(x0) := x0;
 
-f2(x0, x1) := If(x1, f1(x0), f3(x0));
+f2(x0, c) := If(c, f1(x0), f3(x0));
 
 f3(x0) := F();
 
-f4(x0, x1, x2) := If(x1, f1(x0), f2(x0, x2));
+f4(x0, a, c) := If(a, f1(x0), f2(x0, c));
 
-f5(x0, x1, x2) := If(x1, f2(x0, x2), f1(x0));
+f5(x0, e, g) := If(e, f2(x0, g), f1(x0));
 
-f6(x0, x1) := If(x1, f3(x0), f1(x0));
+f6(x0, c) := If(c, f3(x0), f1(x0));
 
-f7(x0, x1, x2, x3) := If(x1, f1(x0), If(x2, f6(x0, x3), f1(x0)));
+f7(x0, a, b, c) := If(a, f1(x0), If(b, f6(x0, c), f1(x0)));
 
 f8(x0) := match x0 {
     F() -> F(),

examples/share-globals/target/output.mz

@@ -1,6 +1,6 @@
 main(x, y) := Pair(f0(x), f0(y));
 
-f0(x0) := match x0 {
-    A(x1) -> B(x1),
-    C(x1) -> D(x1)
+f0(x) := match x {
+    A(x0) -> B(x0),
+    C(x0) -> D(x0)
 };

examples/sum-squares-tree/target/output.mz

@@ -1,8 +1,8 @@
 main(xs) := f0(xs);
 
-f0(x0) := match x0 {
-    Branch(x1, x2) -> +(f1(x1), f1(x2)),
-    Leaf(x1) -> *(x1, x1)
+f0(xs) := match xs {
+    Branch(x0, x1) -> +(f1(x0), f1(x1)),
+    Leaf(x0) -> *(x0, x0)
 };
 
 f1(x0) := f0(x0);

examples/sum-squares/target/output.mz

@@ -1,6 +1,6 @@
 main(xs) := f0(xs);
 
-f0(x0) := match x0 {
-    Cons(x1, x2) -> +(*(x1, x1), f0(x2)),
+f0(xs) := match xs {
+    Cons(x0, x1) -> +(*(x0, x0), f0(x1)),
     Nil() -> 0i32
 };

examples/useless-params/target/output.mz

@@ -1,3 +1,3 @@
 main(x, _y, _z) := f0(_y, _z, x);
 
-f0(x0, x1, x2) := f0(x2, x2, x2);
+f0(_y, _z, x) := f0(x, x, x);

examples/zip-map-tree/target/output.mz

@@ -3,21 +3,21 @@ main(xs, ys) := match xs {
     Node(x0, x1, x2) -> f1(x0, x1, x2, ys)
 };
 
-f0(x0) := Empty();
+f0(ys) := Empty();
 
-f1(x0, x1, x2, x3) := match x3 {
+f1(x0, x1, x2, ys) := match ys {
     Empty() -> Empty(),
-    Node(x4, x5, x6) -> match x0 {
+    Node(x3, x4, x5) -> match x0 {
         Empty() -> match x2 {
-            Empty() -> Node(f0(x4), Pair(Blah(x1), Blah(x5)), f0(x6)),
-            Node(x7, x8, x9) -> Node(f0(x4), Pair(Blah(x1), Blah(x5)), f2(x7, x8
-            , x9, x6))
+            Empty() -> Node(f0(x3), Pair(Blah(x1), Blah(x4)), f0(x5)),
+            Node(x6, x7, x8) -> Node(f0(x3), Pair(Blah(x1), Blah(x4)), f2(x6, x7
+            , x8, x5))
         },
-        Node(x7, x8, x9) -> match x2 {
-            Empty() -> Node(f2(x7, x8, x9, x4), Pair(Blah(x1), Blah(x5)), f0(x6)
+        Node(x6, x7, x8) -> match x2 {
+            Empty() -> Node(f2(x6, x7, x8, x3), Pair(Blah(x1), Blah(x4)), f0(x5)
             ),
-            Node(x10, x11, x12) -> Node(f2(x7, x8, x9, x4), Pair(Blah(x1), Blah(
-            x5)), f2(x10, x11, x12, x6))
+            Node(x9, x10, x11) -> Node(f2(x6, x7, x8, x3), Pair(Blah(x1), Blah(
+            x4)), f2(x9, x10, x11, x5))
         }
     }
 };

examples/zip-map/target/output.mz

@@ -3,10 +3,10 @@ main(xs, ys) := match xs {
     Nil() -> f1(ys)
 };
 
-f0(x0, x1, x2) := match x2 {
-    Cons(x3, x4) -> match x1 {
-        Cons(x5, x6) -> Cons(Pair(Blah(x0), Blah(x3)), f0(x5, x6, x4)),
-        Nil() -> Cons(Pair(Blah(x0), Blah(x3)), f1(x4))
+f0(x0, x1, ys) := match ys {
+    Cons(x2, x3) -> match x1 {
+        Cons(x4, x5) -> Cons(Pair(Blah(x0), Blah(x2)), f0(x4, x5, x3)),
+        Nil() -> Cons(Pair(Blah(x0), Blah(x2)), f1(x3))
     },
     Nil() -> Nil()
 };