cryptol-2.8.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
- 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]
  - | TRecord [Named (Type n)]
  - | TTuple [Type n]
  - | TWild
  - | TLocated (Type n) Range
  - | TParens (Type n)
  - | 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
- data Module name = Module {
  - mName :: Located ModName
  - mInstance :: !(Maybe (Located ModName))
  - mImports :: [Located Import]
  - mDecls :: [TopDecl 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)
  - | DParameterType (ParameterType name)
  - | DParameterConstraint [Located (Prop name)]
  - | DParameterFun (ParameterFun name)
- data Decl name
  - = 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
- 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 String
  }
- data BindDef name
  - = DPrim
  - | DExpr (Expr name)
- type LBindDef = Located (BindDef PName)
- data Pragma
  - = PragmaNote String
  - | PragmaProperty
- data ExportType
  - = Public
  - | Private
- data TopLevel a = TopLevel {
  - tlExport :: ExportType
  - tlDoc :: Maybe (Located String)
  - tlValue :: a
  }
- data Import = Import {
  - iModule :: !ModName
  - iAs :: Maybe ModName
  - iSpec :: Maybe ImportSpec
  }
- data ImportSpec
  - = Hiding [Ident]
  - | Only [Ident]
- data Newtype name = Newtype {
  - nName :: Located name
  - nParams :: [TParam name]
  - nBody :: [Named (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 String
  - ptFixity :: Maybe Fixity
  - ptNumber :: !Int
  }
- data ParameterFun name = ParameterFun {
  - pfName :: Located name
  - pfSchema :: Schema name
  - pfDoc :: Maybe String
  - pfFixity :: Maybe Fixity
  }
- data ReplInput name
  - = ExprInput (Expr name)
  - | LetInput (Decl 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
  - = ECNum Integer NumInfo
  - | ECString String
- data NumInfo
  - = BinLit Int
  - | OctLit Int
  - | DecLit
  - | HexLit Int
  - | CharLit
  - | PolyLit Int
- data Match name
  - = Match (Pattern name) (Expr name)
  - | MatchLet (Bind name)
- data Pattern n
  - = PVar (Located n)
  - | PWild
  - | PTuple [Pattern n]
  - | PRecord [Named (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 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 #

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

Instances details

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 #
Show Ident Source # |
Instance details Defined in Cryptol.Utils.Ident Methods showsPrec :: Int -> Ident -> ShowS Source # show :: Ident -> String Source # showList :: [Ident] -> ShowS Source #
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 #
NFData Ident Source # |
Instance details Defined in Cryptol.Utils.Ident Methods rnf :: Ident -> () Source #
PP Ident Source # |
Instance details Defined in Cryptol.Utils.PP Methods ppPrec :: Int -> Ident -> Doc Source #
ShowParseable Ident Source # |
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Ident -> Doc Source #
type Rep Ident Source # |

Instance details

Defined in Cryptol.Utils.Ident

type Rep Ident = D1 ('MetaData "Ident" "Cryptol.Utils.Ident" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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)))

mkIdent :: Text -> Ident Source #

mkInfix :: Text -> Ident Source #

isInfixIdent :: Ident -> Bool Source #

nullIdent :: Ident -> Bool Source #

identText :: Ident -> Text Source #

data ModName Source #

Module names are just text.

#### Instances

Instances details

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 #
Show ModName Source # |
Instance details Defined in Cryptol.Utils.Ident Methods showsPrec :: Int -> ModName -> ShowS Source # show :: ModName -> String Source # showList :: [ModName] -> ShowS Source #
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 #
NFData ModName Source # |
Instance details Defined in Cryptol.Utils.Ident Methods rnf :: ModName -> () Source #
PP ModName Source # |
Instance details Defined in Cryptol.Utils.PP Methods ppPrec :: Int -> ModName -> Doc Source #
type Rep ModName Source # |
Instance details Defined in Cryptol.Utils.Ident type Rep ModName = D1 ('MetaData "ModName" "Cryptol.Utils.Ident" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" 'False) (C1 ('MetaCons "ModName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)))

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

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 #
Show PName Source # |
Instance details Defined in Cryptol.Parser.Name Methods showsPrec :: Int -> PName -> ShowS Source # show :: PName -> String Source # showList :: [PName] -> ShowS Source #
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 #
NFData PName Source # |
Instance details Defined in Cryptol.Parser.Name Methods rnf :: PName -> () Source #
PPName PName Source # |
Instance details Defined in Cryptol.Parser.Name Methods ppNameFixity :: PName -> Maybe (Assoc, Int) Source # ppPrefixName :: PName -> Doc Source # ppInfixName :: PName -> Doc Source #
PP PName Source # |
Instance details Defined in Cryptol.Parser.Name Methods ppPrec :: Int -> PName -> Doc Source #
RemovePatterns [Decl PName] Source # |
Instance details Defined in Cryptol.Parser.NoPat Methods removePatterns :: [Decl PName] -> ([Decl PName], [Error]) Source #
RemovePatterns (Expr PName) Source # |
Instance details Defined in Cryptol.Parser.NoPat Methods removePatterns :: Expr PName -> (Expr PName, [Error]) Source #
RemovePatterns (Module PName) Source # |
Instance details Defined in Cryptol.Parser.NoPat Methods removePatterns :: Module PName -> (Module PName, [Error]) Source #
RemovePatterns (Program PName) Source # |
Instance details Defined in Cryptol.Parser.NoPat Methods removePatterns :: Program PName -> (Program PName, [Error]) Source #
BindsNames (TParam PName) Source # | Generate the naming environment for a type parameter.
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: TParam PName -> BuildNamingEnv 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.NamingEnv Methods namingEnv :: Schema PName -> BuildNamingEnv Source #
BindsNames (Module PName) Source # | The naming environment for a single module. This is the mapping from unqualified names to fully qualified names with uniques.
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: Module PName -> BuildNamingEnv Source #
BindsNames (InModule (PrimType PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (PrimType PName) -> BuildNamingEnv Source #
BindsNames (InModule (Newtype PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (Newtype PName) -> BuildNamingEnv Source #
BindsNames (InModule (Bind PName)) Source # | Introduce the name
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (Bind PName) -> BuildNamingEnv Source #
BindsNames (InModule (ParameterFun PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (ParameterFun PName) -> BuildNamingEnv Source #
BindsNames (InModule (ParameterType PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (ParameterType PName) -> BuildNamingEnv Source #
BindsNames (InModule (Decl PName)) Source # | The naming environment for a single declaration.
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (Decl PName) -> BuildNamingEnv Source #
BindsNames (InModule (TopDecl PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (TopDecl PName) -> BuildNamingEnv Source #
type Rep PName Source # |

Instance details

Defined in Cryptol.Parser.Name

type Rep PName = D1 ('MetaData "PName" "Cryptol.Parser.Name" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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

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 #
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 #
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 #
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 #
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 #
NFData a => NFData (Named a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Named a -> () Source #
HasLoc a => HasLoc (Named a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: Named a -> Maybe Range Source #
NoPos t => NoPos (Named t) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Named t -> Named t Source #
type Rep (Named a) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (Named a) = D1 ('MetaData "Named" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 |

#### Instances

Instances details

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 #
Show Pass Source # |
Instance details Defined in Cryptol.Parser.Name Methods showsPrec :: Int -> Pass -> ShowS Source # show :: Pass -> String Source # showList :: [Pass] -> ShowS Source #
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 #
NFData Pass Source # |
Instance details Defined in Cryptol.Parser.Name Methods rnf :: Pass -> () Source #
type Rep Pass Source # |
Instance details Defined in Cryptol.Parser.Name type Rep Pass = D1 ('MetaData "Pass" "Cryptol.Parser.Name" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" 'False) (C1 ('MetaCons "NoPat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MonoValues" 'PrefixI 'False) (U1 :: Type -> Type))

data Assoc Source #

Information about associativity.

Constructors

LeftAssoc |
RightAssoc |
NonAssoc |

#### Instances

Instances details

Eq Assoc Source # |
Instance details Defined in Cryptol.Utils.PP Methods (==) :: Assoc -> Assoc -> Bool Source # (/=) :: Assoc -> Assoc -> Bool Source #
Show Assoc Source # |
Instance details Defined in Cryptol.Utils.PP Methods showsPrec :: Int -> Assoc -> ShowS Source # show :: Assoc -> String Source # showList :: [Assoc] -> ShowS Source #
Generic Assoc Source # |
Instance details Defined in Cryptol.Utils.PP Associated Types type Rep Assoc :: Type -> Type Source # Methods from :: Assoc -> Rep Assoc x Source # to :: Rep Assoc x -> Assoc Source #
NFData Assoc Source # |
Instance details Defined in Cryptol.Utils.PP Methods rnf :: Assoc -> () Source #
PP Assoc Source # |
Instance details Defined in Cryptol.Utils.PP Methods ppPrec :: Int -> Assoc -> Doc Source #
type Rep Assoc Source # |
Instance details Defined in Cryptol.Utils.PP type Rep Assoc = D1 ('MetaData "Assoc" "Cryptol.Utils.PP" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 #
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 #
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 #
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 #
NFData n => NFData (Schema n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Schema n -> () Source #
PPName name => PP (Schema name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Schema name -> Doc 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 #
NoPos (Schema name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Schema name -> Schema name 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.NamingEnv Methods namingEnv :: Schema PName -> BuildNamingEnv Source #
type Rep (Schema n) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (Schema n) = D1 ('MetaData "Schema" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 #
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 #
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 #
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 #
NFData n => NFData (TParam n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: TParam n -> () Source #
PPName name => PP (TParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> TParam name -> Doc 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 #
NoPos (TParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TParam name -> TParam name Source #
BindsNames (TParam PName) Source # | Generate the naming environment for a type parameter.
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: TParam PName -> BuildNamingEnv Source #
type Rep (TParam n) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (TParam n) = D1 ('MetaData "TParam" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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

Eq Kind Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Kind -> Kind -> Bool Source # (/=) :: Kind -> Kind -> Bool 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 #
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 #
NFData Kind Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Kind -> () Source #
PP Kind Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Kind -> Doc Source #
type Rep Kind Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep Kind = D1 ('MetaData "Kind" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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

TRecord [Named (Type n)]

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

TTuple [Type n]

    ([8], [32])

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

TParens (Type n)

     (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 # | Resolve fixity, then rename the resulting type.
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: Type PName -> RenameM (Type Name) 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 #
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 #
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 #
NFData n => NFData (Type n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Type n -> () Source #
PPName name => PP (Type name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Type name -> Doc 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 #
NoPos (Type name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Type name -> Type name Source #
type Rep (Type n) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (Type n) = D1 ('MetaData "Type" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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))))))))

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 #
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 #
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 #
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 #
NFData n => NFData (Prop n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Prop n -> () Source #
PPName name => PP (Prop name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Prop name -> Doc Source #
NoPos (Prop name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Prop name -> Prop name Source #
type Rep (Prop n) Source # |
Instance details Defined in Cryptol.Parser.AST type Rep (Prop n) = D1 ('MetaData "Prop" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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

data Module name Source #

A parsed module.

Constructors

Module |

Fields

- mName :: Located ModName

  Name of the module

- mInstance :: !(Maybe (Located ModName))

  Functor to instantiate (if this is a functor instnaces)

- mImports :: [Located Import]

  Imports for the module

- mDecls :: [TopDecl name]

  Declartions for the module

#### Instances

Instances details

Show name => Show (Module name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Module name -> ShowS Source # show :: Module name -> String Source # showList :: [Module name] -> ShowS Source #
Generic (Module name) Source # |
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Module name) :: Type -> Type Source # Methods from :: Module name -> Rep (Module name) x Source # to :: Rep (Module name) x -> Module name Source #
NFData name => NFData (Module name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Module name -> () Source #
(Show name, PPName name) => PP (Module name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Module name -> Doc Source #
HasLoc (Module name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: Module name -> Maybe Range Source #
NoPos (Module name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Module name -> Module name Source #
RemovePatterns (Module PName) Source # |
Instance details Defined in Cryptol.Parser.NoPat Methods removePatterns :: Module PName -> (Module PName, [Error]) Source #
BindsNames (Module PName) Source # | The naming environment for a single module. This is the mapping from unqualified names to fully qualified names with uniques.
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: Module PName -> BuildNamingEnv Source #
type Rep (Module name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (Module name) = D1 ('MetaData "Module" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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]))))

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 #
(Show name, PPName name) => PP (Program name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Program name -> Doc 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 #

data TopDecl name Source #

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

Instances details

Rename TopDecl Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: TopDecl PName -> RenameM (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 #
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 #
NFData name => NFData (TopDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: TopDecl name -> () Source #
(Show name, PPName name) => PP (TopDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> TopDecl name -> Doc Source #
HasLoc (TopDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: TopDecl name -> Maybe Range Source #
NoPos (TopDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TopDecl name -> TopDecl name Source #
BindsNames (InModule (TopDecl PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (TopDecl PName) -> BuildNamingEnv Source #
FromDecl (TopDecl Name) Source # |
Instance details Defined in Cryptol.TypeCheck.Depends Methods toBind :: TopDecl Name -> Maybe (Bind Name) Source # toParamFun :: TopDecl Name -> Maybe (ParameterFun Name) Source # toParamConstraints :: TopDecl Name -> [Located (Prop Name)] Source # toTyDecl :: TopDecl Name -> Maybe TyDecl Source # isTopDecl :: TopDecl Name -> Bool Source #
type Rep (TopDecl name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (TopDecl name) = D1 ('MetaData "TopDecl" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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))))))

data Decl name Source #

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

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 #
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 #
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 #
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 #
NFData name => NFData (Decl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Decl name -> () Source #
(Show name, PPName name) => PP (Decl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Decl name -> Doc 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 #
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 #
BindsNames (InModule (Decl PName)) Source # | The naming environment for a single declaration.
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (Decl PName) -> BuildNamingEnv Source #
FromDecl (Decl Name) Source # |
Instance details Defined in Cryptol.TypeCheck.Depends Methods toBind :: Decl Name -> Maybe (Bind Name) Source # toParamFun :: Decl Name -> Maybe (ParameterFun Name) Source # toParamConstraints :: Decl Name -> [Located (Prop Name)] Source # toTyDecl :: Decl Name -> Maybe TyDecl Source # isTopDecl :: 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-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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)))))

data Fixity Source #

Constructors

Fixity |

Fields

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

#### Instances

Instances details

Eq Fixity Source # |
Instance details Defined in Cryptol.Parser.Fixity Methods (==) :: Fixity -> Fixity -> Bool Source # (/=) :: Fixity -> Fixity -> Bool Source #
Show Fixity Source # |
Instance details Defined in Cryptol.Parser.Fixity Methods showsPrec :: Int -> Fixity -> ShowS Source # show :: Fixity -> String Source # showList :: [Fixity] -> ShowS Source #
Generic Fixity Source # |
Instance details Defined in Cryptol.Parser.Fixity Associated Types type Rep Fixity :: Type -> Type Source # Methods from :: Fixity -> Rep Fixity x Source # to :: Rep Fixity x -> Fixity Source #
NFData Fixity Source # |
Instance details Defined in Cryptol.Parser.Fixity Methods rnf :: Fixity -> () Source #
PP Fixity Source # |
Instance details Defined in Cryptol.Parser.Fixity Methods ppPrec :: Int -> Fixity -> Doc Source #
type Rep Fixity Source # |
Instance details Defined in Cryptol.Parser.Fixity type Rep Fixity = D1 ('MetaData "Fixity" "Cryptol.Parser.Fixity" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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

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

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

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 #
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 #
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 #
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 #
NFData n => NFData (TySyn n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: TySyn n -> () Source #
PPName name => PP (TySyn name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> TySyn name -> Doc Source #
NoPos (TySyn name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TySyn name -> TySyn name Source #
type Rep (TySyn n) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (TySyn n) = D1 ('MetaData "TySyn" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 #
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 #
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 #
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 #
NFData n => NFData (PropSyn n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: PropSyn n -> () Source #
PPName name => PP (PropSyn name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> PropSyn name -> Doc Source #
NoPos (PropSyn name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: PropSyn name -> PropSyn name Source #
type Rep (PropSyn n) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (PropSyn n) = D1 ('MetaData "PropSyn" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 String

  Optional doc string

#### 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 #
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 #
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 #
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 #
NFData name => NFData (Bind name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Bind name -> () Source #
(Show name, PPName name) => PP (Bind name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Bind name -> Doc Source #
HasLoc (Bind name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: Bind name -> Maybe Range Source #
NoPos (Bind name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Bind name -> Bind name Source #
BindsNames (InModule (Bind PName)) Source # | Introduce the name
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (Bind PName) -> BuildNamingEnv Source #
type Rep (Bind name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (Bind name) = D1 ('MetaData "Bind" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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)))))))

data BindDef name Source #

Constructors

DPrim |
DExpr (Expr 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 #
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 #
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 #
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 #
NFData name => NFData (BindDef name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: BindDef name -> () Source #
(Show name, PPName name) => PP (BindDef name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> BindDef name -> Doc Source #
type Rep (BindDef name) Source # |
Instance details Defined in Cryptol.Parser.AST type Rep (BindDef name) = D1 ('MetaData "BindDef" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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))))

type LBindDef = Located (BindDef PName) Source #

data Pragma Source #

Constructors

PragmaNote String |
PragmaProperty |

#### Instances

Instances details

Eq Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Pragma -> Pragma -> Bool Source # (/=) :: Pragma -> Pragma -> Bool 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 #
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 #
NFData Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Pragma -> () Source #
PP Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Pragma -> Doc Source #
NoPos Pragma Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Pragma -> Pragma Source #
type Rep Pragma Source # |
Instance details Defined in Cryptol.Parser.AST type Rep Pragma = D1 ('MetaData "Pragma" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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

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 #

Show ExportType Source # |
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ExportType -> ShowS Source # show :: ExportType -> String Source # showList :: [ExportType] -> ShowS Source #
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 #
NFData ExportType Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ExportType -> () Source #
type Rep ExportType Source # |
Instance details Defined in Cryptol.Parser.AST type Rep ExportType = D1 ('MetaData "ExportType" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 String)
- tlValue :: a

#### Instances

Instances details

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 #
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 #
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 #
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 #
NFData a => NFData (TopLevel a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: TopLevel a -> () Source #
PP a => PP (TopLevel a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> TopLevel a -> Doc Source #
HasLoc a => HasLoc (TopLevel a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: TopLevel a -> Maybe Range Source #
NoPos a => NoPos (TopLevel a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TopLevel a -> 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-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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))))

data Import Source #

An import declaration.

Constructors

Import |

Fields

- iModule :: !ModName
- iAs :: Maybe ModName
- iSpec :: Maybe ImportSpec

#### Instances

Instances details

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

Instance details

Defined in Cryptol.Parser.AST

type Rep Import = D1 ('MetaData "Import" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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.

Constructors

Hiding [Ident] |
Only [Ident] |

#### Instances

Instances details

Eq ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: ImportSpec -> ImportSpec -> Bool Source # (/=) :: ImportSpec -> ImportSpec -> Bool 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 #
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 #
NFData ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ImportSpec -> () Source #
PP ImportSpec Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ImportSpec -> Doc Source #
type Rep ImportSpec Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep ImportSpec = D1 ('MetaData "ImportSpec" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 Newtype name Source #

Constructors

Newtype |

Fields

- nName :: Located name

  Type name

- nParams :: [TParam name]

  Type params

- nBody :: [Named (Type name)]

  Constructor

#### Instances

Instances details

Rename Newtype Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods rename :: Newtype PName -> RenameM (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 #
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 #
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 #
NFData name => NFData (Newtype name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Newtype name -> () Source #
PPName name => PP (Newtype name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Newtype name -> Doc Source #
HasLoc (Newtype name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: Newtype name -> Maybe Range Source #
NoPos (Newtype name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Newtype name -> Newtype name Source #
BindsNames (InModule (Newtype PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (Newtype PName) -> BuildNamingEnv Source #
type Rep (Newtype name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (Newtype name) = D1 ('MetaData "Newtype" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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)]))))

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 #
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 #
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 #
NFData name => NFData (PrimType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: PrimType name -> () Source #
(Show name, PPName name) => PP (PrimType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> PrimType name -> Doc Source #
HasLoc (PrimType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: PrimType name -> Maybe Range Source #
NoPos (PrimType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: PrimType name -> PrimType name Source #
BindsNames (InModule (PrimType PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (PrimType PName) -> BuildNamingEnv Source #
type Rep (PrimType name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (PrimType name) = D1 ('MetaData "PrimType" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 |

Fields

- ptName :: Located name

  name of type parameter

- ptKind :: Kind

  kind of parameter

- ptDoc :: Maybe String

  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 #
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 #
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 #
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 #
NFData name => NFData (ParameterType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ParameterType name -> () Source #
(Show name, PPName name) => PP (ParameterType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ParameterType name -> Doc Source #
HasLoc (ParameterType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: ParameterType name -> Maybe Range Source #
NoPos (ParameterType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ParameterType name -> ParameterType name Source #
BindsNames (InModule (ParameterType PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (ParameterType PName) -> BuildNamingEnv Source #
type Rep (ParameterType name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (ParameterType name) = D1 ('MetaData "ParameterType" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 |

Fields

- pfName :: Located name

  name of value parameter

- pfSchema :: Schema name

  schema for parameter

- pfDoc :: Maybe String

  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 #
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 #
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 #
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 #
NFData name => NFData (ParameterFun name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ParameterFun name -> () Source #
(Show name, PPName name) => PP (ParameterFun name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> ParameterFun name -> Doc Source #
HasLoc (ParameterFun name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: ParameterFun name -> Maybe Range Source #
NoPos (ParameterFun x) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: ParameterFun x -> ParameterFun x Source #
BindsNames (InModule (ParameterFun PName)) Source # |
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (ParameterFun PName) -> BuildNamingEnv Source #
type Rep (ParameterFun name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (ParameterFun name) = D1 ('MetaData "ParameterFun" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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

data ReplInput name Source #

Input at the REPL, which can either be an expression or a `let` statement.

Constructors

ExprInput (Expr name) |
LetInput (Decl name) |

#### Instances

Instances details

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 #
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 #

# Expressions

data Expr n Source #

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) | ``(x + 1)`, `x` is a type

EFun [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 (Expr n) (Located n) Fixity (Expr n) | `a + b` (Removed by Fixity)

#### 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 #
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 #
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 #
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 #
NFData n => NFData (Expr n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Expr n -> () Source #
(Show name, PPName name) => PP (Expr name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Expr name -> Doc 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 #
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 #
type Rep (Expr n) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (Expr n) = D1 ('MetaData "Expr" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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)))))))))

data Literal Source #

Literals.

Constructors

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

ECString String

    "hello"

#### Instances

Instances details

Eq Literal Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Literal -> Literal -> Bool Source # (/=) :: Literal -> Literal -> Bool 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 #
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 #
NFData Literal Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Literal -> () Source #
PP Literal Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Literal -> Doc Source #
type Rep Literal Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep Literal = D1 ('MetaData "Literal" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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)))

data NumInfo Source #

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

Instances details

Eq NumInfo Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: NumInfo -> NumInfo -> Bool Source # (/=) :: NumInfo -> NumInfo -> Bool 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 #
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 #
NFData NumInfo Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: NumInfo -> () Source #
type Rep NumInfo Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep NumInfo = D1 ('MetaData "NumInfo" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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)))))

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 #
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 #
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 #
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 #
NFData name => NFData (Match name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Match name -> () Source #
(Show name, PPName name) => PP (Match name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Match name -> Doc Source #
HasLoc (Match name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods getLoc :: Match name -> Maybe Range Source #
NoPos (Match name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Match name -> Match name Source #
type Rep (Match name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (Match name) = D1 ('MetaData "Match" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 [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

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 #
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 #
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 #
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 #
NFData n => NFData (Pattern n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Pattern n -> () Source #
PPName name => PP (Pattern name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> Pattern name -> Doc 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 #
NoPos (Pattern name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Pattern name -> Pattern name Source #
type Rep (Pattern n) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (Pattern n) = D1 ('MetaData "Pattern" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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)))))

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

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 #
Show Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Methods showsPrec :: Int -> Selector -> ShowS Source # show :: Selector -> String Source # showList :: [Selector] -> ShowS Source #
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 #
NFData Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Methods rnf :: Selector -> () Source #
PP Selector Source # |
Instance details Defined in Cryptol.Parser.Selector Methods ppPrec :: Int -> Selector -> Doc Source #
ShowParseable Selector Source # |
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Selector -> Doc Source #
type Rep Selector Source # |

Instance details

Defined in Cryptol.Parser.Selector

type Rep Selector = D1 ('MetaData "Selector" "Cryptol.Parser.Selector" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 #
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 #
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 #
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 #
NFData name => NFData (TypeInst name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: TypeInst name -> () Source #
PPName name => PP (TypeInst name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> TypeInst name -> Doc Source #
NoPos (TypeInst name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TypeInst name -> TypeInst name Source #
type Rep (TypeInst name) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (TypeInst name) = D1 ('MetaData "TypeInst" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 #
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 #
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 #
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 #
NFData n => NFData (UpdField n) Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: UpdField n -> () Source #
(Show name, PPName name) => PP (UpdField name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> UpdField name -> Doc Source #
NoPos (UpdField name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: UpdField name -> UpdField name Source #
type Rep (UpdField n) Source # |

Instance details

Defined in Cryptol.Parser.AST

type Rep (UpdField n) = D1 ('MetaData "UpdField" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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

Eq UpdHow Source # |
Instance details Defined in Cryptol.Parser.AST Methods (==) :: UpdHow -> UpdHow -> Bool Source # (/=) :: UpdHow -> UpdHow -> Bool 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 #
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 #
NFData UpdHow Source # |
Instance details Defined in Cryptol.Parser.AST Methods rnf :: UpdHow -> () Source #
PP UpdHow Source # |
Instance details Defined in Cryptol.Parser.AST Methods ppPrec :: Int -> UpdHow -> Doc Source #
type Rep UpdHow Source # |
Instance details Defined in Cryptol.Parser.AST type Rep UpdHow = D1 ('MetaData "UpdHow" "Cryptol.Parser.AST" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" 'False) (C1 ('MetaCons "UpdSet" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UpdFun" 'PrefixI 'False) (U1 :: Type -> Type))

# Positions

data Located a Source #

Constructors

Located |

Fields

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

#### Instances

Instances details

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 #
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 #
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 #
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 #
NFData a => NFData (Located a) Source # |
Instance details Defined in Cryptol.Parser.Position Methods rnf :: Located a -> () Source #
PPName a => PPName (Located a) Source # |
Instance details 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 # |
Instance details Defined in Cryptol.Parser.Position Methods ppPrec :: Int -> Located a -> Doc 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 #
NoPos (Located t) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Located t -> Located t Source #
ShowParseable a => ShowParseable (Located a) Source # |
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Located a -> Doc Source #
type Rep (Located a) Source # |

Instance details

Defined in Cryptol.Parser.Position

type Rep (Located a) = D1 ('MetaData "Located" "Cryptol.Parser.Position" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 t => NoPos [t] Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: [t] -> [t] Source #
NoPos t => NoPos (Maybe t) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Maybe t -> Maybe t Source #
NoPos (Located t) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Located t -> Located t Source #
NoPos (Prop name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Prop name -> Prop name Source #
NoPos (Type name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Type name -> Type name Source #
NoPos (TParam name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TParam name -> TParam name Source #
NoPos (Schema name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Schema name -> Schema name Source #
NoPos t => NoPos (Named t) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Named t -> Named t Source #
NoPos (Pattern name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Pattern name -> Pattern name Source #
NoPos (Match name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Match name -> Match 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 (Expr name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Expr name -> Expr name Source #
NoPos a => NoPos (TopLevel a) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TopLevel a -> TopLevel a Source #
NoPos (PrimType name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: PrimType name -> PrimType name Source #
NoPos (Newtype name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Newtype name -> Newtype name Source #
NoPos (Bind name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Bind name -> Bind name Source #
NoPos (PropSyn name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: PropSyn name -> PropSyn name Source #
NoPos (TySyn name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TySyn name -> TySyn 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 (Decl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Decl name -> Decl name Source #
NoPos (TopDecl name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: TopDecl name -> TopDecl name Source #
NoPos (Module name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Module name -> Module name Source #
NoPos (Program name) Source # |
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Program name -> Program name 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.