expressions 0.1.2 → 0.1.3

raw patch · 4 files changed

+105/−18 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• ChangeLog.md +7/−16
• expressions.cabal +2/−1
• src/Data/Expression.hs +3/−1
• src/Data/Expression/IfThenElse.hs +93/−0

@@ -1,34 +1,25 @@ # Change Log -## 0.1.1 -- 2017-09-06+## 0.1.3 +* Extracting variables occurring in expression * Distinguish quantifier-free expressions * Convert to negation normal form * Convert to prenex form * Convert to flat form (select and store have only variables or constants as arguments) * Replace store with an instance of its axiomatization -## 0.1.0.5  -- 2017-08-29--* Extracting variables occurring in expression--## 0.1.0.4  -- 2017-08-25+## 0.1.2  * Foldable with sort index * Traversable with sort index -## 0.1.0.3  -- 2017-07-11--* Expression substitution--## 0.1.0.2  -- 2017-05-26--* Equality of expressions--## 0.1.0.1  -- 2017-05-24+## 0.1.1  * Parsing+* Equality of expressions+* Expression substitution -## 0.1.0.0  -- 2017-05-23+## 0.1.0  * Sorted Expressions à la Carte

@@ -1,5 +1,5 @@ name:                expressions-version:             0.1.2+version:             0.1.3 synopsis:            Expressions and Formulae a la carte description:   This package is aimed at providing means of fixing a first-order language and@@ -46,6 +46,7 @@                        Data.Expression.Arithmetic,                        Data.Expression.Array,                        Data.Expression.Equality,+                       Data.Expression.IfThenElse,                        Data.Expression.Parser,                        Data.Expression.Sort,                        Data.Expression.Utils.Indexed.Eq,

@@ -30,6 +30,7 @@ module Data.Expression ( module Data.Expression.Arithmetic                        , module Data.Expression.Array                        , module Data.Expression.Equality+                       , module Data.Expression.IfThenElse                        , module Data.Expression.Parser                        , module Data.Expression.Sort                        , module Data.Expression.Utils.Indexed.Eq@@ -135,6 +136,7 @@ import Data.Expression.Arithmetic import Data.Expression.Array import Data.Expression.Equality+import Data.Expression.IfThenElse import Data.Expression.Parser import Data.Expression.Sort hiding (index) import Data.Expression.Utils.Indexed.Eq@@ -151,7 +153,7 @@ type QFLogicF = EqualityF :+: ConjunctionF :+: DisjunctionF :+: NegationF :+: VarF  -- | A functor representing the language of quantifier-free linear integer arithmetic theory in first order logic (integer constants, integer variables, addition, multiplication, divisibility, ordering)-type QFLiaF = ArithmeticF :+: QFLogicF+type QFLiaF = ArithmeticF :+: IfThenElseF :+: QFLogicF  -- | A functor much like `QFLiaF` with quantifiers over booleans and integers type LiaF = ExistentialF 'BooleanSort :+: ExistentialF 'IntegralSort :+: UniversalF 'BooleanSort :+: UniversalF 'IntegralSort :+: QFLiaF

@@ -0,0 +1,93 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}++{-# LANGUAGE FlexibleContexts+           , FlexibleInstances+           , GADTs+           , MultiParamTypeClasses+           , OverloadedStrings+           , RankNTypes+           , ScopedTypeVariables+           , TypeInType+           , TypeOperators #-}++--------------------------------------------------------------------------------+-- |+-- Module     :  Data.Expression.IfThenElse+-- 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.IfThenElse ( IfThenElseF(..)+                                  , ite ) where++import Data.Monoid+import Data.Singletons+import Data.Singletons.Decide++import Data.Expression.Arithmetic+import Data.Expression.Parser+import Data.Expression.Sort+import Data.Expression.Utils.Indexed.Eq+import Data.Expression.Utils.Indexed.Foldable+import Data.Expression.Utils.Indexed.Functor+import Data.Expression.Utils.Indexed.Show+import Data.Expression.Utils.Indexed.Sum+import Data.Expression.Utils.Indexed.Traversable++import qualified Data.Functor.Const as F++-- | A functor representing a conditional value (if-then-else)+data IfThenElseF a (s :: Sort) where+    IfThenElse :: Sing s -> a 'BooleanSort -> a s -> a s -> IfThenElseF a s++instance IEq1 IfThenElseF where+    IfThenElse sa ia ta ea `ieq1` IfThenElse sb ib tb eb = ia `ieq` ib && case sa %~ sb of+        Proved Refl -> ta `ieq` tb && ea `ieq` eb+        Disproved _ -> False++instance IFunctor IfThenElseF where+    imap f (IfThenElse s i t e) = IfThenElse s (f i) (f t) (f e)+    index (IfThenElse s _ _ _) = s++instance IFoldable IfThenElseF where+    ifold (IfThenElse _ i t e) = F.Const $ F.getConst i <> F.getConst t <> F.getConst e++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) = F.Const $ "(ite " ++ F.getConst i ++ " " ++ F.getConst t ++ " " ++ F.getConst e ++ ")"++instance IfThenElseF :<: f => Parseable IfThenElseF f where+    parser _ r = do+        _ <- char '(' *> string "ite" *> space+        i <- r+        _ <- space+        t <- r+        _ <- space+        e <- r+        _ <- char ')'+        ifThenElse i t e <?> "IfThenElse" where++        ifThenElse :: DynamicallySorted f -> DynamicallySorted f -> DynamicallySorted f -> Parser (DynamicallySorted f)+        ifThenElse (DynamicallySorted s1 i)+                   (DynamicallySorted s2 t)+                   (DynamicallySorted s3 e) = case s1 %~ SBooleanSort of+            Proved Refl -> case s2 %~ s3 of+                Proved Refl -> return . DynamicallySorted s2 $ inject (IfThenElse s2 i t e)+                Disproved _ -> fail "inconsistent sorts of then and else branches"+            Disproved _ -> fail "branching on non-boolean expression"++-- | A smart constructor for an if-then-else expression+ite :: forall f s. ( IfThenElseF :<: f, SingI s ) => IFix f 'BooleanSort -> IFix f s -> IFix f s -> IFix f s+ite i t e = inject (IfThenElse (sing :: Sing s) i t e)++instance ( ArithmeticF :<: f, IfThenElseF :<: f ) => Num (IFix f 'IntegralSort) where+    (+) = (.+.)+    (*) = (.*.)+    abs a = ite (a .<. 0) (negate a) a+    signum a = ite (a .<. 0) (-1) (ite (a .>. 0) 1 0)+    fromInteger = cnst . fromIntegral+    negate = (* cnst (-1))