cryptol-2.5.0: Cryptol: The Language of Cryptography

Copyright(c) 2014-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell98

Cryptol.TypeCheck.Solver.Numeric.AST

Description

The sytnax of numeric propositions.

Synopsis

Documentation

data Name Source #

Constructors

UserName TVar 
SysName Int 

Instances

Eq Name Source # 

Methods

(==) :: Name -> Name -> Bool #

(/=) :: Name -> Name -> Bool #

Ord Name Source # 

Methods

compare :: Name -> Name -> Ordering #

(<) :: Name -> Name -> Bool #

(<=) :: Name -> Name -> Bool #

(>) :: Name -> Name -> Bool #

(>=) :: Name -> Name -> Bool #

max :: Name -> Name -> Name #

min :: Name -> Name -> Name #

Show Name Source # 

Methods

showsPrec :: Int -> Name -> ShowS #

show :: Name -> String #

showList :: [Name] -> ShowS #

Generic Name Source # 

Associated Types

type Rep Name :: * -> * #

Methods

from :: Name -> Rep Name x #

to :: Rep Name x -> Name #

type Rep Name Source # 
type Rep Name = D1 * (MetaData "Name" "Cryptol.TypeCheck.Solver.Numeric.AST" "cryptol-2.5.0-3PqSAAliSLCBJq4xfXtTdA" False) ((:+:) * (C1 * (MetaCons "UserName" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * TVar))) (C1 * (MetaCons "SysName" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Int))))

ppName :: Name -> Doc Source #

Pretty print a name.

data Prop Source #

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

Methods

(==) :: Prop -> Prop -> Bool #

(/=) :: Prop -> Prop -> Bool #

Show Prop Source # 

Methods

showsPrec :: Int -> Prop -> ShowS #

show :: Prop -> String #

showList :: [Prop] -> ShowS #

Generic Prop Source # 

Associated Types

type Rep Prop :: * -> * #

Methods

from :: Prop -> Rep Prop x #

to :: Rep Prop x -> Prop #

HasVars Prop Source # 

Methods

apSubst :: Subst -> Prop -> Maybe Prop Source #

DebugLog Prop Source # 

Methods

debugLog :: Solver -> Prop -> IO () Source #

debugLogList :: Solver -> [Prop] -> IO () Source #

type Rep Prop Source # 
type Rep Prop = D1 * (MetaData "Prop" "Cryptol.TypeCheck.Solver.Numeric.AST" "cryptol-2.5.0-3PqSAAliSLCBJq4xfXtTdA" False) ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "Fin" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr))) (C1 * (MetaCons ":==" (InfixI NotAssociative 4) False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr))))) ((:+:) * (C1 * (MetaCons ":>=" (InfixI NotAssociative 4) False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)))) ((:+:) * (C1 * (MetaCons ":>" (InfixI NotAssociative 4) False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)))) (C1 * (MetaCons ":==:" (InfixI NotAssociative 4) False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr))))))) ((:+:) * ((:+:) * (C1 * (MetaCons ":>:" (InfixI NotAssociative 4) False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)))) ((:+:) * (C1 * (MetaCons ":&&" (InfixI RightAssociative 3) False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Prop)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Prop)))) (C1 * (MetaCons ":||" (InfixI RightAssociative 2) False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Prop)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Prop)))))) ((:+:) * (C1 * (MetaCons "Not" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Prop))) ((:+:) * (C1 * (MetaCons "PFalse" PrefixI False) (U1 *)) (C1 * (MetaCons "PTrue" PrefixI False) (U1 *))))))

cryPropExprs :: Prop -> [Expr] Source #

Compute all expressions in a property.

cryPropFVS :: Prop -> Set Name Source #

Compute the free variables in a proposition.

ppProp :: Prop -> Doc Source #

Pretty print a top-level property.

ppPropPrec :: Int -> Prop -> Doc Source #

Pretty print a proposition, in the given precedence context.

data Expr Source #

Expressions, representing Cryptol's numeric types.

Instances

Eq Expr Source # 

Methods

(==) :: Expr -> Expr -> Bool #

(/=) :: Expr -> Expr -> Bool #

Ord Expr Source # 

Methods

compare :: Expr -> Expr -> Ordering #

(<) :: Expr -> Expr -> Bool #

(<=) :: Expr -> Expr -> Bool #

(>) :: Expr -> Expr -> Bool #

(>=) :: Expr -> Expr -> Bool #

max :: Expr -> Expr -> Expr #

min :: Expr -> Expr -> Expr #

Show Expr Source # 

Methods

showsPrec :: Int -> Expr -> ShowS #

show :: Expr -> String #

showList :: [Expr] -> ShowS #

Generic Expr Source # 

Associated Types

type Rep Expr :: * -> * #

Methods

from :: Expr -> Rep Expr x #

to :: Rep Expr x -> Expr #

HasVars Expr Source # 

Methods

apSubst :: Subst -> Expr -> Maybe Expr Source #

