cryptol-3.1.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 #

The type of identifiers. * The boolean flag indicates whether or not they're infix operators. The boolean is present just as cached information from the lexer, and never used during comparisons. * The MaybeAnon indicates if this is an anonymous name

Instances

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

Show Ident Source # 
Instance details

Defined in Cryptol.Utils.Ident

Methods

showsPrec :: Int -> Ident -> ShowS #

show :: Ident -> String #

showList :: [Ident] -> ShowS #

ShowParseable Ident Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

PP Ident Source # 
Instance details

Defined in Cryptol.Utils.PP

Methods

ppPrec :: Int -> Ident -> Doc Source #

NFData Ident Source # 
Instance details

Defined in Cryptol.Utils.Ident

Methods

rnf :: Ident -> () #

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 #

type Rep Ident Source # 
Instance details

Defined in Cryptol.Utils.Ident

type Rep Ident

mkIdent :: Text -> Ident Source #

Make a normal (i.e., not anonymous) identifier

data ModName Source #

Top-level Module names are just text.

Instances

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

Show ModName Source # 
Instance details

Defined in Cryptol.Utils.Ident

PP ModName Source # 
Instance details

Defined in Cryptol.Utils.PP

Methods

ppPrec :: Int -> ModName -> Doc Source #

PPName ModName Source # 
Instance details

Defined in Cryptol.Utils.PP

NFData ModName Source # 
Instance details

Defined in Cryptol.Utils.Ident

Methods

rnf :: ModName -> () #

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

type Rep ModName Source # 
Instance details

Defined in Cryptol.Utils.Ident

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

Show PName Source # 
Instance details

Defined in Cryptol.Parser.Name

Methods

showsPrec :: Int -> PName -> ShowS #

show :: PName -> String #

showList :: [PName] -> ShowS #

PP PName Source # 
Instance details

Defined in Cryptol.Parser.Name

Methods

ppPrec :: Int -> PName -> Doc Source #

PPName PName Source # 
Instance details

Defined in Cryptol.Parser.Name

NFData PName Source # 
Instance details

Defined in Cryptol.Parser.Name

Methods

rnf :: PName -> () #

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 #

BindsNames (InModule (Bind PName)) Source #

Introduce the name

Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (Bind PName) -> BuildNamingEnv

BindsNames (InModule (Decl PName)) Source #

