| 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.
- data Name
- ppName :: Name -> Doc
- data Prop
- cryPropExprs :: Prop -> [Expr]
- cryPropFVS :: Prop -> Set Name
- ppProp :: Prop -> Doc
- ppPropPrec :: Int -> Prop -> Doc
- data 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'
- 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
Propopsitions, representing Cryptol's numeric constraints (and a bit more).
cryPropExprs :: Prop -> [Expr] Source #
Compute all expressions in a property.
ppPropPrec :: Int -> Prop -> Doc Source #
Pretty print a proposition, in the given precedence context.
Expressions, representing Cryptol's numeric types.
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.
ppExprPrec :: Int -> Expr -> Doc Source #
Pretty print an expression, in the given precedence context.
Natural numbers with an infinity element
Constructors
| If p (IfExpr' p a) (IfExpr' p a) | |
| Return a | |
| Impossible |
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
doAppSubst :: HasVars a => Subst -> a -> a Source #