Smarter helper rules

dag_in_context/src/optimizations/memory.egg

@@ -240,7 +240,8 @@
 (rule ((PointsToCells (Get x i) ap))
       ((PointsToCells x ap))
       :ruleset memory-helpers)
-(rule ((PointsToCells (Concat x y) ap))
+(rule ((PointsToCells (Concat x y) ap)
+       (= x (Single x-inner)))
       ((PointsToCells x ap)
        (PointsToCells y ap))
       :ruleset memory-helpers)
@@ -254,6 +255,7 @@
            (UnwrapTuplePointsTo (PointsToCells x aps))
            (UnwrapTuplePointsTo (PointsToCells y aps))))
          :when ((= concat-x-y (Concat x y))
+                (= x (Single x-inner))
                 (HasType concat-x-y ty) (PointerishType ty))
          :ruleset memory-helpers)
 

dag_in_context/src/type_analysis.egg

@@ -5,20 +5,21 @@
 (rewrite (TLConcat (TNil) r) r :ruleset type-helpers)
 (rewrite (TLConcat (TCons hd tl) r)
          (TCons hd (TLConcat tl r))
+         :subsume
          :ruleset type-helpers)
 
 (function TypeList-length (TypeList) i64 :unextractable)
 (function TypeList-ith (TypeList i64) BaseType :unextractable)
-(function TypeList-suffix (TypeList i64) TypeList :unextractable)
 
