Re: [isabelle-dev] ML equality types
I use those frequently as a curried version of 'op =', e.g. 'filter (equal "..." o fst) ...'. Lars Le 10 septembre 2015 12:31:14 GMT+02:00, Florian Haftmann a écrit : >In src/Pure/library.ML, the signature still contains the discouraged >and >nowadays rarely used entries > > val equal: ''a -> ''a -> bool > val not_equal: ''a -> ''a -> bool > >Shall we attempt to get rid of them finally? > > Florian > >-- > >PGP available: >http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de > > > > > >___ >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] ML equality types
On Thu, 10 Sep 2015, Florian Haftmann wrote: In src/Pure/library.ML, the signature still contains the discouraged and nowadays rarely used entries val equal: ''a -> ''a -> bool val not_equal: ''a -> ''a -> bool These operations are a bit old-fashioned, but why are they discouraged? As far as I know, David Matthews is doing a dictionary construction internally (for some years already). So it is just a minimal form of Haskell-style type-class discipline. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS
On Thu, 10 Sep 2015, Larry Paulson wrote: Purely FYI: the names of all of these constants were originally based on the corresponding names in Martin-Löf type theory. I do remember the good old times of MLTT, where it was clear what the basic combinators are. Interestingly, MLTT is up-to-date once again, in the guise of HoTT. I now wonder if these guys have a 15th standard of naming things, or are using the primordial one. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS
> I hope you will also restore the printing of "λ(x,y). x+y" as "λ(x,y).
> x+y" rather than "uncurry op +".
Okay, this is really unpleasant. Thanks for reporting this.
Florian
>
> Tobias
>
> On 10/09/2015 12:48, Florian Haftmann wrote:
>> Hi Andreas,
>>
>>> I noticed that the new printing interacts strangely with set
>>> comprehensions. In Isabelle/92858a52e45b, "{(x, y). P x y}" prints as
>>> "Collect (uncurry P)" which I find rather hard to read. Are you aware of
>>> this effect and could you please restore the former situation?
>>
>> this is on my to-do list, together with other binder-related issues like
>> "{p. case p of (x, y) => P x y}".
>>
>> Florian
>>
>>>
>>> Best,
>>> Andreas
>>>
>>> On 10/09/15 12:02, Florian Haftmann wrote:
* Combinator to represent case distinction on products is named
"uncurry", with "split" and "prod_case" retained as input
abbreviations.
Partially applied occurences of "uncurry" with eta-contracted body
terms are not printed with special syntax, to provide a compact
notation and getting rid of a special-case print translation.
Hence, the "uncurry"-expressions are printed the following way:
a) fully applied "uncurry f p": explicit case-expression;
b) partially applied with explicit double lambda abstraction in
the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;
c) partially applied with eta-contracted body term "uncurry f":
no special syntax, plain "uncurry" combinator.
This aims for maximum readability in a given subterm.
INCOMPATIBILITY.
This refers to e6b1236f9b3d.
This schema emerged after some experimentation and seems to be a
convenient compromise. The longer perspective is to overcome the
case_prod/split schism eventually and consolidate theorem names
accordingly.
The next step after this initial cleanup is to tackle the »let (a, b) =
… in …« issue.
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 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] NEWS
On 10.09.2015 12:19, Dmitriy Traytel wrote: > Hi Florian, > > while I very much welcome the simplified printing rules and your effort > of unifying case_prod/split, I am not sure if adding a third alternative > name is the way to go. The situation reminds me of the one depicted in [1]. > > Clearly, case_prod is the "right" name from the perspective of the > (co)datatype package. I also prefer a name following the usual case_ convention over a special case for type prod. >> b) partially applied with explicit double lambda abstraction in >> the body term "uncurry (%a b. t [a, b])": explicit paired abstraction; >> >> c) partially applied with eta-contracted body term "uncurry f": >> no special syntax, plain "uncurry" combinator. This does not seem to work right now; case b) is printed like c) if the body is eta-contractable (but not eta-contracted). >> This schema emerged after some experimentation and seems to be a >> convenient compromise. The longer perspective is to overcome the >> case_prod/split schism eventually and consolidate theorem names accordingly. What is the problem with converging to the default names created by the new datatype package? -- Laras ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS
Purely FYI: the names of all of these constants were originally based on the corresponding names in Martin-Löf type theory. Larry > On 10 Sep 2015, at 12:34, Tobias Nipkow wrote: > > > On 10/09/2015 12:19, Dmitriy Traytel wrote: >> Hi Florian, >> >> while I very much welcome the simplified printing rules and your effort of >> unifying case_prod/split, I am not sure if adding a third alternative name is >> the way to go. The situation reminds me of the one depicted in [1]. >> >> Clearly, case_prod is the "right" name from the perspective of the >> (co)datatype >> package. > > Yes, we should return to that name in the end. > > Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS
On 10/09/2015 12:19, Dmitriy Traytel wrote: Hi Florian, while I very much welcome the simplified printing rules and your effort of unifying case_prod/split, I am not sure if adding a third alternative name is the way to go. The situation reminds me of the one depicted in [1]. Clearly, case_prod is the "right" name from the perspective of the (co)datatype package. Yes, we should return to that name in the end. Tobias Dmitriy [1] https://xkcd.com/927/ On 10.09.2015 12:02, Florian Haftmann wrote: * Combinator to represent case distinction on products is named "uncurry", with "split" and "prod_case" retained as input abbreviations. Partially applied occurences of "uncurry" with eta-contracted body terms are not printed with special syntax, to provide a compact notation and getting rid of a special-case print translation. Hence, the "uncurry"-expressions are printed the following way: a) fully applied "uncurry f p": explicit case-expression; b) partially applied with explicit double lambda abstraction in the body term "uncurry (%a b. t [a, b])": explicit paired abstraction; c) partially applied with eta-contracted body term "uncurry f": no special syntax, plain "uncurry" combinator. This aims for maximum readability in a given subterm. INCOMPATIBILITY. This refers to e6b1236f9b3d. This schema emerged after some experimentation and seems to be a convenient compromise. The longer perspective is to overcome the case_prod/split schism eventually and consolidate theorem names accordingly. The next step after this initial cleanup is to tackle the »let (a, b) = … in …« issue. 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 smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS
I hope you will also restore the printing of "λ(x,y). x+y" as "λ(x,y). x+y"
rather than "uncurry op +".
Tobias
On 10/09/2015 12:48, Florian Haftmann wrote:
Hi Andreas,
I noticed that the new printing interacts strangely with set
comprehensions. In Isabelle/92858a52e45b, "{(x, y). P x y}" prints as
"Collect (uncurry P)" which I find rather hard to read. Are you aware of
this effect and could you please restore the former situation?
this is on my to-do list, together with other binder-related issues like
"{p. case p of (x, y) => P x y}".
Florian
Best,
Andreas
On 10/09/15 12:02, Florian Haftmann wrote:
* Combinator to represent case distinction on products is named
"uncurry", with "split" and "prod_case" retained as input abbreviations.
Partially applied occurences of "uncurry" with eta-contracted body
terms are not printed with special syntax, to provide a compact
notation and getting rid of a special-case print translation.
Hence, the "uncurry"-expressions are printed the following way:
a) fully applied "uncurry f p": explicit case-expression;
b) partially applied with explicit double lambda abstraction in
the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;
c) partially applied with eta-contracted body term "uncurry f":
no special syntax, plain "uncurry" combinator.
This aims for maximum readability in a given subterm.
INCOMPATIBILITY.
This refers to e6b1236f9b3d.
This schema emerged after some experimentation and seems to be a
convenient compromise. The longer perspective is to overcome the
case_prod/split schism eventually and consolidate theorem names
accordingly.
The next step after this initial cleanup is to tackle the »let (a, b) =
… in …« issue.
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
smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code generation to OCaml and Scala
Hi Florian, For SML, I kept everything as it is since a) the code is separate from OCaml anyway b) the "let … end" is always safe regardless of surrounding whitespace. Or did I miss something here? Here the SML part should be kept as it is (the generation was working correctly for me in SML), so your modifications on OCaml side are enough, this is good! Thanks also for your changes in Scala, Frédéric ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] ML equality types
I can't see any specific benefit of doing this. I still think that the next big project of this kind should be to sort out the real/of_nat mess. I’ve proposed an approach to doing it, but haven’t yet found a sufficient block of time in which executed. Larry > On 10 Sep 2015, at 11:31, Florian Haftmann > wrote: > > In src/Pure/library.ML, the signature still contains the discouraged and > nowadays rarely used entries > > val equal: ''a -> ''a -> bool > val not_equal: ''a -> ''a -> bool > > Shall we attempt to get rid of them finally? > > Florian > > -- > > PGP available: > http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de > > ___ > 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] NEWS
Hi Andreas,
> I noticed that the new printing interacts strangely with set
> comprehensions. In Isabelle/92858a52e45b, "{(x, y). P x y}" prints as
> "Collect (uncurry P)" which I find rather hard to read. Are you aware of
> this effect and could you please restore the former situation?
this is on my to-do list, together with other binder-related issues like
"{p. case p of (x, y) => P x y}".
Florian
>
> Best,
> Andreas
>
> On 10/09/15 12:02, Florian Haftmann wrote:
>> * Combinator to represent case distinction on products is named
>> "uncurry", with "split" and "prod_case" retained as input abbreviations.
>>
>> Partially applied occurences of "uncurry" with eta-contracted body
>> terms are not printed with special syntax, to provide a compact
>> notation and getting rid of a special-case print translation.
>>
>> Hence, the "uncurry"-expressions are printed the following way:
>>
>> a) fully applied "uncurry f p": explicit case-expression;
>>
>> b) partially applied with explicit double lambda abstraction in
>> the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;
>>
>> c) partially applied with eta-contracted body term "uncurry f":
>> no special syntax, plain "uncurry" combinator.
>> This aims for maximum readability in a given subterm.
>> INCOMPATIBILITY.
>>
>> This refers to e6b1236f9b3d.
>>
>> This schema emerged after some experimentation and seems to be a
>> convenient compromise. The longer perspective is to overcome the
>> case_prod/split schism eventually and consolidate theorem names
>> accordingly.
>>
>> The next step after this initial cleanup is to tackle the »let (a, b) =
>> … in …« issue.
>>
>> Florian
>>
>>
>>
>> ___
>> 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] NEWS
Hi Florian,
I noticed that the new printing interacts strangely with set comprehensions. In
Isabelle/92858a52e45b, "{(x, y). P x y}" prints as "Collect (uncurry P)" which I find
rather hard to read. Are you aware of this effect and could you please restore the former
situation?
Best,
Andreas
On 10/09/15 12:02, Florian Haftmann wrote:
* Combinator to represent case distinction on products is named
"uncurry", with "split" and "prod_case" retained as input abbreviations.
Partially applied occurences of "uncurry" with eta-contracted body
terms are not printed with special syntax, to provide a compact
notation and getting rid of a special-case print translation.
Hence, the "uncurry"-expressions are printed the following way:
a) fully applied "uncurry f p": explicit case-expression;
b) partially applied with explicit double lambda abstraction in
the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;
c) partially applied with eta-contracted body term "uncurry f":
no special syntax, plain "uncurry" combinator.
This aims for maximum readability in a given subterm.
INCOMPATIBILITY.
This refers to e6b1236f9b3d.
This schema emerged after some experimentation and seems to be a
convenient compromise. The longer perspective is to overcome the
case_prod/split schism eventually and consolidate theorem names accordingly.
The next step after this initial cleanup is to tackle the »let (a, b) =
… in …« issue.
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] [isabelle] Code setup for Fraction_Field
Hi Florian, I am continuing this thread on isabelle-dev as you have suggested. 3. For fraction fields over polynomials over rings (rather than fields), one can use subresultants, but I have not been able to find them formalised in Isabelle. Are they hidden somewhere? If not, are there any plans to formalise them? Are subresultants really necessary for this? definition ppdivmod_rel :: "'a::idom poly ⇒ 'a poly ⇒ 'a poly ⇒ 'a poly ⇒ 'a ⇒ bool" where "ppdivmod_rel x y q r m ⟷ ( smult m x = q * y + r ∧ (if y = 0 then q = 0 else r = 0 ∨ degree r < degree y) ∧ ( m= (if x=0 ∨ y=0 then 1 else (lead_coeff y) ^ (degree x + 1 - degree y" I am somehow lost how the »algebraic stack« is supposed to look like in the whole example. Something like Fraction over Poly over Int? Yes, that's the idea. Since Poly over Int forms a factorial ring but not an euclidean ring, the question is how to generalize normalization of quotients a / b accordingly. It won't work naturally with type classes: Poly over Rat --> normalization via gcd / eucl Poly over Poly over Rat --> somehow different Hence, some type class magic would be needed to detect whether to use the rather efficient euclidean algorithm or something different – or even refrain from normalization at all!? The type class magic needed for this sort of decision is pretty simple, it's described in my paper on AFP/Containers from ITP 2013. You just have to wrap a gcd function in "_ option" such that the normalisation algorithm for fraction fields can check whether normalisation via gcd is possible or whether something else is needed. If fraction field is implemented via code_abstype with the invariant that only normalised fractions occur, then the decision about the normalisation algorithm is logically relevant, as the normalisation function shows up in the code equations of the form fract_of (p + q) = normalize_fract ( (fract_of p) (fract_of q)) However, if we do not require normalised fractions and instead use a quotient-like code setup for fraction fields with code_datatype, the decision about normalisation need *not* be logically relevant. The code equations then look like the following: Fract a b + Fract c d = normalise_fract ( (a, b) (c, d))) The function normalise_fract can be a type class parameter, so one can define it differently for different types. As it returns the quotiented value, the decision whether to normalise and how to normalise is no longer logically relevant. So the choice could depend on extra-logical tricks (like inspecting the name of types). Best, Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] ML equality types
In src/Pure/library.ML, the signature still contains the discouraged and nowadays rarely used entries val equal: ''a -> ''a -> bool val not_equal: ''a -> ''a -> bool Shall we attempt to get rid of them finally? Florian -- 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] NEWS
Hi Dmitriy, > while I very much welcome the simplified printing rules and your effort > of unifying case_prod/split, I am not sure if adding a third alternative > name is the way to go. The situation reminds me of the one depicted in [1]. the other two are mere input abbreviations, which could disappear some time in the future. Where we have a real mess are the lemma names which follow different conventions, depending on their origin in the »split« or »case« world. This is now the first time when there is perspective to converge against one name. I do not insist that »uncurry« must be the last word on that, but I deem that expressions like »map (uncurry f) xs« »(uncurry o curry) = id« are much more intuitive to read (and write) than »map (split f) xs« »(split o curry) = id« »map (prod_case f) xs« »(prod_case o curry) = id« > Clearly, case_prod is the "right" name from the perspective of the > (co)datatype package. Which I hope is name-ignorant ;-). The point is that case expressions are always fully expanded and so an »uncurry« will never show up there. The situation is similar to inj_on / inj, SIGMA / _ x _, coprime / gcd, dvd / even where syntax decides how to present logically similar constructs in a specific fashion but keep them unified internally. Florian > > Dmitriy > > [1] https://xkcd.com/927/ > > On 10.09.2015 12:02, Florian Haftmann wrote: >> * Combinator to represent case distinction on products is named >> "uncurry", with "split" and "prod_case" retained as input abbreviations. >> >> Partially applied occurences of "uncurry" with eta-contracted body >> terms are not printed with special syntax, to provide a compact >> notation and getting rid of a special-case print translation. >> >> Hence, the "uncurry"-expressions are printed the following way: >> >> a) fully applied "uncurry f p": explicit case-expression; >> >> b) partially applied with explicit double lambda abstraction in >> the body term "uncurry (%a b. t [a, b])": explicit paired abstraction; >> >> c) partially applied with eta-contracted body term "uncurry f": >> no special syntax, plain "uncurry" combinator. >> This aims for maximum readability in a given subterm. >> INCOMPATIBILITY. >> >> This refers to e6b1236f9b3d. >> >> This schema emerged after some experimentation and seems to be a >> convenient compromise. The longer perspective is to overcome the >> case_prod/split schism eventually and consolidate theorem names accordingly. >> >> The next step after this initial cleanup is to tackle the »let (a, b) = >> … in …« issue. >> >> Florian >> >> >> >> ___ >> 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] NEWS
Hi Florian, while I very much welcome the simplified printing rules and your effort of unifying case_prod/split, I am not sure if adding a third alternative name is the way to go. The situation reminds me of the one depicted in [1]. Clearly, case_prod is the "right" name from the perspective of the (co)datatype package. Dmitriy [1] https://xkcd.com/927/ On 10.09.2015 12:02, Florian Haftmann wrote: * Combinator to represent case distinction on products is named "uncurry", with "split" and "prod_case" retained as input abbreviations. Partially applied occurences of "uncurry" with eta-contracted body terms are not printed with special syntax, to provide a compact notation and getting rid of a special-case print translation. Hence, the "uncurry"-expressions are printed the following way: a) fully applied "uncurry f p": explicit case-expression; b) partially applied with explicit double lambda abstraction in the body term "uncurry (%a b. t [a, b])": explicit paired abstraction; c) partially applied with eta-contracted body term "uncurry f": no special syntax, plain "uncurry" combinator. This aims for maximum readability in a given subterm. INCOMPATIBILITY. This refers to e6b1236f9b3d. This schema emerged after some experimentation and seems to be a convenient compromise. The longer perspective is to overcome the case_prod/split schism eventually and consolidate theorem names accordingly. The next step after this initial cleanup is to tackle the »let (a, b) = … in …« issue. 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] NEWS
* Combinator to represent case distinction on products is named "uncurry", with "split" and "prod_case" retained as input abbreviations. Partially applied occurences of "uncurry" with eta-contracted body terms are not printed with special syntax, to provide a compact notation and getting rid of a special-case print translation. Hence, the "uncurry"-expressions are printed the following way: a) fully applied "uncurry f p": explicit case-expression; b) partially applied with explicit double lambda abstraction in the body term "uncurry (%a b. t [a, b])": explicit paired abstraction; c) partially applied with eta-contracted body term "uncurry f": no special syntax, plain "uncurry" combinator. This aims for maximum readability in a given subterm. INCOMPATIBILITY. This refers to e6b1236f9b3d. This schema emerged after some experimentation and seems to be a convenient compromise. The longer perspective is to overcome the case_prod/split schism eventually and consolidate theorem names accordingly. The next step after this initial cleanup is to tackle the »let (a, b) = … in …« issue. Florian -- 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] Code generation to OCaml and Scala
Hi Fréderic, see now http://isabelle.in.tum.de/repos/isabelle/rev/774752af4a1f http://isabelle.in.tum.de/repos/isabelle/rev/8e736ce4c6f4 >> By comparing the generating code for SML and OCaml in >> src/Tools/Code/code_ml.ML, I would be tempted to replace >> "brackify_block" by "brackets" everytime in the corresponding >> "print_case" clause, and skip this optimization like in the SML part >> where "let"..."in"..."end" are inserted everytime, what about you? For SML, I kept everything as it is since a) the code is separate from OCaml anyway b) the "let … end" is always safe regardless of surrounding whitespace. Or did I miss something here? >> In the same spirit, the following code does not compile after exporting >> to Scala: >> datatype n = N nat >> definition "b = (let _ = N in False)" >> This is because N is a function, and no parentheses are generated around >> functions (at least in this example). Abstractions in Scala are now always in parenthesis, but only once for abstraction chains. Thanks a lot again, Florian -- 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
