| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe |
| Language | Haskell2010 |
Cryptol.TypeCheck.AST
Description
Synopsis
- data DeclDef
- data Decl = Decl {}
- data DeclGroup
- = Recursive [Decl]
- | NonRecursive Decl
- data Match
- data Expr
- data ModVParam = ModVParam {}
- data ModTParam = ModTParam {}
- data Module = Module {}
- isParametrizedModule :: Module -> Bool
- mtpParam :: ModTParam -> TParam
- groupDecls :: DeclGroup -> [Decl]
- ePrim :: PrimMap -> Ident -> 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
- data Import = Import {}
- data ImportSpec
- data ExportType
- data ExportSpec name = ExportSpec {}
- isExportedBind :: Ord name => name -> ExportSpec name -> Bool
- isExportedType :: Ord name => name -> ExportSpec name -> Bool
- data Pragma
- data Fixity = Fixity {}
- data PrimMap = PrimMap {}
- data TCErrorMessage = TCErrorMessage {
- tcErrorMessage :: !String
- module Cryptol.TypeCheck.Type
Documentation
Instances
| Show DeclDef Source # | |
| Generic DeclDef Source # | |
| NFData DeclDef Source # | |
Defined in Cryptol.TypeCheck.AST | |
| ShowParseable DeclDef Source # | |
Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: DeclDef -> Doc Source # | |
| FreeVars DeclDef Source # | |
| TVars 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.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" False) (C1 (MetaCons "DPrim" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "DExpr" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr))) | |
Constructors
| Decl | |
Instances
Constructors
| 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 # | |
| ShowParseable DeclGroup Source # | |
Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: DeclGroup -> Doc Source # | |
| Defs DeclGroup Source # | |
| FreeVars DeclGroup Source # | |
| TVars 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.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" 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))) | |
Constructors
| From Name Type Type Expr | Type arguments are the length and element type of the sequence expression |
| Let Decl |
Instances
Constructors
| EList [Expr] Type | List value (with type of elements) |
| ETuple [Expr] | Tuple value |
| ERec [(Ident, Expr)] | Record value |
| ESel Expr Selector | Elimination for tuplerecordlist |
| ESet Expr Selector Expr | Change the value of a field. |
| 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 |
| 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 `e : p => t`, then `EProofApp e : t`,
as long as we can prove 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 value parameter of a module.
Constructors
| ModVParam | |
Instances
| Show ModVParam Source # | |
| Generic ModVParam Source # | |
| NFData ModVParam Source # | |
Defined in Cryptol.TypeCheck.AST | |
| type Rep ModVParam Source # | |
Defined in Cryptol.TypeCheck.AST type Rep ModVParam = D1 (MetaData "ModVParam" "Cryptol.TypeCheck.AST" "cryptol-2.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" False) (C1 (MetaCons "ModVParam" PrefixI True) ((S1 (MetaSel (Just "mvpName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Just "mvpType") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Schema)) :*: (S1 (MetaSel (Just "mvpDoc") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe String)) :*: S1 (MetaSel (Just "mvpFixity") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Fixity))))) | |
A type parameter of a module.
Constructors
| ModTParam | |
Instances
| Show ModTParam Source # | |
| Generic ModTParam Source # | |
| NFData ModTParam Source # | |
Defined in Cryptol.TypeCheck.AST | |
| type Rep ModTParam Source # | |
Defined in Cryptol.TypeCheck.AST type Rep ModTParam = D1 (MetaData "ModTParam" "Cryptol.TypeCheck.AST" "cryptol-2.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" False) (C1 (MetaCons "ModTParam" PrefixI True) ((S1 (MetaSel (Just "mtpName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Just "mtpKind") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind)) :*: (S1 (MetaSel (Just "mtpNumber") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int) :*: S1 (MetaSel (Just "mtpDoc") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe String))))) | |
A Cryptol module.
Constructors
| Module | |
Fields
| |
Instances
isParametrizedModule :: Module -> Bool Source #
Is this a parameterized module?
groupDecls :: DeclGroup -> [Decl] Source #
ePrim :: PrimMap -> Ident -> Expr Source #
Construct a primitive, given a map to the unique names of the Cryptol module.
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.
Constructors
| 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.
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
An import declaration.
Instances
| Eq Import Source # | |
| Show Import Source # | |
| Generic Import Source # | |
| NFData Import Source # | |
Defined in Cryptol.Parser.AST | |
| PP Import Source # | |
| type Rep Import Source # | |
Defined in Cryptol.Parser.AST type Rep Import = D1 (MetaData "Import" "Cryptol.Parser.AST" "cryptol-2.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" False) (C1 (MetaCons "Import" PrefixI True) (S1 (MetaSel (Just "iModule") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 ModName) :*: (S1 (MetaSel (Just "iAs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe ModName)) :*: S1 (MetaSel (Just "iSpec") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe ImportSpec))))) | |
data ImportSpec Source #
The list of names following an import.
INVARIANT: All of the Name entries in the list are expected to be
unqualified names; the QName or NewName constructors should not be
present.
Instances
| Eq ImportSpec Source # | |
Defined in Cryptol.Parser.AST | |
| Show ImportSpec Source # | |
Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ImportSpec -> ShowS # show :: ImportSpec -> String # showList :: [ImportSpec] -> ShowS # | |
| Generic ImportSpec Source # | |
Defined in Cryptol.Parser.AST Associated Types type Rep ImportSpec :: Type -> Type # | |
| NFData ImportSpec Source # | |
Defined in Cryptol.Parser.AST Methods rnf :: ImportSpec -> () # | |
| PP ImportSpec Source # | |
Defined in Cryptol.Parser.AST | |
| type Rep ImportSpec Source # | |
Defined in Cryptol.Parser.AST type Rep ImportSpec = D1 (MetaData "ImportSpec" "Cryptol.Parser.AST" "cryptol-2.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" 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 ExportType Source #
Export information for a declaration.
Instances
| Eq ExportType Source # | |
Defined in Cryptol.Parser.AST | |
| Ord ExportType Source # | |
Defined in Cryptol.Parser.AST Methods compare :: ExportType -> ExportType -> Ordering # (<) :: ExportType -> ExportType -> Bool # (<=) :: ExportType -> ExportType -> Bool # (>) :: ExportType -> ExportType -> Bool # (>=) :: ExportType -> ExportType -> Bool # max :: ExportType -> ExportType -> ExportType # min :: ExportType -> ExportType -> ExportType # | |
| Show ExportType Source # | |
Defined in Cryptol.Parser.AST Methods showsPrec :: Int -> ExportType -> ShowS # show :: ExportType -> String # showList :: [ExportType] -> ShowS # | |
| Generic ExportType Source # | |
Defined in Cryptol.Parser.AST Associated Types type Rep ExportType :: Type -> Type # | |
| NFData ExportType Source # | |
Defined in Cryptol.Parser.AST Methods rnf :: ExportType -> () # | |
| type Rep ExportType Source # | |
data ExportSpec name Source #
Constructors
| ExportSpec | |
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.
Constructors
| PragmaNote String | |
| PragmaProperty |
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.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" 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.Parser.Fixity | |
| PP Fixity Source # | |
| type Rep Fixity Source # | |
Defined in Cryptol.Parser.Fixity type Rep Fixity = D1 (MetaData "Fixity" "Cryptol.Parser.Fixity" "cryptol-2.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" 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 # | |
| 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.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" False) (C1 (MetaCons "PrimMap" PrefixI True) (S1 (MetaSel (Just "primDecls") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map Ident Name)) :*: S1 (MetaSel (Just "primTypes") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map Ident Name)))) | |
data TCErrorMessage Source #
Constructors
| TCErrorMessage | |
Fields
| |
Instances
module Cryptol.TypeCheck.Type