Cryptol.Parser.AST

Names

data Ident

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

Defined in Cryptol.Utils.Ident

Methods

(==) :: Ident -> Ident -> Bool

(/=) :: Ident -> Ident -> Bool

Ord Ident

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

Defined in Cryptol.Utils.Ident

Methods

showsPrec :: Int -> Ident -> ShowS

show :: Ident -> String

showList :: [Ident] -> ShowS

IsString Ident

Defined in Cryptol.Utils.Ident

Methods

fromString :: String -> Ident

Generic Ident

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

Defined in Cryptol.Utils.Ident

Methods

rnf :: Ident -> ()

PP Ident

Defined in Cryptol.Utils.PP

Methods

ppPrec :: Int -> Ident -> Doc

ShowParseable Ident

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Ident -> Doc

type Rep Ident

Defined in Cryptol.Utils.Ident

type Rep Ident = D1 (MetaData "Ident" "Cryptol.Utils.Ident" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

mkInfix :: Text -> Ident

isInfixIdent :: Ident -> Bool

nullIdent :: Ident -> Bool

identText :: Ident -> Text

data ModName

Module names are just text.

Instances

Eq ModName

Defined in Cryptol.Utils.Ident

Methods

(==) :: ModName -> ModName -> Bool

(/=) :: ModName -> ModName -> Bool

Ord ModName

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

Defined in Cryptol.Utils.Ident

Methods

showsPrec :: Int -> ModName -> ShowS

show :: ModName -> String

showList :: [ModName] -> ShowS

Generic ModName

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

Defined in Cryptol.Utils.Ident

Methods

rnf :: ModName -> ()

PP ModName

Defined in Cryptol.Utils.PP

Methods

ppPrec :: Int -> ModName -> Doc

type Rep ModName

Defined in Cryptol.Utils.Ident

type Rep ModName = D1 (MetaData "ModName" "Cryptol.Utils.Ident" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (C1 (MetaCons "ModName" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Text)))

modRange :: Module name -> Range

data PName

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

Defined in Cryptol.Parser.Name

Methods

(==) :: PName -> PName -> Bool

(/=) :: PName -> PName -> Bool

Ord PName

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

Defined in Cryptol.Parser.Name

Methods

showsPrec :: Int -> PName -> ShowS

show :: PName -> String

showList :: [PName] -> ShowS

Generic PName

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

Defined in Cryptol.Parser.Name

Methods

rnf :: PName -> ()

PPName PName

Defined in Cryptol.Parser.Name

Methods

ppNameFixity :: PName -> Maybe (Assoc, Int)

ppPrefixName :: PName -> Doc

ppInfixName :: PName -> Doc

PP PName

Defined in Cryptol.Parser.Name

Methods

ppPrec :: Int -> PName -> Doc

RemovePatterns [Decl PName]

Defined in Cryptol.Parser.NoPat

Methods

removePatterns :: [Decl PName] -> ([Decl PName], [Error])

RemovePatterns (Expr PName)

Defined in Cryptol.Parser.NoPat

Methods

removePatterns :: Expr PName -> (Expr PName, [Error])

RemovePatterns (Module PName)

Defined in Cryptol.Parser.NoPat

Methods

removePatterns :: Module PName -> (Module PName, [Error])

RemovePatterns (Program PName)

Defined in Cryptol.Parser.NoPat

Methods

removePatterns :: Program PName -> (Program PName, [Error])

BindsNames (TParam PName)

Generate the naming environment for a type parameter.

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: TParam PName -> BuildNamingEnv

BindsNames (Schema PName)

Generate a type renaming environment from the parameters that are bound by this schema.

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: Schema PName -> BuildNamingEnv

BindsNames (Module PName)

The naming environment for a single module. This is the mapping from unqualified names to fully qualified names with uniques.

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: Module PName -> BuildNamingEnv

BindsNames (InModule (Newtype PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (Newtype PName) -> BuildNamingEnv

BindsNames (InModule (Bind PName))

Introduce the name

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (Bind PName) -> BuildNamingEnv

BindsNames (InModule (ParameterFun PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (ParameterFun PName) -> BuildNamingEnv

BindsNames (InModule (ParameterType PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (ParameterType PName) -> BuildNamingEnv

BindsNames (InModule (Decl PName))

The naming environment for a single declaration.

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (Decl PName) -> BuildNamingEnv

BindsNames (InModule (TopDecl PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (TopDecl PName) -> BuildNamingEnv

type Rep PName

Defined in Cryptol.Parser.Name

type Rep PName = D1 (MetaData "PName" "Cryptol.Parser.Name" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

getIdent :: PName -> Ident

mkUnqual :: Ident -> PName

mkQual :: ModName -> Ident -> PName

data Named a

Constructors

Named

Fields

• name :: Located Ident
• value :: a

Instances

Functor Named

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> Named a -> Named b

(<$) :: a -> Named b -> Named a

Foldable Named

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

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)

Defined in Cryptol.Parser.AST

Methods

(==) :: Named a -> Named a -> Bool

(/=) :: Named a -> Named a -> Bool

Show a => Show (Named a)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Named a -> ShowS

show :: Named a -> String

showList :: [Named a] -> ShowS

Generic (Named a)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: Named a -> ()

HasLoc a => HasLoc (Named a)

Defined in Cryptol.Parser.AST

Methods

getLoc :: Named a -> Maybe Range

NoPos t => NoPos (Named t)

Defined in Cryptol.Parser.AST

Methods

noPos :: Named t -> Named t

type Rep (Named a)

Defined in Cryptol.Parser.AST

type Rep (Named a) = D1 (MetaData "Named" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Passes that can generate fresh names.

Constructors

NoPat

MonoValues

Instances

Eq Pass

Defined in Cryptol.Parser.Name

Methods

(==) :: Pass -> Pass -> Bool

(/=) :: Pass -> Pass -> Bool

Ord Pass

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

Defined in Cryptol.Parser.Name

Methods

showsPrec :: Int -> Pass -> ShowS

show :: Pass -> String

showList :: [Pass] -> ShowS

Generic Pass

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

Defined in Cryptol.Parser.Name

Methods

rnf :: Pass -> ()

type Rep Pass

Defined in Cryptol.Parser.Name

type Rep Pass = D1 (MetaData "Pass" "Cryptol.Parser.Name" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (C1 (MetaCons "NoPat" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "MonoValues" PrefixI False) (U1 :: Type -> Type))

data Assoc

Information about associativity.

Constructors

LeftAssoc

RightAssoc

NonAssoc

Instances

Eq Assoc

Defined in Cryptol.Utils.PP

Methods

(==) :: Assoc -> Assoc -> Bool

(/=) :: Assoc -> Assoc -> Bool

Show Assoc

Defined in Cryptol.Utils.PP

Methods

showsPrec :: Int -> Assoc -> ShowS

show :: Assoc -> String

showList :: [Assoc] -> ShowS

Generic Assoc

Defined in Cryptol.Utils.PP

Associated Types

type Rep Assoc :: Type -> Type

Methods

from :: Assoc -> Rep Assoc x

to :: Rep Assoc x -> Assoc

NFData Assoc

Defined in Cryptol.Utils.PP

Methods

rnf :: Assoc -> ()

type Rep Assoc

Defined in Cryptol.Utils.PP

type Rep Assoc = D1 (MetaData "Assoc" "Cryptol.Utils.PP" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

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

Instances

Functor Schema

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> Schema a -> Schema b

(<$) :: a -> Schema b -> Schema a

Rename Schema

Rename a schema, assuming that none of its type variables are already in scope.

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Schema PName -> RenameM (Schema Name)

Eq n => Eq (Schema n)

Defined in Cryptol.Parser.AST

Methods

(==) :: Schema n -> Schema n -> Bool

(/=) :: Schema n -> Schema n -> Bool

Show n => Show (Schema n)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Schema n -> ShowS

show :: Schema n -> String

showList :: [Schema n] -> ShowS

Generic (Schema n)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: Schema n -> ()

PPName name => PP (Schema name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Schema name -> Doc

AddLoc (Schema name)

Defined in Cryptol.Parser.AST

Methods

addLoc :: Schema name -> Range -> Schema name

dropLoc :: Schema name -> Schema name

HasLoc (Schema name)

Defined in Cryptol.Parser.AST

Methods

getLoc :: Schema name -> Maybe Range

NoPos (Schema name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Schema name -> Schema name

BindsNames (Schema PName)

Generate a type renaming environment from the parameters that are bound by this schema.

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: Schema PName -> BuildNamingEnv

type Rep (Schema n)

Defined in Cryptol.Parser.AST

type Rep (Schema n) = D1 (MetaData "Schema" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

TParam

Fields

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

Instances

Functor TParam

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> TParam a -> TParam b

(<$) :: a -> TParam b -> TParam a

Rename TParam

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: TParam PName -> RenameM (TParam Name)

Eq n => Eq (TParam n)

Defined in Cryptol.Parser.AST

Methods

(==) :: TParam n -> TParam n -> Bool

(/=) :: TParam n -> TParam n -> Bool

Show n => Show (TParam n)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> TParam n -> ShowS

show :: TParam n -> String

showList :: [TParam n] -> ShowS

Generic (TParam n)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: TParam n -> ()

PPName name => PP (TParam name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> TParam name -> Doc

AddLoc (TParam name)

Defined in Cryptol.Parser.AST

Methods

addLoc :: TParam name -> Range -> TParam name

dropLoc :: TParam name -> TParam name

HasLoc (TParam name)

Defined in Cryptol.Parser.AST

Methods

getLoc :: TParam name -> Maybe Range

NoPos (TParam name)

Defined in Cryptol.Parser.AST

Methods

noPos :: TParam name -> TParam name

BindsNames (TParam PName)

Generate the naming environment for a type parameter.

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: TParam PName -> BuildNamingEnv

type Rep (TParam n)

Defined in Cryptol.Parser.AST

type Rep (TParam n) = D1 (MetaData "TParam" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

KNum

KType

KFun Kind Kind

Instances

Eq Kind

Defined in Cryptol.Parser.AST

Methods

(==) :: Kind -> Kind -> Bool

(/=) :: Kind -> Kind -> Bool

Show Kind

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Kind -> ShowS

show :: Kind -> String

showList :: [Kind] -> ShowS

Generic Kind

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

Defined in Cryptol.Parser.AST

Methods

rnf :: Kind -> ()

PP Kind

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Kind -> Doc

type Rep Kind

Defined in Cryptol.Parser.AST

type Rep Kind = D1 (MetaData "Kind" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (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

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

TApp TCon [Type n]

2 + x Note that the parser never produces these; instead it produces a TUser value. The TApp is introduced by the renamer when it spots built-in functions. XXX: We should just add primitive declarations for the built-in type functions, and simplify all this.

TRecord [Named (Type n)]

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

TTuple [Type n]

([8], [32])

TWild

_, just some type.

TLocated (Type n) Range

Location information

TParens (Type n)

 (ty)

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

 ty + ty

Instances

Functor Type

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> Type a -> Type b

(<$) :: a -> Type b -> Type a

Rename Type

Resolve fixity, then rename the resulting type.

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Type PName -> RenameM (Type Name)

Eq n => Eq (Type n)

Defined in Cryptol.Parser.AST

Methods

(==) :: Type n -> Type n -> Bool

(/=) :: Type n -> Type n -> Bool

Show n => Show (Type n)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Type n -> ShowS

show :: Type n -> String

showList :: [Type n] -> ShowS

Generic (Type n)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: Type n -> ()

PPName name => PP (Type name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Type name -> Doc

AddLoc (Type name)

Defined in Cryptol.Parser.AST

Methods

addLoc :: Type name -> Range -> Type name

dropLoc :: Type name -> Type name

HasLoc (Type name)

Defined in Cryptol.Parser.AST

Methods

getLoc :: Type name -> Maybe Range

NoPos (Type name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Type name -> Type name

type Rep (Type n)

Defined in Cryptol.Parser.AST

type Rep (Type n) = D1 (MetaData "Type" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (((C1 (MetaCons "TFun" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n))) :+: (C1 (MetaCons "TSeq" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n))) :+: C1 (MetaCons "TBit" PrefixI False) (U1 :: Type -> Type))) :+: (C1 (MetaCons "TNum" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer)) :+: (C1 (MetaCons "TChar" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Char)) :+: C1 (MetaCons "TUser" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 n) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Type n]))))) :+: ((C1 (MetaCons "TApp" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TCon) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Type n])) :+: (C1 (MetaCons "TRecord" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Named (Type n)])) :+: C1 (MetaCons "TTuple" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Type n])))) :+: ((C1 (MetaCons "TWild" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TLocated" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Range))) :+: (C1 (MetaCons "TParens" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n))) :+: C1 (MetaCons "TInfix" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Located n))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Fixity) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n))))))))

data Prop n

Constructors

CFin (Type n)

 fin x

CEqual (Type n) (Type n)

 x == 10

CNeq (Type n) (Type n)

 x != 10

CGeq (Type n) (Type n)

 x >= 10

CZero (Type n)

 Zero a

CLogic (Type n)

 Logic a

CArith (Type n)

 Arith a

CCmp (Type n)

 Cmp a

CSignedCmp (Type n)

 SignedCmp a

CLiteral (Type n) (Type n)

 Literal val a

CUser n [Type n]

Constraint synonym

CLocated (Prop n) Range

Location information

CType (Type n)

After parsing

Instances

Functor Prop

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> Prop a -> Prop b

(<$) :: a -> Prop b -> Prop a

Rename Prop

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Prop PName -> RenameM (Prop Name)

Eq n => Eq (Prop n)

Defined in Cryptol.Parser.AST

Methods

(==) :: Prop n -> Prop n -> Bool

(/=) :: Prop n -> Prop n -> Bool

Show n => Show (Prop n)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Prop n -> ShowS

show :: Prop n -> String

showList :: [Prop n] -> ShowS

Generic (Prop n)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: Prop n -> ()

PPName name => PP (Prop name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Prop name -> Doc

AddLoc (Prop name)

Defined in Cryptol.Parser.AST

Methods

addLoc :: Prop name -> Range -> Prop name

dropLoc :: Prop name -> Prop name

HasLoc (Prop name)

Defined in Cryptol.Parser.AST

Methods

getLoc :: Prop name -> Maybe Range

NoPos (Prop name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Prop name -> Prop name

type Rep (Prop n)

Defined in Cryptol.Parser.AST

type Rep (Prop n) = D1 (MetaData "Prop" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (((C1 (MetaCons "CFin" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n))) :+: (C1 (MetaCons "CEqual" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n))) :+: C1 (MetaCons "CNeq" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n))))) :+: (C1 (MetaCons "CGeq" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n))) :+: (C1 (MetaCons "CZero" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n))) :+: C1 (MetaCons "CLogic" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n)))))) :+: ((C1 (MetaCons "CArith" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n))) :+: (C1 (MetaCons "CCmp" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n))) :+: C1 (MetaCons "CSignedCmp" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n))))) :+: ((C1 (MetaCons "CLiteral" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n))) :+: C1 (MetaCons "CUser" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 n) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Type n]))) :+: (C1 (MetaCons "CLocated" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Prop n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Range)) :+: C1 (MetaCons "CType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n)))))))

Declarations

data Module name

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)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Module name -> ShowS

