#
95d60bd3 |
|
02-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove -- as an alias for Term parser. As per comment in release notes this has long been replaced as appropriate style.
|
#
0d994131 |
|
30-Jul-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Clean quotient examples: now use core Mutual lib, rather than own copy This is a start, of sorts, on having a go at github issue #10
|
#
0bbd2a7e |
|
21-Jun-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Rename TruePrefix to Prefix; use fixity options with NONE for what was Prefix. 90+% of this work was done by Ramana Kumar. The following list are the commits for a series of individual commits that have been squished into one big change: * remove mention of TruePrefix from the add_rule docfile * first batch of changes removing TruePrefix from src/parse * replace TruePrefix by Prefix in boolScript.sml * remove TruePrefix from Rsyntax is a fixity ever required for new_specification? * some more Prefix -> NONE and TruePrefix -> Prefix in theories * TruePrefix changes for datatype * TruePrefix changes for res_quan * TruePrefix->Prefix in a TeX selftest * TruePrefix changes for quotient * TruePrefix changes for integer and real * fix quotient examples for TruePrefix removal * more fixes for quotient examples * fixes for lambda example for TruePrefix removal * Reword description manual in light of removal of TruePrefix. * Fix msgTheory quotient example; Poly 5.3 had problems with monotypes. * Fixes for files in examples/lambda given removal of TruePrefix. * Fix in examples/unification given removal of TruePrefix. * Fix in examples/HolCheck given removal of TruePrefix. * Fixes in examples/acl2 given removal of TruePrefix.
|
#
d653fb1c |
|
11-Feb-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement unary minus (the old ~ still also works). Selftest level 2 passes. Changes in the "words world" were replacing $- with -. In the two quotient changes, I made sure that the infix operator that used the - character was part of the grammar before it was parsed. This is necessary because - is now a non-aggregating character, mainly so that ``--p`` parses as three tokens, not two. Of course, if you added -- to your grammar, then it would go back to parsing as two.
|
#
968c06bb |
|
28-Nov-2008 |
Peter Homeier <palantir@trustworthytools.com> |
A bug in the quotient package was exposed by the recent change in the representation of strings to be lists of characters. The bug was that when the package calculated quotient theorems (or equivalence theorems) for a given type, it would develop the resulting theorem according to the recursive structure of the type, within all type operators for which a conditional quotient theorem had been provided. This went too far when the type operator was being used on argument types not being lifted, as here with ``:string`` which is now ``:char list``. The following two functions of the quotient package have had their signatures modified: val make_equiv : Thm.thm list -> (* base equivalence theorems *) Thm.thm list -> (* polymorphic type operator equivalence theorems *) Type.hol_type -> (* type, whose equivalence relation is desired *) Thm.thm (* returns equivalence theorem for hol_type: !x y. R x y = (R x = R y) *) val make_quotient : Thm.thm list -> (* quotient theorems for primary lifted types *) Thm.thm list -> (* conditional quotient ths for type operators *) Type.hol_type -> (* type (not lifted) of desired quotient *) Thm.thm (* returns quotient theorem for given type: (!a. abs (rep a) = a) /\ (|x y. R x y = (abs x = abs y)) *) Previously the first two arguments of each function were just one argument, as the concatenation of the two arguments here. Distinguishing between the two lists permits the easy recognition of when a type operator is being applied to type arguments which are not being lifted. Now "build -selftest" works for the current version of Kananaskis-5. Many thanks to Michael Norrish for pointing out this bug!
|
#
d9003833 |
|
26-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fairly dramatic change, supporting the use of "syntactic patterns". It is now possible to overload a name to term (typically a lambda-abstraction) in order to create syntax-only definitions. For example, there is a definition of not-equals now in the system: val _ = overload_on ("<>", ``\x y. ~(x = y)``) val _ = set_fixity "<>" (Infix(NONASSOC, 450)) This definition is parsed and pretty-printed. Two other annoying changes. The interface for adding unicode variants has changed, and I have made precedence level 450 of the parser non-associative. This latter change has caused most of the (minor) adjustments to the files below. The regression test doesn't go through yet. (Currently there is a failure in quotient/examples/sigma that I don't understand.)
|
#
ef58dbeb |
|
19-Jun-2008 |
Peter Homeier <palantir@trustworthytools.com> |
Revised quotient package to use proofManagerLib instead of goalstackLib.
|
#
4dd0a94b |
|
18-Mar-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
A proof in quotient/examples/sigma/liftScript.sml breaks under the experimental kernel thanks to a particular choice of bound name (the two kernels don't always agree). Fix the proof to be more robust in the face of differences like this.
|
#
da2c39e1 |
|
24-Aug-2007 |
Peter Homeier <palantir@trustworthytools.com> |
Revised one of the quotient examples (sigma calculus) which broke with recent changes to the TFL package.
|
#
61977fd2 |
|
06-Oct-2006 |
Peter Homeier <palantir@trustworthytools.com> |
---------------------------------------------------------------------- Committing in a fix to a bug in the quotient library example for the sigma calculus. Modified Files: liftScript.sml ----------------------------------------------------------------------
|
#
c20e5e83 |
|
24-Jun-2005 |
Peter Homeier <palantir@trustworthytools.com> |
---------------------------------------------------------------------- Committing in a revised version of the quotients package, where now erroneous input theorems are usually detected early, and the erroneous theorem listed in an error message. This should greatly improve the usability of the package, especially for new users. Thanks to Michael Norrish for prodding me on this one. Also added a new version of finite sets from lists, due to Michael Norrish. Also moved the "obj" directory to now be called "sigma"; this contains the sigma calculus example from Abadi and Cardelli, as described in the longer 45-page paper. Modified Files: hol98/src/quotient/examples/finite_setScript.sml hol98/src/quotient/src/quotient.sml hol98/src/quotient/src/quotientScript.sml Added Files: hol98/src/quotient/examples/ext_finite_setScript.sml hol98/src/quotient/examples/sigma/MutualIndThen.sig hol98/src/quotient/examples/sigma/MutualIndThen.sml hol98/src/quotient/examples/sigma/alphaScript.sml hol98/src/quotient/examples/sigma/barendregt.sig hol98/src/quotient/examples/sigma/barendregt.sml hol98/src/quotient/examples/sigma/ind_rel.sig hol98/src/quotient/examples/sigma/ind_rel.sml hol98/src/quotient/examples/sigma/liftScript.sml hol98/src/quotient/examples/sigma/more_listScript.sml hol98/src/quotient/examples/sigma/more_setScript.sml hol98/src/quotient/examples/sigma/objectScript.sml hol98/src/quotient/examples/sigma/reductionScript.sml hol98/src/quotient/examples/sigma/semanticsScript.sml hol98/src/quotient/examples/sigma/tactics.sig hol98/src/quotient/examples/sigma/tactics.sml hol98/src/quotient/examples/sigma/variableScript.sml Removed Files: hol98/src/quotient/examples/obj/MutualIndThen.sig hol98/src/quotient/examples/obj/MutualIndThen.sml hol98/src/quotient/examples/obj/alphaScript.sml hol98/src/quotient/examples/obj/barendregt.sig hol98/src/quotient/examples/obj/barendregt.sml hol98/src/quotient/examples/obj/ind_rel.sig hol98/src/quotient/examples/obj/ind_rel.sml hol98/src/quotient/examples/obj/liftScript.sml hol98/src/quotient/examples/obj/more_listScript.sml hol98/src/quotient/examples/obj/more_setScript.sml hol98/src/quotient/examples/obj/objectScript.sml hol98/src/quotient/examples/obj/reductionScript.sml hol98/src/quotient/examples/obj/semanticsScript.sml hol98/src/quotient/examples/obj/tactics.sig hol98/src/quotient/examples/obj/tactics.sml hol98/src/quotient/examples/obj/variableScript.sml ----------------------------------------------------------------------
|