Copyright | (c) 2013-2015 Galois, Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell98 |
This module contains machinery to reason about ordering of variables, their finiteness, and their possible intervals.
- data OrdFacts
- data AssertResult
- 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 AssertResult Source
Possible outcomes, when asserting a fact.
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. |
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