Re: [isabelle-dev] AFP config files?

2016-06-23 Thread Gerwin Klein 
This specific entry currently exists only in devel. Release is clean.

Cheers,
Gerwin



> On 23.06.2016, at 17:54, Lars Hupel  wrote:
>
>> This is my entry. I submitted it a few days ago, and I included the
>> config file in my submission. I was not aware that those don't exist
>> anymore.
>
> They have been superseded by the "notify" configuration in the
> "metadata" file.
>
> If one AFP maintainer could please delete "thys/Catalan_Numbers/config"
> in stable AFP, that would be much appreciated.
>
> Cheers
> Lars
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Scala implicits

2016-06-23 Thread Florian Haftmann 
> Florian, what are you plans w.r.t. merging this patch into the
> distribution?

It's currently on the testboard.

Florian

> 
> Manuel
> 
> 
> On 23/06/16 11:22, Manuel Eberl wrote:
>> Looks good. After applying the patch, HOL-Codegenerator_Test goes
>> through with the code equation in Binomial.thy enabled.
>>
>>
>> Cheers,
>>
>> Manuel
>>
>>
>> On 23/06/16 09:48, Manuel Eberl wrote:
>>> The uncommented code equation at the end of ~~/src/HOL/Binomial.thy used
>>> to break Codegenerator_Test. I can have a look later to see whether this
>>> is still the case.
>>>
>>> If it is not, we should probably proceed to move some more of René
>>> Thiemann et al's efficient code equations from the AFP to the
>>> distribution.
>>>
>>> I'm glad to see this (hopefully) resolved.
>>>
>>>
>>> Cheers,
>>>
>>> Manuel
>>>
>>>
>>> On 23/06/16 09:45, Florian Haftmann wrote:
 Dear power users of code generation to Scala,

 during the last months there have been some reports on ambiguity
 problems with implicits in Scala.

 One kind of these has been known for long and can be addressed in more
 recent versions of Scala, which has been done in 7cffe366d333.

 One other kind is presumably resolved with the patch attached,
 applicable to b3e5bdb784f5. The key idea is to generate implicits in
 Scala (stemming from type class instances) into the respective
 companion
 objects of corresponding type classes.

 Since I have no example at hand where such ambiguities have been
 observed to happen, I would kindly ask whether someone might try
 whether
 that patch resolves the issue. No problems on the visible theory
 universe (Isabelle distribution plus AFP) have been encountered.

 The patch still keeps the traditional Scala approach that each implicit
 dictionary holds all operations of all super classes. I don't know
 whether this is still apt to expose problems, but this could be tackled
 in a second step.

 Thanks to Lars Hupel for suggesting these solutions.

 Cheers,
 Florian



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



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

-- 

PGP available:
http://isabelle.in.tum.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] Scala implicits

2016-06-23 Thread Manuel Eberl 

Florian, what are you plans w.r.t. merging this patch into the distribution?

Manuel


On 23/06/16 11:22, Manuel Eberl wrote:
Looks good. After applying the patch, HOL-Codegenerator_Test goes 
through with the code equation in Binomial.thy enabled.



Cheers,

Manuel


On 23/06/16 09:48, Manuel Eberl wrote:

The uncommented code equation at the end of ~~/src/HOL/Binomial.thy used
to break Codegenerator_Test. I can have a look later to see whether this
is still the case.

If it is not, we should probably proceed to move some more of René
Thiemann et al's efficient code equations from the AFP to the 
distribution.


I'm glad to see this (hopefully) resolved.


Cheers,

Manuel


On 23/06/16 09:45, Florian Haftmann wrote:

Dear power users of code generation to Scala,

during the last months there have been some reports on ambiguity
problems with implicits in Scala.

One kind of these has been known for long and can be addressed in more
recent versions of Scala, which has been done in 7cffe366d333.

One other kind is presumably resolved with the patch attached,
applicable to b3e5bdb784f5. The key idea is to generate implicits in
Scala (stemming from type class instances) into the respective 
companion

objects of corresponding type classes.

Since I have no example at hand where such ambiguities have been
observed to happen, I would kindly ask whether someone might try 
whether

that patch resolves the issue. No problems on the visible theory
universe (Isabelle distribution plus AFP) have been encountered.

The patch still keeps the traditional Scala approach that each implicit
dictionary holds all operations of all super classes. I don't know
whether this is still apt to expose problems, but this could be tackled
in a second step.

