Ivor.TT

Quickly convert a ViewTerm into a real Term. This is dangerous; you must know that typechecking will succeed, and the resulting term won't have a valid type, but you will be able to run it. This is useful if you simply want to do a substitution into a ViewTerm.

checkCtxt :: IsTerm a => Context -> Goal -> a -> TTM Term

Source

Check a term in the context of the given goal

converts :: (IsTerm a, IsTerm b) => Context -> Goal -> a -> b -> TTM Bool

Source

Check whether the conversion relation holds between two terms, in the context of the given goal

compile

Source

:: Context	context to compile
-> String	root of filenames to generate
-> IO ()
Create a .hs file containing (unreadable) Haskell code implementing all of the definitions. (TODO: Generate a more readable, usable interface)

Exported view of terms

class IsTerm a where

Source

Methods

check :: Context -> a -> TTM Term

Source

Typecheck a term

Instances

IsTerm String

IsTerm Raw

IsTerm ViewTerm

IsTerm Term

class IsData a where

Source

Methods

addData :: Context -> a -> TTM Context

Source

addDataNoElim :: Context -> a -> TTM Context

Instances

data TTError

Constructors

CantUnify ViewTerm ViewTerm
NotConvertible ViewTerm ViewTerm
Message String
Unbound ViewTerm ViewTerm ViewTerm ViewTerm [Name]
NoSuchVar Name
ErrContext String TTError

Instances

Show TTError

Error TTError

ttfail :: String -> TTM a

Source

getError :: IError -> TTError

Source

type TTM = Either TTError

Source

Definitions and Theorems

addDef :: IsTerm a => Context -> Name -> a -> TTM Context

Source

Add a new definition to the global state.

addTypedDef :: (IsTerm term, IsTerm ty) => Context -> Name -> term -> ty -> TTM Context

Source

Add a new definition, with its type to the global state. These definitions can be recursive, so use with care.

addAxiom :: IsTerm a => Context -> Name -> a -> TTM Context

Source

Add a new axiom to the global state.

declare :: IsTerm a => Context -> Name -> a -> TTM Context

Source

Declare a name which is to be defined later

declareData :: IsTerm a => Context -> Name -> a -> TTM Context

Source

Declare a type constructor which is to be defined later

theorem :: IsTerm a => Context -> Name -> a -> TTM Context

Source

Begin a new proof.

interactive :: IsTerm a => Context -> Name -> a -> TTM Context

Source

Begin a new interactive definition. Actually, just the same as theorem but this version allows you to make recursive calls, which should of course be done with care.

addPrimitive

Source

:: Context
-> Name	Type name
-> TTM Context
Add a new primitive type. This should be done in assocation with creating an instance of `ViewConst` for the type, and creating appropriate primitive functions.

addBinOp :: (ViewConst a, ViewConst b, ViewConst c, IsTerm ty) => Context -> Name -> (a -> b -> c) -> ty -> TTM Context

Source

Add a new binary operator on constants. Warning: The type you give is not checked!

addBinFn :: (ViewConst a, ViewConst b, IsTerm ty) => Context -> Name -> (a -> b -> ViewTerm) -> ty -> TTM Context

Source

Add a new binary function on constants. Warning: The type you give is not checked!

addPrimFn :: (ViewConst a, IsTerm ty) => Context -> Name -> (a -> ViewTerm) -> ty -> TTM Context

Source

Add a new primitive function on constants, usually used for converting to some form which can be examined in the type theory itself. Warning: The type you give is not checked!

addExternalFn

Source

:: IsTerm ty
=> Context
-> Name
-> Int	arity
-> [ViewTerm] -> Maybe ViewTerm	The function, which must accept a list of the right length given by arity.
-> ty
-> TTM Context
Add a new externally defined function. Warning: The type you give is not checked!

addEquality

Source

:: Context
-> Name	Name to give equality type
-> Name	Name to give constructor
-> TTM Context
Add the heterogenous ("John Major") equality rule and its reduction

forgetDef :: Context -> Name -> TTM Context

Source

Forget a definition and all following definitions.

addGenRec

Source

:: Context
-> Name	Name to give recursion rule
-> TTM Context
Add the general recursion elimination rule, thus making all further definitions untrustworthy :).

addImplicit :: Context -> ViewTerm -> (Int, ViewTerm)

Source

Add implicit binders for names used in a type, but not declared. |Returns the new type and the number of implicit names bound.

Pattern matching definitions

data PClause

Source

Constructors

PClause

arguments :: [ViewTerm]
returnval :: ViewTerm

PWithClause

arguments :: [ViewTerm]
scrutinee :: ViewTerm
patterns :: Patterns

Instances

Show PClause

data Patterns

Source

Constructors

Patterns [PClause]

Instances

Show Patterns

data PattOpt

Source

Constructors

Partial	No need to cover all cases
GenRec	No termination checking
Holey	Allow metavariables in the definition, which will become theorems which need to be proved.

Instances

Eq PattOpt

addPatternDef

