Skip to content

Commit 1c6dea4

Browse files
jvanbrueggejvanbruegge
committed
Make use of free vars in mrbnf when constructing mrsbnf/bmv from them
1 parent 40e4b0b commit 1c6dea4

File tree

5 files changed

+293
-95
lines changed

5 files changed

+293
-95
lines changed

‎Tools/bmv_monad_def.ML‎

Lines changed: 113 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -93,10 +93,8 @@ signature BMV_MONAD_DEF = sig
9393
val pbmv_monad_of_generic: Context.generic -> string -> bmv_monad option;
9494
val pbmv_monad_of: Proof.context -> string -> bmv_monad option;
9595

96-
val id_mrbnf: MRBNF_Def.mrbnf;
97-
98-
val pbmv_monad_of_bnf: BNF_Def.bnf -> local_theory -> bmv_monad * local_theory
99-
val register_bnf_as_pbmv_monad: string -> local_theory -> local_theory
96+
val pbmv_monad_of_mrbnf: MRBNF_Def.mrbnf -> local_theory -> bmv_monad * local_theory
97+
val register_mrbnf_as_pbmv_monad: string -> local_theory -> local_theory
10098
val note_bmv_monad_thms: (Proof.context -> BNF_Def.fact_policy) -> (binding -> binding)
10199
-> binding option -> bmv_monad -> local_theory -> (string * thm list) list * local_theory
102100
val bmv_monad_def: BNF_Def.inline_policy -> (Proof.context -> BNF_Def.fact_policy)
@@ -110,8 +108,6 @@ structure BMV_Monad_Def : BMV_MONAD_DEF = struct
110108

111109
open MRBNF_Util
112110

113-
val id_mrbnf = the (MRBNF_Def.mrbnf_of @{context} "BMV_Monad.ID");
114-
115111
type 'a bmv_monad_axioms = {
116112
Sb_Inj: 'a,
117113
Sb_comp_Injs: 'a list,
@@ -539,11 +535,11 @@ fun mk_param_axiom Map Supps SSupps Sb Injs RVrs Vrs bd lthy =
539535
))
540536
) (RVrs @ Vrs);
541537

