expressions 0.1.9 → 0.2

raw patch · 4 files changed

+42/−3 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

+ Data.Expression.Utils.Indexed.Sum: embed :: (IFunctor f, f :<<: g) => IFix f i -> IFix g i

+ Data.Expression.Utils.Indexed.Sum: instance forall i (f :: (i -> *) -> i -> *). Data.Expression.Utils.Indexed.Functor.IFunctor f => f Data.Expression.Utils.Indexed.Sum.:<<: f

+ Data.Expression.Utils.Indexed.Sum: instance forall k (f :: (k -> *) -> k -> *) (g :: (k -> *) -> k -> *) (h :: (k -> *) -> k -> *). (Data.Expression.Utils.Indexed.Functor.IFunctor f, Data.Expression.Utils.Indexed.Functor.IFunctor g, Data.Expression.Utils.Indexed.Functor.IFunctor h, f Data.Expression.Utils.Indexed.Sum.:<<: g) => f Data.Expression.Utils.Indexed.Sum.:<<: (h Data.Expression.Utils.Indexed.Sum.:+: g)

+ Data.Expression.Utils.Indexed.Sum: instance forall k (f :: (k -> *) -> k -> *) (g :: (k -> *) -> k -> *). (Data.Expression.Utils.Indexed.Functor.IFunctor f, Data.Expression.Utils.Indexed.Functor.IFunctor g) => f Data.Expression.Utils.Indexed.Sum.:<<: (g Data.Expression.Utils.Indexed.Sum.:+: f)

+ Data.Expression.Utils.Indexed.Sum: restrict :: (ITraversable g, f :<<: g) => IFix g i -> Maybe (IFix f i)

- Data.Expression.Utils.Indexed.Sum: class (IFunctor f, IFunctor g) => f :<: g

+ Data.Expression.Utils.Indexed.Sum: class (IFunctor f, IFunctor g) => f :<<: g

Files

ChangeLog.md +4/−0
expressions.cabal +1/−1
src/Data/Expression/Utils/Indexed/Sum.hs +29/−1
test/Main.hs +8/−1

ChangeLog.md view

@@ -1,5 +1,9 @@ # Change Log +## 0.2++* Add `embed` and `restrict` to convert between expression languages+ ## 0.1.9  * Bump dependencies

expressions.cabal view

@@ -1,5 +1,5 @@ name:                expressions-version:             0.1.9+version:             0.2 synopsis:            Expressions and Formulae a la carte description:   This package is aimed at providing means of fixing a first-order language and

src/Data/Expression/Utils/Indexed/Sum.hs view

@@ -13,8 +13,10 @@ -- Stability  :  experimental -------------------------------------------------------------------------------- -module Data.Expression.Utils.Indexed.Sum ((:+:)(..), (:<:)(..), inject, match) where+module Data.Expression.Utils.Indexed.Sum ((:+:)(..), (:<:)(..), (:<<:), inject, match, embed, restrict) where +import Control.Monad+ import Data.Expression.Utils.Indexed.Eq import Data.Expression.Utils.Indexed.Foldable import Data.Expression.Utils.Indexed.Functor@@ -50,6 +52,24 @@     prj (InL _) = Nothing     prj (InR a) = prj a +class (IFunctor f, IFunctor g) => f :<<: g where+    emb :: f a i -> g a i+    res :: g a i -> Maybe (f a i)++instance IFunctor f => f :<<: f where+    emb = id+    res = Just++instance (IFunctor f, IFunctor g) => f :<<: (g :+: f) where+    emb = InR+    res (InL _) = Nothing+    res (InR a) = Just a++instance {-# OVERLAPPABLE #-} (IFunctor f, IFunctor g, IFunctor h, f :<<: g) => f :<<: (h :+: g) where+    emb = InR . emb+    res (InL _) = Nothing+    res (InR a) = res a+ -- | Inject a component into a sum. inject :: g :<: f => forall i. g (IFix f) i -> IFix f i inject = IFix . inj@@ -57,6 +77,14 @@ -- | Try to unpack a sum into a component. match :: g :<: f => forall i. IFix f i -> Maybe (g (IFix f) i) match = prj . unIFix++-- | Embed a subset in a superset.+embed :: (IFunctor f, f :<<: g) => IFix f i -> IFix g i+embed = icata (IFix . emb)++-- | Try to restrict a superset to a subset.+restrict :: (ITraversable g, f :<<: g) => IFix g i -> Maybe (IFix f i)+restrict = fmap IFix . res <=< (itraverse restrict) . unIFix  instance (IEq1 f, IEq1 g) => IEq1 (f :+: g) where     InL a `ieq1` InL b = a `ieq1` b

test/Main.hs view

@@ -38,7 +38,10 @@             , e4 == parseJust "(select (a : array int (array int bool)) (+ (b : int) 3))"             , e5 == parseJust "(forall ((x : int)) (exists ((y : int)) (and true (= (b : bool) (< x y)))))"             , e6 == parseJust "(and (forall ((x : int) (y : int)) (< x (+ y (z : int)))) (= z 3))"-            , e7 == e8 ]+            , e7 == e8+            , e9 == e10+            , isJust (restrict e9 :: Maybe (QFALia ('ArraySort 'IntegralSort 'BooleanSort)))+            , isNothing (restrict e5 :: Maybe (QFLia 'BooleanSort)) ]      e1, e2, e3 :: ALia 'IntegralSort     e1 = a@@ -55,3 +58,7 @@     e7, e8 :: Lia 'IntegralSort     e7 = a .*. (a .+. c3) `substitute` (c3 `for` (a .+. c3))     e8 = inject (Mul [a, c3])++    e9, e10 :: ALia ('ArraySort 'IntegralSort 'BooleanSort)+    e9  = select a (b .+. c3)+    e10 = embed e4