(*  Title:      HOL/Tools/record.ML

    Author:     Wolfgang Naraschewski, TU Muenchen

    Author:     Markus Wenzel, TU Muenchen

    Author:     Norbert Schirmer, TU Muenchen

    Author:     Thomas Sewell, NICTA

Extensible records with structural subtyping.

*)

signature RECORD =

sig

  val type_abbr: bool Config.T

  val type_as_fields: bool Config.T

  val timing: bool Config.T

  type 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_info: theory -> string -> info option

  val the_info: theory -> string -> info

  val get_hierarchy: theory -> (string * typ list) -> (string * ((string * sort) * typ) list) list

  val add_record: (string * sort) list * binding -> (typ list * string) option ->

    (binding * typ * mixfix) list -> theory -> theory

  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 simproc: simproc

  val eq_simproc: simproc

  val upd_simproc: simproc

  val split_simproc: (term -> int) -> simproc

  val ex_sel_eq_simproc: simproc

  val split_tac: int -> tactic

  val split_simp_tac: thm list -> (term -> int) -> int -> tactic

  val split_wrapper: string * (Proof.context -> wrapper)

  val updateN: string

  val ext_typeN: string

  val extN: string

  val setup: theory -> theory

end;

signature ISO_TUPLE_SUPPORT =

sig

  val add_iso_tuple_type: binding * (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 Record.tuple_iso_tuple}, @{thm tuple_iso_tuple});

fun named_cterm_instantiate values thm =  (* FIXME eliminate *)

  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 get_typedef_info tyco vs

    (({rep_type, Abs_name, ...}, {Rep_inject, Abs_inverse, ... }) : Typedef.info) thy =

  let

    val exists_thm =

      UNIV_I

      |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];

    val proj_constr = Abs_inverse OF [exists_thm];

    val absT = Type (tyco, map TFree vs);

  in

    thy

    |> pair (tyco, ((Rep_inject, proj_constr), Const (Abs_name, rep_type --> absT), absT))

  end

fun do_typedef raw_tyco repT raw_vs thy =

  let

    val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT;

    val vs = map (Proof_Context.check_tfree ctxt) raw_vs;

  in

    thy

    |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)

        (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1)

    |-> (fn (tyco, info) => get_typedef_info tyco vs info)

  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 Record.iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $

      Const (fst tuple_iso_tuple, isomT) $ left $ right

  end;

fun dest_cons_tuple (Const (@{const_name Record.iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)

  | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);

fun add_iso_tuple_type (b, alphas) (leftT, rightT) thy =

  let

    val repT = HOLogic.mk_prodT (leftT, rightT);

    val ((_, ((rep_inject, abs_inverse), absC, absT)), typ_thy) =

      thy

      |> do_typedef b repT alphas

      ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)

    (*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.suffix_name isoN b;

    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_global ((isom_binding, isomT), NoSyn) |> snd

      |> Global_Theory.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 Record.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

  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 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};

(** name components **)

val rN = "r";

val wN = "w";

val moreN = "more";

val schemeN = "_scheme";

val ext_typeN = "_ext";

val inner_typeN = "_inner";

val extN ="_ext";

val updateN = "_update";

val makeN = "make";

val fields_selN = "fields";

val extendN = "extend";

val truncateN = "truncate";

(*** utilities ***)

fun varifyT idx = map_type_tfree (fn (a, S) => TVar ((a, idx), S));

(* timing *)

val timing = Attrib.setup_config_bool @{binding record_timing} (K false);

fun timeit_msg ctxt s x = if Config.get ctxt timing then (warning s; timeit x) else x ();

fun timing_msg ctxt s = if Config.get ctxt timing then warning s else ();

(* syntax *)

val Trueprop = HOLogic.mk_Trueprop;

infix 0 :== ===;

infixr 0 ==>;

val op :== = Misc_Legacy.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 info and parent_info *)

