cryptol-2.11.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.Parser.AST

Description

 
Synopsis

Names

data Ident Source #

Identifiers, along with a flag that indicates whether or not they're infix operators. The boolean is present just as cached information from the lexer, and never used during comparisons.

Instances

Instances details
Eq Ident Source # 
Instance details

Defined in Cryptol.Utils.Ident

Methods

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

(/=) :: 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

type Rep Ident Source # 
Instance details

Defined in Cryptol.Utils.Ident

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

data ModName Source #

Module names are just text.

Instances

Instances details
Eq ModName Source # 
Instance details

Defined in Cryptol.Utils.Ident

Methods

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

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

Ord ModName Source # 
Instance details

Defined in Cryptol.Utils.Ident

Show ModName Source # 
Instance details

Defined in Cryptol.Utils.Ident

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.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "ModName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)))

data PName Source #

Names that originate in the parser.

Constructors

UnQual !Ident

Unqualified names like x, Foo, or +.

Qual !ModName !Ident

Qualified names like Foo::bar or module::!.

NewName !Pass !Int

Fresh names generated by a pass.

Instances

Instances details
Eq PName Source # 
Instance details

Defined in Cryptol.Parser.Name

Methods

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

(/=) :: 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

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

RemovePatterns (Expr PName) Source # 
Instance details

Defined in Cryptol.Parser.NoPat

RemovePatterns (Module PName) Source # 
Instance details

Defined in Cryptol.Parser.NoPat

RemovePatterns (Program PName) Source # 
Instance details

Defined in Cryptol.Parser.NoPat

BindsNames (TParam PName) Source #

Generate the naming environment for a type parameter.

Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

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

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

BindsNames (InModule (PrimType PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (Newtype PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (Bind PName)) Source #

Introduce the name

Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (ParameterFun PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (ParameterType PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (Decl PName)) Source #

The naming environment for a single declaration.

Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (TopDecl PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

type Rep PName Source # 
Instance details

Defined in Cryptol.Parser.Name

data Named a Source #

Constructors

Named 

Fields

Instances

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

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.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "Named" 'PrefixI 'True) (S1 ('MetaSel ('Just "name") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located Ident)) :*: S1 ('MetaSel ('Just "value") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

data Pass Source #

Passes that can generate fresh names.

Constructors

NoPat 
MonoValues 

Instances

Instances details
Eq Pass Source # 
Instance details

Defined in Cryptol.Parser.Name

Methods

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

(/=) :: 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.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "NoPat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MonoValues" 'PrefixI 'False) (U1 :: Type -> Type))

data Assoc Source #

Information about associativity.

Constructors

LeftAssoc 
RightAssoc 
NonAssoc 

Instances

Instances details
Eq Assoc Source # 
Instance details

Defined in Cryptol.Utils.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.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "LeftAssoc" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "RightAssoc" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NonAssoc" 'PrefixI 'False) (U1 :: Type -> Type)))

Types

data Schema n Source #

Constructors

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

Instances

Instances details
Functor Schema Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

(<$) :: 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

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

type Rep (Schema n) Source # 
Instance details

Defined in Cryptol.Parser.AST

data TParam n Source #

Constructors

TParam 

Fields

Instances

Instances details
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

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

type Rep (TParam n) Source # 
Instance details

Defined in Cryptol.Parser.AST

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

data Kind Source #

Constructors

KProp 
KNum 
KType 
KFun Kind Kind 

Instances

Instances details
Eq Kind Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

(/=) :: 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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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

Instances details
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

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

Instances details
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

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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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 #

Declarations

data Module name Source #

A parsed module.

Constructors

Module 

Fields

Instances

Instances details
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

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

