Re: [isabelle-dev] Countable instantiation addition
On 07/22/2011 10:44 AM, Lukas Bulwahn wrote: On 07/22/2011 09:36 AM, Alexander Krauss wrote: datatype foo = deriving countable, finite, Tobias also mentioned "set_of", "map_of", etc. But since these aren't class instantiations (we have no constructor classes such as "functor"), we end up with the good old generic datatype interpretation (roughly: datatype -> theory -> theory). So it seems like we simply want named datatype interpretations that are explicitly invoked via "deriving" (stretching the original Haskell notion quite a bit...) Yes, this was my first goal for the "deriving" project, creating a nice user interface and providing a "implementation guide" for datatype interpretations, and automatic type class instantiations, which would end up as "recipe" in the Isabelle Cookbook. A second goal was to automatically derive the interpretation by asking the user to give the definitions for some examples (as this can also be done in Haskell). Of course, the student would have to have a strong ML background and must learn a lot about data types. Therefore, I wrote the project idea down, even if such a prospective student might never exist. I forgot to mention that the "deriving" project I was talking about was one of the project ideas for this year's Google Summer of Code, which was not chosen to be completed. Lukas ___ 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] Countable instantiation addition
On 07/22/2011 09:36 AM, Alexander Krauss wrote: datatype foo = deriving countable, finite, Tobias also mentioned "set_of", "map_of", etc. But since these aren't class instantiations (we have no constructor classes such as "functor"), we end up with the good old generic datatype interpretation (roughly: datatype -> theory -> theory). So it seems like we simply want named datatype interpretations that are explicitly invoked via "deriving" (stretching the original Haskell notion quite a bit...) Yes, this was my first goal for the "deriving" project, creating a nice user interface and providing a "implementation guide" for datatype interpretations, and automatic type class instantiations, which would end up as "recipe" in the Isabelle Cookbook. A second goal was to automatically derive the interpretation by asking the user to give the definitions for some examples (as this can also be done in Haskell). Of course, the student would have to have a strong ML background and must learn a lot about data types. Therefore, I wrote the project idea down, even if such a prospective student might never exist. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Countable instantiation addition
datatype foo = deriving countable, finite, Tobias also mentioned "set_of", "map_of", etc. But since these aren't class instantiations (we have no constructor classes such as "functor"), we end up with the good old generic datatype interpretation (roughly: datatype -> theory -> theory). So it seems like we simply want named datatype interpretations that are explicitly invoked via "deriving" (stretching the original Haskell notion quite a bit...) 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: "_encode" *)
val dtype_add_encfun: string list -> local_theory -> local_theory
(* Add also the injectiity thm as "inj_>_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))
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
