Hi Christian,
> Thanks for pointing this out. While yours is a valid observation, it
> seems that observing "abbrev_mode" is not enough to obtain nicer output,
> i.e., when using
>
> fun uncheck ctxt ts =
> - if Config.get ctxt show_variants orelse exists (is_none o try
> Term.type_of) ts then
On 01/28/2015 06:15 PM, Florian Haftmann wrote:
fun uncheck ctxt ts =
- if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of)
ts then ts
+ if Proof_Context.abbrev_mode ctxt orelse
+Config.get ctxt show_variants orelse
+exists (can Term.type_of) ts then ts
> fun uncheck ctxt ts =
> - if Config.get ctxt show_variants orelse exists (is_none o try
> Term.type_of) ts then ts
> + if Proof_Context.abbrev_mode ctxt orelse
> +Config.get ctxt show_variants orelse
> +exists (can Term.type_of) ts then ts
>else map (insert_overloaded ctxt) ts;
N
Oops! You are right, of course. I was so delighted to see the nice
output for my example that I completely forgot about checking whether
previously "correct" results of adhoc overloading are still okay.
Thanks for testing and your report! I will have to investigate further ...
cheers
chris
O
Hi,
after looking a little bit closer at the proposed patch, I doubt that it
has the desired effect: it basically disables the uncheck phase almost
always (e.g. for term and lemma). Consider:
consts T :: 'a
adhoc_overloading T True
declare[[show_variants = false]]
term T
The term command wil
Hi Chris,
I've pushed it to the testboard (and will push it to the repository in
case of success):
http://isabelle.in.tum.de/testboard/Isabelle/rev/0d7de4d99eac
Cheers,
Dmitriy
On 28.01.2015 09:55, Christian Sternagel wrote:
It is amazing how easy some things get when a wizard is looking ove
It is amazing how easy some things get when a wizard is looking over
your shoulder (thanks Florian!). It turns out that adhoc overloading
(which is in essence very similar to abbreviations) did not observe some
conventions that are followed by the "abbreviation" command.
By peeking into the so
Here is a related thread
https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04950.html
which was originated by myself ;) (how embarassing).
cheers
chris
On 01/16/2015 02:35 PM, Christian Sternagel wrote:
Dear all,
in Isabelle2014 as well as c7f6f01ede15 I notic
Dear all,
in Isabelle2014 as well as c7f6f01ede15 I noticed that the output when
using adhoc overloading together with abbreviations is not optimal
(maybe this was already discovered before but I forgot about it). Now,
it turns out that the same issue (at least superficially it's the same,
bu
On Sat, 1 Feb 2014, Makarius wrote:
If not, could one of the devs incorporate this tiny change please?
OK, I will try this out.
See now:
changeset: 55237:1e341728bae9
user:wenzelm
date:Sat Feb 01 20:46:19 2014 +0100
files: src/Tools/adhoc_overloading.ML
description:
On Sat, 1 Feb 2014, Christian Sternagel wrote:
So my idea was to instead use top-down rewriting (i.e., first replace
maximal subterms that fit a given pattern). This is what
"Pattern.rewrite_term_top" does, right? So after replacing
"rewrite_term" by "rewrite_term_top", I get the expected resu
Dear all,
recently I was working a lot with adhoc_overloading. Doing so I often
experienced that my output differed from my input (w.r.t. adhoc
overloading). At that time I did not think too much about it since being
able to input readable formulas was quite enough. But today I suddenly
had a
On Tue, 6 Aug 2013, Christian Sternagel wrote:
Please find attached a file containing all my changes.
OK, this is now at Isabelle/73e32ed924b3 and a few changes before.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://m
Dear Makarius,
actually even more is missing, since I was not able to properly use "hg
export" (I am used to "hg bundle" which "exports" *all* changesets that
are only local, whereas for "hg export" I have to give all revisions
that should be exported explicitly). Sorry for that. Please find
On Fri, 2 Aug 2013, Christian Sternagel wrote:
On 08/02/2013 12:04 AM, Makarius wrote:
On Wed, 17 Jul 2013, Christian Sternagel wrote:
in case anybody finds localized ad-hoc overloading useful.
Quite often it is just a matter to tell users about the existence of
such useful tools.
Do you f
On 08/02/2013 12:04 AM, Makarius wrote:
On Wed, 17 Jul 2013, Christian Sternagel wrote:
in case anybody finds localized ad-hoc overloading useful.
Quite often it is just a matter to tell users about the existence of
such useful tools.
Do you feel like making an example theory, e.g.
src/HOL/e
On Wed, 17 Jul 2013, Christian Sternagel wrote:
in case anybody finds localized ad-hoc overloading useful.
Quite often it is just a matter to tell users about the existence of such
useful tools.
Do you feel like making an example theory, e.g.
src/HOL/ex/Adhoc_Overloading_Examples.thy or a
On Wed, 17 Jul 2013, Christian Sternagel wrote:
Here are two follow-up patches (this time generated by "hg export") that
improve error messages for multiple instances (actually showing the
existing instances to the user).
I have imported them as 72cda5eb5a39 and 1e13b2515e2b.
BTW, the log me
On Wednesday, July 17, 2013 at 13:43:34 (+0900), Christian Sternagel wrote:
>
> @all: please let me know, in case anybody finds localized ad-hoc
> overloading useful.
>
> An aside: I'm currently using localized ad-hoc overloading for a port of
> Nominal2's permutation type, where I use
Dear Makarius,
thanks for applying the patch. Here are two follow-up patches (this time
generated by "hg export") that improve error messages for multiple
instances (actually showing the existing instances to the user).
cheers
chris
@all: please let me know, in case anybody finds localized
On Fri, 12 Jul 2013, Christian Sternagel wrote:
The patches should be ready to push (for your convenience I attached them
once more; the attached patches are the same as from my previous e-mail).
Btw, I generated the patches against Isabelle 8afb396d9178 and AFP
908304753f7d (but I guess this
The patches should be ready to push (for your convenience I attached
them once more; the attached patches are the same as from my previous
e-mail). Btw, I generated the patches against Isabelle 8afb396d9178 and
AFP 908304753f7d (but I guess this information is also included in the
patches ;)).
On Fri, 12 Jul 2013, Makarius wrote:
On Fri, 12 Jul 2013, Christian Sternagel wrote:
Dear all,
please find attached patches for localizing
src/Tools/Adhoc_Overloading.thy.
I will take care to apply the changesets to Isabelle and AFP.
Looking closer, I see several versions of patches. Ar
On Fri, 12 Jul 2013, Christian Sternagel wrote:
Dear all,
please find attached patches for localizing src/Tools/Adhoc_Overloading.thy.
I will take care to apply the changesets to Isabelle and AFP.
(Later there might be more tips coming about the implementation
techniques, but I first need t
Dear all,
please find attached patches for localizing
src/Tools/Adhoc_Overloading.thy. It should work like the previous
version in the non-local case, besides a more convenient interface,
i.e., instead of
setup {*
Adhoc_Overloading.add_overloaded @{const_name foo}
#> Adhoc_Overload
Dear all,
here is an update to my previous message. Corresponding patches are
attached (tested with `isabelle build_doc -pa` and `isabelle afp_build -A`).
Some comments:
1) Variants are stored as terms but where all types are mapped to
"dummyT" (which makes it easier to check for a given ter
First of all, thanks for all the useful answers and sorry for my late
reply (I visited a conference and had some holidays ;)). As Alexander
suggested, I first tried to modify the existing adhoc_overloading.ML in
such a way that variants may be arbitrary terms. Please find the results
of my atte
>> There is no point to do
>> such low-level optimizations in the syntax layer. It is for hardcore
>> kernel operations only
>
> So should I manually check the result for equality, or does the
> framework do this for me?
See
http://isabelle.in.tum.de/repos/isabelle/file/41d7946e2595/src/Pure/Syn
Hi Chris,
I'm currently (as of changeset e6433b34364b) investigating whether it
would be possible to allow adhoc overloading (implemented in
~~/src/Tools/adhoc_overloading.ML) inside local contexts.
Nice!
For completeness find my current adhoc_overloading.ML attached
Apart from the various
On Fri, 31 May 2013, Christian Sternagel wrote:
- So far so good. Everything compiles fine. When I actually use my newly
defined command, I get the error "Stale theory encountered". So obviously I'm
doing something wrong in the above "f" (if I replace "f" by "I" the error
disappears, but of co
On Fri, 31 May 2013, Christian Sternagel wrote:
- To set up a command ("adhoc_overloading" in my case) that should also work
inside local contexts I use "Outer_Syntax.local_theory".
This is fine. Basically you make some concrete syntax for this:
syntax_declaration {*
fn phi => fn conte
Dear all,
as I said earlier I am trying to make some changes (in Generic_Data)
persistent from inside a command. (My special case is ad-hoc
overloading, but I think that is irrelevant for the following.)
My current setup is (could you please point out any inadequate choices):
- To set up a c
On Wed, 29 May 2013, Florian Haftmann wrote:
Alternatively, use Context.>> directly in the body of the ML file
(which, I guess, is nowadays preferred over explicit setup in the
surrounding theory).
Hypersearch over the sources shows that Context.>> is still quite rare,
and there is no trend t
Dear Florian,
On 05/30/2013 06:03 AM, Florian Haftmann wrote:
Hi Christian,
- For Overload_Data instead of Theory_Data, I should use Generic_Data
(such that it is available in top-level theories and local theories).
Currently that means that I do the following in the setup (where
Adhoc_Overload
Hi Christian,
> - For Overload_Data instead of Theory_Data, I should use Generic_Data
> (such that it is available in top-level theories and local theories).
> Currently that means that I do the following in the setup (where
> Adhoc_Overloading.setup is now of type "Context.generic ->
> Context.gen
In the meanwhile I had a first look at the implementation of the
"notation" command. Some things I noted w.r.t. localizing ad-hoc
overloading (please correct me if I'm wrong):
- For Overload_Data instead of Theory_Data, I should use Generic_Data
(such that it is available in top-level theories
On Fri, 24 May 2013, Christian Sternagel wrote:
Since I'm not too sure about the internals of local contexts, would that
make sense in principle?
Yes. According to the "local everything approach" from 2006, locality is
the normal situation unless there are very strong reasons against it. In
Dear all,
I'm currently (as of changeset e6433b34364b) investigating whether it
would be possible to allow adhoc overloading (implemented in
~~/src/Tools/adhoc_overloading.ML) inside local contexts.
Since I'm not too sure about the internals of local contexts, would that
make sense in princi
38 matches
Mail list logo
