cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.TypeCheck.AST

Description

Synopsis

- data Module = Module {
  - mName :: !ModName
  - mExports :: ExportSpec Name
  - mImports :: [Import]
  - mTySyns :: Map Name TySyn
  - mNewtypes :: Map Name Newtype
  - mDecls :: [DeclGroup]
  }
- data Kind
  - = KType
  - | KNum
  - | KProp
  - | Kind :-> Kind
- data Schema = Forall {
  - sVars :: [TParam]
  - sProps :: [Prop]
  - sType :: Type
  }
- data TySyn = TySyn {
  - tsName :: Name
  - tsParams :: [TParam]
  - tsConstraints :: [Prop]
  - tsDef :: Type
  }
- data Newtype = Newtype {
  - ntName :: Name
  - ntParams :: [TParam]
  - ntConstraints :: [Prop]
  - ntFields :: [(Ident, Type)]
  }
- data TParam = TParam {
  - tpUnique :: !Int
  - tpKind :: Kind
  - tpName :: Maybe Name
  }
- tpVar :: TParam -> TVar
- data Type
  - = TCon TCon [Type]
  - | TVar TVar
  - | TUser Name [Type] Type
  - | TRec [(Ident, Type)]
- type Prop = Type
- type SType = Type
- data TVar
  - = TVFree !Int Kind (Set TVar) Doc
  - | TVBound !Int Kind
- data TCon
  - = TC TC
  - | PC PC
  - | TF TFun
- data PC
  - = PEqual
  - | PNeq
  - | PGeq
  - | PFin
  - | PHas Selector
  - | PArith
  - | PCmp
- data TC
  - = TCNum Integer
  - | TCInf
  - | TCBit
  - | TCSeq
  - | TCFun
  - | TCTuple Int
  - | TCNewtype UserTC
- data UserTC = UserTC Name Kind
- data Expr
  - = EList [Expr] Type
  - | ETuple [Expr]
  - | ERec [(Ident, Expr)]
  - | ESel Expr Selector
  - | EIf Expr Expr Expr
  - | EComp Type Expr [[Match]]
  - | EVar Name
  - | ETAbs TParam Expr
  - | ETApp Expr Type
  - | EApp Expr Expr
  - | EAbs Name Type Expr
  - | EProofAbs Prop Expr
  - | EProofApp Expr
  - | ECast Expr Type
  - | EWhere Expr [DeclGroup]
- data Match
  - = From Name Type Expr
  - | Let Decl
- data DeclGroup
  - = Recursive [Decl]
  - | NonRecursive Decl
- groupDecls :: DeclGroup -> [Decl]
- data Decl = Decl {
  - dName :: !Name
  - dSignature :: Schema
  - dDefinition :: DeclDef
  - dPragmas :: [Pragma]
  - dInfix :: !Bool
  - dFixity :: Maybe Fixity
  - dDoc :: Maybe String
  }
- data DeclDef
  - = DPrim
  - | DExpr Expr
- isFreeTV :: TVar -> Bool
- isBoundTV :: TVar -> Bool
- tIsNat' :: Type -> Maybe Nat'
- tIsNum :: Type -> Maybe Integer
- tIsInf :: Type -> Bool
- tIsVar :: Type -> Maybe TVar
- tIsFun :: Type -> Maybe (Type, Type)
- tIsSeq :: Type -> Maybe (Type, Type)
- tIsBit :: Type -> Bool
- tIsTuple :: Type -> Maybe [Type]
- tIsBinFun :: TFun -> Type -> Maybe (Type, Type)
- tSplitFun :: TFun -> Type -> [Type]
- pIsFin :: Prop -> Maybe Type
- pIsGeq :: Prop -> Maybe (Type, Type)
- pIsEq :: Prop -> Maybe (Type, Type)
- pIsArith :: Prop -> Maybe Type
- pIsCmp :: Prop -> Maybe Type
- pIsNumeric :: Prop -> Bool
- tNum :: Integral a => a -> Type
- tZero :: Type
- tOne :: Type
- tTwo :: Type
- tInf :: Type
- tNat' :: Nat' -> Type
- tBit :: Type
- tWord :: Type -> Type
- tSeq :: Type -> Type -> Type
- tChar :: Type
- tString :: Int -> Type
- tRec :: [(Ident, Type)] -> Type
- tTuple :: [Type] -> Type
- tFun :: Type -> Type -> Type
- tNoUser :: Type -> Type
- tWidth :: Type -> Type
- tLenFromThen :: Type -> Type -> Type -> Type
- tLenFromThenTo :: Type -> Type -> Type -> Type
- tMax :: Type -> Type -> Type
- (=#=) :: Type -> Type -> Prop
- (=/=) :: Type -> Type -> Prop
- pArith :: Type -> Prop
- pCmp :: Type -> Prop
- (>==) :: Type -> Type -> Prop
- pHas :: Selector -> Type -> Type -> Prop
- pFin :: Type -> Prop
- (.*.) :: Type -> Type -> Type
- (.+.) :: Type -> Type -> Type
- (.-.) :: Type -> Type -> Type
- (.^.) :: Type -> Type -> Type
- tDiv :: Type -> Type -> Type
- tMod :: Type -> Type -> Type
- tMin :: Type -> Type -> Type
- newtypeTyCon :: Newtype -> TCon
- newtypeConType :: Newtype -> Schema
- ePrim :: PrimMap -> Ident -> Expr
- eError :: PrimMap -> Type -> String -> Expr
- eString :: PrimMap -> String -> Expr
- eChar :: PrimMap -> Char -> Expr
- class HasKind t where
- quickApply :: Kind -> [a] -> Kind
- addTNames :: [TParam] -> NameMap -> NameMap
- ppNewtypeShort :: Newtype -> Doc
- 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)
- data Name
- data TFun
  - = TCAdd
  - | TCSub
  - | TCMul
  - | TCDiv
  - | TCMod
  - | TCExp
  - | TCWidth
  - | TCMin
  - | TCMax
  - | TCLenFromThen
  - | TCLenFromThenTo
- data Selector
  - = TupleSel Int (Maybe Int)
  - | RecordSel Ident (Maybe [Ident])
  - | ListSel Int (Maybe Int)
- data Import = Import {
  - iModule :: !ModName
  - iAs :: Maybe ModName
  - iSpec :: Maybe ImportSpec
  }
- data ImportSpec
  - = Hiding [Ident]
  - | Only [Ident]
- data ExportType
  - = Public
  - | Private
