Copyright | (c) 2013-2016 Galois Inc. |
---|---|

License | BSD3 |

Maintainer | cryptol@galois.com |

Stability | provisional |

Portability | portable |

Safe Haskell | Safe |

Language | Haskell2010 |

Solving class constraints.

## Synopsis

- classStep :: Prop -> Solved
- solveZeroInst :: Type -> Solved
- solveLogicInst :: Type -> Solved
- solveArithInst :: Type -> Solved
- solveCmpInst :: Type -> Solved
- solveSignedCmpInst :: Type -> Solved
- solveLiteralInst :: Type -> Type -> Solved
- expandProp :: Prop -> [Prop]

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

solveArithInst :: Type -> Solved Source #

Solve an Arith constraint by instance, if possible.

solveCmpInst :: Type -> Solved Source #

Solve Cmp constraints.

solveSignedCmpInst :: Type -> Solved Source #

Solve SignedCmp constraints.

expandProp :: Prop -> [Prop] Source #

Add propositions that are implied by the given one. The result contains the orignal proposition, and maybe some more.