ivor-0.1.11: 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
| Annotation {
annotation :: Annot
term :: ViewTerm
}
| Metavar {
var :: Name
}
data Annot = FileLoc FilePath Int
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]
transform :: ViewTerm -> ViewTerm -> ViewTerm -> ViewTerm
getArgTypes :: ViewTerm -> [(Name, ViewTerm)]
getReturnType :: ViewTerm -> ViewTerm
dbgshow :: Name -> [Char]
data Inductive = Inductive {
typecon :: Name
parameters :: [(Name, ViewTerm)]
indices :: [(Name, ViewTerm)]
contype :: ViewTerm
constructors :: [(Name, ViewTerm)]
}
Variable names
data Name Source
show/hide Instances
Eq Name
Ord Name
Show Name
Typeable Name
Binary Name
Forget Name String
Forget Normal (TT Name)
Weak (TT Name)
Show Name => Forget (TT Name) Raw
Forget (Bind (Model Scope)) (Bind (TT Name))
Forget (Binder (Model Scope)) (Binder (TT Name))
Forget (MComp Scope) (Computation Name)
Forget (Blocked Scope) (TT Name)
Forget (Ready Scope) (TT Name)
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
Annotationadditional annotations
annotation :: Annot
term :: ViewTerm
Metavar
var :: Name
show/hide Instances
data Annot Source
Constructors
FileLoc FilePath Intsource file, line number
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.
transformSource
:: ViewTermLeft hand side, with metavariables
-> ViewTermRight hand side, with metavariables
-> ViewTermTerm to rewrite
-> ViewTerm
Transform a term according to a rewrite rule.
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 :: Name -> [Char]Source
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.6.0