-- |
-- Module      :  $Header$
-- Copyright   :  (c) 2014-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
-- 
-- TODO:
--  - Putting in a normal form to spot "prove by assumption"
--  - Additional simplification rules, namely various cancelation.
--  - Things like:  lg2 e(x) = x, where we know thate is increasing.

{-# LANGUAGE Safe, PatternGuards, BangPatterns #-}
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}

module Cryptol.TypeCheck.Solver.Numeric.Simplify
  (
  -- * Simplify a property
  crySimplify, crySimplifyMaybe

  -- * Simplify expressions in a prop
  , crySimpPropExpr, crySimpPropExprMaybe
  ) where

import           Cryptol.TypeCheck.Solver.Numeric.AST
import           Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr
import           Cryptol.TypeCheck.Solver.InfNat(genLog,genRoot,rootExact)
import           Cryptol.Utils.Misc ( anyJust )

import           Control.Monad ( mplus )
import           Data.List ( sortBy )
import           Data.Maybe ( fromMaybe )
import qualified Data.Set as Set


-- | Simplify a property, if possible.
crySimplify :: Prop -> Prop
crySimplify p = fromMaybe p (crySimplifyMaybe p)

-- | Simplify a property, if possible.
crySimplifyMaybe :: Prop -> Maybe Prop
crySimplifyMaybe p =
  let mbSimpExprs = simpSubs p
      exprsSimped = fromMaybe p mbSimpExprs
      mbRearrange = tryRearrange exprsSimped
      rearranged  = fromMaybe exprsSimped mbRearrange
  in crySimplify `fmap` (crySimpStep rearranged `mplus` mbRearrange
                                                `mplus` mbSimpExprs)

  where
  tryRearrange q = case q of
                    _ :&& _ -> cryRearrangeAnd q
                    _ :|| _ -> cryRearrangeOr  q
                    _       -> Nothing

  simpSubs q = case q of
                Not a     -> Not `fmap` crySimplifyMaybe a
                a :&& b   -> do [a',b'] <- anyJust crySimplifyMaybe [a,b]
                                return (a' :&& b')
                a :|| b   -> do [a',b'] <- anyJust crySimplifyMaybe [a,b]
                                return (a' :|| b')
                _         -> crySimpPropExprMaybe q





-- | A single simplification step.
crySimpStep :: Prop -> Maybe Prop
crySimpStep prop =
  case prop of

    Fin x     -> cryIsFin x   -- Fin only on variables.

    x :== y   -> Just (cryIsEq x y)
    x :>  y   -> Just (cryIsGt x y)

    x :>= y   ->
      case (x,y) of
        -- XXX: DUPLICTION
        (K (Nat 0), _)       -> Just (y :== zero)
        (K (Nat a), Width b) -> Just (K (Nat (2 ^ a)) :>= b)

        (_,       K (Nat 0)) -> Just PTrue
        (Width e, K (Nat b)) -> Just (e :>= K (Nat (2^(b-1))))


        (K Inf, _)     -> Just PTrue
        (_, K Inf)     -> Just (x :== inf)
        _              -> Just (x :== inf :|| one :+ x :> y)

    x :==: y ->
      case (x,y) of
        (K a, K b)     -> Just (if a == b then PTrue else PFalse)
        (K (Nat n), _) | Just p <- cryIsNat True n y -> Just p
        (_, K (Nat n)) | Just p <- cryIsNat True n x -> Just p

        _ | x == y    -> Just PTrue
          | otherwise -> case (x,y) of
                           (Var _, _) -> Nothing
                           (_, Var _) -> Just (y :==: x)
                           _          -> Nothing

    x :>: y ->
      case (x,y) of
        (K (Nat n),_)  | Just p <- cryNatGt True n y -> Just p
        (_, K (Nat n)) | Just p <- cryGtNat True n x -> Just p

        _ | x == y      -> Just PFalse
          | otherwise   -> Nothing


    -- For :&& and :|| we assume that the props have been rearrnaged
    p :&& q -> cryAnd p q
    p :|| q -> cryOr p q

    Not p   -> cryNot p
    PFalse  -> Nothing
    PTrue   -> Nothing


