Pattern Matches Library — patternMatchesLib
HOL supports two different types of case expressions: decision tree based and \pmatch{} case expressions. These are presented in Section 7.5. In subsection 7.5.2, the basic usage of \pmatch{} case expressions is discussed. Some concepts presented there briefly are discussed here in detail. Moreover, advanced features are discussed here.
Simplification
The most important tool to deal with \pmatch{} case expressions
is the conversion PMATCH_SIMP_CONV or the corresponding
PMATCH_SIMP_ss, which is part of bossLib.std_ss. It
combines the following methods of simplifying and (partially)
evaluating \pmatch{} case expressions. A subset of these methods
that skips normalisations and potentially expensive searches for
redundant and subsumed rows is available as
PMATCH_FAST_SIMP_CONV.
Normalisation
Many simplifications rely on the variables of a pattern being
named consistently and no extra, unused pattern variables being
present. The conversion PMATCH_CLEANUP_PVARS_CONV removes
unused pattern variables and ensures that the names of variables
used by the pattern, the guard and the right-hand-side of a row
coincide.
> PMATCH_CLEANUP_PVARS_CONV ``PMATCH (x:('a # 'b) option) [
PMATCH_ROW (\x:'a. NONE) (\x. T) (\x. 5);
PMATCH_ROW (\ (x,(y:'c)). SOME (x,z)) (\ (x,y). T) (\ (x,y). 8);
PMATCH_ROW (\ (x,z). SOME (x,z)) (\_. T) (\ (a,y). 8)]``
val it =
⊢ PMATCH x
[PMATCH_ROW (λx. NONE) (λx. T) (λx. 5);
PMATCH_ROW (λ(x,y). SOME (x,z)) (λ(x,y). T) (λ(x,y). 8);
PMATCH_ROW (λ(x,z). SOME (x,z)) (λ_0. T) (λ(a,y). 8)] =
pmatch x of NONE => 5 | x .| SOME (x,z) => 8 | SOME (x,z) => 8: thm
Similarly, many \pmatch{} tools rely on each pattern of a case
expression having the same number of columns. This normal form
is enforced by PMATCH_EXPAND_COLS_CONV.
> PMATCH_EXPAND_COLS_CONV ``pmatch (x,y,z) of
(0,y,T) => y
| xyz when ~ SND (SND xyz) => 2
| (x,yz) => x``
val it =
⊢ (pmatch (x,y,z) of
(0,y,T) => y | xyz when ¬SND (SND xyz) => 2 | (x,yz) => x) =
pmatch (x,y,z) of
(0,y,T) => y
| (xyz_0,xyz_1,xyz_2) when ¬SND (SND (xyz_0,xyz_1,xyz_2)) => 2
| (x,yz_0,yz_1) => x: thm
Finally, the conversion PMATCH_INTRO_WILDCARDS_CONV
renames unused pattern variables such that they start with an
underscore. As a result, they are printed as a wildcard pattern,
making case expressions more readable. It also renames used
variables that start with an underscore. This is rarely needed,
though.
> PMATCH_INTRO_WILDCARDS_CONV ``pmatch (x,y,z) of
(_x, y, z) => _x + y
| (x, y, z) when z => x``
val it =
⊢ (pmatch (x,y,z) of (_,y,z) => _ + y | (x,y,z) when z => x) =
pmatch (x,y,z) of (v0,y,_) => v0 + y | (x,_,z) when z => x: thm
A combination of these conversions for normalising \pmatch{} case
expressions is available as PMATCH_NORMALISE_CONV.
(Partial) evaluation
The function PMATCH_CLEANUP_CONV checks each row of a
\pmatch{} case expression and determines whether it matches the
tested expression. There are three possible outcomes of such a
check: a proof that the row matches, a proof that the row does
not match or that it could not be decided whether the row matches.
Rows that are proved to not match are removed. Similarly, all
rows after the first matching row are redundant and are removed.
If the first remaining row is known to match, the whole case
expression is evaluated.
The proof of whether a row matches is attempted using some default
proof methods. In particular information about datatype
constructors is automatically used from TypeBase and
constrFamiliesLib (see Section 8.9.6.2).
If used via PMATCH_SIMP_ss, a callback to the simplifier
is used. The conversion PMATCH_CLEANUP_CONV_GEN is a
generalised version of the partial evaluation conversion that
allows manually providing additional simpset fragments to the
used proof method.
In the following example, the first row is removed, because it
does not match. The second line is kept, since depending on the
value of y it might or might not match. Since the third line
matches in any case, the fourth one is deleted.
> PMATCH_CLEANUP_CONV ``pmatch (SOME (x:num),y) of
(NONE, y) => 1
| (x, 0) => 2
| (SOME x, y) => 3
| (x, y) => 4``
val it =
⊢ (pmatch (SOME x,y) of
(NONE,y) => 1 | (x,0) => 2 | (SOME x,y) => 3 | (x,y) => 4) =
pmatch (SOME x,y) of (x,0) => 2 | (SOME x,y) => 3: thm
If the first row remaining matches, the case expression is evaluated:
> PMATCH_CLEANUP_CONV ``pmatch (SOME x, y) of
(NONE, y) => 1
| (SOME x, y) => x+y
| (x, y) => 4``
val it =
⊢ (pmatch (SOME x,y) of (NONE,y) => 1 | (SOME x,y) => x + y | (x,y) => 4) =
x + y: thm
Similarly, if no row matches, the whole case expression is evaluated.
> PMATCH_CLEANUP_CONV ``pmatch (SOME (x:num), y:num) of (NONE, y) => 1``
val it = ⊢ (pmatch (SOME x,y) of (NONE,y) => 1) = PMATCH_INCOMPLETE: thm
Simplifying columns
Before, we saw how rows can be removed.
PMATCH_SIMP_COLS_CONV allows removing a column of a
\pmatch{} case expression. If for all rows a certain column
matches the input value for this column, the column can be
removed. This situation usually arises after removing certain
rows from a case expression via partial evaluation.
> PMATCH_SIMP_COLS_CONV ``pmatch (SOME x,y) of
| (SOME x, 1) => x+y
| (x, y) => 4``
val it =
⊢ (pmatch (SOME x,y) of (SOME x,1) => x + y | (x,y) => 4) =
pmatch y of 1 => x + y | y => 4: thm
Similarly, a column is partially evaluated if all rows contain either a variable, a wildcard or a term of the same constructor in this column.
> PMATCH_SIMP_COLS_CONV ``pmatch (SOME x,y) of
| (SOME x, 1) => SOME (x+y)
| (SOME 2, 2) => NONE
| (x, y) => x``
val it =
⊢ (pmatch (SOME x,y) of
(SOME x,1) => SOME (x + y) | (SOME 2,2) => NONE | (x,y) => x) =
pmatch (x,y) of
(x,1) => SOME (x + y) | (2,2) => NONE | (x_0,y) => SOME x_0: thm
Removing redundant rows
The simplifications above easily lead to case expressions that
contain multiple similar rows. The conversion
PMATCH_REMOVE_FAST_REDUNDANT_CONV is intended to cleanup
such rows. A row is called redundant if each value that matches
it also matches an earlier row. Redundant rows will never matter
and can therefore safely be removed. Thus the conversion
PMATCH_REMOVE_FAST_REDUNDANT_CONV checks whether a
pattern of a row is an instance of a pattern of an earlier row.
This simple, fast heuristic is sufficient to detect most instances
of redundant rows occurring during simplification. In the
following example, the rows with right-hand-side 2, 4 and 5 are
redundant. However, this simple heuristic cannot detect that
row 5 is redundant. A more advanced method for removing redundant
rows, which is slower but for example able to detect that row 5
is redundant, is discussed in
Section 8.9.7.
> PMATCH_REMOVE_FAST_REDUNDANT_CONV ``pmatch xy of
| (SOME x, y) => 1 | (SOME 2, 3) => 2
| (NONE, y) => 3 | (NONE, y) => 4
| (x, 5) => 5``
val it =
⊢ (pmatch xy of
(SOME x,y) => 1
| (SOME 2,3) => 2
| (NONE,y) => 3
| (NONE,y) => 4
| (x,5) => 5) =
pmatch xy of (SOME x,y) => 1 | (NONE,y) => 3 | (x,5) => 5: thm
Removing subsumed rows
Redundant rows are rows that are not needed, because they are
shadowed by an earlier row. Similarly, subsumed rows are rows
that can be dropped, because in case they match a later row
matches as well and evaluates to the same value. It is trickier
to check for subsumed rows, because one needs to check that no
row between the subsuming row and the possibly subsumed row
matches, and because the right hand sides of the rows need to be
considered as well. The function
PMATCH_REMOVE_FAST_SUBSUMED_CONV removes subsumed rows
that can be detected quickly.
If no row matches, a \pmatch{} case expression evaluates to ARB.
Therefore, a row with right-hand-side of ARB is considered to
be subsumed if no further row matches. This is not always what
users expect or want. For example, the user might not want to
see an exhaustive pattern match turn into a non-exhaustive one.
Thus PMATCH_REMOVE_FAST_SUBSUMED_CONV takes an additional
boolean argument ra, which allows one to configure whether such
rows are removed.
> PMATCH_REMOVE_FAST_SUBSUMED_CONV true ``pmatch xy of
| (SOME 2, _) => 2 | (NONE, 3) => 1
| (SOME x, _) => x | (NONE, y) => y
| (x, 5) => ARB``
val it =
⊢ (pmatch xy of
(SOME 2,_) => 2
| (NONE,3) => 1
| (SOME x,_) => x
| (NONE,y) => y
| (x,5) => ARB) =
pmatch xy of (NONE,3) => 1 | (SOME x,_) => x | (NONE,y) => y: thm
> PMATCH_REMOVE_FAST_SUBSUMED_CONV false ``pmatch xy of
| (SOME 2, _) => 2 | (NONE, 3) => 1
| (SOME x, _) => x | (NONE, y) => y
| (x, 5) => ARB``
val it =
⊢ (pmatch xy of
(SOME 2,_) => 2
| (NONE,3) => 1
| (SOME x,_) => x
| (NONE,y) => y
| (x,5) => ARB) =
pmatch xy of
(NONE,3) => 1 | (SOME x,_) => x | (NONE,y) => y | (x,5) => ARB: thm
The PMATCH_SIMP_CONV conversion keeps such rows.
> PMATCH_SIMP_CONV ``pmatch xy of
| (SOME 2, _) => 2 | (NONE, 3) => 1
| (SOME x, _) => x | (NONE, y) => y
| (x, 5) => ARB``
val it =
⊢ (pmatch xy of
(SOME 2,_) => 2
| (NONE,3) => 1
| (SOME x,_) => x
| (NONE,y) => y
| (x,5) => ARB) =
pmatch xy of
(NONE,3) => 1 | (SOME x,_) => x | (NONE,y) => y | (_,5) => ARB: thm
Support for computeLib
The conversion PMATCH_CLEANUP_CONV (see
Section 8.9.1.2) is added to the internal
database of computeLib. This allows the efficient evaluation
of ground terms that contain \pmatch{} case expressions.
> EVAL ``pmatch (SOME 3, SOME 4) of
| (SOME x, SOME y) => SOME (x + y)
| (_, _) => NONE``
val it =
⊢ (pmatch (SOME 3,SOME 4) of
(SOME x,SOME y) => SOME (x + y) | (_,_) => NONE) =
SOME 7: thm
> EVAL ``pmatch (NONE, SOME 4) of
| (SOME x, SOME y) => SOME (x + y)
| (_, _) => NONE``
val it =
⊢ (pmatch (NONE,SOME 4) of (SOME x,SOME y) => SOME (x + y) | (_,_) => NONE) =
NONE: thm
Removing extra features
\pmatch{} case expressions support features that are not usually supported by programming languages. One can use the same pattern variable multiple times in a pattern and use variables not bound by a pattern. Moreover, there is support for guards.
Sometimes, it is desirable to remove such features from a \pmatch{} case expression. A typical example is that they need to be removed before code-extraction.
Normalising pattern variables
The function PMATCH_REMOVE_DOUBLE_BIND_CONV and the
corresponding simpset fragment PMATCH_REMOVE_DOUBLE_BIND_ss
remove variables bound multiple times by a pattern as well as
variables not bound by the pattern. This is easily achievable by
introducing extra variables into the pattern and constraining
their value by adding extra conditions to the guard.
> PMATCH_REMOVE_DOUBLE_BIND_CONV ``pmatch xy of
| (x, x) when x > 0 => x + x
| x.| (x, y) => x
| (x, _) => SUC x``
val it =
⊢ (pmatch xy of
(x,x) when x > 0 => x + x | x .| (x,y) => x | (x,_) => SUC x) =
pmatch xy of
(x,x') when x' = x ∧ x > 0 => x + x
| (x,y') when y' = y => x
| (x,_) => SUC x: thm
Removing guards
Guards can be removed by introducing an if-then-else expression
on the right-hand-side. The else-part of this if-then-else
expression needs to continue the case-split with the rows
occurring after the row whose guard is removed. Usually this
case expression can be simplified significantly, since we know
that the input matches the pattern of the row, whose guard is
removed. Therefore, the conversion
PMATCH_REMOVE_GUARDS_CONV as well as the corresponding
PMATCH_REMOVE_GUARDS_ss internally call
PMATCH_SIMP_CONV.
> PMATCH_REMOVE_GUARDS_CONV ``pmatch (x, y) of
| (x, 2) when EVEN x => x + x
| (SUC x, y) when ODD x => y + x + SUC x
| (SUC x, 1) => x
| (x, _) => x+3``
val it =
⊢ (pmatch (x,y) of
(x,2) when EVEN x => x + x
| (SUC x,y) when ODD x => y + x + SUC x
| (SUC x,1) => x
| (x,_) => x + 3) =
pmatch (x,y) of
(x,2) =>
if EVEN x then x + x
else pmatch x of SUC x when ODD x => 2 + x + SUC x | x => x + 3
| (SUC x,y) =>
if ODD x then y + x + SUC x
else pmatch y of 1 => x | _ => SUC x + 3
| (x,_) => x + 3: thm
> PMATCH_REMOVE_GUARDS_CONV ``pmatch (x, y) of
| (x, 0) when EVEN x => (SOME x, T)
| (x, 0) => (SOME x, F)
| (0, _) => (NONE, T)
| (_, _) => (NONE, F)``
val it =
⊢ (pmatch (x,y) of
(x,0) when EVEN x => (SOME x,T)
| (x,0) => (SOME x,F)
| (0,_) => (NONE,T)
| (_,_) => (NONE,F)) =
pmatch (x,y) of
(x,0) => if EVEN x then (SOME x,T) else (SOME x,F)
| (0,_) => (NONE,T)
| (_,_) => (NONE,F): thm
> SIMP_CONV (std_ss ++ PMATCH_REMOVE_GUARDS_ss) [] ``pmatch x of
| _ when x < 5 => 0
| _ when x < 10 => 1
| _ => 2``
val it =
⊢ (pmatch x of _ when x < 5 => 0 | _ when x < 10 => 1 | _ => 2) =
if x < 5 then 0 else if x < 10 then 1 else 2: thm
Lifting case expressions
HOL provides powerful tools for rewriting. Probably the most
commonly used way of using case expressions in HOL is at
top-level for defining recursive functions. Special support in
Define turns multiple top-level equations into a decision
tree case expressions, uses this case expression for defining a
function and then derives top-level equations similar to the
input ones. Since compilation to decision trees is used, the
issues discussed in Section 7.5 are present. It is
sometimes hard to predict, which equations will be generated.
There might be a blow-up in the number of equations. Moreover,
equations cannot overlap and are therefore often unnecessarily
complicated.
As an example consider the following definition of a zipping functions for lists.
> val MYZIP_def = Define `
(MYZIP [] _ = []) /\
(MYZIP _ [] = []) /\
(MYZIP (x::xs) (y::ys) = (x,y) :: (MYZIP xs ys))` ... output elided ...
val MYZIP_def =
⊢ (∀v0. MYZIP [] v0 = []) ∧ (∀v4 v3. MYZIP (v3::v4) [] = []) ∧
∀ys y xs x. MYZIP (x::xs) (y::ys) = (x,y)::MYZIP xs ys: thm
> val MYZIP2_def = Pmatch.with_classic_heuristic Define `
(MYZIP2 [] _ = []) /\
(MYZIP2 _ [] = []) /\
(MYZIP2 (x::xs) (y::ys) = (x,y) :: (MYZIP2 xs ys))` ... output elided ...
val MYZIP2_def =
⊢ MYZIP2 [] [] = [] ∧ (∀v8 v7. MYZIP2 [] (v7::v8) = []) ∧
(∀v4 v3. MYZIP2 (v3::v4) [] = []) ∧
∀ys y xs x. MYZIP2 (x::xs) (y::ys) = (x,y)::MYZIP2 xs ys: thm
We can use \pmatch{} case expressions to fight these issues.
There is, however, no special support for \pmatch{} case
expressions built into Define. Instead, one needs to define
a function with a \pmatch{} case expression on the right-hand-side.
Using the rule PMATCH_TO_TOP_RULE then produces the
desired (conditional) equations.
> val MYZIP3_def = Define `
MYZIP3 xl yl = (pmatch (xl, yl) of
| ([], _) => []
| (_, []) => []
| (x::xs, y::ys) => (x,y) :: (MYZIP3 xs ys))` ... output elided ...
> val MYZIP3_EQS = PMATCH_TO_TOP_RULE MYZIP3_def
val MYZIP3_EQS =
⊢ (∀yl. MYZIP3 [] yl = []) ∧ (∀xl. MYZIP3 xl [] = []) ∧
∀x xs y ys. MYZIP3 (x::xs) (y::ys) = (x,y)::MYZIP3 xs ys: thm
Similarly, the resulting induction theorems are more predictable and contain fewer cases. However, the structure tends not to be as nice.
val MYZIP_ind =
⊢ ∀P. (∀v0. P [] v0) ∧ (∀v3 v4. P (v3::v4) []) ∧
(∀x xs y ys. P xs ys ⇒ P (x::xs) (y::ys)) ⇒
∀v v1. P v v1: thm
val MYZIP2_ind =
⊢ ∀P. P [] [] ∧ (∀v7 v8. P [] (v7::v8)) ∧ (∀v3 v4. P (v3::v4) []) ∧
(∀x xs y ys. P xs ys ⇒ P (x::xs) (y::ys)) ⇒
∀v v1. P v v1: thm
val MYZIP3_ind =
⊢ ∀P. (∀xl yl.
(∀x xs y ys. (xl,yl) = (x::xs,y::ys) ∧ T ⇒ P xs ys) ⇒ P xl yl) ⇒
∀v v1. P v v1: thm
For the zipping examples the resulting equations are particularly nice. In general, conditional equations need to be generated. The preconditions state that no previous row matched or that the result of such a matching row coincides with the result of the current row.
> val MYZIP4_def = Define `
MYZIP4 xl yl = (pmatch (xl, yl) of
| ([], []) => (NONE, [])
| ([], _) => (SOME T, [])
| (_, []) => (SOME F, [])
| (x::xs, y::ys) => (case (MYZIP4 xs ys) of
| (r, l) => (r, (x,y)::l)))` ... output elided ...
> val MYZIP4_EQS = PMATCH_TO_TOP_RULE MYZIP4_def
val MYZIP4_EQS =
⊢ MYZIP4 [] [] = (NONE,[]) ∧ (∀yl. yl ≠ [] ⇒ MYZIP4 [] yl = (SOME T,[])) ∧
(∀xl. xl ≠ [] ⇒ MYZIP4 xl [] = (SOME F,[])) ∧
∀x xs y ys.
MYZIP4 (x::xs) (y::ys) = case MYZIP4 xs ys of (r,l) => (r,(x,y)::l):
thm
The lifting functionality is also available via
PMATCH_LIFT_BOOL_ss and PMATCH_LIFT_BOOL_CONV,
which lift a \pmatch{} case expression to the next highest
boolean level and expands it there. Since trying to prove
exhaustiveness (see Section 8.9.9) might be
slow, there is flag for turning it on and off explicitly.
Moreover, notice that PMATCH_LIFT_BOOL_CONV always tries
to lift to the top-level. Therefore, it should usually be combined
with something like DEPTH_CONV.
> DEPTH_CONV (PMATCH_LIFT_BOOL_CONV true) ``
P /\ (f (pmatch x of [] => 0 | x::xs => x) = 5) /\ Q``
val it =
⊢ P ∧ f (pmatch x of [] => 0 | x::xs => x) = 5 ∧ Q ⇔
P ∧ ((x = [] ⇒ f 0 = 5) ∧ ∀x' xs. x = x'::xs ⇒ f x' = 5) ∧ Q: thm
> DEPTH_CONV (PMATCH_LIFT_BOOL_CONV false) ``
P /\ (f (pmatch x of [] => 0 | x::xs => x) = 5) /\ Q``
val it =
⊢ P ∧ f (pmatch x of [] => 0 | x::xs => x) = 5 ∧ Q ⇔
P ∧
((x = [] ⇒ f 0 = 5) ∧ (∀x' xs. x = x'::xs ⇒ f x' = 5) ∧
(¬PMATCH_IS_EXHAUSTIVE x
[PMATCH_ROW (λ_. []) (λ_. T) (λ_. 0);
PMATCH_ROW (λ(x,xs). x::xs) (λ(x,xs). T) (λ(x,xs). x)] ⇒
f ARB = 5)) ∧ Q: thm
Translating \pmatch{} and decision tree case expressions
As discussed in Section 7.5, there are benefits to both \pmatch{} and decision tree based case expressions. Therefore, there are tools for translating between both representations.
The function pmatch2case uses the pattern compilation
algorithm implemented in HOL's parser to generate decision
tree case expressions. This is done outside the logic without any
formal justification. However, a brute force method that
repeatedly performs case splits and evaluates is sufficient for
proving equivalence. This leads to PMATCH_ELIM_CONV.
Only \pmatch{} case expressions that fall into the subset supported by decision tree ones can be translated. This means that no guards can be used and that all patterns need to be constructor patterns.
> PMATCH_ELIM_CONV
``pmatch (xy:(num option # num list)) of (NONE, x::xs) => 0``
<<HOL message: mk_functional:
pattern completion has added 2 clauses to the original specification.>>
val it =
⊢ (pmatch xy of (NONE,x::xs) => 0) =
case xy of (v,[]) => ARB | (NONE,x::xs) => 0 | (SOME v5,x::xs) => ARB:
thm
An approach similar to the one implemented in HOL's pretty
printer allows the translation of decision tree case expressions
to equivalent \pmatch{} expressions. The underlying function is
case2pmatch do_opt, where the do_opt flag determines
whether certain non-trivial optimisations are attempted. The
corresponding conversions are named PMATCH_INTRO_CONV and
PMATCH_INTRO_CONV_NO_OPTIMISE.
> PMATCH_INTRO_CONV
``case (xy:(num option # num list)) of (NONE, x::xs) => 0``
<<HOL message: mk_functional:
pattern completion has added 2 clauses to the original specification.>>
val it =
⊢ (case xy of (v,[]) => ARB | (NONE,x::xs) => 0 | (SOME v5,x::xs) => ARB) =
pmatch xy of (NONE,_::_) => 0: thm
> PMATCH_INTRO_CONV_NO_OPTIMISE
``case (xy:(num option # num list)) of (NONE, x::xs) => 0``
<<HOL message: mk_functional:
pattern completion has added 2 clauses to the original specification.>>
val it =
⊢ (case xy of (v,[]) => ARB | (NONE,x::xs) => 0 | (SOME v5,x::xs) => ARB) =
pmatch xy of (v,[]) => ARB | (NONE,x::xs) => 0 | (SOME v5,x::xs) => ARB:
thm
Pattern Compilation
The pmatch2case function allows \pmatch{} case expressions
to be compiled into decision tree case expressions. It is fast
and the result is usually pretty good. However, it relies on
the pattern compilation implementation of HOL's parser. This
has several drawbacks. The most significant one is that it is
an all-or-nothing approach. Either the compilation succeeds and
we get an equivalent decision tree case expression (without proof)
or it fails and one has nothing. It is not easily possible to
get partial results or use the information obtained during
pattern compilation to prove exhaustiveness or find a set of
missing patterns. With simplification of \pmatch{} case
expressions (see Section 8.9.1) in place, it
is straightforward to implement pattern compilation. One
performs a case-split on one variable occurring in the input of
the case expression, simplifies and iterates. This is implemented
as PMATCH_CASE_SPLIT_CONV.
Note that PMATCH_CASE_SPLIT_CONV has no support for
guards or pattern variables bound multiple times. These features
need to be removed (see Section 8.9.3)
before calling it.
> PMATCH_CASE_SPLIT_CONV
``pmatch l of (SOME x, SOME y) => SOME (x+y) | (_, _) => NONE``
val it =
⊢ (pmatch l of (SOME x,SOME y) => SOME (x + y) | (_,_) => NONE) =
case l of
(NONE,v') => NONE
| (SOME x',NONE) => NONE
| (SOME x',SOME x'') => SOME (x' + x''): thm
The trick is to choose which case split to apply next. This decision is taken by two mechanisms: a column heuristic picks the column to perform a case split on and the available case-splits are maintained by the constructor family library.
Column Heuristic
The most important decision during pattern compilation is which
column, i.e., which input variable to perform a case split on
next. Different decisions lead to different decision trees,
which can differ significantly in size and time needed to
evaluate. It is not trivial to find a good column to split on.
Currently, mainly heuristics presented by
Maranget (Maranget 2008) are implemented. In HOL a column
heuristic is a ML function of type column_heuristic. Given
a list of columns such a heuristic returns the number of the
column to perform a split on. There are very simple heuristics
like always picking the first or last column, but also
sophisticated ones like qba (see (Maranget 2008)). Users can
easily implement additional heuristics should the need arise.
Figure 8.9.6.1 shows the
effects of using different heuristics.
Figure 8.9.6.1. Effect of different column heuristics.
val t =
...
> PMATCH_CASE_SPLIT_CONV_HEU colHeu_first_col t
metis: r[+0+5]+0+0+1+1+2+0+1+0+0#
metis: r[+0+5]+0+0+1+1+2+0+1+0+0#
metis: r[+0+5]+0+0+1+1+2+0+1+0+0#
metis: r[+0+5]+0+0+1+1+2+0+1+0+0#
metis: r[+0+5]+0+0+1+1+2+0+1+0+0#
metis: r[+0+5]+0+0+1+1+2+0+1+0+0#
val it =
⊢ (pmatch (x,y,z) of
(_,F,T) => 1 | (F,T,_) => 2 | (_,_,F) => 3 | (_,_,T) => 4) =
case (x,y,z) of
(T,T,T) => 4
| (T,T,F) => 3
| (T,F,T) => 1
| (T,F,F) => 3
| (F,T,v'³') => 2
| (F,F,T) => 1
| (F,F,F) => 3: thm
> PMATCH_CASE_SPLIT_CONV_HEU colHeu_last_col t
metis: r[+0+5]+0+0+1+1+2+0+1+0+0#
metis: r[+0+5]+0+0+1+1+2+0+1+0+0#
metis: r[+0+5]+0+0+1+1+2+0+1+0+0#
metis: r[+0+5]+0+0+1+1+2+0+1+0+0#
metis: r[+0+5]+0+0+1+1+2+0+1+0+0#
val it =
⊢ (pmatch (x,y,z) of
(_,F,T) => 1 | (F,T,_) => 2 | (_,_,F) => 3 | (_,_,T) => 4) =
case (x,y,z) of
(T,T,T) => 4
| (F,T,T) => 2
| (v,F,T) => 1
| (T,T,F) => 3
| (F,T,F) => 2
| (v,F,F) => 3: thm
> PMATCH_CASE_SPLIT_CONV_HEU colHeu_default t
metis: r[+0+5]+0+0+1+1+2+0+1+0+0#
metis: r[+0+5]+0+0+1+1+2+0+1+0+0#
metis: r[+0+5]+0+0+1+1+2+0+1+0+0#
metis: r[+0+5]+0+0+1+1+2+0+1+0+0#
val it =
⊢ (pmatch (x,y,z) of
(_,F,T) => 1 | (F,T,_) => 2 | (_,_,F) => 3 | (_,_,T) => 4) =
case (x,y,z) of
(T,T,T) => 4
| (T,T,F) => 3
| (F,T,v'³') => 2
| (v,F,T) => 1
| (v,F,F) => 3: thm
Constructor Family Library
Once a column has been chosen, a case split needs to be performed. This requires getting information about an appropriate case split function. Moreover, even for selecting the column some heuristics need information. It might for example be desirable to know to how many cases splitting on a column would lead.
Essentially, one needs to lookup the constructors of a datatype
together with its case-constant. Moreover, theorems about
injectivity and pairwise distinctiveness of the constructors as
well as some theorems about the case-constant are needed. All
this information can be found in TypeBase (see
Section 7.2). The pattern compilation algorithm
in the parser uses TypeBase. However, patternMatchesLib
has two demands not met by TypeBase. For each type, it
should be possible to store multiple sets of constructors.
Moreover, sometimes the case split should not be stored
statically but — given a column — be computed dynamically. These
demands lead to the implementation of constrFamiliesLib.
The constructor family library contrFamiliesLib is a library
for collecting information about constructors and case-splits.
At its core is the concept of a constructor family. A
constructor family is a list of functions together with a
case-split functions. The functions should all be injective and
pairwise distinct. The case-split function should provide a
case-analysis that corresponds with the functions. Constructor
families can be exhaustive or inexhaustive. For inexhaustive
ones, the case-split function has to provide an extra
otherwise-case.
The constructors of datatypes together with the case constant
form constructor families. For example, the constructors []
and CONS with list_CASE form an exhaustive constructor family
for lists. The information for the constructor families
corresponding to the datatype constructors is automatically
extracted from TypeBase and available via
constrFamiliesLib. However, there might be other interesting
constructor families. For example, [] and SNOC together with
an appropriate case split function form another exhaustive
constructor family for lists.
First, we need to define a case-split function for [] and SNOC.
> val list_REVCASE_def = Define `
list_REVCASE l c_nil c_snoc =
(if l = [] then c_nil else (c_snoc (LAST l) (BUTLAST l)))` ... output elided ...
Next, we define an exhaustive list of constructors. This is the list of functions combined with names for the arguments of each constructor.
> open constrFamiliesLib ... output elided ...
> val cl = make_constructorList true [
(``[]:'a list``, []),
(``SNOC: 'a -> 'a list -> 'a list``, ["x", "xs"])]
val cl =
{cl_constructors = [CONSTR (“[]”, []), CONSTR (“SNOC”, ["x", "xs"])],
cl_is_exhaustive = true, cl_type = “:α list”}: constructorList
The function mk_constructorFamily is then used to create a
constructor family. This requires proving the discussed
properties. In order to develop the necessary tactic,
set_constructorFamily can be used.
> set_constructorFamily (cl, ``list_REVCASE``)
val it =
Proof manager status: 2 proofs.
2. Incomplete goalstack:
Initial goal:
x = 10 ∧ x < 16
Current goal:
x = 10
1. Incomplete goalstack:
Initial goal:
(∀x xs x' xs'. SNOC x xs = SNOC x' xs' ⇔ x = x' ∧ xs = xs') ∧
((∀x xs. [] ≠ SNOC x xs) ∧ ∀x xs. SNOC x xs ≠ []) ∧
(∀ff x. ff x = list_REVCASE x (ff []) (λx' xs. ff (SNOC x' xs))) ∧
(∀x' f1 f2 x f1' f2'.
x' = x ⇒
(x = [] ⇒ f1 = f1') ⇒
(∀x' xs. x = SNOC x' xs ⇒ f2 x' xs = f2' x' xs) ⇒
list_REVCASE x' f1 f2 = list_REVCASE x f1' f2') ∧
∀x. x = [] ∨ ∃x' xs. x = SNOC x' xs
> val cf = mk_constructorFamily (cl, ``list_REVCASE``, ... some tactic ...)
val cf =
{case_cong_thm =
⊢ ∀x' f1 f2 x f1' f2'.
x' = x ⇒
(x = [] ⇒ f1 = f1') ⇒
(∀x' xs. x = SNOC x' xs ⇒ f2 x' xs = f2' x' xs) ⇒
list_REVCASE x' f1 f2 = list_REVCASE x f1' f2', case_const =
“list_REVCASE”, case_split_thm =
⊢ ∀ff x. ff x = list_REVCASE x (ff []) (λx' xs. ff (SNOC x' xs)),
constructors =
{cl_constructors = [CONSTR (“[]”, []), CONSTR (“SNOC”, ["x", "xs"])],
cl_is_exhaustive = true, cl_type = “:α list”}, distinct_thm =
SOME ⊢ (∀x xs. [] ≠ SNOC x xs) ∧ ∀x xs. SNOC x xs ≠ [], nchotomy_thm =
SOME ⊢ ∀x. x = [] ∨ ∃x' xs. x = SNOC x' xs, one_one_thm =
SOME ⊢ ∀x xs x' xs'. SNOC x xs = SNOC x' xs' ⇔ x = x' ∧ xs = xs'}:
constructorFamily
Finally, we can register this newly defined constructor family.
> val _ = pmatch_compile_db_register_constrFam cf
Now this new family is available for pattern compilation. Notice, that the old constructors for lists are still present.
> PMATCH_CASE_SPLIT_CONV ``pmatch ll of
(SNOC x xs, []) => x
| ([], x::xs) => x
| (_, _) => 0``
metis: r[+0+5]+0+0+0+1+0+2#
val it =
⊢ (pmatch ll of (SNOC x xs,[]) => x | ([],x::xs) => x | (_,_) => 0) =
case ll of
(v,v') =>
list_REVCASE v (case v' of [] => 0 | h::t => h)
(λx' xs. case v' of [] => x' | h'::t' => 0): thm
Inexhaustive constructor families are often handy as well. Consider the example of red-black-trees defined as follows:
> val _ = Datatype `
tree = Empty
| Red tree 'a tree
| Black tree 'a tree`; ... output elided ...
A lot of functions (e.g., balancing) treat black nodes and leaves
the same. However, when compiling corresponding case expressions
to decision trees, 3 cases instead of the required 2 are produced.
Defining an inexhaustive constructor family for just the RED
constructor solves this issue (see
Figure 8.9.6.2).
Figure 8.9.6.2. Example inexhaustive constructor family.
val tree_red_CASE_def = Define
tree_red_CASE tr f_red f_else = tree_CASE tr (f_else Empty) f_red (\t1 n t2. f_else (Black t1 n t2))... output elided ... val cl = make_constructorList false [(Red, ["t1", "n", "t2"])] ... output elided ...
> val cf = mk_constructorFamily (cl, ``tree_red_CASE``, ... some tactic ...)
> val _ = pmatch_compile_db_register_constrFam cf ... output elided ...
> PMATCH_CASE_SPLIT_CONV ``pmatch (t:'a tree) of
| Red _ _ _ => T
| _ => F``
val it =
⊢ (pmatch t of Red _ _ _ => T | _ => F) ⇔
tree_red_CASE t (λt1 n t2. T) (λx. F): thm
> PMATCH_CASE_SPLIT_CONV ``pmatch (t:'a tree) of
| Black _ _ _ => T
| _ => F``
val it =
⊢ (pmatch t of Black _ _ _ => T | _ => F) ⇔
case t of Empty => F | Red t a t0 => F | Black t' a' t0' => T: thm
Compiling to nchotomy theorems
Compiling to decision tree based case expressions is sometimes handy. However, computing the patterns corresponding to this decision tree is even more useful, since this set of patterns has very interesting properties. It is exhaustive and for each input pattern each pattern in this set is either a subpattern of the input pattern or distinct. There are no partial overlaps. Even better, whether an output pattern is a subpattern of an input pattern is checkable via simple first order matching.
Let's look at an example. First we compile a case expression to a decision tree.
> PMATCH_CASE_SPLIT_CONV ``pmatch xy of
| (SOME x, SOME y) => x + y
| (_, SOME 0) => 0``
metis: r[+0+5]+0+0+1+0+0#
val it =
⊢ (pmatch xy of (SOME x,SOME y) => x + y | (_,SOME 0) => 0) =
case xy of
(v,NONE) => ARB
| (NONE,SOME 0) => 0
| (NONE,SOME (SUC n)) => ARB
| (SOME x'',SOME x') => x'' + x': thm
We end up with 4 rows in the pretty-printed form of the decision
tree case expression. These 4 output patterns have the desired
properties. They are exhaustive and for example (NONE, SOME 0)
is a subpattern of (_, SOME 0), but distinct from
(SOME x, SOME y). The nchotomy_of_pats
function compiles the list of input patterns to an
nchotomy-theorem containing exactly these 4 patterns.
> nchotomy_of_pats [``\(x,y). (SOME (x:num), SOME (y:num))``,
``\(xo:num option). (xo, SOME 0)``]
val it =
⊢ ∀x. (∃v0. x = (v0,NONE)) ∨ x = (NONE,SOME 0) ∨
(∃v4. x = (NONE,SOME (SUC v4))) ∨ (∃v3. x = (SOME v3,SOME 0)) ∨
∃v3 v5. x = (SOME v3,SOME (SUC v5)): thm
Such nchotomy theorems are very useful for finding missing patterns, detecting redundant rows and proving exhaustiveness. Essentially, one just removes one input pattern after the other by applying first order matching. The patterns that remain are not covered by the input.
Removing Redundant Rows
Using pattern compilation, it is straightforward to implement
advanced redundancy checks. The conversion
PMATCH_REMOVE_REDUNDANT_CONV
and the corresponding simpset fragment
PMATCH_REMOVE_REDUNDANT_ss are able to remove row 5 of
the example already discussed in
Section 8.9.1.4.
> PMATCH_REMOVE_REDUNDANT_CONV ``pmatch xy of
| (SOME x, y) => 1 | (SOME 2, 3) => 2
| (NONE, y) => 3 | (NONE, y) => 4
| (x, 5) => 5``
metis: r[+0+5]+0+0+0+2+2+0+0+1+0+2#
metis: r[+0+7]+0+0+0+0+0+2+2+2+2+2+2+0+0+0+0+1+0+1+0+1+1+0+1+1#
val it =
⊢ (pmatch xy of
(SOME x,y) => 1
| (SOME 2,3) => 2
| (NONE,y) => 3
| (NONE,y) => 4
| (x,5) => 5) =
pmatch xy of (SOME x,y) => 1 | (NONE,y) => 3: thm
If the redundancy of a row depends not only on patterns, but also guards, the automated method often fails. Figure 8.9.7 shows an example, where the information that each natural number is either even or odd is needed to show that a row is redundant. In such situations, it is often beneficial to combine the automated redundancy removal technique with manual reasoning (as in the figure).
Figure 8.9.7. Manual reasoning about redundant rows.
val t =
pmatch x of _ when EVEN x => 0 | _ when ODD x => 1 | _ => 2... output elided ... PMATCH_REMOVE_REDUNDANT_CONV t Exception- UNCHANGED raised
val info = COMPUTE_REDUNDANT_ROWS_INFO_OF_PMATCH t val info = ⊢ IS_REDUNDANT_ROWS_INFO x [PMATCH_ROW (λ_0. _0) (λ_0. EVEN x) (λ_0. 0); PMATCH_ROW (λ_0. _0) (λ_0. ODD x) (λ_0. 1); PMATCH_ROW (λ_0. _0) (λ_0. T) (λ_0. 2)] F [¬∃_0. x = _0 ∧ EVEN x; (∃v0. x = v0 ∧ ¬EVEN x) ⇒ ¬∃_0. x = _0 ∧ ODD x; (∃v0. x = v0 ∧ ¬EVEN x ∧ ¬ODD x) ⇒ ¬∃_0. x = _0]: thm
IS_REDUNDANT_ROWS_INFO_SHOW_ROW_IS_REDUNDANT_set_goal info 2 val it = Proof manager status: 4 proofs.
-
Incomplete goalstack: Initial goal: x = 10 ∧ x < 16
Current goal: x = 10
-
Incomplete goalstack: Initial goal: (∀x xs x' xs'. SNOC x xs = SNOC x' xs' ⇔ x = x' ∧ xs = xs') ∧ ((∀x xs. [] ≠ SNOC x xs) ∧ ∀x xs. SNOC x xs ≠ []) ∧ (∀ff x. ff x = list_REVCASE x (ff []) (λx' xs. ff (SNOC x' xs))) ∧ (∀x' f1 f2 x f1' f2'. x' = x ⇒ (x = [] ⇒ f1 = f1') ⇒ (∀x' xs. x = SNOC x' xs ⇒ f2 x' xs = f2' x' xs) ⇒ list_REVCASE x' f1 f2 = list_REVCASE x f1' f2') ∧ ∀x. x = [] ∨ ∃x' xs. x = SNOC x' xs
-
Incomplete goalstack: Initial goal: (∃v0. x = v0 ∧ ¬EVEN x ∧ ¬ODD x) ⇒ ¬∃_0. x = _0
-
Incomplete goalstack: Initial goal: (∃v0. x = v0 ∧ ¬EVEN x ∧ ¬ODD x) ⇒ ¬∃_0. x = _0
> val info' = IS_REDUNDANT_ROWS_INFO_SHOW_ROW_IS_REDUNDANT info 2 ...
val info' =
⊢ IS_REDUNDANT_ROWS_INFO x
[PMATCH_ROW (λ_0. _0) (λ_0. EVEN x) (λ_0. 0);
PMATCH_ROW (λ_0. _0) (λ_0. ODD x) (λ_0. 1);
PMATCH_ROW (λ_0. _0) (λ_0. T) (λ_0. 2)] F
[¬∃_0. x = _0 ∧ EVEN x;
(∃v0. x = v0 ∧ ¬EVEN x) ⇒ ¬∃_0. x = _0 ∧ ODD x; T]: thm
> val thm = IS_REDUNDANT_ROWS_INFO_TO_PMATCH_EQ_THM info'
val thm =
⊢ (pmatch x of _ when EVEN x => 0 | _ when ODD x => 1 | _ => 2) =
pmatch x of _ when EVEN x => 0 | _ when ODD x => 1: thm
Pattern Match Completion
The techniques used for computing redundant rows implicitly
compute a set of missing patterns. The conversion
PMATCH_COMPLETE_CONV
and simpset fragment PMATCH_COMPLETE_ss use this implicitly
computed information to extend case expressions with ARB rows
and thereby produce exhaustive \pmatch{} case expressions. A
flag determines whether these newly introduced rows should use
guards.
> PMATCH_COMPLETE_CONV true ``pmatch (xy : (num option # num option)) of
(SOME x, NONE) when x > 0 => 0 | (NONE, _) => 1``;
val it =
⊢ (pmatch xy of (SOME x,NONE) when x > 0 => 0 | (NONE,_) => 1) =
pmatch xy of
(SOME x,NONE) when x > 0 => 0
| (NONE,_) => 1
| (SOME v2,NONE) when ¬(v2 > 0) => ARB
| (SOME v2,SOME v3) => ARB: thm
> PMATCH_COMPLETE_CONV false ``pmatch (xy : (num option # num option)) of
(SOME x, NONE) when x > 0 => 0 | (NONE, _) => 1``;
val it =
⊢ (pmatch xy of (SOME x,NONE) when x > 0 => 0 | (NONE,_) => 1) =
pmatch xy of
(SOME x,NONE) when x > 0 => 0
| (NONE,_) => 1
| (SOME v2,NONE) => ARB
| (SOME v2,SOME v3) => ARB: thm
Exhaustiveness Checks
Similarly, exhaustiveness can be derived via pattern compilation.
> PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK
``pmatch (xy : (num option # num option)) of
(SOME _, _) => 0 | (_, NONE) => 1 | (NONE, SOME _) => 2``
val it =
⊢ PMATCH_IS_EXHAUSTIVE xy
[PMATCH_ROW (λ(_0,_1). (SOME _0,_1)) (λ(_0,_1). T) (λ(_0,_1). 0);
PMATCH_ROW (λ_0. (_0,NONE)) (λ_0. T) (λ_0. 1);
PMATCH_ROW (λ_0. (NONE,SOME _0)) (λ_0. T) (λ_0. 2)] ⇔ T: thm
Often, the exhaustiveness can be proved much faster by just searching a matching row.
> PMATCH_IS_EXHAUSTIVE_FAST_CHECK ``pmatch (x:num option, y:num) of
(SOME _, _) => 0 | (_, _) => 1``
val it =
⊢ PMATCH_IS_EXHAUSTIVE (x,y)
[PMATCH_ROW (λ(_0,_1). (SOME _0,_1)) (λ(_0,_1). T) (λ(_0,_1). 0);
PMATCH_ROW (λ(_0,_1). (_0,_1)) (λ(_0,_1). T) (λ(_0,_1). 1)] ⇔ T: thm
> PMATCH_IS_EXHAUSTIVE_FAST_CHECK ``pmatch (xy : (num option # num option)) of
(SOME _, _) => 0 | (_, NONE) => 1 | (NONE, SOME _) => 2``
Exception- UNCHANGED raised
Both methods are combined to from PMATCH_IS_EXHAUSTIVE_CHECK.
Another interface to the pattern compilation engine is provided
by SHOW_NCHOTOMY_CONSEQ_CONV.
Exhaustiveness is this time expressed in the form of an nchotomy
theorem. Missing cases are automatically added.
> SHOW_NCHOTOMY_CONSEQ_CONV
``!x:'a list. (x = []) \/ (?e. x = [e]) \/ (?e1 e2 l. x = e1::e2::l)``
val it = ⊢ ∀x. T ⇒ x = [] ∨ (∃e. x = [e]) ∨ ∃e1 e2 l. x = e1::e2::l: thm
> SHOW_NCHOTOMY_CONSEQ_CONV
``!x:'a list. (x = []) \/ (?e1 e2 l. x = e1::e2::l)``
val it = ⊢ ∀x. ¬(∃v1. x = [v1]) ⇒ x = [] ∨ ∃e1 e2 l. x = e1::e2::l: thm
Code Extraction
There is support for \pmatch{} case expressions in EmitML.
However, not all case expressions are supported. Supported case
expressions may only contain constructor patterns and each pattern
variable needs to be used exactly once. Moreover, when extracting
to SML, no guards are allowed.
To check whether a case expression can be exported, the function
analyse_pmatch can be used. The flag of this function
indicates whether an exhaustiveness proof should be attempted.
> val info = analyse_pmatch false
``pmatch l of [] => 1 | [x] when (x > 2) => 2 | _ => 3``
val info =
{pmi_exhaustiveness_cond = NONE, pmi_has_double_bound_pat_vars = [],
pmi_has_free_pat_vars = [], pmi_has_guards = [1], pmi_has_lambda_in_pat =
[], pmi_has_non_contr_in_pat = [], pmi_has_unused_pat_vars = [],
pmi_ill_formed_rows = [], pmi_is_well_formed = true}: pmatch_info
> val sml_ok = is_sml_pmatch info
val sml_ok = false: bool
> val ocaml_ok = is_ocaml_pmatch info
val ocaml_ok = true: bool