#
a424d55e |
|
09-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
licenses: convert license tags to SPDX
|
#
5120e351 |
|
04-Nov-2019 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: improve wp tracing When tracing wp can now print the instantiated version of the rules being used. It also says which set each used rule is from.
|
#
96588daf |
|
17-Jul-2019 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: improve message printing for crunch and wp, and refactor common printing functions
|
#
f757e0ca |
|
06-May-2019 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: wp cleanup and parser improvements The main visible change is from wp_trace', 'wp_once' and 'wp_once_trace' to 'wp (trace)', 'wp (once)' and 'wp (once, trace)'. The option for printing a warning for unused supplied wp rules has also been removed.
|
#
a70aeda3 |
|
21-Jan-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
lib: Datatype_Schematic and WPFix. Add two new tactics/methods which can fix common painful problems with schematic variables. Method datatype_schem improves unification outcomes, by making judicious use of selectors like fst/snd/the/hd to bring variables into scope, and also using a wrapper to avoid singleton constants like True being captured needlessly by unification. Method wpfix uses strengthen machinery to instantiate rogue postcondition schematics to True and to split precondition schematics that are shared across different sites.
|
#
7bff086f |
|
18-Jan-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
lib/wp: Slight cleanup in WP-method.ML
|
#
796887d9 |
|
11-Jul-2017 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Removes all trailing whitespaces
|
#
3dd496f4 |
|
10-Mar-2017 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
wp: separate wp_pre method, used in wp and wpc
|
#
905f8e6f |
|
18-Dec-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
apply_debug: discard context modifications Demotes "break" to a regular tactic, simplifying its integration with other tools
|
#
e240f0b0 |
|
13-Dec-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
apply_debug: support context modifications in wp Rebuild the ruleset if the context changes during execution. This allows breakpoints to modify the wp set (during a given execution), although this does not survive outside of the method.
|
#
7250bd1a |
|
13-Dec-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
apply_debug: add "wp" breakpoint Lift low-level wp tactic into context_tactic to support breakpoints modifying context (i.e. wp set)
|
#
063602d8 |
|
13-Jan-2017 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
wp: more constrained behaviour - restrict to one goal (no fall-through) - apply a wp_pre rule if there is no schematic in the goal - apply trivial cleanup rules at the end
|
#
92139db6 |
|
25-May-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
autolevity: refine tracing apply everywhere to work via Proof module hooks This avoids doing redundant tactic operations at the top-level and lets us trace "by" statements easily.
|
#
84b923a6 |
|
17-Apr-2016 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
lib: start disentangling spaghetti word dependencies
|