Cryptol.TypeCheck.Solver.Numeric.AST

The sytnax of numeric propositions.

Documentation

data Name

Constructors

UserName TVar

SysName Int

Instances

Eq Name

Ord Name

Show Name

Generic Name

type Rep Name

ppName :: Name -> Doc

Pretty print a name.

data Prop

Propopsitions, representing Cryptol's numeric constraints (and a bit more).

Constructors

Fin Expr

Expr :== Expr infix 4

Expr :>= Expr infix 4

Expr :> Expr infix 4

Expr :==: Expr infix 4

Expr :>: Expr infix 4

Prop :&& Prop infixr 3

Prop :|| Prop infixr 2

Not Prop

PFalse

PTrue

Instances

Eq Prop

Show Prop

Generic Prop

HasVars Prop

DebugLog Prop

type Rep Prop

cryPropExprs :: Prop -> [Expr]

Compute all expressions in a property.

cryPropFVS :: Prop -> Set Name

Compute the free variables in a proposition.

ppProp :: Prop -> Doc

Pretty print a top-level property.

ppPropPrec :: Int -> Prop -> Doc

Pretty print a proposition, in the given precedence context.

data Expr

Expressions, representing Cryptol's numeric types.

Constructors

K Nat'

Var Name

Expr :+ Expr infixl 6

Expr :- Expr infixl 6

Expr :* Expr infixl 7

Div Expr Expr

Mod Expr Expr

Expr :^^ Expr infixr 8

Min Expr Expr

Max Expr Expr

Width Expr

LenFromThen Expr Expr Expr

LenFromThenTo Expr Expr Expr

Instances

Eq Expr

Ord Expr

Show Expr

Generic Expr

HasVars Expr

type Rep Expr

zero :: Expr

The constant 0.

one :: Expr

The constant 1.

two :: Expr

The constant 2.

inf :: Expr

The constant infinity.

cryAnds :: [Prop] -> Prop

Make a conjucntion of the given properties.

cryOrs :: [Prop] -> Prop

Make a disjunction of the given properties.

cryExprExprs :: Expr -> [Expr]

Compute the immediate sub-expressions of an expression.

cryRebuildExpr :: Expr -> [Expr] -> Expr

Rebuild an expression, using the top-level strucutre of the first expression, but the second list of expressions as sub-expressions.

cryExprFVS :: Expr -> Set Name

Compute the free variables in an expression.

ppExpr :: Expr -> Doc

Pretty print an expression at the top level.

ppExprPrec :: Int -> Expr -> Doc

Pretty print an expression, in the given precedence context.

data Nat'

Natural numbers with an infinity element

Constructors

Nat Integer

Inf

Instances

Eq Nat'

Ord Nat'

Show Nat'

Generic Nat'

TrieKey Nat'

type Rep Nat'

type TrieRep Nat' = TrieRepDefault Nat'

type IfExpr = IfExpr' Prop

data IfExpr' p a

Constructors

If p (IfExpr' p a) (IfExpr' p a)

Return a

Impossible

Instances

Monad (IfExpr' p)

Functor (IfExpr' p)

Applicative (IfExpr' p)

(Eq p, Eq a) => Eq (IfExpr' p a)

ppIf :: (p -> Doc) -> (a -> Doc) -> IfExpr' p a -> Doc

Pretty print an experssion with ifs.

ppIfExpr :: IfExpr Expr -> Doc

Pretty print an experssion with ifs.

type Subst = Map Name Expr

class HasVars ast where

Replaces occurances of the name with the expression. Returns Nothing if there were no occurances of the name.

Methods

apSubst :: Subst -> ast -> Maybe ast

Instances

HasVars Bool

This is used in the simplification to "apply" substitutions to Props.

HasVars Expr

HasVars Prop

cryLet :: HasVars e => Name -> Expr -> e -> Maybe e

composeSubst :: Subst -> Subst -> Subst

doAppSubst :: HasVars a => Subst -> a -> a