feat(naive_rewriter): also rewrite expressions inside lettings

Allow rewriting of expressions inside lettings. The rewriter, on each pass, checks for possible applicable rules in the lettings then the model. The semantics of rewriting sub-expressions inside lettings and the model are the same as before. Rewriting `letting A be EXPENSIVE` (where EXPENSIVE is a complex expression which needs many rule applications to refine) before we substitute it should reduce the number of rule applications needed.
conjure-cp · Jan 31, 2025 · f5af399 · f5af399
1 parent 742d745
commit f5af399
Show file tree

Hide file tree

Showing 5 changed files with 397 additions and 282 deletions.
diff --git a/..._oxide/tests/integration/basic/lettings/03-value-expr/input-expected-rule-trace-human.txt b/..._oxide/tests/integration/basic/lettings/03-value-expr/input-expected-rule-trace-human.txt
@@ -10,38 +10,38 @@ such that
 
 --
 
-(b < 3), 
-   ~~> lt_to_leq ([("Minion", 8400)]) 
-(b <= Sum([3, -1])) 
+Not(Not(Not(A))), 
+   ~~> remove_double_negation ([("Base", 8400)]) 
+Not(A) 
 
 --
 
-Sum([3, -1]), 
-   ~~> apply_eval_constant ([("Constant", 9001)]) 
-2 
+A, 
+   ~~> substitute_value_lettings ([("Base", 5000)]) 
+false 
 
 --
 
-NotA, 
-   ~~> substitute_value_lettings ([("Base", 5000)]) 
-Not(Not(Not(A))) 
+Not(false), 
+   ~~> apply_eval_constant ([("Constant", 9001)]) 
+true 
 
 --
 
-Not(Not(Not(A))), 
-   ~~> remove_double_negation ([("Base", 8400)]) 
-Not(A) 
+(b < 3), 
+   ~~> lt_to_leq ([("Minion", 8400)]) 
+(b <= Sum([3, -1])) 
 
 --
 
-A, 
-   ~~> substitute_value_lettings ([("Base", 5000)]) 
-false 
+Sum([3, -1]), 
+   ~~> apply_eval_constant ([("Constant", 9001)]) 
+2 
 
 --
 
-Not(false), 
-   ~~> apply_eval_constant ([("Constant", 9001)]) 
+NotA, 
+   ~~> substitute_value_lettings ([("Base", 5000)]) 
 true 
 
 --
@@ -61,7 +61,7 @@ Ineq(b, 2, 0)
 Final model:
 
 letting A be false
-letting NotA be Not(Not(Not(A)))
+letting NotA be true
 find b: int(1..20)
 
 such that

