History log of /seL4-l4v-master/HOL4/src/1/PmatchHeuristics.sig
Revision Date Author Comments
# 52219a36 09-Jan-2020 Michael Norrish <michael.norrish@data61.csiro.au>

Reformat file to get it under 80 columns


# c3e3e54e 25-Mar-2015 Michael Norrish <Michael.Norrish@nicta.com.au>

Delete trailing whitespace in src/


# 48345816 28-Feb-2015 Thomas Tuerk <thomas@tuerk-brechen.de>

add manual pattern match heuristic / improve exhaustive one

Implement a new pattern match heuristic that allows manually
specifying in which order to do case splits. This one prints
a lot of debugging information in order to allow the user to
make decent choices. The techniques for producing this debug
have also been added to the exhaustive tactic. It now prints
debugging information on how far the exhaustive search
progressed and on intermediate results


# 8d315d0c 09-Dec-2014 Michael Norrish <michael.norrish@nicta.com.au>

Delete trailing whitespace in src/

This needs doing periodically, and is best done to a whole bunch of files
at once.


# d814567b 08-Aug-2013 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Fallback on "classic" cases heuristic when Induction.mk_induction raises an exception. This closes issue #127.


# 1d91518a 15-Apr-2013 Thomas Tuerk <tt291@cl.cam.ac.uk>

cleanup of Pmatch

Following a suggestion of Anthony, I cleaned-up the interface of Pmatch.
To this end, I moved much of the heuristics-code to a new library called
PmatchHeuristics. This new library is used by Pmatch. This allows to
clean-up the code and interface of Pmatch. If less frequently used functions
are needed, the library PmatchHeuristics has to be used now.