packages feed

expressions 0.1.5 → 0.1.6

raw patch · 8 files changed

+66/−37 lines, 8 filesdep +freedep ~base

Dependencies added: free

Dependency ranges changed: base

Files

ChangeLog.md view
@@ -1,5 +1,9 @@ # Change Log +## 0.1.6++* GHC 8.4 compatibility+ ## 0.1.5  * Bump dependencies, fix equality, tweak readme
expressions.cabal view
@@ -1,5 +1,5 @@ name:                expressions-version:             0.1.5+version:             0.1.6 synopsis:            Expressions and Formulae a la carte description:   This package is aimed at providing means of fixing a first-order language and@@ -71,15 +71,16 @@                        TypeSynonymInstances,                        UndecidableInstances   build-depends:       attoparsec >=0.13 && <0.14,-                       base >=4.9 && <4.12,+                       base >=4.11 && <4.13,                        containers >=0.5.7 && <0.6,+                       free >=4.2 && <5.1,                        lattices >=1.6 && <1.8,                        singletons >=2.2 && <2.5,                        text >=1.2 && <1.3,                        transformers >=0.5.2 && <0.6   hs-source-dirs:      src   default-language:    Haskell2010-  ghc-options:         -Wall+  ghc-options:         -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns  test-suite test   type:                exitcode-stdio-1.0@@ -90,4 +91,4 @@   hs-source-dirs:      test   main-is:             Main.hs   default-language:    Haskell2010-  ghc-options:         -Wall+  ghc-options:         -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns
src/Data/Expression.hs view
@@ -121,14 +121,17 @@  import Algebra.Lattice import Control.Applicative hiding (Const)+import Control.Comonad.Trans.Coiter import Control.Monad import Control.Monad.Trans.Class import Control.Monad.Trans.Reader import Control.Monad.Trans.State+import Data.Functor.Identity import Data.List hiding (and, or, union)-import Data.Map hiding (map, drop, foldr, mapMaybe, partition)+import Data.Map hiding (map, drop, foldl, foldr, mapMaybe, partition) import Data.Maybe-import Data.Monoid+import Data.Monoid hiding ((<>))+import Data.Semigroup hiding (First, getFirst) import Data.Singletons import Data.Singletons.Decide import Prelude hiding (and, or, not)@@ -308,9 +311,12 @@     Just b -> b     Nothing -> IFix . imap (flip substitute s) . unIFix $ a +instance Semigroup (Substitution f) where+    (Substitution f) <> (Substitution g) = Substitution $ \a -> getFirst (mconcat ([First . f, First . g] <*> [a]))+ instance Monoid (Substitution f) where     mempty  = Substitution (const Nothing)-    (Substitution f) `mappend` (Substitution g) = Substitution $ \a -> getFirst (mconcat ([First . f, First . g] <*> [a]))+    mappend = (<>)  -- | A functor representing a logical connective for conjunction data ConjunctionF a (s :: Sort) where@@ -691,24 +697,28 @@      pool = [ [x] | x <- ['a'..'z'] ] ++ [ x ++ [y] | x <- pool, y <- ['a'..'z'] ] -freenames :: forall f (s :: Sort). ( VarF :<: f, IFunctor f, IFoldable f ) => IFix f s -> [String]-freenames a = map (\n -> freename a ++ show n) ([0..] :: [Int])+type VariableNamePool = Coiter String -pushQuantifier' :: ( VarF :<: f, IEq1 f ) => ([Var v] -> IFix f 'BooleanSort -> IFix f 'BooleanSort) -> [Var v] -> IFix f 'BooleanSort -> State ([String], IFix f 'BooleanSort -> IFix f 'BooleanSort) (IFix f 'BooleanSort)+rename :: VariableNamePool -> [Var v] -> ([Var v], VariableNamePool)+rename pool = foldl (\(vs, ns) (IFix (Var _ s)) -> let (n', ns') = runCoiter ns in (IFix (Var n' s) : vs, ns')) ([], pool)++freenames :: forall f (s :: Sort). ( VarF :<: f, IFunctor f, IFoldable f ) => IFix f s -> VariableNamePool+freenames a = fmap (\n -> freename a ++ show n) $ unfold (succ . runIdentity) (Identity (0 :: Int))++pushQuantifier' :: ( VarF :<: f, IEq1 f ) => ([Var v] -> IFix f 'BooleanSort -> IFix f 'BooleanSort) -> [Var v] -> IFix f 'BooleanSort -> State (VariableNamePool, IFix f 'BooleanSort -> IFix f 'BooleanSort) (IFix f 'BooleanSort) pushQuantifier' c vs a = do     (ns, q) <- get -    let vs' = zipWith (\(IFix (Var _ s)) n' -> IFix (Var n' s)) vs ns-        ns' = drop (length vs) ns-        q'  = c vs' . q-        sub = mconcat $ zipWith (\(IFix (Var n s)) n' -> inject (Var n' s) `for` inject (Var n s)) vs ns+    let (vs', ns') = rename ns vs+        q'         = c vs' . q+        sub        = mconcat $ zipWith (\(IFix (Var n s)) (IFix (Var n' _)) -> inject (Var n' s) `for` inject (Var n s)) vs vs'      put (ns', q')      return $ a `substitute` sub  class MaybeQuantified f => MaybeQuantified' f g where-    pushQuantifier :: f (IFix g) s -> State ([String], IFix g 'BooleanSort -> IFix g 'BooleanSort) (IFix g s)+    pushQuantifier :: f (IFix g) s -> State (VariableNamePool, IFix g 'BooleanSort -> IFix g 'BooleanSort) (IFix g s)  instance ( VarF :<: g, UniversalF v :<: g, IEq1 g ) => MaybeQuantified' (UniversalF v) g where     pushQuantifier (Forall vs a) = pushQuantifier' forall vs a@@ -731,29 +741,33 @@ 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 ([String], [([DynamicallySorted VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s))+    bind :: Proxy f -> IFix g s -> Maybe (Bool, State (VariableNamePool, [([DynamicallySorted VarF], 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         Proved Refl -> Just . (\s -> (False, s)) $ do-            (n : ns, q) <- get+            (ns, q) <- get              let x :: forall f. VarF :<: f => IFix f v                 x = var n -            put (ns, (freevars a, forall [x] . (x .=. a .->.)) : q)+                (n, ns') = runCoiter ns++            put (ns', (freevars a, forall [x] . (x .=. a .->.)) : q)             return x         Disproved _ -> Nothing  instance forall g v. ( VarF :<: g, EqualityF :<: g, ConjunctionF :<: g, ExistentialF v :<: g, MaybeQuantified g, SingI v ) => Bind (ExistentialF v) g where     bind _ a = case index (unIFix a) %~ (sing :: Sing v) of         Proved Refl -> Just . (\s -> (True, s)) $ do-            (n : ns, q) <- get+            (ns, q) <- get              let x :: forall f. VarF :<: f => IFix f v                 x = var n -            put (ns, (freevars a, exists [x] . (x .=. a .&.)) : q)+                (n, ns') = runCoiter ns++            put (ns', (freevars a, exists [x] . (x .=. a .&.)) : q)             return x         Disproved _ -> Nothing @@ -773,7 +787,7 @@     bind _ _ = Nothing  class Bind' f g where-    bind' :: Bind g g => f (IFix g) s -> Maybe (Bool, State ([String], [([DynamicallySorted VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s))+    bind' :: Bind g g => f (IFix g) s -> Maybe (Bool, State (VariableNamePool, [([DynamicallySorted VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s))  instance VarF :<: g => Bind' VarF g where     bind' v = Just (True, return . inject $ v)@@ -797,11 +811,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 ([String], [([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 VarF], 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 ([String], [([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 VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s)  instance ArrayF :<: g => MaybeQuantified'' ArrayF g where     flatten' (Select is es a i) = do@@ -870,18 +884,20 @@     quantify _ _ = Nothing  class Axiomatized f g where-    instantiate :: Forall g g => IFix g s -> f (IFix g) s -> Maybe (State [String] (IFix g 'BooleanSort))+    instantiate :: Forall g g => IFix g s -> f (IFix g) s -> Maybe (State VariableNamePool (IFix g 'BooleanSort))  instance ( VarF :<: g, ConjunctionF :<: g, DisjunctionF :<: g, NegationF :<: g, EqualityF :<: g, ArrayF :<: g ) => Axiomatized ArrayF g where     instantiate a' (Store (is :: Sing is) es a i e) = case quantify (Proxy :: Proxy g) is of         Just q -> Just $ do-            (n : ns) <- get+            ns <- get              let j :: forall f. VarF :<: f => IFix f is                 j = inject $ Var n is -            put ns+                (n, ns') = runCoiter ns +            put ns'+             return $ inject (Equals es (inject (Select is es a' i)) e) .&. q [j] (not (inject (Equals is i j)) .->. inject (Equals es (inject (Select is es a' j)) (inject (Select is es a j))))         Nothing -> Nothing     instantiate _ _ = Nothing@@ -899,5 +915,5 @@ -- | Replaces `store` with an instance of its axiomatization. unstore :: forall f. Unstore f => IFix f 'BooleanSort -> IFix f 'BooleanSort unstore a = let a' = flatten a in evalState (imapM unstore' a') (freenames a') where-    unstore' :: IFix f s -> State [String] (IFix f s)+    unstore' :: IFix f s -> State VariableNamePool (IFix f s)     unstore' a' = fromMaybe (return a') (match a' >>= \(Equals _ l r) -> instantiate l (unIFix r) <|> instantiate r (unIFix l))
src/Data/Expression/Array.hs view
@@ -22,7 +22,6 @@                              , store ) where  import Data.Functor.Const-import Data.Monoid import Data.Singletons import Data.Singletons.Decide
src/Data/Expression/Equality.hs view
@@ -21,7 +21,6 @@                                 , (.=.) ) where  import Data.Functor.Const-import Data.Monoid import Data.Singletons import Data.Singletons.Decide
src/Data/Expression/IfThenElse.hs view
@@ -21,7 +21,6 @@                                   , ite ) where  import Data.Functor.Const-import Data.Monoid import Data.Singletons import Data.Singletons.Decide
src/Data/Expression/Sort.hs view
@@ -1,7 +1,8 @@ {-# OPTIONS_GHC -fno-warn-unused-binds #-} -{-# LANGUAGE GADTs+{-# LANGUAGE EmptyCase            , DataKinds+           , GADTs            , KindSignatures            , OverloadedStrings            , RankNTypes
test/Main.hs view
@@ -32,16 +32,26 @@ main :: IO () main = guard (P.and props) where -    props = [ e1 == (parseJust "(a : int)"                                                                   :: ALia 'IntegralSort)-            , e2 /= (parseJust "(+ (a : int) 3)"                                                             :: ALia 'IntegralSort)-            , e3 == (parseJust "(+ (a : int) 1)"                                                             :: ALia 'IntegralSort)-            , e4 == (parseJust "(select (a : array int (array int bool)) (+ (b : int) 3))"                   :: QFALia ('ArraySort 'IntegralSort 'BooleanSort))-            , e5 == (parseJust "(forall ((x : int)) (exists ((y : int)) (and true (= (b : bool) (< x y)))))" :: Lia 'BooleanSort)-            , e6 == (parseJust "(and (forall ((x : int) (y : int)) (< x (+ y (z : int)))) (= z 3))"          :: Lia 'BooleanSort) ]+    props = [ e1 == parseJust "(a : int)"+            , e2 /= parseJust "(+ (a : int) 3)"+            , e3 == parseJust "(+ (a : int) 1)"+            , 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 ] +    e1, e2, e3 :: ALia 'IntegralSort     e1 = a     e2 = a     e3 = a .+. c1++    e4 :: QFALia ('ArraySort 'IntegralSort 'BooleanSort)     e4 = select a (b .+. c3)++    e5, e6 :: Lia 'BooleanSort     e5 = forall [x :: Var 'IntegralSort] (exists [y :: Var 'IntegralSort] (and [true, b .=. (x .<. y)]))     e6 = forall [x :: Var 'IntegralSort, y] (x .<. y .+. z) .&. z .=. c3++    e7, e8 :: Lia 'IntegralSort+    e7 = a .*. (a .+. c3) `substitute` (c3 `for` (a .+. c3))+    e8 = inject (Mul [a, c3])