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

Description

Solver code that does not depend on the type inference monad.

Synopsis

- numericStep :: OrdFacts -> Goal -> Solved
- simpFin :: OrdFacts -> Prop -> Maybe [Prop]
- goalOrderModel :: OrdFacts -> [Goal] -> (OrdFacts, [Goal], [Goal])

# Documentation

numericStep :: OrdFacts -> Goal -> Solved Source

Try to perform a single step of simplification for a numeric goal. We assume that the substitution has been applied to the goal.

simpFin :: OrdFacts -> Prop -> Maybe [Prop] Source

goalOrderModel :: OrdFacts -> [Goal] -> (OrdFacts, [Goal], [Goal]) Source

Collect `fin` and `<=` constraints in the ord model Returns (new model, bad goals, other goals). "bad goals" are goals that are incompatible with the model "other goals" are ones that are not "<=" or "fin"