# bblum/atomic-all-nighters

Switch branches/tags
Nothing to show
Fetching contributors…
Cannot retrieve contributors at this time
64 lines (51 sloc) 1.98 KB
 -- Constraint definition and solving. -- Author: Ben Blum module Constraints where import Data.List (intercalate) import qualified Rules as R -- Identifiers for symbolic (i.e., unsolved) function rules and effects. data RV = RV Int String data EV = EV Int String type Unknown = (RV,EV) instance Eq RV where (RV a _) == (RV b _) = a == b instance Eq EV where (EV a _) == (EV b _) = a == b -- instance Ord RV where -- in case I need to put them in maps, I guess? -- (RV a _) <= (RV b _) = a <= b -- instance Ord EV where -- (EV a _) <= (EV b _) = a <= b instance Show RV where show (RV _ name) = "R{" ++ name ++ "}" instance Show EV where show (EV _ name) = "E{" ++ name ++ "}" -- The elements of constraint expressions. Can be variables or fixed constants. data R = RuleVar RV | RuleConst R.Rule deriving Eq data E = EffectVar EV | EffectConst R.Effect deriving Eq instance Show R where show (RuleVar rv) = show rv show (RuleConst rule) = show rule instance Show E where show (EffectVar ev) = show ev show (EffectConst effect) = show effect -- Note: the "<=" in the rule constraint is the subtyping comparison, not -- the numeric comparison, so it's reversed (e.g., infinity <= 0). data Constraint = EffectConstraint E [E] -- e = e1 + e2 + ... en | RuleConstraint R R [E] -- r <= r1 + e1 + e2 + ... en | InvariantConstraint R R -- r == r1; in fnptr assignment deriving Eq instance Show Constraint where show (EffectConstraint e es) = show e ++ " = " ++ (intercalate " + " \$ map show es) show (RuleConstraint r r1 []) = show r ++ " <= " ++ show r1 show (RuleConstraint r r1 es) = show r ++ " <= " ++ show r1 ++ " + " ++ (intercalate " + " \$ map show es) show (InvariantConstraint r r1) = show r ++ " = " ++ show r1 -- -- Constaint processing. -- -- Constant folding. cfold :: Constraint -> Either (Maybe Constraint) (Constraint) cfold x = Left \$ Just x