Copyright	(c) 2022 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Cryptol.Parser.ExpandPropGuards

Description

Expands PropGuards into a top-level definition for each case, and rewrites the body of each case to be an appropriate call to the respectively generated function.

Synopsis

type ExpandPropGuardsM a = Either Error a
runExpandPropGuardsM :: ExpandPropGuardsM a -> Either Error a
data Error
- = NoSignature (Located PName)
- | NestedConstraintGuard (Located PName)
expandPropGuards :: ModuleG mname PName -> ExpandPropGuardsM (ModuleG mname PName)
expandModuleDef :: ModuleDefinition PName -> ExpandPropGuardsM (ModuleDefinition PName)
expandTopDecl :: TopDecl PName -> ExpandPropGuardsM [TopDecl PName]
expandDecl :: Decl PName -> ExpandPropGuardsM [Decl PName]
expandBind :: Bind PName -> ExpandPropGuardsM [Bind PName]
checkNestedGuardsInExpr :: Expr PName -> ExpandPropGuardsM ()
checkNestedGuardsInDecl :: Decl PName -> ExpandPropGuardsM ()
checkNestedGuardsInBind :: Bind PName -> ExpandPropGuardsM ()
patternToExpr :: Pattern PName -> Expr PName
newName :: Located PName -> [Prop PName] -> ExpandPropGuardsM (Located PName)

Documentation

type ExpandPropGuardsM a = Either Error a Source #

Monad

runExpandPropGuardsM :: ExpandPropGuardsM a -> Either Error a Source #

data Error Source #

Errors that can happen while expanding constraint guards.

Constructors

NoSignature (Located PName)	A declaration using constraints guard lacks an explicit type signature, which is a requirement.
NestedConstraintGuard (Located PName)	Constraint guards appear somewhere other than the top level, which is not allowed.

Instances

Instances details

Generic Error Source #
Instance details Defined in Cryptol.Parser.ExpandPropGuards Associated Types type Rep Error :: Type -> Type # Methods from :: Error -> Rep Error x # to :: Rep Error x -> Error #
Show Error Source #
Instance details Defined in Cryptol.Parser.ExpandPropGuards Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #
PP Error Source #
Instance details Defined in Cryptol.Parser.ExpandPropGuards Methods ppPrec :: Int -> Error -> Doc Source #
NFData Error Source #
Instance details Defined in Cryptol.Parser.ExpandPropGuards Methods rnf :: Error -> () #
type Rep Error Source #
Instance details Defined in Cryptol.Parser.ExpandPropGuards type Rep Error = D1 ('MetaData "Error" "Cryptol.Parser.ExpandPropGuards" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" 'False) (C1 ('MetaCons "NoSignature" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located PName))) :+: C1 ('MetaCons "NestedConstraintGuard" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located PName))))

expandPropGuards :: ModuleG mname PName -> ExpandPropGuardsM (ModuleG mname PName) Source #

expandModuleDef :: ModuleDefinition PName -> ExpandPropGuardsM (ModuleDefinition PName) Source #

expandTopDecl :: TopDecl PName -> ExpandPropGuardsM [TopDecl PName] Source #

expandDecl :: Decl PName -> ExpandPropGuardsM [Decl PName] Source #

expandBind :: Bind PName -> ExpandPropGuardsM [Bind PName] Source #

checkNestedGuardsInExpr :: Expr PName -> ExpandPropGuardsM () Source #

Check for nested uses of constraint guards in an expression (e.g., in a local definition bound with where).

checkNestedGuardsInDecl :: Decl PName -> ExpandPropGuardsM () Source #

Check for nested uses of constraint guards in a local declaration.

checkNestedGuardsInBind :: Bind PName -> ExpandPropGuardsM () Source #

Check for nested uses of constraint guards in a local bind.

patternToExpr :: Pattern PName -> Expr PName Source #

newName :: Located PName -> [Prop PName] -> ExpandPropGuardsM (Located PName) Source #