source: sizechecking/NC.hs @ 10

{- Constraints -}
newtype Term = Term [String]
    deriving (Show, Eq, Ord)
nullterm = Term []
newtype Arithmetics = Arithmetics (Map Term Int)
    deriving (Show, Eq)

termmul (Term a) (Term b) = Term $ termmul' a b
    where
    termmul' []        l         = l
    termmul' l         []        = l
    termmul' l1@(x:xs) l2@(y:ys) = if x<y then x:termmul' xs l2
                                          else y:termmul' l1 ys

instance Num Arithmetics where
    fromInteger l = Arithmetics $ singleton nullterm $ fromInteger l
    (Arithmetics a) + (Arithmetics b) = Arithmetics $ unionWith (+) a b
    (Arithmetics a) * (Arithmetics b) = Arithmetics amul
        where
        amul = foldrWithKey tmul empty a
        tmul :: Term -> Int -> Map Term Int -> Map Term Int
        tmul t1 v1 val = unionWith (+) val (mapKeys (termmul t1) $ M.map (*v1) b)
    abs = undefined
    signum = undefined

data Condition = ZC Arithmetics | LTC Arithmetics Arithmetics | GEC Arithmetics Arithmetics
    deriving (Show)