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]
- | TTyApp [Named (Type n)]
- | TRecord (Rec (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 (Rec (Expr n))
- | ESel (Expr n) Selector
- | EUpd (Maybe (Expr n)) [UpdField n]
- | EList [Expr n]
- | EFromTo (Type n) (Maybe (Type n)) (Type n) (Maybe (Type n))
- | 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
- | ECChar Char
- | ECFrac Rational FracInfo
- | ECString String
data NumInfo
- = BinLit Int
- | OctLit Int
- | DecLit
- | HexLit Int
- | PolyLit Int
data FracInfo
- = BinFrac
- | OctFrac
- | DecFrac
- | HexFrac
data Match name
- = Match (Pattern name) (Expr name)
- | MatchLet (Bind name)
data Pattern n
- = PVar (Located n)
- | PWild
- | PTuple [Pattern n]
- | PRecord (Rec (Pattern n))
- | PList [Pattern n]
- | PTyped (Pattern n) (Type n)
- | PSplit (Pattern n) (Pattern n)
- | PLocated (Pattern n) Range
data Selector
- = TupleSel Int (Maybe Int)
- | RecordSel Ident (Maybe [Ident])
- | ListSel Int (Maybe Int)
data TypeInst name
- = NamedInst (Named (Type name))
- | PosInst (Type name)
data UpdField n = UpdField UpdHow [Located Selector] (Expr n)
data UpdHow
- = UpdSet
- | UpdFun
data 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

Eq Ident Source #
Instance details Defined in Cryptol.Utils.Ident Methods (==) :: Ident -> Ident -> Bool # (/=) :: Ident -> Ident -> Bool #
Ord Ident Source #
Instance details Defined in Cryptol.Utils.Ident Methods compare :: Ident -> Ident -> Ordering # (<) :: Ident -> Ident -> Bool # (<=) :: Ident -> Ident -> Bool # (>) :: Ident -> Ident -> Bool # (>=) :: Ident -> Ident -> Bool # max :: Ident -> Ident -> Ident # min :: Ident -> Ident -> Ident #
Show Ident Source #
Instance details Defined in Cryptol.Utils.Ident Methods showsPrec :: Int -> Ident -> ShowS # show :: Ident -> String # showList :: [Ident] -> ShowS #
IsString Ident Source #
Instance details Defined in Cryptol.Utils.Ident Methods fromString :: String -> Ident #
Generic Ident Source #
Instance details Defined in Cryptol.Utils.Ident Associated Types type Rep Ident :: Type -> Type # Methods from :: Ident -> Rep Ident x # to :: Rep Ident x -> Ident #
NFData Ident Source #
Instance details Defined in Cryptol.Utils.Ident Methods rnf :: Ident -> () #
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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

Eq ModName Source #
Instance details Defined in Cryptol.Utils.Ident Methods (==) :: ModName -> ModName -> Bool # (/=) :: ModName -> ModName -> Bool #
Ord ModName Source #
Instance details Defined in Cryptol.Utils.Ident Methods compare :: ModName -> ModName -> Ordering # (<) :: ModName -> ModName -> Bool # (<=) :: ModName -> ModName -> Bool # (>) :: ModName -> ModName -> Bool # (>=) :: ModName -> ModName -> Bool # max :: ModName -> ModName -> ModName # min :: ModName -> ModName -> ModName #
Show ModName Source #
Instance details Defined in Cryptol.Utils.Ident Methods showsPrec :: Int -> ModName -> ShowS # show :: ModName -> String # showList :: [ModName] -> ShowS #
Generic ModName Source #
Instance details Defined in Cryptol.Utils.Ident Associated Types type Rep ModName :: Type -> Type # Methods from :: ModName -> Rep ModName x # to :: Rep ModName x -> ModName #
NFData ModName Source #
Instance details Defined in Cryptol.Utils.Ident Methods rnf :: ModName -> () #
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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

Eq PName Source #
Instance details Defined in Cryptol.Parser.Name Methods (==) :: PName -> PName -> Bool # (/=) :: PName -> PName -> Bool #
Ord PName Source #
Instance details Defined in Cryptol.Parser.Name Methods compare :: PName -> PName -> Ordering # (<) :: PName -> PName -> Bool # (<=) :: PName -> PName -> Bool # (>) :: PName -> PName -> Bool # (>=) :: PName -> PName -> Bool # max :: PName -> PName -> PName # min :: PName -> PName -> PName #
Show PName Source #
Instance details Defined in Cryptol.Parser.Name Methods showsPrec :: Int -> PName -> ShowS # show :: PName -> String # showList :: [PName] -> ShowS #
Generic PName Source #
Instance details Defined in Cryptol.Parser.Name Associated Types type Rep PName :: Type -> Type # Methods from :: PName -> Rep PName x # to :: Rep PName x -> PName #
NFData PName Source #
Instance details Defined in Cryptol.Parser.Name Methods rnf :: PName -> () #
PPName PName Source #
Instance details Defined in Cryptol.Parser.Name Methods ppNameFixity :: PName -> Maybe Fixity 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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

Functor Named Source #
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Named a -> Named b # (<$) :: a -> Named b -> Named a #
Foldable Named Source #
Instance details Defined in Cryptol.Parser.AST Methods fold :: Monoid m => Named m -> m # foldMap :: Monoid m => (a -> m) -> Named a -> m # foldr :: (a -> b -> b) -> b -> Named a -> b # foldr' :: (a -> b -> b) -> b -> Named a -> b # foldl :: (b -> a -> b) -> b -> Named a -> b # foldl' :: (b -> a -> b) -> b -> Named a -> b # foldr1 :: (a -> a -> a) -> Named a -> a # foldl1 :: (a -> a -> a) -> Named a -> a # toList :: Named a -> [a] # null :: Named a -> Bool # length :: Named a -> Int # elem :: Eq a => a -> Named a -> Bool # maximum :: Ord a => Named a -> a # minimum :: Ord a => Named a -> a # sum :: Num a => Named a -> a # product :: Num a => Named a -> a #
Traversable Named Source #
Instance details Defined in Cryptol.Parser.AST Methods traverse :: Applicative f => (a -> f b) -> Named a -> f (Named b) # sequenceA :: Applicative f => Named (f a) -> f (Named a) # mapM :: Monad m => (a -> m b) -> Named a -> m (Named b) # sequence :: Monad m => Named (m a) -> m (Named a) #
Eq a => Eq (Named a) Source #
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Named a -> Named a -> Bool # (/=) :: Named a -> Named a -> Bool #
Show a => Show (Named a) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Named a -> ShowS # show :: Named a -> String # showList :: [Named a] -> ShowS #
Generic (Named a) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Named a) :: Type -> Type # Methods from :: Named a -> Rep (Named a) x # to :: Rep (Named a) x -> Named a #
NFData a => NFData (Named a) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Named a -> () #
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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

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

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

Functor Schema Source #
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Schema a -> Schema b # (<$) :: a -> Schema b -> Schema a #
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 # (/=) :: Schema n -> Schema n -> Bool #
Show n => Show (Schema n) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Schema n -> ShowS # show :: Schema n -> String # showList :: [Schema n] -> ShowS #
Generic (Schema n) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Schema n) :: Type -> Type # Methods from :: Schema n -> Rep (Schema n) x # to :: Rep (Schema n) x -> Schema n #
NFData n => NFData (Schema n) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Schema n -> () #
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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

