cryptol-2.2.6: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2015 Galois, Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.TypeCheck.Solver.Eval

Description

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

Synopsis

- assumedOrderModel :: OrdFacts -> [Prop] -> Either (OrdFacts, Prop) (OrdFacts, [Prop])
- derivedOrd :: OrdFacts -> Prop -> [Prop]
- 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
- tfMul :: OrdFacts -> Type -> Type -> Maybe Type
- 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
- tfWidth :: OrdFacts -> Type -> Maybe Type
- 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

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

isSimpleType :: Type -> Bool Source

simpType :: OrdFacts -> Type -> Type Source

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

commuteArgs :: [Type] -> [Type] Source

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

typeInterval :: OrdFacts -> Type -> Interval Source

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

typeKnownFin :: OrdFacts -> Type -> Bool Source

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

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

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

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

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

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

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

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

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

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

toNat' :: Type -> Maybe Nat' Source

fromNat' :: Nat' -> Type Source

oneOrMore :: OrdFacts -> Type -> Bool Source

twoOrMore :: OrdFacts -> Type -> Bool Source