Cryptol.TypeCheck.Solver.Eval

We define the behavior of Cryptol's type-level functions on integers.

Documentation

assumedOrderModel :: OrdFacts -> [Prop] -> Either (OrdFacts, Prop) (OrdFacts, [Prop])

Collect fin and simple <= constraints in the ord model Returns Left if we find a goal which is incompatible with the others. Otherwise, we return Right with a model, and the remaining (i.e., the non-order related) properties.

These sorts of facts are quite useful during type simplification, because they provide information which potentially useful for cancellation (e.g., this variables is finite and not 0)

derivedOrd :: OrdFacts -> Prop -> [Prop]

This returns order properties that are implied by the give property. It is important that the returned properties are propoer ordering properties (i.e., addFact will not return OrdCannot).

isSimpleType :: Type -> Bool

simpType :: OrdFacts -> Type -> Type

reorderArgs :: TFun -> [Type] -> [Type]

commuteArgs :: [Type] -> [Type]

evalTFun :: OrdFacts -> TFun -> [Type] -> Maybe Type

typeInterval :: OrdFacts -> Type -> Interval

typeKnownLeq :: OrdFacts -> Type -> Type -> Bool

typeKnownFin :: OrdFacts -> Type -> Bool

tfAdd :: OrdFacts -> Type -> Type -> Maybe Type

tfSub :: OrdFacts -> Type -> Type -> Maybe Type

tfSub x y = Just z iff z is the unique value such that tfAdd y z = Just x

tfMul :: OrdFacts -> Type -> Type -> Maybe Type

It is important that the 0 rules come before the Inf ones

tfDiv :: OrdFacts -> Type -> Type -> Maybe Type

tfMod :: OrdFacts -> Type -> Type -> Maybe Type

tfMin :: OrdFacts -> Type -> Type -> Maybe Type

tfMax :: OrdFacts -> Type -> Type -> Maybe Type

tfExp :: OrdFacts -> Type -> Type -> Maybe Type

tfLg2 :: OrdFacts -> Type -> Maybe Type

Rounds up lg2 x = Just y, if y is the smallest number such that x <= 2 ^ y

tfWidth :: OrdFacts -> Type -> Maybe Type

XXX: width and lg2 are almost the same! width n == lg2 (n + 1)

tfLenFromThen :: OrdFacts -> Type -> Type -> Type -> Maybe Type

tfLenFromThenTo :: OrdFacts -> Type -> Type -> Type -> Maybe Type

toNat' :: Type -> Maybe Nat'

fromNat' :: Nat' -> Type

oneOrMore :: OrdFacts -> Type -> Bool

twoOrMore :: OrdFacts -> Type -> Bool