[isabelle] Proof of concept: BNF-based records



Dear list,

I'd like to demonstrate that it is quite simple to base records on BNFs.

The short story is: it takes about 160 lines of ML code and 50 lines of syntax declarations to achieve almost (one big caveat, see below) feature parity to the standard record package (sources attached).

Looking for your input on whether this is useful, and whether it belongs into HOL-Library, the AFP, or the bin.


What is supported? Pretty much the old syntax:

  bnf_record ('a, 'b) foo =
    field_1 :: 'a
    field_2 :: 'b

  term "⦇ field_1 = 3, field_2 = () ⦈"
  term "foo ⦇ field_1 := y ⦈"

Also, record construction syntax is supported out of the box for arbitrary single-free-constructor types:

  datatype x = X (a: int) (b: int)

  term "⦇ a = 1, b = 2 ⦈"

Update syntax for existing types can be installed like this:

  local_setup ‹BNF_Record.mk_update_defs @{type_name x}›

  term "(X 1 2) ⦇ b := 3 ⦈ = X 1 3"

What isn't supported?

- No extensions (i.e. "_ext", "_scheme" etc.).
- Full flags and options of the datatype package (e.g. declaring type variables as dead, disabling plugins).
- Any kind of compatibility between standard and BNF records.

How is it implemented?

1. Define a single-constructor datatype.
2. Generate update functions for each field.
3. Lots of syntax sugar.

Why?

The short reason: the "record" package isn't localized.

The longer reason: there are more problems with records, e.g. there is no support for nested recursion (they do not constitute BNFs), and even "copy_bnf" can't fix the absence of a suitable "size" function (which makes termination proofs impossible).

Why not?

The internal construction of standard records is much faster. Half of the 50 lines to declare syntax is required to un-declare record syntax. Unfortunately raw "syntax" rules can't be bundle-d. Importing the theory breaks all existing record syntax.

What is the motivation for this?

Lem supports records. CakeML uses them for some core types, and specifies nested recursion through them. Whenever CakeML updates, I can either change the generated sources to include a bunch of magic incantations to make termination proofs work, or I can change Lem to emit "bnf_record" instead of "record".* As a third option (somewhere between band-aid and proper solution), Jasmin has already suggested a few months to port the size plugin to records. I attempted that but unfortunately it took me too much time and ultimately I didn't manage to. This here was much quicker to pull off (approx. 3 h) and fixes an immediate problem I had. (Jasmin did however prevent me from writing a plugin that generates update functions for all datatypes.)

Cheers
Lars


* Changing Lem to emit "datatype" doesn't solve the absence of updating functions that are also required for Lem/CakeML.
signature BNF_RECORD = sig
  val mk_update_defs:
    string -> local_theory -> local_theory

  val bnf_record:
    binding -> typ list -> (binding * typ) list -> local_theory -> local_theory

  val bnf_record_cmd:
    binding -> string list -> (binding * string) list -> local_theory -> local_theory

  val setup: theory -> theory
end

structure BNF_Record : BNF_RECORD = struct

type data = string Symtab.table

structure Data = Theory_Data
(
  type T = data
  val empty = Symtab.empty
  val merge = Symtab.merge op =
  val extend = I
)

