Commit 4d6dcf7d authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

some more simplifications in CExp

parent 6149003d
......@@ -41,13 +41,17 @@ plus c1 c2 = Plus c1 c2
sum :: (Eq c, Num c) => [CExp c] -> CExp c
sum = foldl plus zero
sup :: Eq c => CExp c -> CExp c -> CExp c
sup c1 c2 | c1 == c2 = c1
sup :: (Eq c, Num c) => CExp c -> CExp c -> CExp c
sup c1 c2 | c1 == zero = c2
| c2 == zero = c1
| c1 == c2 = c1
sup c1 c2 = Sup c1 c2
cond :: Eq c => BExp -> CExp c -> CExp c -> CExp c
cond Top c _ = c
cond Bot _ d = d
cond _ c d
| c == d = c
cond g (Cond g' c1 c2) d
| c2 == d = cond (g .&& g') c1 d
cond g c d = Cond g c d
......@@ -60,12 +64,19 @@ divBy c 1 = c
divBy (Div c e) f = Div c (e * f)
divBy c f = Div c f
-- TODO: factor
simplify :: (Eq c, Num c) => CExp c -> CExp c
simplify (E e) = E (E.norm e)
simplify (Div c e) = simplify c `divBy` E.norm e
simplify (Plus c d) = simplify c `plus` simplify d
simplify (Sup c d) = simplify c `sup` simplify d
simplify (Cond g c d) = cond g (simplify c) (simplify d)
scale :: (Eq c, Num c) => E.Expression c -> CExp c -> CExp c
scale 0 _ = zero
scale 1 c = c
scale e (E f) = E (e * f)
scale e (Div d f) = scale e d `divBy` f
scale e (Div d f) = scale e' d `divBy` f' where
(_,(e',f')) = E.factor e f
scale e (Plus d1 d2) = scale e d1 `plus` scale e d2
scale e (Sup d1 d2) = scale e d1 `sup` scale e d2
scale e (Cond g d1 d2) = cond g (scale e d1) (scale e d2)
......
......@@ -12,6 +12,7 @@ module Data.PWhile.Expression
, constant
, variables
, factor
, P.norm
, Substitutable (..)
-- distributions
-- , Frac (..)
......
......@@ -193,7 +193,7 @@ type CExp = C.CExp Rational
type AExp = C.CExp SmtExpression
decode :: AExp -> SmtM CExp
decode = traverse decodeCoeff where
decode c = C.simplify <$> traverse decodeCoeff c where
decodeCoeff = fmap SMT.ratio . P.evalWithM SMT.getValue
encode :: CExp -> AExp
......
......@@ -24,7 +24,7 @@ import qualified GUBS.Polynomial as Poly (evalWith)
import Data.PWhile.BoolExpression
import qualified Data.PWhile.CostExpression as C
import Data.PWhile.Expression
import Data.PWhile.Expression hiding (norm)
import Data.PWhile.Program
import PWhile.InferEt (Result (..), ect, runAny)
import PWhile.Testbed.DSL (Program, gen)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment