cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright | (c) 2014-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.TypeCheck.Solver.Numeric.AST

Description

The sytnax of numeric propositions.

Synopsis

- data Name
  - = UserName TVar
  - | SysName Int
- ppName :: Name -> Doc
- data Prop
  - = Fin Expr
  - | Expr :== Expr
  - | Expr :>= Expr
  - | Expr :> Expr
  - | Expr :==: Expr
  - | Expr :>: Expr
  - | Prop :&& Prop
  - | Prop :|| Prop
  - | Not Prop
  - | PFalse
  - | PTrue
- cryPropExprs :: Prop -> [Expr]
- cryPropFVS :: Prop -> Set Name
- ppProp :: Prop -> Doc
- ppPropPrec :: Int -> Prop -> Doc
- data Expr
  - = K Nat'
  - | Var Name
  - | Expr :+ Expr
  - | Expr :- Expr
  - | Expr :* Expr
  - | Div Expr Expr
  - | Mod Expr Expr
  - | Expr :^^ Expr
  - | Min Expr Expr
  - | Max Expr Expr
  - | Width Expr
  - | LenFromThen Expr Expr Expr
  - | LenFromThenTo Expr Expr Expr
- zero :: Expr
- one :: Expr
- two :: Expr
- inf :: Expr
- cryAnds :: [Prop] -> Prop
- cryOrs :: [Prop] -> Prop
- cryExprExprs :: Expr -> [Expr]
- cryRebuildExpr :: Expr -> [Expr] -> Expr
- cryExprFVS :: Expr -> Set Name
- ppExpr :: Expr -> Doc
- ppExprPrec :: Int -> Expr -> Doc
- data Nat'
  - = Nat Integer
  - | Inf
- type IfExpr = IfExpr' Prop
- data IfExpr' p a
  - = If p (IfExpr' p a) (IfExpr' p a)
  - | Return a
  - | Impossible
- ppIf :: (p -> Doc) -> (a -> Doc) -> IfExpr' p a -> Doc
- ppIfExpr :: IfExpr Expr -> Doc
- type Subst = Map Name Expr
- class HasVars ast where
- cryLet :: HasVars e => Name -> Expr -> e -> Maybe e
- composeSubst :: Subst -> Subst -> Subst
- doAppSubst :: HasVars a => Subst -> a -> a

# 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.4.0-CN28BMG3PUFD1lr9WvB1U9" 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.4.0-CN28BMG3PUFD1lr9WvB1U9" 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.

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 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.4.0-CN28BMG3PUFD1lr9WvB1U9" 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.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "Nat" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer))) (C1 (MetaCons "Inf" PrefixI False) U1))

type IfExpr = IfExpr' Prop Source #

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 # (*>) :: 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.

type Subst = Map Name Expr Source #

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 #

composeSubst :: Subst -> Subst -> Subst Source #

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