Thanks to Lars Hupel for suggesting these solutions.

Cheers,
Florian



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






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

Re: [isabelle-dev] Scala implicits

2016-06-23 Thread Manuel Eberl 
Looks good. After applying the patch, HOL-Codegenerator_Test goes 
through with the code equation in Binomial.thy enabled.



Cheers,

Manuel


On 23/06/16 09:48, Manuel Eberl wrote:

The uncommented code equation at the end of ~~/src/HOL/Binomial.thy used
to break Codegenerator_Test. I can have a look later to see whether this
is still the case.

If it is not, we should probably proceed to move some more of René
Thiemann et al's efficient code equations from the AFP to the distribution.

I'm glad to see this (hopefully) resolved.


Cheers,

Manuel


On 23/06/16 09:45, Florian Haftmann wrote:

Dear power users of code generation to Scala,

during the last months there have been some reports on ambiguity
problems with implicits in Scala.

One kind of these has been known for long and can be addressed in more
recent versions of Scala, which has been done in 7cffe366d333.

One other kind is presumably resolved with the patch attached,
applicable to b3e5bdb784f5. The key idea is to generate implicits in
Scala (stemming from type class instances) into the respective companion
objects of corresponding type classes.

Since I have no example at hand where such ambiguities have been
observed to happen, I would kindly ask whether someone might try whether
that patch resolves the issue. No problems on the visible theory
universe (Isabelle distribution plus AFP) have been encountered.

The patch still keeps the traditional Scala approach that each implicit
dictionary holds all operations of all super classes. I don't know
whether this is still apt to expose problems, but this could be tackled
in a second step.

Thanks to Lars Hupel for suggesting these solutions.

Cheers,
Florian



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



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

Re: [isabelle-dev] AFP config files?

2016-06-23 Thread Manuel Eberl 
This is my entry. I submitted it a few days ago, and I included the 
config file in my submission. I was not aware that those don't exist 
anymore.



On 23/06/16 09:49, Florian Haftmann wrote:

Dear AFP maintainers,

in 79fb78da1ef0 there exists exactly one file named "config", namely

./thys/Catalan_Numbers/config

All the others I gone.

I suspect this is an accidental left-over.

Cheers,
Florian



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


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

Re: [isabelle-dev] Scala implicits

2016-06-23 Thread Manuel Eberl 
The uncommented code equation at the end of ~~/src/HOL/Binomial.thy used 
to break Codegenerator_Test. I can have a look later to see whether this 
is still the case.


If it is not, we should probably proceed to move some more of René 
Thiemann et al's efficient code equations from the AFP to the distribution.


I'm glad to see this (hopefully) resolved.


Cheers,

Manuel


On 23/06/16 09:45, Florian Haftmann wrote:

Dear power users of code generation to Scala,

during the last months there have been some reports on ambiguity
problems with implicits in Scala.

One kind of these has been known for long and can be addressed in more
recent versions of Scala, which has been done in 7cffe366d333.

One other kind is presumably resolved with the patch attached,
applicable to b3e5bdb784f5. The key idea is to generate implicits in
Scala (stemming from type class instances) into the respective companion
objects of corresponding type classes.

Since I have no example at hand where such ambiguities have been
observed to happen, I would kindly ask whether someone might try whether
that patch resolves the issue. No problems on the visible theory
universe (Isabelle distribution plus AFP) have been encountered.

The patch still keeps the traditional Scala approach that each implicit
dictionary holds all operations of all super classes. I don't know
whether this is still apt to expose problems, but this could be tackled
in a second step.

Thanks to Lars Hupel for suggesting these solutions.

Cheers,
Florian



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


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

[isabelle-dev] Scala implicits

2016-06-23 Thread Florian Haftmann 
Dear power users of code generation to Scala,

during the last months there have been some reports on ambiguity
problems with implicits in Scala.

One kind of these has been known for long and can be addressed in more
recent versions of Scala, which has been done in 7cffe366d333.

One other kind is presumably resolved with the patch attached,
applicable to b3e5bdb784f5. The key idea is to generate implicits in
Scala (stemming from type class instances) into the respective companion
objects of corresponding type classes.

