diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,5 +1,9 @@ # Change Log +## 0.1.8 + +* Bump dependencies + ## 0.1.7 * Added simple utility function `toDynamicallySorted` diff --git a/expressions.cabal b/expressions.cabal --- a/expressions.cabal +++ b/expressions.cabal @@ -1,5 +1,5 @@ name: expressions -version: 0.1.7 +version: 0.1.8 synopsis: Expressions and Formulae a la carte description: This package is aimed at providing means of fixing a first-order language and @@ -72,7 +72,7 @@ UndecidableInstances build-depends: attoparsec >=0.13 && <0.14, base >=4.11 && <4.13, - containers >=0.5.7 && <0.6, + containers >=0.5.7 && <0.7, free >=4.2 && <5.1, lattices >=1.6 && <1.8, singletons >=2.2 && <2.5, diff --git a/src/Data/Expression.hs b/src/Data/Expression.hs --- a/src/Data/Expression.hs +++ b/src/Data/Expression.hs @@ -382,7 +382,7 @@ instance ConjunctionF :<: f => Parseable ConjunctionF f where parser _ r = choice [ true', and' ] "Conjunction" where - true' = string "true" *> pure (DynamicallySorted SBooleanSort $ true) + true' = string "true" *> pure (toDynamicallySorted true) and' = do _ <- char '(' *> string "and" *> space @@ -391,12 +391,12 @@ and'' as and'' as = case mapM toStaticallySorted as of - Just as' -> return . DynamicallySorted SBooleanSort $ and as' + Just as' -> return . toDynamicallySorted . and $ as' Nothing -> fail "and of non-boolean arguments" instance DisjunctionF :<: f => Parseable DisjunctionF f where parser _ r = choice [ false', or' ] "Disjunction" where - false' = string "false" *> pure (DynamicallySorted SBooleanSort $ false) + false' = string "false" *> pure (toDynamicallySorted false) or' = do _ <- char '(' *> string "or" *> space @@ -405,7 +405,7 @@ or'' os or'' os = case mapM toStaticallySorted os of - Just os' -> return . DynamicallySorted SBooleanSort $ or os' + Just os' -> return . toDynamicallySorted . or $ os' Nothing -> fail "or of non-boolean arguments" instance NegationF :<: f => Parseable NegationF f where @@ -417,7 +417,7 @@ not'' n not'' n = case toStaticallySorted n of - Just n' -> return . DynamicallySorted SBooleanSort $ not n' + Just n' -> return . toDynamicallySorted . not $ n' Nothing -> fail "not of non-boolean arguments" -- | `literals` decomposes a boolean combination (formed with conjunctions and disjunctions, preferably in negation normal form) into its constituents. @@ -566,7 +566,7 @@ forall'' [] _ = fail "quantifying zero variables" forall'' vs phi = case (mapM toStaticallySorted vs :: Maybe [Var v]) of Just vs' -> case toStaticallySorted phi of - Just phi' -> return . DynamicallySorted SBooleanSort $ forall vs' phi' + Just phi' -> return . toDynamicallySorted . forall vs' $ phi' Nothing -> fail "quantifying non-boolean expression" Nothing -> fail "ill-sorted quantifier" @@ -590,7 +590,7 @@ exists'' [] _ = fail "quantifying zero variables" exists'' vs phi = case (mapM toStaticallySorted vs :: Maybe [Var v]) of Just vs' -> case toStaticallySorted phi of - Just phi' -> return . DynamicallySorted SBooleanSort $ exists vs' phi' + Just phi' -> return . toDynamicallySorted . exists vs' $ phi' Nothing -> fail "quantifying non-boolean expression" Nothing -> fail "ill-sorted quantifier" diff --git a/src/Data/Expression/Arithmetic.hs b/src/Data/Expression/Arithmetic.hs --- a/src/Data/Expression/Arithmetic.hs +++ b/src/Data/Expression/Arithmetic.hs @@ -99,7 +99,7 @@ instance ArithmeticF :<: f => Parseable ArithmeticF f where parser _ r = choice [ cnst', add', mul', divides', lessThan' ] "Arithmetic" where - cnst' = DynamicallySorted SIntegralSort . cnst <$> signed decimal + cnst' = toDynamicallySorted . cnst <$> signed decimal add' = do _ <- char '(' *> char '+' *> space @@ -130,19 +130,19 @@ lessThan'' a b add'' as = case mapM toStaticallySorted as of - Just as' -> return . DynamicallySorted SIntegralSort $ add as' + Just as' -> return . toDynamicallySorted . add $ as' Nothing -> fail "add of non-integral arguments" mul'' ms = case mapM toStaticallySorted ms of - Just ms' -> return . DynamicallySorted SIntegralSort $ mul ms' + Just ms' -> return . toDynamicallySorted . mul $ ms' Nothing -> fail "mul of non-integral arguments" divides'' c a = case toStaticallySorted a of - Just a' -> return . DynamicallySorted SBooleanSort $ c .\. a' + Just a' -> return . toDynamicallySorted $ c .\. a' _ -> fail "divisibility of non-integral argument" lessThan'' a b = case mapM toStaticallySorted [a, b] of - Just [a', b'] -> return . DynamicallySorted SBooleanSort $ a' .<. b' + Just [a', b'] -> return . toDynamicallySorted $ a' .<. b' _ -> fail "less-than of non-integral arguments" -- | A smart constructor for integer constants diff --git a/src/Data/Expression/Equality.hs b/src/Data/Expression/Equality.hs --- a/src/Data/Expression/Equality.hs +++ b/src/Data/Expression/Equality.hs @@ -67,7 +67,7 @@ equals :: DynamicallySorted f -> DynamicallySorted f -> Parser (DynamicallySorted f) equals (DynamicallySorted s1 a) (DynamicallySorted s2 b) = case s1 %~ s2 of - Proved Refl -> return . DynamicallySorted SBooleanSort $ inject (Equals s1 a b) + Proved Refl -> return . toDynamicallySorted . inject $ Equals s1 a b Disproved _ -> fail "multi-sorted equality" -- | A smart constructor for an equality predicate diff --git a/src/Data/Expression/Sort.hs b/src/Data/Expression/Sort.hs --- a/src/Data/Expression/Sort.hs +++ b/src/Data/Expression/Sort.hs @@ -98,7 +98,7 @@ Proved Refl -> Just x Disproved _ -> Nothing --- | Converts statically sorted expression to a dynamically sorted one. +-- | Converts a statically sorted expression to a dynamically sorted one. toDynamicallySorted :: forall f (s :: Sort). SingI s => IFix f s -> DynamicallySorted f toDynamicallySorted = DynamicallySorted (sing :: Sing s)