Theory Floor1_examp
section‹Main Translation for: Example (Floor 1)›
theory Floor1_examp
imports Core_init
begin
definition "list_bind f0 f l =
(let l = L.map f0 l in
if list_ex (λ None ⇒ True | _ ⇒ False) l then
None
else
Some (f (List.map_filter id l)))"
definition "rbt_of_class env =
(let rbt = (snd o fold_class_gen (λ_ name l_attr l_inh _ _ rbt.
( [()]
, modify_def (RBT.empty, []) name
(let f_fold = λtag l rbt.
let (rbt, _, n) = List.fold
(λ (name_attr, ty) ⇒ λ(rbt, cpt, l_obj).
(insert name_attr (ty, tag, OptIdent cpt) rbt, Succ cpt, (case ty of ToyTy_object (ToyTyObj (ToyTyCore ty_obj) _) ⇒ Some ty_obj | _ ⇒ None) # l_obj))
l
(rbt, 0, []) in
(rbt, (tag, n)) in
(λ(rbt, _).
let (rbt, info_own) = f_fold OptOwn l_attr rbt in
let (rbt, info_inh) = f_fold OptInh (L.flatten (map_class_inh l_inh)) rbt in
(rbt, [info_own, info_inh])))
rbt)) RBT.empty) (case D_input_class env of Some c ⇒ c) in
(λname.
let rbt = lookup rbt name in
( rbt = None
, λ name_attr.
Option.bind rbt (λ(rbt, _). lookup rbt name_attr)
, λ v. Option.bind rbt (λ(_, l).
map_option (λl f accu.
let (_, accu) =
List.fold
(let f_fold = λb (n, accu). (Succ n, f b n accu) in
if D_toy_semantics env = Gen_only_design then
f_fold
else
λ Some _ ⇒ (λ(n, accu). (Succ n, accu))
| None ⇒ f_fold None) (rev l) (0, accu) in
accu) (L.assoc v l)))))"
definition "inst_name toyi = (case Inst_name toyi of Some n ⇒ n)"
definition "init_map_class env l =
(let (rbt_nat, rbt_str, _, _) =
List.fold
(λ toyi (rbt_nat, rbt_str, oid_start, accu).
( RBT.insert (Oid accu) oid_start rbt_nat
, insert (inst_name toyi) oid_start rbt_str
, oidSucInh oid_start
, Succ accu))
l
( RBT.empty
, RBT.bulkload (L.map (λ(k, _, v). (String⇩b⇩a⇩s⇩e.to_list k, v)) (D_input_instance env))
, D_toy_oid_start env
, 0) in
(rbt_of_class env, RBT.lookup rbt_nat, lookup rbt_str))"
definition "print_examp_def_st_assoc_build_rbt_gen f rbt map_self map_username l_assoc =
List.fold
(λ (toyi, cpt). fold_instance_single
(λ ty l_attr.
let (f_attr_ty, _) = rbt ty in
f ty
(List.fold (λ(_, name_attr, shall).
case f_attr_ty name_attr of
Some (ToyTy_object (ToyTyObj (ToyTyCore ty_obj) _), _, _) ⇒
modify_def ([], ty_obj) name_attr
(λ(l, accu). case let find_map = λ ShallB_str s ⇒ map_username s | ShallB_self s ⇒ map_self s | _ ⇒ None in
case shall of
ShallB_list l ⇒ if list_ex (λx. find_map x = None) l then
None
else
Some (List.map_filter find_map l)
| _ ⇒ map_option (λx. [x]) (find_map shall) of
None ⇒ (l, accu)
| Some oid ⇒ (L.map (L.map oidGetInh) [[cpt], oid] # l, accu))
| _ ⇒ id) l_attr)) toyi) l_assoc RBT.empty"
definition "print_examp_def_st_assoc_build_rbt = print_examp_def_st_assoc_build_rbt_gen (modify_def RBT.empty)"
definition "print_examp_def_st_assoc rbt map_self map_username l_assoc =
(let b = λs. Term_basic [s]
; rbt = print_examp_def_st_assoc_build_rbt rbt map_self map_username l_assoc in
Term_app var_map_of_list [Term_list (fold (λname. fold (λname_attr (l_attr, ty_obj) l_cons.
let cpt_from = TyObjN_ass_switch (TyObj_from ty_obj) in
Term_pair
(Term_basic [print_access_oid_uniq_name cpt_from (λs. s @@ String.isub name) name_attr])
(Term_app ‹List.map›
[ Term_binop (let var_x = ‹x›
; var_y = ‹y› in
Term_lambdas0
(Term_pair (b var_x) (b var_y))
(Term_list [b var_x, b var_y]))
‹o›
(b (print_access_choose_name
(TyObj_ass_arity ty_obj)
cpt_from
(TyObjN_ass_switch (TyObj_to ty_obj))))
, Term_list' (Term_list' (Term_list' (Term_oid var_oid_uniq))) l_attr ])
# l_cons)) rbt [])])"
definition "print_examp_instance_oid thy_definition_hol l env = (L.map thy_definition_hol o L.flatten)
(let (f1, f2) = (λ var_oid _ _. var_oid, λ _ _ cpt. Term_oid ‹› (oidGetInh cpt)) in
L.map (λ (toyi, cpt).
if List.fold (λ(_, _, cpt0) b. b | oidGetInh cpt0 = oidGetInh cpt) (D_input_instance env) False then
[]
else
let var_oid = Term_oid var_oid_uniq (oidGetInh cpt)
; isub_name = λs. s @@ String.isub (inst_ty toyi) in
[Definition (Term_rewrite (f1 var_oid isub_name toyi) ‹=› (f2 toyi isub_name cpt))]) l)"
definition "check_export_code f_writeln f_warning f_error f_raise l_report msg_last =
(let l_err =
List.fold
(λ (Writeln, s) ⇒ λacc. case f_writeln s of () ⇒ acc
| (Warning, s) ⇒ λacc. case f_warning s of () ⇒ acc
| (Error, s) ⇒ λacc. case f_error s of () ⇒ s # acc)
l_report
[] in
if l_err = [] then
()
else
f_raise (String.nat_to_digit10 (length l_err) @@ msg_last))"
definition "print_examp_instance_defassoc_gen name l_toyi env =
(case D_toy_semantics env of Gen_only_analysis ⇒ [] | Gen_default ⇒ [] | Gen_only_design ⇒
let a = λf x. Term_app f [x]
; b = λs. Term_basic [s]
; (rbt :: _ ⇒ _ × _ × (_ ⇒ ((_ ⇒ natural ⇒ _ ⇒ (toy_ty × toy_data_shallow) option list) ⇒ _ ⇒ _) option)
, (map_self, map_username)) =
init_map_class env (fst (L.split l_toyi))
; l_toyi = if list_ex (λ(toyi, _). inst_ty0 toyi = None) l_toyi then [] else l_toyi in
[Definition
(Term_rewrite name
‹=›
(let var_oid_class = ‹oid_class›
; var_to_from = ‹to_from›
; var_oid = ‹oid›
; a_l = λs. Typ_apply (Typ_base var_ty_list) [s] in
Term_lambdas
[var_oid_class, var_to_from, var_oid]
(Term_annot (Term_case
(Term_app var_deref_assocs_list
[ Term_annot (b var_to_from) (Ty_arrow
(a_l (a_l (Typ_base const_oid)))
(let t = a_l (Typ_base const_oid) in
Ty_times t t))
, Term_annot' (b var_oid) const_oid
, a ‹drop›
(Term_applys (print_examp_def_st_assoc (snd o rbt) map_self map_username l_toyi)
[Term_annot' (b var_oid_class) const_oid])])
[ (b ‹Nil›, b ‹None›)
, let b_l = b ‹l› in
(b_l, a ‹Some› b_l)] ) (Typ_apply (Typ_base ‹option›) [a_l (Typ_base const_oid)]))))])"
definition "print_examp_instance_defassoc = (λ ToyInstance l ⇒ λ env.
let l = L.flatten (fst (L.mapM (λtoyi cpt. ([(toyi, cpt)], oidSucInh cpt)) l (D_toy_oid_start env))) in
(λl_res.
( print_examp_instance_oid O.definition l env
@@@@ L.map O.definition l_res
, env))
(print_examp_instance_defassoc_gen
(Term_oid var_inst_assoc (oidGetInh (D_toy_oid_start env)))
l
env))"
definition "print_examp_instance_name = id"
definition "print_examp_instance = (λ ToyInstance l ⇒ λ env.
(λ ((l_res, oid_start), instance_rbt).
((L.map O.definition o L.flatten) l_res, env ⦇ D_toy_oid_start := oid_start, D_input_instance := instance_rbt ⦈))
(let ( rbt :: _ ⇒ _ × _ × (_ ⇒ ((_ ⇒ nat ⇒ _ ⇒ _) ⇒ _ ⇒
(toy_ty_class option ×
(toy_ty × (string × string) option × toy_data_shallow) option) list) option)
, (map_self, map_username)) = init_map_class env l
; a = λf x. Term_app f [x]
; b = λs. Term_basic [s] in
( let var_inst_ass = ‹inst_assoc› in
L.mapM
(λ toyi cpt.
( []
, oidSucInh cpt))
l
(D_toy_oid_start env)
, List.fold (λtoyi instance_rbt.
let n = inst_name toyi in
(String.to_String⇩b⇩a⇩s⇩e n, toyi, case map_username n of Some oid ⇒ oid) # instance_rbt) l (D_input_instance env))))"
definition "print_examp_def_st1 = (λ ToyDefSt name l ⇒ bootstrap_floor
(λl env. (L.flatten [l], env))
(L.map META_all_meta_embedding
(let (l, _) = List.fold (λ (pos, core) (l, n).
((pos, pos - n, core) # l,
case core of ToyDefCoreAdd _ ⇒ n
| ToyDefCoreBinding _ ⇒ Succ n))
(L.mapi Pair l)
([], 0)
; (l_inst, l_defst) =
List.fold (λ (pos, _, ToyDefCoreAdd toyi) ⇒ λ(l_inst, l_defst).
let i_name = case Inst_name toyi of Some x ⇒ x | None ⇒ S.flatten [name, ‹_object›, String.natural_to_digit10 pos] in
( map_instance_single (map_prod id (map_prod id (map_data_shallow_self (λOid self ⇒
(case L.assoc self l of
Some (_, ToyDefCoreBinding name) ⇒ ShallB_str name
| Some (p, _) ⇒ ShallB_self (Oid p)
| _ ⇒ ShallB_list []))))) toyi
⦇ Inst_name := Some i_name ⦈
# l_inst
, ToyDefCoreBinding i_name # l_defst)
| (_, _, ToyDefCoreBinding name) ⇒ λ(l_inst, l_defst).
( l_inst
, ToyDefCoreBinding name # l_defst))
l
([], [])
; l = [ META_def_state Floor2 (ToyDefSt name l_defst) ] in
if l_inst = [] then
l
else
META_instance (ToyInstance l_inst) # l)))"
definition "print_pre_post = (λ ToyDefPP name s_pre s_post ⇒ bootstrap_floor
(λf env. (L.flatten [f env], env))
(λenv.
let pref_name = case name of Some n ⇒ n
| None ⇒ ‹WFF_› @@ String.nat_to_digit10 (length (D_input_meta env))
; f_comp = λNone ⇒ id | Some (_, f) ⇒ f
; f_conv = λmsg.
λ ToyDefPPCoreAdd toy_def_state ⇒
let n = pref_name @@ msg in
(ToyDefPPCoreBinding n, Cons (META_def_state Floor1 (ToyDefSt n toy_def_state)))
| s ⇒ (s, id) in
L.map
META_all_meta_embedding
(let o_pre = Some (f_conv ‹_pre› s_pre)
; o_post = map_option (f_conv ‹_post›) s_post in
(f_comp o_pre o f_comp o_post)
[ META_def_pre_post Floor2 (ToyDefPP name
(case o_pre of Some (n, _) ⇒ n)
(map_option fst o_post)) ])))"
end