-- | Rebalance parens, and arrange conjucts so that we can transfer
-- information left-to-right.
cryRearrangeAnd :: Prop -> Maybe Prop
cryRearrangeAnd prop =
  case rebalance prop of
    Just p  -> Just p
    Nothing -> cryAnds `fmap` cryRearrange cmpAnd (split prop)
  where
  rebalance (a :&& b) =
    case a of
      PFalse    -> Just PFalse
      PTrue     -> Just b
      a1 :&& a2 -> Just (a1 :&& (a2 :&& b))
      _         -> fmap (a :&&) (rebalance b)
  rebalance _ = Nothing

  split (a :&& b) = a : split b
  split a         = [a]


-- | Rebalance parens, and arrange disjuncts so that we can transfer
-- information left-to-right.
cryRearrangeOr :: Prop -> Maybe Prop
cryRearrangeOr prop =
  case rebalance prop of
    Just p  -> Just p
    Nothing -> cryOrs `fmap` cryRearrange cmpOr (split prop)
  where
  rebalance (a :|| b) =
    case a of
      PFalse    -> Just b
      PTrue     -> Just PTrue
      a1 :|| a2 -> Just (a1 :|| (a2 :|| b))
      _         -> fmap (a :||) (rebalance b)
  rebalance _ = Nothing

  split (a :|| b) = a : split b
  split a         = [a]




-- | Identify propositions that are suiatable for inlining.
cryIsDefn :: Prop -> Maybe (Name, Expr)
cryIsDefn (Var x :==: e) = if (x `Set.member` cryExprFVS e)
                              then Nothing
                              else Just (x,e)
cryIsDefn _              = Nothing





type PropOrdering = (Int,Prop) -> (Int,Prop) -> Ordering

{- | Rearrange proposition for conjuctions and disjunctions.

information left-to-right, so we put proposition with information content
on the left.
-}
cryRearrange :: PropOrdering -> [Prop] -> Maybe [Prop]
cryRearrange cmp ps = if ascending keys then Nothing else Just sortedProps
  where
  -- We tag each proposition with a number, so that later we can tell easily
  -- if the propositions got rearranged.
  (keys, sortedProps) = unzip (sortBy cmp (zip [ 0 :: Int .. ] ps))

  ascending (x : y : zs) = x < y && ascending (y : zs)
  ascending _            = True


cmpAnd :: PropOrdering
cmpAnd (k1,prop1) (k2,prop2) =
  case (prop1, prop2) of

    -- First comes PFalse, maybe we don't need to do anything
    (PFalse, PFalse) -> compare k1 k2
    (PFalse, _)      -> LT
    (_,PFalse)       -> GT

    -- Next comes PTrue
    (PTrue, PTrue)   -> compare k1 k2
    (PTrue, _)       -> LT
    (_,PTrue)        -> GT

    -- Next come `not (fin a)`  (i.e, a = inf)
    (Not (Fin (Var x)), Not (Fin (Var y))) -> cmpVars x y
    (Not (Fin (Var _)), _)                 -> LT
    (_, Not (Fin (Var _)))                 -> GT

    -- Next come defintions: `x = e` (with `x` not in `fvs e`)
    -- XXX: Inefficient, because we keep recomputing free variables
    -- (here, and then when actually applying the substitution)
    _ | Just (x,_) <- mbL
      , Just (y,_) <- mbR  -> cmpVars x y
      | Just _     <- mbL  -> LT
      | Just _     <- mbR  -> GT
      where
      mbL = cryIsDefn prop1
      mbR = cryIsDefn prop2

    -- Next come `fin a`
    (Fin (Var x), Fin (Var y)) -> cmpVars x y
    (Fin (Var _), _)           -> LT
    (_, Fin (Var _))           -> GT

    -- Everything else stays as is
    _ -> compare k1 k2

  where
  cmpVars x y
    | x < y     = LT
    | x > y     = GT
    | otherwise = compare k1 k2


