[isabelle-dev] Code generation in Isabelle
Hello all, at the moment, we have two code generators in Isabelle: 1. An ancient code generator in Isabelle by Stefan Berghofer - limited to SML without supporting type classes. Commands to invoke it were code_module and code_library. 2. A generic code generator in Isabelle by Florian Haftmann - extenible to multiple target languages, supporting type classes, basic integration of reflection and abstraction mechanisms Commands to invoke it are export_code, value, code_reflect, and some others. The second subsumes the first, so we intend to remove the first code generator from the next Isabelle distribution if there are not any strong defenders of the ancient code generator. Any thoughts? Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Code generation in Isabelle
We moved recently to the new code-generator. Burkhart Am 21.07.2011 um 12:18 schrieb Lukas Bulwahn: Hello all, at the moment, we have two code generators in Isabelle: 1. An ancient code generator in Isabelle by Stefan Berghofer - limited to SML without supporting type classes. Commands to invoke it were code_module and code_library. 2. A generic code generator in Isabelle by Florian Haftmann - extenible to multiple target languages, supporting type classes, basic integration of reflection and abstraction mechanisms Commands to invoke it are export_code, value, code_reflect, and some others. The second subsumes the first, so we intend to remove the first code generator from the next Isabelle distribution if there are not any strong defenders of the ancient code generator. Any thoughts? Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Countable instantiation addition
This is definitely a useful tool for ImperativeHOL ... One could probably integrate it into the datatype package, such that datatypes automatically become countable (like Haskell infers some typeclasses automatically (on demand)) Peter Mathieu Giorgino schrieb: Hi all, I have written a little ML library allowing to automatically prove, in most cases, instantiations of types (typedefs, records and datatypes) as countable (see ~~/src/HOL/Library/Countable). The style of the library is still a little rough but I think it could be a nice addition to the Isabelle Library with some more work, mostly for Imperative_HOL (~~/src/HOL/Imperative_HOL) which can only store values of countable types in its heap. However, as Lukas Bulwhan said to me, improving it and integrating it in Isabelle while nobody use it would certainly be a lost of time. So here is my question: would anybody be interested in this addition ? I attach this library with a theory containing tests/examples. Anyway, if you have some advices for improving it, they would be welcome. Regards, Mathieu Giorgino ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Countable instantiation addition
Hi Matthieu, I have written a little ML library allowing to automatically prove, in most cases, instantiations of types (typedefs, records and datatypes) as countable (see ~~/src/HOL/Library/Countable). It seems that for datatypes we now have such functionality, implemented four weeks ago by Brian Huffman: http://isabelle.in.tum.de/repos/isabelle/rev/15df7bc8e93f It comes in the form of a method, so it has to be invoked explicitly, but like this it doesn't produce any penalty when it is not used. If you want to contribute an extension to records/typedefs, you are welcome, but you probably want to study Brian's implementation first. I assume that he is also the most appropriate person to review patches for this functionality. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Countable instantiation addition
On 21/07/2011, at 8:15 PM, Alexander Krauss wrote: It comes in the form of a method, so it has to be invoked explicitly, but like this it doesn't produce any penalty when it is not used. A separate command like this method looks like the right way to do such things. The idea has potential for generalisation. Could we turn this into something similar to Haskell's deriving? The command would take a datatype and a list of instantiation methods that each know how to instantiate a datatype for a specific type class, e.g. enum, countable, order, etc. An instantiation method would be basically a usual proof method plus some small part that knows how to set up the specific instantiation goal (probably the same code for pretty much all applications of this) plus some background theory that provides the basic setup. The methods would not have to work on every kind of data type (just failing if they can't prove their goal), and the list of available ones could be easily extended using the same Isar setup mechanisms that we use for proof methods, attributes, and other things. The command would not pollute normal datatype usage and would not need to be integrated with the datatype package, keeping the code separate. The interface would just be the user-visible final definition of the datatype as in Brian's case. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Countable instantiation addition
On 07/21/2011 09:47 PM, Gerwin Klein wrote: The idea has potential for generalisation. Could we turn this into something similar to Haskell's deriving? The command would take a datatype and a list of instantiation methods that each know how to instantiate a datatype for a specific type class, e.g. enum, countable, order, etc. An instantiation method would be basically a usual proof method plus some small part that knows how to set up the specific instantiation goal (probably the same code for pretty much all applications of this) plus some background theory that provides the basic setup. I like this approach. You ask for something explicitly and then you get it, but you don't have to remember a new obscure syntax for every bit of it. You would just write datatype foo = deriving countable, finite, Several existing things fit into this scheme: When I define a fresh datatype foo = Bar in Main, it automatically becomes an instance of the following type classes: - equal (executable equality, for code generation) - term_of(reifiable term structure, for code generation) - size (size function, for termination proofs) - full_exhaustive(for exhaustive quickcheck) (there is actually a large zoo of type classes for quickcheck...) This doesn't mean that we have to make every last thing explicit, but a mechanism would make sense. Note that in general, a proof method is not enough, since we have to define overloaded constants. Here, countable is an exception since the class has no parameters. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Countable instantiation addition
Hello everyone, Attached is an implementation of a countable_typedef method that I just wrote. (It works in a very similar manner to the countable_datatype method.) Since records are implemented as typedefs of product types, the same method works for record types as well. I'd be happy to add this to Library/Countable.thy if anyone wants me to. I haven't had time to study Mathieu's ML library yet, but if it has any features or capabilities that my system lacks, we should definitely try to incorporate those into whatever ends up in the next Isabelle release. I also need to remember to add an item to the NEWS file letting people know that these new proof methods exist. - Brian On Thu, Jul 21, 2011 at 11:15 AM, Alexander Krauss kra...@in.tum.de wrote: Hi Matthieu, I have written a little ML library allowing to automatically prove, in most cases, instantiations of types (typedefs, records and datatypes) as countable (see ~~/src/HOL/Library/Countable). It seems that for datatypes we now have such functionality, implemented four weeks ago by Brian Huffman: http://isabelle.in.tum.de/repos/isabelle/rev/15df7bc8e93f It comes in the form of a method, so it has to be invoked explicitly, but like this it doesn't produce any penalty when it is not used. If you want to contribute an extension to records/typedefs, you are welcome, but you probably want to study Brian's implementation first. I assume that he is also the most appropriate person to review patches for this functionality. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev Countable_Typedef.thy Description: application/isabelle-theory ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code generation in Isabelle
On 07/21/2011 04:25 PM, Steven Obua wrote: Actually, there is a third code generator hidden somewhere in Isabelle. If you are talking about what I know under the name Compute Oracle, then rest assured that it is hidden well enough that the chance of some user accidentially confusing it with the mainstream code generator is negligible. Interested parties can discover it using grep, of course. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code generation in Isabelle
Lukas already assured me of that. No worries here. - Steven On 22.07.2011, at 00:07, Alexander Krauss wrote: On 07/21/2011 04:25 PM, Steven Obua wrote: Actually, there is a third code generator hidden somewhere in Isabelle. If you are talking about what I know under the name Compute Oracle, then rest assured that it is hidden well enough that the chance of some user accidentially confusing it with the mainstream code generator is negligible. Interested parties can discover it using grep, of course. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Countable instantiation addition
Hi all,
I have written a little ML library allowing to automatically prove, in most
cases, instantiations of types (typedefs, records and datatypes) as countable
(see ~~/src/HOL/Library/Countable). The style of the library is still a little
rough but I think it could be a nice addition to the Isabelle Library with
some more work, mostly for Imperative_HOL (~~/src/HOL/Imperative_HOL) which
can only store values of countable types in its heap.
However, as Lukas Bulwhan said to me, improving it and integrating it in
Isabelle while nobody use it would certainly be a lost of time.
So here is my question: would anybody be interested in this addition ?
I attach this library with a theory containing tests/examples.
Anyway, if you have some advices for improving it, they would be welcome.
Regards,
Mathieu Giorginosignature COUNTABLE =
sig
(* typedef: Works for countable embedding type *)
val typedef_instantiate: string - theory - theory
(* records: Works for records with countable fields *)
val record_instantiate: string - theory - theory
(* Datatypes: works for any mutual recursive datatype which contains only:
- countable types
- or/and type parameters
- or/and mutual/recursive types
*)
(* Add a function encoding datatypes to natural numbers: type_encode *)
val dtype_add_encfun: string list - local_theory - local_theory
(* Add also the injectiity thm as inj_type1..._typei_encode *)
val dtype_add_encfun_and_injthm: string list - local_theory - local_theory
(* Instantiate the type as countable *)
val dtype_instantiate: string list - theory - theory
(* Add the encoding function and instantiate the type as countable *)
val dtype_add_encfun_and_instantiate: string list - theory - theory
end (* signature COUNTABLE_DATATYPE *)
structure Countable : COUNTABLE =
struct
type fun_spec = ((string * typ) * term) list
type descr_elem =
int * (string * Datatype_Data.dtyp list * (string * Datatype_Data.dtyp list) list);
type the_descr = Datatype_Data.descr * (string * sort) list * string list
* string * (string list * string list) * (typ list * typ list);
(* Replacing o with x to avoid a conflict with Fun.comp for
induction variables ... *)
fun varname_from_typname s =
String.substring (String.map Char.toLower (Long_Name.base_name s), 0, 1)
| (fn o = x | s = s);
fun varname_from_type (t as Type (s, ts)) =
if s = @{type_name list}
then (#1 (varname_from_type (hd ts)) ^ s, t)
else (varname_from_typname s, t)
| varname_from_type t = (x, t);
fun lookup_or_id f xs x = (case f xs x of NONE = x | SOME t' = t')
fun fresh_typ ctxt f tys =
tys
| (fn x = (x, x))
|| map #2
|| (fn Ss = Variable.invent_types Ss ctxt)
|| #1
|| map TFree
| map f
| ListPair.zip
| lookup_or_id (AList.lookup (op =))
fun apply_fresh_args f ts ctxt =
f
| fastype_of
| binder_types
| map varname_from_type
| Variable.variant_frees ctxt (f :: ts)
| map Free
| (fn x = (x, x))
| curry list_comb f;
fun encode_fun_name s = (Long_Name.base_name s) ^ _encode;
fun tree_app e _ _ [] = e
| tree_app _ f1 _ [t] = f1 t
| tree_app _ _ f2 [t1, t2] = f2 t1 t2
| tree_app e f1 f2 ts =
let val n = (length ts) div 2 in
f2 (tree_app e f1 f2 (take n ts)) (tree_app e f1 f2 (drop n ts))
end;
fun tyenv_unif thy ty1 ty2 =
#1 ((Sign.typ_unify thy (ty1, ty2)) (Vartab.empty, 0))
fun tconstrs typ thy t = the ((Datatype_Data.get_constrs thy) t)
| map (apsnd (fn t = Envir.norm_type (tyenv_unif thy (Type typ) (body_type t)) t))
| map Const;
fun constrs typ dconstrs thy =
ListPair.zip (tconstrs typ thy (#1 typ), map #2 dconstrs);
(* TODO: detect functions whose at least one parameter is non-finite *)
(* TODO: case where a function with this name is already defined *)
fun mk_fun_spec ctxt typ constrs (mut_typs:string list) =
let
fun nth_type_name n = nth mut_typs n;
fun nth_encode_fun_name n = encode_fun_name (nth_type_name n);
val current_encode_fun_name = encode_fun_name (#1 (dest_Type typ));
fun ensure_countable (Datatype_Aux.DtRec n) t =
Free (nth_encode_fun_name n, dummyT) $ t
| ensure_countable _ t = t;
fun first_prod n = Const(@{const_name to_nat}, dummyT) $ HOLogic.mk_number @{typ nat} n;
fun pair_const (t1, t2) = Const (@{const_name Pair}, dummyT) $ t1 $ t2
val prods_encode_tree =
map (fn (t, v) = (ensure_countable t) v)
# tree_app @{term to_nat ()} I (curry pair_const);
fun mk_fun_spec_aux [] _ ts = ts
| mk_fun_spec_aux ((constr, constr_dtyps)::constrs) n ts =
let val encode_fun = (current_encode_fun_name, typ -- @{typ nat}) in
(apply_fresh_args constr [] ctxt)
| curry op $ (Free encode_fun)
|| curry ListPair.zip constr_dtyps
|| prods_encode_tree
|| curry op $ (Const(@{const_name to_nat}, dummyT))
|| (fn t = Const(@{const_name to_nat}, dummyT) $ pair_const (first_prod n, t))
| (fn (x, y) = (encode_fun, HOLogic.mk_eq (x, y)))
Re: [isabelle-dev] [isabelle] Countable instantiation addition
It does not work for any datatype (for example as soon as a non-countable type is used in the datatype) but it could be integrated in the datatype package with some checks. However, I don't know if the time penalty (which isn't so big but there anyway) on a so much used feature worth the benefit... unless it would be present as an option (perhaps even with a recursive call on included non- instantiated types). And an option would be mostly equivalent to (in fact even less flexible than) a new command or an ML call subsequent to the datatype definition. Mathieu Le jeudi 21 juillet 2011 19:02:41 Peter Lammich a écrit : This is definitely a useful tool for ImperativeHOL ... One could probably integrate it into the datatype package, such that datatypes automatically become countable (like Haskell infers some typeclasses automatically (on demand)) Peter Mathieu Giorgino schrieb: Hi all, I have written a little ML library allowing to automatically prove, in most cases, instantiations of types (typedefs, records and datatypes) as countable (see ~~/src/HOL/Library/Countable). The style of the library is still a little rough but I think it could be a nice addition to the Isabelle Library with some more work, mostly for Imperative_HOL (~~/src/HOL/Imperative_HOL) which can only store values of countable types in its heap. However, as Lukas Bulwhan said to me, improving it and integrating it in Isabelle while nobody use it would certainly be a lost of time. So here is my question: would anybody be interested in this addition ? I attach this library with a theory containing tests/examples. Anyway, if you have some advices for improving it, they would be welcome. Regards, Mathieu Giorgino ___ 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
