Theory Meta_Toy

(******************************************************************************
 * HOL-TOY
 *
 * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France
 *               2013-2017 IRT SystemX, France
 *               2011-2015 Achim D. Brucker, Germany
 *               2016-2018 The University of Sheffield, UK
 *               2016-2017 Nanyang Technological University, Singapore
 *               2017-2018 Virginia Tech, USA
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

section‹Toy Meta-Model aka. AST definition of Toy (I)›

theory  Meta_Toy
imports "../../../meta_isabelle/Meta_Pure"
        "../Init_rbt"
begin

subsection‹Type Definition›

datatype toy_collection = Set
                        | Sequence
                        | Ordered0 ― ‹ordered set›
                        | Subsets0 ― ‹binding›
                        | Union0
                        | Redefines0 ― ‹binding›
                        | Derived0 ― ‹string›
                        | Qualifier0 ― ‹binding × use_toyty›
                        | Nonunique0 ― ‹bag›

datatype toy_multiplicity_single = Mult_nat nat
                                 | Mult_star
                                 | Mult_infinity

record toy_multiplicity = TyMult :: "(toy_multiplicity_single × toy_multiplicity_single option) list"
                          TyRole :: "string option"
                          TyCollect :: "toy_collection list" ― ‹return type of the accessor (constrained by the above multiplicity)›

record toy_ty_class_node =  TyObjN_ass_switch :: nat
                            TyObjN_role_multip :: toy_multiplicity
                            TyObjN_role_ty :: string
record toy_ty_class =       TyObj_name :: string
                            TyObj_ass_id :: nat
                            TyObj_ass_arity :: nat
                            TyObj_from :: toy_ty_class_node
                            TyObj_to :: toy_ty_class_node
datatype toy_ty_obj_core =  ToyTyCore_pre string ― ‹class name, untyped› (* FIXME perform the typing separately *)
                          | ToyTyCore toy_ty_class ― ‹class name, typed›
datatype toy_ty_obj =       ToyTyObj  toy_ty_obj_core
                                     "toy_ty_obj_core list ― ‹the and semantics›
                                                           list ― ‹x # …› means x < …›" ― ‹superclass›
datatype toy_ty =           ToyTy_base_void (* NOTE can be merged in a generic tuple *)
                          | ToyTy_base_boolean
                          | ToyTy_base_integer
                          | ToyTy_base_unlimitednatural
                          | ToyTy_base_real
                          | ToyTy_base_string
                          | ToyTy_object toy_ty_obj
                          | ToyTy_collection toy_multiplicity toy_ty
                          | ToyTy_pair toy_ty toy_ty (* NOTE can be merged in a generic tuple *)
                          | ToyTy_binding "string option ― ‹name› × toy_ty" (* NOTE can be merged in a generic tuple *)
                          | ToyTy_arrow toy_ty toy_ty
                          | ToyTy_class_syn string
                          | ToyTy_enum string
                          | ToyTy_raw string ― ‹denoting raw HOL-type› (* FIXME to be removed *)


datatype toy_association_type = ToyAssTy_native_attribute
                              | ToyAssTy_association
                              | ToyAssTy_composition
                              | ToyAssTy_aggregation
datatype toy_association_relation = ToyAssRel "(toy_ty_obj × toy_multiplicity) list"
record toy_association =        ToyAss_type     :: toy_association_type
                                ToyAss_relation :: toy_association_relation

datatype toy_ctxt_prefix = ToyCtxtPre | ToyCtxtPost

datatype toy_ctxt_term = T_pure "term"
                       | T_to_be_parsed string ― ‹raw, it includes extra quoting characters like DEL (char 127)›
                                        string ― ‹same string but escaped without those quoting characters›
                       | T_lambda string toy_ctxt_term
datatype toy_prop = ToyProp_ctxt "string option" ― ‹name› toy_ctxt_term
                  (*| ToyProp_rel toy_ty_obj (* states that the constraint should be true *)
                  | ToyProp_ass toy_association_relation (* states the relation as true *)*)
datatype toy_ctxt_term_inv = T_inv bool ― ‹True: existential› toy_prop
datatype toy_ctxt_term_pp = T_pp toy_ctxt_prefix toy_prop
                          | T_invariant toy_ctxt_term_inv

record toy_ctxt_pre_post = Ctxt_fun_name :: string ― ‹function name›
                           Ctxt_fun_ty :: toy_ty
                           Ctxt_expr :: "toy_ctxt_term_pp list"

datatype toy_ctxt_clause = Ctxt_pp toy_ctxt_pre_post
                         | Ctxt_inv toy_ctxt_term_inv
record toy_ctxt = Ctxt_param :: "string list" ― ‹param›
                  Ctxt_ty :: toy_ty_obj
                  Ctxt_clause :: "toy_ctxt_clause list"

datatype toy_class =   ToyClass
                         string ― ‹name of the class›
                         "(string ― ‹name› × toy_ty) list" ― ‹attribute›
                         "toy_class list" ― ‹link to subclasses›

record toy_class_raw = ClassRaw_name :: toy_ty_obj
                       ClassRaw_own :: "(string ― ‹name› × toy_ty) list" ― ‹attribute›
                       ClassRaw_clause :: "toy_ctxt_clause list"
                       ClassRaw_abstract :: bool ― ‹True: abstract›

datatype toy_ass_class = ToyAssClass toy_association
                                     toy_class_raw

datatype toy_class_synonym = ToyClassSynonym string ― ‹name alias› toy_ty

datatype toy_enum = ToyEnum string ― ‹name› "string ― ‹constructor name› list"

subsection‹Extending the Meta-Model›

definition "T_lambdas = List.fold T_lambda"
definition "TyObjN_role_name = TyRole o TyObjN_role_multip"
definition "ToyTy_class c = ToyTy_object (ToyTyObj (ToyTyCore c) [])"
definition "ToyTy_class_pre c = ToyTy_object (ToyTyObj (ToyTyCore_pre c) [])"
definition "ToyAss_relation' l = (case ToyAss_relation l of ToyAssRel l  l)"

fun fold_pair_var where
   "fold_pair_var f t accu = (case t of
    ToyTy_pair t1 t2  Option.bind (fold_pair_var f t1 accu) (fold_pair_var f t2)
  | ToyTy_binding (Some v, t)  fold_pair_var f t (f (v, t) accu)
  | ToyTy_binding (None, t)  fold_pair_var f t accu
  | ToyTy_collection _ t  fold_pair_var f t accu
  | ToyTy_arrow _ _  None
  | _  Some accu)"

