<commit_before>(*  Title:      HOL/Tools/record.ML
    Author:     <NAME>, TU Muenchen
    Author:     <NAME>, TU Muenchen
    Author:     <NAME>, TU Muenchen
    Author:     <NAME>, NICTA

Extensible records with structural subtyping.
*)

signature BASIC_RECORD =
sig
  type record_info =
   {args: (string * sort) list,
    parent: (typ list * string) option,
    fields: (string * typ) list,
    extension: (string * typ list),
    ext_induct: thm, ext_inject: thm, ext_surjective: thm, ext_split: thm, ext_def: thm,
    select_convs: thm list, update_convs: thm list, select_defs: thm list, update_defs: thm list,
    fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list,
    surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm,
    cases: thm, simps: thm list, iffs: thm list}
  val get_record: theory -> string -> record_info option
  val the_record: theory -> string -> record_info
  val record_simproc: simproc
  val record_eq_simproc: simproc
  val record_upd_simproc: simproc
  val record_split_simproc: (term -> int) -> simproc
  val record_ex_sel_eq_simproc: simproc
  val record_split_tac: int -> tactic
  val record_split_simp_tac: thm list -> (term -> int) -> int -> tactic
  val record_split_name: string
  val record_split_wrapper: string * wrapper
  val print_record_type_abbr: bool Unsynchronized.ref
  val print_record_type_as_fields: bool Unsynchronized.ref
end;

signature RECORD =
sig
  include BASIC_RECORD
  val timing: bool Unsynchronized.ref
  val updateN: string
  val ext_typeN: string
  val extN: string
  val makeN: string
  val moreN: string
  val last_extT: typ -> (string * typ list) option
  val dest_recTs: typ -> (string * typ list) list
  val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
  val get_recT_fields: theory -> typ -> (string * typ) list * (string * typ)
  val get_parent: theory -> string -> (typ list * string) option
  val get_extension: theory -> string -> (string * typ list) option
  val get_extinjects: theory -> thm list
  val get_simpset: theory -> simpset
  val print_records: theory -> unit
  val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list
  val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list
  val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
    (binding * typ * mixfix) list -> theory -> theory
  val add_record_cmd: bool -> (string * string option) list * binding -> string option ->
    (binding * string * mixfix) list -> theory -> theory
  val setup: theory -> theory
end;


signature ISO_TUPLE_SUPPORT =
sig
  val add_iso_tuple_type: bstring * (string * sort) list ->
    typ * typ -> theory -> (term * term) * theory
  val mk_cons_tuple: term * term -> term
  val dest_cons_tuple: term -> term * term
  val iso_tuple_intros_tac: int -> tactic
  val named_cterm_instantiate: (string * cterm) list -> thm -> thm
end;

structure Iso_Tuple_Support: ISO_TUPLE_SUPPORT =
struct

val isoN = "_Tuple_Iso";

val iso_tuple_intro = @{thm isomorphic_tuple_intro};
val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};

val tuple_iso_tuple = (@{const_name tuple_iso_tuple}, @{thm tuple_iso_tuple});

fun named_cterm_instantiate values thm =
  let
    fun match name ((name', _), _) = name = name';
    fun getvar name =
      (case find_first (match name) (Term.add_vars (prop_of thm) []) of
        SOME var => cterm_of (theory_of_thm thm) (Var var)
      | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]));
  in
    cterm_instantiate (map (apfst getvar) values) thm
  end;

structure Iso_Tuple_Thms = Theory_Data
(
  type T = thm Symtab.table;
  val empty = Symtab.make [tuple_iso_tuple];
  val extend = I;
  fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
);