-(rule ((TupleT tylist)) ((union (TypeList-suffix tylist 0) tylist)) :ruleset type-helpers)
-
-(rule ((= (TypeList-suffix top n) (TCons hd tl)))
-    ((union (TypeList-ith top n) hd)
-     (union (TypeList-suffix top (+ n 1)) tl)) :ruleset type-helpers)
-
-(rule ((= (TypeList-suffix list n) (TNil)))
-    ((set (TypeList-length list) n)) :ruleset type-helpers)
+;; Don't match on TypeList-ith because it is now lazily instantiated!
+(rule () ((set (TypeList-length (TNil)) 0)) :ruleset type-helpers)
+(rule ((= lst (TCons hd tl))
+       (= len (TypeList-length tl)))
+      ((set (TypeList-length lst) (+ 1 len))) :ruleset type-helpers)
+(rewrite (TypeList-ith (TCons hd tl) 0) hd :ruleset type-helpers)
+(rewrite (TypeList-ith (TCons hd tl) i) (TypeList-ith tl (- i 1)) 
+      :when ((> i 0)) 
+      :ruleset type-helpers)
 
 (rule ((TypeList-ith list i)
        (= (TypeList-length list) n)
@@ -372,13 +373,13 @@
       :ruleset type-analysis)
 
 (rule (
-        (= lhs (Concat e1 e2))
-        (HasType e1 (TupleT tylist1))
+        (= lhs (Concat (Single e1) e2))
+        (HasType e1 (Base t1))
         (HasType e2 (TupleT tylist2))
       )
       ; TLConcat needs to compute immediately, so we need to saturate type-helpers
       ; rules between every iter of type-analysis rules.
-      ((HasType lhs (TupleT (TLConcat tylist1 tylist2))))
+      ((HasType lhs (TupleT (TCons t1 tylist2))))
       :ruleset type-analysis)
 
 ; =================================

dag_in_context/src/utility/add_context.egg

@@ -63,9 +63,9 @@
 (rewrite (AddContext ctx (Single c1))
          (Single (AddContext ctx c1))
          :ruleset context)
-(rewrite (AddContext ctx (Concat c1 c2))
+(rewrite (AddContext ctx (Concat (Single c1) c2))
          (Concat
-           (AddContext ctx c1)
+           (Single (AddContext ctx c1))
            (AddContext ctx c2))
          :ruleset context)
 

dag_in_context/src/utility/canonicalize.egg

@@ -41,13 +41,16 @@
 ; Make Concats right-deep
 (rewrite (Concat (Concat a b) c)
          (Concat a (Concat b c))
+         :subsume
          :ruleset always-run)
 ; Simplify Concat's with empty
 (rewrite (Concat (Empty ty ctx) x)
          x
+         :subsume
          :ruleset always-run)
 (rewrite (Concat x (Empty ty ctx))
          x
+         :subsume
          :ruleset always-run)
 
 ; Make a tuple that is a sub-range of another tuple
@@ -56,36 +59,29 @@
 
 (rewrite (SubTuple expr x 0)
          (Empty ty ctx)
+         :subsume
          :when ((HasArgType expr ty) (ContextOf expr ctx))
          :ruleset always-run)
 
 (rewrite (SubTuple expr x 1)
          (Single (Get expr x))
+         :subsume
          :ruleset always-run)
 
 (rewrite (SubTuple expr a b)
          (Concat (Single (Get expr a)) (SubTuple expr (+ a 1) (- b 1)))
+         :subsume
          :when ((> b 1))
          :ruleset always-run)
 
-; Also figure out what existing expressions are subtuples of other things
-; this helps remove concat layers
-(rule ((Get expr i))
-      ((union (Single (Get expr i))
-              (SubTuple expr i 1)))
+; ;; This rule makes sure every tuple can be 
+; ;; normalized as a list of (Concat (Single e1) (Concat (Single e2) ...))
+(rewrite e (SubTuple e 0 len)
+      :when ((tuples-to-generate-get-for e)
+             (HasType e (TupleT t))
+             (= len (TypeList-length t)))
       :ruleset always-run)
 
-(rewrite (Concat (SubTuple expr a b)
-                 (SubTuple expr (+ a b) c))
-         (SubTuple expr a (+ b c))
-         :ruleset always-run)
-;; a subtuple which is the entire tuple is the tuple itself
-;; this removes unecessary layers of concat
-(rewrite (SubTuple expr 0 len)
-         expr
-         :when ((= len (tuple-length expr)))
-         :ruleset always-run)
-
 ; Helper functions to remove one element from a tuple or type list
 ;                           tuple    idx
 (function TupleRemoveAt    (Expr     i64) Expr     :unextractable)

dag_in_context/src/utility/debug-helper.egg

@@ -31,10 +31,6 @@
       ((delete (BinaryOpIsPure e)))
       :ruleset debug-deletes)
 
-(rule ((TypeList-suffix e a))
-      ((delete (TypeList-suffix e a)))
-      :ruleset debug-deletes)
-
 (rule ((ContextOf e a))
       ((delete (ContextOf e a)))
       :ruleset debug-deletes)

dag_in_context/src/utility/drop_at.egg

@@ -89,7 +89,9 @@
       :ruleset drop)
 
 (rule ((= lhs (DropAtInternal newty newctx idx (Concat c1 c2)))
-       (ExprIsResolved (Concat c1 c2)))
+       (ExprIsResolved (Concat c1 c2))
+       ;; canonicalize Concat to be right deep
+       (= c1 (Single c1-inner)))
       ((DelayedDropUnion lhs (Concat
             (DropAtInternal newty newctx idx c1)
             (DropAtInternal newty newctx idx c2))))

dag_in_context/src/utility/subst.egg

@@ -106,7 +106,8 @@
       ((DelayedSubstUnion lhs
          (Single (Subst assum to c1))))
          :ruleset subst)
