Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

[Clemens Ballarin]

I have now committed this.  See isabelle/e89cfc004f18; the AFP didn't require 
changes.

The final version does not activate abbreviations as aggressively as my first 
proposal.  This was necessary so abbreviations are not propagated over rewrite 
morphisms, which would have been very confusing.

I did check that this change does not accidentally change any of the Isabelle 
documentation.  I also ran Makarius' termination stress test on Isabelle and 
the AFP.  The latter needed timeout_scale=8.

Clemens


On 08 November, 2015 18:59 CET, Makarius  wrote: 
 
> On Sat, 7 Nov 2015, Makarius wrote:
> 
> > Since the actual change to src/Pure/Isar/generic_target.ML is so small, 
> > we should just go ahead with it -- after a full test with AFP.
> 
> The option "timeout_scale" from Isabelle/a2f0f659a3c2 should help to do 
> this.
> 
> Note that AFP is presently a bit broken:
> 
>[RIPEMD-160-SPARK] is still on FAIL.
>[ShortestPath] is still on FAIL.
>[Graph_Theory] is still on FAIL.
> 
>Full entry status at http://afp.sourceforge.net/status.shtml
> 
>AFP version: development -- hg id f433a3e7bbf1
>Isabelle version: devel -- hg id 15952a05133c
> 
> 
>   Makarius
 
 
 
 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

[Florian Haftmann]

Hi Clemens,

> I'm not familiar with the termination argument for abbreviations, but
certainly we can say that abbreviations define a reduction system (in
fact a rewrite system), and I would assume that there are no cycles and
infinite paths.  Now my patch will clone part of this system,
introducing additional nodes and transitions, but I don't see how it
would introduce cycles if there were no cycles without it.  It could
introduce infinite chains, but only for infinite chains of
interpretations.  The latter are not allowed by the roundup algorithm.
Am I missing something?

Well, I am not so sure about the cycles:

As a starting point, take A --> B --> C.

Let the interpretation morphism map these as follows:

A |-> D
B |-> E
C |-> D

Then under the morphism we have D --> E --> D.

But maybe this is forbidden by the properties of a morphism itself.

I did not work to contrieve a meaningful counterexample yet.

Cheers,
Florian

> 
> Clemens
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

[Makarius]

On Sat, 7 Nov 2015, Makarius wrote:

Since the actual change to src/Pure/Isar/generic_target.ML is so small, 
we should just go ahead with it -- after a full test with AFP.


The option "timeout_scale" from Isabelle/a2f0f659a3c2 should help to do 
this.


Note that AFP is presently a bit broken:

  [RIPEMD-160-SPARK] is still on FAIL.
  [ShortestPath] is still on FAIL.
  [Graph_Theory] is still on FAIL.

  Full entry status at http://afp.sourceforge.net/status.shtml

  AFP version: development -- hg id f433a3e7bbf1
  Isabelle version: devel -- hg id 15952a05133c


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

[Makarius]

On Fri, 6 Nov 2015, Makarius wrote:


On Wed, 4 Nov 2015, Clemens Ballarin wrote:


 On 30 October, 2015 20:02 CET, Makarius  wrote:

>  Standard batch build prints relatively few terms, so this is not yet
>  significant as a test.
> 
>  The following change prints every intermediate Isar toplevel state. 
>  With

>  that I get timeouts or interrupts due to out-of-memory situation in
>  various sessions, e.g. HOL-Nominal-Examples or Jinja.

 Unfortunately this already fails without my patch, so it cannot be used as
 a test.


Odd. I am in the process of looking more closely what really happens here, 
both with and without your change.


These tests always take very long, but there is probably not much behind 
it.  Printing requires a lot of resources (space and time) and the 
timeouts are just that: the session takes very long and is interrupted.  I 
have increased some timeouts manually to get more sessions through.


Included is a slightly refined change for testing: it avoids producing a 
lot of big strings.



Since the actual change to src/Pure/Isar/generic_target.ML is so small, we 
should just go ahead with it -- after a full test with AFP.



Makarius# HG changeset patch
# User wenzelm
# Date 1446936258 -3600
#  Sat Nov 07 23:44:18 2015 +0100
# Node ID 8fab417a5955afbe2d211cb45d6138dd2fb880f5
# Parent  15952a05133c8b05eeadd7697333a6e70f58aeeb
test