type Rep Expr Source # 
type Rep Expr = D1 * (MetaData "Expr" "Cryptol.TypeCheck.Solver.Numeric.AST" "cryptol-2.5.0-3PqSAAliSLCBJq4xfXtTdA" False) ((:+:) * ((:+:) * ((:+:) * (C1 * (MetaCons "K" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Nat'))) ((:+:) * (C1 * (MetaCons "Var" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Name))) (C1 * (MetaCons ":+" (InfixI LeftAssociative 6) False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)))))) ((:+:) * (C1 * (MetaCons ":-" (InfixI LeftAssociative 6) False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)))) ((:+:) * (C1 * (MetaCons ":*" (InfixI LeftAssociative 7) False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)))) (C1 * (MetaCons "Div" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr))))))) ((:+:) * ((:+:) * (C1 * (MetaCons "Mod" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)))) ((:+:) * (C1 * (MetaCons ":^^" (InfixI RightAssociative 8) False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)))) (C1 * (MetaCons "Min" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)))))) ((:+:) * ((:+:) * (C1 * (MetaCons "Max" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)))) (C1 * (MetaCons "Width" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)))) ((:+:) * (C1 * (MetaCons "LenFromThen" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr))))) (C1 * (MetaCons "LenFromThenTo" PrefixI False) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) ((:*:) * (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Expr)))))))))

zero :: Expr Source #

The constant 0.

one :: Expr Source #

The constant 1.

two :: Expr Source #

The constant 2.

inf :: Expr Source #

The constant infinity.

cryAnds :: [Prop] -> Prop Source #

Make a conjucntion of the given properties.

cryOrs :: [Prop] -> Prop Source #

Make a disjunction of the given properties.

cryExprExprs :: Expr -> [Expr] Source #

Compute the immediate sub-expressions of an expression.

cryRebuildExpr :: Expr -> [Expr] -> Expr Source #

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

Compute the free variables in an expression.

ppExpr :: Expr -> Doc Source #

Pretty print an expression at the top level.

ppExprPrec :: Int -> Expr -> Doc Source #

Pretty print an expression, in the given precedence context.

data Nat' Source #

Natural numbers with an infinity element

Constructors

Nat Integer 
Inf 

Instances

Eq Nat' Source # 

Methods

(==) :: Nat' -> Nat' -> Bool #

(/=) :: Nat' -> Nat' -> Bool #

Ord Nat' Source # 

Methods

compare :: Nat' -> Nat' -> Ordering #

(<) :: Nat' -> Nat' -> Bool #

(<=) :: Nat' -> Nat' -> Bool #

(>) :: Nat' -> Nat' -> Bool #

(>=) :: Nat' -> Nat' -> Bool #

max :: Nat' -> Nat' -> Nat' #

min :: Nat' -> Nat' -> Nat' #

Show Nat' Source # 

Methods

showsPrec :: Int -> Nat' -> ShowS #

show :: Nat' -> String #

showList :: [Nat'] -> ShowS #

Generic Nat' Source # 

Associated Types

type Rep Nat' :: * -> * #

Methods

from :: Nat' -> Rep Nat' x #

to :: Rep Nat' x -> Nat' #

NFData Nat' Source # 

Methods

rnf :: Nat' -> () #

type Rep Nat' Source # 
type Rep Nat' = D1 * (MetaData "Nat'" "Cryptol.TypeCheck.Solver.InfNat" "cryptol-2.5.0-3PqSAAliSLCBJq4xfXtTdA" False) ((:+:) * (C1 * (MetaCons "Nat" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * Integer))) (C1 * (MetaCons "Inf" PrefixI False) (U1 *)))

data IfExpr' p a Source #

Constructors

If p (IfExpr' p a) (IfExpr' p a) 
Return a 
Impossible 

Instances

Monad (IfExpr' p) Source # 

Methods

(>>=) :: IfExpr' p a -> (a -> IfExpr' p b) -> IfExpr' p b #

(>>) :: IfExpr' p a -> IfExpr' p b -> IfExpr' p b #

return :: a -> IfExpr' p a #

fail :: String -> IfExpr' p a #

Functor (IfExpr' p) Source # 

Methods

fmap :: (a -> b) -> IfExpr' p a -> IfExpr' p b #

(<$) :: a -> IfExpr' p b -> IfExpr' p a #

Applicative (IfExpr' p) Source # 

Methods

pure :: a -> IfExpr' p a #

(<*>) :: IfExpr' p (a -> b) -> IfExpr' p a -> IfExpr' p b #

liftA2 :: (a -> b -> c) -> IfExpr' p a -> IfExpr' p b -> IfExpr' p c #

(*>) :: IfExpr' p a -> IfExpr' p b -> IfExpr' p b #

(<*) :: IfExpr' p a -> IfExpr' p b -> IfExpr' p a #

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

Methods

(==) :: IfExpr' p a -> IfExpr' p a -> Bool #

(/=) :: IfExpr' p a -> IfExpr' p a -> Bool #

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

Pretty print an experssion with ifs.

ppIfExpr :: IfExpr Expr -> Doc Source #

Pretty print an experssion with ifs.

class HasVars ast where Source #

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

Minimal complete definition

apSubst

Methods

apSubst :: Subst -> ast -> Maybe ast Source #

Instances

HasVars Bool Source #

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

Methods

apSubst :: Subst -> Bool -> Maybe Bool Source #

HasVars Expr Source # 

Methods

apSubst :: Subst -> Expr -> Maybe Expr Source #

HasVars Prop Source # 

Methods

apSubst :: Subst -> Prop -> Maybe Prop Source #

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

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