Re: [isabelle-dev] scala-2.12.2

[Lars Hupel]

> The guys there are talking about Dotty. Do you think it will be also
> taken into account by the regular scalac maintainers eventually?

Those are Martin Odersky's students, so it's natural that they want to
avoid this in Dotty.

I'm confident that the scalac team at Lightbend will also have a look,
but we should give them a couple of days.

> Alternatively, if Florian has an idea for a workaround it is also fine.

I'm still not quite sure about the impact of this.

If I manually increase the stack size (-Xss), as is done in
ISABELLE_SCALAC_OPTIONS, the problem goes away (even for the full
"test.scala" file). This would explain why the problem didn't manifest
itself in the testboard. However, I'm not sure if we should expect users
of code generation to invoke compilers with specific options.

Regardless, this is clearly a regression in Scala.

Alternatively, Florian might offer some insight why he set up the code
equations for that particular constant in that way (see "String.thy",
where a ML snippet generates 256 code equations). Note that large
pattern matches on the JVM should be avoided, lest we violate the 64k
method length limit in class files ("integer_of_char" currently requires
58044 bytes).
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] scala-2.12.2

[Lars Hupel]

> a "StackOverflowError" (in the patmat phase), before I even got a chance
> at running this

I have investigated this now. It is a regression from Scala 2.11.x to
Scala 2.12.x.

The offending function is "integer_of_char", which performs a 256-way
pattern matching. Maybe this should be implemented differently.

In any case, I have filed this as a bug:

  

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

Re: [isabelle-dev] scala-2.12.2

[Makarius]

On 22/06/17 14:10, Lars Hupel wrote:
>> a "StackOverflowError" (in the patmat phase), before I even got a chance
>> at running this
> 
> I have investigated this now. It is a regression from Scala 2.11.x to
> Scala 2.12.x.
> 
> The offending function is "integer_of_char", which performs a 256-way
> pattern matching. Maybe this should be implemented differently.
> 
> In any case, I have filed this as a bug:
> 
>   

The guys there are talking about Dotty. Do you think it will be also
taken into account by the regular scalac maintainers eventually?

Alternatively, if Florian has an idea for a workaround it is also fine.


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

Re: [isabelle-dev] scala-2.12.2

[Lars Hupel]

> I took the opportunity to have a look at it and found out it can be done
> differently, see attached patch.

The patch is now running on testboard:
.

> The clue about "integer_of_char" is that it had to work regardless
> whether HOL chars are represented authentic or by target language
> characters (importing "~~/src/HOL/Library/Code_Char").
> 
> Nowadays this can be achieved without spelling out the chars explicitly.
>  The last stone to turn around before had been the de-constructivation
> of the char type (b3f2b8c906a6).

Thanks for investigating this.

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

Re: [isabelle-dev] scala-2.12.2

[Florian Haftmann]

> Alternatively, Florian might offer some insight why he set up the code
> equations for that particular constant in that way (see "String.thy",
> where a ML snippet generates 256 code equations). Note that large
> pattern matches on the JVM should be avoided, lest we violate the 64k
> method length limit in class files ("integer_of_char" currently requires
> 58044 bytes).

I took the opportunity to have a look at it and found out it can be done
differently, see attached patch.

The clue about "integer_of_char" is that it had to work regardless
whether HOL chars are represented authentic or by target language
characters (importing "~~/src/HOL/Library/Code_Char").

Nowadays this can be achieved without spelling out the chars explicitly.
 The last stone to turn around before had been the de-constructivation
of the char type (b3f2b8c906a6).

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
# HG changeset patch
# Parent  45d3d43abee7147fd43e63a6b4ba6340a5d4b74f
more direct construction of integer_of_num;
code equations for integer_of_char may rely on pattern matching on Char

diff -r 45d3d43abee7 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy  Thu Jun 22 16:59:14 2017 +0200
+++ b/src/HOL/Code_Numeral.thy  Thu Jun 22 17:31:28 2017 +0200
@@ -149,24 +149,19 @@
   "int_of_integer (Num.sub k l) = Num.sub k l"
   by transfer rule
 
-lift_definition integer_of_num :: "num \ integer"
-  is "numeral :: num \ int"
-  .
+definition integer_of_num :: "num \ integer"
+  where [simp]: "integer_of_num = numeral"
 
 lemma integer_of_num [code]:
-  "integer_of_num num.One = 1"
-  "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)"
-  "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
-  by (transfer, simp only: numeral.simps Let_def)+
-
-lemma numeral_unfold_integer_of_num:
-  "numeral = integer_of_num"
-  by (simp add: integer_of_num_def map_fun_def fun_eq_iff)
+  "integer_of_num Num.One = 1"
+  "integer_of_num (Num.Bit0 n) = (let k = integer_of_num n in k + k)"
+  "integer_of_num (Num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
+  by (simp_all only: integer_of_num_def numeral.simps Let_def)
 
 lemma integer_of_num_triv:
   "integer_of_num Num.One = 1"
   "integer_of_num (Num.Bit0 Num.One) = 2"
-  by (transfer, simp)+
+  by simp_all
 
 instantiation integer :: "{linordered_idom, equal}"
 begin
@@ -301,7 +296,7 @@
 end
 
 declare divmod_algorithm_code [where ?'a = integer,
-  unfolded numeral_unfold_integer_of_num, unfolded integer_of_num_triv, 
+  folded integer_of_num_def, unfolded integer_of_num_triv, 
   code]
 
 lemma integer_of_nat_0: "integer_of_nat 0 = 0"
diff -r 45d3d43abee7 src/HOL/String.thy
--- a/src/HOL/String.thyThu Jun 22 16:59:14 2017 +0200
+++ b/src/HOL/String.thyThu Jun 22 17:31:28 2017 +0200
@@ -160,35 +160,10 @@
   by (simp only: integer_of_char_def integer_of_nat_def comp_apply 
nat_of_char_Char map_fun_def
 id_apply zmod_int modulo_integer.abs_eq [symmetric]) simp
 
-lemma less_256_integer_of_char_Char:
-  assumes "numeral k < (256 :: integer)"
-  shows "integer_of_char (Char k) = numeral k"
-proof -
-  have "numeral k mod 256 = (numeral k :: integer)"
-by (rule semiring_numeral_div_class.mod_less) (insert assms, simp_all)
-  then show ?thesis using integer_of_char_Char [of k]
-by (simp only:)
-qed
-
-setup \
-let
-  val chars = map_range (Thm.cterm_of @{context} o HOLogic.mk_numeral o curry 
(op +) 1) 255;
-  val simpset =
-put_simpset HOL_ss @{context}
-  addsimps @{thms numeral_less_iff less_num_simps};
-  fun mk_code_eqn ct =
-Thm.instantiate' [] [SOME ct] @{thm less_256_integer_of_char_Char}
-|> full_simplify simpset;
-  val code_eqns = map mk_code_eqn chars;
-in
-  Global_Theory.note_thmss ""
-[((@{binding integer_of_char_simps}, []), [(code_eqns, [])])]
-  #> snd
-end
-\
-
-declare integer_of_char_simps [code]
-
+lemma integer_of_char_Char_code [code]:
+  "integer_of_char (Char k) = integer_of_num k mod 256"
+  by simp
+  
 lemma nat_of_char_code [code]:
   "nat_of_char = nat_of_integer \ integer_of_char"
   by (simp add: integer_of_char_def fun_eq_iff)


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