Source

:: IsTerm ty
=> Context
-> Name
-> ty	Type
-> Patterns	Definition
-> [PattOpt]	Options to set which definitions will be accepted
-> TTM (Context, [(Name, ViewTerm)])
Add a new definition to the global state. By default, these definitions must cover all cases and be well-founded, but can be optionally partial or general recursive. Returns the new context, and a list of names which need to be defined to complete the definition.

toPattern :: Context -> ViewTerm -> ViewTerm

Source

Manipulating Proof State

proving :: Context -> Bool

Source

Return whether we are in the middle of proving something.

numUnsolved :: Context -> Int

Source

Get the number of unsolved goals

suspend :: Context -> Context

Source

Suspend the current proof. Clears the current proof state; use resume to continue the proof.

resume :: Context -> Name -> TTM Context

Source

Resume an unfinished proof, suspending the current one if necessary. Fails if there is no such name. Can also be used to begin a proof of an identifier previously claimed as an axiom. Remember that you will need to attack the goal if you are resuming an axiom.

save :: Context -> Context

Source

Save the state (e.g. for Undo)

restore :: Context -> TTM Context

Source

Restore a saved state; fails if none have been saved.

clearSaved :: Context -> Context

Source

Clears the saved state (e.g. if undo no longer makes sense, like when a proof has been completed)

proofterm :: Context -> TTM Term

Source

Get the current proof term, if we are in the middle of a proof.

getGoals :: Context -> [Goal]

Source

Get the goals still to be solved.

getGoal :: Context -> Goal -> TTM ([(Name, Term)], Term)

Source

Get the type and context of the given goal, if it exists

uniqueName

Source

:: Context
-> Name	Suggested name
-> TTM Name	Unique name based on suggested name
Create a name unique in the proof state

allSolved :: Context -> Bool

Source

Return whether all goals have been solved.

qed :: Context -> TTM Context

Source

Lift a finished proof into the context

Examining the Context

eval :: Context -> Term -> Term

Source

