module Cryptol.TypeCheck.Solver.Numeric.Defined where
import Cryptol.TypeCheck.Solver.Numeric.AST
import Cryptol.Utils.Panic ( panic )
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)
]
cryDefined :: Expr -> Prop
cryDefined expr =
case expr of
K _ -> PTrue
Var _ -> PTrue
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)