fun do_typedef name repT alphas thy =
  let
    fun get_thms thy name =
      let
        val [({Abs_name, abs_type = absT, ...}, {Rep_inject, Abs_inverse, ...})] =
          Typedef.get_info_global thy name;
        val rewrite_rule =
          MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}];
      in
        (map rewrite_rule [Rep_inject, Abs_inverse], Const (Abs_name, repT --> absT), absT)
      end;
  in
    thy
    |> Typecopy.typecopy (Binding.name name, alphas) repT NONE
    |-> (fn (name, _) => `(fn thy => get_thms thy name))
  end;

fun mk_cons_tuple (left, right) =
  let
    val (leftT, rightT) = (fastype_of left, fastype_of right);
    val prodT = HOLogic.mk_prodT (leftT, rightT);
    val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]);
  in
    Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
      Const (fst tuple_iso_tuple, isomT) $ left $ right
  end;

fun dest_cons_tuple (Const (@{const_name iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
  | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);

fun add_iso_tuple_type (name, alphas) (leftT, rightT) thy =
  let
    val repT = HOLogic.mk_prodT (leftT, rightT);

    val (([rep_inject, abs_inverse], absC, absT), typ_thy) =
      thy
      |> do_typedef name repT alphas
      ||> Sign.add_path name;

    (*construct a type and body for the isomorphism constant by
      instantiating the theorem to which the definition will be applied*)
    val intro_inst =
      rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
    val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
    val isomT = fastype_of body;
    val isom_binding = Binding.name (name ^ isoN);
    val isom_name = Sign.full_name typ_thy isom_binding;
    val isom = Const (isom_name, isomT);

    val ([isom_def], cdef_thy) =
      typ_thy
      |> Sign.declare_const ((isom_binding, isomT), NoSyn) |> snd
      |> PureThy.add_defs false
        [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];

    val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
    val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT);

    val thm_thy =
      cdef_thy
      |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
      |> Sign.restore_naming thy
      |> Code.add_default_eqn isom_def;
  in
    ((isom, cons $ isom), thm_thy)
  end;

val iso_tuple_intros_tac =
  resolve_from_net_tac iso_tuple_intros THEN'
  CSUBGOAL (fn (cgoal, i) =>
    let
      val thy = Thm.theory_of_cterm cgoal;
      val goal = Thm.term_of cgoal;

      val isthms = Iso_Tuple_Thms.get thy;
      fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]);

      val goal' = Envir.beta_eta_contract goal;
      val is =
        (case goal' of
          Const (@{const_name Trueprop}, _) $
            (Const (@{const_name isomorphic_tuple}, _) $ Const is) => is
        | _ => err "unexpected goal format" goal');
      val isthm =
        (case Symtab.lookup isthms (#1 is) of
          SOME isthm => isthm
        | NONE => err "no thm found for constant" (Const is));
    in rtac isthm i end);

end;


structure Record: RECORD =
struct

val eq_reflection = @{thm eq_reflection};
val atomize_all = @{thm HOL.atomize_all};
val atomize_imp = @{thm HOL.atomize_imp};
val meta_allE = @{thm Pure.meta_allE};
val prop_subst = @{thm prop_subst};
val K_record_comp = @{thm K_record_comp};
val K_comp_convs = [@{thm o_apply}, K_record_comp];
val o_assoc = @{thm o_assoc};
val id_apply = @{thm id_apply};
val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
val Not_eq_iff = @{thm Not_eq_iff};

val refl_conj_eq = @{thm refl_conj_eq};

val surject_assistI = @{thm iso_tuple_surjective_proof_assistI};
val surject_assist_idE = @{thm iso_tuple_surjective_proof_assist_idE};

val updacc_accessor_eqE = @{thm update_accessor_accessor_eqE};
val updacc_updator_eqE = @{thm update_accessor_updator_eqE};
val updacc_eq_idI = @{thm iso_tuple_update_accessor_eq_assist_idI};
val updacc_eq_triv = @{thm iso_tuple_update_accessor_eq_assist_triv};

val updacc_foldE = @{thm update_accessor_congruence_foldE};
val updacc_unfoldE = @{thm update_accessor_congruence_unfoldE};
val updacc_noopE = @{thm update_accessor_noopE};
val updacc_noop_compE = @{thm update_accessor_noop_compE};
val updacc_cong_idI = @{thm update_accessor_cong_assist_idI};
val updacc_cong_triv = @{thm update_accessor_cong_assist_triv};
val updacc_cong_from_eq = @{thm iso_tuple_update_accessor_cong_from_eq};

val o_eq_dest = @{thm o_eq_dest};
val o_eq_id_dest = @{thm o_eq_id_dest};
val o_eq_dest_lhs = @{thm o_eq_dest_lhs};



(** name components **)

val rN = "r";
val wN = "w";
val moreN = "more";
val schemeN = "_scheme";
val ext_typeN = "_ext_type";
val inner_typeN = "_inner_type";
val extN ="_ext";
val updateN = "_update";
val makeN = "make";
val fields_selN = "fields";
val extendN = "extend";
val truncateN = "truncate";



(*** utilities ***)

fun but_last xs = fst (split_last xs);

fun varifyT midx =
  let fun varify (a, S) = TVar ((a, midx + 1), S);
  in map_type_tfree varify end;


(* timing *)

val timing = Unsynchronized.ref false;
fun timeit_msg s x = if ! timing then (warning s; timeit x) else x ();
fun timing_msg s = if ! timing then warning s else ();


(* syntax *)

val Trueprop = HOLogic.mk_Trueprop;
fun All xs t = Term.list_all_free (xs, t);

infix 0 :== ===;
infixr 0 ==>;

val op :== = OldGoals.mk_defpair;
val op === = Trueprop o HOLogic.mk_eq;
val op ==> = Logic.mk_implies;


(* constructor *)

fun mk_ext (name, T) ts =
  let val Ts = map fastype_of ts
  in list_comb (Const (suffix extN name, Ts ---> T), ts) end;


(* selector *)

fun mk_selC sT (c, T) = (c, sT --> T);

fun mk_sel s (c, T) =
  let val sT = fastype_of s
  in Const (mk_selC sT (c, T)) $ s end;


(* updates *)

fun mk_updC sfx sT (c, T) = (suffix sfx c, (T --> T) --> sT --> sT);

fun mk_upd' sfx c v sT =
  let val vT = domain_type (fastype_of v);
  in Const (mk_updC sfx sT (c, vT)) $ v end;

fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s;


(* types *)

fun dest_recT (typ as Type (c_ext_type, Ts as (_ :: _))) =
      (case try (unsuffix ext_typeN) c_ext_type of
        NONE => raise TYPE ("Record.dest_recT", [typ], [])
      | SOME c => ((c, Ts), List.last Ts))
  | dest_recT typ = raise TYPE ("Record.dest_recT", [typ], []);

val is_recT = can dest_recT;

fun dest_recTs T =
  let val ((c, Ts), U) = dest_recT T
  in (c, Ts) :: dest_recTs U
  end handle TYPE _ => [];

fun last_extT T =
  let val ((c, Ts), U) = dest_recT T in
    (case last_extT U of
      NONE => SOME (c, Ts)
    | SOME l => SOME l)
  end handle TYPE _ => NONE;

fun rec_id i T =
  let
    val rTs = dest_recTs T;
    val rTs' = if i < 0 then rTs else take i rTs;
  in implode (map #1 rTs') end;



(*** extend theory by record definition ***)

(** record info **)

(* type record_info and parent_info *)

type record_info =
 {args: (string * sort) list,
  parent: (typ list * string) option,
  fields: (string * typ) list,
  extension: (string * typ list),

  ext_induct: thm,
  ext_inject: thm,
  ext_surjective: thm,
  ext_split: thm,
  ext_def: thm,

  select_convs: thm list,
  update_convs: thm list,
  select_defs: thm list,
  update_defs: thm list,
  fold_congs: thm list,
  unfold_congs: thm list,
  splits: thm list,
  defs: thm list,

  surjective: thm,
  equality: thm,
  induct_scheme: thm,
  induct: thm,
  cases_scheme: thm,
  cases: thm,

  simps: thm list,
  iffs: thm list};

fun make_record_info args parent fields extension
    ext_induct ext_inject ext_surjective ext_split ext_def
    select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs
    surjective equality induct_scheme induct cases_scheme cases
    simps iffs : record_info =
 {args = args, parent = parent, fields = fields, extension = extension,
  ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective,
  ext_split = ext_split, ext_def = ext_def, select_convs = select_convs,
  update_convs = update_convs, select_defs = select_defs, update_defs = update_defs,
  fold_congs = fold_congs, unfold_congs = unfold_congs, splits = splits, defs = defs,
  surjective = surjective, equality = equality, induct_scheme = induct_scheme,
  induct = induct, cases_scheme = cases_scheme, cases = cases, simps = simps, iffs = iffs};

type parent_info =
 {name: string,
  fields: (string * typ) list,
  extension: (string * typ list),
  induct_scheme: thm,
  ext_def: thm};

fun make_parent_info name fields extension ext_def induct_scheme : parent_info =
 {name = name, fields = fields, extension = extension,
  ext_def = ext_def, induct_scheme = induct_scheme};


(* theory data *)

type record_data =
 {records: record_info Symtab.table,
  sel_upd:
   {selectors: (int * bool) Symtab.table,
    updates: string Symtab.table,
    simpset: Simplifier.simpset,
    defset: Simplifier.simpset,
    foldcong: Simplifier.simpset,
    unfoldcong: Simplifier.simpset},
  equalities: thm Symtab.table,
  extinjects: thm list,
  extsplit: thm Symtab.table,  (*maps extension name to split rule*)
  splits: (thm * thm * thm * thm) Symtab.table,  (*!!, ALL, EX - split-equalities, induct rule*)
  extfields: (string * typ) list Symtab.table,  (*maps extension to its fields*)
  fieldext: (string * typ list) Symtab.table};  (*maps field to its extension*)

fun make_record_data
    records sel_upd equalities extinjects extsplit splits extfields fieldext =
 {records = records, sel_upd = sel_upd,
  equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
  extfields = extfields, fieldext = fieldext }: record_data;

structure Records_Data = Theory_Data
(
  type T = record_data;
  val empty =
    make_record_data Symtab.empty
      {selectors = Symtab.empty, updates = Symtab.empty,
          simpset = HOL_basic_ss, defset = HOL_basic_ss,
          foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
       Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
  val extend = I;
  fun merge
   ({records = recs1,
     sel_upd =
      {selectors = sels1, updates = upds1,
       simpset = ss1, defset = ds1,
       foldcong = fc1, unfoldcong = uc1},
     equalities = equalities1,
     extinjects = extinjects1,
     extsplit = extsplit1,
     splits = splits1,
     extfields = extfields1,
     fieldext = fieldext1},
    {records = recs2,
     sel_upd =
      {selectors = sels2, updates = upds2,
       simpset = ss2, defset = ds2,
       foldcong = fc2, unfoldcong = uc2},
     equalities = equalities2,
     extinjects = extinjects2,
     extsplit = extsplit2,
     splits = splits2,
     extfields = extfields2,
     fieldext = fieldext2}) =
    make_record_data
      (Symtab.merge (K true) (recs1, recs2))
      {selectors = Symtab.merge (K true) (sels1, sels2),
        updates = Symtab.merge (K true) (upds1, upds2),
        simpset = Simplifier.merge_ss (ss1, ss2),
        defset = Simplifier.merge_ss (ds1, ds2),
        foldcong = Simplifier.merge_ss (fc1, fc2),
        unfoldcong = Simplifier.merge_ss (uc1, uc2)}
      (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
      (Thm.merge_thms (extinjects1, extinjects2))
      (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
      (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
          Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
          Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
      (Symtab.merge (K true) (extfields1, extfields2))
      (Symtab.merge (K true) (fieldext1, fieldext2));
);

fun print_records thy =
  let
    val {records = recs, ...} = Records_Data.get thy;
    val prt_typ = Syntax.pretty_typ_global thy;

    fun pretty_parent NONE = []
      | pretty_parent (SOME (Ts, name)) =
          [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];

    fun pretty_field (c, T) = Pretty.block
      [Pretty.str (Sign.extern_const thy c), Pretty.str " ::",
        Pretty.brk 1, Pretty.quote (prt_typ T)];

    fun pretty_record (name, {args, parent, fields, ...}: record_info) =
      Pretty.block (Pretty.fbreaks (Pretty.block
        [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
        pretty_parent parent @ map pretty_field fields));
  in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;


(* access 'records' *)

val get_record = Symtab.lookup o #records o Records_Data.get;

fun the_record thy name =
  (case get_record thy name of
    SOME info => info
  | NONE => error ("Unknown record type " ^ quote name));

fun put_record name info thy =
  let
    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
      Records_Data.get thy;
    val data = make_record_data (Symtab.update (name, info) records)
      sel_upd equalities extinjects extsplit splits extfields fieldext;
  in Records_Data.put data thy end;


(* access 'sel_upd' *)

val get_sel_upd = #sel_upd o Records_Data.get;

val is_selector = Symtab.defined o #selectors o get_sel_upd;
val get_updates = Symtab.lookup o #updates o get_sel_upd;
fun get_ss_with_context getss thy = Simplifier.global_context thy (getss (get_sel_upd thy));

val get_simpset = get_ss_with_context #simpset;
val get_sel_upd_defs = get_ss_with_context #defset;

fun get_update_details u thy =
  let val sel_upd = get_sel_upd thy in
    (case Symtab.lookup (#updates sel_upd) u of
      SOME s =>
        let val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s
        in SOME (s, dep, ismore) end
    | NONE => NONE)
  end;

fun put_sel_upd names more depth simps defs (folds, unfolds) thy =
  let
    val all = names @ [more];
    val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
    val upds = map (suffix updateN) all ~~ all;

    val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
      equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy;
    val data = make_record_data records
      {selectors = fold Symtab.update_new sels selectors,
        updates = fold Symtab.update_new upds updates,
        simpset = Simplifier.addsimps (simpset, simps),
        defset = Simplifier.addsimps (defset, defs),
        foldcong = foldcong addcongs folds,
        unfoldcong = unfoldcong addcongs unfolds}
       equalities extinjects extsplit splits extfields fieldext;
  in Records_Data.put data thy end;


(* access 'equalities' *)

fun add_record_equalities name thm thy =
  let
    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
      Records_Data.get thy;
    val data = make_record_data records sel_upd
      (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext;
  in Records_Data.put data thy end;

val get_equalities = Symtab.lookup o #equalities o Records_Data.get;


(* access 'extinjects' *)

fun add_extinjects thm thy =
  let
    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
      Records_Data.get thy;
    val data =
      make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
        extsplit splits extfields fieldext;
  in Records_Data.put data thy end;

val get_extinjects = rev o #extinjects o Records_Data.get;


(* access 'extsplit' *)

fun add_extsplit name thm thy =
  let
    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
      Records_Data.get thy;
    val data =
      make_record_data records sel_upd equalities extinjects
        (Symtab.update_new (name, thm) extsplit) splits extfields fieldext;
  in Records_Data.put data thy end;


(* access 'splits' *)

fun add_record_splits name thmP thy =
  let
    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
      Records_Data.get thy;
    val data =
      make_record_data records sel_upd equalities extinjects extsplit
        (Symtab.update_new (name, thmP) splits) extfields fieldext;
  in Records_Data.put data thy end;

val get_splits = Symtab.lookup o #splits o Records_Data.get;


(* parent/extension of named record *)

val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Records_Data.get);
val get_extension = Option.map #extension oo (Symtab.lookup o #records o Records_Data.get);


(* access 'extfields' *)

fun add_extfields name fields thy =
  let
    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
      Records_Data.get thy;
    val data =
      make_record_data records sel_upd equalities extinjects extsplit splits
        (Symtab.update_new (name, fields) extfields) fieldext;
  in Records_Data.put data thy end;

val get_extfields = Symtab.lookup o #extfields o Records_Data.get;

fun get_extT_fields thy T =
  let
    val ((name, Ts), moreT) = dest_recT T;
    val recname =
      let val (nm :: _ :: rst) = rev (Long_Name.explode name)   (* FIXME !? *)
      in Long_Name.implode (rev (nm :: rst)) end;
    val midx = maxidx_of_typs (moreT :: Ts);
    val varifyT = varifyT midx;
    val {records, extfields, ...} = Records_Data.get thy;
    val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
    val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));

    val subst = fold (Sign.typ_match thy) (but_last args ~~ but_last Ts) Vartab.empty;
    val fields' = map (apsnd (Envir.norm_type subst o varifyT)) fields;
  in (fields', (more, moreT)) end;

fun get_recT_fields thy T =
  let
    val (root_fields, (root_more, root_moreT)) = get_extT_fields thy T;
    val (rest_fields, rest_more) =
      if is_recT root_moreT then get_recT_fields thy root_moreT
      else ([], (root_more, root_moreT));
  in (root_fields @ rest_fields, rest_more) end;


(* access 'fieldext' *)

fun add_fieldext extname_types fields thy =
  let
    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
      Records_Data.get thy;
    val fieldext' =
      fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
    val data =
      make_record_data records sel_upd equalities extinjects
        extsplit splits extfields fieldext';
  in Records_Data.put data thy end;

val get_fieldext = Symtab.lookup o #fieldext o Records_Data.get;


(* parent records *)

fun add_parents _ NONE parents = parents
  | add_parents thy (SOME (types, name)) parents =
      let
        fun err msg = error (msg ^ " parent record " ^ quote name);

        val {args, parent, fields, extension, induct_scheme, ext_def, ...} =
          (case get_record thy name of SOME info => info | NONE => err "Unknown");
        val _ = if length types <> length args then err "Bad number of arguments for" else ();

        fun bad_inst ((x, S), T) =
          if Sign.of_sort thy (T, S) then NONE else SOME x
        val bads = map_filter bad_inst (args ~~ types);
        val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");

        val inst = map fst args ~~ types;
        val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
        val parent' = Option.map (apfst (map subst)) parent;
        val fields' = map (apsnd subst) fields;
        val extension' = apsnd (map subst) extension;
      in
        add_parents thy parent'
          (make_parent_info name fields' extension' ext_def induct_scheme :: parents)
      end;



(** concrete syntax for records **)

(* decode type *)

fun decode_type thy t =
  let
    fun get_sort env xi =
      the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname));
  in
    Syntax.typ_of_term (get_sort (Syntax.term_sorts t)) t
  end;


(* parse translations *)

local

fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
      (name, arg)
  | field_type_tr t = raise TERM ("field_type_tr", [t]);

fun field_types_tr (Const (@{syntax_const "_field_types"}, _) $ t $ u) =
      field_type_tr t :: field_types_tr u
  | field_types_tr t = [field_type_tr t];

fun record_field_types_tr more ctxt t =
  let
    val thy = ProofContext.theory_of ctxt;
    fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);

    fun split_args (field :: fields) ((name, arg) :: fargs) =
          if can (unsuffix name) field then
            let val (args, rest) = split_args fields fargs
            in (arg :: args, rest) end
          else err ("expecting field " ^ field ^ " but got " ^ name)
      | split_args [] (fargs as (_ :: _)) = ([], fargs)
      | split_args (_ :: _) [] = err "expecting more fields"
      | split_args _ _ = ([], []);

    fun mk_ext (fargs as (name, _) :: _) =
          (case get_fieldext thy (Sign.intern_const thy name) of
            SOME (ext, alphas) =>
              (case get_extfields thy ext of
                SOME fields =>
                  let
                    val fields' = but_last fields;
                    val types = map snd fields';
                    val (args, rest) = split_args (map fst fields') fargs;
                    val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
                    val midx = fold Term.maxidx_typ argtypes 0;
                    val varifyT = varifyT midx;
                    val vartypes = map varifyT types;

                    val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes) Vartab.empty
                      handle Type.TYPE_MATCH => err "type is no proper record (extension)";
                    val alphas' =
                      map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT)
                        (but_last alphas);

                    val more' = mk_ext rest;
                  in
                    list_comb
                      (Syntax.const (Syntax.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
                  end
              | NONE => err ("no fields defined for " ^ ext))
          | NONE => err (name ^ " is no proper field"))
      | mk_ext [] = more;
  in
    mk_ext (field_types_tr t)
  end;

fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const @{type_syntax unit}) ctxt t
  | record_type_tr _ ts = raise TERM ("record_type_tr", ts);

fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t
  | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts);


fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg)
  | field_tr t = raise TERM ("field_tr", [t]);

fun fields_tr (Const (@{syntax_const "_fields"}, _) $ t $ u) = field_tr t :: fields_tr u
  | fields_tr t = [field_tr t];

fun record_fields_tr more ctxt t =
  let
    val thy = ProofContext.theory_of ctxt;
    fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);

    fun split_args (field :: fields) ((name, arg) :: fargs) =
          if can (unsuffix name) field
          then
            let val (args, rest) = split_args fields fargs
            in (arg :: args, rest) end
          else err ("expecting field " ^ field ^ " but got " ^ name)
      | split_args [] (fargs as (_ :: _)) = ([], fargs)
      | split_args (_ :: _) [] = err "expecting more fields"
      | split_args _ _ = ([], []);

    fun mk_ext (fargs as (name, _) :: _) =
          (case get_fieldext thy (Sign.intern_const thy name) of
            SOME (ext, _) =>
              (case get_extfields thy ext of
                SOME fields =>
                  let
                    val (args, rest) = split_args (map fst (but_last fields)) fargs;
                    val more' = mk_ext rest;
                  in list_comb (Syntax.const (Syntax.mark_const (ext ^ extN)), args @ [more']) end
              | NONE => err ("no fields defined for " ^ ext))
          | NONE => err (name ^ " is no proper field"))
      | mk_ext [] = more;
  in mk_ext (fields_tr t) end;

fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t
  | record_tr _ ts = raise TERM ("record_tr", ts);

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


fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
      Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg)
  | field_update_tr t = raise TERM ("field_update_tr", [t]);

fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
      field_update_tr t :: field_updates_tr u
  | field_updates_tr t = [field_update_tr t];

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

in

val parse_translation =
 [(@{syntax_const "_record_update"}, record_update_tr)];

val advanced_parse_translation =
 [(@{syntax_const "_record"}, record_tr),
  (@{syntax_const "_record_scheme"}, record_scheme_tr),
  (@{syntax_const "_record_type"}, record_type_tr),
  (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];

end;


(* print translations *)

val print_record_type_abbr = Unsynchronized.ref true;
val print_record_type_as_fields = Unsynchronized.ref true;


local

(* FIXME early extern (!??) *)
(* FIXME Syntax.free (??) *)
fun field_type_tr' (c, t) = Syntax.const @{syntax_const "_field_type"} $ Syntax.const c $ t;

fun field_types_tr' (t, u) = Syntax.const @{syntax_const "_field_types"} $ t $ u;

fun record_type_tr' ctxt t =
  let
    val thy = ProofContext.theory_of ctxt;

    val T = decode_type thy t;
    val varifyT = varifyT (Term.maxidx_of_typ T);

    val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts);

    fun strip_fields T =
      (case T of
        Type (ext, args as _ :: _) =>
          (case try (unsuffix ext_typeN) ext of
            SOME ext' =>
              (case get_extfields thy ext' of
                SOME (fields as (x, _) :: _) =>
                  (case get_fieldext thy x of
                    SOME (_, alphas) =>
                     (let
                        val f :: fs = but_last fields;
                        val fields' =
                          apfst (Sign.extern_const thy) f :: map (apfst Long_Name.base_name) fs;
                        val (args', more) = split_last args;
                        val alphavars = map varifyT (but_last alphas);
                        val subst = fold (Sign.typ_match thy) (alphavars ~~ args') Vartab.empty;
                        val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
                      in fields'' @ strip_fields more end
                      handle Type.TYPE_MATCH => [("", T)]
                        | Library.UnequalLengths => [("", T)])
                  | _ => [("", T)])
              | _ => [("", T)])
          | _ => [("", T)])
      | _ => [("", T)]);

    val (fields, (_, moreT)) = split_last (strip_fields T);
    val _ = null fields andalso raise Match;
    val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields);
  in
    if not (! print_record_type_as_fields) orelse null fields then raise Match
    else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
    else Syntax.const @{syntax_const "_record_type_scheme"} $ u $ term_of_type moreT
  end;

(*try to reconstruct the record name type abbreviation from
  the (nested) extension types*)
fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
  let
    val thy = ProofContext.theory_of ctxt;
    val T = decode_type thy tm;
    val midx = maxidx_of_typ T;
    val varifyT = varifyT midx;

    fun mk_type_abbr subst name args =
      let val abbrT = Type (name, map (varifyT o TFree) args)
      in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;

    fun match rT T = Sign.typ_match thy (varifyT rT, T) Vartab.empty;
  in
    if ! print_record_type_abbr then
      (case last_extT T of
        SOME (name, _) =>
          if name = last_ext then
            let val subst = match schemeT T in
              if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta)))
              then mk_type_abbr subst abbr alphas
              else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
            end handle Type.TYPE_MATCH => record_type_tr' ctxt tm
          else raise Match (*give print translation of specialised record a chance*)
      | _ => raise Match)
    else record_type_tr' ctxt tm
  end;

in

fun record_ext_type_tr' name =
  let
    val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
    fun tr' ctxt ts =
      record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
  in (ext_type_name, tr') end;
<commit_msg>more robust record syntax: use Type.raw_match to ignore sort constraints as in regular abbreviations (also note that constraints only affect operations, not types);<commit_after>(*  Title:      HOL/Tools/record.ML
    Author:     <NAME>, TU Muenchen
    Author:     <NAME>, TU Muenchen
    Author:     <NAME>, TU Muenchen
    Author:     <NAME>, NICTA

Extensible records with structural subtyping.
*)

signature BASIC_RECORD =
sig
  type record_info =
   {args: (string * sort) list,
    parent: (typ list * string) option,
    fields: (string * typ) list,
    extension: (string * typ list),
    ext_induct: thm, ext_inject: thm, ext_surjective: thm, ext_split: thm, ext_def: thm,
    select_convs: thm list, update_convs: thm list, select_defs: thm list, update_defs: thm list,
    fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list,
    surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm,
    cases: thm, simps: thm list, iffs: thm list}
  val get_record: theory -> string -> record_info option
  val the_record: theory -> string -> record_info
  val record_simproc: simproc
  val record_eq_simproc: simproc
  val record_upd_simproc: simproc
  val record_split_simproc: (term -> int) -> simproc
  val record_ex_sel_eq_simproc: simproc
  val record_split_tac: int -> tactic
  val record_split_simp_tac: thm list -> (term -> int) -> int -> tactic
  val record_split_name: string
  val record_split_wrapper: string * wrapper
  val print_record_type_abbr: bool Unsynchronized.ref
  val print_record_type_as_fields: bool Unsynchronized.ref
end;

signature RECORD =
sig
  include BASIC_RECORD
  val timing: bool Unsynchronized.ref
  val updateN: string
  val ext_typeN: string
  val extN: string
  val makeN: string
  val moreN: string
  val last_extT: typ -> (string * typ list) option
  val dest_recTs: typ -> (string * typ list) list
  val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
  val get_recT_fields: theory -> typ -> (string * typ) list * (string * typ)
  val get_parent: theory -> string -> (typ list * string) option
  val get_extension: theory -> string -> (string * typ list) option
  val get_extinjects: theory -> thm list
  val get_simpset: theory -> simpset
  val print_records: theory -> unit
  val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list
  val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list
  val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
    (binding * typ * mixfix) list -> theory -> theory
  val add_record_cmd: bool -> (string * string option) list * binding -> string option ->
    (binding * string * mixfix) list -> theory -> theory
  val setup: theory -> theory
end;


signature ISO_TUPLE_SUPPORT =
sig
  val add_iso_tuple_type: bstring * (string * sort) list ->
    typ * typ -> theory -> (term * term) * theory
  val mk_cons_tuple: term * term -> term
  val dest_cons_tuple: term -> term * term
  val iso_tuple_intros_tac: int -> tactic
  val named_cterm_instantiate: (string * cterm) list -> thm -> thm
end;

structure Iso_Tuple_Support: ISO_TUPLE_SUPPORT =
struct

val isoN = "_Tuple_Iso";

val iso_tuple_intro = @{thm isomorphic_tuple_intro};
val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};

val tuple_iso_tuple = (@{const_name tuple_iso_tuple}, @{thm tuple_iso_tuple});

fun named_cterm_instantiate values thm =
  let
    fun match name ((name', _), _) = name = name';
    fun getvar name =
      (case find_first (match name) (Term.add_vars (prop_of thm) []) of
        SOME var => cterm_of (theory_of_thm thm) (Var var)
      | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]));
  in
    cterm_instantiate (map (apfst getvar) values) thm
  end;

structure Iso_Tuple_Thms = Theory_Data
(
  type T = thm Symtab.table;
  val empty = Symtab.make [tuple_iso_tuple];
  val extend = I;
  fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
);

fun do_typedef name repT alphas thy =
  let
    fun get_thms thy name =
      let
        val [({Abs_name, abs_type = absT, ...}, {Rep_inject, Abs_inverse, ...})] =
          Typedef.get_info_global thy name;
        val rewrite_rule =
          MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}];
      in
        (map rewrite_rule [Rep_inject, Abs_inverse], Const (Abs_name, repT --> absT), absT)
      end;
  in
    thy
    |> Typecopy.typecopy (Binding.name name, alphas) repT NONE
    |-> (fn (name, _) => `(fn thy => get_thms thy name))
  end;

