Re: [isabelle-dev] sets and code generation
On Tue, 27 Mar 2012, Jesus Aransay wrote: trying to import simultaneously the theory file HOL/Matrix/Matrix.thy and the afp entry http://afp.sourceforge.net/entries/Matrix.shtml into a file theory Matrix_ex imports ~~/src/HOL/Matrix/Matrix Matrix/Matrix begin Is there an easy way out of this situation in Isabelle2011-1? Renaming one of the theory files is an acceptable solution in this case? Renaming one of the theory files (on your private copy) is the only solution in contemporary Isabelle. It is acceptable, because it is just one file here. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sets and code generation
Hi Jesus, trying to import simultaneously the theory file HOL/Matrix/Matrix.thy and the afp entry http://afp.sourceforge.net/entries/Matrix.shtml into a file, it seems that the second theory file unloads the first one (as Makarius suggested in his mail): theory Matrix_ex imports ~~/src/HOL/Matrix/Matrix Matrix/Matrix begin Is there an easy way out of this situation in Isabelle2011-1? Renaming one of the theory files is an acceptable solution in this case? It is. Cf. the previous email of Makarius on the same thread. Cheers, 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] sets and code generation
Dear all, trying to import simultaneously the theory file HOL/Matrix/Matrix.thy and the afp entry http://afp.sourceforge.net/entries/Matrix.shtml into a file, it seems that the second theory file unloads the first one (as Makarius suggested in his mail): theory Matrix_ex imports ~~/src/HOL/Matrix/Matrix Matrix/Matrix begin Is there an easy way out of this situation in Isabelle2011-1? Renaming one of the theory files is an acceptable solution in this case? Thanks for your help, Jesus On Fri, Mar 23, 2012 at 1:25 PM, Makarius makar...@sketis.net wrote: On Fri, 23 Mar 2012, Christian Sternagel wrote: Maybe the AFP entry for executable matrix operations is useful for you. http://afp.sourceforge.net/entries/Matrix.shtml (HOL/Matrix/Matrix.thy). Note that in current Isabelle/08c22e8ffe70 HOL/Matrix is actually called HOL/Matrix_LP, in order to avoid a name clash of the AFP/HOL-Matrix session (the latter was introduced later, but AFP names are not so easy to change as I understand it). Technically, the motivation is to get globally unique session names for official Isabelle + AFP sessions. Then when we eventually get a decent build system (based on Isabelle/Scala), the user can refer to sessions robustly without tinkering IsaMakefiles or funny search paths. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- Jesús María Aransay Azofra Universidad de La Rioja Dpto. de Matemáticas y Computación tlf.: (+34) 941299438 fax: (+34) 941299460 mail: jesus-maria.aran...@unirioja.es ; web: http://www.unirioja.es/cu/jearansa Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sets and code generation
On 03/23/2012 11:45 AM, Jesus Aransay wrote: I know there is an alternative way to get that, by means of sparse matrices (SparseMatrix.thy), but it demands translating every operation over the matrix type to its equivalent version for sparse matrices, which may be sometimes hard work. Code generation often requires translating or transfering every operation from one type to another. At the moment, users have to do this manually (which can be hard work as you said), but we are working on a mechanism that should soon automate this. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sets and code generation
On Fri, 23 Mar 2012, Christian Sternagel wrote: Maybe the AFP entry for executable matrix operations is useful for you. http://afp.sourceforge.net/entries/Matrix.shtml (HOL/Matrix/Matrix.thy). Note that in current Isabelle/08c22e8ffe70 HOL/Matrix is actually called HOL/Matrix_LP, in order to avoid a name clash of the AFP/HOL-Matrix session (the latter was introduced later, but AFP names are not so easy to change as I understand it). Technically, the motivation is to get globally unique session names for official Isabelle + AFP sessions. Then when we eventually get a decent build system (based on Isabelle/Scala), the user can refer to sessions robustly without tinkering IsaMakefiles or funny search paths. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] sets and code generation
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
as a code equation leads to an error stating that terms (x and y are
first-order terms) do not support the enum class. Since the possible
terms (using strings as function symbols and variables) cannot be
enumerated in a (finite) list, I can also not introduce an enum instance.
In the NEWS I found that the default setup for sets during code
generation is as a container type (instead of predicates). What are the
reasons for this decision? Is there an easy fix for such code equations?
One other thing. Syntax (e.g., ord) suggests 'a = 'a = bool for
relations, but the library support (starting with more standard symbols)
is leaning towards 'a rel. As a user it would be nice to have some
indication what is preferable/best practice (e.g., in terms of future
support; I already switched several times in our IsaFoR formalization,
currently rewrite relations are of type ('f, 'v) term rel, is this the
way to go?).
cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sets and code generation
On 03/21/2012 08:36 AM, Christian Sternagel wrote:
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
as a code equation leads to an error stating that terms (x and y are
first-order terms) do not support the enum class. Since the possible
terms (using strings as function symbols and variables) cannot be
enumerated in a (finite) list, I can also not introduce an enum instance.
Introducing 'a set as a type constructor now allows us to refine the set
operations to operations on lists (by Florian's way of data refinement
for code generation).
However, this now disallows the execution of op | on the type ...
set. To execute this, you have to move this specification to predicates
('a = bool):
Define op | = (%(x, y). supt_impl x y)
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sets and code generation
On 03/21/2012 05:05 PM, Lukas Bulwahn wrote:
On 03/21/2012 08:36 AM, Christian Sternagel wrote:
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
as a code equation leads to an error stating that terms (x and y are
first-order terms) do not support the enum class. Since the possible
terms (using strings as function symbols and variables) cannot be
enumerated in a (finite) list, I can also not introduce an enum instance.
Introducing 'a set as a type constructor now allows us to refine the set
operations to operations on lists (by Florian's way of data refinement
for code generation).
However, this now disallows the execution of op | on the type ...
set. To execute this, you have to move this specification to predicates
('a = bool):
Define op | = (%(x, y). supt_impl x y)
Lukas
Sorry I don't quite get it. op | is already defined to be of type
('f, 'v) term rel (and used heavily as a set). So the above equation
would not be well-typed. Is your suggestion to change op | into a
predicate?
cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sets and code generation
On 03/21/2012 09:08 AM, Christian Sternagel wrote:
On 03/21/2012 05:05 PM, Lukas Bulwahn wrote:
On 03/21/2012 08:36 AM, Christian Sternagel wrote:
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
as a code equation leads to an error stating that terms (x and y are
first-order terms) do not support the enum class. Since the possible
terms (using strings as function symbols and variables) cannot be
enumerated in a (finite) list, I can also not introduce an enum
instance.
Introducing 'a set as a type constructor now allows us to refine the set
operations to operations on lists (by Florian's way of data refinement
for code generation).
However, this now disallows the execution of op | on the type ...
set. To execute this, you have to move this specification to predicates
('a = bool):
Define op | = (%(x, y). supt_impl x y)
Lukas
Sorry I don't quite get it. op | is already defined to be of type
('f, 'v) term rel (and used heavily as a set). So the above equation
would not be well-typed. Is your suggestion to change op | into a
predicate?
cheers
chris
Yes.
If you have an infinite set during the execution in the generated code,
which you hinted at before, you cannot use the type 'a set for code
generation, but you must use 'a = bool.
I cannot estimate how much work that is in your case.
If it is unfeasible in your formalisation to change this, there might
also be other means to obtain an executable specification by creating an
alternative data refinement for sets, but I only had this in the back of
my mind, and we have not done this (yet).
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sets and code generation
Hi Christian,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
there is a couple of issues you are hitting at here.
A. The (re-)introduction of the set type constructor
See
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg01736.html
for one possible entry into the motivation and discussion concerning that.
B. The default code generation for setup
You can always turn back to sets-as-predicates by
code_datatype Collect
and then proving appropriate theorems for the set operation etc. – this
would fir best into a library theory which could then be part of the
distribution. But I guess your issue is mainly with…
C. Relations
Both kinds of relations 'a = 'a = bool and ('a * 'a) set are present
in their own right, but with disjoint developments in the HOL theoris.
Note that you can convert between both using pred/set conversions, the
same infrastructure as inductive_set is using.
So, if you want predicate relations, it seems to be best to convert your
stuff to them, filling existing gaps in the HOL theories by additional
definitions and suitable pred/set conversion declarations.
See theory Relation for examples for making use of pred/set
conversions by means of attributes to_set and to_pred; and
declarations of pred/set conversions by means of attribute pred_set_conv.
Unfortunately, there is no reference for them in the Isabelle Reference
Manual. Maybe one day this is subsumed by an emerging generic »lifting«
infrastructure.
Hope this helps,
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
