Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell2010 |
Cryptol.Parser.AST
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
- getModName :: PName -> Maybe ModName
- getIdent :: PName -> Ident
- mkUnqual :: Ident -> PName
- mkQual :: ModName -> Ident -> PName
- data Named a = Named {}
- data Pass
- = NoPat
- | MonoValues
- data Assoc
- data Schema n = Forall [TParam n] [Prop n] (Type n) (Maybe Range)
- data TParam n = TParam {}
- data Kind
- data 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
- data Module name = Module {}
- newtype Program name = Program [TopDecl name]
- data TopDecl name
- = Decl (TopLevel (Decl name))
- | DPrimType (TopLevel (PrimType name))
- | TDNewtype (TopLevel (Newtype name))
- | Include (Located FilePath)
- | DParameterType (ParameterType name)
- | DParameterConstraint [Located (Prop name)]
- | DParameterFun (ParameterFun name)
- data Decl name
- data Fixity = Fixity {}
- defaultFixity :: Fixity
- data FixityCmp
- 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 {}
- data BindDef name
- type LBindDef = Located (BindDef PName)
- data Pragma
- data ExportType
- data TopLevel a = TopLevel {}
- data Import = Import {}
- data ImportSpec
- data Newtype name = Newtype {}
- data PrimType name = PrimType {}
- data ParameterType name = ParameterType {}
- data ParameterFun name = ParameterFun {}
- data ReplInput name
- data Expr n
- = EVar n
- | ELit Literal
- | ENeg (Expr n)
- | EComplement (Expr n)
- | EGenerate (Expr n)
- | ETuple [Expr n]
- | ERecord [Named (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))
- | 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 [Pattern n] (Expr n)
- | ELocated (Expr n) Range
- | ESplit (Expr n)
- | EParens (Expr n)
- | EInfix (Expr n) (Located n) Fixity (Expr n)
- data Literal
- data NumInfo
- data Match name
- data Pattern n
- data Selector
- data TypeInst name
- data UpdField n = UpdField UpdHow [Located Selector] (Expr n)
- data UpdHow
- data Located a = Located {}
- 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
Identifiers, along with a flag that indicates whether or not they're infix operators. The boolean is present just as cached information from the lexer, and never used during comparisons.
Instances
Eq Ident Source # | |
Ord Ident Source # | |
Show Ident Source # | |
IsString Ident Source # | |
Defined in Cryptol.Utils.Ident Methods fromString :: String -> Ident | |
Generic Ident Source # | |
NFData Ident Source # | |
Defined in Cryptol.Utils.Ident | |
PP Ident Source # | |
ShowParseable Ident Source # | |
Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Ident -> Doc Source # | |
type Rep Ident Source # | |
Defined in Cryptol.Utils.Ident type Rep Ident = D1 ('MetaData "Ident" "Cryptol.Utils.Ident" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "Ident" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text))) |
isInfixIdent :: Ident -> Bool Source #
Module names are just text.
Instances
Eq ModName Source # | |
Ord ModName Source # | |
Show ModName Source # | |
Generic ModName Source # | |
NFData ModName Source # | |
Defined in Cryptol.Utils.Ident | |
PP ModName Source # | |
type Rep ModName Source # | |
Defined in Cryptol.Utils.Ident type Rep ModName = D1 ('MetaData "ModName" "Cryptol.Utils.Ident" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "ModName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text))) |
Names that originate in the parser.
Constructors
UnQual !Ident | Unqualified names like |
Qual !ModName !Ident | Qualified names like |
NewName !Pass !Int | Fresh names generated by a pass. |
Instances
Eq PName Source # | |
Ord PName Source # | |
Show PName Source # | |
Generic PName Source # | |
NFData PName Source # | |
Defined in Cryptol.Parser.Name | |
PPName PName Source # | |
Defined in Cryptol.Parser.Name Methods ppNameFixity :: PName -> Maybe (Assoc, Int) Source # ppPrefixName :: PName -> Doc Source # ppInfixName :: PName -> Doc Source # | |
PP PName Source # | |
RemovePatterns [Decl PName] Source # | |
Defined in Cryptol.Parser.NoPat | |
RemovePatterns (Expr PName) Source # | |
Defined in Cryptol.Parser.NoPat | |
RemovePatterns (Module PName) Source # | |
Defined in Cryptol.Parser.NoPat | |
RemovePatterns (Program PName) Source # | |
Defined in Cryptol.Parser.NoPat | |
BindsNames (TParam PName) Source # | Generate the naming environment for a type parameter. |
Defined in Cryptol.ModuleSystem.NamingEnv | |
BindsNames (Schema PName) Source # | Generate a type renaming environment from the parameters that are bound by this schema. |
Defined in Cryptol.ModuleSystem.NamingEnv | |
BindsNames (Module PName) Source # | The naming environment for a single module. This is the mapping from unqualified names to fully qualified names with uniques. |
Defined in Cryptol.ModuleSystem.NamingEnv | |
BindsNames (InModule (PrimType PName)) Source # | |
Defined in Cryptol.ModuleSystem.NamingEnv | |
BindsNames (InModule (Newtype PName)) Source # | |
Defined in Cryptol.ModuleSystem.NamingEnv | |
BindsNames (InModule (Bind PName)) Source # | Introduce the name |
Defined in Cryptol.ModuleSystem.NamingEnv | |
BindsNames (InModule (ParameterFun PName)) Source # | |
Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (ParameterFun PName) -> BuildNamingEnv Source # | |
BindsNames (InModule (ParameterType PName)) Source # | |
Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (ParameterType PName) -> BuildNamingEnv Source # | |
BindsNames (InModule (Decl PName)) Source # | The naming environment for a single declaration. |
Defined in Cryptol.ModuleSystem.NamingEnv | |
BindsNames (InModule (TopDecl PName)) Source # | |
Defined in Cryptol.ModuleSystem.NamingEnv | |
type Rep PName Source # | |
Defined in Cryptol.Parser.Name type Rep PName = D1 ('MetaData "PName" "Cryptol.Parser.Name" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 #
Instances
Functor Named Source # | |
Foldable Named Source # | |
Defined in Cryptol.Parser.AST Methods fold :: Monoid m => Named m -> m foldMap :: Monoid m => (a -> m) -> Named a -> m foldMap' :: Monoid m => (a -> m) -> Named a -> m foldr :: (a -> b -> b) -> b -> Named a -> b foldr' :: (a -> b -> b) -> b -> Named a -> b foldl :: (b -> a -> b) -> b -> Named a -> b foldl' :: (b -> a -> b) -> b -> Named a -> b foldr1 :: (a -> a -> a) -> Named a -> a foldl1 :: (a -> a -> a) -> Named a -> a elem :: Eq a => a -> Named a -> Bool maximum :: Ord a => Named a -> a | |
Traversable Named Source # | |
Eq a => Eq (Named a) Source # | |
Show a => Show (Named a) Source # | |
Generic (Named a) Source # | |
NFData a => NFData (Named a) Source # | |
Defined in Cryptol.Parser.AST | |
HasLoc a => HasLoc (Named a) Source # | |
NoPos t => NoPos (Named t) Source # | |
type Rep (Named a) Source # | |
Defined in Cryptol.Parser.AST type Rep (Named a) = D1 ('MetaData "Named" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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))) |
Passes that can generate fresh names.
Constructors
NoPat | |
MonoValues |
Instances
Eq Pass Source # | |
Ord Pass Source # | |
Show Pass Source # | |
Generic Pass Source # | |
NFData Pass Source # | |
Defined in Cryptol.Parser.Name | |
type Rep Pass Source # | |
Defined in Cryptol.Parser.Name type Rep Pass = D1 ('MetaData "Pass" "Cryptol.Parser.Name" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "NoPat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MonoValues" 'PrefixI 'False) (U1 :: Type -> Type)) |
Information about associativity.
Constructors
LeftAssoc | |
RightAssoc | |
NonAssoc |
Instances
Eq Assoc Source # | |
Show Assoc Source # | |
Generic Assoc Source # | |
NFData Assoc Source # | |
Defined in Cryptol.Utils.PP | |
PP Assoc Source # | |
type Rep Assoc Source # | |
Defined in Cryptol.Utils.PP type Rep Assoc = D1 ('MetaData "Assoc" "Cryptol.Utils.PP" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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
Instances
Functor Schema Source # | |
Rename Schema Source # | Rename a schema, assuming that none of its type variables are already in scope. |
Eq n => Eq (Schema n) Source # | |
Show n => Show (Schema n) Source # | |
Generic (Schema n) Source # | |
NFData n => NFData (Schema n) Source # | |
Defined in Cryptol.Parser.AST | |
PPName name => PP (Schema name) Source # | |
AddLoc (Schema name) Source # | |
HasLoc (Schema name) Source # | |
NoPos (Schema name) Source # | |
BindsNames (Schema PName) Source # | Generate a type renaming environment from the parameters that are bound by this schema. |
Defined in Cryptol.ModuleSystem.NamingEnv | |
type Rep (Schema n) Source # | |
Defined in Cryptol.Parser.AST type Rep (Schema n) = D1 ('MetaData "Schema" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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))))) |
Instances
Functor TParam Source # | |
Rename TParam Source # | |
Eq n => Eq (TParam n) Source # | |
Show n => Show (TParam n) Source # | |
Generic (TParam n) Source # | |
NFData n => NFData (TParam n) Source # | |
Defined in Cryptol.Parser.AST | |
PPName name => PP (TParam name) Source # | |
AddLoc (TParam name) Source # | |
HasLoc (TParam name) Source # | |
NoPos (TParam name) Source # | |
BindsNames (TParam PName) Source # | Generate the naming environment for a type parameter. |
Defined in Cryptol.ModuleSystem.NamingEnv | |
type Rep (TParam n) Source # | |
Defined in Cryptol.Parser.AST type Rep (TParam n) = D1 ('MetaData "TParam" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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))))) |
Instances
Eq Kind Source # | |
Show Kind Source # | |
Generic Kind Source # | |
NFData Kind Source # | |
Defined in Cryptol.Parser.AST | |
PP Kind Source # | |
type Rep Kind Source # | |
Defined in Cryptol.Parser.AST type Rep Kind = D1 ('MetaData "Kind" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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)))) |
Constructors
TFun (Type n) (Type n) | [8] -> [8] |
TSeq (Type n) (Type n) | [8] a |
TBit | Bit |
TNum Integer | 10 |
TChar Char |
|
TUser n [Type n] | A type variable or synonym |
TRecord [Named (Type n)] | { x : [8], y : [32] } |
TTuple [Type n] | ([8], [32]) |
TWild |
|
TLocated (Type n) Range | Location information |
TParens (Type n) | (ty) |
TInfix (Type n) (Located n) Fixity (Type n) | ty + ty |
Instances
Functor Type Source # | |
Rename Type Source # | Resolve fixity, then rename the resulting type. |
Eq n => Eq (Type n) Source # | |
Show n => Show (Type n) Source # | |
Generic (Type n) Source # | |
NFData n => NFData (Type n) Source # | |
Defined in Cryptol.Parser.AST | |
PPName name => PP (Type name) Source # | |
AddLoc (Type name) Source # | |
HasLoc (Type name) Source # | |
NoPos (Type name) Source # | |
type Rep (Type n) Source # | |
Defined in Cryptol.Parser.AST type Rep (Type n) = D1 ('MetaData "Type" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (((C1 ('MetaCons "TFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n))) :+: (C1 ('MetaCons "TSeq" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n))) :+: C1 ('MetaCons "TBit" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "TNum" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)) :+: (C1 ('MetaCons "TChar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Char)) :+: C1 ('MetaCons "TUser" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 n) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type n]))))) :+: ((C1 ('MetaCons "TRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Named (Type n)])) :+: (C1 ('MetaCons "TTuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type n])) :+: C1 ('MetaCons "TWild" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "TLocated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "TParens" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n))) :+: C1 ('MetaCons "TInfix" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located n))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n)))))))) |
Instances
Functor Prop Source # | |
Rename Prop Source # | |
Eq n => Eq (Prop n) Source # | |
Show n => Show (Prop n) Source # | |
Generic (Prop n) Source # | |
NFData n => NFData (Prop n) Source # | |
Defined in Cryptol.Parser.AST | |
PPName name => PP (Prop name) Source # | |
NoPos (Prop name) Source # | |
type Rep (Prop n) Source # | |
Defined in Cryptol.Parser.AST |
Declarations
A parsed module.
Constructors
Module | |
Instances
Show name => Show (Module name) Source # | |
Generic (Module name) Source # | |
NFData name => NFData (Module name) Source # | |
Defined in Cryptol.Parser.AST | |
(Show name, PPName name) => PP (Module name) Source # | |
HasLoc (Module name) Source # | |
NoPos (Module name) Source # | |
RemovePatterns (Module PName) Source # | |
Defined in Cryptol.Parser.NoPat | |
BindsNames (Module PName) Source # | The naming environment for a single module. This is the mapping from unqualified names to fully qualified names with uniques. |
Defined in Cryptol.ModuleSystem.NamingEnv | |
type Rep (Module name) Source # | |
Defined in Cryptol.Parser.AST type Rep (Module name) = D1 ('MetaData "Module" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "Module" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located ModName)) :*: S1 ('MetaSel ('Just "mInstance") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe (Located ModName)))) :*: (S1 ('MetaSel ('Just "mImports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located Import]) :*: S1 ('MetaSel ('Just "mDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TopDecl name])))) |
Constructors
Decl (TopLevel (Decl name)) | |
DPrimType (TopLevel (PrimType name)) | |
TDNewtype (TopLevel (Newtype name)) | @newtype T as = t |
Include (Located FilePath) | include File |
DParameterType (ParameterType name) | parameter type T : # |
DParameterConstraint [Located (Prop name)] | parameter type constraint (fin T) |
DParameterFun (ParameterFun name) | parameter someVal : [256] |
Instances
Rename TopDecl Source # | |
Show name => Show (TopDecl name) Source # | |
Generic (TopDecl name) Source # | |
NFData name => NFData (TopDecl name) Source # | |
Defined in Cryptol.Parser.AST | |
(Show name, PPName name) => PP (TopDecl name) Source # | |
HasLoc (TopDecl name) Source # | |
NoPos (TopDecl name) Source # | |
BindsNames (InModule (TopDecl PName)) Source # | |
Defined in Cryptol.ModuleSystem.NamingEnv | |
FromDecl (TopDecl Name) Source # | |
Defined in Cryptol.TypeCheck.Depends | |
type Rep (TopDecl name) Source # | |
Defined in Cryptol.Parser.AST type Rep (TopDecl name) = D1 ('MetaData "TopDecl" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 "DParameterType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ParameterType name)))) :+: (C1 ('MetaCons "DParameterConstraint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located (Prop name)])) :+: C1 ('MetaCons "DParameterFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ParameterFun name)))))) |
Constructors
DSignature [Located name] (Schema name) | |
DFixity !Fixity [Located name] | |
DPragma [Located name] Pragma | |
DBind (Bind name) | |
DPatBind (Pattern name) (Expr name) | |
DType (TySyn name) | |
DProp (PropSyn name) | |
DLocated (Decl name) Range |
Instances
Functor Decl Source # | |
Rename Decl Source # | |
Eq name => Eq (Decl name) Source # | |
Show name => Show (Decl name) Source # | |
Generic (Decl name) Source # | |
NFData name => NFData (Decl name) Source # | |
Defined in Cryptol.Parser.AST | |
(Show name, PPName name) => PP (Decl name) Source # | |
AddLoc (Decl name) Source # | |
HasLoc (Decl name) Source # | |
NoPos (Decl name) Source # | |
RemovePatterns [Decl PName] Source # | |
Defined in Cryptol.Parser.NoPat | |
BindsNames (InModule (Decl PName)) Source # | The naming environment for a single declaration. |
Defined in Cryptol.ModuleSystem.NamingEnv | |
FromDecl (Decl Name) Source # | |
Defined in Cryptol.TypeCheck.Depends | |
type Rep (Decl name) Source # | |
Defined in Cryptol.Parser.AST type Rep (Decl name) = D1 ('MetaData "Decl" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 "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))))) |
Instances
Eq Fixity Source # | |
Show Fixity Source # | |
Generic Fixity Source # | |
NFData Fixity Source # | |
Defined in Cryptol.Parser.Fixity | |
PP Fixity Source # | |
type Rep Fixity Source # | |
Defined in Cryptol.Parser.Fixity type Rep Fixity = D1 ('MetaData "Fixity" "Cryptol.Parser.Fixity" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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.
Instances
Functor TySyn Source # | |
Rename TySyn Source # | |
Eq n => Eq (TySyn n) Source # | |
Show n => Show (TySyn n) Source # | |
Generic (TySyn n) Source # | |
NFData n => NFData (TySyn n) Source # | |
Defined in Cryptol.Parser.AST | |
PPName name => PP (TySyn name) Source # | |
NoPos (TySyn name) Source # | |
type Rep (TySyn n) Source # | |
Defined in Cryptol.Parser.AST type Rep (TySyn n) = D1 ('MetaData "TySyn" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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))))) |
Instances
Functor PropSyn Source # | |
Rename PropSyn Source # | |
Eq n => Eq (PropSyn n) Source # | |
Show n => Show (PropSyn n) Source # | |
Generic (PropSyn n) Source # | |
NFData n => NFData (PropSyn n) Source # | |
Defined in Cryptol.Parser.AST | |
PPName name => PP (PropSyn name) Source # | |
NoPos (PropSyn name) Source # | |
type Rep (PropSyn n) Source # | |
Defined in Cryptol.Parser.AST type Rep (PropSyn n) = D1 ('MetaData "PropSyn" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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])))) |
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
|
Instances
Functor Bind Source # | |
Rename Bind Source # | Rename a binding. |
Eq name => Eq (Bind name) Source # | |
Show name => Show (Bind name) Source # | |
Generic (Bind name) Source # | |
NFData name => NFData (Bind name) Source # | |
Defined in Cryptol.Parser.AST | |
(Show name, PPName name) => PP (Bind name) Source # | |
HasLoc (Bind name) Source # | |
NoPos (Bind name) Source # | |
BindsNames (InModule (Bind PName)) Source # | Introduce the name |
Defined in Cryptol.ModuleSystem.NamingEnv | |
type Rep (Bind name) Source # | |
Defined in Cryptol.Parser.AST type Rep (Bind name) = D1 ('MetaData "Bind" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 String))))))) |
Instances
Functor BindDef Source # | |
Rename BindDef Source # | |
Eq name => Eq (BindDef name) Source # | |
Show name => Show (BindDef name) Source # | |
Generic (BindDef name) Source # | |
NFData name => NFData (BindDef name) Source # | |
Defined in Cryptol.Parser.AST | |
(Show name, PPName name) => PP (BindDef name) Source # | |
type Rep (BindDef name) Source # | |
Defined in Cryptol.Parser.AST type Rep (BindDef name) = D1 ('MetaData "BindDef" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "DPrim" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr name)))) |
Constructors
PragmaNote String | |
PragmaProperty |
Instances
Eq Pragma Source # | |
Show Pragma Source # | |
Generic Pragma Source # | |
NFData Pragma Source # | |
Defined in Cryptol.Parser.AST | |
PP Pragma Source # | |
NoPos Pragma Source # | |
type Rep Pragma Source # | |
Defined in Cryptol.Parser.AST type Rep Pragma = D1 ('MetaData "Pragma" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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.
Instances
Eq ExportType Source # | |
Defined in Cryptol.Parser.AST | |
Ord ExportType Source # | |
Defined in Cryptol.Parser.AST Methods compare :: ExportType -> ExportType -> Ordering (<) :: ExportType -> ExportType -> Bool (<=) :: ExportType -> ExportType -> Bool (>) :: ExportType -> ExportType -> Bool (>=) :: ExportType -> ExportType -> Bool max :: ExportType -> ExportType -> ExportType min :: ExportType -> ExportType -> ExportType | |
Show ExportType Source # | |
Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ExportType -> ShowS show :: ExportType -> String showList :: [ExportType] -> ShowS | |
Generic ExportType Source # | |
Defined in Cryptol.Parser.AST Associated Types type Rep ExportType :: Type -> Type | |
NFData ExportType Source # | |
Defined in Cryptol.Parser.AST Methods rnf :: ExportType -> () | |
type Rep ExportType Source # | |
Defined in Cryptol.Parser.AST type Rep ExportType = D1 ('MetaData "ExportType" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "Public" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Private" 'PrefixI 'False) (U1 :: Type -> Type)) |
A top-level module declaration.
Instances
Functor TopLevel Source # | |
Foldable TopLevel Source # | |
Defined in Cryptol.Parser.AST Methods fold :: Monoid m => TopLevel m -> m foldMap :: Monoid m => (a -> m) -> TopLevel a -> m foldMap' :: Monoid m => (a -> m) -> TopLevel a -> m foldr :: (a -> b -> b) -> b -> TopLevel a -> b foldr' :: (a -> b -> b) -> b -> TopLevel a -> b foldl :: (b -> a -> b) -> b -> TopLevel a -> b foldl' :: (b -> a -> b) -> b -> TopLevel a -> b foldr1 :: (a -> a -> a) -> TopLevel a -> a foldl1 :: (a -> a -> a) -> TopLevel a -> a elem :: Eq a => a -> TopLevel a -> Bool maximum :: Ord a => TopLevel a -> a minimum :: Ord a => TopLevel a -> a | |
Traversable TopLevel Source # | |
Show a => Show (TopLevel a) Source # | |
Generic (TopLevel a) Source # | |
NFData a => NFData (TopLevel a) Source # | |
Defined in Cryptol.Parser.AST | |
PP a => PP (TopLevel a) Source # | |
HasLoc a => HasLoc (TopLevel a) Source # | |
NoPos a => NoPos (TopLevel a) Source # | |
type Rep (TopLevel a) Source # | |
Defined in Cryptol.Parser.AST type Rep (TopLevel a) = D1 ('MetaData "TopLevel" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 String))) :*: S1 ('MetaSel ('Just "tlValue") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))) |
An import declaration.
Instances
Eq Import Source # | |
Show Import Source # | |
Generic Import Source # | |
NFData Import Source # | |
Defined in Cryptol.Parser.AST | |
PP Import Source # | |
type Rep Import Source # | |
Defined in Cryptol.Parser.AST type Rep Import = D1 ('MetaData "Import" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "Import" 'PrefixI 'True) (S1 ('MetaSel ('Just "iModule") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModName) :*: (S1 ('MetaSel ('Just "iAs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModName)) :*: S1 ('MetaSel ('Just "iSpec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ImportSpec))))) |
data ImportSpec Source #
The list of names following an import.
INVARIANT: All of the Name
entries in the list are expected to be
unqualified names; the QName
or NewName
constructors should not be
present.
Instances
Eq ImportSpec Source # | |
Defined in Cryptol.Parser.AST | |
Show ImportSpec Source # | |
Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ImportSpec -> ShowS show :: ImportSpec -> String showList :: [ImportSpec] -> ShowS | |
Generic ImportSpec Source # | |
Defined in Cryptol.Parser.AST Associated Types type Rep ImportSpec :: Type -> Type | |
NFData ImportSpec Source # | |
Defined in Cryptol.Parser.AST Methods rnf :: ImportSpec -> () | |
PP ImportSpec Source # | |
Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ImportSpec -> Doc Source # | |
type Rep ImportSpec Source # | |
Defined in Cryptol.Parser.AST type Rep ImportSpec = D1 ('MetaData "ImportSpec" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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]))) |
Constructors
Newtype | |
Instances
Rename Newtype Source # | |
Eq name => Eq (Newtype name) Source # | |
Show name => Show (Newtype name) Source # | |
Generic (Newtype name) Source # | |
NFData name => NFData (Newtype name) Source # | |
Defined in Cryptol.Parser.AST | |
PPName name => PP (Newtype name) Source # | |
HasLoc (Newtype name) Source # | |
NoPos (Newtype name) Source # | |
BindsNames (InModule (Newtype PName)) Source # | |
Defined in Cryptol.ModuleSystem.NamingEnv | |
type Rep (Newtype name) Source # | |
Defined in Cryptol.Parser.AST type Rep (Newtype name) = D1 ('MetaData "Newtype" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "Newtype" 'PrefixI 'True) (S1 ('MetaSel ('Just "nName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located name)) :*: (S1 ('MetaSel ('Just "nParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam name]) :*: S1 ('MetaSel ('Just "nBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Named (Type name)])))) |
A declaration for a type with no implementation.
Constructors
PrimType | |
Instances
Rename PrimType Source # | |
Show name => Show (PrimType name) Source # | |
Generic (PrimType name) Source # | |
NFData name => NFData (PrimType name) Source # | |
Defined in Cryptol.Parser.AST | |
(Show name, PPName name) => PP (PrimType name) Source # | |
HasLoc (PrimType name) Source # | |
NoPos (PrimType name) Source # | |
BindsNames (InModule (PrimType PName)) Source # | |
Defined in Cryptol.ModuleSystem.NamingEnv | |
type Rep (PrimType name) Source # | |
Defined in Cryptol.Parser.AST type Rep (PrimType name) = D1 ('MetaData "PrimType" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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
Constructors
ParameterType | |
Instances
Rename ParameterType Source # | |
Defined in Cryptol.ModuleSystem.Renamer Methods rename :: ParameterType PName -> RenameM (ParameterType Name) Source # | |
Eq name => Eq (ParameterType name) Source # | |
Defined in Cryptol.Parser.AST Methods (==) :: ParameterType name -> ParameterType name -> Bool (/=) :: ParameterType name -> ParameterType name -> Bool | |
Show name => Show (ParameterType name) Source # | |
Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ParameterType name -> ShowS show :: ParameterType name -> String showList :: [ParameterType name] -> ShowS | |
Generic (ParameterType name) Source # | |
Defined in Cryptol.Parser.AST Associated Types type Rep (ParameterType name) :: Type -> Type Methods from :: ParameterType name -> Rep (ParameterType name) x to :: Rep (ParameterType name) x -> ParameterType name | |
NFData name => NFData (ParameterType name) Source # | |
Defined in Cryptol.Parser.AST Methods rnf :: ParameterType name -> () | |
(Show name, PPName name) => PP (ParameterType name) Source # | |
Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ParameterType name -> Doc Source # | |
HasLoc (ParameterType name) Source # | |
Defined in Cryptol.Parser.AST Methods getLoc :: ParameterType name -> Maybe Range Source # | |
NoPos (ParameterType name) Source # | |
Defined in Cryptol.Parser.AST Methods noPos :: ParameterType name -> ParameterType name Source # | |
BindsNames (InModule (ParameterType PName)) Source # | |
Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (ParameterType PName) -> BuildNamingEnv Source # | |
type Rep (ParameterType name) Source # | |
Defined in Cryptol.Parser.AST type Rep (ParameterType name) = D1 ('MetaData "ParameterType" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 String)) :*: (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
Constructors
ParameterFun | |
Instances
Rename ParameterFun Source # | |
Defined in Cryptol.ModuleSystem.Renamer Methods rename :: ParameterFun PName -> RenameM (ParameterFun Name) Source # | |
Eq name => Eq (ParameterFun name) Source # | |
Defined in Cryptol.Parser.AST Methods (==) :: ParameterFun name -> ParameterFun name -> Bool (/=) :: ParameterFun name -> ParameterFun name -> Bool | |
Show name => Show (ParameterFun name) Source # | |
Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ParameterFun name -> ShowS show :: ParameterFun name -> String showList :: [ParameterFun name] -> ShowS | |
Generic (ParameterFun name) Source # | |
Defined in Cryptol.Parser.AST Associated Types type Rep (ParameterFun name) :: Type -> Type Methods from :: ParameterFun name -> Rep (ParameterFun name) x to :: Rep (ParameterFun name) x -> ParameterFun name | |
NFData name => NFData (ParameterFun name) Source # | |
Defined in Cryptol.Parser.AST Methods rnf :: ParameterFun name -> () | |
(Show name, PPName name) => PP (ParameterFun name) Source # | |
Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ParameterFun name -> Doc Source # | |
HasLoc (ParameterFun name) Source # | |
Defined in Cryptol.Parser.AST Methods getLoc :: ParameterFun name -> Maybe Range Source # | |
NoPos (ParameterFun x) Source # | |
Defined in Cryptol.Parser.AST Methods noPos :: ParameterFun x -> ParameterFun x Source # | |
BindsNames (InModule (ParameterFun PName)) Source # | |
Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (ParameterFun PName) -> BuildNamingEnv Source # | |
type Rep (ParameterFun name) Source # | |
Defined in Cryptol.Parser.AST type Rep (ParameterFun name) = D1 ('MetaData "ParameterFun" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 String)) :*: S1 ('MetaSel ('Just "pfFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity))))) |
Interactive
Input at the REPL, which can either be an expression or a let
statement.
Expressions
Constructors
EVar n | x |
ELit Literal | 0x10 |
ENeg (Expr n) | -1 |
EComplement (Expr n) | ~1 |
EGenerate (Expr n) | generate f |
ETuple [Expr n] | (1,2,3) |
ERecord [Named (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] |
EInfFrom (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) |
|
EFun [Pattern n] (Expr n) | \x y -> x |
ELocated (Expr n) Range | position annotation |
ESplit (Expr n) |
|
EParens (Expr n) |
|
EInfix (Expr n) (Located n) Fixity (Expr n) |
|
Instances
Functor Expr Source # | |
Rename Expr Source # | |
Eq n => Eq (Expr n) Source # | |
Show n => Show (Expr n) Source # | |
Generic (Expr n) Source # | |
NFData n => NFData (Expr n) Source # | |
Defined in Cryptol.Parser.AST | |
(Show name, PPName name) => PP (Expr name) Source # | |
AddLoc (Expr n) Source # | |
HasLoc (Expr name) Source # | |
NoPos (Expr name) Source # | |
RemovePatterns (Expr PName) Source # | |
Defined in Cryptol.Parser.NoPat | |
type Rep (Expr n) Source # | |
Defined in Cryptol.Parser.AST type Rep (Expr n) = D1 ('MetaData "Expr" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) ((((C1 ('MetaCons "EVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 n)) :+: (C1 ('MetaCons "ELit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "ENeg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n))))) :+: (C1 ('MetaCons "EComplement" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n))) :+: (C1 ('MetaCons "EGenerate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n))) :+: C1 ('MetaCons "ETuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr n]))))) :+: ((C1 ('MetaCons "ERecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Named (Expr n)])) :+: (C1 ('MetaCons "ESel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Selector)) :+: C1 ('MetaCons "EUpd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Expr n))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [UpdField n])))) :+: (C1 ('MetaCons "EList" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr n])) :+: (C1 ('MetaCons "EFromTo" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Type n)))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Type n))))) :+: C1 ('MetaCons "EInfFrom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Expr n)))))))) :+: (((C1 ('MetaCons "EComp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [[Match n]])) :+: (C1 ('MetaCons "EApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n))) :+: C1 ('MetaCons "EAppT" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TypeInst n])))) :+: (C1 ('MetaCons "EIf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n)))) :+: (C1 ('MetaCons "EWhere" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Decl n])) :+: C1 ('MetaCons "ETyped" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n)))))) :+: ((C1 ('MetaCons "ETypeVal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n))) :+: (C1 ('MetaCons "EFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Pattern n]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n))) :+: C1 ('MetaCons "ELocated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "ESplit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n))) :+: (C1 ('MetaCons "EParens" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n))) :+: C1 ('MetaCons "EInfix" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located n))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n))))))))) |
Literals.
Instances
Eq Literal Source # | |
Show Literal Source # | |
Generic Literal Source # | |
NFData Literal Source # | |
Defined in Cryptol.Parser.AST | |
PP Literal Source # | |
type Rep Literal Source # | |
Defined in Cryptol.Parser.AST type Rep Literal = D1 ('MetaData "Literal" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 "ECString" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) |
Infromation about the representation of a numeric constant.
Constructors
BinLit Int | n-digit binary literal |
OctLit Int | n-digit octal literal |
DecLit | overloaded decimal literal |
HexLit Int | n-digit hex literal |
CharLit | character literal |
PolyLit Int | polynomial literal |
Instances
Eq NumInfo Source # | |
Show NumInfo Source # | |
Generic NumInfo Source # | |
NFData NumInfo Source # | |
Defined in Cryptol.Parser.AST | |
type Rep NumInfo Source # | |
Defined in Cryptol.Parser.AST type Rep NumInfo = D1 ('MetaData "NumInfo" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) ((C1 ('MetaCons "BinLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: (C1 ('MetaCons "OctLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "DecLit" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "HexLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: (C1 ('MetaCons "CharLit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PolyLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))) |
Instances
Functor Match Source # | |
Rename Match Source # | |
Eq name => Eq (Match name) Source # | |
Show name => Show (Match name) Source # | |
Generic (Match name) Source # | |
NFData name => NFData (Match name) Source # | |
Defined in Cryptol.Parser.AST | |
(Show name, PPName name) => PP (Match name) Source # | |
HasLoc (Match name) Source # | |
NoPos (Match name) Source # | |
type Rep (Match name) Source # | |
Defined in Cryptol.Parser.AST type Rep (Match name) = D1 ('MetaData "Match" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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)))) |
Constructors
PVar (Located n) | x |
PWild | _ |
PTuple [Pattern n] | (x,y,z) |
PRecord [Named (Pattern n)] | { x = (a,b,c), y = z } |
PList [Pattern n] | [ x, y, z ] |
PTyped (Pattern n) (Type n) | x : [8] |
PSplit (Pattern n) (Pattern n) | (x # y) |
PLocated (Pattern n) Range | Location information |
Instances
Functor Pattern Source # | |
Rename Pattern Source # | |
Eq n => Eq (Pattern n) Source # | |
Show n => Show (Pattern n) Source # | |
Generic (Pattern n) Source # | |
NFData n => NFData (Pattern n) Source # | |
Defined in Cryptol.Parser.AST | |
PPName name => PP (Pattern name) Source # | |
AddLoc (Pattern name) Source # | |
HasLoc (Pattern name) Source # | |
NoPos (Pattern name) Source # | |
type Rep (Pattern n) Source # | |
Defined in Cryptol.Parser.AST type Rep (Pattern n) = D1 ('MetaData "Pattern" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (((C1 ('MetaCons "PVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located n))) :+: C1 ('MetaCons "PWild" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PTuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Pattern n])) :+: C1 ('MetaCons "PRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Named (Pattern n)])))) :+: ((C1 ('MetaCons "PList" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Pattern n])) :+: C1 ('MetaCons "PTyped" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type n)))) :+: (C1 ('MetaCons "PSplit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern n))) :+: C1 ('MetaCons "PLocated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) |
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
Eq Selector Source # | |
Ord Selector Source # | |
Defined in Cryptol.Parser.Selector | |
Show Selector Source # | |
Generic Selector Source # | |
NFData Selector Source # | |
Defined in Cryptol.Parser.Selector | |
PP Selector Source # | |
ShowParseable Selector Source # | |
Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Selector -> Doc Source # | |
type Rep Selector Source # | |
Defined in Cryptol.Parser.Selector type Rep Selector = D1 ('MetaData "Selector" "Cryptol.Parser.Selector" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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))))) |
Instances
Functor TypeInst Source # | |
Rename TypeInst Source # | |
Eq name => Eq (TypeInst name) Source # | |
Show name => Show (TypeInst name) Source # | |
Generic (TypeInst name) Source # | |
NFData name => NFData (TypeInst name) Source # | |
Defined in Cryptol.Parser.AST | |
PPName name => PP (TypeInst name) Source # | |
NoPos (TypeInst name) Source # | |
type Rep (TypeInst name) Source # | |
Defined in Cryptol.Parser.AST type Rep (TypeInst name) = D1 ('MetaData "TypeInst" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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)))) |
Instances
Functor UpdField Source # | |
Rename UpdField Source # | Note that after this point the |
Eq n => Eq (UpdField n) Source # | |
Show n => Show (UpdField n) Source # | |
Generic (UpdField n) Source # | |
NFData n => NFData (UpdField n) Source # | |
Defined in Cryptol.Parser.AST | |
(Show name, PPName name) => PP (UpdField name) Source # | |
NoPos (UpdField name) Source # | |
type Rep (UpdField n) Source # | |
Defined in Cryptol.Parser.AST type Rep (UpdField n) = D1 ('MetaData "UpdField" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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))))) |
Instances
Eq UpdHow Source # | |
Show UpdHow Source # | |
Generic UpdHow Source # | |
NFData UpdHow Source # | |
Defined in Cryptol.Parser.AST | |
PP UpdHow Source # | |
type Rep UpdHow Source # | |
Defined in Cryptol.Parser.AST type Rep UpdHow = D1 ('MetaData "UpdHow" "Cryptol.Parser.AST" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "UpdSet" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UpdFun" 'PrefixI 'False) (U1 :: Type -> Type)) |
Positions
Instances
Functor Located Source # | |
Eq a => Eq (Located a) Source # | |
Show a => Show (Located a) Source # | |
Generic (Located a) Source # | |
NFData a => NFData (Located a) Source # | |
Defined in Cryptol.Parser.Position | |
PPName a => PPName (Located a) Source # | |
Defined in Cryptol.Parser.Position Methods ppNameFixity :: Located a -> Maybe (Assoc, Int) Source # ppPrefixName :: Located a -> Doc Source # ppInfixName :: Located a -> Doc Source # | |
PP a => PP (Located a) Source # | |
AddLoc (Located a) Source # | |
HasLoc (Located a) Source # | |
NoPos (Located t) Source # | |
ShowParseable a => ShowParseable (Located a) Source # | |
Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Located a -> Doc Source # | |
type Rep (Located a) Source # | |
Defined in Cryptol.Parser.Position type Rep (Located a) = D1 ('MetaData "Located" "Cryptol.Parser.Position" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "Located" 'PrefixI 'True) (S1 ('MetaSel ('Just "srcRange") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Range) :*: S1 ('MetaSel ('Just "thing") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a))) |
Instances
Pretty-printing
ppSelector :: Selector -> Doc Source #
Display the thing selected by the selector, nicely.