- data ExportSpec name = ExportSpec {
  - eTypes :: Set name
  - eBinds :: Set name
  }
- isExportedBind :: Ord name => name -> ExportSpec name -> Bool
- isExportedType :: Ord name => name -> ExportSpec name -> Bool
- data Pragma
  - = PragmaNote String
  - | PragmaProperty
- data Fixity = Fixity {
  - fAssoc :: !Assoc
  - fLevel :: !Int
  }
- data PrimMap = PrimMap {
  - primDecls :: Map Ident Name
  - primTypes :: Map Ident Name
  }

# Documentation

data Module Source #

A Cryptol module.

Constructors

Module |

Fields

- mName :: !ModName
- mExports :: ExportSpec Name
- mImports :: [Import]
- mTySyns :: Map Name TySyn
- mNewtypes :: Map Name Newtype
- mDecls :: [DeclGroup]

Instances

Show Module Source # |
Methods showsPrec :: Int -> Module -> ShowS # show :: Module -> String # showList :: [Module] -> ShowS #
Generic Module Source # |
Associated Types type Rep Module :: * -> * # Methods from :: Module -> Rep Module x # to :: Rep Module x -> Module #
NFData Module Source # |
Methods rnf :: Module -> () #
PP Module Source # |
Methods ppPrec :: Int -> Module -> Doc Source #
TVars Module Source # |
Methods apSubst :: Subst -> Module -> Module Source #
PP (WithNames Module) Source # |
Methods ppPrec :: Int -> WithNames Module -> Doc Source #
type Rep Module Source # |

type Rep Module = D1 (MetaData "Module" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "Module" PrefixI True) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "mName") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 ModName)) ((:*:) (S1 (MetaSel (Just Symbol "mExports") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (ExportSpec Name))) (S1 (MetaSel (Just Symbol "mImports") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Import])))) ((:*:) (S1 (MetaSel (Just Symbol "mTySyns") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map Name TySyn))) ((:*:) (S1 (MetaSel (Just Symbol "mNewtypes") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map Name Newtype))) (S1 (MetaSel (Just Symbol "mDecls") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [DeclGroup]))))))

data Kind Source #

Kinds, classify types.

Constructors

KType |
KNum |
KProp |
Kind :-> Kind infixr 5 |

Instances

Eq Kind Source # |
Methods (==) :: Kind -> Kind -> Bool # (/=) :: Kind -> Kind -> Bool #
Show Kind Source # |
Methods showsPrec :: Int -> Kind -> ShowS # show :: Kind -> String # showList :: [Kind] -> ShowS #
Generic Kind Source # |
Associated Types type Rep Kind :: * -> * # Methods from :: Kind -> Rep Kind x # to :: Rep Kind x -> Kind #
NFData Kind Source # |
Methods rnf :: Kind -> () #
PP Kind Source # |
Methods ppPrec :: Int -> Kind -> Doc Source #
type Rep Kind Source # |

type Rep Kind = D1 (MetaData "Kind" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) ((:+:) (C1 (MetaCons "KType" PrefixI False) U1) (C1 (MetaCons "KNum" PrefixI False) U1)) ((:+:) (C1 (MetaCons "KProp" PrefixI False) U1) (C1 (MetaCons ":->" (InfixI RightAssociative 5) False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind))))))

data Schema Source #

The types of polymorphic values.

Constructors

Forall |

Fields

- sVars :: [TParam]
- sProps :: [Prop]
- sType :: Type

Instances

Eq Schema Source # |
Methods (==) :: Schema -> Schema -> Bool # (/=) :: Schema -> Schema -> Bool #
Show Schema Source # |
Methods showsPrec :: Int -> Schema -> ShowS # show :: Schema -> String # showList :: [Schema] -> ShowS #
Generic Schema Source # |
Associated Types type Rep Schema :: * -> * # Methods from :: Schema -> Rep Schema x # to :: Rep Schema x -> Schema #
NFData Schema Source # |
Methods rnf :: Schema -> () #
PP Schema Source # |
Methods ppPrec :: Int -> Schema -> Doc Source #
TVars Schema Source # | WARNING: This instance assumes that the quantified variables in the types in the substitution will not get captured by the quantified variables. This is reasonable because there should be no shadowing of quantified variables but, just in case, we make a sanity check and panic if somehow capture did occur.
Methods apSubst :: Subst -> Schema -> Schema Source #
FVS Schema Source # |
Methods fvs :: Schema -> Set TVar Source #
PP (WithNames Schema) Source # |
Methods ppPrec :: Int -> WithNames Schema -> Doc Source #
type Rep Schema Source # |

type Rep Schema = D1 (MetaData "Schema" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "Forall" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "sVars") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TParam])) ((:*:) (S1 (MetaSel (Just Symbol "sProps") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Prop])) (S1 (MetaSel (Just Symbol "sType") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)))))

data TySyn Source #

Type synonym.

Constructors

TySyn |

Fields

- tsName :: Name

  Name

- tsParams :: [TParam]

  Parameters

- tsConstraints :: [Prop]

  Ensure body is OK

- tsDef :: Type

  Definition

Instances

Eq TySyn Source # |
Methods (==) :: TySyn -> TySyn -> Bool # (/=) :: TySyn -> TySyn -> Bool #
Show TySyn Source # |
Methods showsPrec :: Int -> TySyn -> ShowS # show :: TySyn -> String # showList :: [TySyn] -> ShowS #
Generic TySyn Source # |
Associated Types type Rep TySyn :: * -> * # Methods from :: TySyn -> Rep TySyn x # to :: Rep TySyn x -> TySyn #
NFData TySyn Source # |
Methods rnf :: TySyn -> () #
PP TySyn Source # |
Methods ppPrec :: Int -> TySyn -> Doc Source #
HasKind TySyn Source # |
Methods kindOf :: TySyn -> Kind Source #
PP (WithNames TySyn) Source # |
Methods ppPrec :: Int -> WithNames TySyn -> Doc Source #
type Rep TySyn Source # |

type Rep TySyn = D1 (MetaData "TySyn" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "TySyn" PrefixI True) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "tsName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Just Symbol "tsParams") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TParam]))) ((:*:) (S1 (MetaSel (Just Symbol "tsConstraints") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Prop])) (S1 (MetaSel (Just Symbol "tsDef") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)))))

data Newtype Source #

Named records

Constructors

Newtype |

Fields

- ntName :: Name
- ntParams :: [TParam]
- ntConstraints :: [Prop]
- ntFields :: [(Ident, Type)]

Instances