definition "Ctxt_fun_ty_arg ctxt =
 (case 
    fold_pair_var
      Cons
      (case Ctxt_fun_ty ctxt of ToyTy_arrow t _  t
                              | t  t)
      []
  of Some l  rev l)"

definition "Ctxt_fun_ty_out ctxt =
 (case Ctxt_fun_ty ctxt of ToyTy_arrow _ t  Some t
                         | _  None)"

definition "map_pre_post f = 
             Ctxt_clause_update
               (L.map 
                  (λ Ctxt_pp ctxt 
                     Ctxt_pp (Ctxt_expr_update
                               (L.map
                                  (λ T_pp pref (ToyProp_ctxt n e) 
                                     T_pp pref (ToyProp_ctxt n (f pref ctxt e))
                                   | x  x))
                               ctxt)
                   | x  x))"

definition "map_invariant f_inv =
             Ctxt_clause_update
               (L.map 
                  (λ Ctxt_pp ctxt 
                     Ctxt_pp (Ctxt_expr_update
                               (L.map
                                 (λ T_invariant ctxt  T_invariant (f_inv ctxt)
                                  | x  x))
                               ctxt)
                   | Ctxt_inv ctxt  Ctxt_inv (f_inv ctxt)))"

fun remove_binding where
   "remove_binding e = (λ ToyTy_collection m ty  ToyTy_collection m (remove_binding ty)
                        | ToyTy_pair ty1 ty2  ToyTy_pair (remove_binding ty1) (remove_binding ty2)
                        | ToyTy_binding (_, ty)  remove_binding ty
                        | ToyTy_arrow ty1 ty2  ToyTy_arrow (remove_binding ty1) (remove_binding ty2)
                        | x  x) e"

