module Data.Integer.Presburger.Prop
( module Data.Integer.Presburger.Prop
, module X
) where
import Data.Integer.Presburger.Term as X
data Prop p = Prop { negated :: !Bool, prop :: !p }
data NormProp p = Ind (Prop PosP)
| Norm (Prop p)
data RelOp = Equal | LessThan | LessThanEqual deriving Eq
data PosP = Bin !RelOp Term Term | Divides !Integer Term | FF
data VarP = NBin !RelOp Term
| NDivides !Integer Term
data CVarP = CVarP { coeff :: !Integer, pprop :: !VarP }
norm :: Name -> Prop PosP -> NormProp CVarP
norm x p = case prop p of
Bin op t1 t2
| k1 == k2 -> Ind p { prop = Bin op t1' t2' }
| k1 > k2 -> Norm p { prop = CVarP (k1 k2) (NBin op (t2' t1')) }
| otherwise -> Norm Prop { prop = CVarP (k2 k1) (NBin op' (t1' t2'))
, negated = neg'
}
where (k1,t1') = split_term x t1
(k2,t2') = split_term x t2
(neg',op') = case op of
Equal -> (negated p, Equal)
LessThan -> (not (negated p), LessThanEqual)
LessThanEqual -> (not (negated p), LessThan)
Divides n t1
| k1 == 0 -> Ind p
| k1 > 0 -> Norm p { prop = CVarP k1 (NDivides n t1') }
| otherwise -> Norm p { prop = CVarP (negate k1) (NDivides n (negate t1'))}
where(k1,t1') = split_term x t1
FF -> Ind p
scale :: Integer -> Prop CVarP -> Prop VarP
scale k p =
let np = prop p
sc = k `div` coeff np
in p { prop = case pprop np of
NBin op t -> NBin op (sc .* t)
NDivides n t -> NDivides (sc * n) (sc .* t)
}
neg_inf :: Term -> Prop VarP -> Prop PosP
neg_inf t p = case prop p of
NBin Equal _ -> Prop { negated = negated p, prop = FF }
NBin _ _ -> Prop { negated = not (negated p), prop = FF }
NDivides n t1 -> p { prop = Divides n (t + t1) }
pos_inf :: Term -> Prop VarP -> Prop PosP
pos_inf t p = case prop p of
NDivides n t1 -> p { prop = Divides n (t + t1) }
_ -> Prop { negated = negated p, prop = FF }
normal :: Term -> Prop VarP -> Prop PosP
normal t p = case prop p of
NBin op t1 -> p { prop = Bin op t t1 }
NDivides n t1 -> p { prop = Divides n (t + t1) }
eval_prop :: Prop PosP -> Env -> Bool
eval_prop (Prop neg p) env = if neg then not res else res
where res = case p of
FF -> False
Divides n t -> divides n (eval_term t env)
Bin op t1 t2 -> bin_op op (eval_term t1 env) (eval_term t2 env)
bin_op :: RelOp -> Integer -> Integer -> Bool
bin_op op x y = case op of
Equal -> x == y
LessThan -> x < y
LessThanEqual -> x <= y
subst_prop :: Name -> Integer -> Prop PosP -> Prop PosP
subst_prop x n (Prop b p) =
case p of
Bin op t1 t2 -> Prop b (Bin op (subst_term x n t1) (subst_term x n t2))
Divides k t -> Prop b (Divides k (subst_term x n t))
FF -> Prop b FF
simplify_prop :: Prop PosP -> Prop PosP
simplify_prop it@(Prop b p) =
case p of
Divides n t -> case is_constant t of
Just v -> Prop (b /= divides n v) FF
Nothing -> it
Bin Equal t1 t2 | not b && t1 == t2 -> Prop True FF
Bin op t1 t2 -> case (is_constant t1, is_constant t2) of
(Just v1, Just v2) -> Prop (b /= bin_op op v1 v2) FF
_ -> it
FF -> it
class SignPP t where
pp_neg :: Bool -> t -> Doc
instance SignPP RelOp where
pp_neg False r = case r of
Equal -> text "=="
LessThan -> text "<"
LessThanEqual -> text "<="
pp_neg True r = case r of
Equal -> text "/="
LessThan -> text ">="
LessThanEqual -> text ">"
pp_neg_div :: Bool -> Doc
pp_neg_div False = text "|"
pp_neg_div True = text "/|"
instance SignPP PosP where
pp_neg n (Bin op t1 t2) = pp t1 <+> pp_neg n op <+> pp t2
pp_neg n (Divides d t) = text (show d) <+> pp_neg_div n <+> pp t
pp_neg n FF = text (if n then "True" else "False")
instance SignPP VarP where
pp_neg n (NBin op t) = text "_" <+> pp_neg n op <+> pp t
pp_neg n (NDivides d t) = text (show d) <+> pp_neg_div n
<+> text "_ +" <+> pp t
instance SignPP CVarP where
pp_neg n p = case pprop p of
NBin op t -> it <+> pp_neg n op <+> pp t
NDivides d t -> text (show d) <+> pp_neg_div n
<+> it <+> text "+" <+> pp t
where it | c == 1 = text "_"
| c == (1) = text "- _"
| otherwise = text (show c) <+> text "* _"
c = coeff p
instance SignPP p => PP (Prop p) where
pp p = pp_neg (negated p) (prop p)
instance SignPP p => PP (NormProp p) where
pp (Ind p) = pp p
pp (Norm p) = pp p