Show Newtype Source # |
Methods showsPrec :: Int -> Newtype -> ShowS # show :: Newtype -> String # showList :: [Newtype] -> ShowS #
Generic Newtype Source # |
Associated Types type Rep Newtype :: * -> * # Methods from :: Newtype -> Rep Newtype x # to :: Rep Newtype x -> Newtype #
NFData Newtype Source # |
Methods rnf :: Newtype -> () #
HasKind Newtype Source # |
Methods kindOf :: Newtype -> Kind Source #
type Rep Newtype Source # |

type Rep Newtype = D1 (MetaData "Newtype" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "Newtype" PrefixI True) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "ntName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Just Symbol "ntParams") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TParam]))) ((:*:) (S1 (MetaSel (Just Symbol "ntConstraints") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Prop])) (S1 (MetaSel (Just Symbol "ntFields") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Ident, Type)])))))

data TParam Source #

Type parameters.

Constructors

TParam |

Fields

- tpUnique :: !Int

  Parameter identifier

- tpKind :: Kind

  Kind of parameter

- tpName :: Maybe Name

  Name from source, if any.

Instances

Eq TParam Source # |
Methods (==) :: TParam -> TParam -> Bool # (/=) :: TParam -> TParam -> Bool #
Ord TParam Source # |
Methods compare :: TParam -> TParam -> Ordering # (<) :: TParam -> TParam -> Bool # (<=) :: TParam -> TParam -> Bool # (>) :: TParam -> TParam -> Bool # (>=) :: TParam -> TParam -> Bool # max :: TParam -> TParam -> TParam # min :: TParam -> TParam -> TParam #
Show TParam Source # |
Methods showsPrec :: Int -> TParam -> ShowS # show :: TParam -> String # showList :: [TParam] -> ShowS #
Generic TParam Source # |
Associated Types type Rep TParam :: * -> * # Methods from :: TParam -> Rep TParam x # to :: Rep TParam x -> TParam #
NFData TParam Source # |
Methods rnf :: TParam -> () #
PP TParam Source # |
Methods ppPrec :: Int -> TParam -> Doc Source #
HasKind TParam Source # |
Methods kindOf :: TParam -> Kind Source #
PP (WithNames TParam) Source # |
Methods ppPrec :: Int -> WithNames TParam -> Doc Source #
type Rep TParam Source # |

type Rep TParam = D1 (MetaData "TParam" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "TParam" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "tpUnique") NoSourceUnpackedness SourceStrict DecidedUnpack) (Rec0 Int)) ((:*:) (S1 (MetaSel (Just Symbol "tpKind") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind)) (S1 (MetaSel (Just Symbol "tpName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Name))))))

tpVar :: TParam -> TVar Source #

data Type Source #

The internal representation of types. These are assumed to be kind correct.

Constructors

TCon TCon [Type] | Type constant with args
TVar TVar | Type variable (free or bound)
TUser Name [Type] Type | This is just a type annotation, for a type that was written as a type synonym. It is useful so that we can use it to report nicer errors. Example: `TUser T ts t` is really just the type `t` that was written as `T ts` by the user.
TRec [(Ident, Type)] | Record type

Instances

Eq Type Source # |
Methods (==) :: Type -> Type -> Bool # (/=) :: Type -> Type -> Bool #
Ord Type Source # |
Methods compare :: Type -> Type -> Ordering # (<) :: Type -> Type -> Bool # (<=) :: Type -> Type -> Bool # (>) :: Type -> Type -> Bool # (>=) :: Type -> Type -> Bool # max :: Type -> Type -> Type # min :: Type -> Type -> Type #
Show Type Source # |
Methods showsPrec :: Int -> Type -> ShowS # show :: Type -> String # showList :: [Type] -> ShowS #
Generic Type Source # |
Associated Types type Rep Type :: * -> * # Methods from :: Type -> Rep Type x # to :: Rep Type x -> Type #
NFData Type Source # |
Methods rnf :: Type -> () #
PP Type Source # |
Methods ppPrec :: Int -> Type -> Doc Source #
HasKind Type Source # |
Methods kindOf :: Type -> Kind Source #
TVars Type Source # |
Methods apSubst :: Subst -> Type -> Type Source #
FVS Type Source # |
Methods fvs :: Type -> Set TVar Source #
DebugLog Type Source # |
Methods debugLog :: Solver -> Type -> IO () Source # debugLogList :: Solver -> [Type] -> IO () Source #
TrieMap TypeMap Type Source # |
Methods emptyTM :: TypeMap a Source # nullTM :: TypeMap a -> Bool Source # lookupTM :: Type -> TypeMap a -> Maybe a Source # alterTM :: Type -> (Maybe a -> Maybe a) -> TypeMap a -> TypeMap a Source # unionTM :: (a -> a -> a) -> TypeMap a -> TypeMap a -> TypeMap a Source # toListTM :: TypeMap a -> [(Type, a)] Source # mapMaybeWithKeyTM :: (Type -> a -> Maybe b) -> TypeMap a -> TypeMap b Source #
PP (WithNames Type) Source # |
Methods ppPrec :: Int -> WithNames Type -> Doc Source #
type Rep Type Source # |

type Rep Type = D1 (MetaData "Type" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) ((:+:) (C1 (MetaCons "TCon" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TCon)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Type])))) (C1 (MetaCons "TVar" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TVar)))) ((:+:) (C1 (MetaCons "TUser" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Type])) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type))))) (C1 (MetaCons "TRec" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Ident, Type)])))))

type Prop = Type Source #

The type is supposed to be of kind `KProp`

type SType = Type Source #

The type is "simple" (i.e., it contains no type functions).

data TVar Source #

Type variables.

Constructors

TVFree !Int Kind (Set TVar) Doc | Unique, kind, ids of bound type variables that are in scope The `Doc` is a description of how this type came to be.
TVBound !Int Kind |

Instances

Eq TVar Source # |
Methods (==) :: TVar -> TVar -> Bool # (/=) :: TVar -> TVar -> Bool #
Ord TVar Source # |
Methods compare :: TVar -> TVar -> Ordering # (<) :: TVar -> TVar -> Bool # (<=) :: TVar -> TVar -> Bool # (>) :: TVar -> TVar -> Bool # (>=) :: TVar -> TVar -> Bool # max :: TVar -> TVar -> TVar # min :: TVar -> TVar -> TVar #
Show TVar Source # |
Methods showsPrec :: Int -> TVar -> ShowS # show :: TVar -> String # showList :: [TVar] -> ShowS #
Generic TVar Source # |
Associated Types type Rep TVar :: * -> * # Methods from :: TVar -> Rep TVar x # to :: Rep TVar x -> TVar #
NFData TVar Source # |
Methods rnf :: TVar -> () #
PP TVar Source # |
Methods ppPrec :: Int -> TVar -> Doc Source #
HasKind TVar Source # |
Methods kindOf :: TVar -> Kind Source #
PP (WithNames TVar) Source # |
Methods ppPrec :: Int -> WithNames TVar -> Doc Source #
type Rep TVar Source # |