diff -r 15952a05133c -r 8fab417a5955 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML Sat Nov 07 20:04:09 2015 +0100
+++ b/src/Pure/Isar/toplevel.ML Sat Nov 07 23:44:18 2015 +0100
@@ -588,6 +588,8 @@
 val opt_err' = opt_err |> Option.map
   (fn Runtime.EXCURSION_FAIL exn_info => exn_info
 | exn => (Runtime.exn_context (try context_of st) exn, at_command tr));
+val _ = writeln (command_msg "" tr);
+val _ = writeln (string_of_int (length (pretty_state st')));
 val _ = get_hooks () |> List.app (fn f => (try (fn () => f tr st st') (); 
()));
   in (st', opt_err') end;
 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

[Makarius]

On Wed, 4 Nov 2015, Clemens Ballarin wrote:


On 30 October, 2015 20:02 CET, Makarius  wrote:


Standard batch build prints relatively few terms, so this is not yet
significant as a test.

The following change prints every intermediate Isar toplevel state.  With
that I get timeouts or interrupts due to out-of-memory situation in
various sessions, e.g. HOL-Nominal-Examples or Jinja.


Unfortunately this already fails without my patch, so it cannot be used 
as a test.


Odd. I am in the process of looking more closely what really happens here, 
both with and without your change.



Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

[Makarius]

On Thu, 29 Oct 2015, Florian Haftmann wrote:

I have not spend any thoughts whether there could be terminaton issues. 
Is there any argument beyond the absence of counterexamples that that 
can never happen?


Standard batch build prints relatively few terms, so this is not yet 
significant as a test.


The following change prints every intermediate Isar toplevel state.  With 
that I get timeouts or interrupts due to out-of-memory situation in 
various sessions, e.g. HOL-Nominal-Examples or Jinja.


I did not look what really happens.


This is Isabelle/d05f3d86a758 and AFP/20f80d4c7850.


Makarius# HG changeset patch
# User wenzelm
# Date 1446231391 -3600
#  Fri Oct 30 19:56:31 2015 +0100
# Node ID 75fa4c345fc77dbd8b5621205ed620f484896b6d
# Parent  d05f3d86a758931d5cd379b9ec86b766eebb20da
test

diff -r d05f3d86a758 -r 75fa4c345fc7 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML Fri Oct 30 17:14:30 2015 +0100
+++ b/src/Pure/Isar/toplevel.ML Fri Oct 30 19:56:31 2015 +0100
@@ -585,6 +585,7 @@
 val (st', opt_err) =
   Context.setmp_thread_data (try (Context.Proof o presentation_context_of) 
st)
 (fn () => app int tr st) ();
+val _ = writeln (string_of_state st');
 val opt_err' = opt_err |> Option.map
   (fn Runtime.EXCURSION_FAIL exn_info => exn_info
 | exn => (Runtime.exn_context (try context_of st) exn, at_command tr));
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

[Florian Haftmann]

»const_decl« is shared by different primitives and operations on various
targets.  Hence the patch looks fine.

The »revert_abbrev« goes back to changeset 2b86fac03ec5 in
named_target.ML, although the guarding criterion has changed over time.
 2b86fac03ec5 is already in the highly experimental layer of local
theory experiments from 2007.  I doubt that digging further will reveal
any insight.  Hence, we just assume that the reverted abbreviations will
not exhibit any problems here.  I have spend no though on the issue

I have not spend any thoughts whether there could be terminaton issues.
 Is there any argument beyond the absence of counterexamples that that
can never happen?

Cheers,
Florian

Am 29.10.2015 um 11:48 schrieb Florian Haftmann:
> Hi Clemens,
> 
> thanks for undertaking this.
> 
> I will have a look at this and give feedback.
> 
> Cheers,
>   Florian
> 
> Am 27.10.2015 um 18:59 schrieb Clemens Ballarin:
>> Related to the below discussion on isabelle-users, I have now refined the 
>> patch I had circulated then.  Here is the NEWS entry:
>>
>> * More gentle suppression of syntax along locale morphisms while
>> printing terms.  Previously 'abbreviation' and 'notation' declarations
>>
>> would be suppressed for morphisms (except term identity).  Now merely
>> 'notation' is suppressed.  This can be of great help when working with
>>
>> complex locale hierarchies, because proof states are displayed much
>> more succinctly.  It also means that only notation needs to be
>> redeclared if desired, as illustrated by this example:
>>
>>   locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\" 65)
>>   begin
>> definition derived (infixl "\" 65) where ...
>>   end
>>
>>   locale morphism =
>> left!: struct composition + right!: struct composition'
>> for composition (infix "\" 65) and composition' (infix "\''" 
>> 65)
>>   begin
>> notation right.derived ("\''")
>>   end
>>
>> The full patch is attached.  Interestingly, it is fully compatible also with 
>> the AFP.  Since I'm not particularly familiar with generic_target.ML I'm 
>> posting it here for feedback.  My intention is to push this in the near 
>> future.
>>
>> Clemens
>>
>>
>> On 28 July, 2015 12:12 CEST, Andreas Lochbihler 
>>  wrote: 
>>  
>>> Hi Julian,
>>>
>>> First of all, I would be very happy if you could solve this problem of 
>>> missing 
>>> contractions. Clemens has never showed me an example where folding of 
>>> abbreviations would 
>>> lead to non-termination. And I do not know precisely how abbreviations and 
>>> locales are 
>>> implemented, so it is hard for me to decide whether something would lead to 
>>> a problem. 
>>> Nevertheless, here is another example:
>>>
>>> locale l = fixes f :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a"
>>> definition (in l) foo where "foo ≡ f (%x. x)"
>>> interpretation l "id" where "l.foo id == id (%x. x)" sorry
>>>
>>> If the interpretation installs abbreviations which respect the rewrite 
>>> morphism, then the 
>>> abbreviation reads as "id (%x. x) == id (%x. x)" which clearly loops. If it 
>>> does not, then 
>>> "id (%x. x)" is always printed as "foo".  This might not be optimal, as the 
>>> right-hand 
>>> sides can be arbitrary general terms that should remain the way they are.
>>>
>>> Andreas
>>>
>>> On 28/07/15 11:33, Julian Brunner wrote:
 Hi Andreas,

 Good call on the overlapping abbreviations, I did not consider this case. 
 However, the
 conflict already arises with the current implementation. Consider the 
 following:

 locale foo =
fixes f :: "'a => 'a => bool"
fixes g :: "'a => 'a => 'a => bool"
 begin

definition test where "test = f"
sublocale f!: foo f "% x y z. g y z x" by this

 end

 This generates the following abbreviations (they end up in the Consts 
 record in this order):

 f.test == foo.test f
 f.f.test == foo.test f
 test == foo.test f

 Since 'test' only depends on the parameter f, which is interpreted under 
 the identity
 morphism (eta contraction seems to matter here, so this does not happen 
 with your original
 example), all of these abbreviations are set up to be contracted before 
 printing. In fact,
 'test' is printed as 'f.test' (presumably due to the order of the 
 abbreviations in the
 Consts record).

 Given that these contraction conflicts are already a problem as it is, I 
 do not think that
 it would make things significantly worse to allow contraction of 
 abbreviations introduced
 via other morphisms (barring other problems like the one you discussed 
 with Clemens Ballarin).

 On Tue, Jul 28, 2015 at 8:53 AM Andreas Lochbihler 
 > wrote:

 Hi Julian,

 I also regularly suffer from these pretty-printing nightmares, but 

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

[Florian Haftmann]

Hi Clemens,

thanks for undertaking this.

I will have a look at this and give feedback.

Cheers,
Florian

Am 27.10.2015 um 18:59 schrieb Clemens Ballarin:
> Related to the below discussion on isabelle-users, I have now refined the 
> patch I had circulated then.  Here is the NEWS entry:
> 
> * More gentle suppression of syntax along locale morphisms while
> printing terms.  Previously 'abbreviation' and 'notation' declarations
> 
> would be suppressed for morphisms (except term identity).  Now merely
> 'notation' is suppressed.  This can be of great help when working with
> 
> complex locale hierarchies, because proof states are displayed much
> more succinctly.  It also means that only notation needs to be
> redeclared if desired, as illustrated by this example:
> 
>   locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\" 65)
>   begin
> definition derived (infixl "\" 65) where ...
>   end
> 
>   locale morphism =
> left!: struct composition + right!: struct composition'
> for composition (infix "\" 65) and composition' (infix "\''" 
> 65)
>   begin
> notation right.derived ("\''")
>   end
> 
> The full patch is attached.  Interestingly, it is fully compatible also with 
> the AFP.  Since I'm not particularly familiar with generic_target.ML I'm 
> posting it here for feedback.  My intention is to push this in the near 
> future.
> 
> Clemens
> 
> 
> On 28 July, 2015 12:12 CEST, Andreas Lochbihler 
>  wrote: 
>  
>> Hi Julian,
>>
>> First of all, I would be very happy if you could solve this problem of 
>> missing 
>> contractions. Clemens has never showed me an example where folding of 
>> abbreviations would 
>> lead to non-termination. And I do not know precisely how abbreviations and 
>> locales are 
>> implemented, so it is hard for me to decide whether something would lead to 
>> a problem. 
>> Nevertheless, here is another example:
>>
>> locale l = fixes f :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a"
>> definition (in l) foo where "foo ≡ f (%x. x)"
>> interpretation l "id" where "l.foo id == id (%x. x)" sorry
>>
>> If the interpretation installs abbreviations which respect the rewrite 
>> morphism, then the 
>> abbreviation reads as "id (%x. x) == id (%x. x)" which clearly loops. If it 
>> does not, then 
>> "id (%x. x)" is always printed as "foo".  This might not be optimal, as the 
>> right-hand 
>> sides can be arbitrary general terms that should remain the way they are.
>>
>> Andreas
>>
>> On 28/07/15 11:33, Julian Brunner wrote:
>>> Hi Andreas,
>>>
>>> Good call on the overlapping abbreviations, I did not consider this case. 
>>> However, the
>>> conflict already arises with the current implementation. Consider the 
>>> following:
>>>
>>> locale foo =
>>>fixes f :: "'a => 'a => bool"
>>>fixes g :: "'a => 'a => 'a => bool"
>>> begin
>>>
>>>definition test where "test = f"
>>>sublocale f!: foo f "% x y z. g y z x" by this
>>>
>>> end
>>>
>>> This generates the following abbreviations (they end up in the Consts 
>>> record in this order):
>>>
>>> f.test == foo.test f
>>> f.f.test == foo.test f
>>> test == foo.test f
>>>
>>> Since 'test' only depends on the parameter f, which is interpreted under 
>>> the identity
>>> morphism (eta contraction seems to matter here, so this does not happen 
>>> with your original
>>> example), all of these abbreviations are set up to be contracted before 
>>> printing. In fact,
>>> 'test' is printed as 'f.test' (presumably due to the order of the 
>>> abbreviations in the
>>> Consts record).
>>>
>>> Given that these contraction conflicts are already a problem as it is, I do 
>>> not think that
>>> it would make things significantly worse to allow contraction of 
>>> abbreviations introduced
>>> via other morphisms (barring other problems like the one you discussed with 
>>> Clemens Ballarin).
>>>
>>> On Tue, Jul 28, 2015 at 8:53 AM Andreas Lochbihler 
>>> >> > wrote:
>>>
>>> Hi Julian,
>>>
>>> I also regularly suffer from these pretty-printing nightmares, but I 
>>> vaguely remember a
>>> discussion with Clemens Ballarin on the subject. IIRC the problem is 
>>> that it is not clear
>>> whether collapsing the abbreviations terminates in all cases. Clemens 
>>> has never showed me
>>> an example where it actually happens, though.
>>>
>>> Yet, I can still think of difficult situations as as the following:
>>>
>>> locale foo =
>>> fixes f :: "'a => 'a => bool"
>>> and g :: "'a => 'a => 'a => bool"
>>>
>>> definition (in foo) test where "test = f"
>>>
>>> sublocale foo ⊆ f: foo "%x y. f y x" "%x y z. g y z x" .
>>>
>>> This sublocale declaration makes the locale subgraph cyclic, However, 
>>> the round-up
>>> algorithm realises that if you go six times through the circle, the 
>>> composed parameter
>>> instantiations are alpha-beta-eta-equivalent to f and g again, so it 

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

[Clemens Ballarin]

Related to the below discussion on isabelle-users, I have now refined the patch 
I had circulated then.  Here is the NEWS entry:

* More gentle suppression of syntax along locale morphisms while
printing terms.  Previously 'abbreviation' and 'notation' declarations

would be suppressed for morphisms (except term identity).  Now merely
'notation' is suppressed.  This can be of great help when working with

complex locale hierarchies, because proof states are displayed much
more succinctly.  It also means that only notation needs to be
redeclared if desired, as illustrated by this example:

  locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\" 65)
  begin
definition derived (infixl "\" 65) where ...
  end

  locale morphism =
left!: struct composition + right!: struct composition'
for composition (infix "\" 65) and composition' (infix "\''" 65)
  begin
notation right.derived ("\''")
  end

The full patch is attached.  Interestingly, it is fully compatible also with 
the AFP.  Since I'm not particularly familiar with generic_target.ML I'm 
posting it here for feedback.  My intention is to push this in the near future.

Clemens


On 28 July, 2015 12:12 CEST, Andreas Lochbihler 
 wrote:

> Hi Julian,
>
> First of all, I would be very happy if you could solve this problem of missing
> contractions. Clemens has never showed me an example where folding of 
> abbreviations would
> lead to non-termination. And I do not know precisely how abbreviations and 
> locales are
> implemented, so it is hard for me to decide whether something would lead to a 
> problem.
> Nevertheless, here is another example:
>
> locale l = fixes f :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a"
> definition (in l) foo where "foo ≡ f (%x. x)"
> interpretation l "id" where "l.foo id == id (%x. x)" sorry
>
> If the interpretation installs abbreviations which respect the rewrite 
> morphism, then the
> abbreviation reads as "id (%x. x) == id (%x. x)" which clearly loops. If it 
> does not, then
> "id (%x. x)" is always printed as "foo".  This might not be optimal, as the 
> right-hand
> sides can be arbitrary general terms that should remain the way they are.
>
> Andreas
>
> On 28/07/15 11:33, Julian Brunner wrote:
> > Hi Andreas,
> >
> > Good call on the overlapping abbreviations, I did not consider this case. 
> > However, the
> > conflict already arises with the current implementation. Consider the 
> > following:
> >
> > locale foo =
> >fixes f :: "'a => 'a => bool"
> >fixes g :: "'a => 'a => 'a => bool"
> > begin
> >
> >definition test where "test = f"
> >sublocale f!: foo f "% x y z. g y z x" by this
> >
> > end
> >
> > This generates the following abbreviations (they end up in the Consts 
> > record in this order):
> >
> > f.test == foo.test f
> > f.f.test == foo.test f
> > test == foo.test f
> >
> > Since 'test' only depends on the parameter f, which is interpreted under 
> > the identity
> > morphism (eta contraction seems to matter here, so this does not happen 
> > with your original
> > example), all of these abbreviations are set up to be contracted before 
> > printing. In fact,
> > 'test' is printed as 'f.test' (presumably due to the order of the 
> > abbreviations in the
> > Consts record).
> >
> > Given that these contraction conflicts are already a problem as it is, I do 
> > not think that
> > it would make things significantly worse to allow contraction of 
> > abbreviations introduced
> > via other morphisms (barring other problems like the one you discussed with 
> > Clemens Ballarin).
> >
> > On Tue, Jul 28, 2015 at 8:53 AM Andreas Lochbihler 
> >  > > wrote:
> >
> > Hi Julian,
> >
> > I also regularly suffer from these pretty-printing nightmares, but I 
> > vaguely remember a
> > discussion with Clemens Ballarin on the subject. IIRC the problem is 
> > that it is not clear
> > whether collapsing the abbreviations terminates in all cases. Clemens 
> > has never showed me
> > an example where it actually happens, though.
> >
> > Yet, I can still think of difficult situations as as the following:
> >
> > locale foo =
> > fixes f :: "'a => 'a => bool"
> > and g :: "'a => 'a => 'a => bool"
> >
> > definition (in foo) test where "test = f"
> >
> > sublocale foo ⊆ f: foo "%x y. f y x" "%x y z. g y z x" .
> >
> > This sublocale declaration makes the locale subgraph cyclic, However, 
> > the round-up
> > algorithm realises that if you go six times through the circle, the 
> > composed parameter
> > instantiations are alpha-beta-eta-equivalent to f and g again, so it 
> > stops. That means
> > that the sublocale command adds five copies of foo to itself. Now 
> > consider the situation
> > for the abbreviations. We have
> >
> > local.test == foo.test f
> >
> > from the original definition. From the sublocale command, we