expressions (empty) → 0.1.1
raw patch · 17 files changed
+1972/−0 lines, 17 filesdep +QuickCheckdep +attoparsecdep +basesetup-changed
Dependencies added: QuickCheck, attoparsec, base, containers, expressions, lattices, singletons, tasty, tasty-quickcheck, text, transformers
Files
- ChangeLog.md +34/−0
- LICENSE +30/−0
- Setup.hs +2/−0
- expressions.cabal +95/−0
- src/Data/Expression.hs +901/−0
- src/Data/Expression/Arithmetic.hs +229/−0
- src/Data/Expression/Array.hs +109/−0
- src/Data/Expression/Equality.hs +78/−0
- src/Data/Expression/Parser.hs +146/−0
- src/Data/Expression/Sort.hs +116/−0
- src/Data/Expression/Utils/Indexed/Eq.hs +23/−0
- src/Data/Expression/Utils/Indexed/Foldable.hs +20/−0
- src/Data/Expression/Utils/Indexed/Functor.hs +42/−0
- src/Data/Expression/Utils/Indexed/Show.hs +18/−0
- src/Data/Expression/Utils/Indexed/Sum.hs +76/−0
- src/Data/Expression/Utils/Indexed/Traversable.hs +27/−0
- test/Main.hs +26/−0
+ ChangeLog.md view
@@ -0,0 +1,34 @@+# Change Log++## 0.1.1 -- 2017-09-06++* 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++* 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++* Parsing++## 0.1.0.0 -- 2017-05-23++* Sorted Expressions à la Carte
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2017, Jakub Daniel++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Jakub Daniel nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ expressions.cabal view
@@ -0,0 +1,95 @@+name: expressions+version: 0.1.1+synopsis: Expressions and Formulas a la carte+description:+ This package is aimed at providing means of fixing a first-order language and+ declaring sorted expressions and formulae, the types ensure the declared+ expressions fall within the language.+ .+ This package pre-defines the common logical symbols for conjunction,+ disjunction, negation, and universal and existential quantification as well+ as some specific non-logical symbols such as equality, addition of linear+ integer arithmetic, and other. Common languages such as Lia and ALia+ (standard linear integer arithmetic and linear integer arithmetic with+ arrays) come included.+ .+ An example of a formula declaration:+ .+ > -- Let's state that zero is successor to no integer (while this would be+ > -- true for non-negative integers, stated this way it is clearly false, but+ > -- it still is a well-formed first-order statement)+ >+ > forall [var "x" :: Var 'IntegralSort] (cnst 0 ./=. var "x" .+. cnst 1) :: Lia 'BooleanSort+ .+ Let's see what declarations the library rejects:+ .+ > (var "x" :: Lia 'BooleanSort) .=. (var "y" :: Lia 'IntegralSort)+ > (var "x" :: Lia 'BooleanSort) .=. (var "y" :: ALia 'BooleanSort)+ > forall [var "x" :: Var 'IntegralSort] true :: QFLia 'BooleanSort++license: BSD3+license-file: LICENSE+author: Jakub Daniel+maintainer: jakub.daniel@protonmail.com+copyright: Copyright (C) 2017 Jakub Daniel+category: Data, Logic, Math+build-type: Simple+extra-source-files: ChangeLog.md+cabal-version: >=1.10++source-repository head+ type: git+ location: https://github.com/jakubdaniel/expressions.git++library+ exposed-modules: Data.Expression,+ Data.Expression.Arithmetic,+ Data.Expression.Array,+ Data.Expression.Equality,+ Data.Expression.Parser,+ Data.Expression.Sort,+ Data.Expression.Utils.Indexed.Eq,+ Data.Expression.Utils.Indexed.Foldable,+ Data.Expression.Utils.Indexed.Functor,+ Data.Expression.Utils.Indexed.Show,+ Data.Expression.Utils.Indexed.Sum+ Data.Expression.Utils.Indexed.Traversable+ other-extensions: DataKinds,+ FlexibleContexts,+ FlexibleInstances,+ GADTs,+ KindSignatures,+ MultiParamTypeClasses,+ OverloadedStrings,+ RankNTypes,+ ScopedTypeVariables,+ TemplateHaskell,+ TypeFamilies,+ TypeInType,+ TypeOperators,+ TypeSynonymInstances,+ UndecidableInstances+ build-depends: attoparsec >=0.13 && <0.14,+ base >=4.9 && <4.10,+ containers >=0.5.7 && <0.5.8,+ lattices >=1.6 && <1.7,+ singletons >=2.2 && <2.3,+ text >=1.2 && <1.3,+ transformers >=0.5.2 && <0.5.3+ hs-source-dirs: src+ default-language: Haskell2010+ ghc-options: -Wall++test-suite test+ type: exitcode-stdio-1.0+ build-depends: base,+ expressions,+ singletons,+ text,+ tasty,+ tasty-quickcheck,+ QuickCheck >=2.10 && <2.11+ hs-source-dirs: test+ main-is: Main.hs+ default-language: Haskell2010+ ghc-options: -Wall
+ src/Data/Expression.hs view
@@ -0,0 +1,901 @@+{-# LANGUAGE DataKinds+ , FlexibleContexts+ , FlexibleInstances+ , GADTs+ , MultiParamTypeClasses+ , OverloadedStrings+ , RankNTypes+ , ScopedTypeVariables+ , TypeInType+ , TypeOperators+ , UndecidableInstances #-}++--------------------------------------------------------------------------------+-- |+-- Module : Data.Expression+-- Copyright : (C) 2017-18 Jakub Daniel+-- License : BSD-style (see the file LICENSE)+-- Maintainer : Jakub Daniel <jakub.daniel@protonmail.com>+-- Stability : experimental+--+-- Usage:+--+-- You can build expressions in predefined languages (`QFLogic`, `QFLia`,+-- `QFALia`, `Lia`, `ALia`) using the smart constructors such as `var`, `and`,+-- `or`, `not`, `forall`, `exists` (or operators `.&.`, `.|.`, `.->.`, `.<-.`,+-- `.<->.`) or you can define your own sorted language as a fixpoint (`IFix`)+-- of a sum (`:+:`) of indexed functors (`IFunctor`).+--------------------------------------------------------------------------------++module Data.Expression ( module Data.Expression.Arithmetic+ , module Data.Expression.Array+ , module Data.Expression.Equality+ , module Data.Expression.Parser+ , module Data.Expression.Sort+ , module Data.Expression.Utils.Indexed.Eq+ , module Data.Expression.Utils.Indexed.Foldable+ , module Data.Expression.Utils.Indexed.Functor+ , module Data.Expression.Utils.Indexed.Show+ , module Data.Expression.Utils.Indexed.Sum+ , module Data.Expression.Utils.Indexed.Traversable++ -- Functors representing usual combinations of languages+ , QFLogicF+ , QFLiaF+ , LiaF+ , QFALiaF+ , ALiaF++ -- Simplest language+ , Var++ -- Usual languages+ , QFLogic+ , QFLia+ , Lia+ , QFALia+ , ALia++ -- Algebraic view of languages+ , ComplementedLattice(..)++ -- Convenient type synonyms+ , VariableName++ -- Functors representing the main language ingredients+ , VarF(..)+ , ConjunctionF(..)+ , DisjunctionF(..)+ , NegationF(..)+ , UniversalF(..)+ , ExistentialF(..)++ -- Substitution facilities+ , Substitution(..)+ , substitute+ , for++ -- Smart expression constructors+ , var+ , true+ , false+ , and+ , or+ , not+ , forall+ , exists++ -- Smart binary expression operators+ , (.&.)+ , (.|.)+ , (.->.)+ , (.<-.)+ , (.<->.)+ , (./=.)++ -- Convenient destructors+ , literals+ , conjuncts+ , disjuncts+ , vars+ , freevars++ -- Predicates+ , MaybeQuantified+ , isQuantified+ , isQuantifierFree++ -- Special forms+ , NNF+ , nnf++ , Prenex+ , prenex++ , Flatten+ , flatten++ , Unstore+ , unstore ) where++import Algebra.Lattice+import Control.Applicative hiding (Const)+import Control.Monad+import Control.Monad.Trans.Class+import Control.Monad.Trans.Reader+import Control.Monad.Trans.State+import Data.List hiding (and, or, union)+import Data.Map hiding (map, foldr, mapMaybe, partition)+import Data.Maybe+import Data.Monoid+import Data.Singletons+import Data.Singletons.Decide+import Prelude hiding (and, or, not)++import Data.Expression.Arithmetic+import Data.Expression.Array+import Data.Expression.Equality+import Data.Expression.Parser+import Data.Expression.Sort hiding (index)+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+import qualified Prelude as P++-- | A functor representing propositional logic embedded in first order logic (quantifier-free, boolean variables aka propositions, logical connectives `and`, `or`, `not`, equality of propositions)+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++-- | A functor much like `QFLiaF` with quantifiers over booleans and integers+type LiaF = ExistentialF 'BooleanSort :+: ExistentialF 'IntegralSort :+: UniversalF 'BooleanSort :+: UniversalF 'IntegralSort :+: QFLiaF++-- | A functor representing the language of quantifier-free linear integer arithmetic and array theories in first order logic (much like `QFLiaF` with additional array variables, `select`, and `store`)+type QFALiaF = ArrayF :+: QFLiaF++-- | A functor much like `QFALiaF` with quantifiers over booleans and integers+type ALiaF = ExistentialF 'BooleanSort :+: ExistentialF 'IntegralSort :+: UniversalF 'BooleanSort :+: UniversalF 'IntegralSort :+: QFALiaF++-- | A language consisting solely of variables (useful for listing variables outside of any particular context, such as bound variables of quantified formula)+type Var = IFix VarF++-- | A language obtained as fixpoint of `QFLogicF`+type QFLogic = IFix QFLogicF++-- | A language obtained as fixpoint of `QFLiaF`+type QFLia = IFix QFLiaF++-- | A language obtained as fixpoint of `LiaF`+type Lia = IFix LiaF++-- | A language obtained as fixpoint of `QFALiaF`+type QFALia = IFix QFALiaF++-- | A language obtained as fixpoint of `ALiaF`+type ALia = IFix ALiaF++-- | Bounded lattices that support complementing elements+--+-- prop> complement . complement = id+-- +class BoundedLattice a => ComplementedLattice a where+ complement :: a -> a++instance JoinSemiLattice (QFLogic 'BooleanSort) where a `join` b = a .|. b+instance JoinSemiLattice (QFLia 'BooleanSort) where a `join` b = a .|. b+instance JoinSemiLattice ( Lia 'BooleanSort) where a `join` b = a .|. b+instance JoinSemiLattice (QFALia 'BooleanSort) where a `join` b = a .|. b+instance JoinSemiLattice ( ALia 'BooleanSort) where a `join` b = a .|. b++instance MeetSemiLattice (QFLogic 'BooleanSort) where a `meet` b = a .&. b+instance MeetSemiLattice (QFLia 'BooleanSort) where a `meet` b = a .&. b+instance MeetSemiLattice ( Lia 'BooleanSort) where a `meet` b = a .&. b+instance MeetSemiLattice (QFALia 'BooleanSort) where a `meet` b = a .&. b+instance MeetSemiLattice ( ALia 'BooleanSort) where a `meet` b = a .&. b++instance Lattice (QFLogic 'BooleanSort)+instance Lattice (QFLia 'BooleanSort)+instance Lattice ( Lia 'BooleanSort)+instance Lattice (QFALia 'BooleanSort)+instance Lattice ( ALia 'BooleanSort)++instance BoundedJoinSemiLattice (QFLogic 'BooleanSort) where bottom = false+instance BoundedJoinSemiLattice (QFLia 'BooleanSort) where bottom = false+instance BoundedJoinSemiLattice ( Lia 'BooleanSort) where bottom = false+instance BoundedJoinSemiLattice (QFALia 'BooleanSort) where bottom = false+instance BoundedJoinSemiLattice ( ALia 'BooleanSort) where bottom = false++instance BoundedMeetSemiLattice (QFLogic 'BooleanSort) where top = true+instance BoundedMeetSemiLattice (QFLia 'BooleanSort) where top = true+instance BoundedMeetSemiLattice ( Lia 'BooleanSort) where top = true+instance BoundedMeetSemiLattice (QFALia 'BooleanSort) where top = true+instance BoundedMeetSemiLattice ( ALia 'BooleanSort) where top = true++instance BoundedLattice (QFLogic 'BooleanSort)+instance BoundedLattice (QFLia 'BooleanSort)+instance BoundedLattice ( Lia 'BooleanSort)+instance BoundedLattice (QFALia 'BooleanSort)+instance BoundedLattice ( ALia 'BooleanSort)++instance ComplementedLattice (QFLogic 'BooleanSort) where complement = nnf . not+instance ComplementedLattice (QFLia 'BooleanSort) where complement = nnf . not+instance ComplementedLattice ( Lia 'BooleanSort) where complement = nnf . not+instance ComplementedLattice (QFALia 'BooleanSort) where complement = nnf . not+instance ComplementedLattice ( ALia 'BooleanSort) where complement = nnf . not++-- | Type of names assigned to variables+type VariableName = String++-- | A functor representing a sorted variable, each variable is identified by its name and sort+data VarF a (s :: Sort) where+ Var :: VariableName -> Sing s -> VarF a s++instance IEq1 VarF where+ Var na _ `ieq1` Var nb _ = na == nb++instance IFunctor VarF where+ imap _ (Var n s) = Var n s+ index (Var _ s) = s++instance IFoldable VarF where+ ifold _ = F.Const mempty++instance ITraversable VarF where+ itraverse _ (Var n s) = pure (Var n s)++instance IShow VarF where+ ishow (Var n s) = F.Const ("(" ++ n ++ " : " ++ show s ++ ")")++instance VarF :<: f => Parseable VarF f where+ parser _ _ = choice [ var', var'' ] <?> "Var" where+ var' = do+ _ <- char '('+ n <- identifier+ _ <- space *> char ':' *> space+ s <- lift . lift $ parseSort+ _ <- char ')'++ assertSort n s++ var''' n s++ var'' = do+ n <- many1 letter++ s <- assumeSort n++ var''' n s++ var''' :: VariableName -> DynamicSort -> Parser (DynamicallySorted f)+ var''' n (DynamicSort (s :: Sing s)) = return $ DynamicallySorted s (inject (Var n s))++-- | A smart constructor for variables of any sort in any language+-- Takes the variable name and infers the target language and sort from context.+--+-- @+-- var "a" :: Lia 'IntegralSort+-- @+var :: forall f s. ( VarF :<: f, SingI s ) => VariableName -> IFix f s+var n = inject (Var n (sing :: Sing s))++-- | Collects a list of all variables occurring in an expression (bound or free).+vars :: ( VarF :<: f, IFoldable f, IFunctor f ) => IFix f s -> [DynamicallySorted VarF]+vars = nub . F.getConst . icata vars' where+ vars' a = case prj a of+ Just (Var n s) -> F.Const [DynamicallySorted s . inject $ Var n s]+ Nothing -> ifold a++-- | Substitution that given an expression produces replacement if the expression is to be replaced or nothing otherwise.+newtype Substitution f = Substitution { runSubstitution :: forall (s :: Sort). IFix f s -> Maybe (IFix f s) }++-- | A simple constructor of substitutions that replaces the latter expression with the former.+for :: forall f (s :: Sort). ( IFunctor f, IEq1 f ) => IFix f s -> IFix f s -> Substitution f+b `for` a = Substitution $ \c -> case index (unIFix a) %~ index (unIFix c) of+ Proved Refl -> if a == c then Just b else Nothing+ Disproved _ -> Nothing++-- | Executes a substitution.+substitute :: ( IFunctor f, IEq1 f ) => IFix f s -> Substitution f -> IFix f s+substitute a s = case runSubstitution s a of+ Just b -> b+ Nothing -> IFix . imap (flip substitute s) . unIFix $ a++instance Monoid (Substitution f) where+ mempty = Substitution (const Nothing)+ (Substitution f) `mappend` (Substitution g) = Substitution $ \a -> getFirst (mconcat ([First . f, First . g] <*> [a]))++-- | A functor representing a logical connective for conjunction+data ConjunctionF a (s :: Sort) where+ And :: [a 'BooleanSort] -> ConjunctionF a 'BooleanSort++-- | A functor representing a logical connective for disjunction+data DisjunctionF a (s :: Sort) where+ Or :: [a 'BooleanSort] -> DisjunctionF a 'BooleanSort++-- | A functor representing a logical connective for negation+data NegationF a (s :: Sort) where+ Not :: a 'BooleanSort -> NegationF a 'BooleanSort++instance IEq1 ConjunctionF where+ And as `ieq1` And bs = foldr (&&) True $ zipWith ieq as bs++instance IEq1 DisjunctionF where+ Or as `ieq1` Or bs = foldr (&&) True $ zipWith ieq as bs++instance IEq1 NegationF where+ Not a `ieq1` Not b = a `ieq` b++instance IFunctor ConjunctionF where+ imap f (And as) = And $ map f as+ index And {} = SBooleanSort++instance IFunctor DisjunctionF where+ imap f (Or os) = Or $ map f os+ index Or {} = SBooleanSort++instance IFunctor NegationF where+ imap f (Not n) = Not $ f n+ index Not {} = SBooleanSort++instance IFoldable ConjunctionF where+ ifold (And as) = F.Const . mconcat . map F.getConst $ as++instance IFoldable DisjunctionF where+ ifold (Or os) = F.Const . mconcat . map F.getConst $ os++instance IFoldable NegationF where+ ifold (Not n) = n++instance ITraversable ConjunctionF where+ itraverse f (And as) = And <$> traverse f as++instance ITraversable DisjunctionF where+ itraverse f (Or os) = Or <$> traverse f os++instance ITraversable NegationF where+ itraverse f (Not n) = Not <$> f n++instance IShow ConjunctionF where+ ishow (And []) = F.Const $ "true"+ ishow (And as) = F.Const $ "(and " ++ intercalate " " (map F.getConst as) ++ ")"++instance IShow DisjunctionF where+ ishow (Or []) = F.Const $ "false"+ ishow (Or os) = F.Const $ "(or " ++ intercalate " " (map F.getConst os) ++ ")"++instance IShow NegationF where+ ishow (Not n) = F.Const $ "(not " ++ F.getConst n ++ ")"++instance ConjunctionF :<: f => Parseable ConjunctionF f where+ parser _ r = choice [ true', and' ] <?> "Conjunction" where+ true' = string "true" *> pure (DynamicallySorted SBooleanSort $ true)++ and' = do+ _ <- char '(' *> string "and" *> space+ as <- r `sepBy1` space+ _ <- char ')'+ and'' as++ and'' as = case mapM toStaticallySorted as of+ Just as' -> return . DynamicallySorted SBooleanSort $ 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)++ or' = do+ _ <- char '(' *> string "or" *> space+ os <- r `sepBy1` space+ _ <- char ')'+ or'' os++ or'' os = case mapM toStaticallySorted os of+ Just os' -> return . DynamicallySorted SBooleanSort $ or os'+ Nothing -> fail "or of non-boolean arguments"++instance NegationF :<: f => Parseable NegationF f where+ parser _ r = not' <?> "Negation" where+ not' = do+ _ <- char '(' *> string "not" *> space+ n <- r+ _ <- char ')'+ not'' n++ not'' n = case toStaticallySorted n of+ Just n' -> return . DynamicallySorted SBooleanSort $ 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.+literals :: ( ConjunctionF :<: f, DisjunctionF :<: f ) => IFix f 'BooleanSort -> [IFix f 'BooleanSort]+literals e = fromMaybe [e] $ (concatMap literals <$> conjuncts' e)+ <|> (concatMap literals <$> disjuncts' e)++conjuncts' :: ConjunctionF :<: f => IFix f 'BooleanSort -> Maybe [IFix f 'BooleanSort]+conjuncts' e = (\(And as) -> as) <$> match e++disjuncts' :: DisjunctionF :<: f => IFix f 'BooleanSort -> Maybe [IFix f 'BooleanSort]+disjuncts' e = (\(Or os) -> os) <$> match e++-- | `conjuncts` decomposes a conjunction into conjuncts.+conjuncts :: ConjunctionF :<: f => IFix f 'BooleanSort -> [IFix f 'BooleanSort]+conjuncts e = fromMaybe [e] (conjuncts' e)++-- | `disjuncts` decomposes a disjunction into disjuncts.+disjuncts :: DisjunctionF :<: f => IFix f 'BooleanSort -> [IFix f 'BooleanSort]+disjuncts e = fromMaybe [e] (disjuncts' e)++-- | A smart constructor for binary conjunction+(.&.) :: ConjunctionF :<: f => IFix f 'BooleanSort -> IFix f 'BooleanSort -> IFix f 'BooleanSort+a .&. b = merge (flatten'' a ++ flatten'' b) where+ merge [] = true+ merge [f] = f+ merge as = inject $ And as++ flatten'' e = case match e of+ Just (And as) -> as+ _ -> [e]++-- | A smart constructor for binary disjunction+(.|.) :: DisjunctionF :<: f => IFix f 'BooleanSort -> IFix f 'BooleanSort -> IFix f 'BooleanSort+a .|. b = merge (flatten'' a ++ flatten'' b) where+ merge [] = false+ merge [f] = f+ merge os = inject $ Or os++ flatten'' e = case match e of+ Just (Or os) -> os+ _ -> [e]++(.->.), (.<-.) :: ( DisjunctionF :<: f, NegationF :<: f ) => IFix f 'BooleanSort -> IFix f 'BooleanSort -> IFix f 'BooleanSort++-- | A smart constructor for implication (an abbreviation for @not a .|. b@)+a .->. b = not a .|. b++-- | A smart constructor for reversed implication (an abbreviation for @a .|. not b@)+a .<-. b = b .->. a++-- | A smart constructor for if-and-only-if connective+(.<->.) :: ( ConjunctionF :<: f, DisjunctionF :<: f, NegationF :<: f ) => IFix f 'BooleanSort -> IFix f 'BooleanSort -> IFix f 'BooleanSort+a .<->. b = (a .->. b) .&. (a .<-. b)++-- | A smart constructor for disequality+(./=.) :: forall f s. ( NegationF :<: f, EqualityF :<: f, SingI s ) => IFix f s -> IFix f s -> IFix f 'BooleanSort+a ./=. b = not (a .=. b)++infix 7 ./=.+infixr 6 .&.+infixr 5 .|.+infixr 4 .->.+infixl 4 .<-.+infix 3 .<->.++-- | Logical tautology+true :: ConjunctionF :<: f => IFix f 'BooleanSort+true = inject $ And []++-- | Logical contradiction+false :: DisjunctionF :<: f => IFix f 'BooleanSort+false = inject $ Or []++-- | A smart constructor for variadic conjunction+and :: ConjunctionF :<: f => [IFix f 'BooleanSort] -> IFix f 'BooleanSort+and [] = true+and [a] = a+and as = foldr (.&.) true as++-- | A smart constructor for variadic disjunction+or :: DisjunctionF :<: f => [IFix f 'BooleanSort] -> IFix f 'BooleanSort+or [] = false+or [o] = o+or os = foldr (.|.) false os++-- | A smart constructor for negation+not :: NegationF :<: f => IFix f 'BooleanSort -> IFix f 'BooleanSort+not n = case match n of+ Just (Not n') -> n'+ _ -> inject $ Not n++-- | A functor representing a mono-sorted universal quantifier binding a number of variables within a formula+data UniversalF (v :: Sort) a (s :: Sort) where+ Forall :: [Var v] -> a 'BooleanSort -> UniversalF v a 'BooleanSort++-- | A functor representing a mono-sorted existential quantifier binding a number of variables within a formula+data ExistentialF (v :: Sort) a (s :: Sort) where+ Exists :: [Var v] -> a 'BooleanSort -> ExistentialF v a 'BooleanSort++instance IEq1 (UniversalF v) where+ Forall as phi `ieq1` Forall bs psi = (foldr (&&) True $ zipWith ieq as bs) && phi `ieq` psi++instance IEq1 (ExistentialF v) where+ Exists as phi `ieq1` Exists bs psi = (foldr (&&) True $ zipWith ieq as bs) && phi `ieq` psi++instance IFunctor (UniversalF v) where+ imap f (Forall vs phi) = Forall vs $ f phi+ index Forall {} = SBooleanSort++instance IFunctor (ExistentialF v) where+ imap f (Exists vs phi) = Exists vs $ f phi+ index Exists {} = SBooleanSort++instance IFoldable (UniversalF v) where+ ifold (Forall _ b) = b++instance IFoldable (ExistentialF v) where+ ifold (Exists _ b) = b++instance ITraversable (UniversalF v) where+ itraverse f (Forall vs b) = Forall vs <$> f b++instance ITraversable (ExistentialF v) where+ itraverse f (Exists vs b) = Exists vs <$> f b++instance IShow (UniversalF v) where+ ishow (Forall vs phi) = F.Const $ "(forall (" ++ intercalate " " (map show vs) ++ ") " ++ F.getConst phi ++ ")"++instance IShow (ExistentialF v) where+ ishow (Exists vs phi) = F.Const $ "(exists (" ++ intercalate " " (map show vs) ++ ") " ++ F.getConst phi ++ ")"++instance ( UniversalF v :<: f, SingI v ) => Parseable (UniversalF v) f where+ parser _ r = forall' <?> "Universal" where+ var' :: Parser (DynamicallySorted VarF)+ var' = parser (Proxy :: Proxy VarF) var'++ forall' = do+ _ <- char '(' *> string "forall" *> space *> char '('+ vs <- var' `sepBy1` space+ _ <- char ')' *> space+ phi <- local (union (fromList $ map context vs)) r+ _ <- char ')'+ forall'' vs phi++ 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'+ Nothing -> fail "quantifying non-boolean expression"+ Nothing -> fail "ill-sorted quantifier"++ context (DynamicallySorted s v) = case match v of+ Just (Var n _) -> (n, DynamicSort s)+ _ -> error "impossible error"++instance ( ExistentialF v :<: f, SingI v ) => Parseable (ExistentialF v) f where+ parser _ r = exists' <?> "Existential" where+ var' :: Parser (DynamicallySorted VarF)+ var' = parser (Proxy :: Proxy VarF) var'++ exists' = do+ _ <- char '(' *> string "exists" *> space *> char '('+ vs <- var' `sepBy1` space+ _ <- char ')' *> space+ phi <- local (union (fromList $ map context vs)) r+ _ <- char ')'+ exists'' vs phi++ 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'+ Nothing -> fail "quantifying non-boolean expression"+ Nothing -> fail "ill-sorted quantifier"++ context (DynamicallySorted s v) = case match v of+ Just (Var n _) -> (n, DynamicSort s)+ _ -> error "impossible error"++class MaybeQuantified f where+ isQuantified' :: MaybeQuantified g => f (IFix g) s -> F.Const Any s+ freevars' :: f (F.Const [DynamicallySorted VarF]) s -> F.Const [DynamicallySorted VarF] s++instance MaybeQuantified VarF where+ isQuantified' _ = F.Const (Any False)+ freevars' (Var n s) = F.Const [DynamicallySorted s . inject $ Var n s]++instance MaybeQuantified (UniversalF v) where+ isQuantified' _ = F.Const (Any True)+ freevars' (Forall vs a) = F.Const . P.filter (`notElem` map (\v@(IFix (Var _ s)) -> DynamicallySorted s v) vs) . F.getConst $ a++instance MaybeQuantified (ExistentialF v) where+ isQuantified' _ = F.Const (Any True)+ freevars' (Exists vs a) = F.Const . P.filter (`notElem` map (\v@(IFix (Var _ s)) -> DynamicallySorted s v) vs) . F.getConst $ a++instance ( MaybeQuantified f, MaybeQuantified g ) => MaybeQuantified (f :+: g) where+ isQuantified' (InL fa) = isQuantified' fa+ isQuantified' (InR gb) = isQuantified' gb+ freevars' (InL fa) = freevars' fa+ freevars' (InR fb) = freevars' fb++instance {-# OVERLAPPABLE #-} ( IFunctor f, IFoldable f ) => MaybeQuantified f where+ isQuantified' = ifold . imap (isQuantified' . unIFix)+ freevars' = ifold++-- | Test whether an expression contains a quantifier.+isQuantified :: MaybeQuantified f => IFix f s -> Bool+isQuantified = getAny . F.getConst . isQuantified' . unIFix++-- | Tests whether an expression is free of any quantifier.+isQuantifierFree :: MaybeQuantified f => IFix f s -> Bool+isQuantifierFree = P.not . isQuantified++-- | Collects a list of all free variables occurring in an expression.+freevars :: ( IFunctor f, MaybeQuantified f ) => IFix f s -> [DynamicallySorted VarF]+freevars = nub . F.getConst . icata freevars'++-- | A smart constructor for universally quantified formulae+forall :: UniversalF v :<: f => [Var v] -> IFix f 'BooleanSort -> IFix f 'BooleanSort+forall [] f = f+forall vs f = case match f of+ Just (Forall vs' f') -> forall (vs ++ vs') f'+ Nothing -> inject $ Forall vs f++-- | A smart constructor for existentially quantified formulae+exists :: ExistentialF v :<: f => [Var v] -> IFix f 'BooleanSort -> IFix f 'BooleanSort+exists [] f = f+exists vs f = case match f of+ Just (Exists vs' f') -> exists (vs ++ vs') f'+ Nothing -> inject $ Exists vs f++class HasDual f g where+ dual :: f (IFix g) 'BooleanSort -> IFix g 'BooleanSort++instance HasDual NegationF g where+ dual (Not a) = a++instance ( DisjunctionF :<: g, HasDual g g ) => HasDual ConjunctionF g where+ dual (And as) = or (map (dual . unIFix) as)++instance ( ConjunctionF :<: g, HasDual g g ) => HasDual DisjunctionF g where+ dual (Or os) = and (map (dual . unIFix) os)++instance ( ExistentialF v :<: g, HasDual g g ) => HasDual (UniversalF v) g where+ dual (Forall vs a) = exists vs (dual . unIFix $ a)++instance ( UniversalF v :<: g, HasDual g g ) => HasDual (ExistentialF v) g where+ dual (Exists vs a) = forall vs (dual . unIFix $ a)++instance ( HasDual f h, HasDual g h ) => HasDual (f :+: g) h where+ dual (InL fa) = dual fa+ dual (InR gb) = dual gb++instance {-# OVERLAPPABLE #-} ( f :<: g, NegationF :<: g ) => HasDual f g where+ dual = not . inject++class ( NegationF :<: f, HasDual f f ) => NNF f+instance ( NegationF :<: f, HasDual f f ) => NNF f++-- | Propagates negation toward boolean atoms (across conjunction, disjunction, quantifiers).+nnf :: forall f. NNF f => IFix f 'BooleanSort -> IFix f 'BooleanSort+nnf = nnf' where++ nnf' :: IFix f s -> IFix f s+ nnf' (IFix f) = case index f %~ SBooleanSort of+ Proved Refl -> fromJust $ ( match (IFix f) >>= not' ) <|> Just (IFix (imap nnf' f))+ Disproved _ -> IFix (imap nnf' f)++ not' :: NegationF (IFix f) 'BooleanSort -> Maybe (IFix f 'BooleanSort)+ not' (Not a) = return . dual . unIFix $ a++freename :: forall f (s :: Sort). ( VarF :<: f, IFunctor f, IFoldable f ) => IFix f s -> String+freename a = head . tail $ dropWhile (\s -> any (>= s) ns) pool where+ fs = vars a+ ns = sort $ map (\(DynamicallySorted _ (IFix (Var n _))) -> takeWhile (`elem` ['a'..'z']) n) fs++ 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])++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)+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++ 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)++instance ( VarF :<: g, UniversalF v :<: g, IEq1 g ) => MaybeQuantified' (UniversalF v) g where+ pushQuantifier (Forall vs a) = pushQuantifier' forall vs a++instance ( VarF :<: g, ExistentialF v :<: g, IEq1 g ) => MaybeQuantified' (ExistentialF v) g where+ pushQuantifier (Exists vs a) = pushQuantifier' exists vs a++instance ( MaybeQuantified' f h, MaybeQuantified' g h ) => MaybeQuantified' (f :+: g) h where+ pushQuantifier (InL fa) = pushQuantifier fa+ pushQuantifier (InR gb) = pushQuantifier gb++instance {-# OVERLAPPABLE #-} ( f :<: g, IFoldable f ) => MaybeQuantified' f g where+ pushQuantifier = return . inject++class ( VarF :<: f, NegationF :<: f, IFunctor f, IFoldable f, ITraversable f, HasDual f f, MaybeQuantified' f f ) => Prenex f+instance ( VarF :<: f, NegationF :<: f, IFunctor f, IFoldable f, ITraversable f, HasDual f f, MaybeQuantified' f f ) => Prenex f++-- | Puts an expression into prenex form (quantifier prefix and a quantifier-free formula).+prenex :: forall f. Prenex f => IFix f 'BooleanSort -> IFix f 'BooleanSort+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))++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++ let x :: forall f. VarF :<: f => IFix f v+ x = var n++ 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++ let x :: forall f. VarF :<: f => IFix f v+ x = var n++ put (ns, (freevars a, exists [x] . (x .=. a .&.)) : q)+ return x+ Disproved _ -> Nothing++instance ( Bind f h, Bind g h ) => Bind (f :+: g) h where+ bind _ a = let ls = bind (Proxy :: Proxy f) a+ rs = bind (Proxy :: Proxy g) a in merge ls rs where++ merge Nothing m = m+ merge m Nothing = m++ merge m@(Just (True, _)) _ = m+ merge _ m@(Just (True, _)) = m++ merge m _ = m++instance {-# OVERLAPPABLE #-} Bind f g where+ 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))++instance VarF :<: g => Bind' VarF g where+ bind' v = Just (True, return . inject $ v)++instance ArithmeticF :<: g => Bind' ArithmeticF g where+ bind' c@Const {} = Just (True, return . inject $ c)+ bind' a = bind (Proxy :: Proxy g) (inject a)++instance ConjunctionF :<: g => Bind' ConjunctionF g where+ bind' a@(And []) = Just (True, return . inject $ a)+ bind' a = bind (Proxy :: Proxy g) (inject a)++instance DisjunctionF :<: g => Bind' DisjunctionF g where+ bind' a@(Or []) = Just (True, return . inject $ a)+ bind' a = bind (Proxy :: Proxy g) (inject a)++instance ( Bind' f h, Bind' g h ) => Bind' (f :+: g) h where+ bind' (InL fa) = bind' fa+ bind' (InR gb) = bind' gb++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'' 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)++instance ArrayF :<: g => MaybeQuantified'' ArrayF g where+ flatten' (Select is es a i) = do+ a' <- bind'' a+ i' <- bind'' i+ return . inject $ Select is es a' i'+ flatten' (Store is es a i e) = do+ a' <- bind'' a+ i' <- bind'' i+ e' <- bind'' e+ return . inject $ Store is es a' i' e'++instance ( UniversalF v :<: g, SingI v ) => MaybeQuantified'' (UniversalF v) g where+ flatten' (Forall vs a) = do+ (ns, qs) <- get++ let (d, i) = partition (\(vs', _) -> any (`elem` mapMaybe toStaticallySorted vs') vs) qs++ put (ns, i)++ return $ forall vs (foldr snd a d)++instance ( ExistentialF v :<: g, SingI v ) => MaybeQuantified'' (ExistentialF v) g where+ flatten' (Exists vs a) = do+ (ns, qs) <- get++ let (d, i) = partition (\(vs', _) -> any (`elem` mapMaybe toStaticallySorted vs') vs) qs++ put (ns, i)++ return $ exists vs (foldr snd a d)++instance ( MaybeQuantified'' f h, MaybeQuantified'' g h ) => MaybeQuantified'' (f :+: g) h where+ flatten' (InL fa) = flatten' fa+ flatten' (InR gb) = flatten' gb++instance {-# OVERLAPPABLE #-} f :<: g => MaybeQuantified'' f g where+ flatten' = return . inject++class ( VarF :<: f, Bind f f, Bind' f f, MaybeQuantified'' f f, IFoldable f, ITraversable f ) => Flatten f+instance ( VarF :<: f, Bind f f, Bind' f f, MaybeQuantified'' f f, IFoldable f, ITraversable f ) => Flatten f++-- | Replaces non-variable and non-constant arguments to uninterpreted functions (such as `select` and `store`) with a fresh bound (universally or existentially) variable that is bound to the original term.+flatten :: forall f. Flatten f => IFix f 'BooleanSort -> IFix f 'BooleanSort+flatten f = let (a, (_, qs)) = runState (imapM flatten'' f) (freenames f, []) in foldr snd a qs where+ flatten'' f' = do+ (ns, q) <- get+ put (ns, [])+ r <- flatten' (unIFix f')+ (ns', q') <- get+ put (ns', q ++ q')+ return r++class Forall f g where+ quantify :: Proxy f -> Sing s -> Maybe ([Var s] -> IFix g 'BooleanSort -> IFix g 'BooleanSort)++instance ( UniversalF v :<: g, SingI v ) => Forall (UniversalF v) g where+ quantify _ s = case s %~ (sing :: Sing v) of+ Proved Refl -> Just forall+ Disproved _ -> Nothing++instance ( Forall f h, Forall g h ) => Forall (f :+: g) h where+ quantify _ s = quantify (Proxy :: Proxy f) s <|> quantify (Proxy :: Proxy g) s++instance {-# OVERLAPPABLE #-} Forall f g where+ quantify _ _ = Nothing++class Axiomatized f g where+ instantiate :: Forall g g => IFix g s -> f (IFix g) s -> Maybe (State [String] (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++ let j :: forall f. VarF :<: f => IFix f is+ j = inject $ Var n is++ 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++instance ( Axiomatized f h, Axiomatized g h ) => Axiomatized (f :+: g) h where+ instantiate v (InL fa) = instantiate v fa+ instantiate v (InR gb) = instantiate v gb++instance {-# OVERLAPPABLE #-} Axiomatized f g where+ instantiate _ _ = Nothing++class ( VarF :<: f, EqualityF :<: f, Bind f f, Bind' f f, MaybeQuantified'' f f, Forall f f, Axiomatized f f, IFoldable f, ITraversable f ) => Unstore f+instance ( VarF :<: f, EqualityF :<: f, Bind f f, Bind' f f, MaybeQuantified'' f f, Forall f f, Axiomatized f f, IFoldable f, ITraversable f ) => Unstore f++-- | 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' a' = fromMaybe (return a') (match a' >>= \(Equals _ l r) -> instantiate l (unIFix r) <|> instantiate r (unIFix l))
+ src/Data/Expression/Arithmetic.hs view
@@ -0,0 +1,229 @@+{-# LANGUAGE DataKinds+ , FlexibleContexts+ , FlexibleInstances+ , GADTs+ , RankNTypes+ , MultiParamTypeClasses+ , ScopedTypeVariables+ , TypeInType+ , TypeOperators #-}++--------------------------------------------------------------------------------+-- |+-- Module : Data.Expression.Arithmetic+-- 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.Arithmetic ( ArithmeticF(..)+ , cnst+ , add+ , mul+ , (.+.)+ , (.*.)+ , (.\.)+ , (.<.)+ , (.>.)+ , (.<=.)+ , (.>=.) ) where++import Data.List+import Data.Maybe+import Data.Monoid++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 linear integer arithmetic: constants (`cnst`), addition (`add` or `.+.`), multiplication (`mul` or `.*.`), divisibility predicate (`.\.`) and ordering (`.<.`, `.>.`, `.<=.`, `.>=.`).+data ArithmeticF a (s :: Sort) where+ Const :: Int -> ArithmeticF a 'IntegralSort+ Add :: [a 'IntegralSort] -> ArithmeticF a 'IntegralSort+ Mul :: [a 'IntegralSort] -> ArithmeticF a 'IntegralSort+ Divides :: Int -> a 'IntegralSort -> ArithmeticF a 'BooleanSort+ LessThan :: a 'IntegralSort -> a 'IntegralSort -> ArithmeticF a 'BooleanSort++instance IEq1 ArithmeticF where+ Const a `ieq1` Const b = a == b+ Add as `ieq1` Add bs = foldr (&&) True $ zipWith ieq as bs+ Mul as `ieq1` Mul bs = foldr (&&) True $ zipWith ieq as bs++ Divides c a `ieq1` Divides d b = a `ieq` b && c == d+ LessThan a c `ieq1` LessThan b d = a `ieq` b && c `ieq` d++ _ `ieq1` _ = False++instance IFunctor ArithmeticF where+ imap _ (Const c) = Const c+ imap f (Add as) = Add $ map f as+ imap f (Mul ms) = Mul $ map f ms+ imap f (c `Divides` a) = c `Divides` f a+ imap f (a `LessThan` b) = f a `LessThan` f b++ index Const {} = SIntegralSort+ index Add {} = SIntegralSort+ index Mul {} = SIntegralSort+ index Divides {} = SBooleanSort+ index LessThan {} = SBooleanSort++instance IFoldable ArithmeticF where+ ifold (Const _) = F.Const $ mempty+ ifold (Add as) = F.Const . mconcat . map F.getConst $ as+ ifold (Mul ms) = F.Const . mconcat . map F.getConst $ ms+ ifold (_ `Divides` a) = F.Const . F.getConst $ a+ ifold (a `LessThan` b) = F.Const (F.getConst a) <> F.Const (F.getConst b)++instance ITraversable ArithmeticF where+ itraverse _ (Const c) = pure (Const c)+ itraverse f (Add as) = Add <$> traverse f as+ itraverse f (Mul ms) = Mul <$> traverse f ms+ itraverse f (c `Divides` a) = Divides c <$> f a+ itraverse f (a `LessThan` b) = LessThan <$> f a <*> f b++instance IShow ArithmeticF where+ ishow (Const c) = F.Const $ show c+ ishow (Add as) = F.Const $ "(+ " ++ intercalate " " (map F.getConst as) ++ ")"+ ishow (Mul ms) = F.Const $ "(* " ++ intercalate " " (map F.getConst ms) ++ ")"+ ishow (c `Divides` a) = F.Const $ "(" ++ show c ++ "| " ++ F.getConst a ++ ")"+ ishow (a `LessThan` b) = F.Const $ "(< " ++ F.getConst a ++ " " ++ F.getConst b ++ ")"++instance ArithmeticF :<: f => Parseable ArithmeticF f where+ parser _ r = choice [ cnst', add', mul', divides', lessThan' ] <?> "Arithmetic" where+ cnst' = DynamicallySorted SIntegralSort . cnst <$> signed decimal++ add' = do+ _ <- char '(' *> char '+' *> space+ as <- r `sepBy1` space+ _ <- char ')'+ add'' as++ mul' = do+ _ <- char '(' *> char '*' *> space+ ms <- r `sepBy1` space+ _ <- char ')'+ mul'' ms++ divides' = do+ _ <- char '('+ c <- decimal+ _ <- char '|' *> space+ a <- r+ _ <- char ')'+ divides'' c a++ lessThan' = do+ _ <- char '(' *> char '<' *> space+ a <- r+ _ <- space+ b <- r+ _ <- char ')'+ lessThan'' a b++ add'' as = case mapM toStaticallySorted as of+ Just as' -> return . DynamicallySorted SIntegralSort $ add as'+ Nothing -> fail "add of non-integral arguments"++ mul'' ms = case mapM toStaticallySorted ms of+ Just ms' -> return . DynamicallySorted SIntegralSort $ mul ms'+ Nothing -> fail "mul of non-integral arguments"++ divides'' c a = case toStaticallySorted a of+ Just a' -> return . DynamicallySorted SBooleanSort $ 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'+ _ -> fail "less-than of non-integral arguments"++-- | A smart constructor for integer constants+cnst :: ArithmeticF :<: f => Int -> IFix f 'IntegralSort+cnst = inject . Const++mergeConstAdd :: ArithmeticF :<: f => IFix f 'IntegralSort -> (Int, [IFix f 'IntegralSort]) -> (Int, [IFix f 'IntegralSort])+mergeConstAdd e (acc, r) = case match e of+ Just (Const c) -> (acc + c, r)+ _ -> (acc, e : r)++-- | A smart constructor for binary addition+(.+.) :: forall f. ArithmeticF :<: f => IFix f 'IntegralSort -> IFix f 'IntegralSort -> IFix f 'IntegralSort+a .+. b = merge . (\(c, r) -> if c == 0 then r else cnst c : r) . foldr mergeConstAdd (0, []) $ flatten a ++ flatten b where+ merge [] = cnst 0+ merge [e] = e+ merge es = inject $ Add es++ flatten e = case match e of+ Just (Const 0) -> []+ Just (Add as) -> as+ _ -> [e]++mergeConstMul :: ArithmeticF :<: f => IFix f 'IntegralSort -> (Int, [IFix f 'IntegralSort]) -> (Int, [IFix f 'IntegralSort])+mergeConstMul e (acc, r) = case match e of+ Just (Const c) -> (acc * c, r)+ _ -> (acc, e : r)++-- | A smart constructor for a binary multiplication+(.*.) :: forall f. ArithmeticF :<: f => IFix f 'IntegralSort -> IFix f 'IntegralSort -> IFix f 'IntegralSort+a .*. b = merge . (\(c, r) -> if c == 1 then r else cnst c : r) . foldr mergeConstMul (1, []) $ flatten a ++ flatten b where+ merge [] = cnst 1+ merge [e] = e+ merge es = inject $ Mul es++ flatten e = case match e of+ Just (Const 1) -> []+ Just (Mul ms) -> ms+ _ -> [e]++-- | A smart constructor for a variadic addition+add :: ArithmeticF :<: f => [IFix f 'IntegralSort] -> IFix f 'IntegralSort+add [] = cnst 0+add [a] = a+add as = foldr (.+.) (cnst 0) as++-- | A smart constructor for a variadic multiplication+mul :: ArithmeticF :<: f => [IFix f 'IntegralSort] -> IFix f 'IntegralSort+mul [] = cnst 1+mul [m] = m+mul ms = foldr (.*.) (cnst 1) ms++-- | A smart constructor for a divisibility predicate+(.\.) :: ArithmeticF :<: f => Int -> IFix f 'IntegralSort -> IFix f 'BooleanSort+c .\. a = inject $ c `Divides` a++(.<.), (.>.), (.<=.), (.>=.) :: forall f. ArithmeticF :<: f => IFix f 'IntegralSort -> IFix f 'IntegralSort -> IFix f 'BooleanSort++-- | A smart constructor for @<@+a .<. b = fromJust . getFirst $ First (mergeL a b) <> First (mergeR a b) <> First (Just . inject $ a `LessThan` b) where+ merge :: (IFix f 'IntegralSort -> IFix f 'IntegralSort -> IFix f 'BooleanSort) -> IFix f 'IntegralSort -> IFix f 'IntegralSort -> Maybe (IFix f 'BooleanSort)+ merge cmp c d = do+ (Const v) <- match c+ (Add as) <- match d+ return . (\(v', r) -> cnst (-v') `cmp` add r) . foldr mergeConstAdd (0, []) $ cnst (-v) : as++ mergeL c d = merge (\x y -> inject $ x `LessThan` y) c d+ mergeR d c = merge (\x y -> inject $ y `LessThan` x) d c++-- | A smart constructor for @>@+a .>. b = b .<. a++-- | A smart constructor for @<=@+a .<=. b = a .<. b .+. cnst 1++-- | A smart constructor for @>=@+a .>=. b = a .+. cnst 1 .>. b++infixl 9 .*.+infixl 8 .+.+infix 7 .\.+infix 7 .<.+infix 7 .>.+infix 7 .<=.+infix 7 .>=.
+ src/Data/Expression/Array.hs view
@@ -0,0 +1,109 @@+{-# LANGUAGE FlexibleContexts+ , FlexibleInstances+ , GADTs+ , MultiParamTypeClasses+ , OverloadedStrings+ , RankNTypes+ , ScopedTypeVariables+ , TypeInType+ , TypeOperators #-}++--------------------------------------------------------------------------------+-- |+-- Module : Data.Expression.Array+-- 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.Array ( ArrayF(..)+ , select+ , store ) where++import Data.Functor.Const+import Data.Monoid+import Data.Singletons+import Data.Singletons.Decide++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++-- | A functor representing array-theoretic terms (`select` and `store` also known as "read" and "write")+data ArrayF a (s :: Sort) where+ Select :: Sing i -> Sing e -> a ('ArraySort i e) -> a i -> ArrayF a e+ Store :: Sing i -> Sing e -> a ('ArraySort i e) -> a i -> a e -> ArrayF a ('ArraySort i e)++instance IEq1 ArrayF where+ Select isa _ aa ia `ieq1` Select isb _ ab ib = case isa %~ isb of+ Proved Refl -> aa `ieq` ab && ia `ieq` ib+ Disproved _ -> False+ Store _ _ aa ia va `ieq1` Store _ _ ab ib vb = aa `ieq` ab && ia `ieq` ib && va `ieq` vb+ _ `ieq1` _ = False++instance IFunctor ArrayF where+ imap f (Select is es a i) = Select is es (f a) (f i)+ imap f (Store is es a i e) = Store is es (f a) (f i) (f e)++ index (Select _ es _ _ ) = es+ index (Store is es _ _ _) = SArraySort is es++instance IFoldable ArrayF where+ ifold (Select _ _ a i) = Const (getConst a) <> Const (getConst i)+ ifold (Store _ _ a i e) = Const (getConst a) <> Const (getConst i) <> Const (getConst e)++instance ITraversable ArrayF where+ itraverse f (Select is es a i) = Select is es <$> f a <*> f i+ itraverse f (Store is es a i e) = Store is es <$> f a <*> f i <*> f e++instance IShow ArrayF where+ ishow (Select _ _ a i) = Const $ "(select " ++ getConst a ++ " " ++ getConst i ++ ")"+ ishow (Store _ _ a i v) = Const $ "(store " ++ getConst a ++ " " ++ getConst i ++ " " ++ getConst v ++ ")"++instance ArrayF :<: f => Parseable ArrayF f where+ parser _ r = choice [ select', store' ] <?> "Array" where+ select' = do+ _ <- char '(' *> string "select" *> space+ a <- r+ _ <- space+ i <- r+ _ <- char ')'+ select'' a i+ store' = do+ _ <- char '(' *> string "store" *> space+ a <- r+ _ <- space+ i <- r+ _ <- space+ v <- r+ _ <- char ')'+ store'' a i v++ select'' :: DynamicallySorted f -> DynamicallySorted f -> Parser (DynamicallySorted f)+ select'' (DynamicallySorted (SArraySort is1 es) a)+ (DynamicallySorted is2 i) = case is1 %~ is2 of+ Proved Refl -> return . DynamicallySorted es $ inject (Select is1 es a i)+ Disproved _ -> fail "ill-sorted select"+ select'' _ _ = fail "selecting from non-array"++ store'' :: DynamicallySorted f -> DynamicallySorted f -> DynamicallySorted f -> Parser (DynamicallySorted f)+ store'' (DynamicallySorted as@(SArraySort _ _) a)+ (DynamicallySorted is i)+ (DynamicallySorted es v) = case as %~ SArraySort is es of+ Proved Refl -> return . DynamicallySorted as $ inject (Store is es a i v)+ Disproved _ -> fail "ill-sorted store"+ store'' _ _ _ = fail "storing to non-array"++-- | A smart constructor for select+select :: ( ArrayF :<: f, SingI i, SingI e ) => IFix f ('ArraySort i e) -> IFix f i -> IFix f e+select a i = inject (Select sing sing a i)++-- | A smart constructor for store+store :: ( ArrayF :<: f, SingI i, SingI e ) => IFix f ('ArraySort i e) -> IFix f i -> IFix f e -> IFix f ('ArraySort i e)+store a i v = inject (Store sing sing a i v)
+ src/Data/Expression/Equality.hs view
@@ -0,0 +1,78 @@+{-# LANGUAGE DataKinds+ , FlexibleContexts+ , FlexibleInstances+ , GADTs+ , MultiParamTypeClasses+ , RankNTypes+ , ScopedTypeVariables+ , TypeInType+ , TypeOperators #-}++--------------------------------------------------------------------------------+-- |+-- Module : Data.Expression.Equality+-- 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.Equality ( EqualityF(..)+ , (.=.) ) where++import Data.Functor.Const+import Data.Monoid+import Data.Singletons+import Data.Singletons.Decide++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++-- | A functor representing an equality predicate between two expressions of matching sort+data EqualityF a (s :: Sort) where+ Equals :: Sing s -> a s -> a s -> EqualityF a 'BooleanSort++instance IEq1 EqualityF where+ Equals sa aa ba `ieq1` Equals sb ab bb = case sa %~ sb of+ Proved Refl -> aa `ieq` ab && ba `ieq` bb+ Disproved _ -> False++instance IFunctor EqualityF where+ imap f (Equals s a b) = Equals s (f a) (f b)+ index (Equals _ _ _) = SBooleanSort++instance IFoldable EqualityF where+ ifold (Equals _ a b) = Const (getConst a) <> Const (getConst b)++instance ITraversable EqualityF where+ itraverse f (Equals s a b) = Equals s <$> f a <*> f b++instance IShow EqualityF where+ ishow (Equals _ a b) = Const $ "(= " ++ getConst a ++ " " ++ getConst b ++ ")"++instance EqualityF :<: f => Parseable EqualityF f where+ parser _ r = do+ _ <- char '(' *> char '=' *> space+ a <- r+ _ <- space+ b <- r+ _ <- char ')'+ equals a b <?> "Equality" where++ 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)+ Disproved _ -> fail "multi-sorted equality"++-- | A smart constructor for an equality predicate+(.=.) :: forall f s. ( EqualityF :<: f, SingI s ) => IFix f s -> IFix f s -> IFix f 'BooleanSort+a .=. b = inject (Equals (sing :: Sing s) a b)++infix 7 .=.
+ src/Data/Expression/Parser.hs view
@@ -0,0 +1,146 @@+{-# LANGUAGE FlexibleInstances+ , MultiParamTypeClasses+ , OverloadedStrings+ , ScopedTypeVariables+ , TypeInType+ , TypeOperators+ , UndecidableInstances #-}++--------------------------------------------------------------------------------+-- |+-- Module : Data.Expression.Parser+-- 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.Parser ( Context+ , Parser+ , Parseable(..)+ , parse+ , parseWith++ , char+ , choice+ , decimal+ , digit+ , letter+ , many1+ , sepBy1+ , signed+ , space+ , string++ , identifier++ , (<?>)++ , assertSort+ , assumeSort ) where++import Control.Monad+import Control.Monad.Trans.Class+import Control.Monad.Trans.Reader+import Control.Monad.Trans.State.Lazy+import Data.Map+import Data.Proxy+import Data.Singletons+import Data.Text hiding ( empty )+import Prelude hiding ( lookup )++import Data.Expression.Sort+import Data.Expression.Utils.Indexed.Functor+import Data.Expression.Utils.Indexed.Sum++import qualified Data.Attoparsec.Text as A++-- | Parsing context assigning sorts to known variables+type Context = Map String DynamicSort++-- | Context-sensitive parser that remembers sorts of variables+type Parser = ReaderT Context (StateT Context A.Parser)++-- | Expressions that can be parsed+class Parseable f g where+ parser :: Proxy f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)++-- | Tries to parse the entire input text and produce an expression in desired language and with desired sort.+parse :: forall f (s :: Sort). ( Parseable f f, SingI s ) => Text -> Maybe (IFix f s)+parse = parseWith empty++-- | Like `parse` but allows adding initial assumption about sorts of some variables.+parseWith :: forall f (s :: Sort). ( Parseable f f, SingI s ) => Context -> Text -> Maybe (IFix f s)+parseWith c = let a = parser (Proxy :: Proxy f) a in toStaticallySorted <=< A.maybeResult . flip A.feed "" . A.parse (evalStateT (runReaderT a c) empty <* A.endOfInput)++instance (Parseable f h, Parseable g h) => Parseable (f :+: g) h where+ parser _ r = A.choice [ parser (Proxy :: Proxy f) r, parser (Proxy :: Proxy g) r ]++-- | Matches a given character.+char :: Char -> Parser Char+char = lift . lift . A.char++-- | Matches first of many choices.+choice :: [Parser a] -> Parser a+choice = A.choice++-- | Matches a given decimal number.+decimal :: Parser Int+decimal = lift . lift $ A.decimal++-- | Matches a given digit.+digit :: Parser Char+digit = lift . lift $ A.digit++-- | Matches any character.+letter :: Parser Char+letter = lift . lift $ A.letter++-- | Matches one or more times.+many1 :: Parser a -> Parser [a]+many1 = A.many1++-- | Matches one or more times, separated by specified separator.+sepBy1 :: Parser a -> Parser s -> Parser [a]+sepBy1 = A.sepBy1++-- | Matches a signed number.+signed :: Parser Int -> Parser Int+signed m = (*) <$> (lift . lift) (A.signed (pure 1)) <*> m++-- | Matches space.+space :: Parser Char+space = lift . lift $ A.space++-- | Matches a given string.+string :: Text -> Parser Text+string = lift . lift . A.string++-- | Matches identifier that starts with [a-zA-Z'_@#] and is followed by [a-zA-Z'_@#0-9].+identifier :: Parser String+identifier = (:) <$> id' <*> A.many' (choice [ id', digit ]) where+ id' = choice [ letter, char '\'', char '_', char '@', char '#' ]++-- | Labels parser.+(<?>) :: Parser a -> String -> Parser a+a <?> l = ReaderT $ \r -> StateT $ \s -> runStateT (runReaderT a r) s A.<?> l++-- | Asserts what sort is assigned to a variable in current context.+assertSort :: String -> DynamicSort -> Parser ()+assertSort n s = do+ ss <- ask+ ds <- lift get++ case n `lookup` (ss `union` ds) of+ Just s' -> when (s /= s') $ fail "sort mismatch"+ Nothing -> lift $ modify (insert n s)++-- | Variable assumes sort based on current context.+assumeSort :: String -> Parser DynamicSort+assumeSort n = do+ ss <- ask+ ds <- lift get++ case n `lookup` (ss `union` ds) of+ Just s -> return s+ Nothing -> fail "unspecified sort"
+ src/Data/Expression/Sort.hs view
@@ -0,0 +1,116 @@+{-# OPTIONS_GHC -fno-warn-unused-binds #-}++{-# LANGUAGE GADTs+ , DataKinds+ , KindSignatures+ , OverloadedStrings+ , RankNTypes+ , ScopedTypeVariables+ , TemplateHaskell+ , TypeFamilies+ , TypeOperators+ , TypeSynonymInstances+ , TypeInType+ , UndecidableInstances #-}++--------------------------------------------------------------------------------+-- |+-- Module : Data.Expression.Sort+-- 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.Sort ( Sort(..)+ , Sing(..)+ , DynamicSort(..)+ , DynamicallySorted(..)+ , parseSort+ , toStaticSort+ , toStaticallySorted ) where++import Data.Attoparsec.Text+import Data.Kind+import Data.Singletons+import Data.Singletons.Decide+import Data.Singletons.TH++import Data.Expression.Utils.Indexed.Eq+import Data.Expression.Utils.Indexed.Functor+import Data.Expression.Utils.Indexed.Show++-- | A universe of recognized sorts+data Sort = BooleanSort -- ^ booleans (true, false)+ | IntegralSort -- ^ integers (..., -1, 0, 1, ...)+ | ArraySort { index :: Sort, element :: Sort } -- ^ arrays indexed by `index` sort, containing elements of `element` sort+ deriving Eq++genSingletons [''Sort]+singDecideInstance ''Sort++show' :: Sort -> String+show' BooleanSort = "bool"+show' IntegralSort = "int"+show' (ArraySort i e) = "(array " ++ show' i ++ " " ++ show' e ++ ")"++instance Show Sort where+ show s@BooleanSort = show' s+ show s@IntegralSort = show' s+ show (ArraySort i e) = "array " ++ show' i ++ " " ++ show' e++ssortToSort :: forall s. SSort s -> Sort+ssortToSort SBooleanSort = BooleanSort+ssortToSort SIntegralSort = IntegralSort+ssortToSort (SArraySort i e) = ArraySort (ssortToSort i) (ssortToSort e)++instance Show (SSort s) where+ show = show . ssortToSort++-- | Some sort (obtained for example during parsing)+data DynamicSort where+ DynamicSort :: forall (s :: Sort). Sing s -> DynamicSort++instance Eq DynamicSort where+ DynamicSort a == DynamicSort b = case a %~ b of+ Proved Refl -> True+ Disproved _ -> False++-- | An expression of some sort (obtained for example during parsing)+data DynamicallySorted (f :: (Sort -> *) -> (Sort -> *)) where+ DynamicallySorted :: forall (s :: Sort) f. Sing s -> IFix f s -> DynamicallySorted f++instance IEq1 f => Eq (DynamicallySorted f) where+ DynamicallySorted sa a == DynamicallySorted sb b = case sa %~ sb of+ Proved Refl -> a == b+ Disproved _ -> False++instance (IFunctor f, IShow f) => Show (DynamicallySorted f) where+ show (DynamicallySorted _ a) = show a++-- | Tries to convert some sort (`DynamicSort`) to a requested sort.+toStaticSort :: forall (s :: Sort). SingI s => DynamicSort -> Maybe (Sing s)+toStaticSort dx = case dx of+ DynamicSort x -> case x %~ (sing :: Sing s) of+ Proved Refl -> Just x+ Disproved _ -> Nothing++-- | Tries to convert an expression (`DynamicallySorted`) of some sort to an expression of requested sort.+-- Performs no conversions.+toStaticallySorted :: forall f (s :: Sort). SingI s => DynamicallySorted f -> Maybe (IFix f s)+toStaticallySorted dx = case dx of+ DynamicallySorted s x -> case s %~ (sing :: Sing s) of+ Proved Refl -> Just x+ Disproved _ -> Nothing++-- | Parser that accepts sort definitions such as @bool@, @int@, @array int int@, @array int (array ...)@.+parseSort :: Parser DynamicSort+parseSort = choice [ bool, int, array ] <?> "Sort" where+ bool = string "bool" *> pure (DynamicSort SBooleanSort)+ int = string "int" *> pure (DynamicSort SIntegralSort)+ array = array' <$> (string "array" *> space *> sort') <*> (space *> sort')++ sort' = choice [ bool, int, char '(' *> array <* char ')' ]++ array' :: DynamicSort -> DynamicSort -> DynamicSort+ array' (DynamicSort i) (DynamicSort e) = DynamicSort (SArraySort i e)
+ src/Data/Expression/Utils/Indexed/Eq.hs view
@@ -0,0 +1,23 @@+{-# LANGUAGE RankNTypes+ , TypeInType #-}++--------------------------------------------------------------------------------+-- |+-- Module : Data.Expression.Utils.Indexed.Eq+-- 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.Utils.Indexed.Eq where++import Data.Kind++-- | Indexed types that can be equated+class IEq (a :: i -> *) where+ ieq :: forall j. a j -> a j -> Bool++-- | Type constructors (usually functors) that produce types that can be equated+class IEq1 (f :: (i -> *) -> (i -> *)) where+ ieq1 :: forall a j. IEq a => f a j -> f a j -> Bool
+ src/Data/Expression/Utils/Indexed/Foldable.hs view
@@ -0,0 +1,20 @@+{-# LANGUAGE RankNTypes+ , TypeInType #-}++--------------------------------------------------------------------------------+-- |+-- Module : Data.Expression.Utils.Indexed.Foldable+-- 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.Utils.Indexed.Foldable (IFoldable(..)) where++import Data.Functor.Const+import Data.Kind++-- | Type constructors (usually functors) that can be folded+class IFoldable (f :: (i -> *) -> (i -> *)) where+ ifold :: Monoid m => f (Const m) i' -> Const m i'
+ src/Data/Expression/Utils/Indexed/Functor.hs view
@@ -0,0 +1,42 @@+{-# LANGUAGE RankNTypes+ , TypeInType+ , UndecidableInstances #-}++--------------------------------------------------------------------------------+-- |+-- Module : Data.Expression.Utils.Indexed.Functor+-- 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.Utils.Indexed.Functor (IFix(..), IFunctor(..), icata) where++import Data.Functor.Const+import Data.Kind+import Data.Singletons++import Data.Expression.Utils.Indexed.Eq+import Data.Expression.Utils.Indexed.Show++-- | A fixpoint of a functor in indexed category+newtype IFix f i = IFix { unIFix :: f (IFix f) i }++-- | A functor in indexed category+class IFunctor (f :: (i -> *) -> (i -> *)) where+ imap :: (forall i'. a i' -> b i') -> (forall i'. f a i' -> f b i')+ index :: forall a i'. f a i' -> Sing i'++-- | Indexed catamorphism+icata :: IFunctor f => (forall i. f a i -> a i) -> (forall i. IFix f i -> a i)+icata f = f . imap (icata f) . unIFix++instance IEq1 f => IEq (IFix f) where+ IFix a `ieq` IFix b = a `ieq1` b++instance IEq1 f => Eq (IFix f i) where+ IFix a == IFix b = a `ieq1` b++instance (IFunctor f, IShow f) => Show (IFix f i) where+ show = getConst . icata ishow
+ src/Data/Expression/Utils/Indexed/Show.hs view
@@ -0,0 +1,18 @@+{-# LANGUAGE TypeInType #-}++--------------------------------------------------------------------------------+-- |+-- Module : Data.Expression.Utils.Indexed.Show+-- 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.Utils.Indexed.Show where++import Data.Functor.Const++-- | `Show` for indexed type constructors (most importantly functors)+class IShow f where+ ishow :: f (Const String) i -> Const String i
+ src/Data/Expression/Utils/Indexed/Sum.hs view
@@ -0,0 +1,76 @@+{-# LANGUAGE FlexibleInstances+ , MultiParamTypeClasses+ , RankNTypes+ , TypeInType+ , TypeOperators #-}++--------------------------------------------------------------------------------+-- |+-- Module : Data.Expression.Utils.Indexed.Sum+-- 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.Utils.Indexed.Sum ((:+:)(..), (:<:)(..), inject, match) where++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.Traversable++-- | Sum of two indexed functors+data (f :+: g) a i = InL (f a i) | InR (g a i)++infixr 8 :+:++instance (IFunctor f, IFunctor g) => IFunctor (f :+: g) where+ imap f (InL fa) = InL $ imap f fa+ imap f (InR ga) = InR $ imap f ga++ index (InL fa) = index fa+ index (InR ga) = index ga++-- | Inclusion relation for indexed sum functors+class (IFunctor f, IFunctor g) => f :<: g where+ inj :: f a i -> g a i+ prj :: g a i -> Maybe (f a i)++instance IFunctor f => f :<: f where+ inj = id+ prj = Just+instance (IFunctor f, IFunctor g) => f :<: (f :+: g) where+ inj = InL+ prj (InL a) = Just a+ prj (InR _) = Nothing+instance {-# OVERLAPPABLE #-} (IFunctor f, IFunctor g, IFunctor h, f :<: g) => f :<: (h :+: g) where+ inj = InR . inj+ prj (InL _) = Nothing+ prj (InR a) = prj a++-- | Inject a component into a sum.+inject :: g :<: f => forall i. g (IFix f) i -> IFix f i+inject = IFix . inj++-- | Try to unpack a sum into a component.+match :: g :<: f => forall i. IFix f i -> Maybe (g (IFix f) i)+match = prj . unIFix++instance (IEq1 f, IEq1 g) => IEq1 (f :+: g) where+ InL a `ieq1` InL b = a `ieq1` b+ InR a `ieq1` InR b = a `ieq1` b+ _ `ieq1` _ = False++instance (IFoldable f, IFoldable g) => IFoldable (f :+: g) where+ ifold (InL fa) = ifold fa+ ifold (InR gb) = ifold gb++instance (ITraversable f, ITraversable g) => ITraversable (f :+: g) where+ itraverse f (InL fa) = InL <$> itraverse f fa+ itraverse f (InR gb) = InR <$> itraverse f gb++instance (IShow f, IShow g) => IShow (f :+: g) where+ ishow (InL fa) = ishow fa+ ishow (InR ga) = ishow ga
+ src/Data/Expression/Utils/Indexed/Traversable.hs view
@@ -0,0 +1,27 @@+{-# LANGUAGE KindSignatures+ , RankNTypes+ , TypeInType #-}++--------------------------------------------------------------------------------+-- |+-- Module : Data.Expression.Utils.Indexed.Traversable+-- 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.Utils.Indexed.Traversable where++import Control.Monad+import Data.Kind++import Data.Expression.Utils.Indexed.Functor++-- | Type constructors (usually functors) that can be traversed+class ITraversable (t :: (i -> *) -> (i -> *)) where+ itraverse :: forall (a :: i -> *) (b :: i -> *) f. Applicative f => (forall (i' :: i). a i' -> f (b i')) -> (forall (i' :: i). t a i' -> f (t b i'))++-- | Maps a monadic action over a traversable functor.+imapM :: ( ITraversable f, Monad m ) => (forall (i' :: i). IFix f i' -> m (IFix f i')) -> (forall (i' :: i). IFix f i' -> m (IFix f i'))+imapM f = f . IFix <=< itraverse (imapM f) . unIFix
+ test/Main.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE DataKinds+ , KindSignatures+ , OverloadedStrings+ , RankNTypes+ , TypeOperators #-}++import Data.Maybe+import Data.Singletons+import Data.Text+import Prelude hiding (and)+import Test.QuickCheck hiding ((.&.))+import Test.Tasty+import Test.Tasty.QuickCheck hiding ((.&.))++import Data.Expression++parseJust :: forall f (s :: Sort). ( Parseable f f, SingI s ) => Text -> IFix f s+parseJust = fromJust . parse++main :: IO ()+main = defaultMain $ testGroup "parsing" [ testProperty "1" $ once $ var "a" == (parseJust "(a : int)" :: ALia 'IntegralSort)+ , testProperty "2" $ once $ var "a" /= (parseJust "(+ (a : int) 3)" :: ALia 'IntegralSort)+ , testProperty "3" $ once $ var "a" .+. cnst 1 == (parseJust "(+ (a : int) 1)" :: ALia 'IntegralSort)+ , testProperty "4" $ once $ select (var "a") (var "b" .+. cnst 3) == (parseJust "(select (a : array int (array int bool)) (+ (b : int) 3))" :: QFALia ('ArraySort 'IntegralSort 'BooleanSort))+ , testProperty "5" $ once $ forall [var "x" :: Var 'IntegralSort] (exists [var "y" :: Var 'IntegralSort] (and [true, var "b" .=. (var "x" .<. var "y")])) == (parseJust "(forall ((x : int)) (exists ((y : int)) (and true (= (b : bool) (< x y)))))" :: Lia 'BooleanSort)+ , testProperty "6" $ once $ forall [var "x" :: Var 'IntegralSort, var "y"] (var "x" .<. var "y" .+. var "z") .&. var "z" .=. cnst 3 == (parseJust "(and (forall ((x : int) (y : int)) (< x (+ y (z : int)))) (= z 3))" :: Lia 'BooleanSort) ]