diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -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 diff --git a/expressions.cabal b/expressions.cabal --- a/expressions.cabal +++ b/expressions.cabal @@ -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, diff --git a/src/Data/Expression.hs b/src/Data/Expression.hs --- a/src/Data/Expression.hs +++ b/src/Data/Expression.hs @@ -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 diff --git a/src/Data/Expression/IfThenElse.hs b/src/Data/Expression/IfThenElse.hs new file mode 100644 --- /dev/null +++ b/src/Data/Expression/IfThenElse.hs @@ -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 +-- 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))