Cryptol.TypeCheck.Solver.FinOrd

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

Documentation

data OrdFacts

Instances

Show OrdFacts

data AssertResult

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

noFacts :: OrdFacts

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

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

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

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]

ordFactsToProps :: OrdFacts -> [Prop]

dumpDot :: Bool -> OrdFacts -> String

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

dumpDoc :: OrdFacts -> Doc

class IsFact t where

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

Methods

factProp :: t -> Prop

factChangeProp :: t -> Prop -> t

factSource :: t -> EdgeSrc

Instances

IsFact Prop

IsFact Goal