Istari

Case analysis

Istari includes a library Case that supplies a convenient mechanism to case-analyzing terms and other forms in the logic.

An example

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.

Performance note

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.

A context example

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.

Entry points

There are many entry points into the case-analysis mechanism. A few of the most important are:

Details

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
Matching term heads
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
Matching terms
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 whatNat     : (term, 'a, 'a * int) matcher
val whatInteger : (term, 'a, 'a * IntInf.int) matcher
val whatSymbol  : (term, 'a, 'a * Symbol.symbol) matcher
Other term combinators
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
Matching spines
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

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.

Matching hypotheses

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.

Matching within contexts

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.

Other generic combinators
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
Recursive matching
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)\.

Entry points

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 matcher grammar

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)
  symbol?                                            (symbol)
  ( 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 ... /))\