cryptol-2.2.5: Cryptol: The Language of Cryptography

Copyright(c) 2013-2015 Galois, Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell98

Cryptol.TypeCheck.Solver.Eval

Description

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

Synopsis

Documentation

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

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] Source

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).

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

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

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

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

tfLg2 :: OrdFacts -> Type -> Maybe Type Source

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

tfWidth :: OrdFacts -> Type -> Maybe Type Source

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