cmpOr :: PropOrdering
cmpOr (k1,prop1) (k2,prop2) =
  case (prop1, prop2) of

    -- First comes PTrue, maybe we don't need to do anything
    (PTrue, PTrue)   -> compare k1 k2
    (PTrue, _)       -> LT
    (_,PTrue)        -> GT

    -- Next comes PFalse
    (PFalse, PFalse) -> compare k1 k2
    (PFalse, _)      -> LT
    (_,PFalse)       -> GT

    -- Next comes `fin a` (because we propagete `a = inf`)
    (Fin (Var x), Fin (Var y)) -> cmpVars x y
    (Fin (Var _), _)           -> LT
    (_, Fin (Var _))           -> GT

    -- Next come `not (fin a)`  (i.e, propagete (fin a))
    (Not (Fin (Var x)), Not (Fin (Var y))) -> cmpVars x y
    (Not (Fin (Var _)), _)                 -> LT
    (_, Not (Fin (Var _)))                 -> GT

    -- we don't propagete (x /= e) for now.

    -- Everything else stays as is
    _ -> compare k1 k2

  where
  cmpVars x y
    | x < y     = LT
    | x > y     = GT
    | otherwise = compare k1 k2





-- | Simplification of ':&&'.
-- Assumes arranged conjucntions.
-- See 'cryRearrangeAnd'.
cryAnd :: Prop -> Prop -> Maybe Prop
cryAnd p q =
  case p of
    PTrue       -> Just q

    PFalse      -> Just PFalse

    Not (Fin (Var x))
      | Just q' <- cryKnownFin x False q -> Just (p :&& q')

    Fin (Var x)
      | Just q' <- cryKnownFin x True q -> Just (p :&& q')

    _ | Just (x,e) <- cryIsDefn p
      , Just q'    <- cryLet x e q
      -> Just (p :&& q')

    _ -> Nothing


-- | Simplification of ':||'.
-- Assumes arranged disjunctions.
-- See 'cryRearrangeOr'
cryOr :: Prop -> Prop -> Maybe Prop
cryOr p q =
  case p of
    PTrue     -> Just PTrue

    PFalse    -> Just q

    Fin (Var x)
      | Just q' <- cryKnownFin x False q -> Just (p :|| q')

    Not (Fin (Var x))
      | Just q' <- cryKnownFin x True q -> Just (p :|| q')

    _ -> Nothing