type Rep (Module name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (Module name) = D1 ('MetaData "Module" "Cryptol.Parser.AST" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "Module" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located ModName)) :*: S1 ('MetaSel ('Just "mInstance") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe (Located ModName)))) :*: (S1 ('MetaSel ('Just "mImports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located Import]) :*: S1 ('MetaSel ('Just "mDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TopDecl name]))))

newtype Program name Source #

Constructors

Program [TopDecl name] 

Instances

Instances details
Show name => Show (Program name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Program name -> ShowS #

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

data TopDecl name Source #

Constructors

Decl (TopLevel (Decl name)) 
DPrimType (TopLevel (PrimType name)) 
TDNewtype (TopLevel (Newtype name))

@newtype T as = t

Include (Located FilePath)
include File
DParameterType (ParameterType name)
parameter type T : #
DParameterConstraint [Located (Prop name)]
parameter type constraint (fin T)
DParameterFun (ParameterFun name)
parameter someVal : [256]

Instances

Instances details
Rename TopDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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

BindsNames (InModule (TopDecl PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

type Rep (TopDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

data Decl name Source #

Constructors

DSignature [Located name] (Schema name) 
DFixity !Fixity [Located name] 
DPragma [Located name] Pragma 
DBind (Bind name) 
DPatBind (Pattern name) (Expr name) 
DType (TySyn name) 
DProp (PropSyn name) 
DLocated (Decl name) Range 

Instances

Instances details
Functor Decl Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

Rename Decl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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

FromDecl (Decl Name) Source # 
Instance details

Defined in Cryptol.TypeCheck.Depends

BindsNames (InModule (Decl PName)) Source #

The naming environment for a single declaration.

Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

type Rep (Decl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (Decl name) = D1 ('MetaData "Decl" "Cryptol.Parser.AST" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" '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

Instances

Instances details
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

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.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "Fixity" 'PrefixI 'True) (S1 ('MetaSel ('Just "fAssoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Assoc) :*: S1 ('MetaSel ('Just "fLevel") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

defaultFixity :: Fixity Source #

The fixity used when none is provided.

data FixityCmp Source #

Constructors

FCError 
FCLeft 
FCRight 

Instances

Instances details
Eq FixityCmp Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Show FixityCmp Source # 
Instance details

Defined in Cryptol.Utils.Fixity

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

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

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

data TySyn n Source #

Constructors

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

Instances

Instances details
Functor TySyn Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

Rename TySyn Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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

data PropSyn n Source #

Constructors

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

Instances

Instances details
Functor PropSyn Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

Rename PropSyn Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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

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

Instances

Instances details
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

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

type Rep (Bind name) Source # 
Instance details

Defined in Cryptol.Parser.AST

data BindDef name Source #

Constructors

DPrim 
DExpr (Expr name) 

Instances

Instances details
Functor BindDef Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

Rename BindDef Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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))))

data Pragma Source #

Instances

Instances details
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

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.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "PragmaNote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "PragmaProperty" 'PrefixI 'False) (U1 :: Type -> Type))

data ExportType Source #

Export information for a declaration.

Constructors

Public 
Private 

Instances

Instances details
Eq ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Ord ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Show ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Generic ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep ExportType :: Type -> Type #

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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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 

Instances

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

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

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.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "TopLevel" 'PrefixI 'True) (S1 ('MetaSel ('Just "tlExport") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExportType) :*: (S1 ('MetaSel ('Just "tlDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Located Text))) :*: S1 ('MetaSel ('Just "tlValue") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))

data Import Source #

An import declaration.

Constructors

Import 

Instances

Instances details
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

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.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "Import" 'PrefixI 'True) (S1 ('MetaSel ('Just "iModule") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModName) :*: (S1 ('MetaSel ('Just "iAs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModName)) :*: S1 ('MetaSel ('Just "iSpec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ImportSpec)))))

data ImportSpec Source #

The list of names following an import.

INVARIANT: All of the Name entries in the list are expected to be unqualified names; the QName or NewName constructors should not be present.

Constructors

Hiding [Ident] 
Only [Ident] 

Instances

Instances details
Eq ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Show ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Generic ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep ImportSpec :: Type -> Type #

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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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

Instances

Instances details
Rename Newtype Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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

type Rep (Newtype name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (Newtype name)

data PrimType name Source #

A declaration for a type with no implementation.

Constructors

PrimType 

Fields

Instances

Instances details
Rename PrimType Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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

type Rep (PrimType name) Source # 
Instance details

Defined in Cryptol.Parser.AST

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

Instances

Instances details
Rename ParameterType Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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

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

type Rep (ParameterType name) Source # 
Instance details

Defined in Cryptol.Parser.AST

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

data ParameterFun name Source #

A value parameter

Constructors

ParameterFun 

Fields

Instances

Instances details
Rename ParameterFun Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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

NoPos (ParameterFun x) Source # 
Instance details

Defined in Cryptol.Parser.AST

BindsNames (InModule (ParameterFun PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

type Rep (ParameterFun name) Source # 
Instance details

Defined in Cryptol.Parser.AST

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

Interactive

data ReplInput name Source #

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

Constructors

ExprInput (Expr name) 
LetInput (Decl name) 
EmptyInput 

Instances

Instances details
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]
EFromToLessThan (Type n) (Type n) (Maybe (Type n))
 [ 1 .. < 10 : 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 (FunDesc n) [Pattern n] (Expr n)
 \x y -> x
ELocated (Expr n) Range

position annotation

ESplit (Expr n)

splitAt x (Introduced by NoPat)

EParens (Expr n)

(e) (Removed by Fixity)

EInfix (Expr n) (Located n) Fixity (Expr n)

a + b (Removed by Fixity)

Instances

Instances details
Functor Expr Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

Rename Expr Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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

type Rep (Expr n) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (Expr n)

data Literal Source #

Literals.

Constructors

ECNum Integer NumInfo

0x10 (HexLit 2)

ECChar Char
a
ECFrac Rational FracInfo
1.2e3
ECString String
"hello"

Instances

Instances details
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

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

data NumInfo Source #

Infromation about the representation of a numeric constant.

Constructors

BinLit Text Int

n-digit binary literal

OctLit Text Int

n-digit octal literal

DecLit Text

overloaded decimal literal

HexLit Text Int

n-digit hex literal

PolyLit Int

polynomial literal

Instances

Instances details
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

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

data FracInfo Source #

Information about fractional literals.

Instances

Instances details
Eq FracInfo Source # 
Instance details

Defined in Cryptol.Parser.AST

Show FracInfo Source # 
Instance details

Defined in Cryptol.Parser.AST

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

data Match name Source #

Constructors

Match (Pattern name) (Expr name)

p <- e

MatchLet (Bind name) 

Instances

Instances details
Functor Match Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

Rename Match Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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

Instances details
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

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

Instances details
Eq Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

Ord Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

Show Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

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

type Rep Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

data TypeInst name Source #

Constructors

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

Instances

Instances details
Functor TypeInst Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

Rename TypeInst Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "NamedInst" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Named (Type name)))) :+: C1 ('MetaCons "PosInst" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type name))))

data UpdField n Source #

Constructors

UpdField UpdHow [Located Selector] (Expr n)

non-empty list x.y = e

Instances

Instances details
Functor UpdField Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

(<$) :: 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

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

data UpdHow Source #

Constructors

UpdSet 
UpdFun

Are we setting or updating a field.

Instances

Instances details
Eq UpdHow Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

Show UpdHow Source # 
Instance details

Defined in Cryptol.Parser.AST

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.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "UpdSet" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UpdFun" 'PrefixI 'False) (U1 :: Type -> Type))

data FunDesc n Source #

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

Constructors

FunDesc 

Fields

Instances

Instances details
Functor FunDesc Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

fmap :: (a -> b) -> FunDesc a -> FunDesc b #

(<$) :: a -> FunDesc b -> FunDesc a #

Rename FunDesc Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Eq n => Eq (FunDesc n) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

(==) :: FunDesc n -> FunDesc n -> Bool #

(/=) :: FunDesc n -> FunDesc n -> Bool #

Show n => Show (FunDesc n) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> FunDesc n -> ShowS #

show :: FunDesc n -> String #

showList :: [FunDesc n] -> ShowS #

Generic (FunDesc n) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (FunDesc n) :: Type -> Type #

Methods

from :: FunDesc n -> Rep (FunDesc n) x #

to :: Rep (FunDesc n) x -> FunDesc n #

NFData n => NFData (FunDesc n) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: FunDesc n -> () #

type Rep (FunDesc n) Source # 
Instance details

Defined in Cryptol.Parser.AST

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

Positions

data Located a Source #

Constructors

Located 

Fields

Instances

Instances details
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

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

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

type Rep (Located a) Source # 
Instance details

Defined in Cryptol.Parser.Position

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

type LPName = Located PName Source #

A name with location information.

type LString = Located String Source #

A string with location information.

type LIdent = Located Ident Source #

An identifier with location information.

class NoPos t where Source #

Methods

noPos :: t -> t Source #

Instances

Instances details
NoPos 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

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.