542-
val Supp_Sb = map (fn Supp =>
543-
fold_rev Logic.all (rhos @ hs @ [x]) (mk_Trueprop_eq (
538+
val Supp_Sb = map (fn Supp => fold_rev Logic.all (rhos @ hs @ [x]) (
539+
fold_rev (curry Logic.mk_implies) (mk_small_prems hs rhos SSupps) (mk_Trueprop_eq (
544540
Supp $ (Term.list_comb (Sb, hs @ rhos) $ x), Supp $ x
545541
))
546-
) Supps;
542+
)) Supps;
547543
in {
548544
axioms = {
549545
Map_id = Map_id,
@@ -899,75 +895,139 @@ fun bmv_monad_def const_policy fact_policy qualify bmv_b_opt (model: (Proof.cont
899895
val model = mk_thm_model model params axioms SSupp_eq bd_irco;
900896
in apfst (rpair unfold_set) (mk_bmv_monad const_policy fact_policy qualify SSupp_defs bmv_b_opt model lthy) end
901897

902-
fun pbmv_monad_of_bnf bnf lthy =
898+
fun pbmv_monad_of_mrbnf mrbnf lthy =
903899
let
904-
val (((lives, lives'), deads), _) = lthy
905-
|> mk_TFrees (BNF_Def.live_of_bnf bnf)
906-
||>> mk_TFrees (BNF_Def.live_of_bnf bnf)
907-
||>> mk_TFrees' (map Type.sort_of_atyp (BNF_Def.deads_of_bnf bnf))
908-
val T = BNF_Def.mk_T_of_bnf deads lives bnf;
909-
val n = BNF_Def.live_of_bnf bnf;
910-
val var_class = case BNF_Def.bd_of_bnf bnf of
900+
val (((((lives, lives'), frees), bounds), deads), names_lthy) = lthy
901+
|> mk_TFrees (MRBNF_Def.live_of_mrbnf mrbnf)
902+
||>> mk_TFrees (MRBNF_Def.live_of_mrbnf mrbnf)
903+
||>> mk_TFrees' (map Type.sort_of_atyp (MRBNF_Def.frees_of_mrbnf mrbnf))
904+
||>> mk_TFrees' (map Type.sort_of_atyp (MRBNF_Def.bounds_of_mrbnf mrbnf))
905+
||>> mk_TFrees' (map Type.sort_of_atyp (MRBNF_Def.deads_of_mrbnf mrbnf));
906+
907+
val ((fs, gs), _) = names_lthy
908+
|> mk_Frees "f" (map (fn a => a --> a) frees)
909+
||>> mk_Frees "g" (map2 (curry (op-->)) lives lives');
910+
val T = MRBNF_Def.mk_T_of_mrbnf deads lives bounds frees mrbnf;
911+
val n = MRBNF_Def.live_of_mrbnf mrbnf + MRBNF_Def.bound_of_mrbnf mrbnf + MRBNF_Def.free_of_mrbnf mrbnf;
912+
val var_class = case MRBNF_Def.bd_of_mrbnf mrbnf of
911913
@{term natLeq} => @{class var}
912914
| _ => error "TODO: other var classes"
915+
916+
val (lsets, _, fsets) = MRBNF_Def.deinterlace (MRBNF_Def.mk_sets_of_mrbnf
917+
(replicate n deads) (replicate n lives) (replicate n bounds) (replicate n frees) mrbnf
918+
) (MRBNF_Def.var_types_of_mrbnf mrbnf);
919+
920+
val Sb = if null fs then HOLogic.id_const T else
921+
fold_rev (Term.absfree o dest_Free) fs (Term.list_comb (
922+
MRBNF_Def.mk_map_of_mrbnf deads lives lives bounds frees mrbnf,
923+
MRBNF_Def.interlace (map HOLogic.id_const lives) (map HOLogic.id_const bounds) fs (MRBNF_Def.var_types_of_mrbnf mrbnf)
924+
));
925+
val Map = if null lives then NONE else SOME (
926+
fold_rev (Term.absfree o dest_Free) gs (Term.list_comb (
927+
MRBNF_Def.mk_map_of_mrbnf deads lives lives' bounds frees mrbnf,
928+
MRBNF_Def.interlace gs (map HOLogic.id_const bounds) (map HOLogic.id_const frees) (MRBNF_Def.var_types_of_mrbnf mrbnf)
929+
))
930+
);
913931
in apfst fst (bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I NONE {
914932
ops = [T],
915933
var_class = var_class,
916934
leader = 0,
917-
frees = [[]],
935+
frees = [frees],
918936
lives = [lives],
919937
lives' = [lives'],
920-
deads = [deads],
938+
deads = [bounds @ deads],
921939
bmv_ops = [],
922940
consts = {
923-
bd = BNF_Def.bd_of_bnf bnf,
941+
bd = MRBNF_Def.bd_of_mrbnf mrbnf,
924942
Injs = [[]],
925943
SSupps = [[]],
926-
Sbs = [HOLogic.id_const T],
944+
Sbs = [Sb],
927945
Vrs = [[]],
928-
RVrs = [[]],
929-
params = [SOME {
930-
Map = BNF_Def.mk_map_of_bnf deads lives lives' bnf,
931-
Supps = BNF_Def.mk_sets_of_bnf (replicate n deads) (replicate n lives) bnf
932-
}]
946+
RVrs = [fsets],
947+
params = [Option.map (fn Map => {
948+
Map = Map,
949+
Supps = lsets
950+
}) Map]
933951
},
934-
params = [SOME {
952+
params = [Option.map (fn _ => {
935953
axioms = {
936-
Map_id = fn ctxt => rtac ctxt (BNF_Def.map_id0_of_bnf bnf) 1,
937-
Map_comp = fn ctxt => rtac ctxt (BNF_Def.map_comp0_of_bnf bnf RS sym) 1,
938-
Supp_Map = map (fn thm => fn ctxt => rtac ctxt thm 1) (BNF_Def.set_map_of_bnf bnf),
939-
Supp_bd = map (fn thm => fn ctxt => rtac ctxt thm 1) (BNF_Def.set_bd_of_bnf bnf),
954+
Map_id = fn ctxt => rtac ctxt (MRBNF_Def.map_id0_of_mrbnf mrbnf) 1,
955+
Map_comp = fn ctxt => EVERY1 [
956+
rtac ctxt (trans OF [MRBNF_Def.map_comp0_of_mrbnf mrbnf RS sym]),
957+
REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id},
958+
K (Local_Defs.unfold0_tac ctxt @{thms id_o o_id}),
959+
rtac ctxt refl
960+
],
961+
Supp_Map = map (fn _ => fn ctxt => EVERY1 [
962+
resolve_tac ctxt (MRBNF_Def.set_map_of_mrbnf mrbnf),
963+
REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id}
964+
]) lsets,
965+
Supp_bd = map (fn _ => fn ctxt => resolve_tac ctxt (MRBNF_Def.set_bd_of_mrbnf mrbnf) 1) lsets,
940966
Map_cong = fn ctxt => EVERY1 [
941-
rtac ctxt (BNF_Def.map_cong0_of_bnf bnf),
942-
REPEAT_DETERM o Goal.assume_rule_tac ctxt
967+
rtac ctxt (MRBNF_Def.map_cong0_of_mrbnf mrbnf),
968+
REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id},
969+
REPEAT_DETERM o (rtac ctxt refl ORELSE' Goal.assume_rule_tac ctxt)
943970
]
944971
},
945-
Map_Sb = fn ctxt => Local_Defs.unfold0_tac ctxt @{thms id_o o_id} THEN rtac ctxt refl 1,
946-
Supp_Sb = replicate n (fn ctxt => Local_Defs.unfold0_tac ctxt @{thms id_apply} THEN rtac ctxt refl 1),
947-
Map_Vrs = []
948-
}],
949-
bd_infinite_regular_card_order = fn ctxt => EVERY1 [
950-
rtac ctxt @{thm infinite_regular_card_order.intro},
951-
rtac ctxt (BNF_Def.bd_card_order_of_bnf bnf),
952-
rtac ctxt (BNF_Def.bd_cinfinite_of_bnf bnf),
953-
rtac ctxt (BNF_Def.bd_regularCard_of_bnf bnf)
954-
],
972+
Map_Sb = fn ctxt => EVERY1 [
973+
K (Local_Defs.unfold0_tac ctxt @{thms id_o o_id}),
974+
rtac ctxt refl ORELSE' EVERY' [
975+
rtac ctxt (trans OF [MRBNF_Def.map_comp0_of_mrbnf mrbnf RS sym]),
976+
REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_id_bound bij_id}),
977+
rtac ctxt sym,
978+
rtac ctxt (trans OF [MRBNF_Def.map_comp0_of_mrbnf mrbnf RS sym]),
979+
REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_id_bound bij_id}),
980+
K (Local_Defs.unfold0_tac ctxt @{thms id_o o_id}),
981+
rtac ctxt refl
982+
]
983+
],
984+
Supp_Sb = map (fn _ => fn ctxt => EVERY1 [
985+
K (Local_Defs.unfold0_tac ctxt @{thms id_apply}),
986+
rtac ctxt refl ORELSE' EVERY' [
987+
rtac ctxt trans,
988+
resolve_tac ctxt (MRBNF_Def.set_map_of_mrbnf mrbnf),
989+
REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_id_bound bij_id}),
990+
rtac ctxt @{thm image_id}
991+
]
992+
]) lsets,
993+
Map_Vrs = map (fn _ => fn ctxt => EVERY1 [
994+
rtac ctxt trans,
995+
resolve_tac ctxt (MRBNF_Def.set_map_of_mrbnf mrbnf),
996+
REPEAT_DETERM o resolve_tac ctxt @{thms bij_id supp_id_bound},
997+
rtac ctxt @{thm image_id}
998+
]) fsets
999+
}) Map],
1000+
bd_infinite_regular_card_order = fn ctxt => rtac ctxt (MRBNF_Def.bd_infinite_regular_card_order_of_mrbnf mrbnf) 1,
9551001
SSupp_eq = [[]],
9561002
tacs = [{
957-
Sb_Inj = fn ctxt => rtac ctxt refl 1,
1003+
Sb_Inj = fn ctxt => resolve_tac ctxt [refl, MRBNF_Def.map_id0_of_mrbnf mrbnf] 1,
9581004
Sb_comp_Injs = [],
959-
Sb_comp = fn ctxt => rtac ctxt @{thm id_o} 1,
960-
Vrs_bds = [],
1005+
Sb_comp = fn ctxt => EVERY1 [
1006+
TRY o EVERY' [
1007+
rtac ctxt (trans OF [MRBNF_Def.map_comp0_of_mrbnf mrbnf RS sym]),
1008+
REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_id_bound bij_id})
1009+
],
1010+
K (Local_Defs.unfold0_tac ctxt @{thms id_o o_id}),
1011+
rtac ctxt refl
1012+
],
1013+
Vrs_bds = map (fn _ => fn ctxt => resolve_tac ctxt (MRBNF_Def.set_bd_of_mrbnf mrbnf) 1) fsets,
9611014
Vrs_Injs = [],
962-
Vrs_Sbs = [],
963-
Sb_cong = fn ctxt => rtac ctxt refl 1
1015+
Vrs_Sbs = map (fn _ => fn ctxt => EVERY1 [
1016+
resolve_tac ctxt (MRBNF_Def.set_map_of_mrbnf mrbnf),
1017+
REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_id_bound bij_id})
1018+
]) fsets,
1019+
Sb_cong = fn ctxt => rtac ctxt refl 1 ORELSE EVERY1 [
1020+
rtac ctxt (MRBNF_Def.map_cong0_of_mrbnf mrbnf),
1021+
REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_id_bound bij_id}),
1022+
REPEAT_DETERM o (rtac ctxt refl ORELSE' Goal.assume_rule_tac ctxt)
1023+
]
9641024
}]
9651025
} lthy) end;
9661026