Since I have no example at hand where such ambiguities have been
observed to happen, I would kindly ask whether someone might try whether
that patch resolves the issue. No problems on the visible theory
universe (Isabelle distribution plus AFP) have been encountered.

The patch still keeps the traditional Scala approach that each implicit
dictionary holds all operations of all super classes. I don't know
whether this is still apt to expose problems, but this could be tackled
in a second step.

Thanks to Lars Hupel for suggesting these solutions.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
# HG changeset patch
# Parent  b3e5bdb784f554028901a1a95711cbc97801b7ee
compiling implicit instances into companion objects for classes avoids 
ambiguities

diff -r b3e5bdb784f5 NEWS
--- a/NEWS  Wed Jun 22 16:47:55 2016 +0200
+++ b/NEWS  Wed Jun 22 19:00:12 2016 +0200
@@ -129,6 +129,10 @@
 different phases of code generation. See src/HOL/ex/Code_Timing.thy for
 examples.
 
+* Code generator: implicits in Scala (stemming from type class instances)
+are generated into companion object of corresponding type class, to resolve
+some situations where ambiguities may occur.
+
 
 *** HOL ***
 
diff -r b3e5bdb784f5 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML  Wed Jun 22 16:47:55 2016 +0200
+++ b/src/Tools/Code/code_scala.ML  Wed Jun 22 19:00:12 2016 +0200
@@ -13,8 +13,6 @@
 structure Code_Scala : CODE_SCALA =
 struct
 
-val target = "Scala";
-
 open Basic_Code_Symbol;
 open Basic_Code_Thingol;
 open Code_Printer;
@@ -29,6 +27,15 @@
 
 (** Scala serializer **)
 
+val target = "Scala";
+
+datatype scala_stmt = Fun of typscheme * ((iterm list * iterm) * (thm option * 
bool)) list
+  | Datatype of vname list * ((string * vname list) * itype list) list
+  | Class of (vname * ((class * class) list * (string * itype) list))
+  * (string * { vs: (vname * sort) list,
+  inst_params: ((string * (const * int)) * (thm * bool)) list,
+  superinst_params: ((string * (const * int)) * (thm * bool)) list }) list;
+
 fun print_scala_stmt tyco_syntax const_syntax reserved
 args_num is_constr (deresolve, deresolve_full) =
   let
@@ -172,14 +179,14 @@
 |> single
 |> enclose "(" ")"
   end;
-fun print_context tyvars vs sym = applify "[" "]"
+fun print_context tyvars vs s = applify "[" "]"
   (fn (v, sort) => (Pretty.block o map str)
 (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class 
class]) sort))
-  NOBR ((str o deresolve) sym) vs;
+  NOBR (str s) vs;
 fun print_defhead export tyvars vars const vs params tys ty =
   concat [str "def", constraint (applify "(" ")" (fn (param, ty) =>
 constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
-  NOBR (print_context tyvars vs (Constant const)) (params ~~ tys)) 
(print_typ tyvars NOBR ty),
+  NOBR (print_context tyvars vs (deresolve_const const)) (params ~~ 
tys)) (print_typ tyvars NOBR ty),
 str "="];
 fun print_def export const (vs, ty) [] =
   let
@@ -233,9 +240,38 @@
   (map print_clause eqs)
   end;
 val print_method = str o Library.enclose "`" "`" o deresolve_full o 
Constant;
-fun print_stmt (Constant const, (export, Code_Thingol.Fun (((vs, ty), 
raw_eqs), _))) =
+fun print_inst class (tyco, { vs, inst_params, superinst_params }) =
+  let
+val tyvars = intro_tyvars vs reserved;
+val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
+fun print_classparam_instance ((classparam, (const as { dom, ... }, 
dom_length)), (thm, _)) =
+  let
+val aux_dom = Name.invent_names (snd reserved) "a" dom;
+val auxs = map fst aux_dom;
+val vars = intro_vars auxs reserved;
+val (aux_dom1, aux_dom2) = chop dom_length aux_dom;
+fun abstract_using [] = []
+  | abstract_using aux_dom = [enum "," "(" ")"
+  (map (fn (aux, ty) => constraint ((str o lookup_var vars) 
aux)
+  (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
+val aux_abstr1 = abstract_using aux_dom1;
+val aux_abstr2 = abstract_using aux_dom2;
+  in
+concat ([str "val", print_method classparam, str "="]
+  @ aux_abstr1 @