diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -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 diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/expressions.cabal b/expressions.cabal new file mode 100644 --- /dev/null +++ b/expressions.cabal @@ -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 diff --git a/src/Data/Expression.hs b/src/Data/Expression.hs new file mode 100644 --- /dev/null +++ b/src/Data/Expression.hs @@ -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 +-- 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)) diff --git a/src/Data/Expression/Arithmetic.hs b/src/Data/Expression/Arithmetic.hs new file mode 100644 --- /dev/null +++ b/src/Data/Expression/Arithmetic.hs @@ -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 +-- 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 .>=. diff --git a/src/Data/Expression/Array.hs b/src/Data/Expression/Array.hs new file mode 100644 --- /dev/null +++ b/src/Data/Expression/Array.hs @@ -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 +-- 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) diff --git a/src/Data/Expression/Equality.hs b/src/Data/Expression/Equality.hs new file mode 100644 --- /dev/null +++ b/src/Data/Expression/Equality.hs @@ -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 +-- 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 .=. diff --git a/src/Data/Expression/Parser.hs b/src/Data/Expression/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Data/Expression/Parser.hs @@ -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 +-- 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" diff --git a/src/Data/Expression/Sort.hs b/src/Data/Expression/Sort.hs new file mode 100644 --- /dev/null +++ b/src/Data/Expression/Sort.hs @@ -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 +-- 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) diff --git a/src/Data/Expression/Utils/Indexed/Eq.hs b/src/Data/Expression/Utils/Indexed/Eq.hs new file mode 100644 --- /dev/null +++ b/src/Data/Expression/Utils/Indexed/Eq.hs @@ -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 +-- 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 diff --git a/src/Data/Expression/Utils/Indexed/Foldable.hs b/src/Data/Expression/Utils/Indexed/Foldable.hs new file mode 100644 --- /dev/null +++ b/src/Data/Expression/Utils/Indexed/Foldable.hs @@ -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 +-- 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' diff --git a/src/Data/Expression/Utils/Indexed/Functor.hs b/src/Data/Expression/Utils/Indexed/Functor.hs new file mode 100644 --- /dev/null +++ b/src/Data/Expression/Utils/Indexed/Functor.hs @@ -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 +-- 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 diff --git a/src/Data/Expression/Utils/Indexed/Show.hs b/src/Data/Expression/Utils/Indexed/Show.hs new file mode 100644 --- /dev/null +++ b/src/Data/Expression/Utils/Indexed/Show.hs @@ -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 +-- 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 diff --git a/src/Data/Expression/Utils/Indexed/Sum.hs b/src/Data/Expression/Utils/Indexed/Sum.hs new file mode 100644 --- /dev/null +++ b/src/Data/Expression/Utils/Indexed/Sum.hs @@ -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 +-- 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 diff --git a/src/Data/Expression/Utils/Indexed/Traversable.hs b/src/Data/Expression/Utils/Indexed/Traversable.hs new file mode 100644 --- /dev/null +++ b/src/Data/Expression/Utils/Indexed/Traversable.hs @@ -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 +-- 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 diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -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) ]