fun mk_update_defs typ_name lthy =
  let
    val short_name = Long_Name.base_name typ_name

    val {ctrs, casex, selss, ...} = the (Ctr_Sugar.ctr_sugar_of lthy typ_name)
    val ctr = case ctrs of [ctr] => ctr | _ => error "BNF_Record.mk_update_defs: expected only single constructor"
    val sels = case selss of [sels] => sels | _ => error "BNF_Record.mk_update_defs: expected selectors"
    val ctr_dummy = Const (fst (dest_Const ctr), dummyT)
    val casex_dummy = Const (fst (dest_Const casex), dummyT)

    val len = length sels

    fun mk_name sel =
      Binding.name ("update_" ^ Long_Name.base_name (fst (dest_Const sel)))

    fun mk_t idx =
      let
        val body =
          fold_rev (fn pos => fn t => t $ (if len - pos = idx + 1 then Bound len $ Bound pos else Bound pos)) (0 upto len - 1) ctr_dummy
          |> fold_rev (fn idx => fn t => Abs ("x" ^ Value.print_int idx, dummyT, t)) (1 upto len)
      in
        Abs ("f", dummyT, casex_dummy $ body)
      end

    fun define name t =
      Local_Theory.define ((name, NoSyn), ((Binding.empty, @{attributes [bnf_record_update, code]}), t)) #> snd

    val lthy' =
      Local_Theory.map_background_naming (Name_Space.qualified_path false (Binding.name short_name)) lthy

    fun insert sel =
      Symtab.insert op = (fst (dest_Const sel), Local_Theory.full_name lthy' (mk_name sel))
  in
    lthy'
    |> @{fold 2} define (map mk_name sels) (Syntax.check_terms lthy (map mk_t (0 upto len - 1)))
    |> Local_Theory.background_theory (Data.map (fold insert sels))
    |> Local_Theory.restore_background_naming lthy
  end

fun bnf_record binding tyargs args lthy =
  let
    val tyargs' = map (fn tyarg => (SOME Binding.empty, (tyarg, @{sort type}))) tyargs

    val constructor =
      (((Binding.empty, Binding.map_name (fn c => "make_" ^ c) binding), args), NoSyn)

    val datatyp =
      ((tyargs', binding), NoSyn)

    val dtspec =
      (Ctr_Sugar.default_ctr_options,
       [(((datatyp, [constructor]), (Binding.empty, Binding.empty, Binding.empty)), [])])

    val lthy' =
      BNF_FP_Def_Sugar.co_datatypes BNF_Util.Least_FP BNF_LFP.construct_lfp dtspec lthy
      |> mk_update_defs (Local_Theory.full_name lthy binding)
  in
    lthy'
  end

fun bnf_record_cmd binding tyargs args lthy =
  bnf_record binding (map (TFree o rpair @{sort type}) tyargs)
    (map (apsnd (Syntax.parse_typ lthy)) args) lthy

(* syntax *)

val read_const =
  dest_Const oo Proof_Context.read_const {proper = true, strict = true}

fun field_tr ((Const (\<^syntax_const>\<open>_bnf_field\<close>, _) $ Const (name, _) $ arg)) = (name, arg)
  | field_tr t = raise TERM ("field_tr", [t]);

fun fields_tr (Const (\<^syntax_const>\<open>_bnf_fields\<close>, _) $ t $ u) = field_tr t :: fields_tr u
  | fields_tr t = [field_tr t];

fun record_fields_tr ctxt t =
  let
    val assns = map (apfst (read_const ctxt)) (fields_tr t)

    val typ_name =
      snd (fst (hd assns))
      |> domain_type
      |> dest_Type
      |> fst

    val assns' = map (apfst fst) assns

    val {ctrs, selss, ...} = the (Ctr_Sugar.ctr_sugar_of ctxt typ_name)
    val ctr = case ctrs of [ctr] => ctr | _ => error "BNF_Record.record_fields_tr: expected only single constructor"
    val sels = case selss of [sels] => sels | _ => error "BNF_Record.record_fields_tr: expected selectors"
    val ctr_dummy = Const (fst (dest_Const ctr), dummyT)

    fun mk_arg name =
      case AList.lookup op = assns' name of
        NONE => error ("BNF_Record.record_fields_tr: missing field " ^ name)
      | SOME t => t
  in
    if length assns = length sels then
      list_comb (ctr_dummy, map (mk_arg o fst o dest_Const) sels)
    else
      error ("BNF_Record.record_fields_tr: expected " ^ Value.print_int (length sels) ^ " field(s)")
  end

fun field_update_tr ctxt (Const (\<^syntax_const>\<open>_bnf_field_update\<close>, _) $ Const (name, _) $ arg) =
      let
        val thy = Proof_Context.theory_of ctxt
        val (name, _) = read_const ctxt name
      in
        case Symtab.lookup (Data.get thy) name of
          NONE => raise Fail ("not a valid record field: " ^ name)
        | SOME s => Const (s, dummyT) $ Abs (Name.uu_, dummyT, arg)
      end
  | field_update_tr _ t = raise TERM ("field_update_tr", [@{print} t]);

fun field_updates_tr ctxt (Const (\<^syntax_const>\<open>_bnf_field_updates\<close>, _) $ t $ u) =
      field_update_tr ctxt t :: field_updates_tr ctxt u
  | field_updates_tr ctxt t = [field_update_tr ctxt t];

fun record_tr ctxt [t] = record_fields_tr ctxt t
  | record_tr _ ts = raise TERM ("record_tr", ts);

fun record_update_tr ctxt [t, u] = fold (curry op $) (field_updates_tr ctxt u) t
  | record_update_tr _ ts = raise TERM ("record_update_tr", ts);

val parser =
  (Parse.type_args -- Parse.binding) --
    (\<^keyword>\<open>=\<close> |-- Scan.repeat1 (Parse.binding -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ)))

val _ =
  Outer_Syntax.local_theory
    @{command_keyword bnf_record}
    "Defines a record based on the BNF/datatype machinery"
    (parser >> (fn ((tyargs, binding), args) => bnf_record_cmd binding tyargs args))

val setup =
   (Sign.parse_translation
     [(\<^syntax_const>\<open>_bnf_record_update\<close>, record_update_tr),
      (\<^syntax_const>\<open>_bnf_record\<close>, record_tr)]);

end
section \<open>Records based on BNF/datatype machinery\<close>

theory BNF_Record
imports Main
keywords "bnf_record" :: thy_decl
begin

no_syntax
  "_constify"           :: "id => ident"                        ("_")
  "_constify"           :: "longid => ident"                    ("_")

  "_field_type"         :: "ident => type => field_type"        ("(2_ ::/ _)")
  ""                    :: "field_type => field_types"          ("_")
  "_field_types"        :: "field_type => field_types => field_types"    ("_,/ _")
  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
  "_record_type_scheme" :: "field_types => type => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")

  "_field"              :: "ident => 'a => field"               ("(2_ =/ _)")
  ""                    :: "field => fields"                    ("_")
  "_fields"             :: "field => fields => fields"          ("_,/ _")
  "_record"             :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")
  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")

  "_field_update"       :: "ident => 'a => field_update"        ("(2_ :=/ _)")
  ""                    :: "field_update => field_updates"      ("_")
  "_field_updates"      :: "field_update => field_updates => field_updates"  ("_,/ _")
  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)