Functor TParam Source #
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> TParam a -> TParam b # (<$) :: a -> TParam b -> TParam a #
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 # (/=) :: TParam n -> TParam n -> Bool #
Show n => Show (TParam n) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> TParam n -> ShowS # show :: TParam n -> String # showList :: [TParam n] -> ShowS #
Generic (TParam n) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (TParam n) :: Type -> Type # Methods from :: TParam n -> Rep (TParam n) x # to :: Rep (TParam n) x -> TParam n #
NFData n => NFData (TParam n) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: TParam n -> () #
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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

Eq Kind Source #
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Kind -> Kind -> Bool # (/=) :: Kind -> Kind -> Bool #
Show Kind Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Kind -> ShowS # show :: Kind -> String # showList :: [Kind] -> ShowS #
Generic Kind Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep Kind :: Type -> Type # Methods from :: Kind -> Rep Kind x # to :: Rep Kind x -> Kind #
NFData Kind Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Kind -> () #
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.9.1-EDtcoHURvveHmx5M6ZZjMK" False) ((C1 (MetaCons "KProp" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "KNum" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "KType" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "KFun" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind))))

data Type n Source #

Constructors

TFun (Type n) (Type n)	[8] -> [8]
TSeq (Type n) (Type n)	[8] a
TBit	Bit
TNum Integer	10
TChar Char	`a`
TUser n [Type n]	A type variable or synonym
TTyApp [Named (Type n)]	`{ x = [8], y = Integer }
TRecord (Rec (Type n))	{ x : [8], y : [32] }
TTuple [Type n]	([8], [32])
TWild	`_`, just some type.
TLocated (Type n) Range	Location information
TParens (Type n)	(ty)
TInfix (Type n) (Located n) Fixity (Type n)	ty + ty

Instances

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

newtype Prop n Source #

A Prop is a Type that represents a type constraint.

Constructors

CType (Type n)

Instances

Functor Prop Source #
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Prop a -> Prop b # (<$) :: a -> Prop b -> Prop a #
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 # (/=) :: Prop n -> Prop n -> Bool #
Show n => Show (Prop n) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Prop n -> ShowS # show :: Prop n -> String # showList :: [Prop n] -> ShowS #
Generic (Prop n) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Prop n) :: Type -> Type # Methods from :: Prop n -> Rep (Prop n) x # to :: Rep (Prop n) x -> Prop n #
NFData n => NFData (Prop n) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Prop n -> () #
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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

Show name => Show (Module name) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Module name -> ShowS # show :: Module name -> String # showList :: [Module name] -> ShowS #
Generic (Module name) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Module name) :: Type -> Type # Methods from :: Module name -> Rep (Module name) x # to :: Rep (Module name) x -> Module name #
NFData name => NFData (Module name) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Module name -> () #
(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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

Show name => Show (Program name) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Program name -> ShowS # show :: Program name -> String # showList :: [Program name] -> ShowS #
(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

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 # show :: TopDecl name -> String # showList :: [TopDecl name] -> ShowS #
Generic (TopDecl name) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (TopDecl name) :: Type -> Type # Methods from :: TopDecl name -> Rep (TopDecl name) x # to :: Rep (TopDecl name) x -> TopDecl name #
NFData name => NFData (TopDecl name) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: TopDecl name -> () #
(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 #
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 #
BindsNames (InModule (TopDecl PName)) Source #
Instance details Defined in Cryptol.ModuleSystem.NamingEnv Methods namingEnv :: InModule (TopDecl PName) -> BuildNamingEnv 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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

Functor Decl Source #
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Decl a -> Decl b # (<$) :: a -> Decl b -> Decl a #
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 # (/=) :: Decl name -> Decl name -> Bool #
Show name => Show (Decl name) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Decl name -> ShowS # show :: Decl name -> String # showList :: [Decl name] -> ShowS #
Generic (Decl name) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Decl name) :: Type -> Type # Methods from :: Decl name -> Rep (Decl name) x # to :: Rep (Decl name) x -> Decl name #
NFData name => NFData (Decl name) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Decl name -> () #
(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 #
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 #
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 #
type Rep (Decl name) Source #
Instance details Defined in Cryptol.Parser.AST type Rep (Decl name) = D1 (MetaData "Decl" "Cryptol.Parser.AST" "cryptol-2.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

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

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

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

Let op1 have fixity f1 and op2 have fixity f2. ThencompareFixity f1 f2determines how to parse the infix expressionx op1 y op2 z@.

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

data TySyn n Source #

Constructors

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

Instances

Functor TySyn Source #
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> TySyn a -> TySyn b # (<$) :: a -> TySyn b -> TySyn a #
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 # (/=) :: TySyn n -> TySyn n -> Bool #
Show n => Show (TySyn n) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> TySyn n -> ShowS # show :: TySyn n -> String # showList :: [TySyn n] -> ShowS #
Generic (TySyn n) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (TySyn n) :: Type -> Type # Methods from :: TySyn n -> Rep (TySyn n) x # to :: Rep (TySyn n) x -> TySyn n #
NFData n => NFData (TySyn n) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: TySyn n -> () #
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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

Functor PropSyn Source #
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> PropSyn a -> PropSyn b # (<$) :: a -> PropSyn b -> PropSyn a #
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 # (/=) :: PropSyn n -> PropSyn n -> Bool #
Show n => Show (PropSyn n) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> PropSyn n -> ShowS # show :: PropSyn n -> String # showList :: [PropSyn n] -> ShowS #
Generic (PropSyn n) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (PropSyn n) :: Type -> Type # Methods from :: PropSyn n -> Rep (PropSyn n) x # to :: Rep (PropSyn n) x -> PropSyn n #
NFData n => NFData (PropSyn n) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: PropSyn n -> () #
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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

Functor Bind Source #
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Bind a -> Bind b # (<$) :: a -> Bind b -> Bind a #
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 # (/=) :: Bind name -> Bind name -> Bool #
Show name => Show (Bind name) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Bind name -> ShowS # show :: Bind name -> String # showList :: [Bind name] -> ShowS #
Generic (Bind name) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Bind name) :: Type -> Type # Methods from :: Bind name -> Rep (Bind name) x # to :: Rep (Bind name) x -> Bind name #
NFData name => NFData (Bind name) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Bind name -> () #
(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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

Functor BindDef Source #
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> BindDef a -> BindDef b # (<$) :: a -> BindDef b -> BindDef a #
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 # (/=) :: BindDef name -> BindDef name -> Bool #
Show name => Show (BindDef name) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> BindDef name -> ShowS # show :: BindDef name -> String # showList :: [BindDef name] -> ShowS #
Generic (BindDef name) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (BindDef name) :: Type -> Type # Methods from :: BindDef name -> Rep (BindDef name) x # to :: Rep (BindDef name) x -> BindDef name #
NFData name => NFData (BindDef name) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: BindDef name -> () #
(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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

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

Eq ExportType Source #
Instance details Defined in Cryptol.Parser.AST Methods (==) :: ExportType -> ExportType -> Bool # (/=) :: ExportType -> ExportType -> Bool #
Ord ExportType Source #
Instance details Defined in Cryptol.Parser.AST Methods compare :: ExportType -> ExportType -> Ordering # (<) :: ExportType -> ExportType -> Bool # (<=) :: ExportType -> ExportType -> Bool # (>) :: ExportType -> ExportType -> Bool # (>=) :: ExportType -> ExportType -> Bool # max :: ExportType -> ExportType -> ExportType # min :: ExportType -> ExportType -> ExportType #
Show ExportType Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ExportType -> ShowS # show :: ExportType -> String # showList :: [ExportType] -> ShowS #
Generic ExportType Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep ExportType :: Type -> Type # Methods from :: ExportType -> Rep ExportType x # to :: Rep ExportType x -> ExportType #
NFData ExportType Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ExportType -> () #
type Rep ExportType Source #
Instance details Defined in Cryptol.Parser.AST type Rep ExportType = D1 (MetaData "ExportType" "Cryptol.Parser.AST" "cryptol-2.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

Functor TopLevel Source #
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> TopLevel a -> TopLevel b # (<$) :: a -> TopLevel b -> TopLevel a #
Foldable TopLevel Source #
Instance details Defined in Cryptol.Parser.AST Methods fold :: Monoid m => TopLevel m -> m # foldMap :: Monoid m => (a -> m) -> TopLevel a -> m # foldr :: (a -> b -> b) -> b -> TopLevel a -> b # foldr' :: (a -> b -> b) -> b -> TopLevel a -> b # foldl :: (b -> a -> b) -> b -> TopLevel a -> b # foldl' :: (b -> a -> b) -> b -> TopLevel a -> b # foldr1 :: (a -> a -> a) -> TopLevel a -> a # foldl1 :: (a -> a -> a) -> TopLevel a -> a # toList :: TopLevel a -> [a] # null :: TopLevel a -> Bool # length :: TopLevel a -> Int # elem :: Eq a => a -> TopLevel a -> Bool # maximum :: Ord a => TopLevel a -> a # minimum :: Ord a => TopLevel a -> a # sum :: Num a => TopLevel a -> a # product :: Num a => TopLevel a -> a #
Traversable TopLevel Source #
Instance details Defined in Cryptol.Parser.AST Methods traverse :: Applicative f => (a -> f b) -> TopLevel a -> f (TopLevel b) # sequenceA :: Applicative f => TopLevel (f a) -> f (TopLevel a) # mapM :: Monad m => (a -> m b) -> TopLevel a -> m (TopLevel b) # sequence :: Monad m => TopLevel (m a) -> m (TopLevel a) #
Show a => Show (TopLevel a) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> TopLevel a -> ShowS # show :: TopLevel a -> String # showList :: [TopLevel a] -> ShowS #
Generic (TopLevel a) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (TopLevel a) :: Type -> Type # Methods from :: TopLevel a -> Rep (TopLevel a) x # to :: Rep (TopLevel a) x -> TopLevel a #
NFData a => NFData (TopLevel a) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: TopLevel a -> () #
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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

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

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

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 # (/=) :: Newtype name -> Newtype name -> Bool #
Show name => Show (Newtype name) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Newtype name -> ShowS # show :: Newtype name -> String # showList :: [Newtype name] -> ShowS #
Generic (Newtype name) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Newtype name) :: Type -> Type # Methods from :: Newtype name -> Rep (Newtype name) x # to :: Rep (Newtype name) x -> Newtype name #
NFData name => NFData (Newtype name) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Newtype name -> () #
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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

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 # show :: PrimType name -> String # showList :: [PrimType name] -> ShowS #
Generic (PrimType name) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (PrimType name) :: Type -> Type # Methods from :: PrimType name -> Rep (PrimType name) x # to :: Rep (PrimType name) x -> PrimType name #
NFData name => NFData (PrimType name) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: PrimType name -> () #
(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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

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 # (/=) :: ParameterType name -> ParameterType name -> Bool #
Show name => Show (ParameterType name) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ParameterType name -> ShowS # show :: ParameterType name -> String # showList :: [ParameterType name] -> ShowS #
Generic (ParameterType name) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (ParameterType name) :: Type -> Type # Methods from :: ParameterType name -> Rep (ParameterType name) x # to :: Rep (ParameterType name) x -> ParameterType name #
NFData name => NFData (ParameterType name) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ParameterType name -> () #
(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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

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 # (/=) :: ParameterFun name -> ParameterFun name -> Bool #
Show name => Show (ParameterFun name) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ParameterFun name -> ShowS # show :: ParameterFun name -> String # showList :: [ParameterFun name] -> ShowS #
Generic (ParameterFun name) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (ParameterFun name) :: Type -> Type # Methods from :: ParameterFun name -> Rep (ParameterFun name) x # to :: Rep (ParameterFun name) x -> ParameterFun name #
NFData name => NFData (ParameterFun name) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: ParameterFun name -> () #
(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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

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

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 (Rec (Expr n))	{ x = 1, y = 2 }
ESel (Expr n) Selector	e.l
EUpd (Maybe (Expr n)) [UpdField n]	{ r \| x = e }
EList [Expr n]	[1,2,3]
EFromTo (Type n) (Maybe (Type n)) (Type n) (Maybe (Type n))	[1, 5 .. 117 : t]
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

Functor Expr Source #
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Expr a -> Expr b # (<$) :: a -> Expr b -> Expr a #
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 # (/=) :: Expr n -> Expr n -> Bool #
Show n => Show (Expr n) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Expr n -> ShowS # show :: Expr n -> String # showList :: [Expr n] -> ShowS #
Generic (Expr n) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Expr n) :: Type -> Type # Methods from :: Expr n -> Rep (Expr n) x # to :: Rep (Expr n) x -> Expr n #
NFData n => NFData (Expr n) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Expr n -> () #
(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)

data Literal Source #

Literals.

Constructors

ECNum Integer NumInfo	`0x10` (HexLit 2)
ECChar Char	`a`
ECFrac Rational FracInfo	1.2e3
ECString String	"hello"

Instances

Eq Literal Source #
Instance details Defined in Cryptol.Parser.AST Methods (==) :: Literal -> Literal -> Bool # (/=) :: Literal -> Literal -> Bool #
Show Literal Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Literal -> ShowS # show :: Literal -> String # showList :: [Literal] -> ShowS #
Generic Literal Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep Literal :: Type -> Type # Methods from :: Literal -> Rep Literal x # to :: Rep Literal x -> Literal #
NFData Literal Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Literal -> () #
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.9.1-EDtcoHURvveHmx5M6ZZjMK" False) ((C1 (MetaCons "ECNum" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer) :: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NumInfo)) :+: C1 (MetaCons "ECChar" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Char))) :+: (C1 (MetaCons "ECFrac" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Rational) :: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FracInfo)) :+: C1 (MetaCons "ECString" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))))

data NumInfo Source #

Infromation about the representation of a numeric constant.

Constructors

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

Instances

Eq NumInfo Source #
Instance details Defined in Cryptol.Parser.AST Methods (==) :: NumInfo -> NumInfo -> Bool # (/=) :: NumInfo -> NumInfo -> Bool #
Show NumInfo Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> NumInfo -> ShowS # show :: NumInfo -> String # showList :: [NumInfo] -> ShowS #
Generic NumInfo Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep NumInfo :: Type -> Type # Methods from :: NumInfo -> Rep NumInfo x # to :: Rep NumInfo x -> NumInfo #
NFData NumInfo Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: NumInfo -> () #
type Rep NumInfo Source #
Instance details Defined in Cryptol.Parser.AST type Rep NumInfo = D1 (MetaData "NumInfo" "Cryptol.Parser.AST" "cryptol-2.9.1-EDtcoHURvveHmx5M6ZZjMK" 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 "PolyLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)))))

data FracInfo Source #

Information about fractional literals.

Constructors

BinFrac
OctFrac
DecFrac
HexFrac

Instances

Eq FracInfo Source #
Instance details Defined in Cryptol.Parser.AST Methods (==) :: FracInfo -> FracInfo -> Bool # (/=) :: FracInfo -> FracInfo -> Bool #
Show FracInfo Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> FracInfo -> ShowS # show :: FracInfo -> String # showList :: [FracInfo] -> ShowS #
Generic FracInfo Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep FracInfo :: Type -> Type # Methods from :: FracInfo -> Rep FracInfo x # to :: Rep FracInfo x -> FracInfo #
NFData FracInfo Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: FracInfo -> () #
type Rep FracInfo Source #
Instance details Defined in Cryptol.Parser.AST type Rep FracInfo = D1 (MetaData "FracInfo" "Cryptol.Parser.AST" "cryptol-2.9.1-EDtcoHURvveHmx5M6ZZjMK" False) ((C1 (MetaCons "BinFrac" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "OctFrac" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "DecFrac" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "HexFrac" PrefixI False) (U1 :: Type -> Type)))

data Match name Source #

Constructors

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

Instances

Functor Match Source #
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Match a -> Match b # (<$) :: a -> Match b -> Match a #
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 # (/=) :: Match name -> Match name -> Bool #
Show name => Show (Match name) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Match name -> ShowS # show :: Match name -> String # showList :: [Match name] -> ShowS #
Generic (Match name) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Match name) :: Type -> Type # Methods from :: Match name -> Rep (Match name) x # to :: Rep (Match name) x -> Match name #
NFData name => NFData (Match name) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Match name -> () #
(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.9.1-EDtcoHURvveHmx5M6ZZjMK" False) (C1 (MetaCons "Match" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern name)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr name))) :+: C1 (MetaCons "MatchLet" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Bind name))))

data Pattern n Source #

Constructors

PVar (Located n)	x
PWild	_
PTuple [Pattern n]	(x,y,z)
PRecord (Rec (Pattern n))	{ x = (a,b,c), y = z }
PList [Pattern n]	[ x, y, z ]
PTyped (Pattern n) (Type n)	x : [8]
PSplit (Pattern n) (Pattern n)	(x # y)
PLocated (Pattern n) Range	Location information

Instances

Functor Pattern Source #
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> Pattern a -> Pattern b # (<$) :: a -> Pattern b -> Pattern a #
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 # (/=) :: Pattern n -> Pattern n -> Bool #
Show n => Show (Pattern n) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> Pattern n -> ShowS # show :: Pattern n -> String # showList :: [Pattern n] -> ShowS #
Generic (Pattern n) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (Pattern n) :: Type -> Type # Methods from :: Pattern n -> Rep (Pattern n) x # to :: Rep (Pattern n) x -> Pattern n #
NFData n => NFData (Pattern n) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: Pattern n -> () #
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)

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

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

Functor TypeInst Source #
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> TypeInst a -> TypeInst b # (<$) :: a -> TypeInst b -> TypeInst a #
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 # (/=) :: TypeInst name -> TypeInst name -> Bool #
Show name => Show (TypeInst name) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> TypeInst name -> ShowS # show :: TypeInst name -> String # showList :: [TypeInst name] -> ShowS #
Generic (TypeInst name) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (TypeInst name) :: Type -> Type # Methods from :: TypeInst name -> Rep (TypeInst name) x # to :: Rep (TypeInst name) x -> TypeInst name #
NFData name => NFData (TypeInst name) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: TypeInst name -> () #
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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

Functor UpdField Source #
Instance details Defined in Cryptol.Parser.AST Methods fmap :: (a -> b) -> UpdField a -> UpdField b # (<$) :: a -> UpdField b -> UpdField a #
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 # (/=) :: UpdField n -> UpdField n -> Bool #
Show n => Show (UpdField n) Source #
Instance details Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> UpdField n -> ShowS # show :: UpdField n -> String # showList :: [UpdField n] -> ShowS #
Generic (UpdField n) Source #
Instance details Defined in Cryptol.Parser.AST Associated Types type Rep (UpdField n) :: Type -> Type # Methods from :: UpdField n -> Rep (UpdField n) x # to :: Rep (UpdField n) x -> UpdField n #
NFData n => NFData (UpdField n) Source #
Instance details Defined in Cryptol.Parser.AST Methods rnf :: UpdField n -> () #
(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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

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

Functor Located Source #
Instance details Defined in Cryptol.Parser.Position Methods fmap :: (a -> b) -> Located a -> Located b # (<$) :: a -> Located b -> Located a #
Eq a => Eq (Located a) Source #
Instance details Defined in Cryptol.Parser.Position Methods (==) :: Located a -> Located a -> Bool # (/=) :: Located a -> Located a -> Bool #
Ord a => Ord (Located a) Source #
Instance details Defined in Cryptol.Parser.Position Methods compare :: Located a -> Located a -> Ordering # (<) :: Located a -> Located a -> Bool # (<=) :: Located a -> Located a -> Bool # (>) :: Located a -> Located a -> Bool # (>=) :: Located a -> Located a -> Bool # max :: Located a -> Located a -> Located a # min :: Located a -> Located a -> Located a #
Show a => Show (Located a) Source #
Instance details Defined in Cryptol.Parser.Position Methods showsPrec :: Int -> Located a -> ShowS # show :: Located a -> String # showList :: [Located a] -> ShowS #
Generic (Located a) Source #
Instance details Defined in Cryptol.Parser.Position Associated Types type Rep (Located a) :: Type -> Type # Methods from :: Located a -> Rep (Located a) x # to :: Rep (Located a) x -> Located a #
NFData a => NFData (Located a) Source #
Instance details Defined in Cryptol.Parser.Position Methods rnf :: Located a -> () #
PPName a => PPName (Located a) Source #
Instance details Defined in Cryptol.Parser.Position Methods ppNameFixity :: Located a -> Maybe Fixity Source # ppPrefixName :: Located a -> Doc Source # ppInfixName :: Located a -> Doc Source #
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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

NoPos Range Source #
Instance details Defined in Cryptol.Parser.AST Methods noPos :: Range -> Range Source #
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 #
(NoPos a, NoPos b) => NoPos (a, b) Source #
Instance details Defined in Cryptol.Parser.AST Methods noPos :: (a, b) -> (a, b) Source #

Pretty-printing

cppKind :: Kind -> Doc Source #

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

ppSelector :: Selector -> Doc Source #

Display the thing selected by the selector, nicely.