type Rep TVar = D1 (MetaData "TVar" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "TVFree" PrefixI False) ((:*:) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedUnpack) (Rec0 Int)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind))) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Set TVar))) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Doc))))) (C1 (MetaCons "TVBound" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedUnpack) (Rec0 Int)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind)))))

data TCon Source #

Type constants.

Constructors

TC TC |
PC PC |
TF TFun |

Instances

Eq TCon Source # |
Methods (==) :: TCon -> TCon -> Bool # (/=) :: TCon -> TCon -> Bool #
Ord TCon Source # |
Methods compare :: TCon -> TCon -> Ordering # (<) :: TCon -> TCon -> Bool # (<=) :: TCon -> TCon -> Bool # (>) :: TCon -> TCon -> Bool # (>=) :: TCon -> TCon -> Bool # max :: TCon -> TCon -> TCon # min :: TCon -> TCon -> TCon #
Show TCon Source # |
Methods showsPrec :: Int -> TCon -> ShowS # show :: TCon -> String # showList :: [TCon] -> ShowS #
Generic TCon Source # |
Associated Types type Rep TCon :: * -> * # Methods from :: TCon -> Rep TCon x # to :: Rep TCon x -> TCon #
NFData TCon Source # |
Methods rnf :: TCon -> () #
PP TCon Source # |
Methods ppPrec :: Int -> TCon -> Doc Source #
HasKind TCon Source # |
Methods kindOf :: TCon -> Kind Source #
type Rep TCon Source # |

type Rep TCon = D1 (MetaData "TCon" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "TC" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TC))) ((:+:) (C1 (MetaCons "PC" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PC))) (C1 (MetaCons "TF" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TFun)))))

data PC Source #

Built-in type constants.

Predicate symbols.

Constructors

PEqual

    _ == _

PNeq

    _ /= _

PGeq

    _ >= _

PFin

    fin _

PHas Selector | `Has sel type field` does not appear in schemas

PArith

    Arith _

PCmp

    Cmp _

Instances

Eq PC Source # |
Methods (==) :: PC -> PC -> Bool # (/=) :: PC -> PC -> Bool #
Ord PC Source # |
Methods compare :: PC -> PC -> Ordering # (<) :: PC -> PC -> Bool # (<=) :: PC -> PC -> Bool # (>) :: PC -> PC -> Bool # (>=) :: PC -> PC -> Bool # max :: PC -> PC -> PC # min :: PC -> PC -> PC #
Show PC Source # |
Methods showsPrec :: Int -> PC -> ShowS # show :: PC -> String # showList :: [PC] -> ShowS #
Generic PC Source # |
Associated Types type Rep PC :: * -> * # Methods from :: PC -> Rep PC x # to :: Rep PC x -> PC #
NFData PC Source # |
Methods rnf :: PC -> () #
PP PC Source # |
Methods ppPrec :: Int -> PC -> Doc Source #
HasKind PC Source # |
Methods kindOf :: PC -> Kind Source #
type Rep PC Source # |

type Rep PC = D1 (MetaData "PC" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) ((:+:) (C1 (MetaCons "PEqual" PrefixI False) U1) ((:+:) (C1 (MetaCons "PNeq" PrefixI False) U1) (C1 (MetaCons "PGeq" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "PFin" PrefixI False) U1) (C1 (MetaCons "PHas" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Selector)))) ((:+:) (C1 (MetaCons "PArith" PrefixI False) U1) (C1 (MetaCons "PCmp" PrefixI False) U1))))

data TC Source #

1-1 constants.

Constructors

TCNum Integer | Numbers
TCInf | Inf
TCBit | Bit

TCSeq

    [_] _

TCFun

    _ -> _

TCTuple Int

    (_, _, _)

TCNewtype UserTC | user-defined, `T`

Instances

Eq TC Source # |
Methods (==) :: TC -> TC -> Bool # (/=) :: TC -> TC -> Bool #
Ord TC Source # |
Methods compare :: TC -> TC -> Ordering # (<) :: TC -> TC -> Bool # (<=) :: TC -> TC -> Bool # (>) :: TC -> TC -> Bool # (>=) :: TC -> TC -> Bool # max :: TC -> TC -> TC # min :: TC -> TC -> TC #
Show TC Source # |
Methods showsPrec :: Int -> TC -> ShowS # show :: TC -> String # showList :: [TC] -> ShowS #
Generic TC Source # |
Associated Types type Rep TC :: * -> * # Methods from :: TC -> Rep TC x # to :: Rep TC x -> TC #
NFData TC Source # |
Methods rnf :: TC -> () #
PP TC Source # |
Methods ppPrec :: Int -> TC -> Doc Source #
HasKind TC Source # |
Methods kindOf :: TC -> Kind Source #
type Rep TC Source # |

type Rep TC = D1 (MetaData "TC" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) ((:+:) (C1 (MetaCons "TCNum" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer))) ((:+:) (C1 (MetaCons "TCInf" PrefixI False) U1) (C1 (MetaCons "TCBit" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "TCSeq" PrefixI False) U1) (C1 (MetaCons "TCFun" PrefixI False) U1)) ((:+:) (C1 (MetaCons "TCTuple" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int))) (C1 (MetaCons "TCNewtype" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 UserTC))))))

data UserTC Source #

Constructors

UserTC Name Kind |

Instances

