Theory Core_init
chapter‹Translating Meta-Models›
section‹General Environment for the Translation: Introduction›
theory Core_init
imports "../../Toy_Library_Static"
"../meta_toy/Meta_META"
begin
text‹This file regroups common utilities used by the embedding functions of Toy in Isabelle.›
datatype opt_attr_type = OptInh | OptOwn
datatype opt_ident = OptIdent nat
instantiation internal_oid :: linorder
begin
definition "n_of_internal_oid = (λ Oid n ⇒ n)"
definition "n ≤ m ⟷ n_of_internal_oid n ≤ n_of_internal_oid m"
definition "n < m ⟷ n_of_internal_oid n < n_of_internal_oid m"
instance
apply standard
apply (metis less_eq_internal_oid_def less_imp_le less_internal_oid_def not_less)
apply (metis less_eq_internal_oid_def order_refl)
apply (metis less_eq_internal_oid_def order.trans)
apply (simp add: less_eq_internal_oid_def n_of_internal_oid_def, case_tac x, case_tac y, simp)
apply (metis le_cases less_eq_internal_oid_def)
done
end
definition "var_oid_uniq = ‹oid›"
definition "var_deref_assocs_list = ‹deref_assocs_list›"
definition "var_inst_assoc = ‹inst_assoc›"
definition "var_choose = ‹choose›"
definition "var_switch = ‹switch›"
definition "var_assocs = ‹assocs›"
definition "var_map_of_list = ‹map_of_list›"
definition "var_self = ‹self›"
definition "var_result = ‹result›"
definition "find_class_ass env =
(let (l_class, l_all_meta) =
partition (let f = λclass. ClassRaw_clause class = [] in
λ META_class_raw Floor1 class ⇒ f class
| META_association _ ⇒ True
| META_ass_class Floor1 (ToyAssClass _ class) ⇒ f class
| META_class_synonym _ ⇒ True
| _ ⇒ False) (rev (D_input_meta env)) in
( L.flatten [l_class, List.map_filter (let f = λclass. class ⦇ ClassRaw_clause := [] ⦈ in
λ META_class_raw Floor1 c ⇒ Some (META_class_raw Floor1 (f c))
| META_ass_class Floor1 (ToyAssClass ass class) ⇒ Some (META_ass_class Floor1 (ToyAssClass ass (f class)))
| _ ⇒ None) l_all_meta]
, L.flatten (L.map
(let f = λclass. [ META_ctxt Floor1 (toy_ctxt_ext [] (ClassRaw_name class) (ClassRaw_clause class) ()) ] in
λ META_class_raw Floor1 class ⇒ f class
| META_ass_class Floor1 (ToyAssClass _ class) ⇒ f class
| x ⇒ [x]) l_all_meta)))"
definition "map_enum_syn l_enum l_syn =
(λ ToyTy_object (ToyTyObj (ToyTyCore_pre s) []) ⇒
if list_ex (λsyn. s ≜ (case syn of ToyClassSynonym n _ ⇒ n)) l_syn then
ToyTy_class_syn s
else if list_ex (λenum. s ≜ (case enum of ToyEnum n _ ⇒ n)) l_enum then
ToyTy_enum s
else
ToyTy_object (ToyTyObj (ToyTyCore_pre s) [])
| x ⇒ x)"
definition "arrange_ass with_aggreg with_optim_ass l_c l_enum =
(let l_syn = List.map_filter (λ META_class_synonym e ⇒ Some e
| _ ⇒ None) l_c
; l_class = List.map_filter (λ META_class_raw Floor1 cflat ⇒ Some cflat
| META_ass_class Floor1 (ToyAssClass _ cflat) ⇒ Some cflat
| _ ⇒ None) l_c
; l_class =
L.map
(λ cflat ⇒
cflat ⦇ ClassRaw_own :=
L.map (map_prod id (map_enum_syn l_enum l_syn))
(ClassRaw_own cflat) ⦈) l_class
; l_ass = List.map_filter (λ META_association ass ⇒ Some ass
| META_ass_class Floor1 (ToyAssClass ass _) ⇒ Some ass
| _ ⇒ None) l_c
; ToyMult = λl set. toy_multiplicity_ext l None set ()
; (l_class, l_ass0) =
if with_optim_ass then
map_prod rev rev (List.fold
(λc (l_class, l_ass).
let default = [Set]
; f = λrole t mult_out. ⦇ ToyAss_type = ToyAssTy_native_attribute
, ToyAss_relation = ToyAssRel [(ClassRaw_name c, ToyMult [(Mult_star, None)] default)
,(t, mult_out ⦇ TyRole := Some role ⦈)] ⦈
; (l_own, l_ass) =
List.fold (λ (role, ToyTy_object t) ⇒
λ (l_own, l). (l_own, f role t (ToyMult [(Mult_nat 0, Some (Mult_nat 1))] default) # l)
| (role, ToyTy_collection mult (ToyTy_object t)) ⇒
λ (l_own, l). (l_own, f role t mult # l)
| x ⇒ λ (l_own, l). (x # l_own, l))
(ClassRaw_own c)
([], l_ass) in
(c ⦇ ClassRaw_own := rev l_own ⦈ # l_class, l_ass))
l_class
([], []))
else
(l_class, [])
; (l_class, l_ass) =
if with_aggreg then
map_prod rev rev (List.fold
(λass (l_class, l_ass).
if ToyAss_type ass = ToyAssTy_aggregation then
( fold_max
(λ (cpt_to, (name_to, category_to)).
case TyRole category_to of
Some role_to ⇒
List.fold (λ (cpt_from, (name_from, multip_from)).
L.map_find (λcflat.
if cl_name_to_string cflat ≜ ty_obj_to_string name_from then
Some (cflat ⦇ ClassRaw_own :=
L.flatten [ ClassRaw_own cflat
, [(role_to, let ty = ToyTy_object name_to in
if single_multip category_to then
ty
else
ToyTy_collection category_to ty)]] ⦈)
else None))
| _ ⇒ λ_. id)
(ToyAss_relation' ass)
l_class
, l_ass)
else
(l_class, ass # l_ass)) l_ass (l_class, []))
else
(l_class, l_ass) in
( l_class
, L.flatten [l_ass, l_ass0]))"
definition "datatype_name = ‹ty›"
definition "datatype_ext_name = datatype_name @@ ‹ℰ𝒳𝒯›"
definition "datatype_constr_name = ‹mk›"
definition "datatype_ext_constr_name = datatype_constr_name @@ ‹ℰ𝒳𝒯›"
definition "datatype_in = ‹in›"
subsection‹Main Combinators for the Translation›
text‹
As general remark, all the future translating steps
(e.g., that will occur in @{file ‹Floor1_access.thy›})
will extensively use Isabelle expressions,
represented by its Meta-Model, for example lots of functions will use @{term "Term_app"}...
So the overall can be simplified by the use of polymorphic cartouches.
It looks feasible to add a new front-end for cartouches in @{theory Isabelle_Meta_Model.Init}
supporting the use of Isabelle syntax in cartouches,
then we could obtain at the end a parsed Isabelle Meta-Model in Isabelle.›
definition "start_map f = L.mapM (λx acc. (f x, acc))"
definition "start_map''' f fl = (λ env.
let design_analysis = D_toy_semantics env
; base_attr = (if design_analysis = Gen_only_design then id else L.filter (λ (_, ToyTy_object (ToyTyObj (ToyTyCore _) _)) ⇒ False | _ ⇒ True))
; base_attr' = (λ (l_attr, l_inh). (base_attr l_attr, L.map base_attr l_inh))
; base_attr'' = (λ (l_attr, l_inh). (base_attr l_attr, base_attr l_inh)) in
start_map f (fl design_analysis base_attr base_attr' base_attr'') env)"
definition "start_map'' f fl e = start_map''' f (λ_. fl) e"
definition "start_map'''' f fl = (λ env. start_map f (fl (D_toy_semantics env)) env)"
definition "bootstrap_floor f_x l env =
(let (l, env) = f_x l env
; l_setup = META_boot_setup_env (Boot_setup_env (env ⦇ D_output_disable_thy := True
, D_output_header_thy := None
, D_output_position := (0, 0) ⦈) )
# l
; l = if case D_input_meta env of [] ⇒ True | x # _ ⇒ ignore_meta_header x then
l
else
l_setup in
( if D_output_auto_bootstrap env then
l
else
META_boot_generation_syntax (Boot_generation_syntax (D_toy_semantics env))
# l_setup
, env ⦇ D_output_auto_bootstrap := True ⦈ ))"
definition "wrap_toyty x = ‹⋅› @@ x"
definition "Term_annot_toy e s = Term_annot' e (wrap_toyty s)"
definition "Term_toyset l = (case l of [] ⇒ Term_basic [‹Set{}›] | _ ⇒ Term_paren ‹Set{› ‹}› (term_binop ‹,› l))"
definition "Term_oid s = (λOid n ⇒ Term_basic [s @@ String.natural_to_digit10 n])"
subsection‹Preliminaries on: Enumeration›
subsection‹Preliminaries on: Infrastructure›
subsection‹Preliminaries on: Accessor›
definition "print_access_oid_uniq_name' name_from_nat isub_name attr = S.flatten [ isub_name var_oid_uniq, ‹_›, String.natural_to_digit10 name_from_nat, ‹_›, attr ]"
definition "print_access_oid_uniq_name name_from_nat isub_name attr = print_access_oid_uniq_name' name_from_nat isub_name (String.isup attr)"
definition "print_access_choose_name n i j =
S.flatten [var_switch, String.isub (String.natural_to_digit10 n), ‹_›, String.natural_to_digit10 i, String.natural_to_digit10 j]"
subsection‹Preliminaries on: Example (Floor 1)›