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

Description

Synopsis

- simplifyAllConstraints :: InferM ()
- proveImplication :: LQName -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
- assumedOrderModel :: OrdFacts -> [Prop] -> Either (OrdFacts, Prop) (OrdFacts, [Prop])
- checkTypeFunction :: TFun -> [Type] -> [Prop]

# Documentation

simplifyAllConstraints :: InferM () Source

proveImplication :: LQName -> [TParam] -> [Prop] -> [Goal] -> InferM Subst Source

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)

checkTypeFunction :: TFun -> [Type] -> [Prop] Source