-- | Propagate the fact that the variable is known to be finite ('True')
-- or not-finite ('False').
-- Note that this may introduce new expression redexes.
cryKnownFin :: Name -> Bool -> Prop -> Maybe Prop
cryKnownFin a isFin prop =
  case prop of
    Fin (Var a') | a == a' -> Just (if isFin then PTrue else PFalse)

    p :&& q -> do [p',q'] <- anyJust (cryKnownFin a isFin) [p,q]
                  return (p' :&& q')

    p :|| q -> do [p',q'] <- anyJust (cryKnownFin a isFin) [p,q]
                  return (p' :|| q')

    Not p   -> Not `fmap` cryKnownFin a isFin p

    x :==: y
      | not isFin, Just [x',y'] <- anyJust (cryLet a inf) [x,y]
      -> Just (cryNatOp (:==:) x' y')

    x :>: y
      | not isFin, Just [x',y'] <- anyJust (cryLet a inf) [x,y]
      -> Just (cryNatOp (:>:) x' y')

    -- All the other cases should be simplified, eventually.
    _       -> Nothing




-- | Negation.
cryNot :: Prop -> Maybe Prop
cryNot prop =
  case prop of
    Fin _           -> Nothing

    x :== y         -> Just (x :> y :|| y :> x)
    x :>= y         -> Just (y :>  x)
    x :>  y         -> Just (y :>= x)

    x :==: y        -> Just (x :>: y :|| y :>: x)

    _ :>: _         -> Nothing

    p :&& q         -> Just (Not p :|| Not q)
    p :|| q         -> Just (Not p :&& Not q)
    Not p           -> Just p
    PFalse          -> Just PTrue
    PTrue           -> Just PFalse



-- | Simplificaiton for @:==@
cryIsEq :: Expr -> Expr -> Prop
cryIsEq l r =
  case (l,r) of
    (K m, K n)      -> if m == n then PTrue else PFalse

    (K Inf, _)      -> Not (Fin r)
    (_, K Inf)      -> Not (Fin l)

    (Div x y, z)    -> x :>= z :* y :&& (one :+ z) :* y :> x

    (K (Nat n),_) | Just p <- cryIsNat False n r -> p
    (_,K (Nat n)) | Just p <- cryIsNat False n l -> p

    _               -> Not (Fin l) :&& Not (Fin r)
                   :|| Fin l :&& Fin r :&& cryNatOp (:==:) l r




-- | Simplificatoin for @:>@
cryIsGt :: Expr -> Expr -> Prop
cryIsGt (K m) (K n)   = if m > n then PTrue else PFalse
cryIsGt (K (Nat n)) e | Just p <- cryNatGt False n e = p
cryIsGt e (K (Nat n)) | Just p <- cryGtNat False n e = p

cryIsGt x y           = Fin y :&& (x :== inf :||
                                   Fin x :&& cryNatOp (:>:) x y)



-- | Attempt to simplify a @fin@ constraint.
-- Assumes a defined input.
cryIsFin :: Expr -> Maybe Prop
cryIsFin expr =
  case expr of
    K Inf                -> Just PFalse
    K (Nat _)            -> Just PTrue
    Var _                -> Nothing
    t1 :+ t2             -> Just (Fin t1 :&& Fin t2)
    t1 :- _              -> Just (Fin t1)

    t1 :* t2             -> Just ( Fin t1 :&& Fin t2
                               :|| t1 :== zero :&& t2 :== inf
                               :|| t2 :== zero :&& t1 :== inf
                                 )

    Div t1 _             -> Just (Fin t1)
    Mod _ _              -> Just PTrue

    t1 :^^ t2            ->
      Just ( Fin t1 :&& Fin t2
         :|| t1 :== inf :&& t2 :== zero   -- inf ^^ 0
         :|| t2 :== inf :&& (t1 :== zero :|| t1 :== one)
                             -- 0 ^^ inf,    1 ^^ inf
           )

    Min t1 t2            -> Just (Fin t1 :|| Fin t2)
    Max t1 t2            -> Just (Fin t1 :&& Fin t2)
    Width t1             -> Just (Fin t1)
    LenFromThen  _ _ _   -> Just PTrue
    LenFromThenTo  _ _ _ -> Just PTrue


cryIsNat :: Bool -> Integer -> Expr -> Maybe Prop
cryIsNat useFinite n expr =
  case expr of
    K Inf     -> Just PFalse

    K (Nat m) -> Just (if m == n then PTrue else PFalse)

    Var _ | useFinite   -> Nothing
          | otherwise   -> Just (Fin expr :&& expr :==: K (Nat n))

    K (Nat m) :+ e2     -> Just $ if m > n then PFalse
                                           else eq e2 $ K $ Nat $ n - m

    x :+ y
      | n == 0          -> Just (eq x zero :&& eq y zero)
      | n == 1          -> Just (eq x zero :&& eq y one :||
                                 eq x one  :&& eq y zero)
      | otherwise       -> Nothing

    e1 :- e2            -> Just $ eq (K (Nat n) :+ e1) e2

    K (Nat m) :* e2     ->
      Just $ if m == 0
                then if n == 0 then PTrue else PFalse
                else case divMod n m of
                       (q,r) -> if r == 0 then eq e2 (K (Nat q))
                                          else PFalse
    e1 :* e2
      | n == 0          -> Just (eq e1 zero :|| eq e2 zero)
      | n == 1          -> Just (eq e1 one :&& eq e2 one)
      | otherwise       -> Nothing

    -- (x >= n * y) /\ ((n+1) * y > x)
    Div x y             -> Just (gt (one :+ x) (K (Nat n) :* y) :&&
                                 gt (K (Nat (n + 1)) :* y) x)

    Mod _ _ | useFinite -> Nothing
            | otherwise -> Just (cryNatOp (:==:) expr (K (Nat n)))


    K (Nat m) :^^ y     -> Just $ case genLog n m of
                                    Just (a, exact)
                                      | exact -> eq y (K (Nat a))
                                    _ -> PFalse
    x :^^ K (Nat m)     -> Just $ case rootExact n m of
                                    Just a  -> eq x (K (Nat a))
                                    Nothing -> PFalse
    x :^^ y
      | n == 0          -> Just (eq x zero :&& gt y zero)
      | n == 1          -> Just (eq x one  :|| eq y zero)
      | otherwise       -> Nothing

    Min x y
      | n == 0          -> Just (eq x zero :|| eq y zero)
      | otherwise       -> Just ( eq x (K (Nat n)) :&& gt y (K (Nat (n - 1)))
                              :|| eq y (K (Nat n)) :&& gt x (K (Nat (n - 1)))
                                )

    Max x y             -> Just ( eq x (K (Nat n)) :&& gt (K (Nat (n + 1))) y
                              :|| eq y (K (Nat n)) :&& gt (K (Nat (n + 1))) y
                                )

    Width x
      | n == 0          -> Just (eq x zero)
      | otherwise       -> Just (gt x (K (Nat (2^(n-1) - 1))) :&&
                                 gt (K (Nat (2 ^ n))) x)

    LenFromThen x y w
      | n == 0          -> Just PFalse

      -- See Note [Sequences of Length 1] in 'Cryptol.TypeCheck.Solver.InfNat'
      | n == 1          -> Just (gt y x :&& gt (y :+ one) (two :^^ w))
      | otherwise       -> Nothing -- XXX: maybe some more?


    -- See `nLenFromThenTo` in 'Cryptol.TypeCheck.Solver.InfNat'
    LenFromThenTo x y z
      | n == 0          -> Just ( gt x y :&& gt z x
                              :|| gt y x :&& gt x z
                                )

      -- See Note [Sequences of Length 1] in 'Cryptol.TypeCheck.Solver.InfNat'
      | n == 1          -> Just (gt z y :&& gt (x :+ one) z     :||
                                 gt y z :&& gt (z :+ one) x)
      | otherwise       -> Nothing -- XXX: maybe some more?


  where
  eq x y = if useFinite then x :==: y else x :== y
  gt x y = if useFinite then x :>: y  else x :>  y

-- | Constant > expression
cryNatGt :: Bool -> Integer -> Expr -> Maybe Prop
cryNatGt useFinite n expr
  | n == 0    = Just PFalse
  | n == 1    = Just (eq expr zero)
  | otherwise =
    case expr of
      K x   -> Just $ if Nat n > x then PTrue else PFalse

      Var _ -> Nothing

      K (Nat m) :+ y -> Just $ if n >= m then gt (k (n - m)) y else PFalse
      _ :+ _         -> Nothing

      x :- y         -> Just $ gt (k n :+ y) x

      K (Nat m) :* y
        | m == 0    -> Just PTrue   -- because we know that n > 1
        | otherwise -> Just $ case divMod n m of
                                (q,0) -> gt (k q) y
                                (0,_) -> eq y zero
                                (q,_) -> gt (k (q + 1)) y
      _ :* _          -> Nothing

      Div x y         -> Just $ gt (k n :* y) x

      Mod _ (K (Nat m))
        | m <= n      -> Just PTrue

      Mod (K (Nat m)) _
        | m < n       -> Just PTrue
      Mod _ _         -> Nothing


      K (Nat m) :^^ y
        | m == 0      -> Just PTrue   -- because n > 1
        | m == 1      -> Just PTrue   -- ditto
        | otherwise   -> do (a,exact) <- genLog n m
                            return $ if exact
                                        then gt (k a) y
                                        else gt (k (a + 1)) y
      x :^^ K (Nat m)
        | m == 0      -> Just PTrue
        | m == 1      -> Just (gt (k n) x)
        | otherwise   -> do (a,exact) <- genRoot n m
                            return $ if exact
                                        then gt (k a) x
                                        else gt (k (a + 1)) x
      _ :^^ _         -> Nothing

      Min x y         -> Just $ gt (k n) x :|| gt (k n) y
      Max x y         -> Just $ gt (k n) x :&& gt (k n) y

      Width x         -> Just $ gt (k (2 ^ n)) x

      LenFromThen _ _ _   -> Nothing -- Are there some rules?

      LenFromThenTo _ _ _ -> Nothing -- Are there some rulesj

  where
  k x    = K (Nat x)
  eq x y = if useFinite then x :==: y else x :== y
  gt x y = if useFinite then x :>: y  else x :>  y



-- | Expression > constant
cryGtNat :: Bool -> Integer -> Expr -> Maybe Prop
cryGtNat useFinite n expr =
  case expr of
    K x                 -> Just $ if x > Nat n then PTrue else PFalse
    Var _               -> Nothing

    K (Nat m) :+ y
      | m > n           -> Just PTrue
      | otherwise       -> Just (gt y (K (Nat (n - m))))

    x :+ y
      | n == 0          -> Just (gt x zero :|| gt y zero)
      | otherwise       -> Nothing

    x :- y              -> Just $ gt x (K (Nat n) :+ y)


    K (Nat m) :* y
      | m > 0           -> Just $ case divMod n m of
                                    (a,_) -> gt y $ K $ Nat a

    x :* y
      | n == 0          -> Just (gt x zero :&& gt y zero)
      | otherwise       -> Nothing

    Div x y             -> Just $ gt (one :+ x) (K (Nat (n+1)) :* y)

    Mod _ (K (Nat m))
      | m <= n          -> Just PFalse
    Mod (K (Nat m)) _
      | m < n           -> Just PFalse
    Mod _ _             -> Nothing

    K (Nat m) :^^ y
      | m == 0          -> Just $ if n == 0 then eq y zero else PFalse
      | m == 1          -> Just $ if n == 0 then PTrue else PFalse
      | otherwise       -> do (a,_exact) <- genLog n m
                              Just (gt y (K (Nat a)))

    x :^^ K (Nat m)
      | m == 0          -> Just $ if n == 0 then PTrue else PFalse
      | m == 1          -> Just $ gt x (K (Nat n))
      | otherwise       -> do (a,exact) <- genRoot n m
                              Just $ if exact
                                        then gt x (K (Nat a))
                                        else gt (one :+ x) (K (Nat (a+1)))

    x :^^ y
      | n == 0          -> Just (gt x zero :|| eq y zero)
      | otherwise       -> Nothing

    Min x y             -> Just $ gt x (K (Nat n)) :&& gt y (K (Nat n))
    Max x y             -> Just $ gt x (K (Nat n)) :|| gt y (K (Nat n))

    Width x             -> Just $ gt (one :+ x) (K (Nat (2 ^ n)))

    LenFromThen _ _ _
      | n == 0          -> Just PTrue
      | otherwise       -> Nothing -- Are there some rules?

    LenFromThenTo x y z
      | n == 0          -> Just (gt x y :&& gt z x :|| gt y x :&& gt x z)
      | otherwise       -> Nothing

  where
  eq x y = if useFinite then x :==: y else x :== y
  gt x y = if useFinite then x :>: y  else x :>  y



-- | Simplify only the Expr parts of a Prop.
crySimpPropExpr :: Prop -> Prop
crySimpPropExpr p = fromMaybe p (crySimpPropExprMaybe p)

-- | Simplify only the Expr parts of a Prop.
-- Returns `Nothing` if there were no changes.
crySimpPropExprMaybe  :: Prop -> Maybe Prop
crySimpPropExprMaybe prop =
  case prop of

    Fin e                 -> Fin `fmap` crySimpExprMaybe e

    a :==  b              -> binop crySimpExprMaybe (:== ) a b
    a :>=  b              -> binop crySimpExprMaybe (:>= ) a b
    a :>   b              -> binop crySimpExprMaybe (:>  ) a b
    a :==: b              -> binop crySimpExprMaybe (:==:) a b
    a :>:  b              -> binop crySimpExprMaybe (:>: ) a b

    a :&& b               -> binop crySimpPropExprMaybe (:&&) a b
    a :|| b               -> binop crySimpPropExprMaybe (:||) a b

    Not p                 -> Not `fmap` crySimpPropExprMaybe p

    PFalse                -> Nothing
    PTrue                 -> Nothing

  where

  binop simp f l r =
    case (simp l, simp r) of
      (Nothing,Nothing) -> Nothing
      (l',r')           -> Just (f (fromMaybe l l') (fromMaybe r r'))






-- | Our goal is to bubble @inf@ terms to the top of @Return@.
cryNoInf :: Expr -> IfExpr Expr
cryNoInf expr =
  case expr of

    -- These are the interesting cases where we have to branch

    x :* y ->
      do x' <- cryNoInf x
         y' <- cryNoInf y
         case (x', y') of
           (K Inf, K Inf) -> return inf
           (K Inf, _)     -> mkIf (y' :==: zero) (return zero) (return inf)
           (_, K Inf)     -> mkIf (x' :==: zero) (return zero) (return inf)
           _              -> return (x' :* y')

    x :^^ y ->
      do x' <- cryNoInf x
         y' <- cryNoInf y
         case (x', y') of
           (K Inf, K Inf) -> return inf
           (K Inf, _)     -> mkIf (y' :==: zero) (return one) (return inf)
           (_, K Inf)     -> mkIf (x' :==: zero) (return zero)
                           $ mkIf (x' :==: one)  (return one)
                           $ return inf
           _              -> return (x' :^^ y')



    -- The rest just propagates

    K _     -> return expr
    Var _   -> return expr

    x :+ y  ->
      do x' <- cryNoInf x
         y' <- cryNoInf y
         case (x', y') of
           (K Inf, _)  -> return inf
           (_, K Inf)  -> return inf
           _           -> return (x' :+ y')

    x :- y  ->
      do x' <- cryNoInf x
         y' <- cryNoInf y
         case (x', y') of
           (_, K Inf)  -> Impossible
           (K Inf, _)  -> return inf
           _           -> mkIf (x' :==: y)
                               (return zero)
                               (mkIf (x' :>: y) (return (x' :- y'))
                                                Impossible)

    Div x y ->
      do x' <- cryNoInf x
         y' <- cryNoInf y
         case (x', y') of
           (K Inf, _) -> Impossible
           (_, K Inf) -> return zero
           _          -> mkIf (y' :>: zero) (return (Div x' y')) Impossible

    Mod x y ->
      do x' <- cryNoInf x
         -- `Mod x y` is finite, even if `y` is `inf`, so first check
         -- for finiteness.
         mkIf (Fin y)
              (do y' <- cryNoInf y
                  case (x',y') of
                    (K Inf, _) -> Impossible
                    (_, K Inf) -> Impossible
                    _ -> mkIf (y' :>: zero) (return (Mod x' y')) Impossible
              )
              (return x')

    Min x y ->
      do x' <- cryNoInf x
         y' <- cryNoInf y
         case (x',y') of
           (K Inf, _) -> return y'
           (_, K Inf) -> return x'
           _          -> return (Min x' y')

    Max x y ->
      do x' <- cryNoInf x
         y' <- cryNoInf y
         case (x', y') of
           (K Inf, _) -> return inf
           (_, K Inf) -> return inf
           _          -> return (Max x' y')

    Width x ->
      do x' <- cryNoInf x
         case x' of
           K Inf      -> return inf
           _          -> return (Width x')

    LenFromThen x y w   -> fun3 LenFromThen x y w
    LenFromThenTo x y z -> fun3 LenFromThenTo x y z


  where
  fun3 f x y z =
    do x' <- cryNoInf x
       y' <- cryNoInf y
       z' <- cryNoInf z
       case (x',y',z') of
         (K Inf, _, _) -> Impossible
         (_, K Inf, _) -> Impossible
         (_, _, K Inf) -> Impossible
         _             -> mkIf (x' :==: y') Impossible
                                            (return (f x' y' z'))

  mkIf p t e = case crySimplify p of
                 PTrue  -> t
                 PFalse -> e
                 p'     -> If p' t e




-- | Make an expression that should work ONLY on natural nubers.
-- Eliminates occurances of @inf@.
-- Assumes that the two input expressions are well-formed and finite.
-- The expression is constructed by the given function.
cryNatOp :: (Expr -> Expr -> Prop) -> Expr -> Expr -> Prop
cryNatOp op x y =
  toProp $
  do x' <- noInf x
     y' <- noInf y
     return (op x' y')
  where
  noInf a = do a' <- cryNoInf a
               case a' of
                 K Inf -> Impossible
                 _     -> return a'

  toProp ite =
    case ite of
      Impossible -> PFalse -- It doesn't matter, but @false@ might anihilate.
      Return p   -> p
      If p t e   -> p :&& toProp t :|| Not p :&& toProp e