cryptol-3.0.0: Cryptol: The Language of Cryptography

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

Cryptol.Parser.AST

Contents

- Names
- Types
- Declarations
- Interactive
- Expressions
- Positions
- Pretty-printing

Description

Synopsis

- data Ident
- mkIdent :: Text -> Ident
- mkInfix :: Text -> Ident
- isInfixIdent :: Ident -> Bool
- nullIdent :: Ident -> Bool
- identText :: Ident -> Text
- data ModName
- modRange :: Module name -> Range
- data PName
  - = UnQual !Ident
  - | Qual !ModName !Ident
  - | NewName !Pass !Int
- getModName :: PName -> Maybe ModName
- getIdent :: PName -> Ident
- mkUnqual :: Ident -> PName
- mkQual :: ModName -> Ident -> PName
- data Named a = Named {
  - name :: Located Ident
  - value :: a
  }
- data Pass
  - = NoPat
  - | MonoValues
  - | ExpandPropGuards String
- data Assoc
  - = LeftAssoc
  - | RightAssoc
  - | NonAssoc
- data Schema n = Forall [TParam n] [Prop n] (Type n) (Maybe Range)
- data TParam n = TParam {
  - tpName :: n
  - tpKind :: Maybe Kind
  - tpRange :: Maybe Range
  }
- data Kind
  - = KProp
  - | KNum
  - | KType
  - | KFun Kind Kind
- data Type n
  - = TFun (Type n) (Type n)
  - | TSeq (Type n) (Type n)
  - | TBit
  - | TNum Integer
  - | TChar Char
  - | TUser n [Type n]
  - | TTyApp [Named (Type n)]
  - | TRecord (Rec (Type n))
  - | TTuple [Type n]
  - | TWild
  - | TLocated (Type n) Range
  - | TParens (Type n) (Maybe Kind)
  - | TInfix (Type n) (Located n) Fixity (Type n)
- newtype Prop n = CType (Type n)
- tsName :: TySyn name -> Located name
- psName :: PropSyn name -> Located name
- tsFixity :: TySyn name -> Maybe Fixity
- psFixity :: PropSyn name -> Maybe Fixity
- type Module = ModuleG ModName
- data ModuleG mname name = Module {
  - mName :: Located mname
  - mDef :: ModuleDefinition name
  }
- mDecls :: ModuleG mname name -> [TopDecl name]
- mImports :: ModuleG mname name -> [Located Import]
- mModParams :: ModuleG mname name -> [ModParam name]
- mIsFunctor :: ModuleG mname nmae -> Bool
- isParamDecl :: TopDecl a -> Bool
- data ModuleDefinition name
  - = NormalModule [TopDecl name]
  - | FunctorInstance (Located (ImpName name)) (ModuleInstanceArgs name) (ModuleInstance name)
  - | InterfaceModule (Signature name)
- data ModuleInstanceArgs name
  - = DefaultInstArg (Located (ModuleInstanceArg name))
  - | DefaultInstAnonArg [TopDecl name]
  - | NamedInstArgs [ModuleInstanceNamedArg name]
- data ModuleInstanceNamedArg name = ModuleInstanceNamedArg (Located Ident) (Located (ModuleInstanceArg name))
- data ModuleInstanceArg name
  - = ModuleArg (ImpName name)
  - | ParameterArg Ident
  - | AddParams
- type ModuleInstance name = Map name name
- emptyModuleInstance :: Ord name => ModuleInstance name
- newtype Program name = Program [TopDecl name]
- data TopDecl name
  - = Decl (TopLevel (Decl name))
  - | DPrimType (TopLevel (PrimType name))
  - | TDNewtype (TopLevel (Newtype name))
  - | Include (Located FilePath)
  - | DParamDecl Range (Signature name)
  - | DModule (TopLevel (NestedModule name))
  - | DImport (Located (ImportG (ImpName name)))
  - | DModParam (ModParam name)
  - | DInterfaceConstraint (Maybe Text) (Located [Prop name])
- data Decl name
  - = DSignature [Located name] (Schema name)
  - | DFixity !Fixity [Located name]
  - | DPragma [Located name] Pragma
  - | DBind (Bind name)
  - | DRec [Bind name]
  - | DPatBind (Pattern name) (Expr name)
  - | DType (TySyn name)
  - | DProp (PropSyn name)
  - | DLocated (Decl name) Range
- data Fixity = Fixity {
  - fAssoc :: !Assoc
  - fLevel :: !Int
  }
- defaultFixity :: Fixity
- data FixityCmp
  - = FCError
  - | FCLeft
  - | FCRight
- compareFixity :: Fixity -> Fixity -> FixityCmp
- data TySyn n = TySyn (Located n) (Maybe Fixity) [TParam n] (Type n)
- data PropSyn n = PropSyn (Located n) (Maybe Fixity) [TParam n] [Prop n]
- data Bind name = Bind {
  - bName :: Located name
  - bParams :: [Pattern name]
  - bDef :: Located (BindDef name)
  - bSignature :: Maybe (Schema name)
  - bInfix :: Bool
  - bFixity :: Maybe Fixity
  - bPragmas :: [Pragma]
  - bMono :: Bool
  - bDoc :: Maybe Text
  - bExport :: !ExportType
  }
- data BindDef name
  - = DPrim
  - | DForeign
  - | DExpr (Expr name)
  - | DPropGuards [PropGuardCase name]
- type LBindDef = Located (BindDef PName)
- data Pragma
  - = PragmaNote String
  - | PragmaProperty
- data ExportType
  - = Public
  - | Private
- data TopLevel a = TopLevel {
  - tlExport :: ExportType
  - tlDoc :: Maybe (Located Text)
  - tlValue :: a
  }
- type Import = ImportG ModName
- data ImportG mname = Import {
  - iModule :: !mname
  - iAs :: Maybe ModName
  - iSpec :: Maybe ImportSpec
  - iInst :: !(Maybe (ModuleInstanceArgs PName))
  }
- data ImportSpec
  - = Hiding [Ident]
  - | Only [Ident]
- data ImpName name
  - = ImpTop ModName
  - | ImpNested name
- data Newtype name = Newtype {
  - nName :: Located name
  - nParams :: [TParam name]
  - nConName :: !name
  - nBody :: Rec (Type name)
  }
- data PrimType name = PrimType {
  - primTName :: Located name
  - primTKind :: Located Kind
  - primTCts :: ([TParam name], [Prop name])
  - primTFixity :: Maybe Fixity
  }
- data ParameterType name = ParameterType {
  - ptName :: Located name
  - ptKind :: Kind
  - ptDoc :: Maybe Text
  - ptFixity :: Maybe Fixity
  - ptNumber :: !Int
  }
- data ParameterFun name = ParameterFun {
  - pfName :: Located name
  - pfSchema :: Schema name
  - pfDoc :: Maybe Text
  - pfFixity :: Maybe Fixity
  }
- newtype NestedModule name = NestedModule (ModuleG name name)
- data Signature name = Signature {
  - sigImports :: ![Located (ImportG (ImpName name))]
  - sigTypeParams :: [ParameterType name]
  - sigConstraints :: [Located (Prop name)]
  - sigDecls :: [SigDecl name]
  - sigFunParams :: [ParameterFun name]
  }
- data SigDecl name
  - = SigTySyn (TySyn name) (Maybe Text)
  - | SigPropSyn (PropSyn name) (Maybe Text)
- data ModParam name = ModParam {
  - mpSignature :: Located (ImpName name)
  - mpAs :: Maybe ModName
  - mpName :: !Ident
  - mpDoc :: Maybe (Located Text)
  - mpRenaming :: !(Map name name)
  }
- data ParamDecl name
  - = DParameterType (ParameterType name)
  - | DParameterFun (ParameterFun name)
  - | DParameterDecl (SigDecl name)
  - | DParameterConstraint [Located (Prop name)]
- data PropGuardCase name = PropGuardCase {
  - pgcProps :: [Located (Prop name)]
  - pgcExpr :: Expr name
  }
- data ReplInput name
  - = ExprInput (Expr name)
  - | LetInput [Decl name]
  - | EmptyInput
- data Expr n
  - = EVar n
  - | ELit Literal
  - | EGenerate (Expr n)
  - | ETuple [Expr n]
  - | ERecord (Rec (Expr n))
  - | ESel (Expr n) Selector
  - | EUpd (Maybe (Expr n)) [UpdField n]
  - | EList [Expr n]
  - | EFromTo (Type n) (Maybe (Type n)) (Type n) (Maybe (Type n))
  - | EFromToBy Bool (Type n) (Type n) (Type n) (Maybe (Type n))
  - | EFromToDownBy Bool (Type n) (Type n) (Type n) (Maybe (Type n))
  - | EFromToLessThan (Type n) (Type n) (Maybe (Type n))
  - | EInfFrom (Expr n) (Maybe (Expr n))
  - | EComp (Expr n) [[Match n]]
  - | EApp (Expr n) (Expr n)
  - | EAppT (Expr n) [TypeInst n]
  - | EIf (Expr n) (Expr n) (Expr n)
  - | EWhere (Expr n) [Decl n]
  - | ETyped (Expr n) (Type n)
  - | ETypeVal (Type n)
  - | EFun (FunDesc n) [Pattern n] (Expr n)
  - | ELocated (Expr n) Range
  - | ESplit (Expr n)
  - | EParens (Expr n)
  - | EInfix (Expr n) (Located n) Fixity (Expr n)
  - | EPrefix PrefixOp (Expr n)
- data Literal
  - = ECNum Integer NumInfo
  - | ECChar Char
  - | ECFrac Rational FracInfo
  - | ECString String
- data NumInfo
  - = BinLit Text Int
  - | OctLit Text Int
  - | DecLit Text
  - | HexLit Text Int
  - | PolyLit Int
- data FracInfo
  - = BinFrac Text
  - | OctFrac Text
  - | DecFrac Text
  - | HexFrac Text
- data Match name
  - = Match (Pattern name) (Expr name)
  - | MatchLet (Bind name)
- data Pattern n
  - = PVar (Located n)
  - | PWild
  - | PTuple [Pattern n]
  - | PRecord (Rec (Pattern n))
  - | PList [Pattern n]
  - | PTyped (Pattern n) (Type n)
  - | PSplit (Pattern n) (Pattern n)
  - | PLocated (Pattern n) Range
- data Selector
  - = TupleSel Int (Maybe Int)
  - | RecordSel Ident (Maybe [Ident])
  - | ListSel Int (Maybe Int)
- data TypeInst name
  - = NamedInst (Named (Type name))
  - | PosInst (Type name)
- data UpdField n = UpdField UpdHow [Located Selector] (Expr n)
- data UpdHow
  - = UpdSet
  - | UpdFun
- data FunDesc n = FunDesc {
  - funDescrName :: Maybe n
  - funDescrArgOffset :: Int
  }
- emptyFunDesc :: FunDesc n
- data PrefixOp
  - = PrefixNeg
  - | PrefixComplement
- prefixFixity :: PrefixOp -> Fixity
- asEApps :: Expr n -> (Expr n, [Expr n])
- data Located a = Located {
  - srcRange :: !Range
  - thing :: !a
  }
- type LPName = Located PName
- type LString = Located String
- type LIdent = Located Ident
- class NoPos t where
  - noPos :: t -> t
- cppKind :: Kind -> Doc
- ppSelector :: Selector -> Doc

# Names

data Ident Source #

The type of identifiers. * The boolean flag indicates whether or not they're infix operators. The boolean is present just as cached information from the lexer, and never used during comparisons. * The MaybeAnon indicates if this is an anonymous name

#### Instances

Instances details

IsString Ident Source # |
Instance details Defined in Cryptol.Utils.Ident Methods fromString :: String -> Ident Source #
Generic Ident Source # |
Instance details Defined in Cryptol.Utils.Ident Associated Types type Rep Ident :: Type -> Type Source # Methods from :: Ident -> Rep Ident x Source # to :: Rep Ident x -> Ident Source #
Show Ident Source # |
Instance details Defined in Cryptol.Utils.Ident Methods showsPrec :: Int -> Ident -> ShowS Source # show :: Ident -> String Source # showList :: [Ident] -> ShowS Source #
ShowParseable Ident Source # |
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Ident -> Doc Void Source #
PP Ident Source # |
Instance details Defined in Cryptol.Utils.PP Methods ppPrec :: Int -> Ident -> Doc Source #
NFData Ident Source # |
Instance details Defined in Cryptol.Utils.Ident Methods rnf :: Ident -> () Source #
Eq Ident Source # |
Instance details Defined in Cryptol.Utils.Ident Methods (==) :: Ident -> Ident -> Bool Source # (/=) :: Ident -> Ident -> Bool Source #
Ord Ident Source # |
Instance details Defined in Cryptol.Utils.Ident Methods compare :: Ident -> Ident -> Ordering Source # (<) :: Ident -> Ident -> Bool Source # (<=) :: Ident -> Ident -> Bool Source # (>) :: Ident -> Ident -> Bool Source # (>=) :: Ident -> Ident -> Bool Source # max :: Ident -> Ident -> Ident Source # min :: Ident -> Ident -> Ident Source #
type Rep Ident Source # |
Instance details Defined in Cryptol.Utils.Ident type Rep Ident

mkIdent :: Text -> Ident Source #

Make a normal (i.e., not anonymous) identifier

mkInfix :: Text -> Ident Source #

isInfixIdent :: Ident -> Bool Source #

nullIdent :: Ident -> Bool Source #

identText :: Ident -> Text Source #

