@@ -2,24 +2,26 @@ package effekt.core.optimizer.normalizer.theories
22
33import effekt .core .Block .BlockVar
44import effekt .core .{Expr , Id , Type }
5+ import effekt .core .optimizer .normalizer .semantics .Neutral
56
67/**
78 * Theory for integers with neutral variables: multivariate Laurent polynomials with 64-bit signed integer coefficients.
9+ * Compare https://en.wikipedia.org/wiki/Laurent_polynomial
810 *
911 * KNOWN LIMITATION: This implementation assumes 64-bit signed integers.
1012 * Unfortunately, this is unsound for the JavaScript backend, which uses JavaScript numbers that are IEEE-754 doubles.
1113 */
1214object integers {
13- case class Integer (value : Long , addends : Addends ) {
14- val free : Set [Id ] = addends.flatMap { case (factors, _) => factors.keys }.toSet
15-
15+ case class IntegerRep (value : Long , addends : Addends ) {
16+ val free : Set [Id ] = addends.flatMap { case (factors, _) => factors.keys.flatMap(_.free) }.toSet
17+ def isLiteral : Boolean = addends.isEmpty
1618 def show : String = {
17- val Integer (v, a) = this
19+ val IntegerRep (v, a) = this
1820 val terms = a.map { case (factors, n) =>
1921 val factorStr = if (factors.isEmpty) " 1" else {
20- factors.map { case (id , exp) =>
21- if (exp == 1 ) s " ${id.name} "
22- else s " ${id.name} ^ $exp"
22+ factors.map { case (n , exp) =>
23+ if (exp == 1 ) " <neutral> "
24+ else s " <neutral> ^"
2325 }.mkString(" *"
2426 }
2527 if (n == 1 ) s " $factorStr"
@@ -36,24 +38,25 @@ object integers {
3638 }
3739 import Operation ._
3840
39- def embed (value : Long ): integers.Integer = Integer (value, Map .empty)
40- def embed (id : Id ): integers.Integer = Integer (0 , Map (Map (id -> 1 ) -> 1 ))
41+ def embed (value : Long ): integers.IntegerRep = IntegerRep (value, Map .empty)
42+ def embed (n : Neutral ): integers.IntegerRep = IntegerRep (0 , Map (Map (n -> 1 ) -> 1 ))
4143
42- def reify (value : Integer , embedBuiltinName : String => BlockVar ): Expr = Reify (embedBuiltinName).reify(value)
44+ def reify (value : IntegerRep , embedBuiltinName : String => BlockVar , embedNeutral : Neutral => Expr ): Expr =
45+ Reify (embedBuiltinName, embedNeutral).reify(value)
4346
4447 // 3 * x * x / y = Addend(3, Map(x -> 2, y -> -1))
4548 type Addends = Map [Factors , Long ]
46- type Factors = Map [Id , Int ]
49+ type Factors = Map [Neutral , Int ]
4750
48- def normalize (n : Integer ): Integer = normalized(n.value, n.addends)
51+ def normalize (n : IntegerRep ): IntegerRep = normalized(n.value, n.addends)
4952
50- def normalized (value : Long , addends : Addends ): Integer =
53+ def normalized (value : Long , addends : Addends ): IntegerRep =
5154 val (const, norm) = normalizeAddends(addends)
52- Integer (value + const, norm)
55+ IntegerRep (value + const, norm)
5356
54- def add (l : Integer , r : Integer ): Integer = (l, r) match {
57+ def add (l : IntegerRep , r : IntegerRep ): IntegerRep = (l, r) match {
5558 // 2 + (3 * x) + 4 + (5 * y) = 6 + (3 * x) + (5 * y)
56- case (Integer (x, xs), Integer (y, ys)) =>
59+ case (IntegerRep (x, xs), IntegerRep (y, ys)) =>
5760 normalized(x + y, add(xs, ys))
5861 }
5962
@@ -81,20 +84,20 @@ object integers {
8184 (constant, filtered)
8285 }
8386
84- def neg (l : Integer ): Integer = mul(l, - 1 )
87+ def neg (l : IntegerRep ): IntegerRep = mul(l, - 1 )
8588
8689 // (42 + 3*x + y) - (42 + 3*x + y) = (42 + 3*x + y) + (-1*42 + -1*3*x + -1*y)
87- def sub (l : Integer , r : Integer ): Integer =
90+ def sub (l : IntegerRep , r : IntegerRep ): IntegerRep =
8891 add(l, neg(r))
8992
90- def mul (l : Integer , factor : Long ): Integer = l match {
91- case Integer (value, addends) =>
92- Integer (value * factor, addends.map { case (f, n) => f -> n * factor })
93+ def mul (l : IntegerRep , factor : Long ): IntegerRep = l match {
94+ case IntegerRep (value, addends) =>
95+ IntegerRep (value * factor, addends.map { case (f, n) => f -> n * factor })
9396 }
9497
95- def mul (l : Integer , factor : Factors ): Integer = l match {
96- case Integer (value, addends) =>
97- Integer (0 , Map (factor -> value) ++ addends.map { case (f, n) =>
98+ def mul (l : IntegerRep , factor : Factors ): IntegerRep = l match {
99+ case IntegerRep (value, addends) =>
100+ IntegerRep (0 , Map (factor -> value) ++ addends.map { case (f, n) =>
98101 mul(f, factor) -> n
99102 })
100103 }
@@ -111,20 +114,20 @@ object integers {
111114
112115 // x1^2 * x2^0 * x3^3 = x1^2 * x3^3
113116 def normalizeFactors (f : Factors ): Factors =
114- f.filterNot { case (id , exp) => exp == 0 }
117+ f.filterNot { case (n , exp) => exp == 0 }
115118
116119 // (42 + 3*x + y) * (42 + 3*x + y)
117120 // =
118121 // (42 + 3*x + y) * 42 + (42 + 3*x + y) * 3*x + (42 + 3*x + y) * y
119- def mul (l : Integer , r : Integer ): Integer = r match {
120- case Integer (y, ys) =>
121- var sum : Integer = mul(l, y)
122+ def mul (l : IntegerRep , r : IntegerRep ): IntegerRep = r match {
123+ case IntegerRep (y, ys) =>
124+ var sum : IntegerRep = mul(l, y)
122125 ys.foreach { case (f, n) => sum = add(sum, mul(mul(l, n), f)) }
123126 normalize(sum)
124127 }
125128
126- case class Reify (embedBuiltinName : String => BlockVar ) {
127- def reifyVar (id : Id ): Expr = Expr . ValueVar (id, Type . TInt )
129+ case class Reify (embedBuiltinName : String => BlockVar , embedNeutral : Neutral => Expr ) {
130+ def reifyVar (n : Neutral ): Expr = embedNeutral(n )
128131
129132 def reifyInt (v : Long ): Expr = Expr .Literal (v, Type .TInt )
130133
@@ -135,8 +138,8 @@ object integers {
135138 case Div => Expr .PureApp (embedBuiltinName(" effekt::infixDiv(Int, Int)" List (), List (l, r))
136139 }
137140
138- def reify (v : Integer ): Expr =
139- val Integer (const, addends) = normalize(v)
141+ def reify (v : IntegerRep ): Expr =
142+ val IntegerRep (const, addends) = normalize(v)
140143
141144 val adds = addends.toList.map { case (factors, n) =>
142145 if (n == 1 ) reifyFactors(factors)
@@ -150,7 +153,7 @@ object integers {
150153 reifyInt(const)
151154 }
152155
153- def reifyFactor (x : Id , n : Int ): Expr =
156+ def reifyFactor (x : Neutral , n : Int ): Expr =
154157 if (n <= 0 ) sys error " Should not happen"
155158 else if (n == 1 ) reifyVar(x)
156159 else reifyOp(reifyVar(x), Mul , reifyFactor(x, n - 1 ))
0 commit comments