fun mk_cons_tuple (left, right) =
  let
    val (leftT, rightT) = (fastype_of left, fastype_of right);
    val prodT = HOLogic.mk_prodT (leftT, rightT);
    val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]);
  in
    Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
      Const (fst tuple_iso_tuple, isomT) $ left $ right
  end;

fun dest_cons_tuple (Const (@{const_name iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
  | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);

fun add_iso_tuple_type (name, alphas) (leftT, rightT) thy =
  let
    val repT = HOLogic.mk_prodT (leftT, rightT);

    val (([rep_inject, abs_inverse], absC, absT), typ_thy) =
      thy
      |> do_typedef name repT alphas
      ||> Sign.add_path name;

    (*construct a type and body for the isomorphism constant by
      instantiating the theorem to which the definition will be applied*)
    val intro_inst =
      rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
    val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
    val isomT = fastype_of body;
    val isom_binding = Binding.name (name ^ isoN);
    val isom_name = Sign.full_name typ_thy isom_binding;
    val isom = Const (isom_name, isomT);

    val ([isom_def], cdef_thy) =
      typ_thy
      |> Sign.declare_const ((isom_binding, isomT), NoSyn) |> snd
      |> PureThy.add_defs false
        [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];

    val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
    val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT);

    val thm_thy =
      cdef_thy
      |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
      |> Sign.restore_naming thy
      |> Code.add_default_eqn isom_def;
  in
    ((isom, cons $ isom), thm_thy)
  end;

val iso_tuple_intros_tac =
  resolve_from_net_tac iso_tuple_intros THEN'
  CSUBGOAL (fn (cgoal, i) =>
    let
      val thy = Thm.theory_of_cterm cgoal;
      val goal = Thm.term_of cgoal;

      val isthms = Iso_Tuple_Thms.get thy;
      fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]);

      val goal' = Envir.beta_eta_contract goal;
      val is =
        (case goal' of
          Const (@{const_name Trueprop}, _) $
            (Const (@{const_name isomorphic_tuple}, _) $ Const is) => is
        | _ => err "unexpected goal format" goal');
      val isthm =
        (case Symtab.lookup isthms (#1 is) of
          SOME isthm => isthm
        | NONE => err "no thm found for constant" (Const is));
    in rtac isthm i end);

end;


structure Record: RECORD =
struct

val eq_reflection = @{thm eq_reflection};
val atomize_all = @{thm HOL.atomize_all};
val atomize_imp = @{thm HOL.atomize_imp};
val meta_allE = @{thm Pure.meta_allE};
val prop_subst = @{thm prop_subst};
val K_record_comp = @{thm K_record_comp};
val K_comp_convs = [@{thm o_apply}, K_record_comp];
val o_assoc = @{thm o_assoc};
val id_apply = @{thm id_apply};
val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
val Not_eq_iff = @{thm Not_eq_iff};

val refl_conj_eq = @{thm refl_conj_eq};

val surject_assistI = @{thm iso_tuple_surjective_proof_assistI};
val surject_assist_idE = @{thm iso_tuple_surjective_proof_assist_idE};

val updacc_accessor_eqE = @{thm update_accessor_accessor_eqE};
val updacc_updator_eqE = @{thm update_accessor_updator_eqE};
val updacc_eq_idI = @{thm iso_tuple_update_accessor_eq_assist_idI};
val updacc_eq_triv = @{thm iso_tuple_update_accessor_eq_assist_triv};

val updacc_foldE = @{thm update_accessor_congruence_foldE};
val updacc_unfoldE = @{thm update_accessor_congruence_unfoldE};
val updacc_noopE = @{thm update_accessor_noopE};
val updacc_noop_compE = @{thm update_accessor_noop_compE};
val updacc_cong_idI = @{thm update_accessor_cong_assist_idI};
val updacc_cong_triv = @{thm update_accessor_cong_assist_triv};
val updacc_cong_from_eq = @{thm iso_tuple_update_accessor_cong_from_eq};

val o_eq_dest = @{thm o_eq_dest};
val o_eq_id_dest = @{thm o_eq_id_dest};
val o_eq_dest_lhs = @{thm o_eq_dest_lhs};



(** name components **)

val rN = "r";
val wN = "w";
val moreN = "more";
val schemeN = "_scheme";
val ext_typeN = "_ext_type";
val inner_typeN = "_inner_type";
val extN ="_ext";
val updateN = "_update";
val makeN = "make";
val fields_selN = "fields";
val extendN = "extend";
val truncateN = "truncate";



(*** utilities ***)

fun but_last xs = fst (split_last xs);

fun varifyT midx =
  let fun varify (a, S) = TVar ((a, midx + 1), S);
  in map_type_tfree varify end;


(* timing *)

val timing = Unsynchronized.ref false;
fun timeit_msg s x = if ! timing then (warning s; timeit x) else x ();
fun timing_msg s = if ! timing then warning s else ();


(* syntax *)

val Trueprop = HOLogic.mk_Trueprop;
fun All xs t = Term.list_all_free (xs, t);

infix 0 :== ===;
infixr 0 ==>;

val op :== = OldGoals.mk_defpair;
val op === = Trueprop o HOLogic.mk_eq;
val op ==> = Logic.mk_implies;


(* constructor *)

fun mk_ext (name, T) ts =
  let val Ts = map fastype_of ts
  in list_comb (Const (suffix extN name, Ts ---> T), ts) end;


(* selector *)

fun mk_selC sT (c, T) = (c, sT --> T);

fun mk_sel s (c, T) =
  let val sT = fastype_of s
  in Const (mk_selC sT (c, T)) $ s end;


(* updates *)

fun mk_updC sfx sT (c, T) = (suffix sfx c, (T --> T) --> sT --> sT);

fun mk_upd' sfx c v sT =
  let val vT = domain_type (fastype_of v);
  in Const (mk_updC sfx sT (c, vT)) $ v end;

fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s;


(* types *)

fun dest_recT (typ as Type (c_ext_type, Ts as (_ :: _))) =
      (case try (unsuffix ext_typeN) c_ext_type of
        NONE => raise TYPE ("Record.dest_recT", [typ], [])
      | SOME c => ((c, Ts), List.last Ts))
  | dest_recT typ = raise TYPE ("Record.dest_recT", [typ], []);

val is_recT = can dest_recT;

fun dest_recTs T =
  let val ((c, Ts), U) = dest_recT T
  in (c, Ts) :: dest_recTs U
  end handle TYPE _ => [];

fun last_extT T =
  let val ((c, Ts), U) = dest_recT T in
    (case last_extT U of
      NONE => SOME (c, Ts)
    | SOME l => SOME l)
  end handle TYPE _ => NONE;

fun rec_id i T =
  let
    val rTs = dest_recTs T;
    val rTs' = if i < 0 then rTs else take i rTs;
  in implode (map #1 rTs') end;



(*** extend theory by record definition ***)

(** record info **)

(* type record_info and parent_info *)

type record_info =
 {args: (string * sort) list,
  parent: (typ list * string) option,
  fields: (string * typ) list,
  extension: (string * typ list),

  ext_induct: thm,
  ext_inject: thm,
  ext_surjective: thm,
  ext_split: thm,
  ext_def: thm,

  select_convs: thm list,
  update_convs: thm list,
  select_defs: thm list,
  update_defs: thm list,
  fold_congs: thm list,
  unfold_congs: thm list,
  splits: thm list,
  defs: thm list,

  surjective: thm,
  equality: thm,
  induct_scheme: thm,
  induct: thm,
  cases_scheme: thm,
  cases: thm,

  simps: thm list,
  iffs: thm list};

fun make_record_info args parent fields extension
    ext_induct ext_inject ext_surjective ext_split ext_def
    select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs
    surjective equality induct_scheme induct cases_scheme cases
    simps iffs : record_info =
 {args = args, parent = parent, fields = fields, extension = extension,
  ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective,
  ext_split = ext_split, ext_def = ext_def, select_convs = select_convs,
  update_convs = update_convs, select_defs = select_defs, update_defs = update_defs,
  fold_congs = fold_congs, unfold_congs = unfold_congs, splits = splits, defs = defs,
  surjective = surjective, equality = equality, induct_scheme = induct_scheme,
  induct = induct, cases_scheme = cases_scheme, cases = cases, simps = simps, iffs = iffs};

type parent_info =
 {name: string,
  fields: (string * typ) list,
  extension: (string * typ list),
  induct_scheme: thm,
  ext_def: thm};

fun make_parent_info name fields extension ext_def induct_scheme : parent_info =
 {name = name, fields = fields, extension = extension,
  ext_def = ext_def, induct_scheme = induct_scheme};


(* theory data *)

type record_data =
 {records: record_info Symtab.table,
  sel_upd:
   {selectors: (int * bool) Symtab.table,
    updates: string Symtab.table,
    simpset: Simplifier.simpset,
    defset: Simplifier.simpset,
    foldcong: Simplifier.simpset,
    unfoldcong: Simplifier.simpset},
  equalities: thm Symtab.table,
  extinjects: thm list,
  extsplit: thm Symtab.table,  (*maps extension name to split rule*)
  splits: (thm * thm * thm * thm) Symtab.table,  (*!!, ALL, EX - split-equalities, induct rule*)
  extfields: (string * typ) list Symtab.table,  (*maps extension to its fields*)
  fieldext: (string * typ list) Symtab.table};  (*maps field to its extension*)

fun make_record_data
    records sel_upd equalities extinjects extsplit splits extfields fieldext =
 {records = records, sel_upd = sel_upd,
  equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
  extfields = extfields, fieldext = fieldext }: record_data;

structure Records_Data = Theory_Data
(
  type T = record_data;
  val empty =
    make_record_data Symtab.empty
      {selectors = Symtab.empty, updates = Symtab.empty,
          simpset = HOL_basic_ss, defset = HOL_basic_ss,
          foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
       Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
  val extend = I;
  fun merge
   ({records = recs1,
     sel_upd =
      {selectors = sels1, updates = upds1,
       simpset = ss1, defset = ds1,
       foldcong = fc1, unfoldcong = uc1},
     equalities = equalities1,
     extinjects = extinjects1,
     extsplit = extsplit1,
     splits = splits1,
     extfields = extfields1,
     fieldext = fieldext1},
    {records = recs2,
     sel_upd =
      {selectors = sels2, updates = upds2,
       simpset = ss2, defset = ds2,
       foldcong = fc2, unfoldcong = uc2},
     equalities = equalities2,
     extinjects = extinjects2,
     extsplit = extsplit2,
     splits = splits2,
     extfields = extfields2,
     fieldext = fieldext2}) =
    make_record_data
      (Symtab.merge (K true) (recs1, recs2))
      {selectors = Symtab.merge (K true) (sels1, sels2),
        updates = Symtab.merge (K true) (upds1, upds2),
        simpset = Simplifier.merge_ss (ss1, ss2),
        defset = Simplifier.merge_ss (ds1, ds2),
        foldcong = Simplifier.merge_ss (fc1, fc2),
        unfoldcong = Simplifier.merge_ss (uc1, uc2)}
      (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
      (Thm.merge_thms (extinjects1, extinjects2))
      (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
      (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
          Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
          Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
      (Symtab.merge (K true) (extfields1, extfields2))
      (Symtab.merge (K true) (fieldext1, fieldext2));
);

fun print_records thy =
  let
    val {records = recs, ...} = Records_Data.get thy;
    val prt_typ = Syntax.pretty_typ_global thy;

    fun pretty_parent NONE = []
      | pretty_parent (SOME (Ts, name)) =
          [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];

    fun pretty_field (c, T) = Pretty.block
      [Pretty.str (Sign.extern_const thy c), Pretty.str " ::",
        Pretty.brk 1, Pretty.quote (prt_typ T)];

    fun pretty_record (name, {args, parent, fields, ...}: record_info) =
      Pretty.block (Pretty.fbreaks (Pretty.block
        [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
        pretty_parent parent @ map pretty_field fields));
  in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;


(* access 'records' *)

val get_record = Symtab.lookup o #records o Records_Data.get;

fun the_record thy name =
  (case get_record thy name of
    SOME info => info
  | NONE => error ("Unknown record type " ^ quote name));

fun put_record name info thy =
  let
    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
      Records_Data.get thy;
    val data = make_record_data (Symtab.update (name, info) records)
      sel_upd equalities extinjects extsplit splits extfields fieldext;
  in Records_Data.put data thy end;


(* access 'sel_upd' *)

val get_sel_upd = #sel_upd o Records_Data.get;

val is_selector = Symtab.defined o #selectors o get_sel_upd;
val get_updates = Symtab.lookup o #updates o get_sel_upd;
fun get_ss_with_context getss thy = Simplifier.global_context thy (getss (get_sel_upd thy));

val get_simpset = get_ss_with_context #simpset;
val get_sel_upd_defs = get_ss_with_context #defset;

fun get_update_details u thy =
  let val sel_upd = get_sel_upd thy in
    (case Symtab.lookup (#updates sel_upd) u of
      SOME s =>
        let val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s
        in SOME (s, dep, ismore) end
    | NONE => NONE)
  end;

fun put_sel_upd names more depth simps defs (folds, unfolds) thy =
  let
    val all = names @ [more];
    val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
    val upds = map (suffix updateN) all ~~ all;

    val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
      equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy;
    val data = make_record_data records
      {selectors = fold Symtab.update_new sels selectors,
        updates = fold Symtab.update_new upds updates,
        simpset = Simplifier.addsimps (simpset, simps),
        defset = Simplifier.addsimps (defset, defs),
        foldcong = foldcong addcongs folds,
        unfoldcong = unfoldcong addcongs unfolds}
       equalities extinjects extsplit splits extfields fieldext;
  in Records_Data.put data thy end;


(* access 'equalities' *)

fun add_record_equalities name thm thy =
  let
    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
      Records_Data.get thy;
    val data = make_record_data records sel_upd
      (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext;
  in Records_Data.put data thy end;

val get_equalities = Symtab.lookup o #equalities o Records_Data.get;


(* access 'extinjects' *)

fun add_extinjects thm thy =
  let
    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
      Records_Data.get thy;
    val data =
      make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
        extsplit splits extfields fieldext;
  in Records_Data.put data thy end;

val get_extinjects = rev o #extinjects o Records_Data.get;


(* access 'extsplit' *)

fun add_extsplit name thm thy =
  let
    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
      Records_Data.get thy;
    val data =
      make_record_data records sel_upd equalities extinjects
        (Symtab.update_new (name, thm) extsplit) splits extfields fieldext;
  in Records_Data.put data thy end;


(* access 'splits' *)

fun add_record_splits name thmP thy =
  let
    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
      Records_Data.get thy;
    val data =
      make_record_data records sel_upd equalities extinjects extsplit
        (Symtab.update_new (name, thmP) splits) extfields fieldext;
  in Records_Data.put data thy end;

val get_splits = Symtab.lookup o #splits o Records_Data.get;


(* parent/extension of named record *)

val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Records_Data.get);
val get_extension = Option.map #extension oo (Symtab.lookup o #records o Records_Data.get);


(* access 'extfields' *)

fun add_extfields name fields thy =
  let
    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
      Records_Data.get thy;
    val data =
      make_record_data records sel_upd equalities extinjects extsplit splits
        (Symtab.update_new (name, fields) extfields) fieldext;
  in Records_Data.put data thy end;

val get_extfields = Symtab.lookup o #extfields o Records_Data.get;

fun get_extT_fields thy T =
  let
    val ((name, Ts), moreT) = dest_recT T;
    val recname =
      let val (nm :: _ :: rst) = rev (Long_Name.explode name)   (* FIXME !? *)
      in Long_Name.implode (rev (nm :: rst)) end;
    val midx = maxidx_of_typs (moreT :: Ts);
    val varifyT = varifyT midx;
    val {records, extfields, ...} = Records_Data.get thy;
    val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
    val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));

    val subst = fold (Sign.typ_match thy) (but_last args ~~ but_last Ts) Vartab.empty;
    val fields' = map (apsnd (Envir.norm_type subst o varifyT)) fields;
  in (fields', (more, moreT)) end;

fun get_recT_fields thy T =
  let
    val (root_fields, (root_more, root_moreT)) = get_extT_fields thy T;
    val (rest_fields, rest_more) =
      if is_recT root_moreT then get_recT_fields thy root_moreT
      else ([], (root_more, root_moreT));
  in (root_fields @ rest_fields, rest_more) end;


(* access 'fieldext' *)

fun add_fieldext extname_types fields thy =
  let
    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
      Records_Data.get thy;
    val fieldext' =
      fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
    val data =
      make_record_data records sel_upd equalities extinjects
        extsplit splits extfields fieldext';
  in Records_Data.put data thy end;

val get_fieldext = Symtab.lookup o #fieldext o Records_Data.get;


(* parent records *)

fun add_parents _ NONE parents = parents
  | add_parents thy (SOME (types, name)) parents =
      let
        fun err msg = error (msg ^ " parent record " ^ quote name);

        val {args, parent, fields, extension, induct_scheme, ext_def, ...} =
          (case get_record thy name of SOME info => info | NONE => err "Unknown");
        val _ = if length types <> length args then err "Bad number of arguments for" else ();

        fun bad_inst ((x, S), T) =
          if Sign.of_sort thy (T, S) then NONE else SOME x
        val bads = map_filter bad_inst (args ~~ types);
        val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");

        val inst = map fst args ~~ types;
        val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
        val parent' = Option.map (apfst (map subst)) parent;
        val fields' = map (apsnd subst) fields;
        val extension' = apsnd (map subst) extension;
      in
        add_parents thy parent'
          (make_parent_info name fields' extension' ext_def induct_scheme :: parents)
      end;



(** concrete syntax for records **)

(* decode type *)

fun decode_type thy t =
  let
    fun get_sort env xi =
      the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname));
  in
    Syntax.typ_of_term (get_sort (Syntax.term_sorts t)) t
  end;


(* parse translations *)

local

fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
      (name, arg)
  | field_type_tr t = raise TERM ("field_type_tr", [t]);

fun field_types_tr (Const (@{syntax_const "_field_types"}, _) $ t $ u) =
      field_type_tr t :: field_types_tr u
  | field_types_tr t = [field_type_tr t];

fun record_field_types_tr more ctxt t =
  let
    val thy = ProofContext.theory_of ctxt;
    fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);

    fun split_args (field :: fields) ((name, arg) :: fargs) =
          if can (unsuffix name) field then
            let val (args, rest) = split_args fields fargs
            in (arg :: args, rest) end
          else err ("expecting field " ^ field ^ " but got " ^ name)
      | split_args [] (fargs as (_ :: _)) = ([], fargs)
      | split_args (_ :: _) [] = err "expecting more fields"
      | split_args _ _ = ([], []);

    fun mk_ext (fargs as (name, _) :: _) =
          (case get_fieldext thy (Sign.intern_const thy name) of
            SOME (ext, alphas) =>
              (case get_extfields thy ext of
                SOME fields =>
                  let
                    val fields' = but_last fields;
                    val types = map snd fields';
                    val (args, rest) = split_args (map fst fields') fargs;
                    val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
                    val midx = fold Term.maxidx_typ argtypes 0;
                    val varifyT = varifyT midx;
                    val vartypes = map varifyT types;

                    val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
                      handle Type.TYPE_MATCH => err "type is no proper record (extension)";
                    val alphas' =
                      map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT)
                        (but_last alphas);

                    val more' = mk_ext rest;
                  in
                    list_comb
                      (Syntax.const (Syntax.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
                  end
              | NONE => err ("no fields defined for " ^ ext))
          | NONE => err (name ^ " is no proper field"))
      | mk_ext [] = more;
  in
    mk_ext (field_types_tr t)
  end;

fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const @{type_syntax unit}) ctxt t
  | record_type_tr _ ts = raise TERM ("record_type_tr", ts);

fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t
  | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts);


fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg)
  | field_tr t = raise TERM ("field_tr", [t]);

fun fields_tr (Const (@{syntax_const "_fields"}, _) $ t $ u) = field_tr t :: fields_tr u
  | fields_tr t = [field_tr t];

fun record_fields_tr more ctxt t =
  let
    val thy = ProofContext.theory_of ctxt;
    fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);

    fun split_args (field :: fields) ((name, arg) :: fargs) =
          if can (unsuffix name) field
          then
            let val (args, rest) = split_args fields fargs
            in (arg :: args, rest) end
          else err ("expecting field " ^ field ^ " but got " ^ name)
      | split_args [] (fargs as (_ :: _)) = ([], fargs)
      | split_args (_ :: _) [] = err "expecting more fields"
      | split_args _ _ = ([], []);

    fun mk_ext (fargs as (name, _) :: _) =
          (case get_fieldext thy (Sign.intern_const thy name) of
            SOME (ext, _) =>
              (case get_extfields thy ext of
                SOME fields =>
                  let
                    val (args, rest) = split_args (map fst (but_last fields)) fargs;
                    val more' = mk_ext rest;
                  in list_comb (Syntax.const (Syntax.mark_const (ext ^ extN)), args @ [more']) end
              | NONE => err ("no fields defined for " ^ ext))
          | NONE => err (name ^ " is no proper field"))
      | mk_ext [] = more;
  in mk_ext (fields_tr t) end;

fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t
  | record_tr _ ts = raise TERM ("record_tr", ts);

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


fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
      Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg)
  | field_update_tr t = raise TERM ("field_update_tr", [t]);

fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
      field_update_tr t :: field_updates_tr u
  | field_updates_tr t = [field_update_tr t];

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

in

val parse_translation =
 [(@{syntax_const "_record_update"}, record_update_tr)];

val advanced_parse_translation =
 [(@{syntax_const "_record"}, record_tr),
  (@{syntax_const "_record_scheme"}, record_scheme_tr),
  (@{syntax_const "_record_type"}, record_type_tr),
  (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];

end;


(* print translations *)

val print_record_type_abbr = Unsynchronized.ref true;
val print_record_type_as_fields = Unsynchronized.ref true;


local

(* FIXME early extern (!??) *)
(* FIXME Syntax.free (??) *)
fun field_type_tr' (c, t) = Syntax.const @{syntax_const "_field_type"} $ Syntax.const c $ t;

fun field_types_tr' (t, u) = Syntax.const @{syntax_const "_field_types"} $ t $ u;

fun record_type_tr' ctxt t =
  let
    val thy = ProofContext.theory_of ctxt;

    val T = decode_type thy t;
    val varifyT = varifyT (Term.maxidx_of_typ T);

    val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts);

    fun strip_fields T =
      (case T of
        Type (ext, args as _ :: _) =>
          (case try (unsuffix ext_typeN) ext of
            SOME ext' =>
              (case get_extfields thy ext' of
                SOME (fields as (x, _) :: _) =>
                  (case get_fieldext thy x of
                    SOME (_, alphas) =>
                     (let
                        val f :: fs = but_last fields;
                        val fields' =
                          apfst (Sign.extern_const thy) f :: map (apfst Long_Name.base_name) fs;
                        val (args', more) = split_last args;
                        val alphavars = map varifyT (but_last alphas);
                        val subst = Type.raw_matches (alphavars, args') Vartab.empty;
                        val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
                      in fields'' @ strip_fields more end
                      handle Type.TYPE_MATCH => [("", T)])
                  | _ => [("", T)])
              | _ => [("", T)])
          | _ => [("", T)])
      | _ => [("", T)]);

    val (fields, (_, moreT)) = split_last (strip_fields T);
    val _ = null fields andalso raise Match;
    val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields);
  in
    if not (! print_record_type_as_fields) orelse null fields then raise Match
    else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
    else Syntax.const @{syntax_const "_record_type_scheme"} $ u $ term_of_type moreT
  end;

(*try to reconstruct the record name type abbreviation from
  the (nested) extension types*)
fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
  let
    val thy = ProofContext.theory_of ctxt;
    val T = decode_type thy tm;
    val midx = maxidx_of_typ T;
    val varifyT = varifyT midx;

    fun mk_type_abbr subst name args =
      let val abbrT = Type (name, map (varifyT o TFree) args)
      in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;

    fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
  in
    if ! print_record_type_abbr then
      (case last_extT T of
        SOME (name, _) =>
          if name = last_ext then
            let val subst = match schemeT T in
              if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta)))
              then mk_type_abbr subst abbr alphas
              else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
            end handle Type.TYPE_MATCH => record_type_tr' ctxt tm
          else raise Match (*give print translation of specialised record a chance*)
      | _ => raise Match)
    else record_type_tr' ctxt tm
  end;

in

fun record_ext_type_tr' name =
  let
    val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
    fun tr' ctxt ts =
      record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
  in (ext_type_name, tr') end;

{'fraction_non_alphanumeric': 0.11009048323847598, 'fraction_numerical': 0.0018920609731907167, 'mean_word_length': 3.0826013829190804, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 252, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '203145', 'n_tokens_mistral': 23609, 'n_tokens_neox': 22924, 'n_words': 6813}