type 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,  (* FIXME unused!? *)

  unfold_congs: thm list,  (* FIXME unused!? *)

  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_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 : 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 data =

 {records: info Symtab.table,

  sel_upd:

   {selectors: (int * bool) Symtab.table,

    updates: string Symtab.table,

    simpset: simpset,

    defset: 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_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 }: data;

structure Data = Theory_Data

(

  type T = data;

  val empty =

    make_data Symtab.empty

      {selectors = Symtab.empty, updates = Symtab.empty,

        simpset = HOL_basic_ss, defset = 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},

     equalities = equalities1,

     extinjects = extinjects1,

     extsplit = extsplit1,

     splits = splits1,

     extfields = extfields1,

     fieldext = fieldext1},

    {records = recs2,

     sel_upd = {selectors = sels2, updates = upds2, simpset = ss2, defset = ds2},

     equalities = equalities2,

     extinjects = extinjects2,

     extsplit = extsplit2,

     splits = splits2,

     extfields = extfields2,

     fieldext = fieldext2}) =

    make_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)}

      (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));

);

(* access 'records' *)

val get_info = Symtab.lookup o #records o Data.get;

fun the_info thy name =

  (case get_info thy name of

    SOME info => info

  | NONE => error ("Unknown record type " ^ quote name));

fun put_record name info =

  Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>

    make_data (Symtab.update (name, info) records)

      sel_upd equalities extinjects extsplit splits extfields fieldext);

(* access 'sel_upd' *)

val get_sel_upd = #sel_upd o 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 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},

      equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy;

    val data =

      make_data records

        {selectors = fold Symtab.update_new sels selectors,

          updates = fold Symtab.update_new upds updates,

          simpset = simpset addsimps simps,

          defset = defset addsimps defs}

         equalities extinjects extsplit splits extfields fieldext;

  in Data.put data thy end;

(* access 'equalities' *)

fun add_equalities name thm =

  Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>

    make_data records sel_upd

      (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext);

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

(* access 'extinjects' *)

fun add_extinjects thm =

  Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>

    make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)

      extsplit splits extfields fieldext);

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

(* access 'extsplit' *)

fun add_extsplit name thm =

  Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>

    make_data records sel_upd equalities extinjects

      (Symtab.update_new (name, thm) extsplit) splits extfields fieldext);

(* access 'splits' *)

fun add_splits name thmP =

  Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>

    make_data records sel_upd equalities extinjects extsplit

      (Symtab.update_new (name, thmP) splits) extfields fieldext);

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

(* parent/extension of named record *)

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

val get_extension = Option.map #extension oo (Symtab.lookup o #records o Data.get);

(* access 'extfields' *)

fun add_extfields name fields =

  Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>

    make_data records sel_upd equalities extinjects extsplit splits

      (Symtab.update_new (name, fields) extfields) fieldext);

val get_extfields = Symtab.lookup o #extfields o 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 varifyT = varifyT (maxidx_of_typs (moreT :: Ts) + 1);

    val {records, extfields, ...} = 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) (#1 (split_last args) ~~ #1 (split_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 =

  Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>

    let

      val fieldext' =

        fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;

    in make_data records sel_upd equalities extinjects extsplit splits extfields fieldext' end);

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

(* parent records *)

local

fun add_parents _ NONE = I

  | add_parents thy (SOME (types, name)) =

      let

        fun err msg = error (msg ^ " parent record " ^ quote name);

        val {args, parent, ...} =

          (case get_info 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 = args ~~ types;

        val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);

        val parent' = Option.map (apfst (map subst)) parent;

      in cons (name, inst) #> add_parents thy parent' end;

in

fun get_hierarchy thy (name, types) = add_parents thy (SOME (types, name)) [];

fun get_parent_info thy parent =

  add_parents thy parent [] |> map (fn (name, inst) =>

    let

      val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);

      val {fields, extension, induct_scheme, ext_def, ...} = the_info thy name;

      val fields' = map (apsnd subst) fields;

      val extension' = apsnd (map subst) extension;

    in make_parent_info name fields' extension' ext_def induct_scheme end);

