packages feed

expressions 0.3.1 → 0.4

raw patch · 9 files changed

+128/−30 lines, 9 files

Files

ChangeLog.md view
@@ -1,5 +1,10 @@ # Change Log +## 0.4++* Allow a wide range of dynamically sorted values (not just expressions)+* Utility for extracting array accesses+ ## 0.3.1  * Utility for extracting constants from expressions
expressions.cabal view
@@ -1,5 +1,5 @@ name:                expressions-version:             0.3.1+version:             0.4 synopsis:            Expressions and Formulae a la carte description:   This package is aimed at providing means of fixing a first-order language and@@ -53,8 +53,9 @@                        Data.Expression.Utils.Indexed.Foldable,                        Data.Expression.Utils.Indexed.Functor,                        Data.Expression.Utils.Indexed.Show,-                       Data.Expression.Utils.Indexed.Sum-                       Data.Expression.Utils.Indexed.Traversable+                       Data.Expression.Utils.Indexed.Sum,+                       Data.Expression.Utils.Indexed.Traversable,+                       Data.Expression.Utils.Indexed.Tuple   other-extensions:    DataKinds,                        FlexibleContexts,                        FlexibleInstances,
src/Data/Expression.hs view
@@ -283,7 +283,7 @@              var''' n s -        var''' :: VariableName -> DynamicSort -> Parser (DynamicallySorted f)+        var''' :: VariableName -> DynamicSort -> Parser (DynamicallySortedFix f)         var''' n (DynamicSort (s :: Sing s)) = return $ dynvar n s  -- | A smart constructor for variables of any sort in any language@@ -295,12 +295,12 @@ 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+-- | Like @var@ except it hides the sort inside @DynamicallySortedFix@+dynvar :: forall f (s :: Sort). VarF :<: f => VariableName -> Sing s -> DynamicallySortedFix 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 :: ( VarF :<: f, IFoldable f, IFunctor f ) => IFix f s -> [DynamicallySorted Var] vars = nub . F.getConst . icata vars' where     vars' a = case prj a of         Just (Var n s) -> F.Const [dynvar n s]@@ -564,7 +564,7 @@  instance ( UniversalF v :<: f, SingI v ) => Parseable (UniversalF v) f where     parser _ r = forall' <?> "Universal" where-        var' :: Parser (DynamicallySorted VarF)+        var' :: Parser (DynamicallySorted Var)         var' = parser (Proxy :: Proxy VarF) var'          forall' = do@@ -588,7 +588,7 @@  instance ( ExistentialF v :<: f, SingI v ) => Parseable (ExistentialF v) f where     parser _ r = exists' <?> "Existential" where-        var' :: Parser (DynamicallySorted VarF)+        var' :: Parser (DynamicallySorted Var)         var' = parser (Proxy :: Proxy VarF) var'          exists' = do@@ -612,11 +612,11 @@  class MaybeQuantified f where     isQuantified' :: MaybeQuantified g => f (IFix g) s -> F.Const Any s-    freevars' :: f (F.Const [DynamicallySorted VarF]) s -> F.Const [DynamicallySorted VarF] s+    freevars' :: f (F.Const [DynamicallySorted Var]) s -> F.Const [DynamicallySorted Var] s  instance MaybeQuantified VarF where     isQuantified' _ = coerce False-    freevars' (Var n s) = coerce [dynvar n s]+    freevars' (Var n s) = coerce [dynvar n s :: DynamicallySorted Var]  instance MaybeQuantified (UniversalF v) where     isQuantified' _ = coerce True@@ -645,7 +645,7 @@ isQuantifierFree = P.not . isQuantified  -- | Collects a list of all free variables occurring in an expression.-freevars :: ( IFunctor f, MaybeQuantified f ) => IFix f s -> [DynamicallySorted VarF]+freevars :: ( IFunctor f, MaybeQuantified f ) => IFix f s -> [DynamicallySorted Var] freevars = nub . coerce . icata freevars'  -- | A smart constructor for universally quantified formulae@@ -753,7 +753,7 @@ prenex f = let (a, (_, q)) = runState (imapM (pushQuantifier . unIFix) (nnf f)) (freenames f, id) in q a  class Bind f g where-    bind :: Proxy f -> IFix g s -> Maybe (Bool, State (VariableNamePool, [([DynamicallySorted VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s))+    bind :: Proxy f -> IFix g s -> Maybe (Bool, State (VariableNamePool, [([DynamicallySorted Var], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s))  instance forall g v. ( VarF :<: g, EqualityF :<: g, NegationF :<: g, DisjunctionF :<: g, UniversalF v :<: g, MaybeQuantified g, SingI v ) => Bind (UniversalF v) g where     bind _ a = case index (unIFix a) %~ (sing :: Sing v) of@@ -799,7 +799,7 @@     bind _ _ = Nothing  class Bind' f g where-    bind' :: Bind g g => f (IFix g) s -> Maybe (Bool, State (VariableNamePool, [([DynamicallySorted VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s))+    bind' :: Bind g g => f (IFix g) s -> Maybe (Bool, State (VariableNamePool, [([DynamicallySorted Var], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s))  instance VarF :<: g => Bind' VarF g where     bind' v = Just (True, return . inject $ v)@@ -823,11 +823,11 @@ instance {-# OVERLAPPABLE #-} f :<: g => Bind' f g where     bind' a = bind (Proxy :: Proxy g) (inject a) -bind'' :: forall f (s :: Sort). ( Bind f f, Bind' f f ) => IFix f s -> State (VariableNamePool, [([DynamicallySorted VarF], IFix f 'BooleanSort -> IFix f 'BooleanSort)]) (IFix f s)+bind'' :: forall f (s :: Sort). ( Bind f f, Bind' f f ) => IFix f s -> State (VariableNamePool, [([DynamicallySorted Var], IFix f 'BooleanSort -> IFix f 'BooleanSort)]) (IFix f s) bind'' a = fromMaybe (return a) . fmap snd . bind' . unIFix $ a  class MaybeQuantified'' f g where-    flatten' :: ( Bind g g, Bind' g g ) => f (IFix g) s -> State (VariableNamePool, [([DynamicallySorted VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s)+    flatten' :: ( Bind g g, Bind' g g ) => f (IFix g) s -> State (VariableNamePool, [([DynamicallySorted Var], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s)  instance ArrayF :<: g => MaybeQuantified'' ArrayF g where     flatten' (Select is es a i) = do
src/Data/Expression/Array.hs view
@@ -19,8 +19,10 @@  module Data.Expression.Array ( ArrayF(..)                              , select-                             , store ) where+                             , store+                             , accesses ) where +import Control.Monad.Trans.Writer import Data.Coerce import Data.Functor.Const import Data.Singletons@@ -34,6 +36,7 @@ import Data.Expression.Utils.Indexed.Show import Data.Expression.Utils.Indexed.Sum import Data.Expression.Utils.Indexed.Traversable+import Data.Expression.Utils.Indexed.Tuple  -- | A functor representing array-theoretic terms (`select` and `store` also known as "read" and "write") data ArrayF a (s :: Sort) where@@ -85,14 +88,14 @@             _ <- char ')'             store'' a i v -        select'' :: DynamicallySorted f -> DynamicallySorted f -> Parser (DynamicallySorted f)+        select'' :: DynamicallySortedFix f -> DynamicallySortedFix f -> Parser (DynamicallySortedFix f)         select'' (DynamicallySorted (SArraySort is1 es) a)                  (DynamicallySorted is2                 i) = case is1 %~ is2 of             Proved Refl -> return . DynamicallySorted es $ inject (Select is1 es a i)             Disproved _ -> fail "ill-sorted select"         select'' _ _ = fail "selecting from non-array" -        store'' :: DynamicallySorted f -> DynamicallySorted f -> DynamicallySorted f -> Parser (DynamicallySorted f)+        store'' :: DynamicallySortedFix f -> DynamicallySortedFix f -> DynamicallySortedFix f -> Parser (DynamicallySortedFix f)         store''  (DynamicallySorted as@(SArraySort _ _) a)                  (DynamicallySorted is                  i)                  (DynamicallySorted es                  v) = case as %~ SArraySort is es of@@ -107,3 +110,25 @@ -- | A smart constructor for store store :: ( ArrayF :<: f, SingI i, SingI e ) => IFix f ('ArraySort i e) -> IFix f i -> IFix f e -> IFix f ('ArraySort i e) store a i v = inject (Store sing sing a i v)++newtype Array1 f (i :: Sort) (e :: Sort) = Array1 (IFix f ('ArraySort i e))+newtype Array2 f (i :: Sort)             = Array2 (DynamicallySorted (Array1 f i))++type ArrayAccess f = DynamicallySorted (IT2 (Array2 f) (IFix f))++instance ( IFunctor f, IShow f ) => Show (Array1 f i e) where+  show (Array1 f) = show f++instance ( IFunctor f, IShow f ) => Show (Array2 f i) where+  show (Array2 f) = show f++-- | Collects pairs of arrays and indices that appear together in some @select@ and/or @store@ within an expression+accesses :: forall f (s :: Sort). ( ArrayF :<: f, ITraversable f ) => IFix f s -> [ArrayAccess f]+accesses = execWriter . imapM accesses' where+  accesses' :: forall (s' :: Sort). IFix f s' -> Writer [ArrayAccess f] (IFix f s')+  accesses' e = do+    case match e of+      Just (Select is es a i)   -> tell [ DynamicallySorted is (IT2 (Array2 (DynamicallySorted es (Array1 a)), i)) ]+      Just (Store  is es a i _) -> tell [ DynamicallySorted is (IT2 (Array2 (DynamicallySorted es (Array1 a)), i)) ]+      _                         -> return ()+    return e
src/Data/Expression/Equality.hs view
@@ -65,7 +65,7 @@         _ <- char ')'         equals a b <?> "Equality" where -        equals :: DynamicallySorted f -> DynamicallySorted f -> Parser (DynamicallySorted f)+        equals :: DynamicallySortedFix f -> DynamicallySortedFix f -> Parser (DynamicallySortedFix f)         equals (DynamicallySorted s1 a)                (DynamicallySorted s2 b) = case s1 %~ s2 of             Proved Refl -> return . toDynamicallySorted . inject $ Equals s1 a b
src/Data/Expression/IfThenElse.hs view
@@ -69,7 +69,7 @@         _ <- char ')'         ifThenElse i t e <?> "IfThenElse" where -        ifThenElse :: DynamicallySorted f -> DynamicallySorted f -> DynamicallySorted f -> Parser (DynamicallySorted f)+        ifThenElse :: DynamicallySortedFix f -> DynamicallySortedFix f -> DynamicallySortedFix f -> Parser (DynamicallySortedFix f)         ifThenElse (DynamicallySorted s1 i)                    (DynamicallySorted s2 t)                    (DynamicallySorted s3 e) = case s1 %~ SBooleanSort of
src/Data/Expression/Parser.hs view
@@ -63,7 +63,7 @@  -- | Expressions that can be parsed class Parseable f g where-    parser :: Proxy f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)+    parser :: Proxy f -> Parser (DynamicallySortedFix g) -> Parser (DynamicallySortedFix g)  -- | Tries to parse the entire input text and produce an expression in desired language and with desired sort. parse :: forall f (s :: Sort). ( Parseable f f, SingI s ) => Text -> Maybe (IFix f s)
src/Data/Expression/Sort.hs view
@@ -6,6 +6,7 @@            , GADTs            , KindSignatures            , OverloadedStrings+           , QuantifiedConstraints            , RankNTypes            , ScopedTypeVariables            , TemplateHaskell@@ -29,6 +30,7 @@                             , withSort                             , DynamicSort(..)                             , DynamicallySorted(..)+                            , DynamicallySortedFix                             , parseSort                             , toDynamicallySorted                             , toStaticSort@@ -40,9 +42,7 @@ import Data.Singletons.Decide import Data.Singletons.TH -import Data.Expression.Utils.Indexed.Eq import Data.Expression.Utils.Indexed.Functor-import Data.Expression.Utils.Indexed.Show  -- | A universe of recognized sorts data Sort = BooleanSort                                  -- ^ booleans (true, false)@@ -86,16 +86,19 @@         Proved Refl -> True         Disproved _ -> False +-- | A value of some sort+data DynamicallySorted (d :: Sort -> *) where+  DynamicallySorted :: forall (s :: Sort) d. Sing s -> d s -> DynamicallySorted d+ -- | An expression of some sort (obtained for example during parsing)-data DynamicallySorted (f :: (Sort -> *) -> (Sort -> *)) where-  DynamicallySorted :: forall (s :: Sort) f. Sing s -> IFix f s -> DynamicallySorted f+type DynamicallySortedFix f = DynamicallySorted (IFix f) -instance IEq1 f => Eq (DynamicallySorted f) where+instance (forall (s :: Sort). Eq (d s)) => Eq (DynamicallySorted d) where     DynamicallySorted sa a == DynamicallySorted sb b = case sa %~ sb of         Proved Refl -> a == b         Disproved _ -> False -instance (IFunctor f, IShow f) => Show (DynamicallySorted f) where+instance (forall (s :: Sort). Show (d s)) => Show (DynamicallySorted d) where     show (DynamicallySorted _ a) = show a  -- | Tries to convert some sort (`DynamicSort`) to a requested sort.@@ -106,12 +109,12 @@         Disproved _ -> Nothing  -- | Converts a statically sorted expression to a dynamically sorted one.-toDynamicallySorted :: forall f (s :: Sort). SingI s => IFix f s -> DynamicallySorted f+toDynamicallySorted :: forall d (s :: Sort). SingI s => d s -> DynamicallySorted d toDynamicallySorted = DynamicallySorted (sing :: Sing s)  -- | Tries to convert an expression (`DynamicallySorted`) of some sort to an expression of requested sort. -- Performs no conversions.-toStaticallySorted :: forall f (s :: Sort). SingI s => DynamicallySorted f -> Maybe (IFix f s)+toStaticallySorted :: forall d (s :: Sort). SingI s => DynamicallySorted d -> Maybe (d s) toStaticallySorted dx = case dx of     DynamicallySorted s x -> case s %~ (sing :: Sing s) of         Proved Refl -> Just x
+ src/Data/Expression/Utils/Indexed/Tuple.hs view
@@ -0,0 +1,64 @@+{-# LANGUAGE TypeInType #-}++--------------------------------------------------------------------------------+-- |+-- Module     :  Data.Expression.Array+-- Copyright  :  (C) 2017-18 Jakub Daniel+-- License    :  BSD-style (see the file LICENSE)+-- Maintainer :  Jakub Daniel <jakub.daniel@protonmail.com>+-- Stability  :  experimental+--------------------------------------------------------------------------------++module Data.Expression.Utils.Indexed.Tuple where++newtype IT2 (a :: k -> *)+            (b :: k -> *)+            (i :: k) = IT2 { getIT2 :: (a i, b i) }++newtype IT3 (a :: k -> *)+            (b :: k -> *)+            (c :: k -> *)+            (i :: k) = IT3 { getIT3 :: (a i, b i, c i) }++newtype IT4 (a :: k -> *)+            (b :: k -> *)+            (c :: k -> *)+            (d :: k -> *)+            (i :: k) = IT4 { getIT4 :: (a i, b i, c i, d i) }++newtype IT5 (a :: k -> *)+            (b :: k -> *)+            (c :: k -> *)+            (d :: k -> *)+            (e :: k -> *)+            (i :: k) = IT5 { getIT5 :: (a i, b i, c i, d i, e i) }++newtype IT6 (a :: k -> *)+            (b :: k -> *)+            (c :: k -> *)+            (d :: k -> *)+            (e :: k -> *)+            (f :: k -> *)+            (i :: k) = IT6 { getIT6 :: (a i, b i, c i, d i, e i, f i) }++newtype IT7 (a :: k -> *)+            (b :: k -> *)+            (c :: k -> *)+            (d :: k -> *)+            (e :: k -> *)+            (f :: k -> *)+            (g :: k -> *)+            (i :: k) = IT7 { getIT7 :: (a i, b i, c i, d i, e i, f i, g i) }++newtype IT8 (a :: k -> *)+            (b :: k -> *)+            (c :: k -> *)+            (d :: k -> *)+            (e :: k -> *)+            (f :: k -> *)+            (g :: k -> *)+            (h :: k -> *)+            (i :: k) = IT8 { getIT8 :: (a i, b i, c i, d i, e i, f i, g i, h i) }++instance ( Show (a i), Show (b i) ) => Show (IT2 a b i) where+  show (IT2 (a, b)) = "(" ++ show a ++ ", " ++ show b ++ ")"