diff --git a/Tools/bmv_monad_def.ML b/Tools/bmv_monad_def.ML index 8ad0b52..427c6d5 100644 --- a/Tools/bmv_monad_def.ML +++ b/Tools/bmv_monad_def.ML @@ -81,7 +81,7 @@ signature BMV_MONAD_DEF = sig val bmv_monad_def: BNF_Def.inline_policy -> (Proof.context -> BNF_Def.fact_policy) -> (binding -> binding) -> (Proof.context -> tactic) bmv_monad_model -> local_theory -> (bmv_monad * thm list) * local_theory - val compose_bmv_monad: (binding -> binding) -> bmv_monad -> bmv_monad list -> local_theory + val compose_bmv_monad: (binding -> binding) -> bmv_monad -> (bmv_monad, typ) MRBNF_Util.either list -> local_theory -> (bmv_monad * thm list) * local_theory end @@ -160,7 +160,7 @@ fun morph_bmv_monad_param phi f ({ Map, Supps, axioms, Map_Sb, Supp_Sb, Map_Vrs Supp_Sb = map f Supp_Sb, Map_Vrs = map (map (Option.map f)) Map_Vrs }: 'b bmv_monad_param; - + datatype bmv_monad = BMV of { ops: typ list, bd: term, @@ -551,7 +551,7 @@ fun define_bmv_monad_consts const_policy fact_policy qualify (model: 'a bmv_mona val (lthy, old_lthy) = `Local_Theory.end_nested lthy; val phi = Proof_Context.export_morphism old_lthy lthy; - val vars = #frees model @ #lives model @ #lives' model; + val vars = map TFree (rev (Term.add_tfreesT (nth (#ops model) (#leader model)) [])) @ #lives' model; val subst = (map (Morphism.typ phi) vars ~~ vars); val phi' = Morphism.term_morphism "bmv_monad_export" (Term.subst_atomic_types subst o Morphism.term phi) @@ -716,50 +716,75 @@ fun register_bnf_as_pbmv_monad name lthy = - does not appear in the codomain of any (=of any **other** SOp) Injection, *) -fun compose_bmv_monad qualify (outer : bmv_monad) (inners : bmv_monad list) lthy = +fun compose_bmv_monad qualify (outer : bmv_monad) (inners : (bmv_monad, typ) either list) lthy = let val _ = if length (lives_of_bmv_monad outer) <> length inners then error "Outer needs exactly as many lives as there are inners" else () + val filter_bmvs = map_filter (fn Inl x => SOME x | _ => NONE); + + val frees = fold (fn a => + let val (n, s) = dest_TFree a + in Symtab.map_default (n, s) (curry (Sign.inter_sort (Proof_Context.theory_of lthy)) s) end + ) (frees_of_bmv_monad outer @ maps frees_of_bmv_monad (filter_bmvs inners)) Symtab.empty; + + fun mk_sign_morph bmv = + morph_bmv_monad (MRBNF_Util.subst_typ_morphism (map (fn a => + let val (n, _) = dest_TFree a; + in (a, TFree (n, the (Symtab.lookup frees n))) end + ) (frees_of_bmv_monad bmv))) bmv; + fun mk_T_morph T = + let val vars = Term.add_tfreesT T []; + in Term.typ_subst_atomic (map (fn x => + (TFree x, the_default (TFree x) (Option.map (TFree o pair (fst x)) (Symtab.lookup frees (fst x)))) + ) vars) T end + val outer = mk_sign_morph outer; + val inners = map (map_sum mk_sign_morph mk_T_morph) inners; + val bmvs = Typtab.make_distinct (flat (map (fn bmv => (#ops bmv ~~ ((#params bmv) ~~ (#Injs bmv) ~~ (#Sbs bmv) ~~ (#Vrs bmv) ~~ map SOME (#axioms bmv) ~~ replicate (length (#Sbs bmv)) (SOME bmv)) - )) (map Rep_bmv inners))); + )) (map_filter (fn Inl bmv => SOME (Rep_bmv bmv) | Inr _ => NONE) inners))); val outer_ops' = map (fn T => if Typtab.defined bmvs T then NONE else SOME T) ( - map (Term.typ_subst_atomic (lives_of_bmv_monad outer ~~ map (fn bmv => - nth (ops_of_bmv_monad bmv) (leader_of_bmv_monad bmv) + map (Term.typ_subst_atomic (lives_of_bmv_monad outer ~~ map ( + fn Inl bmv => nth (ops_of_bmv_monad bmv) (leader_of_bmv_monad bmv) + | Inr T => T ) inners)) (ops_of_bmv_monad outer) ); val ((Sbs, Injs), Vrs) = apfst split_list (split_list (@{map 5} (fn NONE => K (K (K (K ((NONE, NONE), NONE)))) | SOME T => (fn NONE => K (K (K ((NONE, NONE), NONE))) | SOME param => fn Sb => fn Injs => fn Vrs => let - val ((Sbs, Ts), (Injss, Vrsss)) = apfst split_list (apsnd split_list (split_list (map (fn bmv => + val ((Sbs, Ts), (Injss, Vrsss)) = apfst split_list (apsnd split_list (split_list (map (fn Inl bmv => let fun pick xs = nth xs (leader_of_bmv_monad bmv) in ( - (pick (Sbs_of_bmv_monad bmv), pick (ops_of_bmv_monad bmv)), - (pick (Injs_of_bmv_monad bmv), pick (Vrs_of_bmv_monad bmv)) + (SOME (pick (Sbs_of_bmv_monad bmv)), pick (ops_of_bmv_monad bmv)), + (SOME (pick (Injs_of_bmv_monad bmv)), SOME (pick (Vrs_of_bmv_monad bmv))) ) end + | Inr T => ((NONE, T), (NONE, NONE)) ) inners))); val subst = (lives_of_bmv_monad outer @ lives'_of_bmv_monad outer) ~~ (Ts @ Ts); - val Injs' = distinct ((op=) o apply2 fastype_of) (Injs @ flat Injss); + val Injs' = distinct ((op=) o apply2 fastype_of) (Injs @ flat (map_filter I Injss)); val ((fs, x), _) = lthy |> mk_Frees "f" (map fastype_of Injs') ||>> apfst hd o mk_Frees "x" [T]; - val Vrs' = @{fold 4} (fn i => fn inner => @{fold 2} (fn Inj => fn Vrs => fn tab => - case Typtab.lookup tab (fastype_of Inj) of - NONE => tab - | SOME inner_tab => - let val inner_tab' = @{fold 2} (fn NONE => K I | SOME Vrs => fn free => - Typtab.map_default (free, [(i, Vrs)]) (cons (i, Vrs)) - ) Vrs (frees_of_bmv_monad inner) inner_tab; - in Typtab.update (fastype_of Inj, inner_tab') tab end - )) (0 upto length inners) (outer :: inners) (Injs :: Injss) (Vrs :: Vrsss) (Typtab.make (map (rpair Typtab.empty o fastype_of) Injs')); + val Vrs' = @{fold 4} (fn i => fn inner => fn Injs => fn Vrss => fn tab => case inner of + Inr _ => tab + | Inl inner => @{fold 2} (fn Inj => fn Vrs => fn tab => + case Typtab.lookup tab (fastype_of Inj) of + NONE => tab + | SOME inner_tab => + let val inner_tab' = @{fold 2} (fn NONE => K I | SOME Vrs => fn free => + Typtab.map_default (free, [(i, Vrs)]) (cons (i, Vrs)) + ) Vrs (frees_of_bmv_monad inner) inner_tab; + in Typtab.update (fastype_of Inj, inner_tab') tab end + ) (the Injs) (the Vrss) tab + ) (0 upto length inners) (Inl outer :: inners) (SOME Injs :: Injss) (SOME Vrs :: Vrsss) (Typtab.make (map (rpair Typtab.empty o fastype_of) Injs')); val frees = distinct (op=) (maps snd (Typtab.dest (Typtab.map (K Typtab.keys) Vrs'))); + val Supps = map (Term.subst_atomic_types subst) (#Supps param); - val Supps = map (Term.subst_atomic_types subst) (#Supps param) val Vrs' = map (fn Inj => map (fn free => Option.mapPartial (fn xs => let val Vrss = distinct (op=) (rev xs); @@ -779,12 +804,15 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : bmv_monad list) lthy val find_fs = map (fn Inj => the (List.find (fn f => fastype_of f = fastype_of Inj) fs) ); + fun mk_comp t = if true orelse length (binder_types (fastype_of Sb)) > 1 then + HOLogic.mk_comp (t, Term.list_comb (Sb, find_fs Injs)) + else t in (( SOME (Term.subst_atomic_types subst ( - fold_rev (Term.absfree o dest_Free) fs (HOLogic.mk_comp ( - Term.list_comb (#Map param, - map2 (fn Sb => fn Injs => Term.list_comb (Sb, find_fs Injs)) Sbs Injss - ), Term.list_comb (Sb, find_fs Injs) + fold_rev (Term.absfree o dest_Free) fs (mk_comp ( + Term.list_comb (#Map param, @{map 3} (fn Inr T => K (K (HOLogic.id_const T)) + | _ => fn Sb => fn Injs => Term.list_comb (the Sb, find_fs (the Injs)) + ) inners Sbs Injss) )) )), SOME Injs'), @@ -806,7 +834,7 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : bmv_monad list) lthy let val bmvs' = Typtab.delete T bmvs in (SOME (add_ops T Injs bmvs'), bmvs') end end - ) Injs bmvs))) + ) Injs bmvs))); fun pick xs = nth xs (leader_of_bmv_monad outer) val ops = add_ops (the (pick outer_ops')) (the (pick Injs)) bmvs; @@ -831,10 +859,12 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : bmv_monad list) lthy val ops' = subtract (fn (bmv, T) => hd (ops_of_bmv_monad bmv) = T) bmv_ops ops; + val inners' = filter_bmvs inners; + val idxs = map (fn T => find_index (curry (op=) T) ops) ops'; val Vrs = map (the o nth Vrs) idxs; val Injs = map (the o nth Injs) idxs; - val frees = distinct (op=) (maps frees_of_bmv_monad (outer :: inners)); + val frees = distinct (op=) (maps frees_of_bmv_monad (outer :: inners')); val outer_Vrs = map (nth (Vrs_of_bmv_monad outer)) idxs; val model = { @@ -844,58 +874,61 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : bmv_monad list) lthy bd_infinite_regular_card_order = fn ctxt => rtac ctxt (bd_infinite_regular_card_order_of_bmv_monad outer) 1, var_class = var_class_of_bmv_monad outer, frees = frees, - lives = distinct (op=) (maps lives_of_bmv_monad inners), - lives' = distinct (op=) (maps lives'_of_bmv_monad inners), + lives = distinct (op=) (maps lives_of_bmv_monad inners'), + lives' = distinct (op=) (maps lives'_of_bmv_monad inners'), params = replicate (length ops') NONE, leader = 0, Injs = Injs, Sbs = map (the o nth Sbs) idxs, Vrs = Vrs, tacs = @{map 5} (fn axioms => fn param => fn Injs => fn Vrs => fn outer_Vrs => { - Sb_Inj = fn ctxt => EVERY [ - Local_Defs.unfold0_tac ctxt (#Sb_Inj axioms :: @{thms o_id}), - Local_Defs.unfold0_tac ctxt ( - #Map_id (#axioms param) - :: maps (map #Sb_Inj o axioms_of_bmv_monad) inners - ), - rtac ctxt refl 1 + Sb_Inj = fn ctxt => EVERY1 [ + rtac ctxt trans, + rtac ctxt @{thm arg_cong2[OF _ refl, of _ _ "(\)"]}, + rtac ctxt ext, + rtac ctxt (trans OF [#Map_cong (#axioms param), #Map_id (#axioms param) RS fun_cong]), + REPEAT_DETERM o resolve_tac ctxt (refl :: maps (map (fn ax => + #Sb_Inj ax RS fun_cong + ) o axioms_of_bmv_monad) inners'), + rtac ctxt @{thm trans[OF id_o]}, + rtac ctxt (#Sb_Inj axioms) ], Sb_comp_Injs = map (fn thm => fn ctxt => print_tac ctxt "Sb_comp_Inj" ) (#Sb_comp_Injs axioms), Sb_comp = fn ctxt => EVERY1 [ - K (Local_Defs.unfold0_tac ctxt @{thms comp_assoc}), + rtac ctxt @{thm trans[OF comp_assoc]}, rtac ctxt trans, rtac ctxt @{thm arg_cong2[OF refl, of _ _ "(\)"]}, - SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms comp_assoc[symmetric]}), + rtac ctxt @{thm trans[OF comp_assoc[symmetric]]}, rtac ctxt trans, rtac ctxt @{thm arg_cong2[OF _ refl, of _ _ "(\)"]}, rtac ctxt (#Map_Sb param RS sym), REPEAT_DETERM o assume_tac ctxt, - SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms comp_assoc}), + rtac ctxt @{thm trans[OF comp_assoc]}, rtac ctxt @{thm arg_cong2[OF refl, of _ _ "(\)"]}, rtac ctxt (#Sb_comp axioms), REPEAT_DETERM o assume_tac ctxt, - K (Local_Defs.unfold0_tac ctxt @{thms comp_assoc[symmetric]}), + rtac ctxt @{thm trans[OF comp_assoc[symmetric]]}, rtac ctxt @{thm arg_cong2[OF _ refl, of _ _ "(\)"]}, rtac ctxt trans, rtac ctxt (#Map_comp (#axioms param)), rtac ctxt ext, rtac ctxt (#Map_cong (#axioms param)), REPEAT_DETERM o EVERY' [ - EqSubst.eqsubst_tac ctxt [0] (maps (map #Sb_comp o axioms_of_bmv_monad) inners), + EqSubst.eqsubst_tac ctxt [0] (maps (map #Sb_comp o axioms_of_bmv_monad) inners'), REPEAT_DETERM o assume_tac ctxt, rtac ctxt refl ] ], Vrs_bds = map (map (Option.map (K (fn ctxt => EVERY1 [ REPEAT_DETERM o resolve_tac ctxt ( - map (fn thm => + maps (map_filter I) (#Vrs_bds axioms) + @ maps (maps (maps (map_filter I) o #Vrs_bds) o axioms_of_bmv_monad) inners' + @ #Supp_bd (#axioms param) + @ map (fn thm => thm OF [bd_infinite_regular_card_order_of_bmv_monad outer] ) @{thms infinite_regular_card_order_Un infinite_regular_card_order_UN} - @ maps (map_filter I) (#Vrs_bds axioms) - @ maps (maps (maps (map_filter I) o #Vrs_bds) o axioms_of_bmv_monad) inners - @ #Supp_bd (#axioms param) ) ])))) Vrs, Vrs_Injs = map (map (Option.map (fn thm => fn ctxt => @@ -904,37 +937,46 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : bmv_monad list) lthy Vrs_Sbs = map (map (Option.map (K (fn ctxt => EVERY1 [ K (Local_Defs.unfold0_tac ctxt @{thms UN_Un}), REPEAT_DETERM o rtac ctxt @{thm arg_cong2[of _ _ _ _ "(\)"]}, - TRY o EVERY' [ - EqSubst.eqsubst_tac ctxt [0] [#Map_Sb param], - REPEAT_DETERM1 o assume_tac ctxt, - SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms comp_def}), - rtac ctxt trans, - resolve_tac ctxt (maps (map_filter I) (#Vrs_Sbs axioms)), - REPEAT_DETERM1 o assume_tac ctxt, - EqSubst.eqsubst_tac ctxt [0] (maps (map_filter I) (#Map_Vrs param)), - rtac ctxt refl - ], - K (Local_Defs.unfold0_tac ctxt (@{thms comp_def} @ #Supp_Map (#axioms param) @ #Supp_Sb param)), - K (Local_Defs.unfold0_tac ctxt (@{thms image_comp[unfolded comp_def] UN_UN_flatten} - @ maps (maps (maps (map_filter I) o #Vrs_Sbs) o axioms_of_bmv_monad) inners - )), - REPEAT_DETERM o rtac ctxt refl + REPEAT_DETERM o FIRST' [ + EVERY' [ + rtac ctxt @{thm trans[OF arg_cong[OF comp_apply]]}, + rtac ctxt trans, + resolve_tac ctxt (maps (map_filter I) (#Map_Vrs param)), + rtac ctxt trans, + resolve_tac ctxt (maps (map_filter I) (#Vrs_Sbs axioms)), + REPEAT_DETERM o assume_tac ctxt, + rtac ctxt refl + ], + EVERY' [ + rtac ctxt trans, + rtac ctxt @{thm arg_cong[of _ _ "\x. \(_ ` x)"]}, + rtac ctxt trans, + rtac ctxt @{thm trans[OF arg_cong[OF comp_apply]]}, + resolve_tac ctxt (#Supp_Map (#axioms param)), + rtac ctxt @{thm arg_cong[of _ _ "\x. _ ` x"]}, + resolve_tac ctxt (#Supp_Sb param), + SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms UN_simps(10)}), + rtac ctxt trans, + rtac ctxt @{thm UN_cong}, + resolve_tac ctxt (maps (maps (maps (map_filter I) o #Vrs_Sbs) o axioms_of_bmv_monad) inners'), + REPEAT_DETERM o assume_tac ctxt, + SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms UN_extend_simps(9)}), + rtac ctxt refl + ] + ] ])))) Vrs, Sb_cong = fn ctxt => EVERY1 [ - K (Local_Defs.unfold0_tac ctxt @{thms comp_def}), + rtac ctxt @{thm comp_apply_eq}, Subgoal.FOCUS_PREMS (fn {context=ctxt, prems, ...} => EVERY1 [ - EqSubst.eqsubst_tac ctxt [0] [Drule.rotate_prems (~(length ( - maps (map_filter I) outer_Vrs - ))) (#Sb_cong axioms)], - resolve_tac ctxt prems, - etac ctxt @{thm contrapos_pp}, - SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms Un_iff de_Morgan_disj}), - REPEAT_DETERM o etac ctxt conjE, - assume_tac ctxt, - REPEAT_DETERM o resolve_tac ctxt prems, + rtac ctxt @{thm trans[rotated]}, + rtac ctxt ( + let val n = length (lives_of_bmv_monad outer); + in mk_arg_cong lthy (n + 1) (#Map param) OF (replicate n refl) end + ), + K (prefer_tac 2), rtac ctxt (#Map_cong (#axioms param)), K (Local_Defs.unfold0_tac ctxt (#Supp_Sb param)), - EVERY' (map (fn inner => EVERY' [ + EVERY' (map (fn Inr _ => rtac ctxt refl | Inl inner => EVERY' [ resolve_tac ctxt (map #Sb_cong (axioms_of_bmv_monad inner)), REPEAT_DETERM o EVERY' [ REPEAT_DETERM o resolve_tac ctxt prems, @@ -946,7 +988,17 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : bmv_monad list) lthy assume_tac ctxt, assume_tac ctxt ] - ]) inners) + ]) inners), + rtac ctxt (#Sb_cong axioms), + REPEAT_DETERM o EVERY' [ + resolve_tac ctxt prems, + TRY o EVERY' [ + etac ctxt @{thm contrapos_pp}, + SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms Un_iff de_Morgan_disj}), + REPEAT_DETERM o etac ctxt conjE, + assume_tac ctxt + ] + ] ]) ctxt ] } : (Proof.context -> tactic) bmv_monad_axioms) @@ -958,12 +1010,14 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : bmv_monad list) lthy val (res, lthy) = bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) qualify model lthy in (res, lthy) end; -fun pbmv_monad_cmd (((((((b, ops), frees), Sbs), Injs), Vrs), param_opt), bd) lthy = +fun pbmv_monad_cmd ((((((b, ops), Sbs), Injs), Vrs), param_opt), bd) lthy = let val ops = map (Syntax.read_typ lthy) ops; val bd = Syntax.read_term lthy bd; - val frees = map (Syntax.read_typ lthy) frees; val Sbs = map (Syntax.read_term lthy) Sbs; + val frees = distinct (op=) (maps ( + map (fst o dest_funT) o fst o split_last o binder_types o fastype_of + ) Sbs); val Injs = map (map (Syntax.read_term lthy)) Injs; val Vrs = map (map (map (fn "_" => NONE | t => SOME (Syntax.read_term lthy t)))) Vrs; @@ -1029,7 +1083,7 @@ fun pbmv_monad_cmd (((((((b, ops), frees), Sbs), Injs), Vrs), param_opt), bd) lt fun print_pbmv_monads ctxt = let - fun pretty_mrbnf (key, BMV {ops, frees, lives, bd, ...}) = + fun pretty_mrbnf (key, BMV {ops, frees, lives, bd, Sbs, ...}) = Pretty.big_list (Pretty.string_of (Pretty.block ([Pretty.str key, Pretty.str ":", Pretty.brk 1] @ map (Pretty.quote o Syntax.pretty_typ ctxt) ops))) @@ -1039,7 +1093,8 @@ fun print_pbmv_monads ctxt = [Pretty.block [Pretty.str "live:", Pretty.brk 1, Pretty.str (string_of_int (length lives)), Pretty.brk 3, Pretty.list "[" "]" (List.map (Syntax.pretty_typ ctxt) lives)]] else []) @ - [Pretty.block [Pretty.str ("bd:"), Pretty.brk 1, + [ Pretty.block ([Pretty.str "Sb:", Pretty.brk 1] @ map (Pretty.quote o Syntax.pretty_term ctxt) Sbs), + Pretty.block [Pretty.str ("bd:"), Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt bd)]]); in Pretty.big_list "Registered parametrized bounded multi-variate monads:" @@ -1054,8 +1109,7 @@ val _ = val _ = Outer_Syntax.local_theory_to_proof @{command_keyword pbmv_monad} "register a parametrized bounded multi-variate monad" - (parse_opt_binding_colon -- Scan.repeat1 (Scan.unless (Parse.reserved "frees") Parse.typ) --| - (Parse.reserved "frees" -- @{keyword ":"}) -- Scan.repeat1 (Scan.unless (Parse.reserved "Sbs") Parse.typ) --| + (parse_opt_binding_colon -- Scan.repeat1 (Scan.unless (Parse.reserved "Sbs") Parse.typ) --| (Parse.reserved "Sbs" -- @{keyword ":"}) -- Scan.repeat1 (Scan.unless (Parse.reserved "Injs") Parse.term) --| (Parse.reserved "Injs" -- @{keyword ":"}) -- Parse.list (Scan.repeat1 (Scan.unless (Parse.reserved "Vrs") Parse.term)) --| (Parse.reserved "Vrs" -- @{keyword ":"}) -- Parse.and_list (Parse.list ( diff --git a/Tools/mrbnf_util.ML b/Tools/mrbnf_util.ML index 06a3b75..73e1906 100644 --- a/Tools/mrbnf_util.ML +++ b/Tools/mrbnf_util.ML @@ -3,6 +3,7 @@ sig include BNF_UTIL datatype ('a, 'b) either = Inl of 'a | Inr of 'b + val map_sum: ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) either -> ('c, 'd) either val filter_like: 'a list -> ('a -> bool) -> 'b list -> 'b list val cond_keep: 'a list -> bool list -> 'a list @@ -83,6 +84,9 @@ open BNF_Util datatype ('a, 'b) either = Inl of 'a | Inr of 'b +fun map_sum f _ (Inl x) = Inl (f x) + | map_sum _ g (Inr x) = Inr (g x) + fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) = apfst (cons (x, T)) (strip_ex t) | strip_ex t = ([], t) diff --git a/Tools/pbmv_monad_comp.ML b/Tools/pbmv_monad_comp.ML new file mode 100644 index 0000000..718ac97 --- /dev/null +++ b/Tools/pbmv_monad_comp.ML @@ -0,0 +1,57 @@ +signature PBMV_MONAD_COMP = sig + + val id_bmv_monad: BMV_Monad_Def.bmv_monad + val mk_id_bmv_monad: string * sort -> BMV_Monad_Def.bmv_monad + + val pbmv_monad_of_typ: bool -> BNF_Def.inline_policy -> (theory -> BNF_Def.fact_policy) + -> (binding -> binding) -> typ -> (thm list * local_theory) + -> BMV_Monad_Def.bmv_monad option * (thm list * local_theory) +end + +structure PBMV_Monad_Comp : PBMV_MONAD_COMP = struct + +open MRBNF_Util + +val id_bmv_monad = the (BMV_Monad_Def.pbmv_monad_of @{context} "BMV_Monad.ID"); + +fun mk_id_bmv_monad free = BMV_Monad_Def.morph_bmv_monad ( + MRBNF_Util.subst_typ_morphism [(hd (BMV_Monad_Def.frees_of_bmv_monad id_bmv_monad), TFree free)] +) id_bmv_monad; + +fun pbmv_monad_of_typ _ _ _ _ (TFree x) accum = (SOME (mk_id_bmv_monad x), accum) + | pbmv_monad_of_typ _ _ _ _ (TVar _) _ = error "unexpected schematic variable" + | pbmv_monad_of_typ optim const_policy inline_policy qualify' (T as Type (n, Ts)) (accum, lthy) = + let val (bmv_opt, lthy) = case BMV_Monad_Def.pbmv_monad_of lthy n of + SOME bmv => (SOME bmv, lthy) + | NONE => case BNF_Def.bnf_of lthy n of + SOME bnf => + let val (bmv, lthy) = BMV_Monad_Def.pbmv_monad_of_bnf bnf lthy + in (SOME bmv, BMV_Monad_Def.register_pbmv_monad n bmv lthy) end + | NONE => (NONE, lthy); + in case bmv_opt of + NONE => (NONE, (accum, lthy)) + | SOME bmv => if null (BMV_Monad_Def.lives_of_bmv_monad bmv) then + let val T = nth (BMV_Monad_Def.ops_of_bmv_monad bmv) (BMV_Monad_Def.leader_of_bmv_monad bmv) + in (SOME (BMV_Monad_Def.morph_bmv_monad (MRBNF_Util.subst_typ_morphism ( + rev (map TFree (Term.add_tfreesT T []) @ map TVar (Term.add_tvarsT T [])) ~~ Ts + )) bmv), (accum, lthy)) end + else let + (* TODO: outer with mixed/frees lives *) + val name = Long_Name.base_name n; + + fun qualify i = + let val namei = name ^ nonzero_string_of_int i; + in qualify' o Binding.qualify true namei end; + + val qualifies = map qualify (1 upto length Ts); + val (bmv_opts, (accum, lthy)) = @{fold_map 2} (pbmv_monad_of_typ optim const_policy inline_policy) qualifies Ts (accum, lthy) + val bmvs = map2 (fn T => fn NONE => Inr T | SOME bmv => Inl bmv) Ts bmv_opts; + in if exists Option.isSome bmv_opts then + let val ((bmv, unfold_set), lthy) = BMV_Monad_Def.compose_bmv_monad (qualify 0) bmv bmvs lthy; + in (SOME bmv, (unfold_set @ accum, lthy)) end + else + (NONE, (accum, lthy)) + end + end; + +end \ No newline at end of file diff --git a/operations/BMV_Monad.thy b/operations/BMV_Monad.thy index 39a9369..635b66b 100644 --- a/operations/BMV_Monad.thy +++ b/operations/BMV_Monad.thy @@ -99,7 +99,6 @@ ML_file \../Tools/bmv_monad_def.ML\ local_setup \fold BMV_Monad_Def.register_bnf_as_pbmv_monad [@{type_name sum}, @{type_name prod}]\ pbmv_monad ID: "'a" - frees: 'a Sbs: "id :: ('a \ 'a) \ 'a \ 'a" Injs: "id :: 'a \ 'a" Vrs: "\(x::'a). {x}" @@ -107,7 +106,6 @@ pbmv_monad ID: "'a" by (auto simp: ID.set_bd infinite_regular_card_order_natLeq) pbmv_monad "'a::var FType" - frees: "'a::var" Sbs: tvsubst_FType Injs: TyVar Vrs: FVars_FType @@ -122,11 +120,39 @@ pbmv_monad "'a::var FType" apply (rule Sb_cong_FType[unfolded SSupp_FType_def tvVVr_tvsubst_FType_def[unfolded comp_def] tv\_FType_tvsubst_FType_def TyVar_def[symmetric]]; assumption) done -print_pbmv_monads +typedef ('a1, 'a2, 'c1, 'c2) L = "UNIV :: ('a1 * 'a1 * ('c1 + 'c2)) set" + by (rule exI, rule UNIV_I) + +(*pbmv_monad "('a1, 'a2, 'c1, 'c2) L" + frees: 'a1 'a2 + Sbs: "\f x. Abs_L (map_prod f (map_prod f id) (Rep_L x))" + Injs: "id :: 'a1 \ 'a1" + Vrs: "\x. case Rep_L x of (x1, x2, _) \ {x1, x2}" + bd: natLeq + lives: 'c1 'c2*) + +ML_file \../Tools/pbmv_monad_comp.ML\ ML \ Multithreading.parallel_proofs := 0 \ +declare [[ML_print_depth=1000]] +local_setup \fn lthy => + let + val (bmv, (thms, lthy)) = PBMV_Monad_Comp.pbmv_monad_of_typ true BNF_Def.Smart_Inline (K BNF_Def.Note_Some) I + @{typ "'a1 * 'a1 * (('a1 * 'a2) + ('a1 * 'a2 * 'a2 * 'a2 FType))"} + ([], lthy) + + val _ = @{print} (map (map (map (Option.map (Thm.cterm_of lthy o + Raw_Simplifier.rewrite_term (Proof_Context.theory_of lthy) + (@{thms } @ thms) [] + )))) ( + BMV_Monad_Def.Vrs_of_bmv_monad (the bmv) + )) + + val _ = @{print} bmv + in lthy end\ +print_pbmv_monads (* *) type_synonym ('a1, 'a2, 'c1, 'c2) L = "'a1 * 'a1 * ('c1 + 'c2)" (* PBMV *) @@ -570,7 +596,7 @@ local_setup \fn lthy => val ((L1_bmv, _), lthy) = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) (Binding.prefix_name "L1_") model_L1 lthy; val ((L2_bmv, _), lthy) = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) (Binding.prefix_name "L2_") model_L2 lthy; - val ((comp_bmv, unfold_set), lthy) = BMV_Monad_Def.compose_bmv_monad I L_bmv [L1_bmv, L2_bmv] lthy + val ((comp_bmv, unfold_set), lthy) = BMV_Monad_Def.compose_bmv_monad I L_bmv [MRBNF_Util.Inl L1_bmv, MRBNF_Util.Inl L2_bmv] lthy val _ = @{print} comp_bmv in lthy end \