The naming environment for a single declaration.

Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (Decl PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (EnumDecl PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (NestedModule PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (Newtype PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (ParameterFun PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (ParameterType PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (PrimType PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (SigDecl PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (TopDecl PName) -> BuildNamingEnv

BindsNames (Pattern PName) Source # 
Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: Pattern PName -> BuildNamingEnv

BindsNames (Schema PName) Source #

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

Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: Schema PName -> BuildNamingEnv

BindsNames (TParam PName) Source #

Generate the naming environment for a type parameter.

Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: TParam PName -> BuildNamingEnv

RemovePatterns (Expr PName) Source # 
Instance details

Defined in Cryptol.Parser.NoPat

RemovePatterns (NestedModule PName) Source # 
Instance details

Defined in Cryptol.Parser.NoPat

RemovePatterns (Program PName) Source # 
Instance details

Defined in Cryptol.Parser.NoPat

RemovePatterns [Decl PName] Source # 
Instance details

Defined in Cryptol.Parser.NoPat

RemovePatterns (ModuleG mname PName) Source # 
Instance details

Defined in Cryptol.Parser.NoPat

Methods

removePatterns :: ModuleG mname PName -> (ModuleG mname PName, [Error]) Source #

type Rep PName Source # 
Instance details

Defined in Cryptol.Parser.Name

data Named a Source #

Constructors

Named 

Fields

Instances

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

Functor Named Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

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 #

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 #

NoPos t => NoPos (Named t) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Named t -> Named t Source #

HasLoc a => HasLoc (Named a) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

getLoc :: Named a -> Maybe Range Source #

NFData a => NFData (Named a) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

type Rep (Named a) Source # 
Instance details

Defined in Cryptol.Parser.AST

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

Instances

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

Show Pass Source # 
Instance details

Defined in Cryptol.Parser.Name

Methods

showsPrec :: Int -> Pass -> ShowS #

show :: Pass -> String #

showList :: [Pass] -> ShowS #

NFData Pass Source # 
Instance details

Defined in Cryptol.Parser.Name

Methods

rnf :: Pass -> () #

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 #

type Rep Pass Source # 
Instance details

Defined in Cryptol.Parser.Name

type Rep Pass = D1 ('MetaData "Pass" "Cryptol.Parser.Name" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "NoPat" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MonoValues" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExpandPropGuards" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))

data Assoc Source #

Information about associativity.

Constructors

LeftAssoc 
RightAssoc 
NonAssoc 

Instances

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

Show Assoc Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Methods

showsPrec :: Int -> Assoc -> ShowS #

show :: Assoc -> String #

showList :: [Assoc] -> ShowS #

PP Assoc Source # 
Instance details

Defined in Cryptol.Utils.PP

Methods

ppPrec :: Int -> Assoc -> Doc Source #

NFData Assoc Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Methods

rnf :: Assoc -> () #

Eq Assoc Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Methods

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

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

Ord Assoc Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Methods

compare :: Assoc -> Assoc -> Ordering #

(<) :: Assoc -> Assoc -> Bool #

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

(>) :: Assoc -> Assoc -> Bool #

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

max :: Assoc -> Assoc -> Assoc #

min :: Assoc -> Assoc -> Assoc #

type Rep Assoc Source # 
Instance details

Defined in Cryptol.Utils.Fixity

type Rep Assoc = D1 ('MetaData "Assoc" "Cryptol.Utils.Fixity" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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

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 #

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 #

BindsNames (Schema PName) Source #

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

Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: Schema PName -> BuildNamingEnv

NoPos (Schema name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Schema name -> Schema name 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 #

PPName name => PP (Schema name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Schema name -> Doc Source #

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

Defined in Cryptol.Parser.AST

Methods

rnf :: Schema n -> () #

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

Defined in Cryptol.Parser.AST

Methods

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

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

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

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 #

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 #

BindsNames (TParam PName) Source #

Generate the naming environment for a type parameter.

Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: TParam PName -> BuildNamingEnv

NoPos (TParam name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: TParam name -> TParam name 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 #

PPName name => PP (TParam name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> TParam name -> Doc Source #

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

Defined in Cryptol.Parser.AST

Methods

rnf :: TParam n -> () #

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

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep (TParam n) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (TParam n) = D1 ('MetaData "TParam" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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
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 #

Show Kind Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> Kind -> ShowS #

show :: Kind -> String #

showList :: [Kind] -> ShowS #

PP Kind Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Kind -> Doc Source #

NFData Kind Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: Kind -> () #

Eq Kind Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep Kind Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep Kind = D1 ('MetaData "Kind" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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) (Maybe Kind)
 (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

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 #

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 #

NoPos (Type name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Type name -> Type name 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 #

PPName name => PP (Type name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Type name -> Doc Source #

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

Defined in Cryptol.Parser.AST

Methods

rnf :: Type n -> () #

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

Defined in Cryptol.Parser.AST

Methods

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

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

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

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 #

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 #

NoPos (Prop name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Prop name -> Prop name Source #

PPName name => PP (Prop name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Prop name -> Doc Source #

PPName name => PP [Prop name] Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> [Prop name] -> Doc Source #

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

Defined in Cryptol.Parser.AST

Methods

rnf :: Prop n -> () #

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

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep (Prop n) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (Prop n) = D1 ('MetaData "Prop" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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

type Module = ModuleG ModName Source #

A top-level module

data ModuleG mname name Source #

A module for the pre-typechecker phasese. The two parameters are:

  • mname the type of module names. This is because top-level and nested modules use differnt types to identify a module.
  • name the type of identifiers used by declarations. In the parser this starts off as PName and after resolving names in the renamer, this becomes Name.

Constructors

Module 

Fields

  • mName :: Located mname

    Name of the module

  • mDef :: ModuleDefinition name
     
  • mInScope :: NamingEnv

    Names in scope inside this module, filled in by the renamer. Also, for the FunctorInstance case this is not the final result of the names in scope. The typechecker adds in the names in scope in the functor, so this will just contain the names in the enclosing scope.

Instances

Instances details
Generic (ModuleG mname name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (ModuleG mname name) :: Type -> Type #

Methods

from :: ModuleG mname name -> Rep (ModuleG mname name) x #

to :: Rep (ModuleG mname name) x -> ModuleG mname name #

(Show mname, Show name) => Show (ModuleG mname name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> ModuleG mname name -> ShowS #

show :: ModuleG mname name -> String #

showList :: [ModuleG mname name] -> ShowS #

NoPos (ModuleG mname name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: ModuleG mname name -> ModuleG mname name Source #

RemovePatterns (ModuleG mname PName) Source # 
Instance details

Defined in Cryptol.Parser.NoPat

Methods

removePatterns :: ModuleG mname PName -> (ModuleG mname PName, [Error]) Source #

HasLoc (ModuleG mname name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

getLoc :: ModuleG mname name -> Maybe Range Source #

(Show name, PPName mname, PPName name) => PP (ModuleG mname name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ModuleG mname name -> Doc Source #

(NFData mname, NFData name) => NFData (ModuleG mname name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ModuleG mname name -> () #

type Rep (ModuleG mname name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (ModuleG mname name) = D1 ('MetaData "ModuleG" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "Module" 'PrefixI 'True) (S1 ('MetaSel ('Just "mName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located mname)) :*: (S1 ('MetaSel ('Just "mDef") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ModuleDefinition name)) :*: S1 ('MetaSel ('Just "mInScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NamingEnv))))

mDecls :: ModuleG mname name -> [TopDecl name] Source #

mImports :: ModuleG mname name -> [Located Import] Source #

Imports of top-level (i.e. "file" based) modules.

mModParams :: ModuleG mname name -> [ModParam name] Source #

Get the module parameters of a module (new module system)

mIsFunctor :: ModuleG mname nmae -> Bool Source #

data ModuleDefinition name Source #

Different flavours of module we have.

Constructors

NormalModule [TopDecl name] 
FunctorInstance (Located (ImpName name)) (ModuleInstanceArgs name) (ModuleInstance name)

The instance is filled in by the renamer

InterfaceModule (Signature name) 

Instances

Instances details
Generic (ModuleDefinition name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (ModuleDefinition name) :: Type -> Type #

Methods

from :: ModuleDefinition name -> Rep (ModuleDefinition name) x #

to :: Rep (ModuleDefinition name) x -> ModuleDefinition name #

Show name => Show (ModuleDefinition name) Source # 
Instance details

Defined in Cryptol.Parser.AST

NoPos (ModuleDefinition name) Source # 
Instance details

Defined in Cryptol.Parser.AST

(Show name, PPName name) => PP (ModuleDefinition name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ModuleDefinition name -> Doc Source #

NFData name => NFData (ModuleDefinition name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ModuleDefinition name -> () #

type Rep (ModuleDefinition name) Source # 
Instance details

Defined in Cryptol.Parser.AST

data ModuleInstanceArgs name Source #

All arguments in a functor instantiation

Constructors

DefaultInstArg (Located (ModuleInstanceArg name))

Single parameter instantitaion

DefaultInstAnonArg [TopDecl name]

Single parameter instantitaion using this anonymous module. (parser only)

NamedInstArgs [ModuleInstanceNamedArg name] 

Instances

Instances details
Rename ModuleInstanceArgs Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Generic (ModuleInstanceArgs name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (ModuleInstanceArgs name) :: Type -> Type #

Show name => Show (ModuleInstanceArgs name) Source # 
Instance details

Defined in Cryptol.Parser.AST

NoPos (ModuleInstanceArgs name) Source # 
Instance details

Defined in Cryptol.Parser.AST

(Show name, PPName name) => PP (ModuleInstanceArgs name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ModuleInstanceArgs name -> Doc Source #

NFData name => NFData (ModuleInstanceArgs name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ModuleInstanceArgs name -> () #

type Rep (ModuleInstanceArgs name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (ModuleInstanceArgs name) = D1 ('MetaData "ModuleInstanceArgs" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "DefaultInstArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located (ModuleInstanceArg name)))) :+: (C1 ('MetaCons "DefaultInstAnonArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TopDecl name])) :+: C1 ('MetaCons "NamedInstArgs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ModuleInstanceNamedArg name]))))

data ModuleInstanceNamedArg name Source #

A named argument in a functor instantiation

Instances

Instances details
Rename ModuleInstanceNamedArg Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Generic (ModuleInstanceNamedArg name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (ModuleInstanceNamedArg name) :: Type -> Type #

Show name => Show (ModuleInstanceNamedArg name) Source # 
Instance details

Defined in Cryptol.Parser.AST

NoPos (ModuleInstanceNamedArg name) Source # 
Instance details

Defined in Cryptol.Parser.AST

(Show name, PPName name) => PP (ModuleInstanceNamedArg name) Source # 
Instance details

Defined in Cryptol.Parser.AST

NFData name => NFData (ModuleInstanceNamedArg name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ModuleInstanceNamedArg name -> () #

type Rep (ModuleInstanceNamedArg name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (ModuleInstanceNamedArg name) = D1 ('MetaData "ModuleInstanceNamedArg" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "ModuleInstanceNamedArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located Ident)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located (ModuleInstanceArg name)))))

data ModuleInstanceArg name Source #

An argument in a functor instantiation

Constructors

ModuleArg (ImpName name)

An argument that is a module

ParameterArg Ident

An argument that is a parameter

AddParams

Arguments adds extra parameters to decls. ("backtick" import)

Instances

Instances details
Rename ModuleInstanceArg Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Generic (ModuleInstanceArg name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (ModuleInstanceArg name) :: Type -> Type #

Methods

from :: ModuleInstanceArg name -> Rep (ModuleInstanceArg name) x #

to :: Rep (ModuleInstanceArg name) x -> ModuleInstanceArg name #

Show name => Show (ModuleInstanceArg name) Source # 
Instance details

Defined in Cryptol.Parser.AST

(Show name, PPName name) => PP (ModuleInstanceArg name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ModuleInstanceArg name -> Doc Source #

NFData name => NFData (ModuleInstanceArg name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ModuleInstanceArg name -> () #

type Rep (ModuleInstanceArg name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (ModuleInstanceArg name) = D1 ('MetaData "ModuleInstanceArg" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "ModuleArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ImpName name))) :+: (C1 ('MetaCons "ParameterArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident)) :+: C1 ('MetaCons "AddParams" 'PrefixI 'False) (U1 :: Type -> Type)))

type ModuleInstance name = Map name name Source #

Maps names in the original functor with names in the instnace. Does *NOT* include the parameters, just names for the definitions. This *DOES* include entrirs for all the name in the instantiated functor, including names in modules nested inside the functor.

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 #

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

(Show name, PPName name) => PP (Program name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Program name -> Doc Source #

data TopDecl name Source #

A declaration that may only appear at the top level of a module. The module may be nested, however.

Constructors

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

@newtype T as = t

TDEnum (TopLevel (EnumDecl name))
enum T as = cons
Include (Located FilePath)

include File (until NoInclude)

DParamDecl Range (Signature name)

parameter ... (parser only)

DModule (TopLevel (NestedModule name))
submodule M where ...
DImport (Located (ImportG (ImpName name)))
import X
DModParam (ModParam name)
import interface X ...
DInterfaceConstraint (Maybe Text) (Located [Prop name])
interface constraint

Instances

Instances details
Rename TopDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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 #

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 #

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (TopDecl PName) -> BuildNamingEnv

NoPos (TopDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: TopDecl name -> TopDecl name Source #

HasLoc (TopDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

getLoc :: TopDecl name -> Maybe Range Source #

(Show name, PPName name) => PP (TopDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> TopDecl name -> Doc Source #

NFData name => NFData (TopDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: TopDecl name -> () #

type Rep (TopDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (TopDecl name) = D1 ('MetaData "TopDecl" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (((C1 ('MetaCons "Decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevel (Decl name)))) :+: C1 ('MetaCons "DPrimType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevel (PrimType name))))) :+: (C1 ('MetaCons "TDNewtype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevel (Newtype name)))) :+: (C1 ('MetaCons "TDEnum" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevel (EnumDecl name)))) :+: C1 ('MetaCons "Include" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located FilePath)))))) :+: ((C1 ('MetaCons "DParamDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Signature name))) :+: C1 ('MetaCons "DModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevel (NestedModule name))))) :+: (C1 ('MetaCons "DImport" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located (ImportG (ImpName name))))) :+: (C1 ('MetaCons "DModParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ModParam name))) :+: C1 ('MetaCons "DInterfaceConstraint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located [Prop name])))))))

data Decl name Source #

A simple declaration. Generally these are things that can appear both at the top-level of a module and in `where` clauses.

Constructors

DSignature [Located name] (Schema name)

A type signature. Eliminated in NoPat--after NoPat signatures are in their associated Bind

DFixity !Fixity [Located name]

A fixity declaration. Eliminated in NoPat---after NoPat fixities are in their associated Bind

DPragma [Located name] Pragma

A pragma declaration. Eliminated in NoPat---after NoPat fixities are in their associated Bind

DBind (Bind name)

A non-recursive binding.

DRec [Bind name]

A group of recursive bindings. Introduced by the renamer.

DPatBind (Pattern name) (Expr name)

A pattern binding. Eliminated in NoPat---after NoPat fixities are in their associated Bind

DType (TySyn name)

A type synonym.

DProp (PropSyn name)

A constraint synonym.

DLocated (Decl name) Range

Keeps track of the location of a declaration.

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

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 #

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 #

BindsNames (InModule (Decl PName)) Source #

The naming environment for a single declaration.

Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (Decl PName) -> BuildNamingEnv

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

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 #

(Show name, PPName name) => PP (Decl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Decl name -> Doc Source #

NFData name => NFData (Decl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: Decl name -> () #

Eq name => Eq (Decl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep (Decl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (Decl name) = D1 ('MetaData "Decl" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 "DRec" '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
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 #

Show Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

PP Fixity Source # 
Instance details

Defined in Cryptol.Utils.PP

Methods

ppPrec :: Int -> Fixity -> Doc Source #

NFData Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Methods

rnf :: Fixity -> () #

Eq Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Methods

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

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

Ord Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

type Rep Fixity Source # 
Instance details

Defined in Cryptol.Utils.Fixity

type Rep Fixity = D1 ('MetaData "Fixity" "Cryptol.Utils.Fixity" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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
Show FixityCmp Source # 
Instance details

Defined in Cryptol.Utils.Fixity

Eq 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

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 #

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 #

NoPos (TySyn name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: TySyn name -> TySyn name Source #

HasLoc (TySyn name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

getLoc :: TySyn name -> Maybe Range Source #

PPName name => PP (TySyn name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> TySyn name -> Doc Source #

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

Defined in Cryptol.Parser.AST

Methods

rnf :: TySyn n -> () #

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

Defined in Cryptol.Parser.AST

Methods

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

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

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

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 #

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 #

NoPos (PropSyn name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: PropSyn name -> PropSyn name Source #

HasLoc (PropSyn name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

getLoc :: PropSyn name -> Maybe Range Source #

PPName name => PP (PropSyn name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> PropSyn name -> Doc Source #

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

Defined in Cryptol.Parser.AST

Methods

rnf :: PropSyn n -> () #

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

Defined in Cryptol.Parser.AST

Methods

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

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

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

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 #

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 #

BindsNames (InModule (Bind PName)) Source #

Introduce the name

Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (Bind PName) -> BuildNamingEnv

NoPos (Bind name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Bind name -> Bind name Source #

HasLoc (Bind name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

getLoc :: Bind name -> Maybe Range Source #

(Show name, PPName name) => PP (Bind name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Bind name -> Doc Source #

NFData name => NFData (Bind name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: Bind name -> () #

Eq name => Eq (Bind name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep (Bind name) Source # 
Instance details

Defined in Cryptol.Parser.AST

data BindDef name Source #

Constructors

DPrim 
DForeign (Maybe (BindImpl name))

Foreign functions can have an optional cryptol implementation

DImpl (BindImpl 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

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 #

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 #

(Show name, PPName name) => PP (BindDef name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> BindDef name -> Doc Source #

NFData name => NFData (BindDef name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: BindDef name -> () #

Eq name => Eq (BindDef name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep (BindDef name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (BindDef name) = D1 ('MetaData "BindDef" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "DPrim" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DForeign" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (BindImpl name)))) :+: C1 ('MetaCons "DImpl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (BindImpl name)))))

data BindImpl name Source #

Constructors

DExpr (Expr name) 
DPropGuards [PropGuardCase name] 

Instances

Instances details
Functor BindImpl Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

Rename BindImpl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Generic (BindImpl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (BindImpl name) :: Type -> Type #

Methods

from :: BindImpl name -> Rep (BindImpl name) x #

to :: Rep (BindImpl name) x -> BindImpl name #

Show name => Show (BindImpl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

show :: BindImpl name -> String #

showList :: [BindImpl name] -> ShowS #

(Show name, PPName name) => PP (BindImpl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> BindImpl name -> Doc Source #

NFData name => NFData (BindImpl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: BindImpl name -> () #

Eq name => Eq (BindImpl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

(==) :: BindImpl name -> BindImpl name -> Bool #

(/=) :: BindImpl name -> BindImpl name -> Bool #

type Rep (BindImpl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (BindImpl name) = D1 ('MetaData "BindImpl" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "DExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr name))) :+: C1 ('MetaCons "DPropGuards" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [PropGuardCase name])))

bindImpl :: Bind name -> Maybe (BindImpl name) Source #

exprDef :: Expr name -> BindDef name Source #

data Pragma Source #

Instances

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

Show Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

NoPos Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Pragma -> Pragma Source #

PP Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Pragma -> Doc Source #

NFData Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: Pragma -> () #

Eq Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep Pragma = D1 ('MetaData "Pragma" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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
Generic ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep ExportType :: Type -> Type #

Show ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

NFData ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ExportType -> () #

Eq ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

Ord ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep ExportType Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep ExportType = D1 ('MetaData "ExportType" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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
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) #

Functor TopLevel Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

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 #

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 #

NoPos a => NoPos (TopLevel a) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: TopLevel a -> TopLevel a Source #

HasLoc a => HasLoc (TopLevel a) Source # 
Instance details

Defined in Cryptol.Parser.AST

PP a => PP (TopLevel a) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> TopLevel a -> Doc Source #

NFData a => NFData (TopLevel a) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: TopLevel a -> () #

type Rep (TopLevel a) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (TopLevel a) = D1 ('MetaData "TopLevel" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 ImportG mname Source #

An import declaration.

Constructors

Import 

Fields

Instances

Instances details
Generic (ImportG mname) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (ImportG mname) :: Type -> Type #

Methods

from :: ImportG mname -> Rep (ImportG mname) x #

to :: Rep (ImportG mname) x -> ImportG mname #

Show mname => Show (ImportG mname) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

showsPrec :: Int -> ImportG mname -> ShowS #

show :: ImportG mname -> String #

showList :: [ImportG mname] -> ShowS #

PP mname => PP (ImportG mname) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ImportG mname -> Doc Source #

NFData mname => NFData (ImportG mname) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ImportG mname -> () #

type Rep (ImportG mname) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (ImportG mname) = D1 ('MetaData "ImportG" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "Import" 'PrefixI 'True) ((S1 ('MetaSel ('Just "iModule") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 mname) :*: S1 ('MetaSel ('Just "iAs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModName))) :*: (S1 ('MetaSel ('Just "iSpec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ImportSpec)) :*: S1 ('MetaSel ('Just "iInst") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe (ModuleInstanceArgs PName))))))

data ImportSpec Source #

The list of names following an import.

Constructors

Hiding [Ident] 
Only [Ident] 

Instances

Instances details
Generic ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep ImportSpec :: Type -> Type #

Show ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

PP ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ImportSpec -> Doc Source #

NFData ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ImportSpec -> () #

Eq ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep ImportSpec Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep ImportSpec = D1 ('MetaData "ImportSpec" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 ImpName name Source #

The name of an imported module

Constructors

ImpTop ModName

A top-level module

ImpNested name

The module in scope with the given name

Instances

Instances details
Rename ImpName Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Generic (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (ImpName name) :: Type -> Type #

Methods

from :: ImpName name -> Rep (ImpName name) x #

to :: Rep (ImpName name) x -> ImpName name #

Show name => Show (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

show :: ImpName name -> String #

showList :: [ImpName name] -> ShowS #

ModuleInstance name => ModuleInstance (ImpName name) Source # 
Instance details

Defined in Cryptol.TypeCheck.ModuleInstance

Methods

moduleInstance :: ImpName name -> ImpName name Source #

PP name => PP (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ImpName name -> Doc Source #

NFData name => NFData (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ImpName name -> () #

Eq name => Eq (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

(==) :: ImpName name -> ImpName name -> Bool #

(/=) :: ImpName name -> ImpName name -> Bool #

Ord name => Ord (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

compare :: ImpName name -> ImpName name -> Ordering #

(<) :: ImpName name -> ImpName name -> Bool #

(<=) :: ImpName name -> ImpName name -> Bool #

(>) :: ImpName name -> ImpName name -> Bool #

(>=) :: ImpName name -> ImpName name -> Bool #

max :: ImpName name -> ImpName name -> ImpName name #

min :: ImpName name -> ImpName name -> ImpName name #

type Rep (ImpName name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (ImpName name) = D1 ('MetaData "ImpName" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "ImpTop" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModName)) :+: C1 ('MetaCons "ImpNested" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 name)))

data Newtype name Source #

Constructors

Newtype 

Fields

Instances

Instances details
Rename Newtype Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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 #

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 #

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (Newtype PName) -> BuildNamingEnv

NoPos (Newtype name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Newtype name -> Newtype name Source #

HasLoc (Newtype name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

getLoc :: Newtype name -> Maybe Range Source #

PPName name => PP (Newtype name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Newtype name -> Doc Source #

NFData name => NFData (Newtype name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: Newtype name -> () #

Eq name => Eq (Newtype name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep (Newtype name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (Newtype name)

data EnumDecl name Source #

Constructors

EnumDecl 

Fields

Instances

Instances details
Rename EnumDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Generic (EnumDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (EnumDecl name) :: Type -> Type #

Methods

from :: EnumDecl name -> Rep (EnumDecl name) x #

to :: Rep (EnumDecl name) x -> EnumDecl name #

Show name => Show (EnumDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

show :: EnumDecl name -> String #

showList :: [EnumDecl name] -> ShowS #

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (EnumDecl PName) -> BuildNamingEnv

NoPos (EnumDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: EnumDecl name -> EnumDecl name Source #

HasLoc (EnumDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

getLoc :: EnumDecl name -> Maybe Range Source #

(Show name, PPName name) => PP (EnumDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> EnumDecl name -> Doc Source #

NFData name => NFData (EnumDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: EnumDecl name -> () #

type Rep (EnumDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (EnumDecl name) = D1 ('MetaData "EnumDecl" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "EnumDecl" 'PrefixI 'True) (S1 ('MetaSel ('Just "eName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located name)) :*: (S1 ('MetaSel ('Just "eParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam name]) :*: S1 ('MetaSel ('Just "eCons") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TopLevel (EnumCon name)]))))

data EnumCon name Source #

Constructors

EnumCon 

Fields

Instances

Instances details
Generic (EnumCon name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (EnumCon name) :: Type -> Type #

Methods

from :: EnumCon name -> Rep (EnumCon name) x #

to :: Rep (EnumCon name) x -> EnumCon name #

Show name => Show (EnumCon name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

show :: EnumCon name -> String #

showList :: [EnumCon name] -> ShowS #

NoPos (EnumCon name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: EnumCon name -> EnumCon name Source #

HasLoc (EnumCon name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

getLoc :: EnumCon name -> Maybe Range Source #

(Show name, PPName name) => PP (EnumCon name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> EnumCon name -> Doc Source #

NFData name => NFData (EnumCon name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: EnumCon name -> () #

type Rep (EnumCon name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (EnumCon name) = D1 ('MetaData "EnumCon" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "EnumCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "ecName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located name)) :*: S1 ('MetaSel ('Just "ecFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type 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

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 #

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 #

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (PrimType PName) -> BuildNamingEnv

NoPos (PrimType name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: PrimType name -> PrimType name Source #

HasLoc (PrimType name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

getLoc :: PrimType name -> Maybe Range Source #

(Show name, PPName name) => PP (PrimType name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> PrimType name -> Doc Source #

NFData name => NFData (PrimType name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: PrimType name -> () #

type Rep (PrimType name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (PrimType name) = D1 ('MetaData "PrimType" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 for a module.

Constructors

ParameterType 

Fields

Instances

Instances details
Rename ParameterType Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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 #

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 #

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (ParameterType PName) -> BuildNamingEnv

NoPos (ParameterType name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: ParameterType name -> ParameterType name Source #

HasLoc (ParameterType name) Source # 
Instance details

Defined in Cryptol.Parser.AST

(Show name, PPName name) => PP (ParameterType name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ParameterType name -> Doc Source #

NFData name => NFData (ParameterType name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ParameterType name -> () #

Eq name => Eq (ParameterType name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep (ParameterType name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (ParameterType name) = D1 ('MetaData "ParameterType" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 for a module.

Constructors

ParameterFun 

Fields

Instances

Instances details
Rename ParameterFun Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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 #

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 #

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (ParameterFun PName) -> BuildNamingEnv

NoPos (ParameterFun x) Source # 
Instance details

Defined in Cryptol.Parser.AST

HasLoc (ParameterFun name) Source # 
Instance details

Defined in Cryptol.Parser.AST

(Show name, PPName name) => PP (ParameterFun name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ParameterFun name -> Doc Source #

NFData name => NFData (ParameterFun name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ParameterFun name -> () #

Eq name => Eq (ParameterFun name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep (ParameterFun name) Source # 
Instance details

Defined in Cryptol.Parser.AST

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

newtype NestedModule name Source #

A nested module.

Constructors

NestedModule (ModuleG name name) 

Instances

Instances details
Rename NestedModule Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Generic (NestedModule name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (NestedModule name) :: Type -> Type #

Methods

from :: NestedModule name -> Rep (NestedModule name) x #

to :: Rep (NestedModule name) x -> NestedModule name #

Show name => Show (NestedModule name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

show :: NestedModule name -> String #

showList :: [NestedModule name] -> ShowS #

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (NestedModule PName) -> BuildNamingEnv

NoPos (NestedModule name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: NestedModule name -> NestedModule name Source #

RemovePatterns (NestedModule PName) Source # 
Instance details

Defined in Cryptol.Parser.NoPat

HasLoc (NestedModule name) Source # 
Instance details

Defined in Cryptol.Parser.AST

(Show name, PPName name) => PP (NestedModule name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> NestedModule name -> Doc Source #

NFData name => NFData (NestedModule name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: NestedModule name -> () #

type Rep (NestedModule name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (NestedModule name) = D1 ('MetaData "NestedModule" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'True) (C1 ('MetaCons "NestedModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ModuleG name name))))

data Signature name Source #

Interface Modules (aka types of functor arguments)

IMPORTANT: Interface Modules are a language construct and are different from the notion of "interface" in the Cryptol implementation.

Note that the names *defined* in an interface module are only really used in the other members of the interface module. When an interface module is "imported" as a functor parameter these names are instantiated to new names, because there could be multiple paramers using the same interface.

Constructors

Signature 

Fields

Instances

Instances details
Generic (Signature name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (Signature name) :: Type -> Type #

Methods

from :: Signature name -> Rep (Signature name) x #

to :: Rep (Signature name) x -> Signature name #

Show name => Show (Signature name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

show :: Signature name -> String #

showList :: [Signature name] -> ShowS #

NoPos (Signature name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Signature name -> Signature name Source #

NFData name => NFData (Signature name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: Signature name -> () #

type Rep (Signature name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (Signature name) = D1 ('MetaData "Signature" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "Signature" 'PrefixI 'True) ((S1 ('MetaSel ('Just "sigImports") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Located (ImportG (ImpName name))]) :*: S1 ('MetaSel ('Just "sigTypeParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ParameterType name])) :*: (S1 ('MetaSel ('Just "sigConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located (Prop name)]) :*: (S1 ('MetaSel ('Just "sigDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SigDecl name]) :*: S1 ('MetaSel ('Just "sigFunParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ParameterFun name])))))

data SigDecl name Source #

A constraint or type synonym declared in an interface.

Constructors

SigTySyn (TySyn name) (Maybe Text) 
SigPropSyn (PropSyn name) (Maybe Text) 

Instances

Instances details
Rename SigDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Generic (SigDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (SigDecl name) :: Type -> Type #

Methods

from :: SigDecl name -> Rep (SigDecl name) x #

to :: Rep (SigDecl name) x -> SigDecl name #

Show name => Show (SigDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

show :: SigDecl name -> String #

showList :: [SigDecl name] -> ShowS #

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (SigDecl PName) -> BuildNamingEnv

NoPos (SigDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: SigDecl name -> SigDecl name Source #

HasLoc (SigDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

getLoc :: SigDecl name -> Maybe Range Source #

(Show name, PPName name) => PP (SigDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> SigDecl name -> Doc Source #

NFData name => NFData (SigDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: SigDecl name -> () #

type Rep (SigDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

data ModParam name Source #

A module parameter declaration.

import interface A
import interface A as B

The name of the parameter is derived from the as clause. If there is no as clause then it is derived from the name of the interface module.

If there is no as clause, then the type/value parameters are unqualified, and otherwise they are qualified.

Constructors

ModParam 

Fields

  • mpSignature :: Located (ImpName name)

    Signature for parameter

  • mpAs :: Maybe ModName

    Qualified for actual params

  • mpName :: !Ident

    Parameter name (for inst.) Note that this is not resolved in the renamer, and is only used when instantiating a functor.

  • mpDoc :: Maybe (Located Text)

    Optional documentation

  • mpRenaming :: !(Map name name)

    Filled in by the renamer. Maps the actual (value/type) parameter names to the names in the interface module.

Instances

Instances details
Rename ModParam Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Generic (ModParam name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (ModParam name) :: Type -> Type #

Methods

from :: ModParam name -> Rep (ModParam name) x #

to :: Rep (ModParam name) x -> ModParam name #

Show name => Show (ModParam name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

show :: ModParam name -> String #

showList :: [ModParam name] -> ShowS #

NoPos (ModParam name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: ModParam name -> ModParam name Source #

HasLoc (ModParam name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

getLoc :: ModParam name -> Maybe Range Source #

(Show name, PPName name) => PP (ModParam name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ModParam name -> Doc Source #

NFData name => NFData (ModParam name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ModParam name -> () #

Eq name => Eq (ModParam name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

(==) :: ModParam name -> ModParam name -> Bool #

(/=) :: ModParam name -> ModParam name -> Bool #

type Rep (ModParam name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (ModParam name) = D1 ('MetaData "ModParam" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "ModParam" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mpSignature") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located (ImpName name))) :*: S1 ('MetaSel ('Just "mpAs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModName))) :*: (S1 ('MetaSel ('Just "mpName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Ident) :*: (S1 ('MetaSel ('Just "mpDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Located Text))) :*: S1 ('MetaSel ('Just "mpRenaming") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map name name))))))

data ParamDecl name Source #

Things that maybe appear in an interface/parameter block. These only exist during parsering.

Constructors

DParameterType (ParameterType name)

parameter type T : # (parser only)

DParameterFun (ParameterFun name)

parameter someVal : [256] (parser only)

DParameterDecl (SigDecl name)

A delcaration in an interface

DParameterConstraint [Located (Prop name)]
parameter type constraint (fin T)

Instances

Instances details
Generic (ParamDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (ParamDecl name) :: Type -> Type #

Methods

from :: ParamDecl name -> Rep (ParamDecl name) x #

to :: Rep (ParamDecl name) x -> ParamDecl name #

Show name => Show (ParamDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

show :: ParamDecl name -> String #

showList :: [ParamDecl name] -> ShowS #

NoPos (ParamDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: ParamDecl name -> ParamDecl name Source #

HasLoc (ParamDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

getLoc :: ParamDecl name -> Maybe Range Source #

(Show name, PPName name) => PP (ParamDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> ParamDecl name -> Doc Source #

NFData name => NFData (ParamDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: ParamDecl name -> () #

type Rep (ParamDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (ParamDecl name) = D1 ('MetaData "ParamDecl" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) ((C1 ('MetaCons "DParameterType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ParameterType name))) :+: C1 ('MetaCons "DParameterFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ParameterFun name)))) :+: (C1 ('MetaCons "DParameterDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SigDecl name))) :+: C1 ('MetaCons "DParameterConstraint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located (Prop name)]))))

data PropGuardCase name Source #

Constructors

PropGuardCase 

Fields

Instances

Instances details
Functor PropGuardCase Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

Rename PropGuardCase Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Generic (PropGuardCase name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep (PropGuardCase name) :: Type -> Type #

Methods

from :: PropGuardCase name -> Rep (PropGuardCase name) x #

to :: Rep (PropGuardCase name) x -> PropGuardCase name #

Show name => Show (PropGuardCase name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

show :: PropGuardCase name -> String #

showList :: [PropGuardCase name] -> ShowS #

NFData name => NFData (PropGuardCase name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: PropGuardCase name -> () #

Eq name => Eq (PropGuardCase name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

(==) :: PropGuardCase name -> PropGuardCase name -> Bool #

(/=) :: PropGuardCase name -> PropGuardCase name -> Bool #

type Rep (PropGuardCase name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (PropGuardCase name) = D1 ('MetaData "PropGuardCase" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "PropGuardCase" 'PrefixI 'True) (S1 ('MetaSel ('Just "pgcProps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located (Prop name)]) :*: S1 ('MetaSel ('Just "pgcExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr name))))

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

Eq name => Eq (ReplInput name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

Expressions

data Expr n Source #

Constructors

EVar n
 x
ELit Literal
 0x10
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]
EFromToBy Bool (Type n) (Type n) (Type n) (Maybe (Type n))
 [1 .. 10 by 2 : t ]
EFromToDownBy Bool (Type n) (Type n) (Type n) (Maybe (Type n))
 [10 .. 1 down by 2 : t ]
EFromToLessThan (Type n) (Type n) (Maybe (Type n))
 [ 1 .. < 10 : t ]
EInfFrom 

Fields

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
ECase (Expr n) [CaseAlt n]
 case e of { P -> e }
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 

Fields

EPrefix PrefixOp (Expr n)
 -1, ~1

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

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 #

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 #

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

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 #

(Show name, PPName name) => PP (Expr name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Expr name -> Doc Source #

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

Defined in Cryptol.Parser.AST

Methods

rnf :: Expr n -> () #

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

Defined in Cryptol.Parser.AST

Methods

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

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

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

Show Literal Source # 
Instance details

Defined in Cryptol.Parser.AST

PP Literal Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Literal -> Doc Source #

NFData Literal Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: Literal -> () #

Eq Literal Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

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

Show NumInfo Source # 
Instance details

Defined in Cryptol.Parser.AST

NFData NumInfo Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: NumInfo -> () #

Eq NumInfo Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep NumInfo Source # 
Instance details

Defined in Cryptol.Parser.AST

data FracInfo Source #

Information about fractional literals.

Instances

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

Show FracInfo Source # 
Instance details

Defined in Cryptol.Parser.AST

NFData FracInfo Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: FracInfo -> () #

Eq FracInfo Source # 
Instance details

Defined in Cryptol.Parser.AST

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

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 #

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 #

NoPos (Match name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Match name -> Match name Source #

HasLoc (Match name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

getLoc :: Match name -> Maybe Range Source #

(Show name, PPName name) => PP (Match name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Match name -> Doc Source #

NFData name => NFData (Match name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: Match name -> () #

Eq name => Eq (Match name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep (Match name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (Match name) = D1 ('MetaData "Match" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 

Fields

PCon (Located n) [Pattern n]
 Just x
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

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 #

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 #

BindsNames (Pattern PName) Source # 
Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: Pattern PName -> BuildNamingEnv

NoPos (Pattern name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Pattern name -> Pattern name 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 #

PPName name => PP (Pattern name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> Pattern name -> Doc Source #

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

Defined in Cryptol.Parser.AST

Methods

rnf :: Pattern n -> () #

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

Defined in Cryptol.Parser.AST

Methods

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

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

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

Show Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

ShowParseable Selector Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

PP Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

Methods

ppPrec :: Int -> Selector -> Doc Source #

NFData Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

Methods

rnf :: Selector -> () #

Eq Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

Ord Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

type Rep Selector Source # 
Instance details

Defined in Cryptol.Parser.Selector

data CaseAlt n Source #

Constructors

CaseAlt (Pattern n) (Expr n) 

Instances

Instances details
Functor CaseAlt Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

Rename CaseAlt Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Generic (CaseAlt n) Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

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

Methods

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

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

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

Defined in Cryptol.Parser.AST

Methods

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

show :: CaseAlt n -> String #

showList :: [CaseAlt n] -> ShowS #

NoPos (CaseAlt name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: CaseAlt name -> CaseAlt name Source #

(Show name, PPName name) => PP (CaseAlt name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> CaseAlt name -> Doc Source #

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

Defined in Cryptol.Parser.AST

Methods

rnf :: CaseAlt n -> () #

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

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep (CaseAlt n) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (CaseAlt n) = D1 ('MetaData "CaseAlt" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "CaseAlt" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Expr n))))

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

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 #

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 #

NoPos (TypeInst name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: TypeInst name -> TypeInst name Source #

PPName name => PP (TypeInst name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> TypeInst name -> Doc Source #

NFData name => NFData (TypeInst name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: TypeInst name -> () #

Eq name => Eq (TypeInst name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep (TypeInst name) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (TypeInst name) = D1 ('MetaData "TypeInst" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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

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 #

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 #

NoPos (UpdField name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: UpdField name -> UpdField name Source #

(Show name, PPName name) => PP (UpdField name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> UpdField name -> Doc Source #

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

Defined in Cryptol.Parser.AST

Methods

rnf :: UpdField n -> () #

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

Defined in Cryptol.Parser.AST

Methods

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

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

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

Show UpdHow Source # 
Instance details

Defined in Cryptol.Parser.AST

PP UpdHow Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

ppPrec :: Int -> UpdHow -> Doc Source #

NFData UpdHow Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: UpdHow -> () #

Eq UpdHow Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep UpdHow Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep UpdHow = D1 ('MetaData "UpdHow" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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

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 #

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 #

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

Defined in Cryptol.Parser.AST

Methods

rnf :: FunDesc n -> () #

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

Defined in Cryptol.Parser.AST

Methods

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

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

type Rep (FunDesc n) Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep (FunDesc n) = D1 ('MetaData "FunDesc" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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)))

data PrefixOp Source #

Prefix operator.

Instances

Instances details
Generic PrefixOp Source # 
Instance details

Defined in Cryptol.Parser.AST

Associated Types

type Rep PrefixOp :: Type -> Type #

Methods

from :: PrefixOp -> Rep PrefixOp x #

to :: Rep PrefixOp x -> PrefixOp #

Show PrefixOp Source # 
Instance details

Defined in Cryptol.Parser.AST

NFData PrefixOp Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

rnf :: PrefixOp -> () #

Eq PrefixOp Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep PrefixOp Source # 
Instance details

Defined in Cryptol.Parser.AST

type Rep PrefixOp = D1 ('MetaData "PrefixOp" "Cryptol.Parser.AST" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "PrefixNeg" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrefixComplement" 'PrefixI 'False) (U1 :: Type -> Type))

asEApps :: Expr n -> (Expr n, [Expr n]) Source #

Positions

data Located a Source #

Constructors

Located 

Fields

Instances

Instances details
Foldable Located Source # 
Instance details

Defined in Cryptol.Parser.Position

Methods

fold :: Monoid m => Located m -> m #

foldMap :: Monoid m => (a -> m) -> Located a -> m #

foldMap' :: Monoid m => (a -> m) -> Located a -> m #

foldr :: (a -> b -> b) -> b -> Located a -> b #

foldr' :: (a -> b -> b) -> b -> Located a -> b #

foldl :: (b -> a -> b) -> b -> Located a -> b #

foldl' :: (b -> a -> b) -> b -> Located a -> b #

foldr1 :: (a -> a -> a) -> Located a -> a #

foldl1 :: (a -> a -> a) -> Located a -> a #

toList :: Located a -> [a] #

null :: Located a -> Bool #

length :: Located a -> Int #

elem :: Eq a => a -> Located a -> Bool #

maximum :: Ord a => Located a -> a #

minimum :: Ord a => Located a -> a #

sum :: Num a => Located a -> a #

product :: Num a => Located a -> a #

Traversable Located Source # 
Instance details

Defined in Cryptol.Parser.Position

Methods

traverse :: Applicative f => (a -> f b) -> Located a -> f (Located b) #

sequenceA :: Applicative f => Located (f a) -> f (Located a) #

mapM :: Monad m => (a -> m b) -> Located a -> m (Located b) #

sequence :: Monad m => Located (m a) -> m (Located a) #

Functor Located Source # 
Instance details

Defined in Cryptol.Parser.Position

Methods

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

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

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 #

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 #

TraverseNames a => TraverseNames (Located a) Source # 
Instance details

Defined in Cryptol.IR.TraverseNames

Methods

traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => Located a -> f (Located a) Source #

NoPos (Located t) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Located t -> Located t 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 #

ModuleInstance a => ModuleInstance (Located a) Source # 
Instance details

Defined in Cryptol.TypeCheck.ModuleInstance

ShowParseable a => ShowParseable (Located a) Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

PP a => PP (Located a) Source # 
Instance details

Defined in Cryptol.Parser.Position

Methods

ppPrec :: Int -> Located a -> Doc Source #

PPName a => PPName (Located a) Source # 
Instance details

Defined in Cryptol.Parser.Position

NFData a => NFData (Located a) Source # 
Instance details

Defined in Cryptol.Parser.Position

Methods

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

type Rep (Located a) Source # 
Instance details

Defined in Cryptol.Parser.Position

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

type LPName = Located PName Source #

A name with location information.

type LString = Located String Source #

A string with location information.

type LIdent = Located Ident Source #

An identifier with location information.

class NoPos t where Source #

Methods

noPos :: t -> t Source #

Instances

Instances details
NoPos Pragma Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Pragma -> Pragma Source #

NoPos Range Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Range -> Range Source #

NoPos (Bind name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Bind name -> Bind name Source #

NoPos (CaseAlt name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: CaseAlt name -> CaseAlt name Source #

NoPos (Decl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Decl name -> Decl name Source #

NoPos (EnumCon name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: EnumCon name -> EnumCon name Source #

NoPos (EnumDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: EnumDecl name -> EnumDecl name Source #

NoPos (Expr name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Expr name -> Expr name Source #

NoPos (Match name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Match name -> Match name Source #

NoPos (ModParam name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: ModParam name -> ModParam name Source #

NoPos (ModuleDefinition name) Source # 
Instance details

Defined in Cryptol.Parser.AST

NoPos (ModuleInstanceArgs name) Source # 
Instance details

Defined in Cryptol.Parser.AST

NoPos (ModuleInstanceNamedArg name) Source # 
Instance details

Defined in Cryptol.Parser.AST

NoPos t => NoPos (Named t) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Named t -> Named t Source #

NoPos (NestedModule name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: NestedModule name -> NestedModule name Source #

NoPos (Newtype name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Newtype name -> Newtype name Source #

NoPos (ParamDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: ParamDecl name -> ParamDecl 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 (Pattern name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Pattern name -> Pattern name Source #

NoPos (PrimType name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: PrimType name -> PrimType name Source #

NoPos (Program name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Program name -> Program name Source #

NoPos (Prop name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Prop name -> Prop name Source #

NoPos (PropSyn name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: PropSyn name -> PropSyn name Source #

NoPos (Schema name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Schema name -> Schema name Source #

NoPos (SigDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: SigDecl name -> SigDecl name Source #

NoPos (Signature name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Signature name -> Signature name Source #

NoPos (TParam name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: TParam name -> TParam name Source #

NoPos (TopDecl name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: TopDecl name -> TopDecl name Source #

NoPos a => NoPos (TopLevel a) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: TopLevel a -> TopLevel a Source #

NoPos (TySyn name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: TySyn name -> TySyn name Source #

NoPos (Type name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Type name -> Type 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 (Located t) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Located t -> Located t Source #

NoPos t => NoPos (Maybe t) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: Maybe t -> Maybe t Source #

NoPos t => NoPos [t] Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: [t] -> [t] Source #

NoPos (ModuleG mname name) Source # 
Instance details

Defined in Cryptol.Parser.AST

Methods

noPos :: ModuleG mname name -> ModuleG mname 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.