module Data.Integer.Presburger.Prop
  ( module Data.Integer.Presburger.Prop
  , module X
  ) where

import Data.Integer.Presburger.Term as X

-- | Possibly negated propositions.
-- For example, we would express "t1 not equal to t2" like this:
-- @Prop { negated = True, prop = Bin Equal t1 t2 }@
data Prop p   = Prop { negated :: !Bool, prop :: !p }

-- | A proposition normalized with respect to a particular variable.
data NormProp p = Ind (Prop PosP)   -- ^ Independent of variable.
                | Norm (Prop p)     -- ^ Depends on variable.

-- | Basic binary relations.
data RelOp    = Equal | LessThan | LessThanEqual deriving Eq

-- | Basic propositions.
data PosP     = Bin !RelOp Term Term | Divides !Integer Term | FF

-- | Propositions specialized to say something about a particular variable.
data VarP     = NBin !RelOp Term        -- ^ x `op` t
              | NDivides !Integer Term  -- ^ n | x + t

-- | Propositions specialized for a variable with a coefficient.
-- For example: 4 * x = t
-- @CVarP { coeff = 4, pprop = NBin Equal t }@
data CVarP    = CVarP { coeff :: !Integer, pprop :: !VarP }


-- | Rewrite a propositions as a predicate about a specific variable.
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   -- t1 = k1 * x + t1'
          (k2,t2')  = split_term x t2   -- t2 = k2 * x + t2'

          (neg',op') = case op of
                         Equal         -> (negated p, Equal)
                         LessThan      -> (not (negated p), LessThanEqual)
                         LessThanEqual -> (not (negated p), LessThan)
 
    -- a < t        --> same
    -- Not (a < t)  --> same
    -- t < a        --> Not (a =< t)
    -- Not (t < a)  --> a =< t


  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     -- t1 = k1 * x + t1'

  FF -> Ind p


-- | Eliminate variable coefficients by scaling the properties appropriately.
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)
       }


-- | Evaluate a proposition for a sufficiently small value of
-- the variable, if possible.  Otherwise, substitute the given term.
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) }

-- | Evaluate a proposition for a sufficiently large value of
-- the variable, if possible.  Otherwise, substitute the given term.
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 }


-- | Evaluate a proposition with a given term for the variable.
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) }


--------------------------------------------------------------------------------

-- | The meanings of atomic propositions
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

-- | Replace a variable with a constant, in a property.
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