| License | BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| Language | Haskell2010 |
Idris.Core.Evaluate
Contents
Description
Synopsis
- normalise :: Context -> Env -> TT Name -> TT Name
- normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
- normaliseC :: Context -> Env -> TT Name -> TT Name
- normaliseAll :: Context -> Env -> TT Name -> TT Name
- normaliseBlocking :: Context -> Env -> [Name] -> TT Name -> TT Name
- toValue :: Context -> Env -> TT Name -> Value
- quoteTerm :: Value -> TT Name
- rt_simplify :: Context -> Env -> TT Name -> TT Name
- simplify :: Context -> Env -> TT Name -> TT Name
- inlineSmall :: Context -> Env -> TT Name -> TT Name
- specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> (TT Name, [(Name, Int)])
- unfold :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
- convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool
- convEq' :: Context -> [Name] -> TT Name -> TT Name -> TC Bool
- data Def
- data CaseInfo = CaseInfo {
- case_inlinable :: Bool
- case_alwaysinline :: Bool
- tc_dictionary :: Bool
- data CaseDefs = CaseDefs {
- cases_compiletime :: !([Name], SC)
- cases_runtime :: !([Name], SC)
- data Accessibility
- type Injectivity = Bool
- data Totality
- type TTDecl = (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)
- data PReason
- = Other [Name]
- | Itself
- | NotCovering
- | NotPositive
- | UseUndef Name
- | ExternalIO
- | BelieveMe
- | Mutual [Name]
- | NotProductive
- data MetaInformation
- data Context
- initContext :: Context
- ctxtAlist :: Context -> [(Name, Def)]
- next_tvar :: Context -> Int
- addToCtxt :: Name -> Term -> Type -> Context -> Context
- setAccess :: Name -> Accessibility -> Context -> Context
- setInjective :: Name -> Injectivity -> Context -> Context
- setTotal :: Name -> Totality -> Context -> Context
- setRigCount :: Name -> RigCount -> Context -> Context
- setMetaInformation :: Name -> MetaInformation -> Context -> Context
- addCtxtDef :: Name -> Def -> Context -> Context
- addTyDecl :: Name -> NameType -> Type -> Context -> Context
- addDatatype :: Datatype Name -> Context -> Context
- addCasedef :: Name -> ErasureInfo -> CaseInfo -> Bool -> SC -> Bool -> Bool -> [(Type, Bool)] -> [Int] -> [Either Term (Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> Type -> Context -> TC Context
- simplifyCasedef :: Name -> [Name] -> [[Name]] -> ErasureInfo -> Context -> TC Context
- addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context
- lookupNames :: Name -> Context -> [Name]
- lookupTyName :: Name -> Context -> [(Name, Type)]
- lookupTyNameExact :: Name -> Context -> Maybe (Name, Type)
- lookupTy :: Name -> Context -> [Type]
- lookupTyExact :: Name -> Context -> Maybe Type
- lookupP :: Name -> Context -> [Term]
- lookupP_all :: Bool -> Bool -> Name -> Context -> [Term]
- lookupDef :: Name -> Context -> [Def]
- lookupNameDef :: Name -> Context -> [(Name, Def)]
- lookupDefExact :: Name -> Context -> Maybe Def
- lookupDefAcc :: Name -> Bool -> Context -> [(Def, Accessibility)]
- lookupDefAccExact :: Name -> Bool -> Context -> Maybe (Def, Accessibility)
- lookupVal :: Name -> Context -> [Value]
- mapDefCtxt :: (Def -> Def) -> Context -> Context
- tcReducible :: Name -> Context -> Bool
- lookupTotalAccessibility :: Name -> Context -> [(Totality, Accessibility)]
- lookupTotal :: Name -> Context -> [Totality]
- lookupTotalExact :: Name -> Context -> Maybe Totality
- lookupInjectiveExact :: Name -> Context -> Maybe Injectivity
- lookupRigCount :: Name -> Context -> [Totality]
- lookupRigCountExact :: Name -> Context -> Maybe RigCount
- lookupNameTotal :: Name -> Context -> [(Name, Totality)]
- lookupMetaInformation :: Name -> Context -> [MetaInformation]
- lookupTyEnv :: Name -> Env -> Maybe (Int, RigCount, Type)
- isTCDict :: Name -> Context -> Bool
- isCanonical :: Type -> Context -> Bool
- isDConName :: Name -> Context -> Bool
- canBeDConName :: Name -> Context -> Bool
- isTConName :: Name -> Context -> Bool
- isConName :: Name -> Context -> Bool
- isFnName :: Name -> Context -> Bool
- conGuarded :: Context -> Name -> Term -> Bool
- data Value
- class Quote a where
- initEval :: EvalState
- uniqueNameCtxt :: Context -> Name -> [Name] -> Name
- uniqueBindersCtxt :: Context -> [Name] -> TT Name -> TT Name
- definitions :: Context -> Ctxt TTDecl
- visibleDefinitions :: Context -> Ctxt TTDecl
- isUniverse :: Term -> Bool
- linearCheck :: Context -> Type -> TC ()
- linearCheckArg :: Context -> Type -> TC ()
Documentation
normaliseC :: Context -> Env -> TT Name -> TT Name Source #
Normalise fully type checked terms (so, assume all names/let bindings resolved)
normaliseAll :: Context -> Env -> TT Name -> TT Name Source #
Normalise everything, whether abstract, private or public
normaliseBlocking :: Context -> Env -> [Name] -> TT Name -> TT Name Source #
As normaliseAll, but with an explicit list of names *not* to reduce
rt_simplify :: Context -> Env -> TT Name -> TT Name Source #
Simplify for run-time (i.e. basic inlining)
simplify :: Context -> Env -> TT Name -> TT Name Source #
Like normalise, but we only reduce functions that are marked as okay to inline, and lets
inlineSmall :: Context -> Env -> TT Name -> TT Name Source #
Like simplify, but we only reduce functions that are marked as okay to inline, and don't reduce lets
unfold :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name Source #
Unfold the given names in a term, the given number of times in a stack. Preserves 'let'. This is primarily to support inlining of the given names, and can also help with partial evaluation by allowing a rescursive definition to be unfolded once only. Specifically used to unfold definitions using interfaces before going to the totality checker (otherwise mutually recursive definitions in implementations will not work...)
A definition is either a simple function (just an expression with a type), a constant, which could be a data or type constructor, an axiom or as an yet undefined function, or an Operator. An Operator is a function which explains how to reduce. A CaseOp is a function defined by a simple case tree
Constructors
| Function !Type !Term | |
| TyDecl NameType !Type | |
| Operator Type Int ([Value] -> Maybe Value) | |
| CaseOp CaseInfo !Type ![(Type, Bool)] ![Either Term (Term, Term)] ![([Name], Term, Term)] !CaseDefs |
Instances
| ToJSON Def | |||||
Defined in IRTS.Portable | |||||
| Binary Def | |||||
| NFData Def | |||||
Defined in Idris.Core.DeepSeq | |||||
| Generic Def Source # | |||||
Defined in Idris.Core.Evaluate Associated Types
| |||||
| Show Def Source # | |||||
| type Rep Def Source # | |||||
Defined in Idris.Core.Evaluate type Rep Def = D1 ('MetaData "Def" "Idris.Core.Evaluate" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" 'False) ((C1 ('MetaCons "Function" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Term)) :+: C1 ('MetaCons "TyDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameType) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Type))) :+: (C1 ('MetaCons "Operator" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ([Value] -> Maybe Value)))) :+: C1 ('MetaCons "CaseOp" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CaseInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Type, Bool)]))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Either Term (Term, Term)]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [([Name], Term, Term)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 CaseDefs)))))) | |||||
Constructors
| CaseInfo | |
Fields
| |
Instances
| ToJSON CaseInfo | |||||
Defined in IRTS.Portable Methods toEncoding :: CaseInfo -> Encoding toJSONList :: [CaseInfo] -> Value toEncodingList :: [CaseInfo] -> Encoding | |||||
| Binary CaseInfo | |||||
| NFData CaseInfo | |||||
Defined in Idris.Core.DeepSeq | |||||
| Generic CaseInfo Source # | |||||
Defined in Idris.Core.Evaluate Associated Types
| |||||
| type Rep CaseInfo Source # | |||||
Defined in Idris.Core.Evaluate type Rep CaseInfo = D1 ('MetaData "CaseInfo" "Idris.Core.Evaluate" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" 'False) (C1 ('MetaCons "CaseInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "case_inlinable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "case_alwaysinline") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "tc_dictionary") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) | |||||
Constructors
| CaseDefs | |
Fields
| |
Instances
| ToJSON CaseDefs | |||||
Defined in IRTS.Portable Methods toEncoding :: CaseDefs -> Encoding toJSONList :: [CaseDefs] -> Value toEncodingList :: [CaseDefs] -> Encoding | |||||
| Binary CaseDefs | |||||
| NFData CaseDefs | |||||
Defined in Idris.Core.DeepSeq | |||||
| Generic CaseDefs Source # | |||||
Defined in Idris.Core.Evaluate Associated Types
| |||||
| type Rep CaseDefs Source # | |||||
Defined in Idris.Core.Evaluate type Rep CaseDefs = D1 ('MetaData "CaseDefs" "Idris.Core.Evaluate" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" 'False) (C1 ('MetaCons "CaseDefs" 'PrefixI 'True) (S1 ('MetaSel ('Just "cases_compiletime") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ([Name], SC)) :*: S1 ('MetaSel ('Just "cases_runtime") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ([Name], SC)))) | |||||
data Accessibility Source #
Instances
| ToJSON Accessibility | |||||
Defined in IRTS.Portable Methods toJSON :: Accessibility -> Value toEncoding :: Accessibility -> Encoding toJSONList :: [Accessibility] -> Value toEncodingList :: [Accessibility] -> Encoding omitField :: Accessibility -> Bool | |||||
| Binary Accessibility | |||||
Defined in Idris.IBC | |||||
| NFData Accessibility | |||||
Defined in Idris.Core.DeepSeq Methods rnf :: Accessibility -> () | |||||
| Generic Accessibility Source # | |||||
Defined in Idris.Core.Evaluate Associated Types
| |||||
| Show Accessibility Source # | |||||
Defined in Idris.Core.Evaluate Methods showsPrec :: Int -> Accessibility -> ShowS show :: Accessibility -> String showList :: [Accessibility] -> ShowS | |||||
| Eq Accessibility Source # | |||||
Defined in Idris.Core.Evaluate | |||||
| Ord Accessibility Source # | |||||
Defined in Idris.Core.Evaluate Methods compare :: Accessibility -> Accessibility -> Ordering (<) :: Accessibility -> Accessibility -> Bool (<=) :: Accessibility -> Accessibility -> Bool (>) :: Accessibility -> Accessibility -> Bool (>=) :: Accessibility -> Accessibility -> Bool max :: Accessibility -> Accessibility -> Accessibility min :: Accessibility -> Accessibility -> Accessibility | |||||
| type Rep Accessibility Source # | |||||
Defined in Idris.Core.Evaluate type Rep Accessibility = D1 ('MetaData "Accessibility" "Idris.Core.Evaluate" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" 'False) ((C1 ('MetaCons "Hidden" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Public" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Frozen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Private" 'PrefixI 'False) (U1 :: Type -> Type))) | |||||
type Injectivity = Bool Source #
The result of totality checking
Constructors
| Total [Int] | well-founded arguments |
| Productive | productive |
| Partial PReason | |
| Unchecked | |
| Generated |
Instances
| ToJSON Totality | |||||
Defined in IRTS.Portable Methods toEncoding :: Totality -> Encoding toJSONList :: [Totality] -> Value toEncodingList :: [Totality] -> Encoding | |||||
| Binary Totality | |||||
| NFData Totality | |||||
Defined in Idris.Core.DeepSeq | |||||
| Generic Totality Source # | |||||
Defined in Idris.Core.Evaluate Associated Types
| |||||
| Show Totality Source # | |||||
| Eq Totality Source # | |||||
| type Rep Totality Source # | |||||
Defined in Idris.Core.Evaluate type Rep Totality = D1 ('MetaData "Totality" "Idris.Core.Evaluate" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" 'False) ((C1 ('MetaCons "Total" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int])) :+: C1 ('MetaCons "Productive" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Partial" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PReason)) :+: (C1 ('MetaCons "Unchecked" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Generated" 'PrefixI 'False) (U1 :: Type -> Type)))) | |||||
type TTDecl = (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation) Source #
Reasons why a function may not be total
Constructors
| Other [Name] | |
| Itself | |
| NotCovering | |
| NotPositive | |
| UseUndef Name | |
| ExternalIO | |
| BelieveMe | |
| Mutual [Name] | |
| NotProductive |
Instances
| Binary PReason | |||||
| NFData PReason | |||||
Defined in Idris.Core.DeepSeq | |||||
| Generic PReason Source # | |||||
Defined in Idris.Core.Evaluate Associated Types
| |||||
| Show PReason Source # | |||||
| Eq PReason Source # | |||||
| type Rep PReason Source # | |||||
Defined in Idris.Core.Evaluate type Rep PReason = D1 ('MetaData "PReason" "Idris.Core.Evaluate" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" 'False) (((C1 ('MetaCons "Other" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: C1 ('MetaCons "Itself" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NotCovering" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotPositive" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UseUndef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "ExternalIO" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BelieveMe" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Mutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: C1 ('MetaCons "NotProductive" 'PrefixI 'False) (U1 :: Type -> Type))))) | |||||
data MetaInformation Source #
Constructors
| EmptyMI | No meta-information |
| DataMI [Int] | Meta information for a data declaration with position of parameters |
Instances
| ToJSON MetaInformation | |||||
Defined in IRTS.Portable Methods toJSON :: MetaInformation -> Value toEncoding :: MetaInformation -> Encoding toJSONList :: [MetaInformation] -> Value toEncodingList :: [MetaInformation] -> Encoding omitField :: MetaInformation -> Bool | |||||
| Binary MetaInformation | |||||
Defined in Idris.IBC | |||||
| NFData MetaInformation | |||||
Defined in Idris.Core.DeepSeq Methods rnf :: MetaInformation -> () | |||||
| Generic MetaInformation Source # | |||||
Defined in Idris.Core.Evaluate Associated Types
Methods from :: MetaInformation -> Rep MetaInformation x to :: Rep MetaInformation x -> MetaInformation | |||||
| Show MetaInformation Source # | |||||
Defined in Idris.Core.Evaluate Methods showsPrec :: Int -> MetaInformation -> ShowS show :: MetaInformation -> String showList :: [MetaInformation] -> ShowS | |||||
| Eq MetaInformation Source # | |||||
Defined in Idris.Core.Evaluate Methods (==) :: MetaInformation -> MetaInformation -> Bool (/=) :: MetaInformation -> MetaInformation -> Bool | |||||
| type Rep MetaInformation Source # | |||||
Defined in Idris.Core.Evaluate type Rep MetaInformation = D1 ('MetaData "MetaInformation" "Idris.Core.Evaluate" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" 'False) (C1 ('MetaCons "EmptyMI" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DataMI" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int]))) | |||||
Contexts used for global definitions and for proof state. They contain universe constraints and existing definitions. Also store maximum RigCount of the name (can't bind a name at multiplicity 1 in a RigW, for example)
Instances
| NFData Context | |||||
Defined in Idris.Core.DeepSeq | |||||
| Generic Context Source # | |||||
Defined in Idris.Core.Evaluate Associated Types
| |||||
| Show Context Source # | |||||
| type Rep Context Source # | |||||
Defined in Idris.Core.Evaluate type Rep Context = D1 ('MetaData "Context" "Idris.Core.Evaluate" "idris-1.3.4-HnQR8FAZ4cFLBT8mcBTBaK" 'False) (C1 ('MetaCons "MkContext" 'PrefixI 'True) (S1 ('MetaSel ('Just "next_tvar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "definitions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Ctxt TTDecl)))) | |||||
initContext :: Context Source #
The initial empty context
setInjective :: Name -> Injectivity -> Context -> Context Source #
setMetaInformation :: Name -> MetaInformation -> Context -> Context Source #
addCasedef :: Name -> ErasureInfo -> CaseInfo -> Bool -> SC -> Bool -> Bool -> [(Type, Bool)] -> [Int] -> [Either Term (Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> Type -> Context -> TC Context Source #
simplifyCasedef :: Name -> [Name] -> [[Name]] -> ErasureInfo -> Context -> TC Context Source #
lookupTyName :: Name -> Context -> [(Name, Type)] Source #
Get the list of pairs of fully-qualified names and their types that match some name
lookupTyNameExact :: Name -> Context -> Maybe (Name, Type) Source #
Get the pair of a fully-qualified name and its type, if there is a unique one matching the name used as a key.
lookupTyExact :: Name -> Context -> Maybe Type Source #
Get the single type that matches some name precisely
lookupDefAcc :: Name -> Bool -> Context -> [(Def, Accessibility)] Source #
lookupDefAccExact :: Name -> Bool -> Context -> Maybe (Def, Accessibility) Source #
tcReducible :: Name -> Context -> Bool Source #
lookupTotalAccessibility :: Name -> Context -> [(Totality, Accessibility)] Source #
lookupInjectiveExact :: Name -> Context -> Maybe Injectivity Source #
lookupMetaInformation :: Name -> Context -> [MetaInformation] Source #
isCanonical :: Type -> Context -> Bool Source #
Return true if the given type is a concrete type familyor primitive False it it's a function to compute a type or a variable
isDConName :: Name -> Context -> Bool Source #
Check whether a resolved name is certainly a data constructor
canBeDConName :: Name -> Context -> Bool Source #
Check whether any overloading of a name is a data constructor
isTConName :: Name -> Context -> Bool Source #
A HOAS representation of values
Constructors
| VP NameType Name Value | |
| VV Int | |
| VBind Bool Name (Binder Value) (Value -> Eval Value) | |
| VBLet RigCount Int Name Value Value Value | |
| VApp Value Value | |
| VType UExp | |
| VUType Universe | |
| VErased | |
| VImpossible | |
| VConstant Const | |
| VProj Value Int | |
| VTmp Int |
uniqueNameCtxt :: Context -> Name -> [Name] -> Name Source #
Create a unique name given context and other existing names
isUniverse :: Term -> Bool Source #