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

Description

This module contains machinery to reason about ordering of variables, their finiteness, and their possible intervals.

Synopsis

- data OrdFacts
- data AssertResult
  - = OrdAdded OrdFacts
  - | OrdAlreadyKnown
  - | OrdImprove Type Type
  - | OrdImpossible
  - | OrdCannot
- noFacts :: OrdFacts
- addFact :: IsFact t => t -> OrdFacts -> AssertResult
- isKnownLeq :: OrdFacts -> Type -> Type -> Bool
- knownInterval :: OrdFacts -> Type -> Interval
- ordFactsToGoals :: OrdFacts -> [Goal]
- ordFactsToProps :: OrdFacts -> [Prop]
- dumpDot :: Bool -> OrdFacts -> String
- dumpDoc :: OrdFacts -> Doc
- class IsFact t where
  - factProp :: t -> Prop
  - factChangeProp :: t -> Prop -> t
  - factSource :: t -> EdgeSrc

# Documentation

data OrdFacts Source

Instances

Show OrdFacts Source |

data AssertResult Source

Possible outcomes, when asserting a fact.

Constructors

OrdAdded OrdFacts | We added a new fact
OrdAlreadyKnown | We already knew this
OrdImprove Type Type | Only if the two types are equal
OrdImpossible | The fact is known to be false
OrdCannot | We could not perform opertaion.

Instances

Show AssertResult Source |

noFacts :: OrdFacts Source

addFact :: IsFact t => t -> OrdFacts -> AssertResult Source

isKnownLeq :: OrdFacts -> Type -> Type -> Bool Source

Query if the one type is known to be smaller than, or equal to, the other. Assumes that the type is simple (i.e., no type functions).

knownInterval :: OrdFacts -> Type -> Interval Source

Compute an interval, that we know definately contains the given type. Assumes that the type is normalized (i.e., no type functions).

ordFactsToGoals :: OrdFacts -> [Goal] Source

ordFactsToProps :: OrdFacts -> [Prop] Source

dumpDot :: Bool -> OrdFacts -> String Source

Render facts in `dot` notation. The boolean says if we want the arrows to point up.

dumpDoc :: OrdFacts -> Doc Source

class IsFact t where Source

Add a `(>=)` or `fin` goal into the model. Assumes that the types are normalized (i.e., no type functions).

Methods

factProp :: t -> Prop Source

factChangeProp :: t -> Prop -> t Source

factSource :: t -> EdgeSrc Source

Instances

IsFact Prop Source |
IsFact Goal Source |