Skip to content

Commit 8551faa

Browse files
jvanbrueggejvanbruegge
committed
Fully support passive position (incl bound and live)
1 parent 97f6a2b commit 8551faa

File tree

8 files changed

+1045
-350
lines changed

8 files changed

+1045
-350
lines changed

‎Tools/bmv_monad_def.ML‎

Lines changed: 43 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -120,7 +120,7 @@ signature BMV_MONAD_DEF = sig
120120
-> { frees: typ list, deads: typ list, lives: typ list } option list -> local_theory
121121
-> (bmv_monad * thm list) * local_theory
122122

123-
val seal_bmv_monad: (binding -> binding) -> thm list -> binding -> typ list -> bmv_monad
123+
val seal_bmv_monad: (binding -> binding) -> thm list -> binding -> (var_type * typ) list -> bmv_monad
124124
-> (string * Typedef.info) option -> local_theory
125125
-> (bmv_monad * thm list * thm list * (string * Typedef.info)) * local_theory
126126
end
@@ -505,7 +505,7 @@ fun mk_bmv_monad_axioms ops consts bmv_ops lthy =
505505
) (List.find (curry (op=) (body_type (fastype_of RVr)) o body_type o fastype_of) RVrs) end
506506
) Vrs rhos in fold_rev Logic.all (fs @ rhos @ [x]) (
507507
fold_rev (curry Logic.mk_implies) small_prems (mk_Trueprop_eq (
508-
RVr $ (Term.list_comb (Sb, fs @ rhos) $ x), foldr1 mk_Un ((mk_image f $ (RVr $ x)) :: UNs)
508+
RVr $ (Term.list_comb (Sb, fs @ rhos) $ x), foldl1 mk_Un ((mk_image f $ (RVr $ x)) :: UNs)
509509
))
510510
) end
511511
) fs RVrs @ map2 (fn Vr => fn Inj =>
@@ -2106,17 +2106,30 @@ fun seal_bmv_monad qualify unfolds name tys bmv info_opt lthy =
21062106
val rep_T = leader ops_of_bmv_monad bmv;
21072107
val ((T_name, info), lthy) = (case info_opt of
21082108
SOME info => (info, lthy)
2109-
| NONE => BNF_Util.typedef (name, map dest_TFree tys, NoSyn)
2109+
| NONE => BNF_Util.typedef (name, map (dest_TFree o snd) tys, NoSyn)
21102110
(HOLogic.mk_UNIV rep_T) NONE (fn ctxt => rtac ctxt @{thm UNIV_witness} 1) lthy)
21112111

21122112
val T = #abs_type (fst info);
21132113
val abs = Const (#Abs_name (fst info), rep_T --> #abs_type (fst info));
21142114
val rep = Const (#Rep_name (fst info), #abs_type (fst info) --> rep_T);
21152115

2116+
val frees = map_filter (fn (Free_Var, a) => SOME a | _ => NONE) tys;
2117+
val lives = map_filter (fn (Live_Var, a) => SOME a | _ => NONE) tys;
2118+
val deads = map_filter (fn (Dead_Var, a) => SOME a | _ => NONE) tys;
2119+
val lives' = map (the o AList.lookup (op=) (leader lives_of_bmv_monad bmv ~~ leader lives'_of_bmv_monad bmv)) lives;
2120+
2121+
val (ifrees, rfrees) = partition (
2122+
member (op=) (map (domain_type o fastype_of) (leader Injs_of_bmv_monad bmv))
2123+
) frees;
2124+
21162125
val (((fs, rhos), gs), _) = lthy
2117-
|> mk_Frees "f" (map ((fn a => a --> a) o HOLogic.dest_setT o body_type o fastype_of) (leader RVrs_of_bmv_monad bmv))
2126+
|> mk_Frees "f" (map (fn a => a --> a) rfrees)
21182127
||>> mk_Frees "\<rho>" (map ((fn T' => if body_type T' = rep_T then domain_type T' --> T else T') o fastype_of) (leader Injs_of_bmv_monad bmv))
2119-
||>> mk_Frees "g" (the_default [] (Option.map (fst o split_last o binder_types o fastype_of) (leader Maps_of_bmv_monad bmv)))
2128+
||>> mk_Frees "g" (map2 (curry (op-->)) lives lives')
2129+
2130+
val rep_fs = map (fn RVrs => the (List.find (fn f =>
2131+
domain_type (fastype_of f) = HOLogic.dest_setT (range_type (fastype_of RVrs))
2132+
) fs)) (leader RVrs_of_bmv_monad bmv);
21202133

21212134
val mk_def_t = mk_def_t false Binding.empty qualify
21222135
val mk_defs_t = mk_defs_t false Binding.empty qualify
@@ -2127,9 +2140,12 @@ fun seal_bmv_monad qualify unfolds name tys bmv info_opt lthy =
21272140
val (((((Sb, RVrs), Injs), Vrs), extra_Vrs), lthy) = lthy
21282141
|> mk_def_t (mk_name "Sb") 0 (fold_rev (Term.absfree o dest_Free) (fs @ rhos) (
21292142
HOLogic.mk_comp (HOLogic.mk_comp (abs, Term.list_comb (leader Sbs_of_bmv_monad bmv,
2130-
fs @ map (fn rho => if body_type (fastype_of rho) = T then HOLogic.mk_comp (rep, rho) else rho) rhos
2143+
rep_fs @ map (fn rho => if body_type (fastype_of rho) = T then HOLogic.mk_comp (rep, rho) else rho) rhos
21312144
)), rep)))
2132-
||>> mk_defs_t (mk_name "RVrs") 0 (map (fn RVrs => HOLogic.mk_comp (RVrs, rep)) (leader RVrs_of_bmv_monad bmv))
2145+
||>> mk_defs_t (mk_name "RVrs") 0 (map (fn free => case List.find (fn RVrs => HOLogic.dest_setT (range_type (fastype_of RVrs)) = free) (leader RVrs_of_bmv_monad bmv) of
2146+
SOME RVrs => HOLogic.mk_comp (RVrs, rep)
2147+
| NONE => Term.abs ("_", T) (mk_bot free)
2148+
) rfrees)
21332149
||>> mk_defs_t (mk_name "Inj") 0 (map_filter (fn Inj =>
21342150
if body_type (fastype_of Inj) = rep_T then SOME (HOLogic.mk_comp (abs, Inj)) else NONE
21352151
) (leader Injs_of_bmv_monad bmv))
@@ -2142,9 +2158,13 @@ fun seal_bmv_monad qualify unfolds name tys bmv info_opt lthy =
21422158
| SOME Map =>
21432159
lthy
21442160
|> apfst SOME o mk_def_t (mk_name "Map") 0 (fold_rev (Term.absfree o dest_Free) gs (
2145-
HOLogic.mk_comp (HOLogic.mk_comp (subst abs, Term.list_comb (Map, gs)), rep)
2161+
HOLogic.mk_comp (HOLogic.mk_comp (subst abs, Term.list_comb (Map, map (fn live =>
2162+
the (List.find (fn g => domain_type (fastype_of g) = live) gs)
2163+
) (leader lives_of_bmv_monad bmv))), rep)
21462164
))
2147-
||>> apfst SOME o mk_defs_t (mk_name "Supp") 0 (map (fn Supp => HOLogic.mk_comp (Supp, rep)) (the (leader Supps_of_bmv_monad bmv)))
2165+
||>> apfst SOME o mk_defs_t (mk_name "Supp") 0 (map (fn live => HOLogic.mk_comp (
2166+
the (List.find (fn Supp => HOLogic.dest_setT (range_type (fastype_of Supp)) = live) (the (leader Supps_of_bmv_monad bmv))),
2167+
rep)) lives)
21482168

21492169
val (lthy, old_lthy) = `Local_Theory.end_nested lthy;
21502170
val phi = Proof_Context.export_morphism old_lthy lthy;
@@ -2188,10 +2208,10 @@ fun seal_bmv_monad qualify unfolds name tys bmv info_opt lthy =
21882208
bmv_ops = map_filter (fn i => if i = leader_of_bmv_monad bmv then NONE else SOME (unsafe_slice_bmv_monad i bmv)) (0 upto length (ops_of_bmv_monad bmv) - 1),
21892209
bd_infinite_regular_card_order = fn ctxt => rtac ctxt (bd_infinite_regular_card_order_of_bmv_monad bmv) 1,
21902210
var_class = var_class_of_bmv_monad bmv,
2191-
frees = [leader frees_of_bmv_monad bmv],
2192-
lives = [leader lives_of_bmv_monad bmv],
2193-
lives' = [leader lives'_of_bmv_monad bmv],
2194-
deads = [map TFree (rev (fold Term.add_tfreesT (leader deads_of_bmv_monad bmv) []))],
2211+
frees = [frees],
2212+
lives = [lives],
2213+
lives' = [lives'],
2214+
deads = [deads],
21952215
consts = consts,
21962216
leader = 0,
21972217
params = [Option.map (fn Supps => {
@@ -2255,13 +2275,13 @@ fun seal_bmv_monad qualify unfolds name tys bmv info_opt lthy =
22552275
rtac ctxt refl
22562276
]) Supps,
22572277
Vrs_Map = map (fn _ => fn ctxt => EVERY1 [
2258-
K (Local_Defs.unfold0_tac ctxt ([
2278+
K (Local_Defs.unfold0_tac ctxt (@{thms image_empty} @ [
22592279
snd (the Map_opt), #Abs_inverse (snd info) OF @{thms UNIV_I},
22602280
infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt rep)] @{thm comp_apply},
22612281
infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt (subst rep))] @{thm comp_apply},
22622282
infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt (subst abs))] @{thm comp_apply}
22632283
] @ map snd Vrs @ map snd RVrs)),
2264-
resolve_tac ctxt (#Vrs_Map (the params))
2284+
resolve_tac ctxt (@{thms refl} @ #Vrs_Map (the params))
22652285
]) (RVrs @ Vrs),
22662286
Map_Injs = map_filter (fn Inj => if body_type (fastype_of Inj) <> T then NONE else
22672287
SOME (fn ctxt => EVERY1 [
@@ -2308,7 +2328,8 @@ fun seal_bmv_monad qualify unfolds name tys bmv info_opt lthy =
23082328
],
23092329
Vrs_bds = map (K (fn ctxt => EVERY1 [
23102330
K (Local_Defs.unfold0_tac ctxt (@{thms comp_def} @ map snd Vrs @ map snd RVrs)),
2311-
resolve_tac ctxt (#Vrs_bds axioms)
2331+
resolve_tac ctxt (@{thms Cinfinite_gt_empty} @ #Vrs_bds axioms),
2332+
TRY o rtac ctxt (@{thm infinite_regular_card_order.Cinfinite} OF [bd_infinite_regular_card_order_of_bmv_monad bmv])
23122333
])) (RVrs @ Vrs),
23132334
Vrs_Injss = map (K (map_filter (fn Inj => if body_type (fastype_of Inj) <> T then NONE else
23142335
SOME (fn ctxt => EVERY1 [
@@ -2317,15 +2338,17 @@ fun seal_bmv_monad qualify unfolds name tys bmv info_opt lthy =
23172338
])
23182339
) Injs)) (RVrs @ Vrs @ extra_Vrs),
23192340
Vrs_Sbs = map (K (fn ctxt => EVERY1 [
2320-
K (Local_Defs.unfold0_tac ctxt ([
2341+
K (Local_Defs.unfold0_tac ctxt (@{thms image_empty} @ [
23212342
snd Sb, @{thm SSupp_type_copy} OF [copy], @{thm IImsupp_type_copy} OF [copy],
23222343
#Abs_inverse (snd info) OF @{thms UNIV_I},
23232344
infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt rep)] @{thm comp_apply},
23242345
infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt abs)] @{thm comp_apply}
23252346
] @ defs)),
2326-
rtac ctxt trans,
2327-
resolve_tac ctxt (#Vrs_Sbs axioms) THEN_ALL_NEW assume_tac ctxt,
2328-
K (Local_Defs.unfold0_tac ctxt @{thms comp_def}),
2347+
TRY o EVERY' [
2348+
rtac ctxt trans,
2349+
resolve_tac ctxt (#Vrs_Sbs axioms) THEN_ALL_NEW assume_tac ctxt,
2350+
K (Local_Defs.unfold0_tac ctxt @{thms comp_def})
2351+
],
23292352
rtac ctxt refl
23302353
])) (RVrs @ Vrs),
23312354
Sb_cong = fn ctxt => EVERY1 [

‎Tools/mrbnf_sugar.ML‎

Lines changed: 10 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -876,6 +876,7 @@ fun create_binder_datatype co (spec : spec) lthy =
876876
K (Local_Defs.unfold0_tac ctxt (
877877
@{thms comp_def sum.set_map UN_empty2 Un_empty_right Un_empty_left UN_singleton map_sum.simps map_prod_simp id_apply sum.inject}
878878
@ MRBNF_Def.set_defs_of_mrbnf pre_mrbnf
879+
@ [MRBNF_Def.map_def_of_mrbnf pre_mrbnf]
879880
@ BMV_Monad_Def.unfolds_of_bmv_monad bmv
880881
@ BMV_Monad_Def.defs_of_bmv_monad bmv
881882
@ [#Abs_inverse (snd info) OF @{thms UNIV_I}, #Abs_inject (snd info) OF @{thms UNIV_I UNIV_I}]
@@ -1121,7 +1122,6 @@ fun create_binder_datatype co (spec : spec) lthy =
11211122

11221123
val (lthy, tvsubst_opt) = if not (null (map_filter I (#etas tvsubst_model))) andalso not co then
11231124
let
1124-
val _ = @{print} "before tvsubst"
11251125
val recursor_result = #recursor_result (the vvsubst_res_opt);
11261126
val rec_mrbnf = #rec_mrbnf (the vvsubst_res_opt);
11271127
val vvsubst_res = #vvsubst_res (the vvsubst_res_opt);
@@ -1130,8 +1130,6 @@ fun create_binder_datatype co (spec : spec) lthy =
11301130
rec_mrbnf (#vvsubst_ctor vvsubst_res) (#vvsubst_permute vvsubst_res) (#pset_ctors (#vvsubst_res (the vvsubst_res_opt))) (#tvsubst_b spec)
11311131
(#etas tvsubst_model) (#QREC_fixed recursor_result) lthy;
11321132

1133-
val _ = @{print} "after tvsubst"
1134-
11351133
val lthy = BMV_Monad_Def.register_pbmv_monad (fst (dest_Type qT))
11361134
(MRSBNF_Def.bmv_monad_of_mrsbnf (#mrsbnf tvsubst_res)) lthy;
11371135
val lthy = MRSBNF_Def.register_mrsbnf (fst (dest_Type qT)) (#mrsbnf tvsubst_res) lthy;
@@ -1153,24 +1151,25 @@ fun create_binder_datatype co (spec : spec) lthy =
11531151
val phi = MRBNF_Util.subst_typ_morphism (map (fn (n, (s, T)) => (TVar (n, s), T)) (Vartab.dest tyenv));
11541152
in BMV_Monad_Def.morph_bmv_monad phi bmv end
11551153
val Injs = hd (BMV_Monad_Def.Injs_of_bmv_monad bmv);
1154+
val RVrs = hd (BMV_Monad_Def.RVrs_of_bmv_monad bmv);
11561155

1157-
val (fs, _) = lthy
1158-
|> mk_Frees "f" (map fastype_of Injs);
1156+
val ((fs, rhos), _) = lthy
1157+
|> mk_Frees "f" (map ((fn a => a --> a) o HOLogic.dest_setT o range_type o fastype_of) RVrs)
1158+
||>> mk_Frees "\<rho>" (map fastype_of Injs);
11591159
val Sbs = BMV_Monad_Def.Sbs_of_bmv_monad bmv;
11601160

11611161
val small_premss = map (map HOLogic.dest_Trueprop) (
1162-
BMV_Monad_Def.mk_small_prems_of_bmv_monad bmv 0 [] fs
1162+
BMV_Monad_Def.mk_small_prems_of_bmv_monad bmv 0 fs rhos
11631163
);
11641164

11651165
fun mk_supp_bound f = if Term.is_TFree (body_type (fastype_of f)) then SOME [MRBNF_Util.mk_supp_bound f] else
11661166
List.find (fn xs => Term.exists_subterm (curry (op=) f) (hd xs)) small_premss;
11671167

1168-
fun mk_imsupp h _ =
1168+
fun mk_imsupp h _ = if Term.is_TFree (body_type (fastype_of h)) then SOME [MRBNF_Util.mk_imsupp h] else
11691169
let
11701170
val Inj = the (List.find (fn Inj => fastype_of Inj = fastype_of h) Injs);
1171-
val Vrs = nth (BMV_Monad_Def.Vrs_of_bmv_monad bmv) (
1172-
find_index (curry (op=) (body_type (fastype_of Inj))) (BMV_Monad_Def.ops_of_bmv_monad bmv)
1173-
);
1171+
val idx = find_index (curry (op=) (body_type (fastype_of Inj))) (BMV_Monad_Def.ops_of_bmv_monad bmv);
1172+
val Vrs = nth (BMV_Monad_Def.RVrs_of_bmv_monad bmv) idx @ nth (BMV_Monad_Def.Vrs_of_bmv_monad bmv) idx;
11741173
val IImsupps = (mk_SSupp Inj $ h) :: map (fn Vrs => mk_IImsupp Inj Vrs $ h) Vrs;
11751174
in SOME IImsupps end
11761175

@@ -1228,7 +1227,7 @@ fun create_binder_datatype co (spec : spec) lthy =
12281227
]
12291228
];
12301229
in map (Local_Defs.unfold0 lthy bmv_unfolds) (
1231-
mk_map_simps lthy false true Sbs plives fs mk_supp_bound mk_imsupp (K []) [] (#tvsubst tvsubst_res) tac
1230+
mk_map_simps lthy false true Sbs plives (fs @ rhos) mk_supp_bound mk_imsupp (K []) [] (#tvsubst tvsubst_res) tac
12321231
) end;
12331232
in (lthy, SOME (tvsubst_res, tvsubst_simps)) end
12341233
else (lthy, NONE);

‎Tools/mrsbnf_comp.ML‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,7 @@ fun seal_mrsbnf qualify (bmv_unfolds, mrbnf_unfolds) name Xs tys mrsbnf info_opt
6161
val (lives, bounds, frees) = MRBNF_Def.deinterlace (map TFree new_tys) var_types;
6262
val bounds = map (resort_tfree_or_tvar var_class) bounds;
6363
val frees = map (resort_tfree_or_tvar var_class) frees;
64+
val new_tys = map dest_TFree (MRBNF_Def.interlace lives bounds frees var_types);
6465

6566
val rep_T = MRBNF_Def.mk_T_of_mrbnf Ds lives bounds frees mrbnf';
6667

@@ -87,9 +88,14 @@ fun seal_mrsbnf qualify (bmv_unfolds, mrbnf_unfolds) name Xs tys mrsbnf info_opt
8788
(BMV_Monad_Def.leader BMV_Monad_Def.lives'_of_bmv_monad bmv);
8889
in BMV_Monad_Def.morph_bmv_monad (MRBNF_Util.subst_typ_morphism subst) bmv end;
8990

91+
val var_types' = map (fn MRBNF_Def.Free_Var => BMV_Monad_Def.Free_Var
92+
| MRBNF_Def.Live_Var => BMV_Monad_Def.Live_Var
93+
| _ => BMV_Monad_Def.Dead_Var
94+
) var_types;
95+
9096
val ((bmv, _, bmv_defs, _), lthy) = BMV_Monad_Def.seal_bmv_monad qualify (
9197
bmv_unfolds @ #map_unfolds mrbnf_unfolds @ flat (#set_unfoldss mrbnf_unfolds)
92-
) name [] bmv (SOME info) lthy;
98+
) name (var_types' ~~ map TFree new_tys) bmv (SOME info) lthy;
9399

94100
val mrbnfs = map_index (fn (i, x) => if i = BMV_Monad_Def.leader_of_bmv_monad bmv then mrbnf else x)
95101
(MRSBNF_Def.mrbnfs_of_mrsbnf mrsbnf);
@@ -178,7 +184,7 @@ fun seal_mrsbnf qualify (bmv_unfolds, mrbnf_unfolds) name Xs tys mrsbnf info_opt
178184
K (Local_Defs.unfold0_tac ctxt @{thms comp_def}),
179185
rtac ctxt refl
180186
]
181-
])) (#set_Vrs axioms)
187+
])) frees
182188
}
183189
) (MRSBNF_Def.axioms_of_mrsbnf mrsbnf)) lthy;
184190
in ((mrsbnf, (snd (dest_Type T), absT_info)), lthy) end

0 commit comments

Comments
 (0)