#
5c272847 |
|
28-Jun-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Add flip as an alias for combin$C
|
#
44aabdd8 |
|
01-Oct-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add some extra automatic rewrites to do with function update Also make sure that rewrites in COMBIN_ss are named so that they can be excluded from simplification tactics if necessary.
|
#
eee03790 |
|
05-Mar-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make equality of "tight" precedence by default Start to work through knock-on effects of this.
|
#
782dc480 |
|
06-Dec-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Pretty-print the new fn-update syntax (e.g., f⦇k ↦ v; x ↦ y⦈) With a selftest. This is the function half of github issue #616. Finite maps still to come.
|
#
ab2c9d3b |
|
04-Dec-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
First steps towards parsing f ⦇ d1 ↦ r1; d2 ↦ r2 ⦈ for fn. UPDATE The ASCII version of the same is f (| d1 |-> r1; d2 |-> r2 |) and of course, the old (d1 =+ r1) ((d2 =+ r2) f) can also be used. The pick of ⦇ ... ⦈ precludes using the same parentheses for s-expressions in the example of the same name (hence the changes in that example). The use of (| |) means that (||) no longer parses as paren-escaping the || operator (hence the change to wordsScript.sml). Pretty-printing still to be done.
|
#
18b6cc8c |
|
26-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix for (new, pretty branch) bug causing computeLib failures with K
|
#
b72e391c |
|
20-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Move smpp to Portable - get everything up to arithmeticScript working
|
#
838f97d0 |
|
19-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Up to core types
|
#
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.
|
#
1f5dfc44 |
|
08-Sep-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove "C" from combinTheory.combin_grammars Currently, combinTheory is set up to hide C from the global grammar when it is loaded, but to leave C in combinTheory's own grammar, which you get via writing things like combinTheory.combin_grammars. This is weird. To make things more consistent, pull C out of combin's grammar properly (without having to use adjoin_to_sml), and have it absent in both descendants, and in combin_grammars. Of course, the standard trick of typing reveal "C" makes it visible again. The code in src/metis/normalForms.sml used this visibility when stating and proving a rewrite about C. This was fixed simply by making the statement use the combin$C notation.
|
#
c2ef1d87 |
|
15-Aug-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Merge operatorTheory into combinTheory This was far too small a theory to live an independent existence. It was included by listTheory so the constant name-space contamination isn't any different for eventual clients.
|
#
6b95018c |
|
21-Feb-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make U+2218 (∘) alternative syntax for combin$o Also bind C-S-0 0 as Emacs keybinding to generate it.
|
#
d0b76345 |
|
01-Nov-2015 |
Ramana Kumar <ramana@member.fsf.org> |
update OpenTheory names for combinTheory constants
|
#
e4576049 |
|
11-Mar-2015 |
Michael Norrish <michael.norrish@nicta.com.au> |
Make 'o' map to existing \HOLTokenCompose in TeX_notation map. Closes #242
|
#
08d7a558 |
|
23-Oct-2014 |
Piotr Trojanek <piotr.trojanek@gmail.com> |
trailing newlines in *.{sml,sig} files from src/ removed Trailing newlines from SML files in src/ were rendered in HTML documentation.
|
#
d16d4401 |
|
30-Nov-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add conversion updateLib.UPDATE_APPLY_CONV.
|
#
66d40728 |
|
12-Feb-2012 |
Ramana Kumar <ramana.kumar@gmail.com> |
update OpenTheory names for combinators to new standard
|
#
81a935b9 |
|
08-Feb-2012 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add new rewrite about abstractions and function composition. This one parallels the existing o_ABS_R. To my surprise, the simplifier currently preserves bound variable names when this rewrite is applied, even though the two x's can well be of different types, and thus different bound variables in a pretty strong sense. For example, SIMP_CONV (srw_ss()) [o_ABS_L] ``(\b. b /\ p) o FST`` gives back |- (λb. b ∧ p) o FST = (λb. FST b ∧ p) The b on the left is a boolean, the b on the right is a pair. This is a bit odd, perhaps even a bug. When the types are the same this is clearly the right thing, but still. The bug, if it is one, will be in the implementation of HO_PART_MATCH.
|
#
c49ade53 |
|
08-Feb-2012 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove structure-struct/end bracketing from combinScript.sml.
|
#
1ceedff5 |
|
27-Oct-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
add OpenTheory name for combin$K
|
#
f8fd8324 |
|
02-Oct-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
add various names to the OpenTheory map This is in preparation for logging llistTheory. Notes: - Sent combin$C to Function.Combinator.c (same for combin$S). Another name might be preferred on the OpenTheory side. - Not sure what bool$BOUNDED is about; dumped it in the HOL4 namespace. - Put lots of pred_set constants in the Set namespace, but in the standard (OpenTheory) library it seems like Set is for constants operating on an abstract type of sets (rather than predicates). I'm not sure whether we should use a different namespace when working with sets-as-predicates or just pretend predicates are the abstract type and do a bit of magic on article reading/writing as necessary (don't know what that would be exactly yet). - Similar for constants in set_relation, which I'm currently putting in the Relation namespace. Although it looks like currently OpenTheory doesn't use an abstract type of relations (but probably it will later). - Sent marker$Cong and marker$Abbrev to Unwanted.id, but not sure if Unwanted.id is supposed to be polymorphic (whereas those are identity functions restricted to bool). Similar for numeral$iZ - sent GSPEC to Set.specification; maybe not an obvious name... - Using top-level "While" namespace for whileTheory - dumped numeral$iiSUC in HOL4 namespace; not sure what to do with it - BIT2 is going to Number.Numeral.bit2; this is in line with wanting the base library to be liberal, i.e. a union of all useful basic constants and theorems (so has bit0, bit1 and bit2)... but I think there may be competing goals for base
|
#
1af7dc8b |
|
16-Sep-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
better match intended semantics of OpenTheory names rather than using strings, now have a type abbreviation otname for string list * string. it might be worth writing more operations on this type (like for manipulating the namespace).
|
#
dc4085a7 |
|
07-Sep-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
add OpenTheory name for combin$I
|
#
e6010675 |
|
04-Dec-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add the useful |> combinator to combinTheory. Had to be ":>" because "|>" is already used for records. If anyone doesn't like the name "APP" then feel free to change it.
|
#
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!
|
#
168f13e5 |
|
01-Feb-2009 |
Scott Owens <Scott.Owens@cl.cam.ac.uk> |
Started moving EmitML code out of source scripts and into a single source script "libraryScript.sml" in src/emitScript, adding calls to emitCAML alongside the emitML calls in libraryScript.sml.
|
#
04aca7c3 |
|
03-Nov-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Replaced o_DEF with o_THM in "the_compset". This fixes a problem when evaluating record updates (and it also provides consistency with srw_ss()). For example: EVAL ``<| f := r |> with f := x``; produces ``<|f := x|>`` instead of ``<|f updated_by (\x'. x)|>``
|
#
46d9ec8c |
|
08-Feb-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
At the behest of Konrad and Michael, SUBST is now called UPDATE. Also, it has been moved into combinTheory (even though it is not a combinator). Unfortunately, the symbol ``:-`` has had to be abandoned because this is used in labelTheory. The new symbol is ``=+``. Without the use of METIS, the theorems have been proved the long way. The theorems are renamed to fall in line with the those of FUPDATE from finite_mapTheory: SUBST_EVAL -> APPLY_UPDATE_THM SUBST_NE_COMMUTES -> UPDATE_COMMUTES SUBST_EQ -> UPDATE_EQ Also: SUBST_IMP_ID -> UPDATE_APPLY_IMP_ID SUBST_ID -> APPLY_UPDATE_ID Some more theorems (again similar to those of FUPDATE) have been added: UPDATE_APPLY_ID UPD11_SAME_KEY_AND_BASE UPD11_SAME_BASE UPD_SAME_KEY_UNWIND SAME_KEY_UPDATE_DIFFER
|
#
e582ce4c |
|
02-Oct-2006 |
Peter Homeier <palantir@trustworthytools.com> |
---------------------------------------------------------------------- Committing in additional theorems to aid in SRW_TAC's use of the new literal patterns. Bug found by Anthony Fox. Modified Files: combinScript.sml ----------------------------------------------------------------------
|
#
0d230e40 |
|
23-Jul-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Another of my changes to the filter removed what I thought was unnecessary code for handling the old-fashioned --`...`-- syntax for terms and types. But it turns out this code is necessary if Parse isn't around. Easiest fix: opening Parse.
|
#
5c8f5906 |
|
22-Jun-2006 |
Konrad Slind <konrad.slind@gmail.com> |
Minor changes and bugfixes to ML code generation. Have renamed EmitML.exportML to EmitML.emitML, since exportML is used in SML/NJ to dump the image. Also renamed Globals.exportMLPath to Globals.emitMLDir (since it's a directory and not a path). Also fixed bug in code generated for constructors and tuples.
|
#
adf911c8 |
|
25-Jul-2005 |
Konrad Slind <konrad.slind@gmail.com> |
Revised exportML so that it takes a path parameter, which tells where the ML corresponding to a theory is to be written. This has been propagated to all the theories that already export ML, and the mkword.exe tool has been upgraded to also take a path where it should write the generated ML. This is useful, because doing an exportML to the same directory as the theory files will end up confusing Holmake.
|
#
138d26bb |
|
04-Aug-2004 |
Konrad Slind <konrad.slind@gmail.com> |
ML code generation for finite_map now added. Also, a whole host of minor changes and robustifications have been applied.
|
#
61d5a40a |
|
27-Jul-2004 |
Konrad Slind <konrad.slind@gmail.com> |
Added new combinator called FAIL, which is equal to K. FAIL is used to generate exception-raising code when translated to ML. For example HD [] = FAIL HD ^(mk_var("Empty list",bool)) [] which is provable since FAIL x y = x. The translator to ML will convert FAIL terms so that the above is HD [] = raise Fail "HD: Empty list"
|
#
fadeb16c |
|
09-Jul-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
New entry point in BasicProvers called LET_ELIM_TAC to do lovely things with lets, whether uncurried or not. They're lifted out of the goal and turned into abbreviations into the assumptions. Plan is to tack LET_ELIM_TAC into the basic action of RW_TAC and SRW_TAC as well.
|
#
ce9b6fbf |
|
04-Jul-2004 |
Konrad Slind <konrad.slind@gmail.com> |
Export ML from combin theory. The exported ML ends up in the directory src/theoryML.
|
#
bb654e4b |
|
26-Jun-2003 |
Konrad Slind <konrad.slind@gmail.com> |
Many small changes, most associated with boolification or lifting.
|
#
2eaf3bfa |
|
16-Feb-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Prove a cute little theorem about the K combinator. This is a necessary prelude to one last change I'm contemplating to make record type definition roughly twice as fast as it is at the moment. The change to relationScript makes it explictly depend on combinTheory, something the automatic dependency analysis can't figure out on its own.
|
#
75372e93 |
|
28-May-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Overlay.sml now exports infix declarations for the "standard" infixes, taken from std.prelude. This means that the infix component of the standard Script boilerplate is unnecessary. Updated Manual documentation to reflect this. Changed combinScript and examples/ind_def/clScript.sml just to show that it worked.
|
#
77efd725 |
|
04-Feb-2001 |
Konrad Slind <konrad.slind@gmail.com> |
New work aimed at making a single global EVAL function, with an underlying compset.
|
#
21d45a6e |
|
05-Jan-2001 |
Konrad Slind <konrad.slind@gmail.com> |
Minor changes.
|
#
069f20bc |
|
30-Nov-2000 |
Konrad Slind <konrad.slind@gmail.com> |
Made sure that the combinator "C" is hidden by default. This will prevent surprises in developments that already use "C" as a variable. In principle I should do the same for "W" ...
|
#
c8540e87 |
|
12-Nov-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Kananaskis compatibility; addition of C and W combinators.
|
#
0058df84 |
|
28-Jun-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixed to bring it up to date with Taupo release 0. (Changes have come across from parse_branch development.)
|
#
caf74236 |
|
29-Apr-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Initial revision
|