#
1728d8b9 |
|
16-Jul-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make PAT_ABBREV_TAC aware of hidden/revealed status of "constants" In particular, use gen_variant Parse.is_constname rather than variant. The latter avoids generating names that clash with constants in the logical signature. The former only avoids those names that the *parser* thinks of as constants. This is better for user-facing code such as PAT_ABBREV_TAC. Closes #431
|
#
923e92e2 |
|
03-Nov-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
MATCH_ABBREV tactics now ignore _ in patterns Tactics affected are - MATCH_ABBREV_TAC - HO_MATCH_ABBREV_TAC - MATCH_ASSUM_ABBREV_TAC Documented and self-tested
|
#
32b250e5 |
|
10-Jun-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Q.PAT_ABBREV_TAC fails rather than bind a bound variable Documentation updated. Previous behaviour would be to attempt to bind a bound variable in an abbreviation and end up creating a vacuous abbreviation. Closes #262
|
#
70bcf8ef |
|
25-May-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Let PAT_ABBREV_TAC use patterns that are more polymorphic than the goal Closes #252
|
#
42c88489 |
|
15-Jan-2015 |
Michael Norrish <michael.norrish@nicta.com.au> |
Fix bugs in Q's match_{rename,abbrev} tactics; refine spec. In particular, make sure that instantiations arising from the matches are applied in an order that is sure to make the substitutions apply as much as possible. There are two obvious ways in which things can go wrong (resulting in a goal-term that doesn't in fact look like the supplied pattern). 1. If the match results in an instantiation that has a variable binding a term that appears within another. E.g., (example from Ramana): Q.MATCH_RENAME_TAC `f v = z` (?- `f (h s) = s`) The match will return (v |-> h s, z |-> s), but if this is applied with the z going first, the goal won't contain `h s` when the substitution for v is attempted. So that's bad, and affects both renaming and abbreviating tactics. The fix is to sort the instantiation list so that larger terms are substituted out first. 2. Distinct variables in the pattern may end up binding the same term. This is something users are less likely to bring about, but it still seems worth trying to nail down what the behaviour should be. E.g., Q.MATCH_RENAME_TAC `a + b = 10` (?- 5 + 5 = 10) This will want to bind a and b to 5. When abbreviating, you might like to see abbreviations `a = 5` and `b = 5` in the assumptions, and when renaming or abbreviating, you might like to have the goal become `a + b = 10`. Achieving both these might be possible, but seems hard. Instead, the operational approach of performing substitutions in a sequence is stuck to, but the substitution is sorted so that the variable with the earlier name goes first. This means you'll get ?- a + a = 10 as the goal, and when abbreviating, you'll get `a = b` and `b = 5` as abbreviations in the assumptions. The fixes in examples/ are generally because proofs have relied on abbreviations *not* occurring, despite the presence of variables in the pattern. The situation is analogous to the situation in 1. above, where the user has exploited the fact that a binding hasn't been introduced for v.
|
#
a6bf2df4 |
|
06-Aug-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Document Q.PAT_ABBREV_TAC. Also flip the default setting of "PAT_ABBREV_TAC: match var/const". Warning: this change will break proofs that are sensitive to (rely on) the current behaviour of PAT_ABBREV_TAC. See commits c5c281b, e824426, and a373506; and issue #79.
|
#
c5c281bd |
|
03-Aug-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add a configuration trace flag "PAT_ABBREV_TAC: match var/const", which should close Issue #79. This flag is false by default. When set (by set_trace or trace) it enables PAT_ABBREV_TAC to match on variables and constants (which is not always desirable). Setting the flag can break existing proofs, e.g. the ARM6 correctness proof fails when more matches are permitted.
|
#
cd8db029 |
|
12-Jul-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement a simple tactic to undo Abbrev in assumptions. Suggested by Magnus, this tactic turns all assumptions of the form Abbrev (t1 = t2) into t2 = t1
|
#
da827655 |
|
27-Feb-2010 |
Ramana Kumar <ramana.kumar@gmail.com> |
Added MATCH_ASSUM_ABBREV_TAC to Q and markerLib. This completes the set of pattern-matching tactics spanning the two dimensions of abbreviate/rename and conclusion/assumptions.
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
c76376ed |
|
29-Apr-2008 |
Konrad Slind <konrad.slind@gmail.com> |
Additional functionality for abbreviations. 1. The labels library has been merged into markerLib and the src/labels directory eliminated. 2. Have added markerSyntax structure. 3. Operations on abbrevs used to all be in structure Q, even those that didn't deal with quotations (like UNABBREV_ALL_TAC). Now markerLib provides all abbrev. operations and these take terms. Operations that benefit from quotes, e.g., ABBREV_TAC, MATCH_ABBREV_TAC, etc. are still to be found in Q. 4. Abbrevs are kept reduced by the simplifiers and there is a REABBREV_TAC which can be separately called. This sorts abbrevs topologically, so that they get restored in a sensible order. 5. For situations where one wants to get rid of all abbrevs, apply a tactic, and then restore the abbrevs, there is WITHOUT_ABBREVS: tactic->tactic. 6. Have added a simple topological sort to Lib. 7. Updated proofs in the src directories, and also in examples/lambda.
|
#
3890ad80 |
|
21-Apr-2008 |
Konrad Slind <konrad.slind@gmail.com> |
Changed behaviour of simplifier to propagate the abbreviation coming from a let binding in the goal being moved to the assumptions. This helps keep the goal in "fully abbreviated form". Also added Q.REABBREV_TAC which re-abbreviates the goal and Q.WITHOUT_ABBREVS tac which temporarily removes all abbreviations, runs tac, then reabbreviates. Probably, Q is not the right place for these functions, but the rest of the abbreviation stuff is there. Also added some internal documentation on what Q.ABBRS_THEN does, and the like.
|
#
007e43f2 |
|
31-May-2005 |
Konrad Slind <konrad.slind@gmail.com> |
Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type in the quotation pre-processor. A mass of trivial changes, but the new way of dealing with files containing code that does parsing (not script files) is to * grab the ambient grammar(s) * set the current grammar(s) to the right values for parsing quotations in the file * the body of the file * reset the current grammar to the ambient grammar For an example, see src/taut/tautLib.sml
|
#
c0732b6e |
|
18-Aug-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
A little code reorganisation and a fix for a bug in the implementation of ASM_SIMP_TAC and FULL_SIMP_TAC: abbreviation references in the argument list weren't being dealt with early enough. In the case of ASM_SIMP_TAC this caused the effect of an abbreviation being eliminated in the assumptions but not in the goal.
|
#
1d04a0ca |
|
07-Jul-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
New treatment of abbreviations. Documentation still to be updated. Backwards compatibility illustrated in examples/lambda/standardisationScript and examples/arm6. New techniques and entry-points illustrated in core distribution and some of the lambda example scripts.
|
#
218d4c24 |
|
03-Jul-2003 |
Konrad Slind <konrad.slind@gmail.com> |
Minor changes to support simpLib upgrade.
|
#
d94b8bf3 |
|
01-Jul-2003 |
Konrad Slind <konrad.slind@gmail.com> |
Support for rewriting annotations.
|
#
e234dcdc |
|
23-Mar-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Got rid of QConv, and made all conversions do the "raise exception to indicate reflexivity" thing. (Also fixed bug in new implementation of ABS_CONV that attempted renaming on failure of conv, and not just failure of ABS.) Next step will be to rework the simplifier's implementation so that it also uses Conv.UNCHANGED, rather than in its own internal version of the same. This will let the simplifier play efficiently with others. May also assess making ABS_CONV not do renaming, and give the rewriter its own special traverser. This might make some things more efficient.
|
#
3c544fd5 |
|
14-Dec-2001 |
Konrad Slind <konrad.slind@gmail.com> |
Minor conflict resolved.
|
#
cfbfad32 |
|
10-Dec-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixed with structure ... end bracketting to protect it from the evils of the W2K file-system.
|
#
c17424b3 |
|
07-Dec-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Moved marker stuff to its own directory, and also used same_const function in new markerLib. In a far off, distant land, where we implement named assumptions using Konrad's NAMED constant (see src/basicProof/Notes), this stuff will need to put back into bool so that the basic tactics can be made to work with named assumptions.
|