no_syntax (ASCII)
  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
  "_record_type_scheme" :: "field_types => type => type"        ("(3'(| _,/ (2... ::/ _) |'))")
  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)

(* copied and adapted from Record.thy *)

nonterminal
  field and
  fields and
  field_update and
  field_updates

syntax
  "_constify"               :: "id => ident"                        ("_")
  "_constify"               :: "longid => ident"                    ("_")

  "_bnf_field"              :: "ident => 'a => field"               ("(2_ =/ _)")
  ""                        :: "field => fields"                    ("_")
  "_bnf_fields"             :: "field => fields => fields"          ("_,/ _")
  "_bnf_record"             :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")
  "_bnf_field_update"       :: "ident => 'a => field_update"        ("(2_ :=/ _)")
  ""                        :: "field_update => field_updates"      ("_")
  "_bnf_field_updates"      :: "field_update => field_updates => field_updates"  ("_,/ _")
  "_bnf_record_update"      :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)

syntax (ASCII)
  "_bnf_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
  "_bnf_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
  "_bnf_record_update"      :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)

named_theorems bnf_record_update

ML_file "bnf_record.ML"
setup \<open>BNF_Record.setup\<close>

end
section \<open>Tests\<close>

theory Test_BNF_Record
imports BNF_Record
begin

subsection \<open>Standard usage\<close>

bnf_record ('a, 'b) foo =
  field_1 :: 'a
  field_2 :: 'b

lemma "\<lparr> field_1 = 3, field_2 = () \<rparr> = (make_foo 3 () :: (nat, unit) foo)" ..

lemma "(make_foo a b) \<lparr> field_1 := y \<rparr> = make_foo y b"
  by (simp add: bnf_record_update)

lemma "(make_foo a b) \<lparr> foo.field_1 := y \<rparr> = make_foo y b"
  by (simp add: bnf_record_update)

subsection \<open>Existing datatypes\<close>

datatype x = X (a: int) (b: int)

lemma "\<lparr> a = 1, b = 2 \<rparr> = X 1 2" ..

local_setup \<open>BNF_Record.mk_update_defs @{type_name x}\<close>

lemma "(X 1 2) \<lparr> b := 3 \<rparr> = X 1 3"
  by (simp add: bnf_record_update)

subsection \<open>Nested recursion\<close>

bnf_record 'a container =
  content :: "'a option"

datatype 'a contrived = Contrived "'a contrived container"

term "Contrived \<lparr> content = None \<rparr>"

end


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.