Skip to content

Commit

Permalink
Merge pull request #615 from egraphs-good/kirstenmg-type-rulesets
Browse files Browse the repository at this point in the history
Add type helper error checking
  • Loading branch information
kirstenmg authored May 29, 2024
2 parents 34e1a85 + fa073ba commit 0d33fc7
Showing 1 changed file with 12 additions and 5 deletions.
17 changes: 12 additions & 5 deletions dag_in_context/src/utility/canonicalize.egg
Original file line number Diff line number Diff line change
Expand Up @@ -71,17 +71,24 @@
; Helper functions to remove one element from a tuple or type list
; tuple idx
(function TupleRemoveAt (Expr i64) Expr :unextractable)
(function TypeListRemoveAt (TypeList i64) TypeList :unextractable)

(rewrite (TupleRemoveAt tuple idx)
(Concat (SubTuple tuple 0 idx)
(SubTuple tuple (+ idx 1) (- len (+ idx 1))))
:when ((= len (tuple-length tuple)))
:ruleset always-run)
(rule ((TupleRemoveAt tuple idx)
(= len (tuple-length tuple))
(>= idx len))
((panic "Index out of bounds for TupleRemoveAt")) :ruleset always-run)


(rewrite (TypeListRemoveAt (TNil) _idx) (TNil) :ruleset always-run)
(rewrite (TypeListRemoveAt (TCons x xs) 0 ) xs :ruleset always-run)
(function TypeListRemoveAt (TypeList i64) TypeList :unextractable)
(rewrite (TypeListRemoveAt (TNil) _idx) (TNil) :ruleset type-helpers)
(rewrite (TypeListRemoveAt (TCons x xs) 0 ) xs :ruleset type-helpers)
(rewrite (TypeListRemoveAt (TCons x xs) idx)
(TCons x (TypeListRemoveAt xs (- idx 1)))
:when ((> idx 0))
:ruleset always-run)
:ruleset type-helpers)

(rule ((TypeListRemoveAt (TNil) _idx))
((panic "Index out of bounds for TypeListRemoveAt.")) :ruleset type-helpers)

0 comments on commit 0d33fc7

Please sign in to comment.