Eq UserTC Source # |
Methods (==) :: UserTC -> UserTC -> Bool # (/=) :: UserTC -> UserTC -> Bool #
Ord UserTC Source # |
Methods compare :: UserTC -> UserTC -> Ordering # (<) :: UserTC -> UserTC -> Bool # (<=) :: UserTC -> UserTC -> Bool # (>) :: UserTC -> UserTC -> Bool # (>=) :: UserTC -> UserTC -> Bool # max :: UserTC -> UserTC -> UserTC # min :: UserTC -> UserTC -> UserTC #
Show UserTC Source # |
Methods showsPrec :: Int -> UserTC -> ShowS # show :: UserTC -> String # showList :: [UserTC] -> ShowS #
Generic UserTC Source # |
Associated Types type Rep UserTC :: * -> * # Methods from :: UserTC -> Rep UserTC x # to :: Rep UserTC x -> UserTC #
NFData UserTC Source # |
Methods rnf :: UserTC -> () #
PP UserTC Source # |
Methods ppPrec :: Int -> UserTC -> Doc Source #
HasKind UserTC Source # |
Methods kindOf :: UserTC -> Kind Source #
type Rep UserTC Source # |
type Rep UserTC = D1 (MetaData "UserTC" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "UserTC" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind))))

data Expr Source #

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
EIf Expr Expr Expr | If-then-else
EComp Type Expr [[Match]] | List comprehensions The type caches the type of the expr.
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 `Type` term, which should be of kind `KProp`.
EProofApp Expr | If `e : p => t`, then `EProofApp e : t`, as long as we can prove `p`. 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.

ECast Expr Type

if e : t1, then cast e : t2 as long as we can prove that 't1 = t2'. We could express this in terms of a built-in constant. `cast :: {a,b} (a =*= b) => a -> b`

Using the constant is a bit verbose though, because we end up with both the source and target type. So, instead we use this language construct, which only stores the target type, and the source type can be reconstructed from the expression.

Another way to think of this is simply as an expression with an explicit type annotation.

EWhere Expr [DeclGroup] |

Instances

Show Expr Source # |
Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #
Generic Expr Source # |
Associated Types type Rep Expr :: * -> * # Methods from :: Expr -> Rep Expr x # to :: Rep Expr x -> Expr #
NFData Expr Source # |
Methods rnf :: Expr -> () #
PP Expr Source # |
Methods ppPrec :: Int -> Expr -> Doc Source #
TVars Expr Source # |
Methods apSubst :: Subst -> Expr -> Expr Source #
PP (WithNames Expr) Source # |
Methods ppPrec :: Int -> WithNames Expr -> Doc Source #
type Rep Expr Source # |

type Rep Expr = D1 (MetaData "Expr" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "EList" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Expr])) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)))) ((:+:) (C1 (MetaCons "ETuple" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Expr]))) (C1 (MetaCons "ERec" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Ident, Expr)]))))) ((:+:) ((:+:) (C1 (MetaCons "ESel" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Selector)))) (C1 (MetaCons "EIf" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr)) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr)))))) ((:+:) (C1 (MetaCons "EComp" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [[Match]]))))) (C1 (MetaCons "EVar" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)))))) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "ETAbs" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TParam)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr)))) (C1 (MetaCons "ETApp" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type))))) ((:+:) (C1 (MetaCons "EApp" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr)))) (C1 (MetaCons "EAbs" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr))))))) ((:+:) ((:+:) (C1 (MetaCons "EProofAbs" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Prop)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr)))) (C1 (MetaCons "EProofApp" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr)))) ((:+:) (C1 (MetaCons "ECast" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)))) (C1 (MetaCons "EWhere" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [DeclGroup]))))))))

data Match Source #

Constructors

From Name Type Expr | do we need this type? it seems like it can be computed from the expr
Let Decl |

Instances

Show Match Source # |
Methods showsPrec :: Int -> Match -> ShowS # show :: Match -> String # showList :: [Match] -> ShowS #
Generic Match Source # |
Associated Types type Rep Match :: * -> * # Methods from :: Match -> Rep Match x # to :: Rep Match x -> Match #
NFData Match Source # |
Methods rnf :: Match -> () #
PP Match Source # |
Methods ppPrec :: Int -> Match -> Doc Source #
TVars Match Source # |
Methods apSubst :: Subst -> Match -> Match Source #
PP (WithNames Match) Source # |
Methods ppPrec :: Int -> WithNames Match -> Doc Source #
type Rep Match Source # |

type Rep Match = D1 (MetaData "Match" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "From" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr))))) (C1 (MetaCons "Let" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Decl))))

data DeclGroup Source #

Constructors

Recursive [Decl] | Mutually recursive declarations
NonRecursive Decl | Non-recursive declaration

Instances

Show DeclGroup Source # |
Methods showsPrec :: Int -> DeclGroup -> ShowS # show :: DeclGroup -> String # showList :: [DeclGroup] -> ShowS #
Generic DeclGroup Source # |
Associated Types type Rep DeclGroup :: * -> * # Methods from :: DeclGroup -> Rep DeclGroup x # to :: Rep DeclGroup x -> DeclGroup #
NFData DeclGroup Source # |
Methods rnf :: DeclGroup -> () #
PP DeclGroup Source # |
Methods ppPrec :: Int -> DeclGroup -> Doc Source #
TVars DeclGroup Source # |
Methods apSubst :: Subst -> DeclGroup -> DeclGroup Source #
PP (WithNames DeclGroup) Source # |
Methods ppPrec :: Int -> WithNames DeclGroup -> Doc Source #
type Rep DeclGroup Source # |

type Rep DeclGroup = D1 (MetaData "DeclGroup" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "Recursive" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Decl]))) (C1 (MetaCons "NonRecursive" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Decl))))

groupDecls :: DeclGroup -> [Decl] Source #

data Decl Source #

Constructors

Decl |

Fields

- dName :: !Name
- dSignature :: Schema
- dDefinition :: DeclDef
- dPragmas :: [Pragma]
- dInfix :: !Bool
- dFixity :: Maybe Fixity
- dDoc :: Maybe String

Instances

Show Decl Source # |
Methods showsPrec :: Int -> Decl -> ShowS # show :: Decl -> String # showList :: [Decl] -> ShowS #
Generic Decl Source # |
Associated Types type Rep Decl :: * -> * # Methods from :: Decl -> Rep Decl x # to :: Rep Decl x -> Decl #
NFData Decl Source # |
Methods rnf :: Decl -> () #
PP Decl Source # |
Methods ppPrec :: Int -> Decl -> Doc Source #
TVars Decl Source # |
Methods apSubst :: Subst -> Decl -> Decl Source #
PP (WithNames Decl) Source # |
Methods ppPrec :: Int -> WithNames Decl -> Doc Source #
type Rep Decl Source # |

type Rep Decl = D1 (MetaData "Decl" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "Decl" PrefixI True) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "dName") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Name)) ((:*:) (S1 (MetaSel (Just Symbol "dSignature") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Schema)) (S1 (MetaSel (Just Symbol "dDefinition") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 DeclDef)))) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "dPragmas") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Pragma])) (S1 (MetaSel (Just Symbol "dInfix") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Bool))) ((:*:) (S1 (MetaSel (Just Symbol "dFixity") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Fixity))) (S1 (MetaSel (Just Symbol "dDoc") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe String)))))))