end;

(** concrete syntax for records **)

(* parse translations *)

local

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 raise Fail ("expecting field " ^ quote field ^ " but got " ^ quote name)

  | split_args [] (fargs as (_ :: _)) = ([], fargs)

  | split_args (_ :: _) [] = raise Fail "expecting more fields"

  | split_args _ _ = ([], []);

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 = Proof_Context.theory_of ctxt;

    fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);

    fun mk_ext (fargs as (name, _) :: _) =

          (case get_fieldext thy (Proof_Context.intern_const ctxt name) of

            SOME (ext, alphas) =>

              (case get_extfields thy ext of

                SOME fields =>

                  let

                    val (fields', _) = split_last fields;

                    val types = map snd fields';

                    val (args, rest) = split_args (map fst fields') fargs

                      handle Fail msg => err msg;

                    val argtypes = Syntax.check_typs ctxt (map Syntax_Phases.decode_typ args);

                    val varifyT = varifyT (fold Term.maxidx_typ argtypes ~1 + 1);

                    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_Phases.term_of_typ ctxt o Envir.norm_type subst o varifyT)

                        (#1 (split_last alphas));

                    val more' = mk_ext rest;

                  in

                    list_comb

                      (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more'])

                  end

              | NONE => err ("no fields defined for " ^ quote ext))

          | NONE => err (quote 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 = Proof_Context.theory_of ctxt;

    fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);

    fun mk_ext (fargs as (name, _) :: _) =

          (case get_fieldext thy (Proof_Context.intern_const ctxt name) of

            SOME (ext, _) =>

              (case get_extfields thy ext of

                SOME fields =>

                  let

                    val (args, rest) = split_args (map fst (fst (split_last fields))) fargs

                      handle Fail msg => err msg;

                    val more' = mk_ext rest;

                  in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end

              | NONE => err ("no fields defined for " ^ quote ext))

          | NONE => err (quote 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 (Name.uu_, 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 type_abbr = Attrib.setup_config_bool @{binding record_type_abbr} (K true);

val type_as_fields = Attrib.setup_config_bool @{binding record_type_as_fields} (K 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 = Proof_Context.theory_of ctxt;

    val T = Syntax_Phases.decode_typ t;

    val varifyT = varifyT (Term.maxidx_of_typ T + 1);

    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, _) = split_last fields;

                        val fields' =

                          apfst (Proof_Context.extern_const ctxt) f ::

                            map (apfst Long_Name.base_name) fs;

                        val (args', more) = split_last args;

                        val alphavars = map varifyT (#1 (split_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 (Syntax_Phases.term_of_typ ctxt)) fields);

  in

    if not (Config.get ctxt 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 $

        Syntax_Phases.term_of_typ ctxt 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 T = Syntax_Phases.decode_typ tm;

    val varifyT = varifyT (maxidx_of_typ T + 1);

    fun mk_type_abbr subst name args =

      let val abbrT = Type (name, map (varifyT o TFree) args)

      in Syntax_Phases.term_of_typ ctxt (Envir.norm_type subst abbrT) end;

    fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;

  in

    if Config.get ctxt 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 = Lexicon.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;

fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =

  let

    val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);

    fun tr' ctxt ts =

      record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt

        (list_comb (Syntax.const ext_type_name, ts));

  in (ext_type_name, tr') end;

end;

local

(* FIXME Syntax.free (??) *)

fun field_tr' (c, t) = Syntax.const @{syntax_const "_field"} $ Syntax.const c $ t;

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

fun record_tr' ctxt t =

  let

    val thy = Proof_Context.theory_of ctxt;

    fun strip_fields t =

      (case strip_comb t of

        (Const (ext, _), args as (_ :: _)) =>

          (case try (Lexicon.unmark_const o unsuffix extN) ext of

            SOME ext' =>

              (case get_extfields thy ext' of

                SOME fields =>

                 (let

                    val (f :: fs, _) = split_last (map fst fields);

                    val fields' = Proof_Context.extern_const ctxt f :: map Long_Name.base_name fs;

                    val (args', more) = split_last args;

                  in (fields' ~~ args') @ strip_fields more end

                  handle ListPair.UnequalLengths => [("", t)])

              | NONE => [("", t)])

          | NONE => [("", t)])

       | _ => [("", t)]);

    val (fields, (_, more)) = split_last (strip_fields t);

    val _ = null fields andalso raise Match;

    val u = foldr1 fields_tr' (map field_tr' fields);

  in

    (case more of

      Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u

    | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more)

  end;

in

fun record_ext_tr' name =

  let

    val ext_name = Lexicon.mark_const (name ^ extN);

    fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));

  in (ext_name, tr') end;

end;

local

fun dest_update ctxt c =

  (case try Lexicon.unmark_const c of

    SOME d => try (unsuffix updateN) (Proof_Context.extern_const ctxt d)

  | NONE => NONE);

fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =

      (case dest_update ctxt c of

        SOME name =>

          (case try Syntax_Trans.const_abs_tr' k of

            SOME t =>

              apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))

                (field_updates_tr' ctxt u)

          | NONE => ([], tm))

      | NONE => ([], tm))

  | field_updates_tr' _ tm = ([], tm);

fun record_update_tr' ctxt tm =

  (case field_updates_tr' ctxt tm of

    ([], _) => raise Match

  | (ts, u) =>

      Syntax.const @{syntax_const "_record_update"} $ u $

        foldr1 (fn (v, w) => Syntax.const @{syntax_const "_field_updates"} $ v $ w) (rev ts));

in

fun field_update_tr' name =

  let

    val update_name = Lexicon.mark_const (name ^ updateN);

    fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)

      | tr' _ _ = raise Match;

  in (update_name, tr') end;

end;

(** record simprocs **)

fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =

  (case get_updates thy u of

    SOME u_name => u_name = s

  | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));

fun mk_comp_id f =

  let val T = range_type (fastype_of f)

  in HOLogic.mk_comp (Const (@{const_name Fun.id}, T --> T), f) end;

fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t

  | get_upd_funs _ = [];

fun get_accupd_simps thy term defset =

  let

    val (acc, [body]) = strip_comb term;

    val upd_funs = sort_distinct Term_Ord.fast_term_ord (get_upd_funs body);

    fun get_simp upd =

      let

        (* FIXME fresh "f" (!?) *)

        val T = domain_type (fastype_of upd);

        val lhs = HOLogic.mk_comp (acc, upd $ Free ("f", T));

        val rhs =

          if is_sel_upd_pair thy acc upd

          then HOLogic.mk_comp (Free ("f", T), acc)

          else mk_comp_id acc;

        val prop = lhs === rhs;

        val othm =

          Goal.prove (Proof_Context.init_global thy) [] [] prop

            (fn _ =>

              simp_tac defset 1 THEN

              REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN

              TRY (simp_tac (HOL_ss addsimps @{thms id_apply id_o o_id}) 1));

        val dest =

          if is_sel_upd_pair thy acc upd

          then @{thm o_eq_dest}

          else @{thm o_eq_id_dest};

      in Drule.export_without_context (othm RS dest) end;

  in map get_simp upd_funs end;

fun get_updupd_simp thy defset u u' comp =

  let

    (* FIXME fresh "f" (!?) *)

    val f = Free ("f", domain_type (fastype_of u));

    val f' = Free ("f'", domain_type (fastype_of u'));

    val lhs = HOLogic.mk_comp (u $ f, u' $ f');

    val rhs =

      if comp

      then u $ HOLogic.mk_comp (f, f')

      else HOLogic.mk_comp (u' $ f', u $ f);

    val prop = lhs === rhs;

    val othm =

      Goal.prove (Proof_Context.init_global thy) [] [] prop

        (fn _ =>

          simp_tac defset 1 THEN

          REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN