Istari includes a library Case that supplies a convenient mechanism
to case-analyzing terms and other forms in the logic.
Suppose we wish to case-analyze the current goal’s conclusion, and
isolate the cases where it is forall, ->, or anything else. The
forall constant is just forall and it takes two arguments: a type
(the domain), and a function returning a type (the codomain). The
-> constant is arrow and it takes two types as arguments.
Then we write:
goalCaseT
/| forall ? (fn . ?) =>
\(fnc dom cod => ... do the forall thing ...)\
| arrow ? ? =>
\(fnc dom cod => ... do the arrow thing ...)\
| _ =>
\(fnc => ... do the catch-all thing ...)\
/
This consists of three clauses, separated by |. In each clause we
typically give a pattern, then =>, then code for that case.
Consider the first clause. It matches against forall applies to two
arguments. The first argument (?) matches anything, and produces a
binding. The second argument (fn . ?) matches only lambda, but the
lambda’s body (again ?) may take any form, and produces a second
binding.
The => serves to attach code to that pattern. The code is
antiquoted IML code. The parentheses within the
antiquote are not necessary but are good style. (Also, Emacs is
happier with them present.) The IML code uses the fnc
form which takes an
iterated pair as its argument. The arguments are the bindings
produced by ? in the pattern, in the order they appeared.
The second clause is similar but simpler. The third clause is simpler
still, but illustrates the wildcard pattern (_), which matches
anything but does not produce a binding.
Note that goalCaseT and its cousins do not perform a tail-call
optimization. Also, they do not build decision trees; they
simply try each clause in order. This is usually acceptable, but if
performance is critical one may need to use primitive ML case analysis
instead of Case.
We can also case-analyze the contents of the context, instead of the
conclusion. Suppose we wish to find any ordinary hypothesis whose
type is forall or ->. Then we write:
goalContextCaseT
/| $tm forall ? (fn . ?) =>
\(fnc hyp dom cod => ... do the forall thing ...)\
| $tm arrow ? ? =>
\(fnc hyp dom cod => ... do the arrow thing ...)\
/
The $tm combinator indicates to match an ordinary (non-future,
non-hidden, term) hypothesis. The attached function’s first argument
(hyp here) is the name of the hypothesis that was matched, while the
remaining arguments (dom and cod here) are generated by the
pattern matching.
Note that including a catch-all in a context matcher would probably
not work as intended, since the first hypothesis tested would match
the catch-all and no further hypotheses would be tested. If one
wanted to provide a tactic to run when no hypotheses match the
pattern, one could place the case analysis within a call to the
first combinator.
There are many entry points into the case-analysis mechanism. A few of the most important are:
goalCaseT /[term matcher]/
Matches against the current goal’s conclusion and returns a tactic, which is applied to that goal. Once it matches the conclusion and determines the tactic, it does not backtrack into other clauses, even if the tactic fails or some subsequent tactic fails.
goalCaseB /[term matcher]/
Like goalCaseT, but it will backtrack into other clauses if the
tactic fails, or if some subsequent tactic fails.
termCaseT /[term]/ /[term matcher]/
Like goalCaseT, but matches on a given term rather than the current
goal’s conclusion.
termCaseB /[term]/ /[term matcher]/
Like goalCaseB, but matches on a given term rather than the
current goal’s conclusion.
termCase /[term]/ /[term matcher]/
Like termCaseT but the result can have any type. If no clauses
apply, termCase raises the NoMatch exception.
goalContextCaseT /[hyp matcher]/
Matches against some hypothesis from the current goal and returns a
tactic, which is applied to that goal. The hypothesis is shifted
into the scope of the full context before matching. That is,
hypothesis i is shifted by i+1. The name of the hypothesis
that was matched is passed as the first binding.
goalContextCaseB /[hyp matcher]/
Like goalContextCaseT, but it will backtrack into other clauses if
the tactic fails, or if some subsequent tactic fails.
allGoalContextCase /[hyp matcher]/ [continuation]
Matches against all hypotheses and passes, to its continuation, a
list containing the result from all successful matches. The
matching process works as in goalContextCaseT. The continuation
must return a tactic.
The Case mechanism consists of collection of matching combinators, a
collection of entry points, and a parser that makes those combinators
nicer to read and write.
The central type is an ('a, 'b, 'c) matcher. In this, 'a is the
type being matched, 'b is the type of all the bindings we have
collected already, and 'c is the type of the result.
The most important combinators are:
val wild : ('a, 'b, 'b) matcher
val what : ('a, 'b, 'b * 'a) matcher
val wrap : ('a, 'b, 'c) matcher -> ('c -> 'd) -> ('a, 'b, 'd) matcher
val alt : ('a, 'b, 'c) matcher list -> ('a, 'b, 'c) matcher
wild matches 'a but generates no bindings, so it returns the
same type as the bindings collected so far ('b). In the parser
wild is written _.
what matches 'a and adds it to the end of the bindings collected
so far, turning 'b into 'b * 'a. In the parser, what is
written ?.
wrap m f (where m and f have the types given above) defers to
m to match 'a, and hands m the bindings collected so far (of
type 'b). When m returns a result of type 'c, wrap calls
f to obtain a result of type d, which it returns. In the
parser, wrap m f is written m => f.
Note that successive uses of what will result in an
left-associated iterated pair, making IML’s fnc
form appropriate for
f.
alt [m1, ..., mn] tries each matcher mi in turn. In the parser,
it is written m1 | ... | mn. (An additional leading | is
optional.)
val constant : Term.constant -> (term, 'a, 'a) matcher
val variable : int -> (term, 'a, 'a) matcher
val whatConstant : (term, 'a, 'a * Term.constant) matcher
val whatVar : (term, 'a, 'a * int) matcher
val whatEvar : (term, 'a, 'a * (Term.ebind * Term.sub)) matcher
constant [const c] matches c, producing no bindings. In the
parser, this is written as the name of the constant, or using an
antiquoted expression of type constant.
variable [number n] matches the variable with index n, producing
no bindings.
whatConstant matches any constant, producing a binding to that
constant. In the parser it is written const?.
whatVar matches any variable, producing a binding to its index.
In the parser it is written var?.
whatEvar matches any evar, producing a binding to its ebind and
substitution. In the parser it is written evar?.
val elim : (term, 'a, 'b) matcher -> (spine, 'b, 'c) matcher -> (term, 'a, 'c) matcher
val lam : (term, 'a, 'b) matcher -> (term, 'a, 'b) matcher
val lamb : (term, 'a * Term.binder, 'b) matcher -> (term, 'a, 'b) matcher
val pair : (term, 'a, 'b) matcher -> (term, 'b, 'c) matcher -> (term, 'a, 'c) matcher
val next : (term, 'a, 'b) matcher -> (term, 'a, 'b) matcher
val triv : (term, 'a, 'a) matcher
val marker : Symbol.symbol -> (term, 'a, 'a) matcher
val nat : (term, 'a, 'a * int) matcher
val integer : (term, 'a, 'a * IntInf.int) matcher
elim m1 m2 matches an elimination form; m1 matches against the
head and m2 matches against the
spine. In the parser it is
written m1 @ m2.
lam m matches a lambda; m matches against the body. In the
parser it is written fn . m.
lamb m also matches a lambda. First a binding is producer for the
lambda’s binder, then m matches against the body. In the parser
it is written fn ? . m.
pair m1 m2 matches a pair; m1 matches against the left
constituent and m2 against the right. In the parser it is written
(m1 , m2). The parser also accepts a tuple longer than two, which
is interpreted as a right-associated iterated pair.
next m matches a future intro; m matches against the body. In
the parser it is written next m.
triv matches against the () term, producing no bindings. In the
parser it is written ().
marker sym matches against a marker term carrying sym, producing
no bindings. Normally sym is the empty symbol. In the parser it
is written $marker \ sym \.
nat matches against natural number literals, producing a binding
of the corresponding int. In the parser it is written nat?.
integer matches against integer literals, producing a binding of
the corresponding integer. In the parser it is written integer?.
val unify : term -> (term, 'a, 'a) matcher
val whnf : (term, 'a, 'b) matcher -> (term, 'a, 'b) matcher
val whnfHard : (term, 'a, 'b) matcher -> (term, 'a, 'b) matcher
val whnfBasic : (term, 'a, 'b) matcher -> (term, 'a, 'b) matcher
unify t matches against any term that unifies with t, producing
no bindings. In the parser it is written $unify \ ... antiquoted
internal term ... \.
whnf m weak-head normalizes the term being matched before passing
it to m. In the parser it is written $whnf m.
whnfHard m hard weak-head normalizes the term being matched before
passing it to m. In the parser it is written $whnfHard m.
whnfBasic m basic weak-head normalizes the term being matched before
passing it to m. In the parser it is written $whnfBasic m.
val null : (spine, 'a, 'a) matcher
val app : (term, 'a, 'b) matcher -> (spine, 'b, 'c) matcher -> (spine, 'a, 'c) matcher
val pi1 : (spine, 'a, 'b) matcher -> (spine, 'a, 'b) matcher
val pi2 : (spine, 'a, 'b) matcher -> (spine, 'a, 'b) matcher
val prev : (spine, 'a, 'b) matcher -> (spine, 'a, 'b) matcher
null matches against the empty spine, producing no bindings.
In the parser it is written $nil.
app m1 m2 matches against a spine that begins with application;
m1 matches against the argument, and m2 matches against the rest
of the spine. In the parser it is written $ap m1 m2.
pi1 m matches against a spine that begins with #1; m matches
against the rest of the spine. In the parser it is written #1 m.
pi2 m matches against a spine that begins with #2; m matches
against the rest of the spine. In the parser it is written #2 m.
prev m matches against a spine that begins with #prev; m
matches against the rest of the spine. In the parser it is written
#prev m.
Suppose you want to match arrow applied to two arguments. In IML
syntax you would use the combinators thus:
elim (const (parseConstant /arrow/)) (app what (app what null))
In the parser, you can write it in three different ways. One is to transliterate the above:
arrow @ $ap ? $ap ? $nil
But this pattern (a constant applied to a spine of known length) is so common that there is an abbreviated syntax:
arrow ? ?
(Compare this with the example at the top of the page.) In the
abbreviated syntax, we can also replace the head constant’s name with
an antiquoted expression of type const:
\(parseConstant /arrow/)\ ? ?
One typically would use this form when the head constant varies.
There is one matching combinator for each sort of hypothesis:
val tm : (term, 'a, 'b) matcher -> (hyp, 'a, 'b) matcher
val tml : (term, 'a, 'b) matcher -> (hyp, 'a, 'b) matcher
val tmh : (term, 'a, 'b) matcher -> (hyp, 'a, 'b) matcher
val tp : (hyp, 'a, 'a) matcher
val tpl : (hyp, 'a, 'a) matcher
val lett : (term, 'a, 'b) matcher -> (hyp, 'a, 'b) matcher
In the parser they are written $tm, $tml, $tmh, $tp, $tpl,
$let.
In all the entry points that match a hypothesis extracted from a
context (i.e., contextCase, contextnCase, contextCaseT,
contextnCaseT, goalHypCaseT, goalContextCaseT,
goalContextnCaseT, contextCaseB, contextnCaseB, goalHypCaseB,
goalContextCaseB, goalContextnCaseB, allContextCase, and
allGoalContextCase), the hypothesis is shifted into the scope of the
full context before matching. That is, hypothesis i is shifted by
i+1.
In the entry points that mention context, the name of the
hypothesis that was matched is passed as the first binding. In the
entry points that mention contextn, the number of the hypothesis
that was matched is passed as the first binding.
val az : ('a, 'b * 'a, 'c) matcher -> ('a, 'b, 'c) matcher
val cond : ('a, 'b, 'c option) matcher -> ('a, 'b, 'c) matcher
val tri : ('a -> 'b) -> ('a -> 'b option)
val wrapk : ('a, 'b, 'c) matcher -> ('c -> 'd) -> ('a, 'b, 'd) matcher
val seq : ('a, 'c, 'd) matcher -> ('b, 'd, 'e) matcher -> ('a * 'b, 'c, 'e) matcher
az m is like an as pattern in ML. It produces a binding for the
whole item, but it also passes the whole item to a sub-matcher m
for additional matching. The az binding takes place before the
additional matching, so the 'b bindings collected already become
'b * 'a when they are handed to m. In the parser, az m is
written $as m. ($az m is also accepted.)
cond m calls the sub-matcher m. If m returns SOME v then
cond m returns v. If m returns NONE, then cond backtracks
to the next applicable clause.
tri m (“try”) calls the sub-matcher m. If m returns v then
tri m returns SOME v. If m raises Backtrack then tri m
returns NONE.
wrapk m f is like wrap m f, but if the wrapper f raises the
Backtrack exception, wrapk backtracks to the next applicable
clause. Equivalent to cond (wrap m (tri f)). In the parser,
wrapk m f is written m =!> f.
seq m1 m2 matches on a pair of type 'a * 'b. The left-hand
component is sent to m1, then the right to m2. In the parser,
seq m1 m2 is written m1 ; m2.
val frame : ('a, unit, 'c) matcher -> ('a, 'b, 'b * 'c) matcher
val fix : (('a, unit, 'b) matcher -> ('a, unit, 'b) matcher) -> ('a, unit, 'b) matcher
The fix combinator enables recursive matching, it returns the fixed
point of the function given as its argument. To understand its use,
consider the two types:
('a, unit, 'c) matcher
('a, 'b, 'b * 'c) matcher
These types are isomorphic: they both represent a matcher that matches
against 'a, producing 'c. The frame combinator coerces the
former to the latter. (The other direction is not often required, but
can be accomplished by instantiating 'b to unit and then wrapping.)
To use fix, you would write something like (with types added for
clarity):
frame (fix (fn m => ... body ...))
where the body calls frame m when it needs to call the matcher
recursively. If the recursive matcher is not part of the a larger
matcher, the outer frame might be omitted.
Here m is assumed to have type (S, unit, T) matcher, so frame m
has the type (S, 'b, 'b * T) matcher. The body has type
(S, unit, T) matcher. (It will need to use a wrapper to get its
result back to T.) Thus, the fix also has that type. Finally, the
outer frame has the type (S, 'b, 'b * T).
In the parser, these combinators must be used with the $lit syntax.
Thus frame m is written $lit \frame m\, and frame (fix f) is
written $lit \frame (fix f)\.
The full collection of entry points is:
(* Returns arbitrary type, raises NoMatch when matching fails. *)
val termCase : term -> (term, unit, 'a) matcher -> 'a
val unitCase : (unit, unit, 'a) matcher -> 'a
val term2Case : term -> term -> (term * term, unit, 'a) matcher -> 'a
val term3Case : term -> term -> term -> (term * (term * term), unit, 'a) matcher -> 'a
val spineCase : spine -> (spine, unit, 'a) matcher -> 'a
val hypCase : hyp -> (hyp, unit, 'a) matcher -> 'a
val contextCase : context -> Directory.directory -> (context, unit * Symbol.symbol, 'a) matcher -> 'a
val contextnCase : context -> (context, unit * int, 'a) matcher -> 'a
(* Returns a tactic. Backtracks when matching fails. Will not try other
matches when the resulting tactic or subsequent tactics fail. *)
val termCaseT : term -> (term, unit, 'a tacticm) matcher -> 'a tacticm
val unitCaseT : (unit, unit, 'a tacticm) matcher -> 'a tacticm
val term2CaseT : term -> term -> (term * term, unit, 'a tacticm) matcher -> 'a tacticm
val term3CaseT : term -> term -> term -> (term * term * term, unit, 'a tacticm) matcher -> 'a tacticm
val spineCaseT : spine -> (spine, unit, 'a tacticm) matcher -> 'a tacticm
val hypCaseT : hyp -> (hyp, unit, 'a tacticm) matcher -> 'a tacticm
val contextCaseT : context -> Directory.directory -> (context, unit * Symbol.symbol, 'a tacticm) matcher -> 'a tacticm
val contextnCaseT : context -> (context, unit * int, 'a tacticm) matcher -> 'a tacticm
val goalCaseT : (term, unit, 'a tacticm) matcher -> 'a tacticm
val goalHypCaseT : int -> (hyp, unit, 'a tacticm) matcher -> 'a tacticm
val goalContextCaseT : (context, unit * Symbol.symbol, 'a tacticm) matcher -> 'a tacticm
val goalContextnCaseT : (context, unit * int, 'a tacticm) matcher -> 'a tacticm
(* Returns a tactic. Backtracks when matching fails. Tries other matches
when the resulting tactic or a subsequent tactic fails. *)
val termCaseB : term -> (term, unit, 'a tacticm) matcher -> 'a tacticm
val unitCaseB : (unit, unit, 'a tacticm) matcher -> 'a tacticm
val term2CaseB : term -> term -> (term * term, unit, 'a tacticm) matcher -> 'a tacticm
val term3CaseB : term -> term -> term -> (term * term * term, unit, 'a tacticm) matcher -> 'a tacticm
val spineCaseB : spine -> (spine, unit, 'a tacticm) matcher -> 'a tacticm
val hypCaseB : hyp -> (hyp, unit, 'a tacticm) matcher -> 'a tacticm
val contextCaseB : context -> Directory.directory -> (context, unit * Symbol.symbol, 'a tacticm) matcher -> 'a tacticm
val contextnCaseB : context -> (context, unit * int, 'a tacticm) matcher -> 'a tacticm
val goalCaseB : (term, unit, 'a tacticm) matcher -> 'a tacticm
val goalHypCaseB : int -> (hyp, unit, 'a tacticm) matcher -> 'a tacticm
val goalContextCaseB : (context, unit * Symbol.symbol, 'a tacticm) matcher -> 'a tacticm
val goalContextnCaseB : (context, unit * int, 'a tacticm) matcher -> 'a tacticm
(* Returns (or passes to its continuation) a list containing the results for all
matching hypotheses. Will not fail. Will not try other matches if subsequent
tactics fail.
*)
val allContextCase : context -> Directory.directory -> (hyp, unit * Symbol.symbol, 'a) matcher -> 'a list
val allGoalContextCase : (hyp, unit * Symbol.symbol, 'a) matcher -> ('a list -> 'b tacticm) -> 'b tacticm
The grammar for matchers is as follows. Capitalized words are nonterminals; lower case words are keywords.
Forms are listed in increasing order of precedence. Grouped forms
have the same precedence. A subterm at the same level of precedence
is given in brackets. For example, Match ; [Match] indicates that
seq is right associative.
Match ::=
Match | ... | Match (alt, length at least 2)
| Match | ... | Match (alt, length at least 2)
Match ; [Match] (seq)
Match => \ ... antiquoted function ... \ (wrap)
Match =!> \ ... antiquoted function ... \ (wrapk)
$lit \ ... antiquoted matcher ... \
$as [Match] (az)
$az [Match] (az)
---------------- terms ----------------
Match @ [Match] (elim)
Constant Spine (elim/constant, nonempty spine)
\ ... antiquoted constant ... \ Spine (elim/constant, nonempty spine)
$var \ ... antiquoted index ... \ Spine (elim/var, nonempty spine)
fn . [Match] (lam)
fn ? . [Match] (lamb)
next [Match] (next)
$marker \ ... antiquoted symbol ... \ (marker)
$unify \ ... antiquoted term ... \ (unify)
$whnf [Match] (whnf)
$whnfHard [Match] (whnfHard)
$whnfBasic [Match] (whnfBasic)
---------------- spines ----------------
$nil (null)
$ap Match [Match] (app)
#1 [Match] (pi1)
#2 [Match] (pi2)
#prev [Match] (prev)
---------------- hypotheses ----------------
$tm [Match] (tm)
$tml [Match] (tml)
$tmh [Match] (tmh)
$tp [Match] (tp)
$tpl [Match] (tpl)
$let [Match] (lett)
( Match )
_ (wild)
? (what)
() (triv)
---------------- terms ----------------
Constant (constant)
\ ... antiquoted constant ... \ (constant)
$var \ ... antiquoted index ... \ (variable)
const? (whatConstant)
var? (whatVar)
evar? (whatEvar)
nat? (nat)
integer? (integer)
( Match , ... , Match ) (pair, length at least 2)
Spine ::=
(null)
Match [Spine] (app)
#1 [Spine] (pi1)
#2 [Spine] (pi2)
#prev [Spine] (prev)
Note that a path can be matched in two different ways: the simple form
Constant Spine, or the general form Constant @ Match where Match
matches the spine. (Variable-headed paths are similar.) The
simple form is usually more convenient, but unlike the general form,
it provides no facility to bind a variable to the spine itself (or a
suffix of it); it can only bind to the applicands. The simple form
also provides no facility for matching an unknown head.
One can parse a matcher using parseMatch, which is actually the
identity function, but IML is instructed to parse its argument using
the Match grammar. For example, one might write a recursive
matcher:
$lit \frame (fix (fn x => parseMatch / ... body ... /))\