expressions 0.4.2 → 0.5

raw patch · 4 files changed

+41/−38 lines, 4 filesdep ~lattices

Dependency ranges changed: lattices

Files

• ChangeLog.md +4/−0
• expressions.cabal +2/−2
• src/Data/Expression.hs +33/−34
• src/Data/Expression/Array.hs +2/−2

@@ -1,5 +1,9 @@ # Change Log +## 0.5++* Switch to lattices-2+ ## 0.4.2  * Allow a wide range of dynamically sorted values (not just expressions)

@@ -1,5 +1,5 @@ name:                expressions-version:             0.4.2+version:             0.5 synopsis:            Expressions and Formulae a la carte description:   This package is aimed at providing means of fixing a first-order language and@@ -74,7 +74,7 @@                        base >=4.11 && <4.13,                        containers >=0.5.7 && <0.7,                        free >=4.2 && <5.2,-                       lattices >=1.6 && <1.8,+                       lattices >=2 && <2.1,                        singletons >=2.2 && <2.6,                        text >=1.2 && <1.3,                        transformers >=0.5.2 && <0.6

@@ -58,9 +58,6 @@                        , QFALia                        , ALia -                       -- Algebraic view of languages-                       , ComplementedLattice(..)-                        -- Convenient type synonyms                        , VariableName @@ -124,6 +121,7 @@                        , Unstore                        , unstore ) where +import Algebra.Heyting import Algebra.Lattice import Control.Applicative hiding (Const) import Control.Comonad.Trans.Coiter@@ -191,31 +189,28 @@ -- | 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 Lattice (QFLogic 'BooleanSort) where+    a /\ b = a .&. b+    a \/ 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 (QFLia   'BooleanSort) where+    a /\ b = a .&. b+    a \/ b = a .|. b -instance Lattice (QFLogic 'BooleanSort)-instance Lattice (QFLia   'BooleanSort)-instance Lattice (  Lia   'BooleanSort)-instance Lattice (QFALia  'BooleanSort)-instance Lattice (  ALia  'BooleanSort)+instance Lattice (  Lia   'BooleanSort) where+    a /\ b = a .&. b+    a \/ b = a .|. b +instance Lattice (QFALia  'BooleanSort) where+    a /\ b = a .&. b+    a \/ b = a .|. b++instance Lattice (  ALia  'BooleanSort) where+    a /\ b = a .&. b+    a \/ b = a .|. b++ instance BoundedJoinSemiLattice (QFLogic 'BooleanSort) where bottom = false instance BoundedJoinSemiLattice (QFLia   'BooleanSort) where bottom = false instance BoundedJoinSemiLattice (  Lia   'BooleanSort) where bottom = false@@ -228,17 +223,21 @@ 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 Heyting (QFLogic 'BooleanSort) where+    a ==> b = nnf (not a \/ b) -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+instance Heyting (QFLia   'BooleanSort) where+    a ==> b = nnf (not a \/ b)++instance Heyting (  Lia   'BooleanSort) where+    a ==> b = nnf (not a \/ b)++instance Heyting (QFALia  'BooleanSort) where+    a ==> b = nnf (not a \/ b)++instance Heyting (  ALia  'BooleanSort) where+    a ==> b = nnf (not a \/ b)+  -- | Type of names assigned to variables type VariableName = String

@@ -117,8 +117,8 @@ 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) -type Array                   f (e :: Sort) (i :: Sort) = IFix f ('ArraySort i e)-type Index                   f (i :: Sort)             = IFix f i+type Array f (e :: Sort) (i :: Sort) = IFix f ('ArraySort i e)+type Index f (i :: Sort)             = IFix f i  newtype ArrayAccess             f (i :: Sort) (e :: Sort) = ArrayAccess             { getAA   :: (Array f e i, Index f i) }            deriving Show via (Array f e i, Index f i) newtype DynamicValueArrayAccess f (i :: Sort)             = DynamicValueArrayAccess { getDVAA :: DynamicallySorted (ArrayAccess f i) } deriving Show via (DynamicallySorted (ArrayAccess f i))