    -- |
    -- Module      :  $Header$
    -- Copyright   :  (c) 2014-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE Safe #-}
    module Cryptol.TypeCheck.Solver.Numeric.Defined where

    import Cryptol.TypeCheck.Solver.Numeric.AST
    import Cryptol.Utils.Panic ( panic )

    -- | A condition ensure that the given *basic* proposition makes sense.
    cryDefinedProp :: Prop -> Prop
    cryDefinedProp prop =
      case prop of
        Fin x   -> cryDefined x
        x :== y -> cryDefined x :&& cryDefined y
        x :>= y -> cryDefined x :&& cryDefined y
        Not p   -> cryDefinedProp p
        _ -> panic "cryDefinedProp" [ "Not a simple property:"
                                    , show (ppProp prop)
                                    ]

    -- | Generate a property ensuring that the expression is well-defined.
    -- This might be a bit too strict.  For example, we reject things like
    -- @max inf (0 - 1)@, which one might think would simplify to @inf@.
    cryDefined :: Expr -> Prop
    cryDefined expr =
      case expr of
        K _       -> PTrue
        Var _     -> PTrue    -- Variables are always assumed to be OK.
                          -- The idea is that we are going to check for
                          -- defined-ness before instantiating variables.
        x :+ y    -> cryDefined x :&& cryDefined y
        x :- y    -> cryDefined x :&& cryDefined y :&&
                     Fin y :&& x :>= y
        x :* y    -> cryDefined x :&& cryDefined y
        Div x y   -> cryDefined x :&& cryDefined y :&&
                     Fin x :&& y :>= K (Nat 1)
        Mod x y   -> cryDefined x :&& cryDefined y :&&
                     Fin x :&& y :>= K (Nat 1)
        x :^^ y   -> cryDefined x :&& cryDefined y
        Min x y   -> cryDefined x :&& cryDefined y
        Max x y   -> cryDefined x :&& cryDefined y
        Width x   -> cryDefined x
        LenFromThen x y w ->
          cryDefined x :&& cryDefined y :&& cryDefined w :&&
          Fin x :&& Fin y :&& Fin w :&& Not (x :== y) :&& w :>= Width x
        LenFromThenTo x y z ->
          cryDefined x :&& cryDefined y :&& cryDefined z :&&
          Fin x :&& Fin y :&& Fin z :&& Not (x :== y)