subsection‹Class Translation Preliminaries›

definition "const_oid = ‹oid›"
definition "var_ty_list = ‹list›"
definition "var_ty_prod = ‹prod›"
definition "const_toyany = ‹ToyAny›"

definition "single_multip = 
  List.list_all (λ (_, Some (Mult_nat n))  n  1
                 | (Mult_nat n, None)  n  1
                 | _  False) o TyMult"

fun fold_max_aux where
   "fold_max_aux f l l_acc accu = (case l of
      []  accu
    | x # xs  fold_max_aux f xs (x # l_acc) (f x (L.flatten [rev l_acc, xs]) accu))"

definition "fold_max f l = fold_max_aux f (L.mapi Pair l) []"

locale RBTS
begin
definition "lookup m k = RBT.lookup m (String.to_list k)"
definition insert where "insert k = RBT.insert (String.to_list k)"
definition "map_entry k = RBT.map_entry (String.to_list k)"
definition "modify_def v k = RBT.modify_def v (String.to_list k)"
definition "keys m = L.map (λs. s) (RBT.keys m)"
definition "lookup2 m = (λ(k1, k2). RBT.lookup2 m (String.to_list k1, String.to_list k2))"
definition "insert2 = (λ(k1, k2). RBT.insert2 (String.to_list k1, String.to_list k2))"
definition fold where "fold f = RBT.fold (λc. f c)"
definition "entries m = L.map (map_prod (λc. c) id) (RBT.entries m)"
end
lemmas [code] =
  ― ‹def›
  RBTS.lookup_def
  RBTS.insert_def
  RBTS.map_entry_def
  RBTS.modify_def_def
  RBTS.keys_def
  RBTS.lookup2_def
  RBTS.insert2_def
  RBTS.fold_def
  RBTS.entries_def

syntax "_rbt_lookup" :: "_  _" ("lookup") translations "lookup"  "CONST RBTS.lookup"
syntax "_rbt_insert" :: "_  _" ("insert") translations "insert"  "CONST RBTS.insert"
syntax "_rbt_map_entry" :: "_  _" ("map'_entry") translations "map_entry"  "CONST RBTS.map_entry"
syntax "_rbt_modify_def" :: "_  _" ("modify'_def") translations "modify_def"  "CONST RBTS.modify_def"
syntax "_rbt_keys" :: "_  _" ("keys") translations "keys"  "CONST RBTS.keys"
syntax "_rbt_lookup2" :: "_  _" ("lookup2") translations "lookup2"  "CONST RBTS.lookup2"
syntax "_rbt_insert2" :: "_  _" ("insert2") translations "insert2"  "CONST RBTS.insert2"
syntax "_rbt_fold" :: "_  _" ("fold") translations "fold"  "CONST RBTS.fold"
syntax "_rbt_entries" :: "_  _" ("entries") translations "entries"  "CONST RBTS.entries"

function (sequential) class_unflat_aux where
(* (* FIXME replace with this simplified form *)
   "class_unflat_aux rbt rbt_inv rbt_cycle r =
   (case lookup rbt_cycle r of (None ― ‹cycle detection›) ⇒
      ToyClass
        r
        (case lookup rbt r of Some l ⇒ l)
        (L.map
          (class_unflat_aux rbt rbt_inv (insert r () rbt_cycle))
          (case lookup rbt_inv r of None ⇒ [] | Some l ⇒ l)))"
*)
   "class_unflat_aux rbt rbt_inv rbt_cycle r =
   (case lookup rbt_inv r of
  None 
(case lookup rbt_cycle r of (None ― ‹cycle detection›) 
      ToyClass
        r
        (case lookup rbt r of Some l  l)
        ( ( [])))
| Some l 
(case lookup rbt_cycle r of (None ― ‹cycle detection›) 
      ToyClass
        r
        (case lookup rbt r of Some l  l)
        (L.map
          (class_unflat_aux rbt rbt_inv (insert r () rbt_cycle))
          ( l))))"
