cryptol-3.0.0: Cryptol: The Language of Cryptography

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

Cryptol.TypeCheck.Solver.Class

Description

Solving class constraints. If you make changes to this file, please update the documenation in RefMan.md

Synopsis

- solveZeroInst :: Type -> Solved
- solveLogicInst :: Type -> Solved
- solveRingInst :: Type -> Solved
- solveFieldInst :: Type -> Solved
- solveIntegralInst :: Type -> Solved
- solveRoundInst :: Type -> Solved
- solveEqInst :: Type -> Solved
- solveCmpInst :: Type -> Solved
- solveSignedCmpInst :: Type -> Solved
- solveLiteralInst :: Type -> Type -> Solved
- solveLiteralLessThanInst :: Type -> Type -> Solved
- solveFLiteralInst :: Type -> Type -> Type -> Type -> Solved
- solveValidFloat :: Type -> Type -> Solved

# Documentation

solveZeroInst :: Type -> Solved Source #

Solve a Zero constraint by instance, if possible.

solveLogicInst :: Type -> Solved Source #

Solve a Logic constraint by instance, if possible.

solveRingInst :: Type -> Solved Source #

Solve a Ring constraint by instance, if possible.

solveFieldInst :: Type -> Solved Source #

Solve a Field constraint by instance, if possible.

solveIntegralInst :: Type -> Solved Source #

Solve an Integral constraint by instance, if possible.

solveRoundInst :: Type -> Solved Source #

Solve a Round constraint by instance, if possible.

solveEqInst :: Type -> Solved Source #

Solve Eq constraints.

solveCmpInst :: Type -> Solved Source #

Solve Cmp constraints.

solveSignedCmpInst :: Type -> Solved Source #

Solve SignedCmp constraints.

solveLiteralInst :: Type -> Type -> Solved Source #

Solve Literal constraints.

solveLiteralLessThanInst :: Type -> Type -> Solved Source #

Solve Literal constraints.

solveFLiteralInst :: Type -> Type -> Type -> Type -> Solved Source #

Solving fractional literal constraints.

solveValidFloat :: Type -> Type -> Solved Source #

This places constraints on the floating point numbers that we can work with. This is a bit of an odd check, as it is really a limitiation of the backend, and not the language itself.

On the other hand, it helps us give sane results if one accidentally types a polymorphic float at the REPL. Hopefully, most users will stick to particular FP sizes, so this should be quite transparent.