data DeclDef Source #

Constructors

DPrim |
DExpr Expr |

Instances

Show DeclDef Source # |
Methods showsPrec :: Int -> DeclDef -> ShowS # show :: DeclDef -> String # showList :: [DeclDef] -> ShowS #
Generic DeclDef Source # |
Associated Types type Rep DeclDef :: * -> * # Methods from :: DeclDef -> Rep DeclDef x # to :: Rep DeclDef x -> DeclDef #
NFData DeclDef Source # |
Methods rnf :: DeclDef -> () #
TVars DeclDef Source # |
Methods apSubst :: Subst -> DeclDef -> DeclDef Source #
PP (WithNames DeclDef) Source # |
Methods ppPrec :: Int -> WithNames DeclDef -> Doc Source #
type Rep DeclDef Source # |
type Rep DeclDef = D1 (MetaData "DeclDef" "Cryptol.TypeCheck.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "DPrim" PrefixI False) U1) (C1 (MetaCons "DExpr" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr))))

isFreeTV :: TVar -> Bool Source #

isBoundTV :: TVar -> Bool Source #

tIsNat' :: Type -> Maybe Nat' Source #

tIsNum :: Type -> Maybe Integer Source #

tIsInf :: Type -> Bool Source #

tIsVar :: Type -> Maybe TVar Source #

tIsFun :: Type -> Maybe (Type, Type) Source #

tIsSeq :: Type -> Maybe (Type, Type) Source #

tIsBit :: Type -> Bool Source #

tIsTuple :: Type -> Maybe [Type] Source #

tIsBinFun :: TFun -> Type -> Maybe (Type, Type) Source #

tSplitFun :: TFun -> Type -> [Type] Source #

Split up repeated occurances of the given binary type-level function.

pIsFin :: Prop -> Maybe Type Source #

pIsGeq :: Prop -> Maybe (Type, Type) Source #

pIsEq :: Prop -> Maybe (Type, Type) Source #

pIsArith :: Prop -> Maybe Type Source #

pIsCmp :: Prop -> Maybe Type Source #

pIsNumeric :: Prop -> Bool Source #

tNum :: Integral a => a -> Type Source #

tZero :: Type Source #

tOne :: Type Source #

tTwo :: Type Source #

tInf :: Type Source #

tNat' :: Nat' -> Type Source #

tBit :: Type Source #

tWord :: Type -> Type Source #

tSeq :: Type -> Type -> Type Source #

tChar :: Type Source #

tString :: Int -> Type Source #

tRec :: [(Ident, Type)] -> Type Source #

tTuple :: [Type] -> Type Source #

tFun :: Type -> Type -> Type infixr 5 Source #

Make a function type.

tNoUser :: Type -> Type Source #

Eliminate outermost type synonyms.

tWidth :: Type -> Type Source #

tLenFromThen :: Type -> Type -> Type -> Type Source #

tLenFromThenTo :: Type -> Type -> Type -> Type Source #

tMax :: Type -> Type -> Type Source #

(=#=) :: Type -> Type -> Prop infix 4 Source #

Equality for numeric types.

(=/=) :: Type -> Type -> Prop Source #

pArith :: Type -> Prop Source #

pCmp :: Type -> Prop Source #

(>==) :: Type -> Type -> Prop infix 4 Source #

Make a greater-than-or-equal-to constraint.

pHas :: Selector -> Type -> Type -> Prop Source #

A `Has` constraint, used for tuple and record selection.

pFin :: Type -> Prop Source #

(.*.) :: Type -> Type -> Type infixl 7 Source #

Make multiplication type.

(.+.) :: Type -> Type -> Type infixl 6 Source #

Make addition type.

(.-.) :: Type -> Type -> Type Source #

(.^.) :: Type -> Type -> Type Source #

tDiv :: Type -> Type -> Type Source #

tMod :: Type -> Type -> Type Source #

tMin :: Type -> Type -> Type Source #

Make a `min` type.

newtypeTyCon :: Newtype -> TCon Source #

newtypeConType :: Newtype -> Schema 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.

eString :: PrimMap -> String -> Expr Source #

eChar :: PrimMap -> Char -> Expr Source #

class HasKind t where Source #

Minimal complete definition

kindOf

Methods

kindOf :: t -> Kind Source #

Instances

HasKind TFun Source # |
Methods kindOf :: TFun -> Kind Source #
HasKind UserTC Source # |
Methods kindOf :: UserTC -> Kind Source #
HasKind TC Source # |
Methods kindOf :: TC -> Kind Source #
HasKind PC Source # |
Methods kindOf :: PC -> Kind Source #
HasKind TCon Source # |
Methods kindOf :: TCon -> Kind Source #
HasKind TVar Source # |
Methods kindOf :: TVar -> Kind Source #
HasKind Type Source # |
Methods kindOf :: Type -> Kind Source #
HasKind TParam Source # |
Methods kindOf :: TParam -> Kind Source #
HasKind Newtype Source # |
Methods kindOf :: Newtype -> Kind Source #
HasKind TySyn Source # |
Methods kindOf :: TySyn -> Kind Source #

quickApply :: Kind -> [a] -> Kind Source #

addTNames :: [TParam] -> NameMap -> NameMap Source #

ppNewtypeShort :: Newtype -> Doc Source #

ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name, Type)] -> Expr -> Doc Source #

splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a) Source #

splitAbs :: Expr -> Maybe ((Name, Type), Expr) Source #

splitTAbs :: Expr -> Maybe (TParam, Expr) Source #

splitProofAbs :: Expr -> Maybe (Prop, Expr) Source #

data Name Source #

Instances

