expressions 0.1.7 → 0.1.8
raw patch · 6 files changed
+20/−16 lines, 6 filesdep ~containers
Dependency ranges changed: containers
Files
- ChangeLog.md +4/−0
- expressions.cabal +2/−2
- src/Data/Expression.hs +7/−7
- src/Data/Expression/Arithmetic.hs +5/−5
- src/Data/Expression/Equality.hs +1/−1
- src/Data/Expression/Sort.hs +1/−1
ChangeLog.md view
@@ -1,5 +1,9 @@ # Change Log +## 0.1.8++* Bump dependencies+ ## 0.1.7 * Added simple utility function `toDynamicallySorted`
expressions.cabal view
@@ -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,
src/Data/Expression.hs view
@@ -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"
src/Data/Expression/Arithmetic.hs view
@@ -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
src/Data/Expression/Equality.hs view
@@ -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
src/Data/Expression/Sort.hs view
@@ -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)