ivor-0.1.8: Theorem proving library based on dependent type theorySource codeContentsIndex
Ivor.ViewTerm
Portabilitynon-portable
Stabilityexperimental
Maintainereb@dcs.st-and.ac.uk
Contents
Variable names
Terms
Inductive types
Description
Exported view of terms and inductive data structures; imported implicitly by Ivor.TT.
Synopsis
data Name
name :: String -> Name
displayName :: Name -> String
data NameType
= Bound
| Free
| DataCon
| TypeCon
| ElimOp
| Unknown
mkVar :: String -> ViewTerm
newtype Term = Term (Indexed Name, Indexed Name)
data ViewTerm
= Name {
nametype :: NameType
var :: Name
}
| App {
fun :: ViewTerm
arg :: ViewTerm
}
| Lambda {
var :: Name
vartype :: ViewTerm
scope :: ViewTerm
}
| Forall {
var :: Name
vartype :: ViewTerm
scope :: ViewTerm
}
| Let {
var :: Name
vartype :: ViewTerm
varval :: ViewTerm
scope :: ViewTerm
}
| Label {
fname :: Name
fargs :: [ViewTerm]
labeltype :: ViewTerm
}
| Call {
fname :: Name
fargs :: [ViewTerm]
callterm :: ViewTerm
}
| Return {
returnterm :: ViewTerm
}
| forall c . Constant c => Constant c
| Star
| Quote {
quotedterm :: ViewTerm
}
| Code {
codetype :: ViewTerm
}
| Eval {
evalterm :: ViewTerm
}
| Escape {
escapedterm :: ViewTerm
}
| Placeholder
| Metavar {
var :: Name
}
apply :: ViewTerm -> [ViewTerm] -> ViewTerm
view :: Term -> ViewTerm
viewType :: Term -> ViewTerm
class (Typeable c, Show c, Eq c) => ViewConst c where
typeof :: c -> Name
freeIn :: Name -> ViewTerm -> Bool
namesIn :: ViewTerm -> [Name]
occursIn :: ViewTerm -> ViewTerm -> Bool
subst :: Name -> ViewTerm -> ViewTerm -> ViewTerm
getApp :: ViewTerm -> ViewTerm
getFnArgs :: ViewTerm -> [ViewTerm]
getArgTypes :: ViewTerm -> [(Name, ViewTerm)]
getReturnType :: ViewTerm -> ViewTerm
dbgshow
data Inductive = Inductive {
typecon :: Name
parameters :: [(Name, ViewTerm)]
indices :: [(Name, ViewTerm)]
contype :: ViewTerm
constructors :: [(Name, ViewTerm)]
}
Variable names
data Name Source
show/hide Instances
name :: String -> NameSource
displayName :: Name -> StringSource
data NameType Source
Categories for names; typechecked terms will know what each variable is for.
Constructors
Bound
Free
DataCon
TypeCon
ElimOp
UnknownUse for sending to typechecker.
show/hide Instances
mkVarSource
:: StringVariable name
-> ViewTerm
Construct a term representing a variable
Terms
newtype Term Source
Abstract type representing a TT term and its type.
Constructors
Term (Indexed Name, Indexed Name)
show/hide Instances
data ViewTerm Source
Constructors
Name
nametype :: NameType
var :: Name
App
fun :: ViewTerm
arg :: ViewTerm
Lambda
var :: Name
vartype :: ViewTerm
scope :: ViewTerm
Forall
var :: Name
vartype :: ViewTerm
scope :: ViewTerm
Let
var :: Name
vartype :: ViewTerm
varval :: ViewTerm
scope :: ViewTerm
Label
fname :: Name
fargs :: [ViewTerm]
labeltype :: ViewTerm
Call
fname :: Name
fargs :: [ViewTerm]
callterm :: ViewTerm
Return
returnterm :: ViewTerm
forall c . Constant c => Constant c
Star
QuoteStaging annotation
quotedterm :: ViewTerm
CodeStaging annotation
codetype :: ViewTerm
EvalStaging annotation
evalterm :: ViewTerm
EscapeStaging annotation
escapedterm :: ViewTerm
Placeholder
Metavar
var :: Name
show/hide Instances
apply :: ViewTerm -> [ViewTerm] -> ViewTermSource
Make an application of a function to several arguments
view :: Term -> ViewTermSource
Get a pattern matchable representation of a term.
viewType :: Term -> ViewTermSource
Get a pattern matchable representation of a term's type.
class (Typeable c, Show c, Eq c) => ViewConst c whereSource
Haskell types which can be used as constants
Methods
typeof :: c -> NameSource
show/hide Instances
freeIn :: Name -> ViewTerm -> BoolSource
Return whether the name occurs free in the term.
namesIn :: ViewTerm -> [Name]Source
Return the names occurring free in a term
occursIn :: ViewTerm -> ViewTerm -> BoolSource
Return whether a subterm occurs in a (first order) term.
subst :: Name -> ViewTerm -> ViewTerm -> ViewTermSource
Substitute a name n with a value v in a term f
getApp :: ViewTerm -> ViewTermSource
Get the function from an application. If no application, returns the entire term.
getFnArgs :: ViewTerm -> [ViewTerm]Source
Get the arguments from a function application.
getArgTypes :: ViewTerm -> [(Name, ViewTerm)]Source
Get the argument names and types from a function type
getReturnType :: ViewTerm -> ViewTermSource
Get the return type from a function type
dbgshow
Inductive types
data Inductive Source
Constructors
Inductive
typecon :: Name
parameters :: [(Name, ViewTerm)]
indices :: [(Name, ViewTerm)]
contype :: ViewTerm
constructors :: [(Name, ViewTerm)]
show/hide Instances
Produced by Haddock version 2.4.2