Normalise a term and its type (using old evaluator_

whnf :: Context -> Term -> Term

Source

Reduce a term and its type to Weak Head Normal Form

evalnew :: Context -> Term -> Term

Source

Reduce a term and its type to Normal Form (using new evaluator)

evalCtxt :: IsTerm a => Context -> Goal -> a -> TTM Term

Source

Evaluate a term in the context of the given goal

getDef :: Context -> Name -> TTM Term

Source

Lookup a definition in the context.

defined :: Context -> Name -> Bool

Source

Check whether a name is defined

getPatternDef :: Context -> Name -> TTM (ViewTerm, Patterns)

Source

Lookup a pattern matching definition in the context. Return the type and the pattern definition.

getAllTypes :: Context -> [(Name, Term)]

Source

Get all the names and types in the context

getAllDefs :: Context -> [(Name, Term)]

Source

getAllPatternDefs :: Context -> [(Name, (ViewTerm, Patterns))]

Source

Get all the pattern matching definitions in the context. Also returns CAFs (i.e. 0 argument functions)

getConstructors :: Context -> Name -> TTM [Name]

Source

Get the names of all of the constructors of an inductive family

getInductive :: Context -> Name -> TTM Inductive

Source

Return the data type with the given name. Note that this knows nothing about the difference between parameters and indices; that information is discarded after the elimination rule is constructed.

getAllInductives :: Context -> [(Name, Inductive)]

Source

Get all the inductive type definitions in the context.

getType :: Context -> Name -> TTM Term

Source

Get the type of a definition in the context.

data Rule

Source

Types of elimination rule

Constructors

Case
Elim

getElimRule

Source

:: Context
-> Name	Type
-> Rule	Which rule to get patterns for (case or elim)
-> TTM Patterns
Get the pattern matching elimination rule for a type

nameType :: Context -> Name -> TTM NameType

Source

Find out what type of variable the given name is

getConstructorTag :: Context -> Name -> TTM Int

Source

Get an integer tag for a constructor. Each constructor has a tag unique within the data type, which could be used by a compiler.

getConstructorArity :: Context -> Name -> TTM Int

Source

Get the arity of the given constructor.

freeze :: Context -> Name -> TTM Context

Source

Freeze a name (i.e., set it so that it does not reduce) Fails if the name does not exist.

thaw :: Context -> Name -> TTM Context

Source

Unfreeze a name (i.e., allow it to reduce). Fails if the name does not exist.

Goals, tactic types

data Goal

Source

Abstract type representing goal or subgoal names.

Instances

Eq Goal

Show Goal

goal :: String -> Goal

Source

defaultGoal :: Goal

Source

type Tactic = Goal -> Context -> TTM Context

Source

A tactic is any function which manipulates a term at the given goal binding. Tactics may fail, hence the monad.

data GoalData

Source

Environment and goal type for a given subgoal

bindings :: GoalData -> [(Name, Term)]

Source

Get the premises of the goal

goalName :: GoalData -> Goal

Source

Get the name of the goal

goalType :: GoalData -> Term

Source

Get the type of the goal

goalData

Source

:: Context
-> Bool	Get all bindings (True), or just lambda bindings (False)
-> Goal
-> TTM GoalData
Get information about a subgoal.

subGoals :: Context -> TTM [(Name, Term)]

Source

Get the names and types of all goals

Primitive Tactics

Basics

intro :: Tactic

Source

Introduce an assumption (i.e. a lambda binding)

introName

Source

:: Name	Name for the assumption
-> Tactic
Introduce an assumption (i.e. a lambda binding)

intros :: Tactic

Source

Keep introducing things until there's nothing left to introduce.

intros1 :: Tactic

Source

Keep introducing things until there's nothing left to introduce, Must introduce at least one thing.

introsNames :: [Name] -> Tactic

Source

As intros, but with names, and stop when we've run out of names. Fails if too many names are given.

addArg :: IsTerm a => Name -> a -> Tactic

Source

Add a new top level argument after the arguments its type depends on (changing the type of the theorem). This can be useful if, for example, you find you need an extra premise to prove a goal.

generalise :: IsTerm a => a -> Tactic

Source

Abstract over the given term in the goal.

dependentGeneralise :: IsTerm a => a -> Tactic

Source

Abstract over the given term in the goal, and also all variables appearing in the goal whose types depend on it.

claim :: IsTerm a => Name -> a -> Tactic

Source

Make a local claim

Proof navigation

focus :: Tactic

Source

Focus on a different hole, i.e. set the default goal.

rename :: Name -> Tactic

Source

Rename the outermost binder in the given goal

attack :: Tactic

Source

Prepare a goal for introduction.

attackWith

Source

:: Name	Name for new goal
-> Tactic
Prepare a goal for introduction.

solve :: Tactic

Source

Finalise a goal's solution.

trySolve :: Tactic

Source

If the goal has a solution, finalise it, otherwise prepare the goal (with attack). Typically, could be used on the subgoals generated by refinement, where some may have solutions attached already, and others will need to be prepared.

keepSolving :: Tactic

Source

Finalise as many solutions of as many goals as possible.

abandon :: Tactic

Source

Remove a solution from a goal.

hide :: Tactic

Source

Hide a premise

Introductions

fill :: IsTerm a => a -> Tactic

Source

Attach a solution to a goal.

refine :: IsTerm a => a -> Tactic

Source

Solve a goal by applying a function. If the term given has arguments, attempts to fill in these arguments by unification and solves them (with solve). See refineWith and basicRefine for slight variations.

basicRefine :: IsTerm a => a -> Tactic

Source

Solve a goal by applying a function. If the term given has arguments, this will create a subgoal for each. Some arguments may be solved by unification, in which case they will already have a guess attached after refinement, but the guess will not be solved (via solve).

refineWith :: IsTerm a => a -> [a] -> Tactic

Source

Solve a goal by applying a function with some arguments filled in. See refine for details.

trivial :: Tactic

Source

Find a trivial solution to the goal by searching through the context for a premise which solves it immediately by refinement

axiomatise

Source

:: Name	Name to give axiom
-> [Name]	Premises to pass to axiom
-> Tactic
Add an axiom to the global context which would solve the goal, and apply it. FIXME: This tactic doesn't pick up all dependencies on types, but is okay for simply typed axioms, e.g. equations on Nats.

Eliminations

Source

:: IsTerm a
=> a	An elimination rule applied to a target.
-> Tactic
Apply an eliminator.

induction

Source

:: IsTerm a
=> a	target of the elimination
-> Tactic
Apply the appropriate induction rule to the term.

cases

Source

:: IsTerm a
=> a	target of the case analysis
-> Tactic
Apply the appropriate case analysis rule to the term. Like `induction`, but no induction hypotheses generated.

Conversions

equiv :: IsTerm a => a -> Tactic

Source

Check that the goal is definitionally equal to the given term, and rewrite the goal accordingly.

compute :: Tactic

Source

Normalise the goal

beta :: Tactic

Source

Beta reduce in the goal

unfold :: Name -> Tactic

Source

Beta reduce the goal, unfolding the given function

Equality

replace

Source

:: (IsTerm a, IsTerm b, IsTerm c, IsTerm d)
=> a	Equality type (e.g. `Eq : (A:)(a:A)(b:A)`)
-> b	replacement lemma (e.g. `repl : (A:)(a:A)(b:A)(q:Eq _ a b)(P:(a:A))(p:P a)(P b)`)
-> c	symmetry lemma (e.g. `sym : (A:*)(a:A)(b:A)(p:Eq _ a b)(Eq _ b a)`)
-> d	equality premise
-> Bool	apply premise backwards (i.e. apply symmetry)
-> Tactic
Replace a term in the goal according to an equality premise. Any equality type with three arguments is acceptable (i.e. the type, and the two values), provided there are suitable replacement and symmetry lemmas. Heterogeneous equality as provided by `addEquality` is acceptable (if you provide the lemmas!).