1 | module Fake where |
---|

2 | |
---|

3 | Poly { noOfVars = n1 } `subset` Poly { noOfVars = n2 } = n1 == n2 |
---|

4 | |
---|

5 | -- | Variable type used to identify dimensions in the polyhedron. |
---|

6 | type DomVar = Int |
---|

7 | |
---|

8 | -- | A constraint is a data type that represents an equality or an |
---|

9 | -- inequality, depending on the context. The semantics of a set of |
---|

10 | -- terms ts and the constant c is that ts <= c holds. The list |
---|

11 | -- of terms is sorted. |
---|

12 | -- |
---|

13 | data Constraint = Constraint { |
---|

14 | terms :: Terms, |
---|

15 | coeff ::Integer |
---|

16 | } deriving Eq |
---|

17 | |
---|

18 | -- | A set of 'Terms' is an ordered list of 'Term's. This |
---|

19 | -- sequence has no zero coefficients and no duplicates. |
---|

20 | newtype Terms = Terms [Term] deriving Eq |
---|

21 | |
---|

22 | -- | A term is a coefficient, variable pair. |
---|

23 | type Term = (Integer, DomVar) |
---|

24 | |
---|

25 | -- | A system of constraints. |
---|

26 | data ConSys = ConSys { |
---|

27 | csEquals :: [Constraint], |
---|

28 | csIneqs :: [Constraint] |
---|

29 | } |
---|

30 | |
---|

31 | -- | A polyhedron represented as a constraint system. |
---|

32 | data Poly = |
---|

33 | Bottom | |
---|

34 | Poly { |
---|

35 | noOfVars :: Int, |
---|

36 | conSys :: ConSys |
---|

37 | } |
---|

38 | |
---|

39 | -- | The full @n@-dimensional state space. |
---|

40 | top :: Int -> Poly |
---|

41 | top n = Poly { noOfVars = n, conSys = ConSys [] [] } |
---|

42 | |
---|

43 | -- | The empty state space. |
---|

44 | bottom :: Poly |
---|

45 | bottom = Bottom |
---|

46 | |
---|

47 | -- | Intersect with a set of inequalities. |
---|

48 | meetAsym :: [Constraint] -> Poly -> Poly |
---|

49 | meetAsym _ Bottom = Bottom |
---|

50 | meetAsym [_] s = s |
---|

51 | meetAsym _ s = Bottom |
---|

52 | |
---|

53 | -- | Calculate the join of two polyhedra. |
---|

54 | join :: Poly -> Poly -> Poly |
---|

55 | join Bottom p = p |
---|

56 | join p Bottom = p |
---|

57 | |
---|

58 | -- | Shorthand for setting a variable to a constant. |
---|

59 | set :: DomVar -> Integer -> Poly -> Poly |
---|

60 | set v rhs p = p |
---|

61 | |
---|