by pat_completeness auto

termination
proof -
 have arith_diff: "a1 a2 (b :: Nat.nat). a1 = a2  a1 > b  a1 - (b + 1) < a2 - b"
 by arith

 have arith_less: "(a:: Nat.nat) b c. b  max (a + 1) c  a < b"
 by arith

 have rbt_length: "rbt_cycle r v. RBT.lookup rbt_cycle r = None 
     length (RBT.keys (RBT.insert r v rbt_cycle)) = length (RBT.keys rbt_cycle) + 1"
  apply(subst (1 2) distinct_card[symmetric], (rule distinct_keys)+)
  apply(simp only: lookup_keys[symmetric], simp)
 by (metis card_insert_if domIff finite_dom_lookup)

 have rbt_fold_union'': "ab a x k. dom (λb. if b = ab then Some a else k b) = {ab}  dom k"
 by(auto)

 have rbt_fold_union': "l rbt_inv a.
       dom (RBT.lookup (List.fold (λ(k, _). RBT.insert k a) l rbt_inv)) =
       dom (map_of l)  dom (RBT.lookup rbt_inv)"
  apply(rule_tac P = "λrbt_inv . dom (RBT.lookup (List.fold (λ(k, _). RBT.insert k a) l rbt_inv)) =
       dom (map_of l)  dom (RBT.lookup rbt_inv)" in allE, simp_all)
  apply(induct_tac l, simp, rule allI)
  apply(case_tac aa, simp)
  apply(simp add: rbt_fold_union'')
 done

 have rbt_fold_union: "rbt_cycle rbt_inv a.
   dom (RBT.lookup (RBT.fold (λk _. RBT.insert k a) rbt_cycle rbt_inv)) =
   dom (RBT.lookup rbt_cycle)  dom (RBT.lookup rbt_inv)"
  apply(simp add: fold_fold)
  apply(subst (2) map_of_entries[symmetric])
  apply(rule rbt_fold_union')
 done

 have rbt_fold_eq: "rbt_cycle rbt_inv a b.
   dom (RBT.lookup (RBT.fold (λk _. RBT.insert k a) rbt_cycle rbt_inv)) =
   dom (RBT.lookup (RBT.fold (λk _. RBT.insert k b) rbt_inv rbt_cycle))"
 by(simp add: rbt_fold_union Un_commute)

 let ?len = "λx. length (RBT.keys x)"
 let ?len_merge = "λrbt_cycle rbt_inv. ?len (RBT.fold (λk _. RBT.insert k []) rbt_cycle rbt_inv)"

 have rbt_fold_large: "rbt_cycle rbt_inv. ?len_merge rbt_cycle rbt_inv  max (?len rbt_cycle) (?len rbt_inv)"
  apply(subst (1 2 3) distinct_card[symmetric], (rule distinct_keys)+)
  apply(simp only: lookup_keys[symmetric], simp)
  apply(subst (1 2) card_mono, simp_all)
  apply(simp add: rbt_fold_union)+
 done

 have rbt_fold_eq: "rbt_cycle rbt_inv r a.
     RBT.lookup rbt_inv r = Some a 
     ?len_merge (RBT.insert r () rbt_cycle) rbt_inv = ?len_merge rbt_cycle rbt_inv"
  apply(subst (1 2) distinct_card[symmetric], (rule distinct_keys)+)
  apply(simp only: lookup_keys[symmetric])
  apply(simp add: rbt_fold_union)
 by (metis Un_insert_right insert_dom)

 show ?thesis
  apply(relation "measure (λ(_, rbt_inv, rbt_cycle, _).
                           ?len_merge rbt_cycle rbt_inv - ?len rbt_cycle)"
       , simp+)
  unfolding RBTS.lookup_def RBTS.insert_def
  apply(subst rbt_length, simp)
  apply(rule arith_diff)
  apply(rule rbt_fold_eq, simp)
  apply(rule arith_less)
  apply(subst rbt_length[symmetric], simp)
  apply(rule rbt_fold_large)
 done
qed
definition "ty_obj_to_string = (λToyTyObj (ToyTyCore_pre s) _  s)"
definition "cl_name_to_string = ty_obj_to_string o ClassRaw_name"

definition "class_unflat = (λ (l_class, l_ass).
  let l =
    let const_toyany' = ToyTyCore_pre const_toyany
      ; rbt = ― ‹fold classes:›
              ― ‹set ToyAny› as default inherited class (for all classes linking to zero inherited classes)›
              insert
                const_toyany
                (toy_class_raw.make (ToyTyObj const_toyany' []) [] [] False)
                (List.fold
                  (λ cflat 
                    insert (cl_name_to_string cflat) (cflat  ClassRaw_name := case ClassRaw_name cflat of ToyTyObj n []  ToyTyObj n [[const_toyany']] | x  x ))
                  l_class
                  RBT.empty) in
    ― ‹fold associations:›
    ― ‹add remaining 'object' attributes›
    L.map snd (entries (List.fold (λ (ass_oid, ass) 
      let l_rel = ToyAss_relation' ass in
      fold_max
        (let n_rel = natural_of_nat (List.length l_rel) in
         (λ (cpt_to, (name_to, category_to)).
           case TyRole category_to of
             Some role_to 
               List.fold (λ (cpt_from, (name_from, mult_from)).
                 let name_from = ty_obj_to_string name_from in
                 map_entry name_from (λcflat. cflat  ClassRaw_own := (role_to,
                   ToyTy_class (toy_ty_class_ext const_oid ass_oid n_rel
                     (toy_ty_class_node_ext cpt_from mult_from name_from ())
                     (toy_ty_class_node_ext cpt_to category_to (ty_obj_to_string name_to) ())
                     ())) # ClassRaw_own cflat ))
           | _  λ_. id))
        l_rel) (L.mapi Pair l_ass) rbt)) in
  class_unflat_aux
    (List.fold (λ cflat. insert (cl_name_to_string cflat) (L.map (map_prod id remove_binding) (ClassRaw_own cflat))) l RBT.empty)
    (List.fold
      (λ cflat.
        case ClassRaw_name cflat of
          ToyTyObj n []  id
        | ToyTyObj n l  case rev ([n] # l) of x0 # xs  λrbt. 
            snd (List.fold
                  (λ x (x0, rbt).
                    (x, List.fold (λ ToyTyCore_pre k  modify_def [] k (λl. L.flatten [L.map (λToyTyCore_pre s  s) x, l]))
                                  x0
                                  rbt))
                  xs
                  (x0, rbt)))
      l
      RBT.empty)
    RBT.empty
    const_toyany)"

definition "apply_optim_ass_arity ty_obj v =
  (if TyObj_ass_arity ty_obj  2 then None
   else Some v)"

definition "is_higher_order = (λ ToyTy_collection _ _  True | ToyTy_pair _ _  True | _  False)"

definition "parse_ty_raw = (λ ToyTy_raw s  if s = ‹int› then ToyTy_base_integer else ToyTy_raw s
                            | x  x)"

definition "is_sequence = list_ex (λ Sequence  True | _  False) o TyCollect"

fun str_of_ty where "str_of_ty e =
 (λ ToyTy_base_void  ‹Void›
  | ToyTy_base_boolean  ‹Boolean›
  | ToyTy_base_integer  ‹Integer›
  | ToyTy_base_unlimitednatural  ‹UnlimitedNatural›
  | ToyTy_base_real  ‹Real›
  | ToyTy_base_string  ‹String›
  | ToyTy_object (ToyTyObj (ToyTyCore_pre s) _)  s
  ⌦‹| ToyTy_object (ToyTyObj (ToyTyCore ty_obj) _)›
  | ToyTy_collection t toy_ty  (if is_sequence t then
                                    S.flatten [‹Sequence(›, str_of_ty toy_ty,‹)›]
                                  else
                                    S.flatten [‹Set(›, str_of_ty toy_ty,‹)›])
  | ToyTy_pair toy_ty1 toy_ty2  S.flatten [‹Pair(›, str_of_ty toy_ty1, ‹,›, str_of_ty toy_ty2,‹)›]
  | ToyTy_binding (_, toy_ty)  str_of_ty toy_ty
  | ToyTy_class_syn s  s
  | ToyTy_enum s  s
  | ToyTy_raw s  S.flatten [‹´›, s, ‹´›]) e"

definition "ty_void = str_of_ty ToyTy_base_void"
definition "ty_boolean = str_of_ty ToyTy_base_boolean"
definition "ty_integer = str_of_ty ToyTy_base_integer"
definition "ty_unlimitednatural = str_of_ty ToyTy_base_unlimitednatural"
definition "ty_real = str_of_ty ToyTy_base_real"
definition "ty_string = str_of_ty ToyTy_base_string"

definition "pref_ty_enum s = ‹ty_enum› @@ String.isub s"
definition "pref_ty_syn s = ‹ty_syn› @@ String.isub s"
definition "pref_constr_enum s = ‹constr› @@ String.isub s"

fun str_hol_of_ty_all where "str_hol_of_ty_all f b e =
 (λ ToyTy_base_void  b ‹unit›
  | ToyTy_base_boolean  b ‹bool›
  | ToyTy_base_integer  b ‹int›
  | ToyTy_base_unlimitednatural  b ‹nat›
  | ToyTy_base_real  b ‹real›
  | ToyTy_base_string  b ‹string›
  | ToyTy_object (ToyTyObj (ToyTyCore_pre s) _)  b const_oid
  | ToyTy_object (ToyTyObj (ToyTyCore ty_obj) _)  f (b var_ty_list) [b (TyObj_name ty_obj)]
  | ToyTy_collection _ ty  f (b var_ty_list) [str_hol_of_ty_all f b ty]
  | ToyTy_pair ty1 ty2  f (b var_ty_prod) [str_hol_of_ty_all f b ty1, str_hol_of_ty_all f b ty2]
  | ToyTy_binding (_, t)  str_hol_of_ty_all f b t
  | ToyTy_class_syn s  b (pref_ty_syn s)
  | ToyTy_enum s  b (pref_ty_enum s)
  | ToyTy_raw s  b s) e"

fun get_class_hierarchy_strict_aux where
   "get_class_hierarchy_strict_aux dataty l_res =
   (List.fold
     (λ ToyClass name l_attr dataty  λ l_res.
       get_class_hierarchy_strict_aux dataty (ToyClass name l_attr dataty # l_res))
     dataty
     l_res)"
definition "get_class_hierarchy_strict d = get_class_hierarchy_strict_aux d []"

fun get_class_hierarchy'_aux where
   "get_class_hierarchy'_aux l_res (ToyClass name l_attr dataty) =
   (let l_res = ToyClass name l_attr dataty # l_res in
    case dataty of []  rev l_res
                 | dataty  List.fold (λx acc. get_class_hierarchy'_aux acc x) dataty l_res)"
definition "get_class_hierarchy' = get_class_hierarchy'_aux []"

definition "get_class_hierarchy e = L.map (λ ToyClass n l _  (n, l)) (get_class_hierarchy' e)"

definition "var_in_pre_state = ‹in_pre_state›"
definition "var_in_post_state = ‹in_post_state›"
definition "var_at_when_hol_post = ‹›"
definition "var_at_when_hol_pre = ‹at_pre›"
definition "var_at_when_toy_post = ‹›"
definition "var_at_when_toy_pre = ‹@pre›"

datatype 'a tmp_sub = Tsub 'a
record 'a inheritance =
  Inh :: 'a
  Inh_sib :: "('a × 'a list ― ‹flat version of the 1st component›) list" ― ‹sibling›
  Inh_sib_unflat :: "'a list" ― ‹sibling›
datatype 'a tmp_inh = Tinh 'a
datatype 'a tmp_univ = Tuniv 'a
definition "of_inh = (λTinh l  l)"
definition "of_linh = L.map Inh"
definition "of_sub = (λTsub l  l)"
definition "of_univ = (λTuniv l  l)"
definition "map_inh f = (λTinh l  Tinh (f l))"

fun fold_class_gen_aux where
   "fold_class_gen_aux l_inh f accu (ToyClass name l_attr dataty) =
 (let accu = f (λs. s @@ String.isub name)
               name
               l_attr
               (Tinh l_inh)
               (Tsub (get_class_hierarchy_strict dataty)) ― ‹order: bfs or dfs (modulo reversing)›
               dataty
               accu in
  case dataty of []  accu
               | _ 
    fst (List.fold
       (λ node (accu, l_inh_l, l_inh_r).
         ( fold_class_gen_aux
             (  Inh = ToyClass name l_attr dataty
               , Inh_sib = L.flatten (L.map (L.map (λl. (l, get_class_hierarchy' l))) [l_inh_l, tl l_inh_r])
               , Inh_sib_unflat = L.flatten [l_inh_l, tl l_inh_r] 
             # l_inh)
             f accu node
         , hd l_inh_r # l_inh_l
         , tl l_inh_r))
      dataty
      (accu, [], dataty)))"

definition "fold_class_gen f accu expr =
 (let (l_res, accu) =
    fold_class_gen_aux
      []
      (λ isub_name name l_attr l_inh l_subtree next_dataty (l_res, accu).
        let (r, accu) = f isub_name name l_attr l_inh l_subtree next_dataty accu in
        (r # l_res, accu))
      ([], accu)
      expr in
  (L.flatten l_res, accu))"

definition "map_class_gen f = fst o fold_class_gen
  (λ isub_name name l_attr l_inh l_subtree last_d. λ () 
    (f isub_name name l_attr l_inh l_subtree last_d, ())) ()"

definition "add_hierarchy'''' f x = (λisub_name name l_attr l_inh l_subtree _. f isub_name name (Tuniv (get_class_hierarchy x)) l_attr (map_inh (L.map (λ ToyClass _ l _  l) o of_linh) l_inh) l_subtree)"
definition "map_class f = map_class_gen (λisub_name name l_attr l_inh l_subtree next_dataty. [f isub_name name l_attr l_inh (Tsub (L.map (λ ToyClass n _ _  n) (of_sub l_subtree))) next_dataty])"
definition "fold_class f = fold_class_gen (λisub_name name l_attr l_inh l_subtree next_dataty accu. let (x, accu) = f isub_name name l_attr (map_inh of_linh l_inh) (Tsub (L.map (λ ToyClass n _ _  n) (of_sub l_subtree))) next_dataty accu in ([x], accu))"
definition "map_class_gen_h'''' f x = map_class_gen (add_hierarchy'''' (λisub_name name l_inherited l_attr l_inh l_subtree. f isub_name name l_inherited l_attr l_inh (Tsub (L.map (λ ToyClass n _ _  n) (of_sub l_subtree)))) x) x"

definition "class_arity = RBT.keys o (λl. List.fold (λx. RBT.insert x ()) l RBT.empty) o
  L.flatten o L.flatten o map_class (λ _ _ l_attr _ _ _.
    L.map (λ (_, ToyTy_object (ToyTyObj (ToyTyCore ty_obj) _))  [TyObj_ass_arity ty_obj]
              | _  []) l_attr)"

definition "map_class_inh l_inherited = L.map (λ ToyClass _ l _  l) (of_inh (map_inh of_linh l_inherited))"

end