data ModName Source #

Top-level Module names are just text.

#### Instances

Instances details

Generic ModName Source # |
Instance details Defined in Cryptol.Utils.Ident Associated Types type Rep ModName :: Type -> Type Source # Methods from :: ModName -> Rep ModName x Source # to :: Rep ModName x -> ModName Source #
Show ModName Source # |
Instance details Defined in Cryptol.Utils.Ident Methods showsPrec :: Int -> ModName -> ShowS Source # show :: ModName -> String Source # showList :: [ModName] -> ShowS Source #
PP ModName Source # |
Instance details Defined in Cryptol.Utils.PP Methods ppPrec :: Int -> ModName -> Doc Source #
PPName ModName Source # |
Instance details Defined in Cryptol.Utils.PP Methods ppNameFixity :: ModName -> Maybe Fixity Source # ppPrefixName :: ModName -> Doc Source # ppInfixName :: ModName -> Doc Source #
NFData ModName Source # |
Instance details Defined in Cryptol.Utils.Ident Methods rnf :: ModName -> () Source #
Eq ModName Source # |
Instance details Defined in Cryptol.Utils.Ident Methods (==) :: ModName -> ModName -> Bool Source # (/=) :: ModName -> ModName -> Bool Source #
Ord ModName Source # |
Instance details Defined in Cryptol.Utils.Ident Methods compare :: ModName -> ModName -> Ordering Source # (<) :: ModName -> ModName -> Bool Source # (<=) :: ModName -> ModName -> Bool Source # (>) :: ModName -> ModName -> Bool Source # (>=) :: ModName -> ModName -> Bool Source # max :: ModName -> ModName -> ModName Source # min :: ModName -> ModName -> ModName Source #
type Rep ModName Source # |
Instance details Defined in Cryptol.Utils.Ident type Rep ModName

modRange :: Module name -> Range Source #

data PName Source #

Names that originate in the parser.

Constructors

UnQual !Ident | Unqualified names like `x`, `Foo`, or `+`.
Qual !ModName !Ident | Qualified names like `Foo::bar` or `module::!`.
NewName !Pass !Int | Fresh names generated by a pass.

#### Instances

Instances details