-(rule ((= e (Concat c1 c2))
+(rule ((= c1 (Single c1-inner))
+       (= e (Concat c1 c2))
        (= lhs (Subst assum to e))
        (ExprIsResolved e))
       ((DelayedSubstUnion lhs

dag_in_context/src/utility/util.egg

@@ -25,34 +25,72 @@
        (= len (TypeList-length tl)))
       ((set (tuple-length expr) len)) :ruleset always-run)
 
+(relation tuples-to-generate-get-for (Expr))
+(relation tuples-to-generate-get-for-list (ListExpr))
+
+(rule ((= e (DoWhile inputs pred_out)))
+      ((tuples-to-generate-get-for e)
+       (tuples-to-generate-get-for inputs)
+       (tuples-to-generate-get-for pred_out))
+      :ruleset always-run)
+(rule ((= e (If cond inputs thn els)))
+       ((tuples-to-generate-get-for e)
+        (tuples-to-generate-get-for inputs)
+        (tuples-to-generate-get-for thn)
+        (tuples-to-generate-get-for els))
+       :ruleset always-run)
+(rule ((= e (Switch pred inputs branch)))
+      ((tuples-to-generate-get-for e)
+       (tuples-to-generate-get-for-list branch)
+       (tuples-to-generate-get-for inputs))
+       :ruleset always-run)
+(rule ((tuples-to-generate-get-for-list (Cons hd tl)))
+      ((tuples-to-generate-get-for hd)
+       (tuples-to-generate-get-for-list tl))
+      :ruleset always-run)
+(rule ((= e (Arg t a)))
+      ((tuples-to-generate-get-for e))
+      :ruleset always-run)
+
+
 ;; Create a Get for every index, and rewrite it to see through Concat
-(rule ((Single expr)) ((union (Get (Single expr) 0) expr)) :ruleset always-run)
+; (rule ((Single expr)) ((union (Get (Single expr) 0) expr)) :ruleset always-run)
 ;; initial get
-(rule ((> (tuple-length tuple) 0))
+(rule ((> (tuple-length tuple) 0)
+       (tuples-to-generate-get-for tuple))
       ((Get tuple 0))
       :ruleset always-run)
 ;; next get
 (rule ((= len (tuple-length tuple))
        (= ith (Get tuple i))
        (< (+ i 1) len)
+       (tuples-to-generate-get-for tuple)
        )
        ((Get tuple (+ 1 i)))
        :ruleset always-run)
 
-;; descend left
-(rule ((Get (Concat expr1 expr2) i)
-       (= (tuple-length expr1) len1)
-       (< i len1))
-      ((union (Get (Concat expr1 expr2) i)
-              (Get expr1 i)))
-       :ruleset always-run)
-;; descend right
-(rule ((Get (Concat expr1 expr2) i)
-       (= (tuple-length expr1) len1)
-       (>= i len1))
-      ((union (Get (Concat expr1 expr2) i)
-              (Get expr2 (- i len1))))
-       :ruleset always-run)
+(function List-suffix (Expr i64) Expr)
+(rule ((Get x i))
+      ((union (List-suffix x 0) x))
+      :ruleset always-run)
+(rule ((= (List-suffix x n) (Concat (Single hd) tl)))
+      ((union (List-suffix x (+ n 1)) tl))
+      :ruleset always-run)
+(rule ((= lhs (Get x i))
+       (= (List-suffix x i) (Concat (Single e) rest)))
+      ((union lhs e))
+      :ruleset always-run)
+(rule ((= lhs (Get x i))
+       (= (List-suffix x i) (Single e)))
+      ((union lhs e))
+      :ruleset always-run)
+; ;; descend left
+; (rewrite (Get (Concat (Single expr1) expr2) 0) expr1
+;        :ruleset always-run)
+; ;; descend right
+; (rewrite (Get (Concat (Single expr1) expr2) i) (Get expr2 (- i 1))
+;        :when ((> i 0))
+;        :ruleset always-run)
 
 
 ;; A temporary context.

dag_in_context/src/utility/util.rs

@@ -78,13 +78,28 @@ fn test_tuple_ith() -> crate::Result {
                   (Concat (Single (Const (Int 0) {emptyt} {ctx})) (Single (Const (Int 1) {emptyt} {ctx})))
                   (Concat (Single (Const (Int 2) {emptyt} {ctx})) (Single (Const (Int 3) {emptyt} {ctx})))))
 
+    ;; Gets of tup and tup2 are only generated when tup and tup2 are in critical positions
+    ;; like inputs to a DoWhile, 
+    (let tup_type (TupleT (TCons (IntT) (TCons (IntT) (TCons (IntT) (TCons (IntT) (TNil)))))))
+    (let body (Concat (Const (Bool true) tup_type (TmpCtx)) (Arg tup_type (TmpCtx))))
+    (let loop (DoWhile tup body))
+    (union (TmpCtx) (InLoop tup body))
+    (delete (TmpCtx))
+
     ;; with print
     (let tup2 (Concat 
                 (Concat 
                     (Single (Bop (Print) (Const (Int 0) {emptyt} {ctx}) (Arg (Base (StateT)) {ctx})))
                     (Concat (Single (Const (Int 1) {emptyt} {ctx})) 
                                 (Single (Const (Int 2) {emptyt} {ctx}))))
                 (Single (Const (Int 3) {emptyt} {ctx}))))
+
+    (let tup2_type (TupleT (TCons (StateT) (TCons (IntT) (TCons (IntT) (TCons (IntT) (TNil)))))))
+    (let body2 (Concat (Const (Bool true) tup2_type (TmpCtx)) (Arg tup2_type (TmpCtx))))
+    (let loop2 (DoWhile tup2 body2))
+    (union (TmpCtx) (InLoop tup2 body2))
+    (delete (TmpCtx))
+
     "
     );
 

tests/snapshots/files__block-diamond-optimize-sequential.snap

@@ -8,31 +8,22 @@ expression: visualization.result
   c2_: int = const 1;
   c3_: int = const 2;
   v4_: bool = lt v0 c3_;
-  c5_: int = const 0;
-  c6_: int = const 5;
-  v7_: int = id c2_;
+  c5_: int = const 4;
+  v6_: int = select v4_ c5_ c2_;
+  v7_: int = id v6_;
   v8_: int = id c2_;
-  v9_: int = id c3_;
-  br v4_ .b10_ .b11_;
+  br v4_ .b9_ .b10_;
+.b9_:
+  v11_: int = add c2_ v7_;
+  print v11_;
+  ret;
+  jmp .b12_;
 .b10_:
-  c12_: int = const 4;
-  v7_: int = id c12_;
+  v13_: int = add c3_ v6_;
+  v7_: int = id v13_;
   v8_: int = id c2_;
-  v9_: int = id c3_;
-  v13_: int = id v7_;
-  v14_: int = id v8_;
-  v15_: int = add c2_ v13_;
-  print v15_;
-  ret;
-  jmp .b16_;
-.b11_:
-  v13_: int = id v7_;
-  v14_: int = id v8_;
-  v17_: int = add v7_ v9_;
-  v13_: int = id v17_;
-  v14_: int = id v8_;
-  v15_: int = add c2_ v13_;
-  print v15_;
+  v11_: int = add c2_ v7_;
+  print v11_;
   ret;
-.b16_:
+.b12_:
 }

tests/snapshots/files__block-diamond-optimize.snap

@@ -8,31 +8,22 @@ expression: visualization.result
   c2_: int = const 1;
   c3_: int = const 2;
   v4_: bool = lt v0 c3_;
-  c5_: int = const 0;
-  c6_: int = const 5;
-  v7_: int = id c2_;
+  c5_: int = const 4;
+  v6_: int = select v4_ c5_ c2_;
+  v7_: int = id v6_;
   v8_: int = id c2_;
-  v9_: int = id c3_;
-  br v4_ .b10_ .b11_;
+  br v4_ .b9_ .b10_;
+.b9_:
+  v11_: int = add c2_ v7_;
+  print v11_;
+  ret;
+  jmp .b12_;
 .b10_:
-  c12_: int = const 4;
-  v7_: int = id c12_;
+  v13_: int = add c3_ v6_;
+  v7_: int = id v13_;
   v8_: int = id c2_;
-  v9_: int = id c3_;
-  v13_: int = id v7_;
-  v14_: int = id v8_;
-  v15_: int = add c2_ v13_;
-  print v15_;
-  ret;
-  jmp .b16_;
-.b11_:
-  v13_: int = id v7_;
-  v14_: int = id v8_;
-  v17_: int = add v7_ v9_;
-  v13_: int = id v17_;
-  v14_: int = id v8_;
-  v15_: int = add c2_ v13_;
-  print v15_;
+  v11_: int = add c2_ v7_;
+  print v11_;
   ret;
-.b16_:
+.b12_:
 }

tests/snapshots/files__collatz_redundant_computation-optimize-sequential.snap

@@ -19,7 +19,7 @@ expression: visualization.result
   v13_: bool = eq v7_ v8_;
   v14_: int = id v6_;
   v15_: int = id v7_;
-  v16_: int = id v8_;
+  v16_: int = id v7_;
   v17_: int = id v9_;
   v18_: int = id v10_;
   v19_: int = id v11_;