5
$\begingroup$

The AFP entry Deriving provides a way to derive the following classes:

class description
comparator generate comparators for given types
compare register types in class compare
compare_order register types in class compare_order
countable register datatypes is class countable
equality generate an equality function
hash_code generate a hash function
hashable register types in class hashable
linorder register types in class linorder

I saw that there is an exposed function register_derive, and would like to add another class. How does this work?

$\endgroup$

1 Answer 1

3
$\begingroup$

To register a new type class with the Deriving_Manager, I found Derive_Aux.define_overloaded useful. Here is an example usage :

theory Derive_enum
  imports Datatype_Order_Generator.Derive_Aux Deriving.Derive
begin

ML ‹

The Derive_Manager.register_derive function expects us to implement a function string -> string -> (theory -> theory):

let
  fun derive_enum tyco params thy = undefined (* ... *)
in
  Derive_Manager.register_derive "enum" "derives enum for a datatype" derive_enum
    |> Theory.setup
end›

Now a call derive (p) enum mytype will end up calling derive_enum "mytype" "p"" and apply the theory morphism to the current theory.


Recall that we want to define the following terms for enum:

instantiation
  mytype :: enum
  enum_mytype == enum_class.enum :: mytype list
  enum_all_mytype == enum_class.enum_all :: (mytype ⇒ bool) ⇒ bool
  enum_ex_mytype == enum_class.enum_ex :: (mytype ⇒ bool) ⇒ bool

Implementing derive_enum is fairly straight-forward, as those definitions are quite simple too:

fun derive_enum tyco params thy =
  let
    (* extract the relevant information from the theory: *)
    val base_name = Long_Name.base_name tyco
    val sort = @{sort enum}
    val info = BNF_LFP_Compat.the_info thy [] tyco

    (* only derive for types with nullary constructors *)
    val ctors_opt = (case #descr info of
        [(_,(_,_,ctor_strs))] =>
          if List.all (snd #> null) ctor_strs then SOME (map fst ctor_strs) else NONE
      | _ => NONE)

    (* if all the constructors are nullary: *)
    fun go ctor_strs =
    let
      open Ctr_Sugar_Util

      val _ = writeln ("creating enum for datatype " ^ base_name)

      (* these are our constructors in HOL *)
      val T = Type (tyco, [])
      val ctors = map (fn x => Const (x, T)) ctor_strs

      (* enum = [ctor0, ctor1...] *)
      val enum_lhs = Const (@{const_name enum_class.enum}, HOLogic.listT T)
      val enum_rhs = HOLogic.mk_list T ctors
      val enum_def = Derive_Aux.mk_def (HOLogic.listT T) @{const_name enum_class.enum} enum_rhs

      val p = Free ("p", T --> @{typ bool})
      val pT = (T --> @{typ bool}) --> @{typ bool}
      val psT = (T --> @{typ bool}) --> HOLogic.listT T --> @{typ bool}

      (* enum_all = λp. list_all p enum *)
      val enum_all_rhs = lambda p
        (Const (@{const_name List.list_all}, psT) $ p $ enum_lhs)
      val enum_all_def = Derive_Aux.mk_def pT @{const_name enum_class.enum_all} enum_all_rhs

      (* enum_ex = λp. list_ex p enum *)
      val enum_ex_rhs = lambda p
        (Const (@{const_name List.list_ex}, psT) $ p $ enum_lhs)
      val enum_ex_def = Derive_Aux.mk_def pT @{const_name enum_class.enum_ex} enum_ex_rhs

      (* define the constants *)
      val (((enum_thm, enum_all_thm), enum_ex_thm), lthy) =
        Class.instantiation ([tyco],[],sort) thy
          |> Derive_Aux.define_overloaded ("enum_" ^ base_name ^ "_def", enum_def)
          ||>> Derive_Aux.define_overloaded ("enum_all_" ^ base_name ^ "_def", enum_all_def)
          ||>> Derive_Aux.define_overloaded ("enum_ex_" ^ base_name ^ "_def", enum_ex_def)

      (* build the tactics required: *)
      val enum_thms = [enum_thm RS @{thm meta_eq_to_obj_eq}, enum_all_thm, enum_ex_thm]

      (* UNIV = {ctor0...} *)
      fun UNIV_eq_tac ctxt =
        EVERY' [rtac ctxt @{thm UNIV_eq_I}, rtac ctxt (#exhaust info)] THEN_ALL_NEW
        EVERY' [K (unfold_tac ctxt (enum_thms @ @{thms list.set insert_iff})), blast_tac ctxt]

      (* _ {ctor0...} _ = _ UNIV _ *)
      fun pred_aux_tac ctxt = EVERY'
        [rtac ctxt @{thm arg_cong[where f="λx. _ x _"]},
         rtac ctxt @{thm sym},
         UNIV_eq_tac ctxt]

      fun enum_tac ctxt = EVERY
        [unfold_tac ctxt (@{thms list_all_iff list_ex_iff list.set} @ enum_thms),
         HEADGOAL (UNIV_eq_tac ctxt),
         HEADGOAL (simp_tac ctxt),
         HEADGOAL (pred_aux_tac ctxt),
         HEADGOAL (pred_aux_tac ctxt)]

      val thy' = Class.prove_instantiation_exit
        (fn ctxt => Class.intro_classes_tac ctxt [] THEN enum_tac ctxt) lthy
      val _ = writeln ("registered " ^ base_name ^ " in class enum")
    in
      thy'
    end

  in case ctors_opt of
      SOME ctors => go ctors
    | _ => warning ("cannot create enum for datatype " ^ base_name) |> K thy
  end

And to show how it all fits together:

datatype day = Sat | Sun | Mon | Tue | Wed | Thu | Fri
derive enum day
print_derives
(*
The following sorts can be derived
...
enum: derives enum for a datatype 
...
*)
value "Enum.enum :: day list" (* [Sat, Sun, Mon, Tue, Wed, Thu, Fri] *)
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.