967-
fun register_bnf_as_pbmv_monad name lthy =
1027+
fun register_mrbnf_as_pbmv_monad name lthy =
9681028
let
969-
val bnf = the (BNF_Def.bnf_of lthy name);
970-
val (bmv, lthy) = pbmv_monad_of_bnf bnf lthy;
1029+
val mrbnf = the (MRBNF_Def.mrbnf_of lthy name);
1030+
val (bmv, lthy) = pbmv_monad_of_mrbnf mrbnf lthy;
9711031
val lthy = register_pbmv_monad name bmv lthy;
9721032
in lthy end
9731033

@@ -980,7 +1040,6 @@ fun slice_bmv_monad n bmv =
9801040
let
9811041
fun f xs = nth xs n;
9821042
val Sb = f (Sbs_of_bmv_monad bmv);
983-
val vars = map TFree (Term.add_tfrees Sb []);
9841043
in BMV {
9851044
ops = [f (ops_of_bmv_monad bmv)],
9861045
var_class = var_class_of_bmv_monad bmv,
@@ -1230,8 +1289,9 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : (bmv_monad, typ) eit
12301289
),
12311290
K (prefer_tac 2),
12321291
rtac ctxt (#Map_cong (#axioms param)),
1233-
K (Local_Defs.unfold0_tac ctxt (#Supp_Sb param)),
12341292
EVERY' (map (fn Inr _ => rtac ctxt refl | Inl inner => EVERY' [
1293+
EqSubst.eqsubst_asm_tac ctxt [0] (#Supp_Sb param),
1294+
REPEAT_DETERM o resolve_tac ctxt prems,
12351295
resolve_tac ctxt (map #Sb_cong (axioms_of_bmv_monad inner)),
12361296
REPEAT_DETERM o resolve_tac ctxt (take (2 * length Injs) prems),
12371297
REPEAT_DETERM o (rtac ctxt refl ORELSE' EVERY' [

‎Tools/mrsbnf_comp.ML‎

Lines changed: 111 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,122 @@
11
signature MRSBNF_COMP = sig
22

3-
val id_mrsbnf: MRSBNF_Def.mrsbnf
4-
5-
val mrsbnf_of_typ: bool -> BNF_Def.inline_policy -> (theory -> BNF_Def.fact_policy)
6-
-> (binding -> binding) -> ((string * sort) * MRBNF_Def.var_type) list -> typ
7-
-> (thm list * local_theory) -> MRSBNF_Def.mrsbnf option * (thm list * local_theory)
3+
val mrsbnf_of_typ: bool -> (theory -> BNF_Def.fact_policy)
4+
-> (binding -> binding) -> (string * sort) list -> ((string * sort) * MRBNF_Def.var_type) list
5+
-> typ -> ((MRBNF_Comp.comp_cache * MRBNF_Comp.unfold_set) * local_theory)
6+
-> ((MRSBNF_Def.mrsbnf, MRBNF_Def.mrbnf) MRBNF_Util.either * (typ list * typ list))
7+
* ((MRBNF_Comp.comp_cache * MRBNF_Comp.unfold_set) * local_theory)
88

99
end
1010

1111
structure MRSBNF_Comp : MRSBNF_COMP = struct
1212

13-
val id_mrsbnf = the (MRSBNF_Def.mrsbnf_of @{context} "BNF_Composition.ID");
13+
open MRBNF_Util
14+
15+
fun mrsbnf_of lthy s = case MRSBNF_Def.mrsbnf_of lthy s of
16+
SOME mrsbnf => SOME (Inl mrsbnf, lthy)
17+
| NONE => (case MRBNF_Def.mrbnf_of lthy s of
18+
SOME mrbnf => SOME (Inr mrbnf, lthy)
19+
| NONE => Option.map (fn bnf =>
20+
apfst Inr (MRBNF_Def.register_bnf_as_mrbnf NONE bnf lthy)
21+
) (BNF_Def.bnf_of lthy s)
22+
)
1423

15-
fun mrsbnf_of_typ _ _ _ _ var_types (TFree (x, _)) accum = (case AList.lookup ((op=) o apsnd fst) var_types x of
16-
SOME MRBNF_Def.Free_Var => (SOME id_mrsbnf, accum)
17-
| _ => (SOME id_mrsbnf, accum))
24+
fun is_Inl (Inl _) = true
25+
| is_Inl _ = false
26+
27+
fun mrsbnf_of_typ _ _ qualify Ds0 var_types (T as TFree T') accum =
28+
(if member (op =) Ds0 T' then ((Inr MRBNF_Comp.DEADID_mrbnf, ([T], [])), accum) else
29+
(case map_filter (fn a => if fst a = T' then SOME (snd a) else NONE) var_types of
30+
[] => ((Inr MRBNF_Comp.ID_mrbnf, ([], [T])), accum)
31+
| [MRBNF_Def.Dead_Var] => error "var_types may only be Live, Free or Bound, use Ds0 for deads"
32+
| [var_type] =>
33+
let
34+
val qualify' = qualify o Binding.suffix_name ("_" ^ fst T')
35+
val (ID', accum') = MRBNF_Comp.demote_mrbnf qualify' [var_type] MRBNF_Comp.ID_mrbnf accum
36+
in ((Inr ID', ([], [T])), accum') end
37+
| _ => error "Same variable appears twice in var_types"
38+
)
39+
)
1840
| mrsbnf_of_typ _ _ _ _ _ (TVar _) _ = error "unexpected schematic variable"
19-
| mrsbnf_of_typ optim const_policy inline_policy qualify var_types (T as Type (n, Ts)) (accum, lthy) =
20-
let
21-
22-
in error "bar" end;
41+
| mrsbnf_of_typ optim const_policy qualify' Ds0 var_types (T as Type (n, Ts)) (accum, lthy) = (case mrsbnf_of lthy n of
42+
NONE => ((Inr MRBNF_Comp.DEADID_mrbnf, ([T], [])), (accum, lthy))
43+
| SOME (outer, lthy) =>
44+
if optim andalso forall is_TFree Ts then
45+
let
46+
val mrbnf = case outer of
47+
Inl mrsbnf => hd (MRSBNF_Def.mrbnfs_of_mrsbnf mrsbnf)
48+
| Inr mrbnf => mrbnf;
49+
val mrbnf' = MRBNF_Def.morph_mrbnf (MRBNF_Util.subst_typ_morphism (
50+
snd (dest_Type (MRBNF_Def.T_of_mrbnf mrbnf)) ~~ Ts
51+
)) mrbnf;
52+
val deads = MRBNF_Def.deads_of_mrbnf mrbnf';
53+
val _ = case filter (Option.isSome o AList.lookup (op=) var_types o dest_TFree) deads of
54+
T'::_ => error ("Variable " ^ Syntax.string_of_typ lthy T' ^ " is forced dead by type " ^ Syntax.string_of_typ lthy T ^ " but was specified as other usage")
55+
| [] => ()
56+
val Ts' = subtract (op=) deads Ts;
57+
val _ = @{print} Ts'
58+
val var_types = map (AList.lookup (op=) var_types o dest_TFree) Ts';
59+
val var_types = @{map 3} (fn req => fn var_type => fn T => if member (op=) Ds0 (dest_TFree T) then
60+
MRBNF_Def.Dead_Var else the_default var_type req
61+
) var_types (MRBNF_Def.var_types_of_mrbnf mrbnf) Ts';
62+
63+
val (mrsbnf, accum) = if MRBNF_Def.var_types_of_mrbnf mrbnf = var_types then
64+
(outer, (accum, lthy))
65+
else case outer of
66+
Inl mrsbnf => error "TODO: Demote MRSBNF"
67+
| Inr mrbnf => apfst Inr (MRBNF_Comp.demote_mrbnf qualify' var_types mrbnf (accum, lthy));
68+
in ((mrsbnf, (inter (op=) Ts (deads @ map TFree Ds0), subtract (op=) (map TFree Ds0) Ts')), accum) end
69+
else
70+
let
71+
val name = Long_Name.base_name n;
72+
fun qualify i =
73+
let val namei = name ^ nonzero_string_of_int i;
74+
in qualify' o Binding.qualify true namei end;
75+
val mrbnf = case outer of
76+
Inl mrsbnf => hd (MRSBNF_Def.mrbnfs_of_mrsbnf mrsbnf)
77+
| Inr mrbnf => mrbnf
78+
79+
val odead = MRBNF_Def.dead_of_mrbnf mrbnf;
80+
val olive = MRBNF_Def.live_of_mrbnf mrbnf;
81+
val obound = MRBNF_Def.bound_of_mrbnf mrbnf;
82+
val ofree = MRBNF_Def.free_of_mrbnf mrbnf;
83+
val Ds = map (fn i => TFree (string_of_int i, [])) (1 upto odead);
84+
val Us = snd (Term.dest_Type (MRBNF_Def.mk_T_of_mrbnf Ds (replicate olive dummyT) (replicate obound dummyT) (replicate ofree dummyT) mrbnf));
85+
val oDs_pos = map (fn x => find_index (fn y => x = y) Us) Ds
86+
|> filter (fn x => x >= 0);
87+
val oAs = map (fn (T, var_type) => case var_type of
88+
MRBNF_Def.Live_Var => NONE | _ => SOME T
89+
) (Ts ~~ MRBNF_Def.var_types_of_mrbnf mrbnf)
90+
val oDs = map (nth Ts) oDs_pos;
91+
val ofree_bound_pos = map_filter I (map_index (fn (i, x) => case x of
92+
SOME _ => SOME i | NONE => NONE
93+
) oAs)
94+
val Ts' = map (nth Ts) (subtract (op =) (oDs_pos @ ofree_bound_pos) (0 upto length Ts - 1));
95+
96+
val ((inners, (Dss, Ass)), (accum, lthy)) =
97+
apfst (apsnd split_list o split_list) (@{fold_map 2}
98+
(fn i => mrsbnf_of_typ optim const_policy (qualify i) Ds0 var_types)
99+
(if length Ts' = 1 then [0] else 1 upto length Ts') Ts' (accum, lthy));
100+
101+
val _ = @{print} T
102+
val Xs = rev (Term.add_tfreesT T []);
103+
val Xs' = map (swap o `(the_default MRBNF_Def.Live_Var o AList.lookup (op=) var_types)) Xs
104+
in if exists is_Inl inners orelse is_Inl outer then
105+
let
106+
val (outer', lthy) = case outer of
107+
Inl mrsbnf => (mrsbnf, lthy)
108+
| Inr mrbnf => MRSBNF_Def.mrsbnf_of_mrbnf mrbnf lthy
109+
val (inners', lthy) = fold_map (fn Inl mrsbnf => (fn lthy => (mrsbnf, lthy))
110+
| Inr mrbnf => MRSBNF_Def.mrsbnf_of_mrbnf mrbnf
111+
) inners lthy;
112+
val _ = @{print} (outer' :: inners')
113+
val _ = ()
114+
in error "TODO: compose mrsbnfs" end
115+
else
116+
apfst (apfst Inr) (MRBNF_Comp.compose_mrbnf MRBNF_Def.Smart_Inline qualify (distinct (op=) o flat)
117+
mrbnf (map (fn Inr x => x | _ => error "impossible") inners) oDs Dss oAs Ass Xs' (accum, lthy)
118+
)
119+
end
120+
);
23121

24122
end

0 commit comments

Comments
 (0)