Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell2010 |
Synopsis
- data DeclDef
- data Decl = Decl {}
- data DeclGroup
- = Recursive [Decl]
- | NonRecursive Decl
- data Match
- data Expr
- = EList [Expr] Type
- | ETuple [Expr]
- | ERec (RecordMap Ident Expr)
- | ESel Expr Selector
- | ESet Type Expr Selector Expr
- | EIf Expr Expr Expr
- | EComp Type Type Expr [[Match]]
- | EVar Name
- | ETAbs TParam Expr
- | ETApp Expr Type
- | EApp Expr Expr
- | EAbs Name Type Expr
- | ELocated Range Expr
- | EProofAbs Prop Expr
- | EProofApp Expr
- | EWhere Expr [DeclGroup]
- type Module = ModuleG ModName
- data ModuleG mname = Module {
- mName :: !mname
- mExports :: ExportSpec Name
- mImports :: [Import]
- mSubModules :: Map Name (IfaceG Name)
- mParamTypes :: Map Name ModTParam
- mParamConstraints :: [Located Prop]
- mParamFuns :: Map Name ModVParam
- mTySyns :: Map Name TySyn
- mNewtypes :: Map Name Newtype
- mPrimTypes :: Map Name AbstractType
- mDecls :: [DeclGroup]
- mFunctors :: Map Name (ModuleG Name)
- emptyModule :: mname -> ModuleG mname
- isParametrizedModule :: ModuleG mname -> Bool
- groupDecls :: DeclGroup -> [Decl]
- ePrim :: PrimMap -> PrimIdent -> Expr
- eError :: PrimMap -> Type -> String -> Expr
- eString :: PrimMap -> String -> Expr
- eChar :: PrimMap -> Char -> Expr
- ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name, Type)] -> Expr -> Doc
- splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a)
- splitAbs :: Expr -> Maybe ((Name, Type), Expr)
- splitTAbs :: Expr -> Maybe (TParam, Expr)
- splitProofAbs :: Expr -> Maybe (Prop, Expr)
- splitTApp :: Expr -> Maybe (Type, Expr)
- splitProofApp :: Expr -> Maybe ((), Expr)
- splitExprInst :: Expr -> (Expr, [Type], Int)
- data Name
- data TFun
- data Selector
- type Import = ImportG ModName
- data ImportG mname = Import {}
- data ImportSpec
- data ExportType
- newtype ExportSpec name = ExportSpec (Map Namespace (Set name))
- isExportedBind :: Ord name => name -> ExportSpec name -> Bool
- isExportedType :: Ord name => name -> ExportSpec name -> Bool
- isExported :: Ord name => Namespace -> name -> ExportSpec name -> Bool
- data Pragma
- data Fixity = Fixity {}
- data PrimMap = PrimMap {}
- module Cryptol.TypeCheck.Type
Documentation
Instances
Show DeclDef Source # | |
Generic DeclDef Source # | |
NFData DeclDef Source # | |
Defined in Cryptol.TypeCheck.AST | |
TVars DeclDef Source # | |
ShowParseable DeclDef Source # | |
Defined in Cryptol.TypeCheck.Parseable | |
FreeVars DeclDef Source # | |
PP (WithNames DeclDef) Source # | |
type Rep DeclDef Source # | |
Defined in Cryptol.TypeCheck.AST type Rep DeclDef = D1 ('MetaData "DeclDef" "Cryptol.TypeCheck.AST" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "DPrim" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) |
Instances
Recursive [Decl] | Mutually recursive declarations |
NonRecursive Decl | Non-recursive declaration |
Instances
Show DeclGroup Source # | |
Generic DeclGroup Source # | |
NFData DeclGroup Source # | |
Defined in Cryptol.TypeCheck.AST | |
PP DeclGroup Source # | |
TVars DeclGroup Source # | |
ShowParseable DeclGroup Source # | |
Defined in Cryptol.TypeCheck.Parseable | |
Defs DeclGroup Source # | |
FreeVars DeclGroup Source # | |
PP (WithNames DeclGroup) Source # | |
type Rep DeclGroup Source # | |
Defined in Cryptol.TypeCheck.AST type Rep DeclGroup = D1 ('MetaData "DeclGroup" "Cryptol.TypeCheck.AST" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "Recursive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Decl])) :+: C1 ('MetaCons "NonRecursive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Decl))) |
From Name Type Type Expr | Type arguments are the length and element type of the sequence expression |
Let Decl |
Instances
EList [Expr] Type | List value (with type of elements) |
ETuple [Expr] | Tuple value |
ERec (RecordMap Ident Expr) | Record value |
ESel Expr Selector | Elimination for tuplerecordlist |
ESet Type Expr Selector Expr | Change the value of a field. The included type gives the type of the record being updated |
EIf Expr Expr Expr | If-then-else |
EComp Type Type Expr [[Match]] | List comprehensions The types cache the length of the sequence and its element type. |
EVar Name | Use of a bound variable |
ETAbs TParam Expr | Function Value |
ETApp Expr Type | Type application |
EApp Expr Expr | Function application |
EAbs Name Type Expr | Function value |
ELocated Range Expr | Source location information |
EProofAbs Prop Expr | Proof abstraction. Because we don't keep proofs around
we don't need to name the assumption, but we still need to
record the assumption. The assumption is the |
EProofApp Expr | If We don't record the actual proofs, as they are not used for anything. It may be nice to keep them around for sanity checking. |
EWhere Expr [DeclGroup] |
Instances
A Cryptol module.
Module | |
|
Instances
emptyModule :: mname -> ModuleG mname Source #
isParametrizedModule :: ModuleG mname -> Bool Source #
Is this a parameterized module?
groupDecls :: DeclGroup -> [Decl] Source #
ePrim :: PrimMap -> PrimIdent -> Expr Source #
Construct a primitive, given a map to the unique primitive name.
eError :: PrimMap -> Type -> String -> Expr Source #
Make an expression that is error
pre-applied to a type and a message.
splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a) Source #
splitExprInst :: Expr -> (Expr, [Type], Int) Source #
Deconstruct an expression, typically polymorphic, into the types and proofs to which it is applied. Since we don't store the proofs, we just return the number of proof applications. The first type is the one closest to the expr.
Instances
Built-in type functions.
If you add additional user-visible constructors,
please update primTys
in Cryptol.Prims.Types.
TCAdd | : Num -> Num -> Num |
TCSub | : Num -> Num -> Num |
TCMul | : Num -> Num -> Num |
TCDiv | : Num -> Num -> Num |
TCMod | : Num -> Num -> Num |
TCExp | : Num -> Num -> Num |
TCWidth | : Num -> Num |
TCMin | : Num -> Num -> Num |
TCMax | : Num -> Num -> Num |
TCCeilDiv | : Num -> Num -> Num |
TCCeilMod | : Num -> Num -> Num |
TCLenFromThenTo |
|
Instances
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.
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
An import declaration.
Instances
Eq mname => Eq (ImportG mname) Source # | |
Show mname => Show (ImportG mname) Source # | |
Generic (ImportG mname) Source # | |
NFData mname => NFData (ImportG mname) Source # | |
Defined in Cryptol.Parser.AST | |
PP mname => PP (ImportG mname) Source # | |
type Rep (ImportG mname) Source # | |
Defined in Cryptol.Parser.AST type Rep (ImportG mname) = D1 ('MetaData "ImportG" "Cryptol.Parser.AST" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" '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))))) |
data ImportSpec Source #
The list of names following an import.
Instances
data ExportType Source #
Export information for a declaration.
Instances
Eq ExportType Source # | |
Defined in Cryptol.Parser.AST (==) :: ExportType -> ExportType -> Bool # (/=) :: ExportType -> ExportType -> Bool # | |
Ord ExportType Source # | |
Defined in Cryptol.Parser.AST compare :: ExportType -> ExportType -> Ordering # (<) :: ExportType -> ExportType -> Bool # (<=) :: ExportType -> ExportType -> Bool # (>) :: ExportType -> ExportType -> Bool # (>=) :: ExportType -> ExportType -> Bool # max :: ExportType -> ExportType -> ExportType # min :: ExportType -> ExportType -> ExportType # | |
Show ExportType Source # | |
Defined in Cryptol.Parser.AST showsPrec :: Int -> ExportType -> ShowS # show :: ExportType -> String # showList :: [ExportType] -> ShowS # | |
Generic ExportType Source # | |
Defined in Cryptol.Parser.AST type Rep ExportType :: Type -> Type # from :: ExportType -> Rep ExportType x # to :: Rep ExportType x -> ExportType # | |
NFData ExportType Source # | |
Defined in Cryptol.Parser.AST rnf :: ExportType -> () # | |
type Rep ExportType Source # | |
newtype ExportSpec name Source #
ExportSpec (Map Namespace (Set name)) |
Instances
isExportedBind :: Ord name => name -> ExportSpec name -> Bool Source #
Check to see if a binding is exported.
isExportedType :: Ord name => name -> ExportSpec name -> Bool Source #
Check to see if a type synonym is exported.
isExported :: Ord name => Namespace -> name -> ExportSpec name -> Bool Source #
Instances
Eq Pragma Source # | |
Show Pragma Source # | |
Generic Pragma Source # | |
NFData Pragma Source # | |
Defined in Cryptol.Parser.AST | |
PP Pragma Source # | |
NoPos Pragma Source # | |
type Rep Pragma Source # | |
Defined in Cryptol.Parser.AST type Rep Pragma = D1 ('MetaData "Pragma" "Cryptol.Parser.AST" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "PragmaNote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "PragmaProperty" 'PrefixI 'False) (U1 :: Type -> Type)) |
Instances
Eq Fixity Source # | |
Show Fixity Source # | |
Generic Fixity Source # | |
NFData Fixity Source # | |
Defined in Cryptol.Utils.Fixity | |
PP Fixity Source # | |
type Rep Fixity Source # | |
Defined in Cryptol.Utils.Fixity type Rep Fixity = D1 ('MetaData "Fixity" "Cryptol.Utils.Fixity" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "Fixity" 'PrefixI 'True) (S1 ('MetaSel ('Just "fAssoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Assoc) :*: S1 ('MetaSel ('Just "fLevel") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))) |
A mapping from an identifier defined in some module to its real name.
Instances
Show PrimMap Source # | |
Generic PrimMap Source # | |
Semigroup PrimMap Source # | |
NFData PrimMap Source # | |
Defined in Cryptol.ModuleSystem.Name | |
type Rep PrimMap Source # | |
Defined in Cryptol.ModuleSystem.Name type Rep PrimMap = D1 ('MetaData "PrimMap" "Cryptol.ModuleSystem.Name" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "PrimMap" 'PrefixI 'True) (S1 ('MetaSel ('Just "primDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map PrimIdent Name)) :*: S1 ('MetaSel ('Just "primTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map PrimIdent Name)))) |
module Cryptol.TypeCheck.Type