packages feed

expressions 0.2 → 0.3

raw patch · 13 files changed

+71/−51 lines, 13 filesdep ~singletons

Dependency ranges changed: singletons

Files

ChangeLog.md view
@@ -1,5 +1,9 @@ # Change Log +## 0.3++* Cleanup, GHC 8.6+ ## 0.2  * Add `embed` and `restrict` to convert between expression languages
expressions.cabal view
@@ -1,5 +1,5 @@ name:                expressions-version:             0.2+version:             0.3 synopsis:            Expressions and Formulae a la carte description:   This package is aimed at providing means of fixing a first-order language and@@ -75,7 +75,7 @@                        containers >=0.5.7 && <0.7,                        free >=4.2 && <5.2,                        lattices >=1.6 && <1.8,-                       singletons >=2.2 && <2.5,+                       singletons >=2.2 && <2.6,                        text >=1.2 && <1.3,                        transformers >=0.5.2 && <0.6   hs-source-dirs:      src
src/Data/Expression.hs view
@@ -2,6 +2,7 @@            , FlexibleContexts            , FlexibleInstances            , GADTs+           , InstanceSigs            , MultiParamTypeClasses            , OverloadedStrings            , RankNTypes@@ -78,6 +79,7 @@                         -- Smart expression constructors                        , var+                       , dynvar                        , true                        , false                        , and@@ -101,6 +103,9 @@                        , vars                        , freevars +                       -- Utilities+                       , freenames+                        -- Predicates                        , MaybeQuantified                        , isQuantified@@ -126,6 +131,7 @@ import Control.Monad.Trans.Class import Control.Monad.Trans.Reader import Control.Monad.Trans.State+import Data.Coerce import Data.Functor.Identity import Data.List hiding (and, or, union) import Data.Map hiding (map, drop, foldl, foldr, mapMaybe, partition)@@ -278,7 +284,7 @@             var''' n s          var''' :: VariableName -> DynamicSort -> Parser (DynamicallySorted f)-        var''' n (DynamicSort (s :: Sing s)) = return $ DynamicallySorted s (inject (Var n s))+        var''' n (DynamicSort (s :: Sing s)) = return $ dynvar n s  -- | A smart constructor for variables of any sort in any language -- Takes the variable name and infers the target language and sort from context.@@ -289,11 +295,15 @@ var :: forall f s. ( VarF :<: f, SingI s ) => VariableName -> IFix f s var n = inject (Var n (sing :: Sing s)) +-- | Like @var@ except it hides the sort inside @DynamicallySorted@+dynvar :: forall f (s :: Sort). VarF :<: f => VariableName -> Sing s -> DynamicallySorted f+dynvar n s = DynamicallySorted s $ withSort s $ var n+ -- | Collects a list of all variables occurring in an expression (bound or free). vars :: ( VarF :<: f, IFoldable f, IFunctor f ) => IFix f s -> [DynamicallySorted VarF] vars = nub . F.getConst . icata vars' where     vars' a = case prj a of-        Just (Var n s) -> F.Const [DynamicallySorted s . inject $ Var n s]+        Just (Var n s) -> F.Const [dynvar n s]         Nothing -> ifold a  -- | Substitution that given an expression produces replacement if the expression is to be replaced or nothing otherwise.@@ -352,10 +362,12 @@     index Not {} = SBooleanSort  instance IFoldable ConjunctionF where-    ifold (And as) = F.Const . mconcat . map F.getConst $ as+    ifold :: forall m (s :: Sort). Monoid m => ConjunctionF (F.Const m) s -> F.Const m s+    ifold (And as) = coerce (mconcat :: [m] -> m) as  instance IFoldable DisjunctionF where-    ifold (Or os) = F.Const . mconcat . map F.getConst $ os+    ifold :: forall m (s :: Sort). Monoid m => DisjunctionF (F.Const m) s -> F.Const m s+    ifold (Or os) = coerce (mconcat :: [m] -> m) os  instance IFoldable NegationF where     ifold (Not n) = n@@ -370,15 +382,15 @@     itraverse f (Not n) = Not <$> f n  instance IShow ConjunctionF where-    ishow (And []) = F.Const $ "true"-    ishow (And as) = F.Const $ "(and " ++ intercalate " " (map F.getConst as) ++ ")"+    ishow (And []) = coerce ("true" :: String)+    ishow (And as) = coerce $ "(and " ++ intercalate " " (coerce as) ++ ")"  instance IShow DisjunctionF where-    ishow (Or []) = F.Const $ "false"-    ishow (Or os) = F.Const $ "(or "  ++ intercalate " " (map F.getConst os) ++ ")"+    ishow (Or []) = coerce ("false" :: String)+    ishow (Or os) = coerce $ "(or "  ++ intercalate " " (coerce os) ++ ")"  instance IShow NegationF where-    ishow (Not n)  = F.Const $ "(not " ++ F.getConst n ++ ")"+    ishow (Not n)  = coerce $ "(not " ++ coerce n ++ ")"  instance ConjunctionF :<: f => Parseable ConjunctionF f where     parser _ r = choice [ true',  and' ] <?> "Conjunction" where@@ -545,10 +557,10 @@     itraverse f (Exists vs b) = Exists vs <$> f b  instance IShow (UniversalF v) where-    ishow (Forall vs phi) = F.Const $ "(forall (" ++ intercalate " " (map show vs) ++ ") " ++ F.getConst phi ++ ")"+    ishow (Forall vs phi) = coerce $ "(forall (" ++ intercalate " " (map show vs) ++ ") " ++ coerce phi ++ ")"  instance IShow (ExistentialF v) where-    ishow (Exists vs phi) = F.Const $ "(exists (" ++ intercalate " " (map show vs) ++ ") " ++ F.getConst phi ++ ")"+    ishow (Exists vs phi) = coerce $ "(exists (" ++ intercalate " " (map show vs) ++ ") " ++ coerce phi ++ ")"  instance ( UniversalF v :<: f, SingI v ) => Parseable (UniversalF v) f where     parser _ r = forall' <?> "Universal" where@@ -603,16 +615,16 @@     freevars' :: f (F.Const [DynamicallySorted VarF]) s -> F.Const [DynamicallySorted VarF] s  instance MaybeQuantified VarF where-    isQuantified' _ = F.Const (Any False)-    freevars' (Var n s) = F.Const [DynamicallySorted s . inject $ Var n s]+    isQuantified' _ = coerce False+    freevars' (Var n s) = coerce [dynvar n s]  instance MaybeQuantified (UniversalF v) where-    isQuantified' _ = F.Const (Any True)-    freevars' (Forall vs a) = F.Const . P.filter (`notElem` map (\v@(IFix (Var _ s)) -> DynamicallySorted s v) vs) . F.getConst $ a+    isQuantified' _ = coerce True+    freevars' (Forall vs a) = coerce (P.filter (`notElem` map (\v@(IFix (Var _ s)) -> DynamicallySorted s v) vs)) a  instance MaybeQuantified (ExistentialF v) where-    isQuantified' _ = F.Const (Any True)-    freevars' (Exists vs a) = F.Const . P.filter (`notElem` map (\v@(IFix (Var _ s)) -> DynamicallySorted s v) vs) . F.getConst $ a+    isQuantified' _ = coerce True+    freevars' (Exists vs a) = coerce (P.filter (`notElem` map (\v@(IFix (Var _ s)) -> DynamicallySorted s v) vs)) a  instance ( MaybeQuantified f, MaybeQuantified g ) => MaybeQuantified (f :+: g) where     isQuantified' (InL fa) = isQuantified' fa@@ -626,7 +638,7 @@  -- | Test whether an expression contains a quantifier. isQuantified :: MaybeQuantified f => IFix f s -> Bool-isQuantified = getAny . F.getConst . isQuantified' . unIFix+isQuantified = coerce . isQuantified' . unIFix  -- | Tests whether an expression is free of any quantifier. isQuantifierFree :: MaybeQuantified f => IFix f s -> Bool@@ -634,7 +646,7 @@  -- | Collects a list of all free variables occurring in an expression. freevars :: ( IFunctor f, MaybeQuantified f ) => IFix f s -> [DynamicallySorted VarF]-freevars = nub . F.getConst . icata freevars'+freevars = nub . coerce . icata freevars'  -- | A smart constructor for universally quantified formulae forall :: UniversalF v :<: f => [Var v] -> IFix f 'BooleanSort -> IFix f 'BooleanSort
src/Data/Expression/Arithmetic.hs view
@@ -29,6 +29,7 @@                                   , (.<=.)                                   , (.>=.) ) where +import Data.Coerce import Data.List import Data.Maybe import Data.Monoid@@ -77,11 +78,11 @@     index LessThan {} = SBooleanSort  instance IFoldable ArithmeticF where-    ifold (Const _) = F.Const $ mempty-    ifold (Add as)  = F.Const . mconcat . map F.getConst $ as-    ifold (Mul ms)  = F.Const . mconcat . map F.getConst $ ms-    ifold (_ `Divides` a)  = F.Const . F.getConst $ a-    ifold (a `LessThan` b) = F.Const (F.getConst a) <> F.Const (F.getConst b)+    ifold (Const _) = mempty+    ifold (Add as)  = mconcat as+    ifold (Mul ms)  = mconcat ms+    ifold (_ `Divides` a)  = coerce a+    ifold (a `LessThan` b) = coerce a <> coerce b  instance ITraversable ArithmeticF where     itraverse _ (Const c) = pure (Const c)@@ -91,11 +92,11 @@     itraverse f (a `LessThan` b) = LessThan <$> f a <*> f b  instance IShow ArithmeticF where-    ishow (Const c)        = F.Const $ show c-    ishow (Add as)         = F.Const $ "(+ " ++ intercalate " " (map F.getConst as) ++ ")"-    ishow (Mul ms)         = F.Const $ "(* " ++ intercalate " " (map F.getConst ms) ++ ")"-    ishow (c `Divides`  a) = F.Const $ "(" ++ show c ++ "| " ++ F.getConst a ++ ")"-    ishow (a `LessThan` b) = F.Const $ "(< " ++ F.getConst a ++ " " ++ F.getConst b ++ ")"+    ishow (Const c)        = coerce $ show c+    ishow (Add as)         = coerce $ "(+ " ++ intercalate " " (coerce as) ++ ")"+    ishow (Mul ms)         = coerce $ "(* " ++ intercalate " " (coerce ms) ++ ")"+    ishow (c `Divides`  a) = coerce $ "(" ++ show c ++ "| " ++ coerce a ++ ")"+    ishow (a `LessThan` b) = coerce $ "(< " ++ coerce a ++ " " ++ coerce b ++ ")"  instance ArithmeticF :<: f => Parseable ArithmeticF f where     parser _ r = choice [ cnst', add', mul', divides', lessThan' ] <?> "Arithmetic" where
src/Data/Expression/Array.hs view
@@ -21,6 +21,7 @@                              , select                              , store ) where +import Data.Coerce import Data.Functor.Const import Data.Singletons import Data.Singletons.Decide@@ -54,16 +55,16 @@     index (Store  is es _ _ _) = SArraySort is es  instance IFoldable ArrayF where-    ifold (Select _ _ a i)   = Const (getConst a) <> Const (getConst i)-    ifold (Store  _ _ a i e) = Const (getConst a) <> Const (getConst i) <> Const (getConst e)+    ifold (Select _ _ a i)   = coerce a <> coerce i+    ifold (Store  _ _ a i e) = coerce a <> coerce i <> coerce e  instance ITraversable ArrayF where     itraverse f (Select is es a i)   = Select is es <$> f a <*> f i     itraverse f (Store  is es a i e) = Store  is es <$> f a <*> f i <*> f e  instance IShow ArrayF where-    ishow (Select _ _ a i)   = Const $ "(select " ++ getConst a ++ " " ++ getConst i ++ ")"-    ishow (Store  _ _ a i v) = Const $ "(store " ++ getConst a ++ " " ++ getConst i ++ " " ++ getConst v ++ ")"+    ishow (Select _ _ a i)   = coerce $ "(select " ++ coerce a ++ " " ++ coerce i ++ ")"+    ishow (Store  _ _ a i v) = coerce $ "(store " ++ coerce a ++ " " ++ coerce i ++ " " ++ coerce v ++ ")"  instance ArrayF :<: f => Parseable ArrayF f where     parser _ r = choice [ select', store' ] <?> "Array" where
src/Data/Expression/Equality.hs view
@@ -20,6 +20,7 @@ module Data.Expression.Equality ( EqualityF(..)                                 , (.=.) ) where +import Data.Coerce import Data.Functor.Const import Data.Singletons import Data.Singletons.Decide@@ -47,13 +48,13 @@     index (Equals _ _ _) = SBooleanSort  instance IFoldable EqualityF where-    ifold (Equals _ a b) = Const (getConst a) <> Const (getConst b)+    ifold (Equals _ a b) = coerce a <> coerce b  instance ITraversable EqualityF where     itraverse f (Equals s a b) = Equals s <$> f a <*> f b  instance IShow EqualityF where-    ishow (Equals _ a b) = Const $ "(= " ++ getConst a ++ " " ++ getConst b ++ ")"+    ishow (Equals _ a b) = coerce $ "(= " ++ coerce a ++ " " ++ coerce b ++ ")"  instance EqualityF :<: f => Parseable EqualityF f where     parser _ r = do
src/Data/Expression/IfThenElse.hs view
@@ -1,6 +1,7 @@ {-# LANGUAGE FlexibleContexts            , FlexibleInstances            , GADTs+           , InstanceSigs            , MultiParamTypeClasses            , OverloadedStrings            , RankNTypes@@ -20,6 +21,7 @@ module Data.Expression.IfThenElse ( IfThenElseF(..)                                   , ite ) where +import Data.Coerce import Data.Functor.Const import Data.Singletons import Data.Singletons.Decide@@ -47,13 +49,14 @@     index (IfThenElse s _ _ _) = s  instance IFoldable IfThenElseF where-    ifold (IfThenElse _ i t e) = Const $ getConst i <> getConst t <> getConst e+    ifold :: forall m (s :: Sort). Monoid m => IfThenElseF (Const m) s -> Const m s+    ifold (IfThenElse _ i t e) = coerce ((coerce i <> coerce t <> coerce e) :: m)  instance ITraversable IfThenElseF where     itraverse f (IfThenElse s i t e) = IfThenElse s <$> f i <*> f t <*> f e  instance IShow IfThenElseF where-    ishow (IfThenElse _ i t e) = Const $ "(ite " ++ getConst i ++ " " ++ getConst t ++ " " ++ getConst e ++ ")"+    ishow (IfThenElse _ i t e) = coerce $ "(ite " ++ coerce i ++ " " ++ coerce t ++ " " ++ coerce e ++ ")"  instance IfThenElseF :<: f => Parseable IfThenElseF f where     parser _ r = do
src/Data/Expression/Sort.hs view
@@ -1,7 +1,8 @@ {-# OPTIONS_GHC -fno-warn-unused-binds #-} -{-# LANGUAGE EmptyCase-           , DataKinds+{-# LANGUAGE DataKinds+           , EmptyCase+           , FlexibleInstances            , GADTs            , KindSignatures            , OverloadedStrings@@ -25,6 +26,7 @@  module Data.Expression.Sort ( Sort(..)                             , Sing(..)+                            , withSort                             , DynamicSort(..)                             , DynamicallySorted(..)                             , parseSort@@ -34,7 +36,6 @@  import Data.Attoparsec.Text import Data.Functor-import Data.Kind import Data.Singletons import Data.Singletons.Decide import Data.Singletons.TH@@ -51,6 +52,12 @@  genSingletons [''Sort] singDecideInstance ''Sort++-- | Turn implicit sort parameter into explicit one+withSort :: forall a (s :: Sort). Sing s -> (SingI s => a) -> a+withSort SBooleanSort     a = a+withSort SIntegralSort    a = a+withSort (SArraySort i e) a = withSort i $ withSort e $ a  show' :: Sort -> String show' BooleanSort     = "bool"
src/Data/Expression/Utils/Indexed/Eq.hs view
@@ -12,8 +12,6 @@  module Data.Expression.Utils.Indexed.Eq where -import Data.Kind- -- | Indexed types that can be equated class IEq (a :: i -> *) where     ieq :: forall j. a j -> a j -> Bool
src/Data/Expression/Utils/Indexed/Foldable.hs view
@@ -13,7 +13,6 @@ module Data.Expression.Utils.Indexed.Foldable (IFoldable(..)) where  import Data.Functor.Const-import Data.Kind  -- | Type constructors (usually functors) that can be folded class IFoldable (f :: (i -> *) -> (i -> *)) where
src/Data/Expression/Utils/Indexed/Functor.hs view
@@ -14,7 +14,6 @@ module Data.Expression.Utils.Indexed.Functor (IFix(..), IFunctor(..), icata) where  import Data.Functor.Const-import Data.Kind import Data.Singletons  import Data.Expression.Utils.Indexed.Eq
src/Data/Expression/Utils/Indexed/Sum.hs view
@@ -56,10 +56,6 @@     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
src/Data/Expression/Utils/Indexed/Traversable.hs view
@@ -14,7 +14,6 @@ module Data.Expression.Utils.Indexed.Traversable where  import Control.Monad-import Data.Kind  import Data.Expression.Utils.Indexed.Functor