show :: Module name -> String

showList :: [Module name] -> ShowS

Generic (Module name)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: Module name -> ()

(Show name, PPName name) => PP (Module name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Module name -> Doc

HasLoc (Module name)

Defined in Cryptol.Parser.AST

Methods

getLoc :: Module name -> Maybe Range

NoPos (Module name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Module name -> Module name

RemovePatterns (Module PName)

Defined in Cryptol.Parser.NoPat

Methods

removePatterns :: Module PName -> (Module PName, [Error])

BindsNames (Module PName)

The naming environment for a single module. This is the mapping from unqualified names to fully qualified names with uniques.

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: Module PName -> BuildNamingEnv

type Rep (Module name)

Defined in Cryptol.Parser.AST

type Rep (Module name) = D1 (MetaData "Module" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

Program [TopDecl name]

Instances

Show name => Show (Program name)

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)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Program name -> Doc

NoPos (Program name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Program name -> Program name

RemovePatterns (Program PName)

Defined in Cryptol.Parser.NoPat

Methods

removePatterns :: Program PName -> (Program PName, [Error])

data TopDecl name

Constructors

Decl (TopLevel (Decl 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

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: TopDecl PName -> RenameM (TopDecl Name)

Show name => Show (TopDecl name)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> TopDecl name -> ShowS

show :: TopDecl name -> String

showList :: [TopDecl name] -> ShowS

Generic (TopDecl name)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: TopDecl name -> ()

(Show name, PPName name) => PP (TopDecl name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> TopDecl name -> Doc

HasLoc (TopDecl name)

Defined in Cryptol.Parser.AST

Methods

getLoc :: TopDecl name -> Maybe Range

NoPos (TopDecl name)

Defined in Cryptol.Parser.AST

Methods

noPos :: TopDecl name -> TopDecl name

BindsNames (InModule (TopDecl PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (TopDecl PName) -> BuildNamingEnv

FromDecl (TopDecl Name)

Defined in Cryptol.TypeCheck.Depends

Methods

toBind :: TopDecl Name -> Maybe (Bind Name)

toParamFun :: TopDecl Name -> Maybe (ParameterFun Name)

toParamConstraints :: TopDecl Name -> [Located (Prop Name)]

toTyDecl :: TopDecl Name -> Maybe TyDecl

isTopDecl :: TopDecl Name -> Bool

type Rep (TopDecl name)

Defined in Cryptol.Parser.AST

type Rep (TopDecl name) = D1 (MetaData "TopDecl" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) ((C1 (MetaCons "Decl" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TopLevel (Decl 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

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

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> Decl a -> Decl b

(<$) :: a -> Decl b -> Decl a

Rename Decl

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Decl PName -> RenameM (Decl Name)

Eq name => Eq (Decl name)

Defined in Cryptol.Parser.AST

Methods

(==) :: Decl name -> Decl name -> Bool

(/=) :: Decl name -> Decl name -> Bool

Show name => Show (Decl name)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Decl name -> ShowS

show :: Decl name -> String

showList :: [Decl name] -> ShowS

Generic (Decl name)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: Decl name -> ()

(Show name, PPName name) => PP (Decl name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Decl name -> Doc

AddLoc (Decl name)

Defined in Cryptol.Parser.AST

Methods

addLoc :: Decl name -> Range -> Decl name

dropLoc :: Decl name -> Decl name

HasLoc (Decl name)

Defined in Cryptol.Parser.AST

Methods

getLoc :: Decl name -> Maybe Range

NoPos (Decl name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Decl name -> Decl name

RemovePatterns [Decl PName]

Defined in Cryptol.Parser.NoPat

Methods

removePatterns :: [Decl PName] -> ([Decl PName], [Error])

BindsNames (InModule (Decl PName))

The naming environment for a single declaration.

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (Decl PName) -> BuildNamingEnv

FromDecl (Decl Name)

Defined in Cryptol.TypeCheck.Depends

Methods

toBind :: Decl Name -> Maybe (Bind Name)

toParamFun :: Decl Name -> Maybe (ParameterFun Name)

toParamConstraints :: Decl Name -> [Located (Prop Name)]

toTyDecl :: Decl Name -> Maybe TyDecl

isTopDecl :: Decl Name -> Bool

type Rep (Decl name)

Defined in Cryptol.Parser.AST

type Rep (Decl name) = D1 (MetaData "Decl" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

Fixity

Fields

• fAssoc :: !Assoc
• fLevel :: !Int

Instances

Eq Fixity

Defined in Cryptol.Parser.Fixity

Methods

(==) :: Fixity -> Fixity -> Bool

(/=) :: Fixity -> Fixity -> Bool

Show Fixity

Defined in Cryptol.Parser.Fixity

Methods

showsPrec :: Int -> Fixity -> ShowS

show :: Fixity -> String

showList :: [Fixity] -> ShowS

Generic Fixity

Defined in Cryptol.Parser.Fixity

Associated Types

type Rep Fixity :: Type -> Type

Methods

from :: Fixity -> Rep Fixity x

to :: Rep Fixity x -> Fixity

NFData Fixity

Defined in Cryptol.Parser.Fixity

Methods

rnf :: Fixity -> ()

type Rep Fixity

Defined in Cryptol.Parser.Fixity

type Rep Fixity = D1 (MetaData "Fixity" "Cryptol.Parser.Fixity" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

The fixity used when none is provided.

data FixityCmp

Constructors

FCError

FCLeft

FCRight

Instances

Eq FixityCmp

Defined in Cryptol.Parser.Fixity

Methods

(==) :: FixityCmp -> FixityCmp -> Bool

(/=) :: FixityCmp -> FixityCmp -> Bool

Show FixityCmp

Defined in Cryptol.Parser.Fixity

Methods

showsPrec :: Int -> FixityCmp -> ShowS

show :: FixityCmp -> String

showList :: [FixityCmp] -> ShowS

compareFixity :: Fixity -> Fixity -> FixityCmp

data TySyn n

Constructors

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

Instances

Functor TySyn

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> TySyn a -> TySyn b

(<$) :: a -> TySyn b -> TySyn a

Rename TySyn

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: TySyn PName -> RenameM (TySyn Name)

Eq n => Eq (TySyn n)

Defined in Cryptol.Parser.AST

Methods

(==) :: TySyn n -> TySyn n -> Bool

(/=) :: TySyn n -> TySyn n -> Bool

Show n => Show (TySyn n)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> TySyn n -> ShowS

show :: TySyn n -> String

showList :: [TySyn n] -> ShowS

Generic (TySyn n)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: TySyn n -> ()

PPName name => PP (TySyn name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> TySyn name -> Doc

NoPos (TySyn name)

Defined in Cryptol.Parser.AST

Methods

noPos :: TySyn name -> TySyn name

type Rep (TySyn n)

Defined in Cryptol.Parser.AST

type Rep (TySyn n) = D1 (MetaData "TySyn" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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 [TParam n]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n)))))

data PropSyn n

Constructors

PropSyn (Located n) [TParam n] [Prop n]

Instances

Functor PropSyn

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> PropSyn a -> PropSyn b

(<$) :: a -> PropSyn b -> PropSyn a

Rename PropSyn

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: PropSyn PName -> RenameM (PropSyn Name)

Eq n => Eq (PropSyn n)

Defined in Cryptol.Parser.AST

Methods

(==) :: PropSyn n -> PropSyn n -> Bool

(/=) :: PropSyn n -> PropSyn n -> Bool

Show n => Show (PropSyn n)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> PropSyn n -> ShowS

show :: PropSyn n -> String

showList :: [PropSyn n] -> ShowS

Generic (PropSyn n)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: PropSyn n -> ()

PPName name => PP (PropSyn name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> PropSyn name -> Doc

NoPos (PropSyn name)

Defined in Cryptol.Parser.AST

Methods

noPos :: PropSyn name -> PropSyn name

type Rep (PropSyn n)

Defined in Cryptol.Parser.AST

type Rep (PropSyn n) = D1 (MetaData "PropSyn" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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 [TParam n]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Prop n]))))

data Bind name

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

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> Bind a -> Bind b

(<$) :: a -> Bind b -> Bind a

Rename Bind

Rename a binding.

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Bind PName -> RenameM (Bind Name)

Eq name => Eq (Bind name)

Defined in Cryptol.Parser.AST

Methods

(==) :: Bind name -> Bind name -> Bool

(/=) :: Bind name -> Bind name -> Bool

Show name => Show (Bind name)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Bind name -> ShowS

show :: Bind name -> String

showList :: [Bind name] -> ShowS

Generic (Bind name)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: Bind name -> ()

(Show name, PPName name) => PP (Bind name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Bind name -> Doc

HasLoc (Bind name)

Defined in Cryptol.Parser.AST

Methods

getLoc :: Bind name -> Maybe Range

NoPos (Bind name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Bind name -> Bind name

BindsNames (InModule (Bind PName))

Introduce the name

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (Bind PName) -> BuildNamingEnv

type Rep (Bind name)

Defined in Cryptol.Parser.AST

type Rep (Bind name) = D1 (MetaData "Bind" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

DPrim

DExpr (Expr name)

Instances

Functor BindDef

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> BindDef a -> BindDef b

(<$) :: a -> BindDef b -> BindDef a

Rename BindDef

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: BindDef PName -> RenameM (BindDef Name)

Eq name => Eq (BindDef name)

Defined in Cryptol.Parser.AST

Methods

(==) :: BindDef name -> BindDef name -> Bool

(/=) :: BindDef name -> BindDef name -> Bool

Show name => Show (BindDef name)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> BindDef name -> ShowS

show :: BindDef name -> String

showList :: [BindDef name] -> ShowS

Generic (BindDef name)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: BindDef name -> ()

(Show name, PPName name) => PP (BindDef name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> BindDef name -> Doc

type Rep (BindDef name)

Defined in Cryptol.Parser.AST

type Rep (BindDef name) = D1 (MetaData "BindDef" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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)

data Pragma

Constructors

PragmaNote String

PragmaProperty

Instances

Eq Pragma

Defined in Cryptol.Parser.AST

Methods

(==) :: Pragma -> Pragma -> Bool

(/=) :: Pragma -> Pragma -> Bool

Show Pragma

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Pragma -> ShowS

show :: Pragma -> String

showList :: [Pragma] -> ShowS

Generic Pragma

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

Defined in Cryptol.Parser.AST

Methods

rnf :: Pragma -> ()

PP Pragma

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Pragma -> Doc

NoPos Pragma

Defined in Cryptol.Parser.AST

Methods

noPos :: Pragma -> Pragma

type Rep Pragma

Defined in Cryptol.Parser.AST

type Rep Pragma = D1 (MetaData "Pragma" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Export information for a declaration.

Constructors

Public

Private

Instances

Eq ExportType

Defined in Cryptol.Parser.AST

Methods

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

(/=) :: ExportType -> ExportType -> Bool

Ord ExportType

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

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> ExportType -> ShowS

show :: ExportType -> String

showList :: [ExportType] -> ShowS

Generic ExportType

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

Defined in Cryptol.Parser.AST

Methods

rnf :: ExportType -> ()

type Rep ExportType

Defined in Cryptol.Parser.AST

type Rep ExportType = D1 (MetaData "ExportType" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (C1 (MetaCons "Public" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Private" PrefixI False) (U1 :: Type -> Type))

data TopLevel a

A top-level module declaration.

Constructors

TopLevel

Fields

• tlExport :: ExportType
• tlDoc :: Maybe (Located String)
• tlValue :: a

Instances

Functor TopLevel

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> TopLevel a -> TopLevel b

(<$) :: a -> TopLevel b -> TopLevel a

Foldable TopLevel

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

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)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> TopLevel a -> ShowS

show :: TopLevel a -> String

showList :: [TopLevel a] -> ShowS

Generic (TopLevel a)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: TopLevel a -> ()

PP a => PP (TopLevel a)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> TopLevel a -> Doc

HasLoc a => HasLoc (TopLevel a)

Defined in Cryptol.Parser.AST

Methods

getLoc :: TopLevel a -> Maybe Range

NoPos a => NoPos (TopLevel a)

Defined in Cryptol.Parser.AST

Methods

noPos :: TopLevel a -> TopLevel a

type Rep (TopLevel a)

Defined in Cryptol.Parser.AST

type Rep (TopLevel a) = D1 (MetaData "TopLevel" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

An import declaration.

Constructors

Import

Fields

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

Instances

Eq Import

Defined in Cryptol.Parser.AST

Methods

(==) :: Import -> Import -> Bool

(/=) :: Import -> Import -> Bool

Show Import

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Import -> ShowS

show :: Import -> String

showList :: [Import] -> ShowS

Generic Import

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

Defined in Cryptol.Parser.AST

Methods

rnf :: Import -> ()

PP Import

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Import -> Doc

type Rep Import

Defined in Cryptol.Parser.AST

type Rep Import = D1 (MetaData "Import" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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

Defined in Cryptol.Parser.AST

Methods

(==) :: ImportSpec -> ImportSpec -> Bool

(/=) :: ImportSpec -> ImportSpec -> Bool

Show ImportSpec

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> ImportSpec -> ShowS

show :: ImportSpec -> String

showList :: [ImportSpec] -> ShowS

Generic ImportSpec

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

Defined in Cryptol.Parser.AST

Methods

rnf :: ImportSpec -> ()

PP ImportSpec

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ImportSpec -> Doc

type Rep ImportSpec

Defined in Cryptol.Parser.AST

type Rep ImportSpec = D1 (MetaData "ImportSpec" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

Newtype

Fields

• nName :: Located name

  Type name

• nParams :: [TParam name]

  Type params

• nBody :: [Named (Type name)]

  Constructor

Instances

Rename Newtype

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Newtype PName -> RenameM (Newtype Name)

Eq name => Eq (Newtype name)

Defined in Cryptol.Parser.AST

Methods

(==) :: Newtype name -> Newtype name -> Bool

(/=) :: Newtype name -> Newtype name -> Bool

Show name => Show (Newtype name)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Newtype name -> ShowS

show :: Newtype name -> String

showList :: [Newtype name] -> ShowS

Generic (Newtype name)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: Newtype name -> ()

PPName name => PP (Newtype name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Newtype name -> Doc

HasLoc (Newtype name)

Defined in Cryptol.Parser.AST

Methods

getLoc :: Newtype name -> Maybe Range

NoPos (Newtype name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Newtype name -> Newtype name

BindsNames (InModule (Newtype PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (Newtype PName) -> BuildNamingEnv

type Rep (Newtype name)

Defined in Cryptol.Parser.AST

type Rep (Newtype name) = D1 (MetaData "Newtype" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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 ParameterType name

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

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: ParameterType PName -> RenameM (ParameterType Name)

Eq name => Eq (ParameterType name)

Defined in Cryptol.Parser.AST

Methods

(==) :: ParameterType name -> ParameterType name -> Bool

(/=) :: ParameterType name -> ParameterType name -> Bool

Show name => Show (ParameterType name)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> ParameterType name -> ShowS

show :: ParameterType name -> String

showList :: [ParameterType name] -> ShowS

Generic (ParameterType name)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: ParameterType name -> ()

(Show name, PPName name) => PP (ParameterType name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ParameterType name -> Doc

HasLoc (ParameterType name)

Defined in Cryptol.Parser.AST

Methods

getLoc :: ParameterType name -> Maybe Range

NoPos (ParameterType name)

Defined in Cryptol.Parser.AST

Methods

noPos :: ParameterType name -> ParameterType name

BindsNames (InModule (ParameterType PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (ParameterType PName) -> BuildNamingEnv

type Rep (ParameterType name)

Defined in Cryptol.Parser.AST

type Rep (ParameterType name) = D1 (MetaData "ParameterType" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: ParameterFun PName -> RenameM (ParameterFun Name)

Eq name => Eq (ParameterFun name)

Defined in Cryptol.Parser.AST

Methods

(==) :: ParameterFun name -> ParameterFun name -> Bool

(/=) :: ParameterFun name -> ParameterFun name -> Bool

Show name => Show (ParameterFun name)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> ParameterFun name -> ShowS

show :: ParameterFun name -> String

showList :: [ParameterFun name] -> ShowS

Generic (ParameterFun name)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: ParameterFun name -> ()

(Show name, PPName name) => PP (ParameterFun name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ParameterFun name -> Doc

HasLoc (ParameterFun name)

Defined in Cryptol.Parser.AST

Methods

getLoc :: ParameterFun name -> Maybe Range

NoPos (ParameterFun x)

Defined in Cryptol.Parser.AST

Methods

noPos :: ParameterFun x -> ParameterFun x

BindsNames (InModule (ParameterFun PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (ParameterFun PName) -> BuildNamingEnv

type Rep (ParameterFun name)

Defined in Cryptol.Parser.AST

type Rep (ParameterFun name) = D1 (MetaData "ParameterFun" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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)

Defined in Cryptol.Parser.AST

Methods

(==) :: ReplInput name -> ReplInput name -> Bool

(/=) :: ReplInput name -> ReplInput name -> Bool

Show name => Show (ReplInput name)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> ReplInput name -> ShowS

show :: ReplInput name -> String

showList :: [ReplInput name] -> ShowS

Expressions

data Expr n

Constructors

EVar n

 x

ELit Literal

 0x10

ENeg (Expr n)

 -1

EComplement (Expr n)

 ~1

ETuple [Expr n]

 (1,2,3)

ERecord [Named (Expr n)]

 { x = 1, y = 2 }

ESel (Expr n) Selector

 e.l

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

 { r | x = e }

EList [Expr n]

 [1,2,3]

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

[1, 5 ..  117 ]

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

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> Expr a -> Expr b

(<$) :: a -> Expr b -> Expr a

Rename Expr

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Expr PName -> RenameM (Expr Name)

Eq n => Eq (Expr n)

Defined in Cryptol.Parser.AST

Methods

(==) :: Expr n -> Expr n -> Bool

(/=) :: Expr n -> Expr n -> Bool

Show n => Show (Expr n)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Expr n -> ShowS

show :: Expr n -> String

showList :: [Expr n] -> ShowS

Generic (Expr n)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: Expr n -> ()

(Show name, PPName name) => PP (Expr name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Expr name -> Doc

AddLoc (Expr n)

Defined in Cryptol.Parser.AST

Methods

addLoc :: Expr n -> Range -> Expr n

dropLoc :: Expr n -> Expr n

HasLoc (Expr name)

Defined in Cryptol.Parser.AST

Methods

getLoc :: Expr name -> Maybe Range

NoPos (Expr name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Expr name -> Expr name

RemovePatterns (Expr PName)

Defined in Cryptol.Parser.NoPat

Methods

removePatterns :: Expr PName -> (Expr PName, [Error])

type Rep (Expr n)

Defined in Cryptol.Parser.AST

type Rep (Expr n) = D1 (MetaData "Expr" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) ((((C1 (MetaCons "EVar" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 n)) :+: C1 (MetaCons "ELit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Literal))) :+: (C1 (MetaCons "ENeg" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n))) :+: (C1 (MetaCons "EComplement" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n))) :+: C1 (MetaCons "ETuple" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Expr n]))))) :+: ((C1 (MetaCons "ERecord" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Named (Expr n)])) :+: (C1 (MetaCons "ESel" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Selector)) :+: C1 (MetaCons "EUpd" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Expr n))) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [UpdField n])))) :+: (C1 (MetaCons "EList" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Expr n])) :+: (C1 (MetaCons "EFromTo" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Type n))) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n)))) :+: C1 (MetaCons "EInfFrom" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe (Expr n)))))))) :+: (((C1 (MetaCons "EComp" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [[Match n]])) :+: (C1 (MetaCons "EApp" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n))) :+: C1 (MetaCons "EAppT" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TypeInst n])))) :+: (C1 (MetaCons "EIf" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n)) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n)))) :+: (C1 (MetaCons "EWhere" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Decl n])) :+: C1 (MetaCons "ETyped" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n)))))) :+: ((C1 (MetaCons "ETypeVal" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n))) :+: (C1 (MetaCons "EFun" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Pattern n]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n))) :+: C1 (MetaCons "ELocated" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Range)))) :+: (C1 (MetaCons "ESplit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n))) :+: (C1 (MetaCons "EParens" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n))) :+: C1 (MetaCons "EInfix" PrefixI False) ((S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Located n))) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Fixity) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Expr n)))))))))

data Literal

Literals.

Constructors

ECNum Integer NumInfo

0x10 (HexLit 2)

ECString String

"hello"

Instances

Eq Literal

Defined in Cryptol.Parser.AST

Methods

(==) :: Literal -> Literal -> Bool

(/=) :: Literal -> Literal -> Bool

Show Literal

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Literal -> ShowS

show :: Literal -> String

showList :: [Literal] -> ShowS

Generic Literal

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

Defined in Cryptol.Parser.AST

Methods

rnf :: Literal -> ()

PP Literal

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Literal -> Doc

type Rep Literal

Defined in Cryptol.Parser.AST

type Rep Literal = D1 (MetaData "Literal" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (C1 (MetaCons "ECNum" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NumInfo)) :+: C1 (MetaCons "ECString" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))

data NumInfo

Infromation about the representation of a numeric constant.

Constructors

BinLit Int

n-digit binary literal

OctLit Int

n-digit octal literal

DecLit

overloaded decimal literal

HexLit Int

n-digit hex literal

CharLit

character literal

PolyLit Int

polynomial literal

Instances

Eq NumInfo

Defined in Cryptol.Parser.AST

Methods

(==) :: NumInfo -> NumInfo -> Bool

(/=) :: NumInfo -> NumInfo -> Bool

Show NumInfo

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> NumInfo -> ShowS

show :: NumInfo -> String

showList :: [NumInfo] -> ShowS

Generic NumInfo

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

Defined in Cryptol.Parser.AST

Methods

rnf :: NumInfo -> ()

type Rep NumInfo

Defined in Cryptol.Parser.AST

type Rep NumInfo = D1 (MetaData "NumInfo" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) ((C1 (MetaCons "BinLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) :+: (C1 (MetaCons "OctLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) :+: C1 (MetaCons "DecLit" PrefixI False) (U1 :: Type -> Type))) :+: (C1 (MetaCons "HexLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) :+: (C1 (MetaCons "CharLit" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "PolyLit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)))))

data Match name

Constructors

Match (Pattern name) (Expr name)

p <- e

MatchLet (Bind name)

Instances

Functor Match

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> Match a -> Match b

(<$) :: a -> Match b -> Match a

Rename Match

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Match PName -> RenameM (Match Name)

Eq name => Eq (Match name)

Defined in Cryptol.Parser.AST

Methods

(==) :: Match name -> Match name -> Bool

(/=) :: Match name -> Match name -> Bool

Show name => Show (Match name)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Match name -> ShowS

show :: Match name -> String

showList :: [Match name] -> ShowS

Generic (Match name)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: Match name -> ()

(Show name, PPName name) => PP (Match name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Match name -> Doc

HasLoc (Match name)

Defined in Cryptol.Parser.AST

Methods

getLoc :: Match name -> Maybe Range

NoPos (Match name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Match name -> Match name

type Rep (Match name)

Defined in Cryptol.Parser.AST

type Rep (Match name) = D1 (MetaData "Match" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

PVar (Located n)

 x

PWild

 _

PTuple [Pattern n]

 (x,y,z)

PRecord [Named (Pattern n)]

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

PList [Pattern n]

 [ x, y, z ]

PTyped (Pattern n) (Type n)

 x : [8]

PSplit (Pattern n) (Pattern n)

 (x # y)

PLocated (Pattern n) Range

Location information

Instances

Functor Pattern

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> Pattern a -> Pattern b

(<$) :: a -> Pattern b -> Pattern a

Rename Pattern

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Pattern PName -> RenameM (Pattern Name)

Eq n => Eq (Pattern n)

Defined in Cryptol.Parser.AST

Methods

(==) :: Pattern n -> Pattern n -> Bool

(/=) :: Pattern n -> Pattern n -> Bool

Show n => Show (Pattern n)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Pattern n -> ShowS

show :: Pattern n -> String

showList :: [Pattern n] -> ShowS

Generic (Pattern n)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: Pattern n -> ()

PPName name => PP (Pattern name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Pattern name -> Doc

AddLoc (Pattern name)

Defined in Cryptol.Parser.AST

Methods

addLoc :: Pattern name -> Range -> Pattern name

dropLoc :: Pattern name -> Pattern name

HasLoc (Pattern name)

Defined in Cryptol.Parser.AST

Methods

getLoc :: Pattern name -> Maybe Range

NoPos (Pattern name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Pattern name -> Pattern name

type Rep (Pattern n)

Defined in Cryptol.Parser.AST

type Rep (Pattern n) = D1 (MetaData "Pattern" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (((C1 (MetaCons "PVar" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Located n))) :+: C1 (MetaCons "PWild" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "PTuple" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Pattern n])) :+: C1 (MetaCons "PRecord" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Named (Pattern n)])))) :+: ((C1 (MetaCons "PList" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Pattern n])) :+: C1 (MetaCons "PTyped" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type n)))) :+: (C1 (MetaCons "PSplit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern n))) :+: C1 (MetaCons "PLocated" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Pattern n)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Range)))))

data Selector

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

Defined in Cryptol.Parser.Selector

Methods

(==) :: Selector -> Selector -> Bool

(/=) :: Selector -> Selector -> Bool

Ord Selector

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

Defined in Cryptol.Parser.Selector

Methods

showsPrec :: Int -> Selector -> ShowS

show :: Selector -> String

showList :: [Selector] -> ShowS

Generic Selector

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

Defined in Cryptol.Parser.Selector

Methods

rnf :: Selector -> ()

PP Selector

Defined in Cryptol.Parser.Selector

Methods

ppPrec :: Int -> Selector -> Doc

ShowParseable Selector

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Selector -> Doc

type Rep Selector

Defined in Cryptol.Parser.Selector

type Rep Selector = D1 (MetaData "Selector" "Cryptol.Parser.Selector" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

NamedInst (Named (Type name))

PosInst (Type name)

Instances

Functor TypeInst

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> TypeInst a -> TypeInst b

(<$) :: a -> TypeInst b -> TypeInst a

Rename TypeInst

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: TypeInst PName -> RenameM (TypeInst Name)

Eq name => Eq (TypeInst name)

Defined in Cryptol.Parser.AST

Methods

(==) :: TypeInst name -> TypeInst name -> Bool

(/=) :: TypeInst name -> TypeInst name -> Bool

Show name => Show (TypeInst name)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> TypeInst name -> ShowS

show :: TypeInst name -> String

showList :: [TypeInst name] -> ShowS

Generic (TypeInst name)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: TypeInst name -> ()

PPName name => PP (TypeInst name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> TypeInst name -> Doc

NoPos (TypeInst name)

Defined in Cryptol.Parser.AST

Methods

noPos :: TypeInst name -> TypeInst name

type Rep (TypeInst name)

Defined in Cryptol.Parser.AST

type Rep (TypeInst name) = D1 (MetaData "TypeInst" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

UpdField UpdHow [Located Selector] (Expr n)

non-empty list x.y = e

Instances

Functor UpdField

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> UpdField a -> UpdField b

(<$) :: a -> UpdField b -> UpdField a

Rename UpdField

Note that after this point the -> updates have an explicit funciton and there are no more nested updates.

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: UpdField PName -> RenameM (UpdField Name)

Eq n => Eq (UpdField n)

Defined in Cryptol.Parser.AST

Methods

(==) :: UpdField n -> UpdField n -> Bool

(/=) :: UpdField n -> UpdField n -> Bool

Show n => Show (UpdField n)

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> UpdField n -> ShowS

show :: UpdField n -> String

showList :: [UpdField n] -> ShowS

Generic (UpdField n)

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)

Defined in Cryptol.Parser.AST

Methods

rnf :: UpdField n -> ()

(Show name, PPName name) => PP (UpdField name)

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> UpdField name -> Doc

NoPos (UpdField name)

Defined in Cryptol.Parser.AST

Methods

noPos :: UpdField name -> UpdField name

type Rep (UpdField n)

Defined in Cryptol.Parser.AST

type Rep (UpdField n) = D1 (MetaData "UpdField" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

UpdSet

UpdFun

Are we setting or updating a field.

Instances

Eq UpdHow

Defined in Cryptol.Parser.AST

Methods

(==) :: UpdHow -> UpdHow -> Bool

(/=) :: UpdHow -> UpdHow -> Bool

Show UpdHow

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> UpdHow -> ShowS

show :: UpdHow -> String

showList :: [UpdHow] -> ShowS

Generic UpdHow

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

Defined in Cryptol.Parser.AST

Methods

rnf :: UpdHow -> ()

PP UpdHow

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> UpdHow -> Doc

type Rep UpdHow

Defined in Cryptol.Parser.AST

type Rep UpdHow = D1 (MetaData "UpdHow" "Cryptol.Parser.AST" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (C1 (MetaCons "UpdSet" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "UpdFun" PrefixI False) (U1 :: Type -> Type))

Positions

data Located a

Constructors

Located

Fields

• srcRange :: !Range
• thing :: !a

Instances

Functor Located

Defined in Cryptol.Parser.Position

Methods

fmap :: (a -> b) -> Located a -> Located b

(<$) :: a -> Located b -> Located a

Eq a => Eq (Located a)

Defined in Cryptol.Parser.Position

Methods

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

(/=) :: Located a -> Located a -> Bool

Show a => Show (Located a)

Defined in Cryptol.Parser.Position

Methods

showsPrec :: Int -> Located a -> ShowS

show :: Located a -> String

showList :: [Located a] -> ShowS

Generic (Located a)

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)

Defined in Cryptol.Parser.Position

Methods

rnf :: Located a -> ()

PPName a => PPName (Located a)

Defined in Cryptol.Parser.Position

Methods

ppNameFixity :: Located a -> Maybe (Assoc, Int)

ppPrefixName :: Located a -> Doc

ppInfixName :: Located a -> Doc

PP a => PP (Located a)

Defined in Cryptol.Parser.Position

Methods

ppPrec :: Int -> Located a -> Doc

AddLoc (Located a)

Defined in Cryptol.Parser.Position

Methods

addLoc :: Located a -> Range -> Located a

dropLoc :: Located a -> Located a

HasLoc (Located a)

Defined in Cryptol.Parser.Position

Methods

getLoc :: Located a -> Maybe Range

NoPos (Located t)

Defined in Cryptol.Parser.AST

Methods

noPos :: Located t -> Located t

ShowParseable a => ShowParseable (Located a)

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Located a -> Doc

type Rep (Located a)

Defined in Cryptol.Parser.Position

type Rep (Located a) = D1 (MetaData "Located" "Cryptol.Parser.Position" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

A name with location information.

type LString = Located String

A string with location information.

type LIdent = Located Ident

An identifier with location information.

class NoPos t where

Methods

noPos :: t -> t

Instances

NoPos Pragma

Defined in Cryptol.Parser.AST

Methods

noPos :: Pragma -> Pragma

NoPos t => NoPos [t]

Defined in Cryptol.Parser.AST

Methods

noPos :: [t] -> [t]

NoPos t => NoPos (Maybe t)

Defined in Cryptol.Parser.AST

Methods

noPos :: Maybe t -> Maybe t

NoPos (Located t)

Defined in Cryptol.Parser.AST

Methods

noPos :: Located t -> Located t

NoPos (Prop name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Prop name -> Prop name

NoPos (Type name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Type name -> Type name

NoPos (TParam name)

Defined in Cryptol.Parser.AST

Methods

noPos :: TParam name -> TParam name

NoPos (Schema name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Schema name -> Schema name

NoPos t => NoPos (Named t)

Defined in Cryptol.Parser.AST

Methods

noPos :: Named t -> Named t

NoPos (Pattern name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Pattern name -> Pattern name

NoPos (Match name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Match name -> Match name

NoPos (TypeInst name)

Defined in Cryptol.Parser.AST

Methods

noPos :: TypeInst name -> TypeInst name

NoPos (UpdField name)

Defined in Cryptol.Parser.AST

Methods

noPos :: UpdField name -> UpdField name

NoPos (Expr name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Expr name -> Expr name

NoPos a => NoPos (TopLevel a)

Defined in Cryptol.Parser.AST

Methods

noPos :: TopLevel a -> TopLevel a

NoPos (Newtype name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Newtype name -> Newtype name

NoPos (Bind name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Bind name -> Bind name

NoPos (PropSyn name)

Defined in Cryptol.Parser.AST

Methods

noPos :: PropSyn name -> PropSyn name

NoPos (TySyn name)

Defined in Cryptol.Parser.AST

Methods

noPos :: TySyn name -> TySyn name

NoPos (ParameterFun x)

Defined in Cryptol.Parser.AST

Methods

noPos :: ParameterFun x -> ParameterFun x

NoPos (ParameterType name)

Defined in Cryptol.Parser.AST

Methods

noPos :: ParameterType name -> ParameterType name

NoPos (Decl name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Decl name -> Decl name

NoPos (TopDecl name)

Defined in Cryptol.Parser.AST

Methods

noPos :: TopDecl name -> TopDecl name

NoPos (Module name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Module name -> Module name

NoPos (Program name)

Defined in Cryptol.Parser.AST

Methods

noPos :: Program name -> Program name

Pretty-printing

cppKind :: Kind -> Doc

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

ppSelector :: Selector -> Doc

Display the thing selected by the selector, nicely.