module Fake where
Poly { noOfVars = n1 } `subset` Poly { noOfVars = n2 } = n1 == n2
-- | Variable type used to identify dimensions in the polyhedron.
type DomVar = Int
-- | A constraint is a data type that represents an equality or an
-- inequality, depending on the context. The semantics of a set of
-- terms ts and the constant c is that ts <= c holds. The list
-- of terms is sorted.
--
data Constraint = Constraint {
terms :: Terms,
coeff ::Integer
} deriving Eq
-- | A set of 'Terms' is an ordered list of 'Term's. This
-- sequence has no zero coefficients and no duplicates.
newtype Terms = Terms [Term] deriving Eq
-- | A term is a coefficient, variable pair.
type Term = (Integer, DomVar)
-- | A system of constraints.
data ConSys = ConSys {
csEquals :: [Constraint],
csIneqs :: [Constraint]
}
-- | A polyhedron represented as a constraint system.
data Poly =
Bottom |
Poly {
noOfVars :: Int,
conSys :: ConSys
}
-- | The full @n@-dimensional state space.
top :: Int -> Poly
top n = Poly { noOfVars = n, conSys = ConSys [] [] }
-- | The empty state space.
bottom :: Poly
bottom = Bottom
-- | Intersect with a set of inequalities.
meetAsym :: [Constraint] -> Poly -> Poly
meetAsym _ Bottom = Bottom
meetAsym [_] s = s
meetAsym _ s = Bottom
-- | Calculate the join of two polyhedra.
join :: Poly -> Poly -> Poly
join Bottom p = p
join p Bottom = p
-- | Shorthand for setting a variable to a constant.
set :: DomVar -> Integer -> Poly -> Poly
set v rhs p = p