Generic PName Source # |
Instance details Defined in Cryptol.Parser.Name Associated Types type Rep PName :: Type -> Type Source # Methods from :: PName -> Rep PName x Source # to :: Rep PName x -> PName Source #
Show PName Source # |
Instance details Defined in Cryptol.Parser.Name Methods showsPrec :: Int -> PName -> ShowS Source # show :: PName -> String Source # showList :: [PName] -> ShowS Source #
PP PName Source # |
Instance details Defined in Cryptol.Parser.Name Methods ppPrec :: Int -> PName -> Doc Source #
PPName PName Source # |
Instance details Defined in Cryptol.Parser.Name Methods ppNameFixity :: PName -> Maybe Fixity Source # ppPrefixName :: PName -> Doc Source # ppInfixName :: PName -> Doc Source #
NFData PName Source # |
Instance details Defined in Cryptol.Parser.Name Methods rnf :: PName -> () Source #
Eq PName Source # |
Instance details Defined in Cryptol.Parser.Name Methods (==) :: PName -> PName -> Bool Source # (/=) :: PName -> PName -> Bool Source #
Ord PName Source # |
Instance details Defined in Cryptol.Parser.Name Methods compare :: PName -> PName -> Ordering Source # (<) :: PName -> PName -> Bool Source # (<=) :: PName -> PName -> Bool Source # (>) :: PName -> PName -> Bool Source # (>=) :: PName -> PName -> Bool Source # max :: PName -> PName -> PName Source # min :: PName -> PName -> PName Source #
BindsNames (InModule (Bind PName)) Source # | Introduce the name
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (Bind PName) -> BuildNamingEnv
BindsNames (InModule (Decl PName)) Source # | The naming environment for a single declaration.
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (Decl PName) -> BuildNamingEnv
BindsNames (InModule (NestedModule PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (NestedModule PName) -> BuildNamingEnv
BindsNames (InModule (Newtype PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (Newtype PName) -> BuildNamingEnv
BindsNames (InModule (ParameterFun PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (ParameterFun PName) -> BuildNamingEnv
BindsNames (InModule (ParameterType PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (ParameterType PName) -> BuildNamingEnv
BindsNames (InModule (PrimType PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (PrimType PName) -> BuildNamingEnv
BindsNames (InModule (SigDecl PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (SigDecl PName) -> BuildNamingEnv
BindsNames (InModule (TopDecl PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (TopDecl PName) -> BuildNamingEnv
BindsNames (Schema PName) Source # | Generate a type renaming environment from the parameters that are bound by this schema.
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: Schema PName -> BuildNamingEnv
BindsNames (TParam PName) Source # | Generate the naming environment for a type parameter.
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: TParam PName -> BuildNamingEnv
RemovePatterns (Expr PName) Source # |
Instance details Defined in Cryptol.Parser.NoPat Methods removePatterns :: Expr PName -> (Expr PName, [Error]) Source #
RemovePatterns (NestedModule PName) Source # |
Instance details Defined in Cryptol.Parser.NoPat Methods removePatterns :: NestedModule PName -> (NestedModule PName, [Error]) Source #
RemovePatterns (Program PName) Source # |
Instance details Defined in Cryptol.Parser.NoPat Methods removePatterns :: Program PName -> (Program PName, [Error]) Source #
RemovePatterns [Decl PName] Source # |
Instance details Defined in Cryptol.Parser.NoPat Methods removePatterns :: [Decl PName] -> ([Decl PName], [Error]) Source #
RemovePatterns (ModuleG mname PName) Source # |
Instance details Defined in Cryptol.Parser.NoPat Methods removePatterns :: ModuleG mname PName -> (ModuleG mname PName, [Error]) Source #
type Rep PName Source # |

Instance details

Defined in Cryptol.Parser.Name

type Rep PName = D1 ('MetaData "PName" "Cryptol.Parser.Name" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "UnQual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Ident)) :+: (C1 ('MetaCons "Qual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Ident)) :+: C1 ('MetaCons "NewName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Pass) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))))

getModName :: PName -> Maybe ModName Source #

getIdent :: PName -> Ident Source #

mkUnqual :: Ident -> PName Source #

mkQual :: ModName -> Ident -> PName Source #

data Named a Source #

Constructors

Named |

Fields

- name :: Located Ident
- value :: a

#### Instances

Instances details

Foldable Named Source # |

Instance details

Defined in Cryptol.Parser.AST

Methods

fold :: Monoid m => Named m -> m Source #

foldMap :: Monoid m => (a -> m) -> Named a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Named a -> m Source #

foldr :: (a -> b -> b) -> b -> Named a -> b Source #

foldr' :: (a -> b -> b) -> b -> Named a -> b Source #

foldl :: (b -> a -> b) -> b -> Named a -> b Source #

foldl' :: (b -> a -> b) -> b -> Named a -> b Source #

foldr1 :: (a -> a -> a) -> Named a -> a Source #

foldl1 :: (a -> a -> a) -> Named a -> a Source #

toList :: Named a -> [a] Source #

null :: Named a -> Bool Source #

length :: Named a -> Int Source #

elem :: Eq a => a -> Named a -> Bool Source #

maximum :: Ord a => Named a -> a Source #

minimum :: Ord a => Named a -> a Source #

sum :: Num a => Named a -> a Source #

product :: Num a => Named a -> a Source #

Traversable Named Source # |
Instance details Defined in Cryptol.Parser.AST Methods traverse :: Applicative f => (a -> f b) -> Named a -> f (Named b) Source # sequenceA :: Applicative f => Named (f a) -> f (Named a) Source # mapM :: Monad m => (a -> m b) -> Named a -> m (Named b) Source # sequence :: Monad m => Named (m a) -> m (Named a) Source #
Functor Named Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Named a -> Named b Source # (<$) :: a -> Named b -> Named a Source #
Generic (Named a) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Named a) :: Type -> Type Source # Methods from :: Named a -> Rep (Named a) x Source # to :: Rep (Named a) x -> Named a Source #
Show a => Show (Named a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Named a -> ShowS Source # show :: Named a -> String Source # showList :: [Named a] -> ShowS Source #
NoPos t => NoPos (Named t) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Named t -> Named t Source #
HasLoc a => HasLoc (Named a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: Named a -> Maybe Range Source #
NFData a => NFData (Named a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Named a -> () Source #
Eq a => Eq (Named a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Named a -> Named a -> Bool Source # (/=) :: Named a -> Named a -> Bool Source #
type Rep (Named a) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (Named a) = D1 ('MetaData "Named" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "Named" 'PrefixI 'True) (S1 ('MetaSel ('Just "name") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located Ident)) :*: S1 ('MetaSel ('Just "value") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

data Pass Source #

Passes that can generate fresh names.

Constructors

NoPat |
MonoValues |
ExpandPropGuards String |

#### Instances

Instances details

Generic Pass Source # |
Instance details Defined in Cryptol.Parser.Name Associated Types type Rep Pass :: Type -> Type Source # Methods from :: Pass -> Rep Pass x Source # to :: Rep Pass x -> Pass Source #
Show Pass Source # |
Instance details Defined in Cryptol.Parser.Name Methods showsPrec :: Int -> Pass -> ShowS Source # show :: Pass -> String Source # showList :: [Pass] -> ShowS Source #
NFData Pass Source # |
Instance details Defined in Cryptol.Parser.Name Methods rnf :: Pass -> () Source #
Eq Pass Source # |
Instance details Defined in Cryptol.Parser.Name Methods (==) :: Pass -> Pass -> Bool Source # (/=) :: Pass -> Pass -> Bool Source #
Ord Pass Source # |
Instance details Defined in Cryptol.Parser.Name Methods compare :: Pass -> Pass -> Ordering Source # (<) :: Pass -> Pass -> Bool Source # (<=) :: Pass -> Pass -> Bool Source # (>) :: Pass -> Pass -> Bool Source # (>=) :: Pass -> Pass -> Bool Source # max :: Pass -> Pass -> Pass Source # min :: Pass -> Pass -> Pass Source #
type Rep Pass Source # |

Instance details

Defined in Cryptol.Parser.Name

type Rep Pass = D1 ('MetaData "Pass" "Cryptol.Parser.Name" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "NoPat" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MonoValues" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExpandPropGuards" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))

data Assoc Source #

Information about associativity.

Constructors

LeftAssoc |
RightAssoc |
NonAssoc |

#### Instances

Instances details

Generic Assoc Source # |
Instance details Defined in Cryptol.Utils.Fixity Associated Types type Rep Assoc :: Type -> Type Source # Methods from :: Assoc -> Rep Assoc x Source # to :: Rep Assoc x -> Assoc Source #
Show Assoc Source # |
Instance details Defined in Cryptol.Utils.Fixity Methods showsPrec :: Int -> Assoc -> ShowS Source # show :: Assoc -> String Source # showList :: [Assoc] -> ShowS Source #
PP Assoc Source # |
Instance details Defined in Cryptol.Utils.PP Methods ppPrec :: Int -> Assoc -> Doc Source #
NFData Assoc Source # |
Instance details Defined in Cryptol.Utils.Fixity Methods rnf :: Assoc -> () Source #
Eq Assoc Source # |
Instance details Defined in Cryptol.Utils.Fixity Methods (==) :: Assoc -> Assoc -> Bool Source # (/=) :: Assoc -> Assoc -> Bool Source #
Ord Assoc Source # |
Instance details Defined in Cryptol.Utils.Fixity Methods compare :: Assoc -> Assoc -> Ordering Source # (<) :: Assoc -> Assoc -> Bool Source # (<=) :: Assoc -> Assoc -> Bool Source # (>) :: Assoc -> Assoc -> Bool Source # (>=) :: Assoc -> Assoc -> Bool Source # max :: Assoc -> Assoc -> Assoc Source # min :: Assoc -> Assoc -> Assoc Source #
type Rep Assoc Source # |
Instance details Defined in Cryptol.Utils.Fixity type Rep Assoc = D1 ('MetaData "Assoc" "Cryptol.Utils.Fixity" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "LeftAssoc" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "RightAssoc" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NonAssoc" 'PrefixI 'False) (U1 :: Type -> Type)))

# Types

data Schema n Source #

Constructors

Forall [TParam n] [Prop n] (Type n) (Maybe Range) |

#### Instances

Instances details

Functor Schema Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Schema a -> Schema b Source # (<$) :: a -> Schema b -> Schema a Source #
Rename Schema Source # | Rename a schema, assuming that none of its type variables are already in scope.
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: Schema PName -> RenameM (Schema Name) Source #
Generic (Schema n) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Schema n) :: Type -> Type Source # Methods from :: Schema n -> Rep (Schema n) x Source # to :: Rep (Schema n) x -> Schema n Source #
Show n => Show (Schema n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Schema n -> ShowS Source # show :: Schema n -> String Source # showList :: [Schema n] -> ShowS Source #
BindsNames (Schema PName) Source # | Generate a type renaming environment from the parameters that are bound by this schema.
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: Schema PName -> BuildNamingEnv
NoPos (Schema name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Schema name -> Schema name Source #
AddLoc (Schema name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods addLoc :: Schema name -> Range -> Schema name Source # dropLoc :: Schema name -> Schema name Source #
HasLoc (Schema name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: Schema name -> Maybe Range Source #
PPName name => PP (Schema name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Schema name -> Doc Source #
NFData n => NFData (Schema n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Schema n -> () Source #
Eq n => Eq (Schema n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Schema n -> Schema n -> Bool Source # (/=) :: Schema n -> Schema n -> Bool Source #
type Rep (Schema n) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (Schema n) = D1 ('MetaData "Schema" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "Forall" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam n]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop n])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Range)))))

data TParam n Source #

Constructors

TParam |

Fields

- tpName :: n
- tpKind :: Maybe Kind
- tpRange :: Maybe Range

#### Instances

Instances details

Functor TParam Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> TParam a -> TParam b Source # (<$) :: a -> TParam b -> TParam a Source #
Rename TParam Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: TParam PName -> RenameM (TParam Name) Source #
Generic (TParam n) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (TParam n) :: Type -> Type Source # Methods from :: TParam n -> Rep (TParam n) x Source # to :: Rep (TParam n) x -> TParam n Source #
Show n => Show (TParam n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> TParam n -> ShowS Source # show :: TParam n -> String Source # showList :: [TParam n] -> ShowS Source #
BindsNames (TParam PName) Source # | Generate the naming environment for a type parameter.
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: TParam PName -> BuildNamingEnv
NoPos (TParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TParam name -> TParam name Source #
AddLoc (TParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods addLoc :: TParam name -> Range -> TParam name Source # dropLoc :: TParam name -> TParam name Source #
HasLoc (TParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: TParam name -> Maybe Range Source #
PPName name => PP (TParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> TParam name -> Doc Source #
NFData n => NFData (TParam n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: TParam n -> () Source #
Eq n => Eq (TParam n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: TParam n -> TParam n -> Bool Source # (/=) :: TParam n -> TParam n -> Bool Source #
type Rep (TParam n) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (TParam n) = D1 ('MetaData "TParam" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "TParam" 'PrefixI 'True) (S1 ('MetaSel ('Just "tpName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 n) :*: (S1 ('MetaSel ('Just "tpKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Kind)) :*: S1 ('MetaSel ('Just "tpRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Range)))))

data Kind Source #

Constructors

KProp |
KNum |
KType |
KFun Kind Kind |

#### Instances

Instances details

Generic Kind Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep Kind :: Type -> Type Source # Methods from :: Kind -> Rep Kind x Source # to :: Rep Kind x -> Kind Source #
Show Kind Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Kind -> ShowS Source # show :: Kind -> String Source # showList :: [Kind] -> ShowS Source #
PP Kind Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Kind -> Doc Source #
NFData Kind Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Kind -> () Source #
Eq Kind Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Kind -> Kind -> Bool Source # (/=) :: Kind -> Kind -> Bool Source #
type Rep Kind Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep Kind = D1 ('MetaData "Kind" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) ((C1 ('MetaCons "KProp" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "KNum" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "KType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "KFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind))))

data Type n Source #

Constructors

TFun (Type n) (Type n)

    [8] -> [8]

TSeq (Type n) (Type n)

    [8] a

TBit

    Bit

TNum Integer

    10

TChar Char

    a

TUser n [Type n] | A type variable or synonym

TTyApp [Named (Type n)]

    `{ x = [8], y = Integer }

TRecord (Rec (Type n))

    { x : [8], y : [32] }

TTuple [Type n]

    ([8], [32])

TWild | `_`, just some type.
TLocated (Type n) Range | Location information

TParens (Type n) (Maybe Kind)

     (ty)

TInfix (Type n) (Located n) Fixity (Type n)

     ty + ty

#### Instances

Instances details

Functor Type Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Type a -> Type b Source # (<$) :: a -> Type b -> Type a Source #
Rename Type Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: Type PName -> RenameM (Type Name) Source #
Generic (Type n) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Type n) :: Type -> Type Source # Methods from :: Type n -> Rep (Type n) x Source # to :: Rep (Type n) x -> Type n Source #
Show n => Show (Type n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Type n -> ShowS Source # show :: Type n -> String Source # showList :: [Type n] -> ShowS Source #
NoPos (Type name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Type name -> Type name Source #
AddLoc (Type name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods addLoc :: Type name -> Range -> Type name Source # dropLoc :: Type name -> Type name Source #
HasLoc (Type name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: Type name -> Maybe Range Source #
PPName name => PP (Type name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Type name -> Doc Source #
NFData n => NFData (Type n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Type n -> () Source #
Eq n => Eq (Type n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Type n -> Type n -> Bool Source # (/=) :: Type n -> Type n -> Bool Source #
type Rep (Type n) Source # |
Instance details Defined in Cryptol.Parser.AST type Rep (Type n)

newtype Prop n Source #

A `Prop` is a `Type` that represents a type constraint.

Constructors

CType (Type n) |

#### Instances

Instances details

Functor Prop Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Prop a -> Prop b Source # (<$) :: a -> Prop b -> Prop a Source #
Rename Prop Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: Prop PName -> RenameM (Prop Name) Source #
Generic (Prop n) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Prop n) :: Type -> Type Source # Methods from :: Prop n -> Rep (Prop n) x Source # to :: Rep (Prop n) x -> Prop n Source #
Show n => Show (Prop n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Prop n -> ShowS Source # show :: Prop n -> String Source # showList :: [Prop n] -> ShowS Source #
NoPos (Prop name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Prop name -> Prop name Source #
PPName name => PP (Prop name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Prop name -> Doc Source #
PPName name => PP [Prop name] Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> [Prop name] -> Doc Source #
NFData n => NFData (Prop n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Prop n -> () Source #
Eq n => Eq (Prop n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Prop n -> Prop n -> Bool Source # (/=) :: Prop n -> Prop n -> Bool Source #
type Rep (Prop n) Source # |
Instance details Defined in Cryptol.Parser.AST type Rep (Prop n) = D1 ('MetaData "Prop" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'True) (C1 ('MetaCons "CType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n))))

tsName :: TySyn name -> Located name Source #

psName :: PropSyn name -> Located name Source #

tsFixity :: TySyn name -> Maybe Fixity Source #

psFixity :: PropSyn name -> Maybe Fixity Source #

# Declarations

type Module = ModuleG ModName Source #

A top-level module

data ModuleG mname name Source #

A module for the pre-typechecker phasese. The two parameters are:

- `mname` the type of module names. This is because top-level and nested modules use differnt types to identify a module.
- `name` the type of identifiers used by declarations. In the parser this starts off as `PName` and after resolving names in the renamer, this becomes `Name`.

Constructors

Module |

Fields

- mName :: Located mname

  Name of the module

- mDef :: ModuleDefinition name

#### Instances

Instances details

Generic (ModuleG mname name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (ModuleG mname name) :: Type -> Type Source # Methods from :: ModuleG mname name -> Rep (ModuleG mname name) x Source # to :: Rep (ModuleG mname name) x -> ModuleG mname name Source #
(Show mname, Show name) => Show (ModuleG mname name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ModuleG mname name -> ShowS Source # show :: ModuleG mname name -> String Source # showList :: [ModuleG mname name] -> ShowS Source #
NoPos (ModuleG mname name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ModuleG mname name -> ModuleG mname name Source #
RemovePatterns (ModuleG mname PName) Source # |
Instance details Defined in Cryptol.Parser.NoPat Methods removePatterns :: ModuleG mname PName -> (ModuleG mname PName, [Error]) Source #
HasLoc (ModuleG mname name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: ModuleG mname name -> Maybe Range Source #
(Show name, PPName mname, PPName name) => PP (ModuleG mname name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ModuleG mname name -> Doc Source #
(NFData mname, NFData name) => NFData (ModuleG mname name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ModuleG mname name -> () Source #
type Rep (ModuleG mname name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (ModuleG mname name) = D1 ('MetaData "ModuleG" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "Module" 'PrefixI 'True) (S1 ('MetaSel ('Just "mName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located mname)) :*: S1 ('MetaSel ('Just "mDef") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ModuleDefinition name))))

mDecls :: ModuleG mname name -> [TopDecl name] Source #

mImports :: ModuleG mname name -> [Located Import] Source #

Imports of top-level (i.e. "file" based) modules.

mModParams :: ModuleG mname name -> [ModParam name] Source #

Get the module parameters of a module (new module system)

mIsFunctor :: ModuleG mname nmae -> Bool Source #

isParamDecl :: TopDecl a -> Bool Source #

data ModuleDefinition name Source #

Different flavours of module we have.

Constructors

NormalModule [TopDecl name] |
FunctorInstance (Located (ImpName name)) (ModuleInstanceArgs name) (ModuleInstance name) | The instance is filled in by the renamer
InterfaceModule (Signature name) |

#### Instances

Instances details

Generic (ModuleDefinition name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (ModuleDefinition name) :: Type -> Type Source # Methods from :: ModuleDefinition name -> Rep (ModuleDefinition name) x Source # to :: Rep (ModuleDefinition name) x -> ModuleDefinition name Source #
Show name => Show (ModuleDefinition name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ModuleDefinition name -> ShowS Source # show :: ModuleDefinition name -> String Source # showList :: [ModuleDefinition name] -> ShowS Source #
NoPos (ModuleDefinition name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ModuleDefinition name -> ModuleDefinition name Source #
(Show name, PPName name) => PP (ModuleDefinition name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ModuleDefinition name -> Doc Source #
NFData name => NFData (ModuleDefinition name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ModuleDefinition name -> () Source #
type Rep (ModuleDefinition name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (ModuleDefinition name) = D1 ('MetaData "ModuleDefinition" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "NormalModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TopDecl name])) :+: (C1 ('MetaCons "FunctorInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located (ImpName name))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ModuleInstanceArgs name)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ModuleInstance name)))) :+: C1 ('MetaCons "InterfaceModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Signature name)))))

data ModuleInstanceArgs name Source #

All arguments in a functor instantiation

Constructors

DefaultInstArg (Located (ModuleInstanceArg name)) | Single parameter instantitaion
DefaultInstAnonArg [TopDecl name] | Single parameter instantitaion using this anonymous module. (parser only)
NamedInstArgs [ModuleInstanceNamedArg name] |

#### Instances

Instances details

Rename ModuleInstanceArgs Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: ModuleInstanceArgs PName -> RenameM (ModuleInstanceArgs Name) Source #
Generic (ModuleInstanceArgs name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (ModuleInstanceArgs name) :: Type -> Type Source # Methods from :: ModuleInstanceArgs name -> Rep (ModuleInstanceArgs name) x Source # to :: Rep (ModuleInstanceArgs name) x -> ModuleInstanceArgs name Source #
Show name => Show (ModuleInstanceArgs name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ModuleInstanceArgs name -> ShowS Source # show :: ModuleInstanceArgs name -> String Source # showList :: [ModuleInstanceArgs name] -> ShowS Source #
NoPos (ModuleInstanceArgs name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ModuleInstanceArgs name -> ModuleInstanceArgs name Source #
(Show name, PPName name) => PP (ModuleInstanceArgs name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ModuleInstanceArgs name -> Doc Source #
NFData name => NFData (ModuleInstanceArgs name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ModuleInstanceArgs name -> () Source #
type Rep (ModuleInstanceArgs name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (ModuleInstanceArgs name) = D1 ('MetaData "ModuleInstanceArgs" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "DefaultInstArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located (ModuleInstanceArg name)))) :+: (C1 ('MetaCons "DefaultInstAnonArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TopDecl name])) :+: C1 ('MetaCons "NamedInstArgs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ModuleInstanceNamedArg name]))))

data ModuleInstanceNamedArg name Source #

A named argument in a functor instantiation

Constructors

ModuleInstanceNamedArg (Located Ident) (Located (ModuleInstanceArg name)) |

#### Instances

Instances details

Rename ModuleInstanceNamedArg Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: ModuleInstanceNamedArg PName -> RenameM (ModuleInstanceNamedArg Name) Source #
Generic (ModuleInstanceNamedArg name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (ModuleInstanceNamedArg name) :: Type -> Type Source # Methods from :: ModuleInstanceNamedArg name -> Rep (ModuleInstanceNamedArg name) x Source # to :: Rep (ModuleInstanceNamedArg name) x -> ModuleInstanceNamedArg name Source #
Show name => Show (ModuleInstanceNamedArg name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ModuleInstanceNamedArg name -> ShowS Source # show :: ModuleInstanceNamedArg name -> String Source # showList :: [ModuleInstanceNamedArg name] -> ShowS Source #
NoPos (ModuleInstanceNamedArg name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ModuleInstanceNamedArg name -> ModuleInstanceNamedArg name Source #
(Show name, PPName name) => PP (ModuleInstanceNamedArg name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ModuleInstanceNamedArg name -> Doc Source #
NFData name => NFData (ModuleInstanceNamedArg name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ModuleInstanceNamedArg name -> () Source #
type Rep (ModuleInstanceNamedArg name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (ModuleInstanceNamedArg name) = D1 ('MetaData "ModuleInstanceNamedArg" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "ModuleInstanceNamedArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located Ident)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located (ModuleInstanceArg name)))))

data ModuleInstanceArg name Source #

An argument in a functor instantiation

Constructors

ModuleArg (ImpName name) | An argument that is a module
ParameterArg Ident | An argument that is a parameter
AddParams | Arguments adds extra parameters to decls. ("backtick" import)

#### Instances

Instances details

Rename ModuleInstanceArg Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: ModuleInstanceArg PName -> RenameM (ModuleInstanceArg Name) Source #
Generic (ModuleInstanceArg name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (ModuleInstanceArg name) :: Type -> Type Source # Methods from :: ModuleInstanceArg name -> Rep (ModuleInstanceArg name) x Source # to :: Rep (ModuleInstanceArg name) x -> ModuleInstanceArg name Source #
Show name => Show (ModuleInstanceArg name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ModuleInstanceArg name -> ShowS Source # show :: ModuleInstanceArg name -> String Source # showList :: [ModuleInstanceArg name] -> ShowS Source #
(Show name, PPName name) => PP (ModuleInstanceArg name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ModuleInstanceArg name -> Doc Source #
NFData name => NFData (ModuleInstanceArg name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ModuleInstanceArg name -> () Source #
type Rep (ModuleInstanceArg name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (ModuleInstanceArg name) = D1 ('MetaData "ModuleInstanceArg" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "ModuleArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ImpName name))) :+: (C1 ('MetaCons "ParameterArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident)) :+: C1 ('MetaCons "AddParams" 'PrefixI 'False) (U1 :: Type -> Type)))

type ModuleInstance name = Map name name Source #

Maps names in the original functor with names in the instnace. Does *NOT* include the parameters, just names for the definitions. This *DOES* include entrirs for all the name in the instantiated functor, including names in modules nested inside the functor.

emptyModuleInstance :: Ord name => ModuleInstance name Source #

newtype Program name Source #

Constructors

Program [TopDecl name] |

#### Instances

Instances details

Show name => Show (Program name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Program name -> ShowS Source # show :: Program name -> String Source # showList :: [Program name] -> ShowS Source #
NoPos (Program name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Program name -> Program name Source #
RemovePatterns (Program PName) Source # |
Instance details Defined in Cryptol.Parser.NoPat Methods removePatterns :: Program PName -> (Program PName, [Error]) Source #
(Show name, PPName name) => PP (Program name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Program name -> Doc Source #

data TopDecl name Source #

A declaration that may only appear at the top level of a module. The module may be nested, however.

Constructors

Decl (TopLevel (Decl name)) |
DPrimType (TopLevel (PrimType name)) |
TDNewtype (TopLevel (Newtype name)) | @newtype T as = t
Include (Located FilePath) | `include File` (until NoInclude)
DParamDecl Range (Signature name) | `parameter ...` (parser only)

DModule (TopLevel (NestedModule name))

    submodule M where ...

DImport (Located (ImportG (ImpName name)))

    import X

DModParam (ModParam name)

    import interface X ...

DInterfaceConstraint (Maybe Text) (Located [Prop name])

    interface constraint

#### Instances

Instances details

Rename TopDecl Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: TopDecl PName -> RenameM (TopDecl Name) Source #
Generic (TopDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (TopDecl name) :: Type -> Type Source # Methods from :: TopDecl name -> Rep (TopDecl name) x Source # to :: Rep (TopDecl name) x -> TopDecl name Source #
Show name => Show (TopDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> TopDecl name -> ShowS Source # show :: TopDecl name -> String Source # showList :: [TopDecl name] -> ShowS Source #
BindsNames (InModule (TopDecl PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (TopDecl PName) -> BuildNamingEnv
NoPos (TopDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TopDecl name -> TopDecl name Source #
HasLoc (TopDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: TopDecl name -> Maybe Range Source #
(Show name, PPName name) => PP (TopDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> TopDecl name -> Doc Source #
NFData name => NFData (TopDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: TopDecl name -> () Source #
type Rep (TopDecl name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (TopDecl name) = D1 ('MetaData "TopDecl" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (((C1 ('MetaCons "Decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevel (Decl name)))) :+: C1 ('MetaCons "DPrimType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevel (PrimType name))))) :+: (C1 ('MetaCons "TDNewtype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevel (Newtype name)))) :+: C1 ('MetaCons "Include" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located FilePath))))) :+: ((C1 ('MetaCons "DParamDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Signature name))) :+: C1 ('MetaCons "DModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevel (NestedModule name))))) :+: (C1 ('MetaCons "DImport" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located (ImportG (ImpName name))))) :+: (C1 ('MetaCons "DModParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ModParam name))) :+: C1 ('MetaCons "DInterfaceConstraint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located [Prop name])))))))

data Decl name Source #

A simple declaration. Generally these are things that can appear both at the top-level of a module and in `where` clauses.

Constructors

DSignature [Located name] (Schema name) | A type signature. Eliminated in NoPat--after NoPat signatures are in their associated Bind
DFixity !Fixity [Located name] | A fixity declaration. Eliminated in NoPat---after NoPat fixities are in their associated Bind
DPragma [Located name] Pragma | A pragma declaration. Eliminated in NoPat---after NoPat fixities are in their associated Bind
DBind (Bind name) | A non-recursive binding.
DRec [Bind name] | A group of recursive bindings. Introduced by the renamer.
DPatBind (Pattern name) (Expr name) | A pattern binding. Eliminated in NoPat---after NoPat fixities are in their associated Bind
DType (TySyn name) | A type synonym.
DProp (PropSyn name) | A constraint synonym.
DLocated (Decl name) Range | Keeps track of the location of a declaration.

#### Instances

Instances details

Functor Decl Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Decl a -> Decl b Source # (<$) :: a -> Decl b -> Decl a Source #
Rename Decl Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: Decl PName -> RenameM (Decl Name) Source #
Generic (Decl name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Decl name) :: Type -> Type Source # Methods from :: Decl name -> Rep (Decl name) x Source # to :: Rep (Decl name) x -> Decl name Source #
Show name => Show (Decl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Decl name -> ShowS Source # show :: Decl name -> String Source # showList :: [Decl name] -> ShowS Source #
BindsNames (InModule (Decl PName)) Source # | The naming environment for a single declaration.
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (Decl PName) -> BuildNamingEnv
NoPos (Decl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Decl name -> Decl name Source #
RemovePatterns [Decl PName] Source # |
Instance details Defined in Cryptol.Parser.NoPat Methods removePatterns :: [Decl PName] -> ([Decl PName], [Error]) Source #
AddLoc (Decl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods addLoc :: Decl name -> Range -> Decl name Source # dropLoc :: Decl name -> Decl name Source #
HasLoc (Decl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: Decl name -> Maybe Range Source #
(Show name, PPName name) => PP (Decl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Decl name -> Doc Source #
NFData name => NFData (Decl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Decl name -> () Source #
Eq name => Eq (Decl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Decl name -> Decl name -> Bool Source # (/=) :: Decl name -> Decl name -> Bool Source #
type Rep (Decl name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (Decl name) = D1 ('MetaData "Decl" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (((C1 ('MetaCons "DSignature" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located name]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Schema name))) :+: C1 ('MetaCons "DFixity" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Fixity) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located name]))) :+: (C1 ('MetaCons "DPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located name]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pragma)) :+: C1 ('MetaCons "DBind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Bind name))))) :+: ((C1 ('MetaCons "DRec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Bind name])) :+: C1 ('MetaCons "DPatBind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern name)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr name)))) :+: (C1 ('MetaCons "DType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TySyn name))) :+: (C1 ('MetaCons "DProp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (PropSyn name))) :+: C1 ('MetaCons "DLocated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Decl name)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))))

data Fixity Source #

Constructors

Fixity |

Fields

- fAssoc :: !Assoc
- fLevel :: !Int

#### Instances

Instances details

Generic Fixity Source # |
Instance details Defined in Cryptol.Utils.Fixity Associated Types type Rep Fixity :: Type -> Type Source # Methods from :: Fixity -> Rep Fixity x Source # to :: Rep Fixity x -> Fixity Source #
Show Fixity Source # |
Instance details Defined in Cryptol.Utils.Fixity Methods showsPrec :: Int -> Fixity -> ShowS Source # show :: Fixity -> String Source # showList :: [Fixity] -> ShowS Source #
PP Fixity Source # |
Instance details Defined in Cryptol.Utils.PP Methods ppPrec :: Int -> Fixity -> Doc Source #
NFData Fixity Source # |
Instance details Defined in Cryptol.Utils.Fixity Methods rnf :: Fixity -> () Source #
Eq Fixity Source # |
Instance details Defined in Cryptol.Utils.Fixity Methods (==) :: Fixity -> Fixity -> Bool Source # (/=) :: Fixity -> Fixity -> Bool Source #
Ord Fixity Source # |
Instance details Defined in Cryptol.Utils.Fixity Methods compare :: Fixity -> Fixity -> Ordering Source # (<) :: Fixity -> Fixity -> Bool Source # (<=) :: Fixity -> Fixity -> Bool Source # (>) :: Fixity -> Fixity -> Bool Source # (>=) :: Fixity -> Fixity -> Bool Source # max :: Fixity -> Fixity -> Fixity Source # min :: Fixity -> Fixity -> Fixity Source #
type Rep Fixity Source # |
Instance details Defined in Cryptol.Utils.Fixity type Rep Fixity = D1 ('MetaData "Fixity" "Cryptol.Utils.Fixity" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "Fixity" 'PrefixI 'True) (S1 ('MetaSel ('Just "fAssoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Assoc) :*: S1 ('MetaSel ('Just "fLevel") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

defaultFixity :: Fixity Source #

The fixity used when none is provided.

data FixityCmp Source #

Constructors

FCError |
FCLeft |
FCRight |

#### Instances

Instances details

Show FixityCmp Source # |
Instance details Defined in Cryptol.Utils.Fixity Methods showsPrec :: Int -> FixityCmp -> ShowS Source # show :: FixityCmp -> String Source # showList :: [FixityCmp] -> ShowS Source #
Eq FixityCmp Source # |
Instance details Defined in Cryptol.Utils.Fixity Methods (==) :: FixityCmp -> FixityCmp -> Bool Source # (/=) :: FixityCmp -> FixityCmp -> Bool Source #

compareFixity :: Fixity -> Fixity -> FixityCmp Source #

Let `op1` have fixity `f1` and `op2` have fixity `f2. Then` compareFixity f1 f2`determines how to parse the infix expression` x op1 y op2 z@.

- `FCLeft`: `(x op1 y) op2 z`
- `FCRight`: `x op1 (y op2 z)`
- `FCError`: no parse

data TySyn n Source #

Constructors

TySyn (Located n) (Maybe Fixity) [TParam n] (Type n) |

#### Instances

Instances details

Functor TySyn Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> TySyn a -> TySyn b Source # (<$) :: a -> TySyn b -> TySyn a Source #
Rename TySyn Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: TySyn PName -> RenameM (TySyn Name) Source #
Generic (TySyn n) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (TySyn n) :: Type -> Type Source # Methods from :: TySyn n -> Rep (TySyn n) x Source # to :: Rep (TySyn n) x -> TySyn n Source #
Show n => Show (TySyn n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> TySyn n -> ShowS Source # show :: TySyn n -> String Source # showList :: [TySyn n] -> ShowS Source #
NoPos (TySyn name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TySyn name -> TySyn name Source #
HasLoc (TySyn name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: TySyn name -> Maybe Range Source #
PPName name => PP (TySyn name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> TySyn name -> Doc Source #
NFData n => NFData (TySyn n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: TySyn n -> () Source #
Eq n => Eq (TySyn n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: TySyn n -> TySyn n -> Bool Source # (/=) :: TySyn n -> TySyn n -> Bool Source #
type Rep (TySyn n) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (TySyn n) = D1 ('MetaData "TySyn" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "TySyn" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam n]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n)))))

data PropSyn n Source #

Constructors

PropSyn (Located n) (Maybe Fixity) [TParam n] [Prop n] |

#### Instances

Instances details

Functor PropSyn Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> PropSyn a -> PropSyn b Source # (<$) :: a -> PropSyn b -> PropSyn a Source #
Rename PropSyn Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: PropSyn PName -> RenameM (PropSyn Name) Source #
Generic (PropSyn n) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (PropSyn n) :: Type -> Type Source # Methods from :: PropSyn n -> Rep (PropSyn n) x Source # to :: Rep (PropSyn n) x -> PropSyn n Source #
Show n => Show (PropSyn n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> PropSyn n -> ShowS Source # show :: PropSyn n -> String Source # showList :: [PropSyn n] -> ShowS Source #
NoPos (PropSyn name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: PropSyn name -> PropSyn name Source #
HasLoc (PropSyn name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: PropSyn name -> Maybe Range Source #
PPName name => PP (PropSyn name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> PropSyn name -> Doc Source #
NFData n => NFData (PropSyn n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: PropSyn n -> () Source #
Eq n => Eq (PropSyn n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: PropSyn n -> PropSyn n -> Bool Source # (/=) :: PropSyn n -> PropSyn n -> Bool Source #
type Rep (PropSyn n) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (PropSyn n) = D1 ('MetaData "PropSyn" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "PropSyn" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam n]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop n]))))

data Bind name Source #

Bindings. Notes:

- The parser does not associate type signatures and pragmas with their bindings: this is done in a separate pass, after de-sugaring pattern bindings. In this way we can associate pragmas and type signatures with the variables defined by pattern bindings as well.
- Currently, there is no surface syntax for defining monomorphic bindings (i.e., bindings that will not be automatically generalized by the type checker. However, they are useful when de-sugaring patterns.

Constructors

Bind |

Fields

- bName :: Located name

  Defined thing

- bParams :: [Pattern name]

  Parameters

- bDef :: Located (BindDef name)

  Definition

- bSignature :: Maybe (Schema name)

  Optional type sig

- bInfix :: Bool

  Infix operator?

- bFixity :: Maybe Fixity

  Optional fixity info

- bPragmas :: [Pragma]

  Optional pragmas

- bMono :: Bool

  Is this a monomorphic binding

- bDoc :: Maybe Text

  Optional doc string

- bExport :: !ExportType

#### Instances

Instances details

Functor Bind Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Bind a -> Bind b Source # (<$) :: a -> Bind b -> Bind a Source #
Rename Bind Source # | Rename a binding.
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: Bind PName -> RenameM (Bind Name) Source #
Generic (Bind name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Bind name) :: Type -> Type Source # Methods from :: Bind name -> Rep (Bind name) x Source # to :: Rep (Bind name) x -> Bind name Source #
Show name => Show (Bind name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Bind name -> ShowS Source # show :: Bind name -> String Source # showList :: [Bind name] -> ShowS Source #
BindsNames (InModule (Bind PName)) Source # | Introduce the name
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (Bind PName) -> BuildNamingEnv
NoPos (Bind name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Bind name -> Bind name Source #
HasLoc (Bind name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: Bind name -> Maybe Range Source #
(Show name, PPName name) => PP (Bind name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Bind name -> Doc Source #
NFData name => NFData (Bind name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Bind name -> () Source #
Eq name => Eq (Bind name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Bind name -> Bind name -> Bool Source # (/=) :: Bind name -> Bind name -> Bool Source #
type Rep (Bind name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (Bind name) = D1 ('MetaData "Bind" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "Bind" 'PrefixI 'True) (((S1 ('MetaSel ('Just "bName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located name)) :*: S1 ('MetaSel ('Just "bParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Pattern name])) :*: (S1 ('MetaSel ('Just "bDef") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located (BindDef name))) :*: (S1 ('MetaSel ('Just "bSignature") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Schema name))) :*: S1 ('MetaSel ('Just "bInfix") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :*: ((S1 ('MetaSel ('Just "bFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity)) :*: S1 ('MetaSel ('Just "bPragmas") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Pragma])) :*: (S1 ('MetaSel ('Just "bMono") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "bDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text)) :*: S1 ('MetaSel ('Just "bExport") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ExportType))))))

data BindDef name Source #

Constructors

DPrim |
DForeign |
DExpr (Expr name) |
DPropGuards [PropGuardCase name] |

#### Instances

Instances details

Functor BindDef Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> BindDef a -> BindDef b Source # (<$) :: a -> BindDef b -> BindDef a Source #
Rename BindDef Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: BindDef PName -> RenameM (BindDef Name) Source #
Generic (BindDef name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (BindDef name) :: Type -> Type Source # Methods from :: BindDef name -> Rep (BindDef name) x Source # to :: Rep (BindDef name) x -> BindDef name Source #
Show name => Show (BindDef name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> BindDef name -> ShowS Source # show :: BindDef name -> String Source # showList :: [BindDef name] -> ShowS Source #
(Show name, PPName name) => PP (BindDef name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> BindDef name -> Doc Source #
NFData name => NFData (BindDef name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: BindDef name -> () Source #
Eq name => Eq (BindDef name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: BindDef name -> BindDef name -> Bool Source # (/=) :: BindDef name -> BindDef name -> Bool Source #
type Rep (BindDef name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (BindDef name) = D1 ('MetaData "BindDef" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) ((C1 ('MetaCons "DPrim" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DForeign" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr name))) :+: C1 ('MetaCons "DPropGuards" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [PropGuardCase name]))))

type LBindDef = Located (BindDef PName) Source #

data Pragma Source #

Constructors

PragmaNote String |
PragmaProperty |

#### Instances

Instances details

Generic Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep Pragma :: Type -> Type Source # Methods from :: Pragma -> Rep Pragma x Source # to :: Rep Pragma x -> Pragma Source #
Show Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Pragma -> ShowS Source # show :: Pragma -> String Source # showList :: [Pragma] -> ShowS Source #
NoPos Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Pragma -> Pragma Source #
PP Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Pragma -> Doc Source #
NFData Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Pragma -> () Source #
Eq Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Pragma -> Pragma -> Bool Source # (/=) :: Pragma -> Pragma -> Bool Source #
type Rep Pragma Source # |
Instance details Defined in Cryptol.Parser.AST type Rep Pragma = D1 ('MetaData "Pragma" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "PragmaNote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "PragmaProperty" 'PrefixI 'False) (U1 :: Type -> Type))

data ExportType Source #

Export information for a declaration.

Constructors

Public |
Private |

#### Instances

Instances details

Generic ExportType Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep ExportType :: Type -> Type Source # Methods from :: ExportType -> Rep ExportType x Source # to :: Rep ExportType x -> ExportType Source #
Show ExportType Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ExportType -> ShowS Source # show :: ExportType -> String Source # showList :: [ExportType] -> ShowS Source #
NFData ExportType Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ExportType -> () Source #
Eq ExportType Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: ExportType -> ExportType -> Bool Source # (/=) :: ExportType -> ExportType -> Bool Source #
Ord ExportType Source # |

Instance details

Defined in Cryptol.Parser.AST

Methods

compare :: ExportType -> ExportType -> Ordering Source #

(<) :: ExportType -> ExportType -> Bool Source #

(<=) :: ExportType -> ExportType -> Bool Source #

(>) :: ExportType -> ExportType -> Bool Source #

(>=) :: ExportType -> ExportType -> Bool Source #

max :: ExportType -> ExportType -> ExportType Source #

min :: ExportType -> ExportType -> ExportType Source #

type Rep ExportType Source # |
Instance details Defined in Cryptol.Parser.AST type Rep ExportType = D1 ('MetaData "ExportType" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "Public" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Private" 'PrefixI 'False) (U1 :: Type -> Type))

data TopLevel a Source #

A top-level module declaration.

Constructors

TopLevel |

Fields

- tlExport :: ExportType
- tlDoc :: Maybe (Located Text)
- tlValue :: a

#### Instances

Instances details

Foldable TopLevel Source # |

Instance details

Defined in Cryptol.Parser.AST

Methods

fold :: Monoid m => TopLevel m -> m Source #

foldMap :: Monoid m => (a -> m) -> TopLevel a -> m Source #

foldMap' :: Monoid m => (a -> m) -> TopLevel a -> m Source #

foldr :: (a -> b -> b) -> b -> TopLevel a -> b Source #

foldr' :: (a -> b -> b) -> b -> TopLevel a -> b Source #

foldl :: (b -> a -> b) -> b -> TopLevel a -> b Source #

foldl' :: (b -> a -> b) -> b -> TopLevel a -> b Source #

foldr1 :: (a -> a -> a) -> TopLevel a -> a Source #

foldl1 :: (a -> a -> a) -> TopLevel a -> a Source #

toList :: TopLevel a -> [a] Source #

null :: TopLevel a -> Bool Source #

length :: TopLevel a -> Int Source #

elem :: Eq a => a -> TopLevel a -> Bool Source #

maximum :: Ord a => TopLevel a -> a Source #

minimum :: Ord a => TopLevel a -> a Source #

sum :: Num a => TopLevel a -> a Source #

product :: Num a => TopLevel a -> a Source #

Traversable TopLevel Source # |
Instance details Defined in Cryptol.Parser.AST Methods traverse :: Applicative f => (a -> f b) -> TopLevel a -> f (TopLevel b) Source # sequenceA :: Applicative f => TopLevel (f a) -> f (TopLevel a) Source # mapM :: Monad m => (a -> m b) -> TopLevel a -> m (TopLevel b) Source # sequence :: Monad m => TopLevel (m a) -> m (TopLevel a) Source #
Functor TopLevel Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> TopLevel a -> TopLevel b Source # (<$) :: a -> TopLevel b -> TopLevel a Source #
Generic (TopLevel a) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (TopLevel a) :: Type -> Type Source # Methods from :: TopLevel a -> Rep (TopLevel a) x Source # to :: Rep (TopLevel a) x -> TopLevel a Source #
Show a => Show (TopLevel a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> TopLevel a -> ShowS Source # show :: TopLevel a -> String Source # showList :: [TopLevel a] -> ShowS Source #
NoPos a => NoPos (TopLevel a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TopLevel a -> TopLevel a Source #
HasLoc a => HasLoc (TopLevel a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: TopLevel a -> Maybe Range Source #
PP a => PP (TopLevel a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> TopLevel a -> Doc Source #
NFData a => NFData (TopLevel a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: TopLevel a -> () Source #
type Rep (TopLevel a) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (TopLevel a) = D1 ('MetaData "TopLevel" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "TopLevel" 'PrefixI 'True) (S1 ('MetaSel ('Just "tlExport") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExportType) :*: (S1 ('MetaSel ('Just "tlDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Located Text))) :*: S1 ('MetaSel ('Just "tlValue") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))

type Import = ImportG ModName Source #

data ImportG mname Source #

An import declaration.

Constructors

Import |

Fields

- iModule :: !mname
- iAs :: Maybe ModName
- iSpec :: Maybe ImportSpec
- iInst :: !(Maybe (ModuleInstanceArgs PName))

  `iInst` exists only during parsing

#### Instances

Instances details

Generic (ImportG mname) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (ImportG mname) :: Type -> Type Source # Methods from :: ImportG mname -> Rep (ImportG mname) x Source # to :: Rep (ImportG mname) x -> ImportG mname Source #
Show mname => Show (ImportG mname) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ImportG mname -> ShowS Source # show :: ImportG mname -> String Source # showList :: [ImportG mname] -> ShowS Source #
PP mname => PP (ImportG mname) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ImportG mname -> Doc Source #
NFData mname => NFData (ImportG mname) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ImportG mname -> () Source #
type Rep (ImportG mname) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (ImportG mname) = D1 ('MetaData "ImportG" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "Import" 'PrefixI 'True) ((S1 ('MetaSel ('Just "iModule") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 mname) :*: S1 ('MetaSel ('Just "iAs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModName))) :*: (S1 ('MetaSel ('Just "iSpec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ImportSpec)) :*: S1 ('MetaSel ('Just "iInst") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe (ModuleInstanceArgs PName))))))

data ImportSpec Source #

The list of names following an import.

Constructors

Hiding [Ident] |
Only [Ident] |

#### Instances

Instances details

Generic ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep ImportSpec :: Type -> Type Source # Methods from :: ImportSpec -> Rep ImportSpec x Source # to :: Rep ImportSpec x -> ImportSpec Source #
Show ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ImportSpec -> ShowS Source # show :: ImportSpec -> String Source # showList :: [ImportSpec] -> ShowS Source #
PP ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ImportSpec -> Doc Source #
NFData ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ImportSpec -> () Source #
Eq ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: ImportSpec -> ImportSpec -> Bool Source # (/=) :: ImportSpec -> ImportSpec -> Bool Source #
type Rep ImportSpec Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep ImportSpec = D1 ('MetaData "ImportSpec" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "Hiding" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Ident])) :+: C1 ('MetaCons "Only" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Ident])))

data ImpName name Source #

The name of an imported module

Constructors

ImpTop ModName | A top-level module
ImpNested name | The module in scope with the given name

#### Instances

Instances details

Rename ImpName Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: ImpName PName -> RenameM (ImpName Name) Source #
Generic (ImpName name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (ImpName name) :: Type -> Type Source # Methods from :: ImpName name -> Rep (ImpName name) x Source # to :: Rep (ImpName name) x -> ImpName name Source #
Show name => Show (ImpName name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ImpName name -> ShowS Source # show :: ImpName name -> String Source # showList :: [ImpName name] -> ShowS Source #
ModuleInstance name => ModuleInstance (ImpName name) Source # |
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: ImpName name -> ImpName name Source #
PP name => PP (ImpName name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ImpName name -> Doc Source #
NFData name => NFData (ImpName name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ImpName name -> () Source #
Eq name => Eq (ImpName name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: ImpName name -> ImpName name -> Bool Source # (/=) :: ImpName name -> ImpName name -> Bool Source #
Ord name => Ord (ImpName name) Source # |

Instance details

Defined in Cryptol.Parser.AST

Methods

compare :: ImpName name -> ImpName name -> Ordering Source #

(<) :: ImpName name -> ImpName name -> Bool Source #

(<=) :: ImpName name -> ImpName name -> Bool Source #

(>) :: ImpName name -> ImpName name -> Bool Source #

(>=) :: ImpName name -> ImpName name -> Bool Source #

max :: ImpName name -> ImpName name -> ImpName name Source #

min :: ImpName name -> ImpName name -> ImpName name Source #

type Rep (ImpName name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (ImpName name) = D1 ('MetaData "ImpName" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "ImpTop" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModName)) :+: C1 ('MetaCons "ImpNested" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 name)))

data Newtype name Source #

Constructors

Newtype |

Fields

- nName :: Located name

  Type name

- nParams :: [TParam name]

  Type params

- nConName :: !name

  Constructor function name

- nBody :: Rec (Type name)

  Body

#### Instances

Instances details

Rename Newtype Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: Newtype PName -> RenameM (Newtype Name) Source #
Generic (Newtype name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Newtype name) :: Type -> Type Source # Methods from :: Newtype name -> Rep (Newtype name) x Source # to :: Rep (Newtype name) x -> Newtype name Source #
Show name => Show (Newtype name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Newtype name -> ShowS Source # show :: Newtype name -> String Source # showList :: [Newtype name] -> ShowS Source #
BindsNames (InModule (Newtype PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (Newtype PName) -> BuildNamingEnv
NoPos (Newtype name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Newtype name -> Newtype name Source #
HasLoc (Newtype name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: Newtype name -> Maybe Range Source #
PPName name => PP (Newtype name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Newtype name -> Doc Source #
NFData name => NFData (Newtype name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Newtype name -> () Source #
Eq name => Eq (Newtype name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Newtype name -> Newtype name -> Bool Source # (/=) :: Newtype name -> Newtype name -> Bool Source #
type Rep (Newtype name) Source # |
Instance details Defined in Cryptol.Parser.AST type Rep (Newtype name)

data PrimType name Source #

A declaration for a type with no implementation.

Constructors

PrimType |

Fields

- primTName :: Located name
- primTKind :: Located Kind
- primTCts :: ([TParam name], [Prop name])

  parameters are in the order used by the type constructor.

- primTFixity :: Maybe Fixity

#### Instances

Instances details

Rename PrimType Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: PrimType PName -> RenameM (PrimType Name) Source #
Generic (PrimType name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (PrimType name) :: Type -> Type Source # Methods from :: PrimType name -> Rep (PrimType name) x Source # to :: Rep (PrimType name) x -> PrimType name Source #
Show name => Show (PrimType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> PrimType name -> ShowS Source # show :: PrimType name -> String Source # showList :: [PrimType name] -> ShowS Source #
BindsNames (InModule (PrimType PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (PrimType PName) -> BuildNamingEnv
NoPos (PrimType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: PrimType name -> PrimType name Source #
HasLoc (PrimType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: PrimType name -> Maybe Range Source #
(Show name, PPName name) => PP (PrimType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> PrimType name -> Doc Source #
NFData name => NFData (PrimType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: PrimType name -> () Source #
type Rep (PrimType name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (PrimType name) = D1 ('MetaData "PrimType" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "PrimType" 'PrefixI 'True) ((S1 ('MetaSel ('Just "primTName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located name)) :*: S1 ('MetaSel ('Just "primTKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located Kind))) :*: (S1 ('MetaSel ('Just "primTCts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ([TParam name], [Prop name])) :*: S1 ('MetaSel ('Just "primTFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity)))))

data ParameterType name Source #

A type parameter for a module.

Constructors

ParameterType |

Fields

- ptName :: Located name

  name of type parameter

- ptKind :: Kind

  kind of parameter

- ptDoc :: Maybe Text

  optional documentation

- ptFixity :: Maybe Fixity

  info for infix use

- ptNumber :: !Int

  number of the parameter

#### Instances

Instances details

Rename ParameterType Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: ParameterType PName -> RenameM (ParameterType Name) Source #
Generic (ParameterType name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (ParameterType name) :: Type -> Type Source # Methods from :: ParameterType name -> Rep (ParameterType name) x Source # to :: Rep (ParameterType name) x -> ParameterType name Source #
Show name => Show (ParameterType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ParameterType name -> ShowS Source # show :: ParameterType name -> String Source # showList :: [ParameterType name] -> ShowS Source #
BindsNames (InModule (ParameterType PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (ParameterType PName) -> BuildNamingEnv
NoPos (ParameterType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ParameterType name -> ParameterType name Source #
HasLoc (ParameterType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: ParameterType name -> Maybe Range Source #
(Show name, PPName name) => PP (ParameterType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ParameterType name -> Doc Source #
NFData name => NFData (ParameterType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ParameterType name -> () Source #
Eq name => Eq (ParameterType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: ParameterType name -> ParameterType name -> Bool Source # (/=) :: ParameterType name -> ParameterType name -> Bool Source #
type Rep (ParameterType name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (ParameterType name) = D1 ('MetaData "ParameterType" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "ParameterType" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ptName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located name)) :*: S1 ('MetaSel ('Just "ptKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :*: (S1 ('MetaSel ('Just "ptDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text)) :*: (S1 ('MetaSel ('Just "ptFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity)) :*: S1 ('MetaSel ('Just "ptNumber") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))))

data ParameterFun name Source #

A value parameter for a module.

Constructors

ParameterFun |

Fields

- pfName :: Located name

  name of value parameter

- pfSchema :: Schema name

  schema for parameter

- pfDoc :: Maybe Text

  optional documentation

- pfFixity :: Maybe Fixity

  info for infix use

#### Instances

Instances details

Rename ParameterFun Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: ParameterFun PName -> RenameM (ParameterFun Name) Source #
Generic (ParameterFun name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (ParameterFun name) :: Type -> Type Source # Methods from :: ParameterFun name -> Rep (ParameterFun name) x Source # to :: Rep (ParameterFun name) x -> ParameterFun name Source #
Show name => Show (ParameterFun name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ParameterFun name -> ShowS Source # show :: ParameterFun name -> String Source # showList :: [ParameterFun name] -> ShowS Source #
BindsNames (InModule (ParameterFun PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (ParameterFun PName) -> BuildNamingEnv
NoPos (ParameterFun x) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ParameterFun x -> ParameterFun x Source #
HasLoc (ParameterFun name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: ParameterFun name -> Maybe Range Source #
(Show name, PPName name) => PP (ParameterFun name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ParameterFun name -> Doc Source #
NFData name => NFData (ParameterFun name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ParameterFun name -> () Source #
Eq name => Eq (ParameterFun name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: ParameterFun name -> ParameterFun name -> Bool Source # (/=) :: ParameterFun name -> ParameterFun name -> Bool Source #
type Rep (ParameterFun name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (ParameterFun name) = D1 ('MetaData "ParameterFun" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "ParameterFun" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pfName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located name)) :*: S1 ('MetaSel ('Just "pfSchema") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Schema name))) :*: (S1 ('MetaSel ('Just "pfDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text)) :*: S1 ('MetaSel ('Just "pfFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity)))))

newtype NestedModule name Source #

A nested module.

Constructors

NestedModule (ModuleG name name) |

#### Instances

Instances details

Rename NestedModule Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: NestedModule PName -> RenameM (NestedModule Name) Source #
Generic (NestedModule name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (NestedModule name) :: Type -> Type Source # Methods from :: NestedModule name -> Rep (NestedModule name) x Source # to :: Rep (NestedModule name) x -> NestedModule name Source #
Show name => Show (NestedModule name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> NestedModule name -> ShowS Source # show :: NestedModule name -> String Source # showList :: [NestedModule name] -> ShowS Source #
BindsNames (InModule (NestedModule PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (NestedModule PName) -> BuildNamingEnv
NoPos (NestedModule name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: NestedModule name -> NestedModule name Source #
RemovePatterns (NestedModule PName) Source # |
Instance details Defined in Cryptol.Parser.NoPat Methods removePatterns :: NestedModule PName -> (NestedModule PName, [Error]) Source #
HasLoc (NestedModule name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: NestedModule name -> Maybe Range Source #
(Show name, PPName name) => PP (NestedModule name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> NestedModule name -> Doc Source #
NFData name => NFData (NestedModule name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: NestedModule name -> () Source #
type Rep (NestedModule name) Source # |
Instance details Defined in Cryptol.Parser.AST type Rep (NestedModule name) = D1 ('MetaData "NestedModule" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'True) (C1 ('MetaCons "NestedModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ModuleG name name))))

data Signature name Source #

Interface Modules (aka types of functor arguments)

IMPORTANT: Interface Modules are a language construct and are different from the notion of "interface" in the Cryptol implementation.

Note that the names *defined* in an interface module are only really used in the other members of the interface module. When an interface module is "imported" as a functor parameter these names are instantiated to new names, because there could be multiple paramers using the same interface.

Constructors

Signature |

Fields

- sigImports :: ![Located (ImportG (ImpName name))]

  Add things in scope

- sigTypeParams :: [ParameterType name]

  Type parameters

- sigConstraints :: [Located (Prop name)]

  Constraints on the type parameters and type synonyms.

- sigDecls :: [SigDecl name]

  Type and constraint synonyms

- sigFunParams :: [ParameterFun name]

  Value parameters

#### Instances

Instances details

Generic (Signature name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Signature name) :: Type -> Type Source # Methods from :: Signature name -> Rep (Signature name) x Source # to :: Rep (Signature name) x -> Signature name Source #
Show name => Show (Signature name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Signature name -> ShowS Source # show :: Signature name -> String Source # showList :: [Signature name] -> ShowS Source #
NoPos (Signature name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Signature name -> Signature name Source #
NFData name => NFData (Signature name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Signature name -> () Source #
type Rep (Signature name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (Signature name) = D1 ('MetaData "Signature" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "Signature" 'PrefixI 'True) ((S1 ('MetaSel ('Just "sigImports") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Located (ImportG (ImpName name))]) :*: S1 ('MetaSel ('Just "sigTypeParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ParameterType name])) :*: (S1 ('MetaSel ('Just "sigConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located (Prop name)]) :*: (S1 ('MetaSel ('Just "sigDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SigDecl name]) :*: S1 ('MetaSel ('Just "sigFunParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ParameterFun name])))))

data SigDecl name Source #

A constraint or type synonym declared in an interface.

Constructors

SigTySyn (TySyn name) (Maybe Text) |
SigPropSyn (PropSyn name) (Maybe Text) |

#### Instances

Instances details

Rename SigDecl Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: SigDecl PName -> RenameM (SigDecl Name) Source #
Generic (SigDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (SigDecl name) :: Type -> Type Source # Methods from :: SigDecl name -> Rep (SigDecl name) x Source # to :: Rep (SigDecl name) x -> SigDecl name Source #
Show name => Show (SigDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> SigDecl name -> ShowS Source # show :: SigDecl name -> String Source # showList :: [SigDecl name] -> ShowS Source #
BindsNames (InModule (SigDecl PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods namingEnv :: InModule (SigDecl PName) -> BuildNamingEnv
NoPos (SigDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: SigDecl name -> SigDecl name Source #
HasLoc (SigDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: SigDecl name -> Maybe Range Source #
(Show name, PPName name) => PP (SigDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> SigDecl name -> Doc Source #
NFData name => NFData (SigDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: SigDecl name -> () Source #
type Rep (SigDecl name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (SigDecl name) = D1 ('MetaData "SigDecl" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "SigTySyn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TySyn name)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text))) :+: C1 ('MetaCons "SigPropSyn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (PropSyn name)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text))))

data ModParam name Source #

A module parameter declaration.

    import interface A
    import interface A as B

The name of the parameter is derived from the `as` clause. If there is no `as` clause then it is derived from the name of the interface module.

If there is no `as` clause, then the type/value parameters are unqualified, and otherwise they are qualified.

Constructors

ModParam |

Fields

- mpSignature :: Located (ImpName name)

  Signature for parameter

- mpAs :: Maybe ModName

  Qualified for actual params

- mpName :: !Ident

  Parameter name (for inst.) Note that this is not resolved in the renamer, and is only used when instantiating a functor.

- mpDoc :: Maybe (Located Text)

  Optional documentation

- mpRenaming :: !(Map name name)

  Filled in by the renamer. Maps the actual (value/type) parameter names to the names in the interface module.

#### Instances

Instances details

Rename ModParam Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: ModParam PName -> RenameM (ModParam Name) Source #
Generic (ModParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (ModParam name) :: Type -> Type Source # Methods from :: ModParam name -> Rep (ModParam name) x Source # to :: Rep (ModParam name) x -> ModParam name Source #
Show name => Show (ModParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ModParam name -> ShowS Source # show :: ModParam name -> String Source # showList :: [ModParam name] -> ShowS Source #
NoPos (ModParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ModParam name -> ModParam name Source #
HasLoc (ModParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: ModParam name -> Maybe Range Source #
(Show name, PPName name) => PP (ModParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ModParam name -> Doc Source #
NFData name => NFData (ModParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ModParam name -> () Source #
Eq name => Eq (ModParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: ModParam name -> ModParam name -> Bool Source # (/=) :: ModParam name -> ModParam name -> Bool Source #
type Rep (ModParam name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (ModParam name) = D1 ('MetaData "ModParam" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "ModParam" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mpSignature") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located (ImpName name))) :*: S1 ('MetaSel ('Just "mpAs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModName))) :*: (S1 ('MetaSel ('Just "mpName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Ident) :*: (S1 ('MetaSel ('Just "mpDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Located Text))) :*: S1 ('MetaSel ('Just "mpRenaming") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map name name))))))

data ParamDecl name Source #

Things that maybe appear in an interface/parameter block. These only exist during parsering.

Constructors

DParameterType (ParameterType name) | `parameter type T : #` (parser only)
DParameterFun (ParameterFun name) | `parameter someVal : [256]` (parser only)
DParameterDecl (SigDecl name) | A delcaration in an interface

DParameterConstraint [Located (Prop name)]

    parameter type constraint (fin T)

#### Instances

Instances details

Generic (ParamDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (ParamDecl name) :: Type -> Type Source # Methods from :: ParamDecl name -> Rep (ParamDecl name) x Source # to :: Rep (ParamDecl name) x -> ParamDecl name Source #
Show name => Show (ParamDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ParamDecl name -> ShowS Source # show :: ParamDecl name -> String Source # showList :: [ParamDecl name] -> ShowS Source #
NoPos (ParamDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ParamDecl name -> ParamDecl name Source #
HasLoc (ParamDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: ParamDecl name -> Maybe Range Source #
(Show name, PPName name) => PP (ParamDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ParamDecl name -> Doc Source #
NFData name => NFData (ParamDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ParamDecl name -> () Source #
type Rep (ParamDecl name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (ParamDecl name) = D1 ('MetaData "ParamDecl" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) ((C1 ('MetaCons "DParameterType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ParameterType name))) :+: C1 ('MetaCons "DParameterFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ParameterFun name)))) :+: (C1 ('MetaCons "DParameterDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SigDecl name))) :+: C1 ('MetaCons "DParameterConstraint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located (Prop name)]))))

data PropGuardCase name Source #

Constructors

PropGuardCase |

Fields

- pgcProps :: [Located (Prop name)]
- pgcExpr :: Expr name

#### Instances

Instances details

Functor PropGuardCase Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> PropGuardCase a -> PropGuardCase b Source # (<$) :: a -> PropGuardCase b -> PropGuardCase a Source #
Rename PropGuardCase Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: PropGuardCase PName -> RenameM (PropGuardCase Name) Source #
Generic (PropGuardCase name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (PropGuardCase name) :: Type -> Type Source # Methods from :: PropGuardCase name -> Rep (PropGuardCase name) x Source # to :: Rep (PropGuardCase name) x -> PropGuardCase name Source #
Show name => Show (PropGuardCase name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> PropGuardCase name -> ShowS Source # show :: PropGuardCase name -> String Source # showList :: [PropGuardCase name] -> ShowS Source #
NFData name => NFData (PropGuardCase name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: PropGuardCase name -> () Source #
Eq name => Eq (PropGuardCase name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: PropGuardCase name -> PropGuardCase name -> Bool Source # (/=) :: PropGuardCase name -> PropGuardCase name -> Bool Source #
type Rep (PropGuardCase name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (PropGuardCase name) = D1 ('MetaData "PropGuardCase" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "PropGuardCase" 'PrefixI 'True) (S1 ('MetaSel ('Just "pgcProps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located (Prop name)]) :*: S1 ('MetaSel ('Just "pgcExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr name))))

# Interactive

data ReplInput name Source #

Input at the REPL, which can be an expression, a `let` statement, or empty (possibly a comment).

Constructors

ExprInput (Expr name) |
LetInput [Decl name] |
EmptyInput |

#### Instances

Instances details

Show name => Show (ReplInput name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ReplInput name -> ShowS Source # show :: ReplInput name -> String Source # showList :: [ReplInput name] -> ShowS Source #
Eq name => Eq (ReplInput name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: ReplInput name -> ReplInput name -> Bool Source # (/=) :: ReplInput name -> ReplInput name -> Bool Source #

# Expressions

data Expr n Source #

Constructors

EVar n

     x

ELit Literal

     0x10

EGenerate (Expr n)

     generate f

ETuple [Expr n]

     (1,2,3)

ERecord (Rec (Expr n))

     { x = 1, y = 2 }

ESel (Expr n) Selector

     e.l

EUpd (Maybe (Expr n)) [UpdField n]

     { r | x = e }

EList [Expr n]

     [1,2,3]

EFromTo (Type n) (Maybe (Type n)) (Type n) (Maybe (Type n))

     [1, 5 .. 117 : t]

EFromToBy Bool (Type n) (Type n) (Type n) (Maybe (Type n))

     [1 .. 10 by 2 : t ]

EFromToDownBy Bool (Type n) (Type n) (Type n) (Maybe (Type n))

     [10 .. 1 down by 2 : t ]

EFromToLessThan (Type n) (Type n) (Maybe (Type n))

     [ 1 .. < 10 : t ]

EInfFrom |

Fields

- (Expr n)
- (Maybe (Expr n))

       [1, 3 ...]

EComp (Expr n) [[Match n]]

     [ 1 | x <- xs ]

EApp (Expr n) (Expr n)

     f x

EAppT (Expr n) [TypeInst n]

     f `{x = 8}, f`{8}

EIf (Expr n) (Expr n) (Expr n)

     if ok then e1 else e2

EWhere (Expr n) [Decl n]

     1 + x where { x = 2 }

ETyped (Expr n) (Type n)

     1 : [8]

ETypeVal (Type n) | ``(x + 1)`, `x` is a type

EFun (FunDesc n) [Pattern n] (Expr n)

     \x y -> x

ELocated (Expr n) Range | position annotation
ESplit (Expr n) | `splitAt x` (Introduced by NoPat)
EParens (Expr n) | `(e)` (Removed by Fixity)
EInfix |

Fields

- (Expr n)
- (Located n)
- Fixity
- (Expr n)

  `a + b` (Removed by Fixity)

EPrefix PrefixOp (Expr n)

     -1, ~1

#### Instances

Instances details

Functor Expr Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Expr a -> Expr b Source # (<$) :: a -> Expr b -> Expr a Source #
Rename Expr Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: Expr PName -> RenameM (Expr Name) Source #
Generic (Expr n) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Expr n) :: Type -> Type Source # Methods from :: Expr n -> Rep (Expr n) x Source # to :: Rep (Expr n) x -> Expr n Source #
Show n => Show (Expr n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Expr n -> ShowS Source # show :: Expr n -> String Source # showList :: [Expr n] -> ShowS Source #
NoPos (Expr name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Expr name -> Expr name Source #
RemovePatterns (Expr PName) Source # |
Instance details Defined in Cryptol.Parser.NoPat Methods removePatterns :: Expr PName -> (Expr PName, [Error]) Source #
AddLoc (Expr n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods addLoc :: Expr n -> Range -> Expr n Source # dropLoc :: Expr n -> Expr n Source #
HasLoc (Expr name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: Expr name -> Maybe Range Source #
(Show name, PPName name) => PP (Expr name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Expr name -> Doc Source #
NFData n => NFData (Expr n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Expr n -> () Source #
Eq n => Eq (Expr n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Expr n -> Expr n -> Bool Source # (/=) :: Expr n -> Expr n -> Bool Source #
type Rep (Expr n) Source # |
Instance details Defined in Cryptol.Parser.AST type Rep (Expr n)

data Literal Source #

Literals.

Constructors

ECNum Integer NumInfo | `0x10` (HexLit 2)

ECChar Char

    a

ECFrac Rational FracInfo

    1.2e3

ECString String

    "hello"

#### Instances

Instances details

Generic Literal Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep Literal :: Type -> Type Source # Methods from :: Literal -> Rep Literal x Source # to :: Rep Literal x -> Literal Source #
Show Literal Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Literal -> ShowS Source # show :: Literal -> String Source # showList :: [Literal] -> ShowS Source #
PP Literal Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Literal -> Doc Source #
NFData Literal Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Literal -> () Source #
Eq Literal Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Literal -> Literal -> Bool Source # (/=) :: Literal -> Literal -> Bool Source #
type Rep Literal Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep Literal = D1 ('MetaData "Literal" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) ((C1 ('MetaCons "ECNum" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NumInfo)) :+: C1 ('MetaCons "ECChar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Char))) :+: (C1 ('MetaCons "ECFrac" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Rational) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FracInfo)) :+: C1 ('MetaCons "ECString" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))

data NumInfo Source #

Infromation about the representation of a numeric constant.

Constructors

BinLit Text Int | n-digit binary literal
OctLit Text Int | n-digit octal literal
DecLit Text | overloaded decimal literal
HexLit Text Int | n-digit hex literal
PolyLit Int | polynomial literal

#### Instances

Instances details

Generic NumInfo Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep NumInfo :: Type -> Type Source # Methods from :: NumInfo -> Rep NumInfo x Source # to :: Rep NumInfo x -> NumInfo Source #
Show NumInfo Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> NumInfo -> ShowS Source # show :: NumInfo -> String Source # showList :: [NumInfo] -> ShowS Source #
NFData NumInfo Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: NumInfo -> () Source #
Eq NumInfo Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: NumInfo -> NumInfo -> Bool Source # (/=) :: NumInfo -> NumInfo -> Bool Source #
type Rep NumInfo Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep NumInfo = D1 ('MetaData "NumInfo" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) ((C1 ('MetaCons "BinLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "OctLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :+: (C1 ('MetaCons "DecLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :+: (C1 ('MetaCons "HexLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "PolyLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))))

data FracInfo Source #

Information about fractional literals.

Constructors

BinFrac Text |
OctFrac Text |
DecFrac Text |
HexFrac Text |

#### Instances

Instances details

Generic FracInfo Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep FracInfo :: Type -> Type Source # Methods from :: FracInfo -> Rep FracInfo x Source # to :: Rep FracInfo x -> FracInfo Source #
Show FracInfo Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> FracInfo -> ShowS Source # show :: FracInfo -> String Source # showList :: [FracInfo] -> ShowS Source #
NFData FracInfo Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: FracInfo -> () Source #
Eq FracInfo Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: FracInfo -> FracInfo -> Bool Source # (/=) :: FracInfo -> FracInfo -> Bool Source #
type Rep FracInfo Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep FracInfo = D1 ('MetaData "FracInfo" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) ((C1 ('MetaCons "BinFrac" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :+: C1 ('MetaCons "OctFrac" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text))) :+: (C1 ('MetaCons "DecFrac" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :+: C1 ('MetaCons "HexFrac" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text))))

data Match name Source #

Constructors

Match (Pattern name) (Expr name) | p <- e
MatchLet (Bind name) |

#### Instances

Instances details

Functor Match Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Match a -> Match b Source # (<$) :: a -> Match b -> Match a Source #
Rename Match Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: Match PName -> RenameM (Match Name) Source #
Generic (Match name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Match name) :: Type -> Type Source # Methods from :: Match name -> Rep (Match name) x Source # to :: Rep (Match name) x -> Match name Source #
Show name => Show (Match name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Match name -> ShowS Source # show :: Match name -> String Source # showList :: [Match name] -> ShowS Source #
NoPos (Match name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Match name -> Match name Source #
HasLoc (Match name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: Match name -> Maybe Range Source #
(Show name, PPName name) => PP (Match name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Match name -> Doc Source #
NFData name => NFData (Match name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Match name -> () Source #
Eq name => Eq (Match name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Match name -> Match name -> Bool Source # (/=) :: Match name -> Match name -> Bool Source #
type Rep (Match name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (Match name) = D1 ('MetaData "Match" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "Match" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern name)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr name))) :+: C1 ('MetaCons "MatchLet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Bind name))))

data Pattern n Source #

Constructors

PVar (Located n)

     x

PWild

     _

PTuple [Pattern n]

     (x,y,z)

PRecord (Rec (Pattern n))

     { x = (a,b,c), y = z }

PList [Pattern n]

     [ x, y, z ]

PTyped (Pattern n) (Type n)

     x : [8]

PSplit |

Fields

- (Pattern n)
- (Pattern n)

       (x # y)

PLocated (Pattern n) Range | Location information

#### Instances

Instances details

Functor Pattern Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Pattern a -> Pattern b Source # (<$) :: a -> Pattern b -> Pattern a Source #
Rename Pattern Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: Pattern PName -> RenameM (Pattern Name) Source #
Generic (Pattern n) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Pattern n) :: Type -> Type Source # Methods from :: Pattern n -> Rep (Pattern n) x Source # to :: Rep (Pattern n) x -> Pattern n Source #
Show n => Show (Pattern n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Pattern n -> ShowS Source # show :: Pattern n -> String Source # showList :: [Pattern n] -> ShowS Source #
NoPos (Pattern name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Pattern name -> Pattern name Source #
AddLoc (Pattern name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods addLoc :: Pattern name -> Range -> Pattern name Source # dropLoc :: Pattern name -> Pattern name Source #
HasLoc (Pattern name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: Pattern name -> Maybe Range Source #
PPName name => PP (Pattern name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Pattern name -> Doc Source #
NFData n => NFData (Pattern n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Pattern n -> () Source #
Eq n => Eq (Pattern n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Pattern n -> Pattern n -> Bool Source # (/=) :: Pattern n -> Pattern n -> Bool Source #
type Rep (Pattern n) Source # |
Instance details Defined in Cryptol.Parser.AST type Rep (Pattern n)

data Selector Source #

Selectors are used for projecting from various components. Each selector has an option spec to specify the shape of the thing that is being selected. Currently, there is no surface syntax for list selectors, but they are used during the desugaring of patterns.

Constructors

TupleSel Int (Maybe Int) | Zero-based tuple selection. Optionally specifies the shape of the tuple (one-based).
RecordSel Ident (Maybe [Ident]) | Record selection. Optionally specifies the shape of the record.
ListSel Int (Maybe Int) | List selection. Optionally specifies the length of the list.

#### Instances

Instances details

Generic Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Associated Types type Rep Selector :: Type -> Type Source # Methods from :: Selector -> Rep Selector x Source # to :: Rep Selector x -> Selector Source #
Show Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Methods showsPrec :: Int -> Selector -> ShowS Source # show :: Selector -> String Source # showList :: [Selector] -> ShowS Source #
ShowParseable Selector Source # |
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Selector -> Doc Void Source #
PP Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Methods ppPrec :: Int -> Selector -> Doc Source #
NFData Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Methods rnf :: Selector -> () Source #
Eq Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Methods (==) :: Selector -> Selector -> Bool Source # (/=) :: Selector -> Selector -> Bool Source #
Ord Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Methods compare :: Selector -> Selector -> Ordering Source # (<) :: Selector -> Selector -> Bool Source # (<=) :: Selector -> Selector -> Bool Source # (>) :: Selector -> Selector -> Bool Source # (>=) :: Selector -> Selector -> Bool Source # max :: Selector -> Selector -> Selector Source # min :: Selector -> Selector -> Selector Source #
type Rep Selector Source # |

Instance details

Defined in Cryptol.Parser.Selector

type Rep Selector = D1 ('MetaData "Selector" "Cryptol.Parser.Selector" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "TupleSel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int))) :+: (C1 ('MetaCons "RecordSel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [Ident]))) :+: C1 ('MetaCons "ListSel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)))))

data TypeInst name Source #

Constructors

NamedInst (Named (Type name)) |
PosInst (Type name) |

#### Instances

Instances details

Functor TypeInst Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> TypeInst a -> TypeInst b Source # (<$) :: a -> TypeInst b -> TypeInst a Source #
Rename TypeInst Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: TypeInst PName -> RenameM (TypeInst Name) Source #
Generic (TypeInst name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (TypeInst name) :: Type -> Type Source # Methods from :: TypeInst name -> Rep (TypeInst name) x Source # to :: Rep (TypeInst name) x -> TypeInst name Source #
Show name => Show (TypeInst name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> TypeInst name -> ShowS Source # show :: TypeInst name -> String Source # showList :: [TypeInst name] -> ShowS Source #
NoPos (TypeInst name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TypeInst name -> TypeInst name Source #
PPName name => PP (TypeInst name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> TypeInst name -> Doc Source #
NFData name => NFData (TypeInst name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: TypeInst name -> () Source #
Eq name => Eq (TypeInst name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: TypeInst name -> TypeInst name -> Bool Source # (/=) :: TypeInst name -> TypeInst name -> Bool Source #
type Rep (TypeInst name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (TypeInst name) = D1 ('MetaData "TypeInst" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "NamedInst" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Named (Type name)))) :+: C1 ('MetaCons "PosInst" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type name))))

data UpdField n Source #

Constructors

UpdField UpdHow [Located Selector] (Expr n) | non-empty list `x.y = e`

#### Instances

Instances details

Functor UpdField Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> UpdField a -> UpdField b Source # (<$) :: a -> UpdField b -> UpdField a Source #
Rename UpdField Source # | Note that after this point the `->` updates have an explicit function and there are no more nested updates.
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: UpdField PName -> RenameM (UpdField Name) Source #
Generic (UpdField n) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (UpdField n) :: Type -> Type Source # Methods from :: UpdField n -> Rep (UpdField n) x Source # to :: Rep (UpdField n) x -> UpdField n Source #
Show n => Show (UpdField n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> UpdField n -> ShowS Source # show :: UpdField n -> String Source # showList :: [UpdField n] -> ShowS Source #
NoPos (UpdField name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: UpdField name -> UpdField name Source #
(Show name, PPName name) => PP (UpdField name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> UpdField name -> Doc Source #
NFData n => NFData (UpdField n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: UpdField n -> () Source #
Eq n => Eq (UpdField n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: UpdField n -> UpdField n -> Bool Source # (/=) :: UpdField n -> UpdField n -> Bool Source #
type Rep (UpdField n) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (UpdField n) = D1 ('MetaData "UpdField" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "UpdField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UpdHow) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located Selector]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n)))))

data UpdHow Source #

Constructors

UpdSet |
UpdFun | Are we setting or updating a field.

#### Instances

Instances details

Generic UpdHow Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep UpdHow :: Type -> Type Source # Methods from :: UpdHow -> Rep UpdHow x Source # to :: Rep UpdHow x -> UpdHow Source #
Show UpdHow Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> UpdHow -> ShowS Source # show :: UpdHow -> String Source # showList :: [UpdHow] -> ShowS Source #
PP UpdHow Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> UpdHow -> Doc Source #
NFData UpdHow Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: UpdHow -> () Source #
Eq UpdHow Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: UpdHow -> UpdHow -> Bool Source # (/=) :: UpdHow -> UpdHow -> Bool Source #
type Rep UpdHow Source # |
Instance details Defined in Cryptol.Parser.AST type Rep UpdHow = D1 ('MetaData "UpdHow" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "UpdSet" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UpdFun" 'PrefixI 'False) (U1 :: Type -> Type))

data FunDesc n Source #

Description of functions. Only trivial information is provided here by the parser. The NoPat pass fills this in as required.

Constructors

FunDesc |

Fields

- funDescrName :: Maybe n

  Name of this function, if it has one

- funDescrArgOffset :: Int

  number of previous arguments to this function bound in surrounding lambdas (defaults to 0)

#### Instances

Instances details

Functor FunDesc Source # |
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> FunDesc a -> FunDesc b Source # (<$) :: a -> FunDesc b -> FunDesc a Source #
Rename FunDesc Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: FunDesc PName -> RenameM (FunDesc Name) Source #
Generic (FunDesc n) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (FunDesc n) :: Type -> Type Source # Methods from :: FunDesc n -> Rep (FunDesc n) x Source # to :: Rep (FunDesc n) x -> FunDesc n Source #
Show n => Show (FunDesc n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> FunDesc n -> ShowS Source # show :: FunDesc n -> String Source # showList :: [FunDesc n] -> ShowS Source #
NFData n => NFData (FunDesc n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: FunDesc n -> () Source #
Eq n => Eq (FunDesc n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: FunDesc n -> FunDesc n -> Bool Source # (/=) :: FunDesc n -> FunDesc n -> Bool Source #
type Rep (FunDesc n) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (FunDesc n) = D1 ('MetaData "FunDesc" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "FunDesc" 'PrefixI 'True) (S1 ('MetaSel ('Just "funDescrName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe n)) :*: S1 ('MetaSel ('Just "funDescrArgOffset") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

emptyFunDesc :: FunDesc n Source #

data PrefixOp Source #

Prefix operator.

Constructors

PrefixNeg

     -

PrefixComplement

     ~

#### Instances

Instances details

Generic PrefixOp Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep PrefixOp :: Type -> Type Source # Methods from :: PrefixOp -> Rep PrefixOp x Source # to :: Rep PrefixOp x -> PrefixOp Source #
Show PrefixOp Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> PrefixOp -> ShowS Source # show :: PrefixOp -> String Source # showList :: [PrefixOp] -> ShowS Source #
NFData PrefixOp Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: PrefixOp -> () Source #
Eq PrefixOp Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: PrefixOp -> PrefixOp -> Bool Source # (/=) :: PrefixOp -> PrefixOp -> Bool Source #
type Rep PrefixOp Source # |
Instance details Defined in Cryptol.Parser.AST type Rep PrefixOp = D1 ('MetaData "PrefixOp" "Cryptol.Parser.AST" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "PrefixNeg" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrefixComplement" 'PrefixI 'False) (U1 :: Type -> Type))

prefixFixity :: PrefixOp -> Fixity Source #

asEApps :: Expr n -> (Expr n, [Expr n]) Source #

# Positions

data Located a Source #

Constructors

Located |

Fields

- srcRange :: !Range
- thing :: !a

#### Instances

Instances details

Foldable Located Source # |

Instance details

Defined in Cryptol.Parser.Position

Methods

fold :: Monoid m => Located m -> m Source #

foldMap :: Monoid m => (a -> m) -> Located a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Located a -> m Source #

foldr :: (a -> b -> b) -> b -> Located a -> b Source #

foldr' :: (a -> b -> b) -> b -> Located a -> b Source #

foldl :: (b -> a -> b) -> b -> Located a -> b Source #

foldl' :: (b -> a -> b) -> b -> Located a -> b Source #

foldr1 :: (a -> a -> a) -> Located a -> a Source #

foldl1 :: (a -> a -> a) -> Located a -> a Source #

toList :: Located a -> [a] Source #

null :: Located a -> Bool Source #

length :: Located a -> Int Source #

elem :: Eq a => a -> Located a -> Bool Source #

maximum :: Ord a => Located a -> a Source #

minimum :: Ord a => Located a -> a Source #

sum :: Num a => Located a -> a Source #

product :: Num a => Located a -> a Source #

Traversable Located Source # |
Instance details Defined in Cryptol.Parser.Position Methods traverse :: Applicative f => (a -> f b) -> Located a -> f (Located b) Source # sequenceA :: Applicative f => Located (f a) -> f (Located a) Source # mapM :: Monad m => (a -> m b) -> Located a -> m (Located b) Source # sequence :: Monad m => Located (m a) -> m (Located a) Source #
Functor Located Source # |
Instance details Defined in Cryptol.Parser.Position Methods fmap :: (a -> b) -> Located a -> Located b Source # (<$) :: a -> Located b -> Located a Source #
Generic (Located a) Source # |
Instance details Defined in Cryptol.Parser.Position Associated Types type Rep (Located a) :: Type -> Type Source # Methods from :: Located a -> Rep (Located a) x Source # to :: Rep (Located a) x -> Located a Source #
Show a => Show (Located a) Source # |
Instance details Defined in Cryptol.Parser.Position Methods showsPrec :: Int -> Located a -> ShowS Source # show :: Located a -> String Source # showList :: [Located a] -> ShowS Source #
TraverseNames a => TraverseNames (Located a) Source # |
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => Located a -> f (Located a) Source #
NoPos (Located t) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Located t -> Located t Source #
AddLoc (Located a) Source # |
Instance details Defined in Cryptol.Parser.Position Methods addLoc :: Located a -> Range -> Located a Source # dropLoc :: Located a -> Located a Source #
HasLoc (Located a) Source # |
Instance details Defined in Cryptol.Parser.Position Methods getLoc :: Located a -> Maybe Range Source #
ModuleInstance a => ModuleInstance (Located a) Source # |
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: Located a -> Located a Source #
ShowParseable a => ShowParseable (Located a) Source # |
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Located a -> Doc Void Source #
PP a => PP (Located a) Source # |
Instance details Defined in Cryptol.Parser.Position Methods ppPrec :: Int -> Located a -> Doc Source #
PPName a => PPName (Located a) Source # |
Instance details Defined in Cryptol.Parser.Position Methods ppNameFixity :: Located a -> Maybe Fixity Source # ppPrefixName :: Located a -> Doc Source # ppInfixName :: Located a -> Doc Source #
NFData a => NFData (Located a) Source # |
Instance details Defined in Cryptol.Parser.Position Methods rnf :: Located a -> () Source #
Eq a => Eq (Located a) Source # |
Instance details Defined in Cryptol.Parser.Position Methods (==) :: Located a -> Located a -> Bool Source # (/=) :: Located a -> Located a -> Bool Source #
Ord a => Ord (Located a) Source # |

Instance details

Defined in Cryptol.Parser.Position

Methods

compare :: Located a -> Located a -> Ordering Source #

(<) :: Located a -> Located a -> Bool Source #

(<=) :: Located a -> Located a -> Bool Source #

(>) :: Located a -> Located a -> Bool Source #

(>=) :: Located a -> Located a -> Bool Source #

max :: Located a -> Located a -> Located a Source #

min :: Located a -> Located a -> Located a Source #

type Rep (Located a) Source # |

Instance details

Defined in Cryptol.Parser.Position

type Rep (Located a) = D1 ('MetaData "Located" "Cryptol.Parser.Position" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "Located" 'PrefixI 'True) (S1 ('MetaSel ('Just "srcRange") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Range) :*: S1 ('MetaSel ('Just "thing") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a)))

type LPName = Located PName Source #

A name with location information.

type LString = Located String Source #

A string with location information.

type LIdent = Located Ident Source #

An identifier with location information.

class NoPos t where Source #

Methods

noPos :: t -> t Source #

#### Instances

Instances details

NoPos Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Pragma -> Pragma Source #
NoPos Range Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Range -> Range Source #
NoPos (Bind name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Bind name -> Bind name Source #
NoPos (Decl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Decl name -> Decl name Source #
NoPos (Expr name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Expr name -> Expr name Source #
NoPos (Match name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Match name -> Match name Source #
NoPos (ModParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ModParam name -> ModParam name Source #
NoPos (ModuleDefinition name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ModuleDefinition name -> ModuleDefinition name Source #
NoPos (ModuleInstanceArgs name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ModuleInstanceArgs name -> ModuleInstanceArgs name Source #
NoPos (ModuleInstanceNamedArg name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ModuleInstanceNamedArg name -> ModuleInstanceNamedArg name Source #
NoPos t => NoPos (Named t) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Named t -> Named t Source #
NoPos (NestedModule name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: NestedModule name -> NestedModule name Source #
NoPos (Newtype name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Newtype name -> Newtype name Source #
NoPos (ParamDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ParamDecl name -> ParamDecl name Source #
NoPos (ParameterFun x) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ParameterFun x -> ParameterFun x Source #
NoPos (ParameterType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ParameterType name -> ParameterType name Source #
NoPos (Pattern name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Pattern name -> Pattern name Source #
NoPos (PrimType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: PrimType name -> PrimType name Source #
NoPos (Program name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Program name -> Program name Source #
NoPos (Prop name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Prop name -> Prop name Source #
NoPos (PropSyn name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: PropSyn name -> PropSyn name Source #
NoPos (Schema name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Schema name -> Schema name Source #
NoPos (SigDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: SigDecl name -> SigDecl name Source #
NoPos (Signature name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Signature name -> Signature name Source #
NoPos (TParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TParam name -> TParam name Source #
NoPos (TopDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TopDecl name -> TopDecl name Source #
NoPos a => NoPos (TopLevel a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TopLevel a -> TopLevel a Source #
NoPos (TySyn name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TySyn name -> TySyn name Source #
NoPos (Type name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Type name -> Type name Source #
NoPos (TypeInst name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TypeInst name -> TypeInst name Source #
NoPos (UpdField name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: UpdField name -> UpdField name Source #
NoPos (Located t) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Located t -> Located t Source #
NoPos t => NoPos (Maybe t) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Maybe t -> Maybe t Source #
NoPos t => NoPos [t] Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: [t] -> [t] Source #
NoPos (ModuleG mname name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ModuleG mname name -> ModuleG mname name Source #
(NoPos a, NoPos b) => NoPos (a, b) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: (a, b) -> (a, b) Source #

# Pretty-printing

cppKind :: Kind -> Doc Source #

Conversational printing of kinds (e.g., to use in error messages)

ppSelector :: Selector -> Doc Source #

Display the thing selected by the selector, nicely.