Cryptol.TypeCheck.Depends

Documentation

data TyDecl

Constructors

TS (TySyn Name) (Maybe String)

Type synonym

NT (Newtype Name) (Maybe String)

Newtype

AT (ParameterType Name) (Maybe String)

Parameter type

PS (PropSyn Name) (Maybe String)

Property synonym

PT (PrimType Name) (Maybe String)

A primitive/abstract typee

Instances

Show TyDecl

Defined in Cryptol.TypeCheck.Depends

Methods

showsPrec :: Int -> TyDecl -> ShowS

show :: TyDecl -> String

showList :: [TyDecl] -> ShowS

setDocString :: Maybe String -> TyDecl -> TyDecl

orderTyDecls :: [TyDecl] -> InferM [TyDecl]

Check for duplicate and recursive type synonyms. Returns the type-synonyms in dependency order.

orderBinds :: [Bind Name] -> [SCC (Bind Name)]

Associate type signatures with bindings and order bindings by dependency.

class FromDecl d where

Methods

toBind :: d -> Maybe (Bind Name)

toParamFun :: d -> Maybe (ParameterFun Name)

toParamConstraints :: d -> [Located (Prop Name)]

toTyDecl :: d -> Maybe TyDecl

isTopDecl :: d -> Bool

Instances

FromDecl (Decl Name)

Defined in Cryptol.TypeCheck.Depends

Methods

toBind :: Decl Name -> Maybe (Bind Name)

toParamFun :: Decl Name -> Maybe (ParameterFun Name)

toParamConstraints :: Decl Name -> [Located (Prop Name)]

toTyDecl :: Decl Name -> Maybe TyDecl

isTopDecl :: Decl Name -> Bool

FromDecl (TopDecl Name)

Defined in Cryptol.TypeCheck.Depends

Methods

toBind :: TopDecl Name -> Maybe (Bind Name)

toParamFun :: TopDecl Name -> Maybe (ParameterFun Name)

toParamConstraints :: TopDecl Name -> [Located (Prop Name)]

toTyDecl :: TopDecl Name -> Maybe TyDecl

isTopDecl :: TopDecl Name -> Bool

mkScc :: [(a, [Name], [Name])] -> [SCC a]

Given a list of declarations, annoted with (i) the names that they define, and (ii) the names that they use, we compute a list of strongly connected components of the declarations. The SCCs are in dependency order.

combineMaps :: [Map Name (Located a)] -> InferM (Map Name (Located a))

Combine a bunch of definitions into a single map. Here we check that each name is defined only onces.

combine :: [(Name, Located a)] -> InferM (Map Name (Located a))

Combine a bunch of definitions into a single map. Here we check that each name is defined only onces.

duplicates :: Ord a => [Located a] -> [(a, [Range])]

Identify multiple occurances of something.