Eq Name Source # |
Methods (==) :: Name -> Name -> Bool # (/=) :: Name -> Name -> Bool #
Ord Name Source # |
Methods compare :: Name -> Name -> Ordering # (<) :: Name -> Name -> Bool # (<=) :: Name -> Name -> Bool # (>) :: Name -> Name -> Bool # (>=) :: Name -> Name -> Bool # max :: Name -> Name -> Name # min :: Name -> Name -> Name #
Show Name Source # |
Methods showsPrec :: Int -> Name -> ShowS # show :: Name -> String # showList :: [Name] -> ShowS #
Generic Name Source # |
Associated Types type Rep Name :: * -> * # Methods from :: Name -> Rep Name x # to :: Rep Name x -> Name #
NFData Name Source # |
Methods rnf :: Name -> () #
PPName Name Source # |
Methods ppNameFixity :: Name -> Maybe (Assoc, Int) Source # ppPrefixName :: Name -> Doc Source # ppInfixName :: Name -> Doc Source #
PP Name Source # |
Methods ppPrec :: Int -> Name -> Doc Source #
FromDecl (Decl Name) Source # |
Methods toBind :: Decl Name -> Maybe (Bind Name) Source # toTyDecl :: Decl Name -> Maybe TyDecl Source # isTopDecl :: Decl Name -> Bool Source #
FromDecl (TopDecl Name) Source # |
Methods toBind :: TopDecl Name -> Maybe (Bind Name) Source # toTyDecl :: TopDecl Name -> Maybe TyDecl Source # isTopDecl :: TopDecl Name -> Bool Source #
type Rep Name Source # |

type Rep Name = D1 (MetaData "Name" "Cryptol.ModuleSystem.Name" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "Name" PrefixI True) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "nUnique") SourceUnpack SourceStrict DecidedUnpack) (Rec0 Int)) (S1 (MetaSel (Just Symbol "nInfo") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 NameInfo))) ((:*:) (S1 (MetaSel (Just Symbol "nIdent") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Ident)) ((:*:) (S1 (MetaSel (Just Symbol "nFixity") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (Maybe Fixity))) (S1 (MetaSel (Just Symbol "nLoc") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Range))))))

data TFun Source #

Built-in 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

TCLenFromThen | `: Num -> Num -> Num -> Num` Example: `[ 1, 5 .. ] :: [lengthFromThen 1 5 b][b]`
TCLenFromThenTo | `: Num -> Num -> Num -> Num` Example: `[ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]`

Instances

Bounded TFun Source # |
Methods minBound :: TFun # maxBound :: TFun #
Enum TFun Source # |
Methods succ :: TFun -> TFun # pred :: TFun -> TFun # toEnum :: Int -> TFun # fromEnum :: TFun -> Int # enumFrom :: TFun -> [TFun] # enumFromThen :: TFun -> TFun -> [TFun] # enumFromTo :: TFun -> TFun -> [TFun] # enumFromThenTo :: TFun -> TFun -> TFun -> [TFun] #
Eq TFun Source # |
Methods (==) :: TFun -> TFun -> Bool # (/=) :: TFun -> TFun -> Bool #
Ord TFun Source # |
Methods compare :: TFun -> TFun -> Ordering # (<) :: TFun -> TFun -> Bool # (<=) :: TFun -> TFun -> Bool # (>) :: TFun -> TFun -> Bool # (>=) :: TFun -> TFun -> Bool # max :: TFun -> TFun -> TFun # min :: TFun -> TFun -> TFun #
Show TFun Source # |
Methods showsPrec :: Int -> TFun -> ShowS # show :: TFun -> String # showList :: [TFun] -> ShowS #
Generic TFun Source # |
Associated Types type Rep TFun :: * -> * # Methods from :: TFun -> Rep TFun x # to :: Rep TFun x -> TFun #
NFData TFun Source # |
Methods rnf :: TFun -> () #
PPName TFun Source # |
Methods ppNameFixity :: TFun -> Maybe (Assoc, Int) Source # ppPrefixName :: TFun -> Doc Source # ppInfixName :: TFun -> Doc Source #
PP TFun Source # |
Methods ppPrec :: Int -> TFun -> Doc Source #
HasKind TFun Source # |
Methods kindOf :: TFun -> Kind Source #
type Rep TFun Source # |

type Rep TFun = D1 (MetaData "TFun" "Cryptol.Prims.Syntax" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "TCAdd" PrefixI False) U1) (C1 (MetaCons "TCSub" PrefixI False) U1)) ((:+:) (C1 (MetaCons "TCMul" PrefixI False) U1) ((:+:) (C1 (MetaCons "TCDiv" PrefixI False) U1) (C1 (MetaCons "TCMod" PrefixI False) U1)))) ((:+:) ((:+:) (C1 (MetaCons "TCExp" PrefixI False) U1) ((:+:) (C1 (MetaCons "TCWidth" PrefixI False) U1) (C1 (MetaCons "TCMin" PrefixI False) U1))) ((:+:) (C1 (MetaCons "TCMax" PrefixI False) U1) ((:+:) (C1 (MetaCons "TCLenFromThen" PrefixI False) U1) (C1 (MetaCons "TCLenFromThenTo" PrefixI False) U1)))))

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

Eq Selector Source # |
Methods (==) :: Selector -> Selector -> Bool # (/=) :: Selector -> Selector -> Bool #
Ord Selector Source # |
Methods compare :: Selector -> Selector -> Ordering # (<) :: Selector -> Selector -> Bool # (<=) :: Selector -> Selector -> Bool # (>) :: Selector -> Selector -> Bool # (>=) :: Selector -> Selector -> Bool # max :: Selector -> Selector -> Selector # min :: Selector -> Selector -> Selector #
Show Selector Source # |
Methods showsPrec :: Int -> Selector -> ShowS # show :: Selector -> String # showList :: [Selector] -> ShowS #
Generic Selector Source # |
Associated Types type Rep Selector :: * -> * # Methods from :: Selector -> Rep Selector x # to :: Rep Selector x -> Selector #
NFData Selector Source # |
Methods rnf :: Selector -> () #
PP Selector Source # |
Methods ppPrec :: Int -> Selector -> Doc Source #
type Rep Selector Source # |

type Rep Selector = D1 (MetaData "Selector" "Cryptol.Parser.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "TupleSel" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Int))))) ((:+:) (C1 (MetaCons "RecordSel" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Ident)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe [Ident]))))) (C1 (MetaCons "ListSel" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Int)))))))

data Import Source #

An import declaration.

Constructors

Import |

Fields

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

Instances

Eq Import Source # |
Methods (==) :: Import -> Import -> Bool # (/=) :: Import -> Import -> Bool #
Show Import Source # |
Methods showsPrec :: Int -> Import -> ShowS # show :: Import -> String # showList :: [Import] -> ShowS #
Generic Import Source # |
Associated Types type Rep Import :: * -> * # Methods from :: Import -> Rep Import x # to :: Rep Import x -> Import #
NFData Import Source # |
Methods rnf :: Import -> () #
PP Import Source # |
Methods ppPrec :: Int -> Import -> Doc Source #
type Rep Import Source # |

type Rep Import = D1 (MetaData "Import" "Cryptol.Parser.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "Import" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "iModule") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 ModName)) ((:*:) (S1 (MetaSel (Just Symbol "iAs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe ModName))) (S1 (MetaSel (Just Symbol "iSpec") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe ImportSpec))))))

