Skip to content

Smarter helper rules #682

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
yihozhang wants to merge 7 commits into from
Closed

Smarter helper rules #682

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
803957f
first attemp
yihozhang Nov 23, 2024
d01478b
test
yihozhang Nov 23, 2024
c28d700
small fix
yihozhang Nov 23, 2024
bea0e22
fix subtuple generator
yihozhang Nov 25, 2024
db81b98
fix test
yihozhang Nov 25, 2024
421d256
revert memory.rs change
yihozhang Nov 25, 2024
c91f879
big regression it seems?
yihozhang Nov 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion dag_in_context/src/optimizations/memory.egg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)

Expand Down
39 changes: 27 additions & 12 deletions dag_in_context/src/type_analysis.egg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,20 +5,34 @@
(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)
Copy link
Collaborator Author

@yihozhang yihozhang Nov 23, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The old TypeList-suffix based implementation is quadratic in the size of the list (which easily goes to 20+)


(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)
; (function TypeList-suffix (TypeList i64) TypeList :unextractable)

;; 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) ty)
; (TypeList-ith (TypeList-suffix list 0) i))
; ((= (TypeList-ith list i) ty)) :ruleset type-helpers)

; (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)

(rule ((TypeList-ith list i)
(= (TypeList-length list) n)
Expand Down Expand Up @@ -372,13 +386,14 @@
:ruleset type-analysis)

(rule (
(= e1 (Single e1-inner))
(= lhs (Concat e1 e2))
(HasType e1 (TupleT tylist1))
(HasType e1-inner (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)

; =================================
Expand Down
4 changes: 2 additions & 2 deletions dag_in_context/src/utility/add_context.egg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
3 changes: 3 additions & 0 deletions dag_in_context/src/utility/canonicalize.egg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions dag_in_context/src/utility/debug-helper.egg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,9 +31,9 @@
((delete (BinaryOpIsPure e)))
:ruleset debug-deletes)

(rule ((TypeList-suffix e a))
((delete (TypeList-suffix e a)))
:ruleset debug-deletes)
; (rule ((TypeList-suffix e a))
; ((delete (TypeList-suffix e a)))
; :ruleset debug-deletes)

(rule ((ContextOf e a))
((delete (ContextOf e a)))
Expand Down
3 changes: 2 additions & 1 deletion dag_in_context/src/utility/drop_at.egg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,8 @@
(DropAtInternal newty newctx idx c1))))
:ruleset drop)

(rule ((= lhs (DropAtInternal newty newctx idx (Concat c1 c2)))
(rule ((= c1 (Single c1-inner))
(= lhs (DropAtInternal newty newctx idx (Concat c1 c2)))
(ExprIsResolved (Concat c1 c2)))
((DelayedDropUnion lhs (Concat
(DropAtInternal newty newctx idx c1)
Expand Down
3 changes: 2 additions & 1 deletion dag_in_context/src/utility/subst.egg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
14 changes: 6 additions & 8 deletions dag_in_context/src/utility/util.egg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,18 +40,16 @@
: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)))
(rule ((Get (Concat expr1 expr2) 0)
(= expr1 (Single expr1-inner)))
((union (Get (Concat expr1 expr2) 0) expr1-inner))
:ruleset always-run)
;; descend right
(rule ((Get (Concat expr1 expr2) i)
(= (tuple-length expr1) len1)
(>= i len1))
(= expr1 (Single expr1-inner))
(> i 0))
((union (Get (Concat expr1 expr2) i)
(Get expr2 (- i len1))))
(Get expr2 (- i 1))))
:ruleset always-run)


Expand Down
2 changes: 1 addition & 1 deletion tests/snapshots/files__if_in_loop-optimize-sequential.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ expression: visualization.result
c2_: int = const 0;
c3_: int = const 1;
c4_: int = const 10;
v5_: bool = lt v0 c3_;
v5_: bool = le v0 c2_;
v6_: int = id c2_;
v7_: int = id c3_;
v8_: int = id v0;
Expand Down
2 changes: 1 addition & 1 deletion tests/snapshots/files__if_in_loop-optimize.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ expression: visualization.result
c2_: int = const 0;
c3_: int = const 1;
c4_: int = const 10;
v5_: bool = lt v0 c3_;
v5_: bool = le v0 c2_;
v6_: int = id c2_;
v7_: int = id c3_;
v8_: int = id v0;
Expand Down
93 changes: 47 additions & 46 deletions tests/snapshots/files__select-optimize-sequential.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,54 +16,55 @@ expression: visualization.result
v10_: bool = eq c9_ v5_;
v11_: bool = not v10_;
v12_: bool = not v11_;
v13_: int = id v4_;
v14_: int = id v5_;
v15_: int = id v6_;
v16_: int = id v7_;
br v12_ .b17_ .b18_;
.b17_:
v4_: int = id v13_;
v5_: int = id v14_;
v6_: int = id v15_;
v7_: int = id v16_;
.b19_:
br v11_ .b8_ .b20_;
v13_: bool = not v12_;
v14_: int = id v4_;
v15_: int = id v5_;
v16_: int = id v6_;
v17_: int = id v7_;
br v13_ .b18_ .b19_;
.b18_:
c21_: int = const 1;
v22_: int = add c21_ v6_;
v23_: bool = eq v22_ v7_;
v24_: int = add v22_ v4_;
v25_: int = id v24_;
v26_: int = id v5_;
v27_: int = id v22_;
v28_: int = id v7_;
br v23_ .b29_ .b30_;
c20_: int = const 1;
v21_: int = add c20_ v6_;
v22_: bool = eq v21_ v7_;
v23_: int = add v21_ v4_;
v24_: int = id v23_;
v25_: int = id v5_;
v26_: int = id v21_;
v27_: int = id v7_;
br v22_ .b28_ .b29_;
.b28_:
c30_: int = const 5;
v24_: int = id v23_;
v25_: int = id c30_;
v26_: int = id v21_;
v27_: int = id v7_;
v14_: int = id v24_;
v15_: int = id v25_;
v16_: int = id v26_;
v17_: int = id v27_;
v4_: int = id v14_;
v5_: int = id v15_;
v6_: int = id v16_;
v7_: int = id v17_;
.b31_:
br v11_ .b8_ .b32_;
.b29_:
c31_: int = const 5;
v25_: int = id v24_;
v26_: int = id c31_;
v27_: int = id v22_;
v28_: int = id v7_;
v13_: int = id v25_;
v14_: int = id v26_;
v15_: int = id v27_;
v16_: int = id v28_;
v4_: int = id v13_;
v5_: int = id v14_;
v6_: int = id v15_;
v7_: int = id v16_;
jmp .b19_;
.b30_:
v13_: int = id v25_;
v14_: int = id v26_;
v15_: int = id v27_;
v16_: int = id v28_;
v4_: int = id v13_;
v5_: int = id v14_;
v6_: int = id v15_;
v7_: int = id v16_;
jmp .b19_;
.b20_:
v14_: int = id v24_;
v15_: int = id v25_;
v16_: int = id v26_;
v17_: int = id v27_;
v4_: int = id v14_;
v5_: int = id v15_;
v6_: int = id v16_;
v7_: int = id v17_;
jmp .b31_;
.b19_:
v4_: int = id v14_;
v5_: int = id v15_;
v6_: int = id v16_;
v7_: int = id v17_;
jmp .b31_;
.b32_:
print v4_;
ret;
}