ivor-0.1.9: Theorem proving library based on dependent type theory Source code Contents Index

Ivor.ViewTerm Portability non-portable Stability experimental Maintainer eb@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] 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

Instances Eq Name Ord Name Show Name Typeable Name Forget Name String

name :: String -> Name Source

displayName :: Name -> String Source

data NameType Source

Categories for names; typechecked terms will know what each variable is for. Constructors Bound Free DataCon TypeCon ElimOp Unknown Use for sending to typechecker. Instances Show NameType

mkVar Source

:: String Variable 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) Instances Show Term IsTerm Term

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 Quote Staging annotation quotedterm :: ViewTerm Code Staging annotation codetype :: ViewTerm Eval Staging annotation evalterm :: ViewTerm Escape Staging annotation escapedterm :: ViewTerm Placeholder Annotation additional annotations annotation :: Annot term :: ViewTerm Metavar var :: Name Instances Eq ViewTerm Show ViewTerm IsTerm ViewTerm Forget ViewTerm Raw

data Annot Source

Constructors FileLoc FilePath Int source file, line number

apply :: ViewTerm -> [ViewTerm] -> ViewTerm Source

Make an application of a function to several arguments

view :: Term -> ViewTerm Source

Get a pattern matchable representation of a term.

viewType :: Term -> ViewTerm Source

Get a pattern matchable representation of a term's type.

class (Typeable c, Show c, Eq c) => ViewConst c where Source

Haskell types which can be used as constants Methods typeof :: c -> Name Source Instances ViewConst Double ViewConst Int ViewConst String

freeIn :: Name -> ViewTerm -> Bool Source

Return whether the name occurs free in the term.

namesIn :: ViewTerm -> [Name] Source

Return the names occurring free in a term

occursIn :: ViewTerm -> ViewTerm -> Bool Source

Return whether a subterm occurs in a (first order) term.

subst :: Name -> ViewTerm -> ViewTerm -> ViewTerm Source

Substitute a name n with a value v in a term f

getApp :: ViewTerm -> ViewTerm Source

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 -> ViewTerm Source

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)] Instances Show Inductive IsData Inductive Forget Inductive String

Produced by Haddock version 2.4.2