data ImportSpec Source #

The list of names following an import.

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

Constructors

Hiding [Ident] |
Only [Ident] |

Instances

Eq ImportSpec Source # |
Methods (==) :: ImportSpec -> ImportSpec -> Bool # (/=) :: ImportSpec -> ImportSpec -> Bool #
Show ImportSpec Source # |
Methods showsPrec :: Int -> ImportSpec -> ShowS # show :: ImportSpec -> String # showList :: [ImportSpec] -> ShowS #
Generic ImportSpec Source # |
Associated Types type Rep ImportSpec :: * -> * # Methods from :: ImportSpec -> Rep ImportSpec x # to :: Rep ImportSpec x -> ImportSpec #
NFData ImportSpec Source # |
Methods rnf :: ImportSpec -> () #
PP ImportSpec Source # |
Methods ppPrec :: Int -> ImportSpec -> Doc Source #
type Rep ImportSpec Source # |
type Rep ImportSpec = D1 (MetaData "ImportSpec" "Cryptol.Parser.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "Hiding" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Ident]))) (C1 (MetaCons "Only" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Ident]))))

data ExportType Source #

Export information for a declaration.

Constructors

Public |
Private |

Instances

Eq ExportType Source # |
Methods (==) :: ExportType -> ExportType -> Bool # (/=) :: ExportType -> ExportType -> Bool #
Ord ExportType Source # |
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 # |
Methods showsPrec :: Int -> ExportType -> ShowS # show :: ExportType -> String # showList :: [ExportType] -> ShowS #
Generic ExportType Source # |
Associated Types type Rep ExportType :: * -> * # Methods from :: ExportType -> Rep ExportType x # to :: Rep ExportType x -> ExportType #
NFData ExportType Source # |
Methods rnf :: ExportType -> () #
type Rep ExportType Source # |
type Rep ExportType = D1 (MetaData "ExportType" "Cryptol.Parser.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "Public" PrefixI False) U1) (C1 (MetaCons "Private" PrefixI False) U1))

data ExportSpec name Source #

Constructors

ExportSpec |

Fields

- eTypes :: Set name
- eBinds :: Set name

Instances

Show name => Show (ExportSpec name) Source # |
Methods showsPrec :: Int -> ExportSpec name -> ShowS # show :: ExportSpec name -> String # showList :: [ExportSpec name] -> ShowS #
Generic (ExportSpec name) Source # |
Associated Types type Rep (ExportSpec name) :: * -> * # Methods from :: ExportSpec name -> Rep (ExportSpec name) x # to :: Rep (ExportSpec name) x -> ExportSpec name #
Ord name => Monoid (ExportSpec name) Source # |
Methods mempty :: ExportSpec name # mappend :: ExportSpec name -> ExportSpec name -> ExportSpec name # mconcat :: [ExportSpec name] -> ExportSpec name #
NFData name => NFData (ExportSpec name) Source # |
Methods rnf :: ExportSpec name -> () #
type Rep (ExportSpec name) Source # |
type Rep (ExportSpec name) = D1 (MetaData "ExportSpec" "Cryptol.Parser.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "ExportSpec" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "eTypes") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Set name))) (S1 (MetaSel (Just Symbol "eBinds") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Set name)))))

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.

data Pragma Source #

Constructors

PragmaNote String |
PragmaProperty |

Instances

Eq Pragma Source # |
Methods (==) :: Pragma -> Pragma -> Bool # (/=) :: Pragma -> Pragma -> Bool #
Show Pragma Source # |
Methods showsPrec :: Int -> Pragma -> ShowS # show :: Pragma -> String # showList :: [Pragma] -> ShowS #
Generic Pragma Source # |
Associated Types type Rep Pragma :: * -> * # Methods from :: Pragma -> Rep Pragma x # to :: Rep Pragma x -> Pragma #
NFData Pragma Source # |
Methods rnf :: Pragma -> () #
PP Pragma Source # |
Methods ppPrec :: Int -> Pragma -> Doc Source #
NoPos Pragma Source # |
Methods noPos :: Pragma -> Pragma Source #
type Rep Pragma Source # |
type Rep Pragma = D1 (MetaData "Pragma" "Cryptol.Parser.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "PragmaNote" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))) (C1 (MetaCons "PragmaProperty" PrefixI False) U1))

data Fixity Source #

Constructors

Fixity |

Fields

- fAssoc :: !Assoc
- fLevel :: !Int

Instances

Eq Fixity Source # |
Methods (==) :: Fixity -> Fixity -> Bool # (/=) :: Fixity -> Fixity -> Bool #
Show Fixity Source # |
Methods showsPrec :: Int -> Fixity -> ShowS # show :: Fixity -> String # showList :: [Fixity] -> ShowS #
Generic Fixity Source # |
Associated Types type Rep Fixity :: * -> * # Methods from :: Fixity -> Rep Fixity x # to :: Rep Fixity x -> Fixity #
NFData Fixity Source # |
Methods rnf :: Fixity -> () #
type Rep Fixity Source # |
type Rep Fixity = D1 (MetaData "Fixity" "Cryptol.Parser.AST" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "Fixity" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "fAssoc") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Assoc)) (S1 (MetaSel (Just Symbol "fLevel") NoSourceUnpackedness SourceStrict DecidedUnpack) (Rec0 Int))))

data PrimMap Source #

A mapping from an identifier defined in some module to its real name.

Constructors

PrimMap |

Fields

- primDecls :: Map Ident Name
- primTypes :: Map Ident Name

Instances

Show PrimMap Source # |
Methods showsPrec :: Int -> PrimMap -> ShowS # show :: PrimMap -> String # showList :: [PrimMap] -> ShowS #
Generic PrimMap Source # |
Associated Types type Rep PrimMap :: * -> * # Methods from :: PrimMap -> Rep PrimMap x # to :: Rep PrimMap x -> PrimMap #
NFData PrimMap Source # |
Methods rnf :: PrimMap -> () #
type Rep PrimMap Source # |
type Rep PrimMap = D1 (MetaData "PrimMap" "Cryptol.ModuleSystem.Name" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "PrimMap" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "primDecls") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map Ident Name))) (S1 (MetaSel (Just Symbol "primTypes") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map Ident Name)))))