diff --git a/conjure_oxide/tests/integration/basic/lettings/03-value-expr/input-expected-rule-trace.json b/conjure_oxide/tests/integration/basic/lettings/03-value-expr/input-expected-rule-trace.json
@@ -1,4 +1,149 @@
 [
+  {
+    "initial_expression": {
+      "Not": [
+        {
+          "Not": [
+            {
+              "Not": [
+                {
+                  "Atomic": [
+                    {
+                      "Reference": {
+                        "UserName": "A"
+                      }
+                    },
+                    {
+                      "clean": false,
+                      "etype": null
+                    }
+                  ]
+                },
+                {
+                  "clean": false,
+                  "etype": null
+                }
+              ]
+            },
+            {
+              "clean": false,
+              "etype": null
+            }
+          ]
+        },
+        {
+          "clean": false,
+          "etype": null
+        }
+      ]
+    },
+    "rule_name": "remove_double_negation",
+    "rule_set": [
+      [
+        "Base",
+        8400
+      ]
+    ],
+    "transformed _expression": {
+      "Not": [
+        {
+          "Atomic": [
+            {
+              "Reference": {
+                "UserName": "A"
+              }
+            },
+            {
+              "clean": false,
+              "etype": null
+            }
+          ]
+        },
+        {
+          "clean": false,
+          "etype": null
+        }
+      ]
+    }
+  },
+  {
+    "initial_expression": {
+      "Atomic": [
+        {
+          "Reference": {
+            "UserName": "A"
+          }
+        },
+        {
+          "clean": false,
+          "etype": null
+        }
+      ]
+    },
+    "rule_name": "substitute_value_lettings",
+    "rule_set": [
+      [
+        "Base",
+        5000
+      ]
+    ],
+    "transformed _expression": {
+      "Atomic": [
+        {
+          "Literal": {
+            "Bool": false
+          }
+        },
+        {
+          "clean": false,
+          "etype": null
+        }
+      ]
+    }
+  },
+  {
+    "initial_expression": {
+      "Not": [
+        {
+          "Atomic": [
+            {
+              "Literal": {
+                "Bool": false
+              }
+            },
+            {
+              "clean": false,
+              "etype": null
+            }
+          ]
+        },
+        {
+          "clean": false,
+          "etype": null
+        }
+      ]
+    },
+    "rule_name": "apply_eval_constant",
+    "rule_set": [
+      [
+        "Constant",
+        9001
+      ]
+    ],
+    "transformed _expression": {
+      "Atomic": [
+        {
+          "Literal": {
+            "Bool": true
+          }
+        },
+        {
+          "clean": false,
+          "etype": null
+        }
+      ]
+    }
+  },
   {
     "initial_expression": {
       "Lt": [
@@ -178,175 +323,6 @@
         5000
       ]
     ],
-    "transformed _expression": {
-      "Not": [
-        {
-          "Not": [
-            {
-              "Not": [
-                {
-                  "Atomic": [
-                    {
-                      "Reference": {
-                        "UserName": "A"
-                      }
-                    },
-                    {
-                      "clean": false,
-                      "etype": null
-                    }
-                  ]
-                },
-                {
-                  "clean": false,
-                  "etype": null
-                }
-              ]
-            },
-            {
-              "clean": false,
-              "etype": null
-            }
-          ]
-        },
-        {
-          "clean": false,
-          "etype": null
-        }
-      ]
-    }
-  },
-  {
-    "initial_expression": {
-      "Not": [
-        {
-          "Not": [
-            {
-              "Not": [
-                {
-                  "Atomic": [
-                    {
-                      "Reference": {
-                        "UserName": "A"
-                      }
-                    },
-                    {
-                      "clean": false,
-                      "etype": null
-                    }
-                  ]
-                },
-                {
-                  "clean": false,
-                  "etype": null
-                }
-              ]
-            },
-            {
-              "clean": false,
-              "etype": null
-            }
-          ]
-        },
-        {
-          "clean": false,
-          "etype": null
-        }
-      ]
-    },
-    "rule_name": "remove_double_negation",
-    "rule_set": [
-      [
-        "Base",
-        8400
-      ]
-    ],
-    "transformed _expression": {
-      "Not": [
-        {
-          "Atomic": [
-            {
-              "Reference": {
-                "UserName": "A"
-              }
-            },
-            {
-              "clean": false,
-              "etype": null
-            }
-          ]
-        },
-        {
-          "clean": false,
-          "etype": null
-        }
-      ]
-    }
-  },
-  {
-    "initial_expression": {
-      "Atomic": [
-        {
-          "Reference": {
-            "UserName": "A"
-          }
-        },
-        {
-          "clean": false,
-          "etype": null
-        }
-      ]
-    },
-    "rule_name": "substitute_value_lettings",
-    "rule_set": [
-      [
-        "Base",
-        5000
-      ]
-    ],
-    "transformed _expression": {
-      "Atomic": [
-        {
-          "Literal": {
-            "Bool": false
-          }
-        },
-        {
-          "clean": false,
-          "etype": null
-        }
-      ]
-    }
-  },
-  {
-    "initial_expression": {
-      "Not": [
-        {
-          "Atomic": [
-            {
-              "Literal": {
-                "Bool": false
-              }
-            },
-            {
-              "clean": false,
-              "etype": null
-            }
-          ]
-        },
-        {
-          "clean": false,
-          "etype": null
-        }
-      ]
-    },
-    "rule_name": "apply_eval_constant",
-    "rule_set": [
-      [
-        "Constant",
-        9001
-      ]
-    ],
     "transformed _expression": {
       "Atomic": [
         {