# HG changeset patch # User kuncar # Date 1406226094 -7200 # Node ID b590fcd03a4aa0a9c46818112ccd203b878bb1a6 # Parent cffd1d6ae1e5ccce7bf7c3871f447faa7d625961 store explicitly quotient types with no_code => more precise registration of code equations diff -r cffd1d6ae1e5 -r b590fcd03a4a src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Jul 24 19:01:06 2014 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu Jul 24 20:21:34 2014 +0200 @@ -401,6 +401,22 @@ val register_code_eq_attribute = Thm.declaration_attribute (fn thm => Context.mapping (register_encoded_code_eq thm) I) val register_code_eq_attrib = Attrib.internal (K register_code_eq_attribute) + + fun no_no_code ctxt (rty, qty) = + if same_type_constrs (rty, qty) then + forall (no_no_code ctxt) (Targs rty ~~ Targs qty) + else + if is_Type qty then + if Lifting_Info.is_no_code_type ctxt (Tname qty) then false + else + let + val (rty', rtyq) = Lifting_Term.instantiate_rtys ctxt (rty, qty) + val (rty's, rtyqs) = (Targs rty', Targs rtyq) + in + forall (no_no_code ctxt) (rty's ~~ rtyqs) + end + else + true in fun register_code_eq abs_eq_thm opt_rep_eq_thm (rty, qty) lthy = @@ -408,8 +424,10 @@ val thy = Proof_Context.theory_of lthy val encoded_code_eq = encode_code_eq thy abs_eq_thm opt_rep_eq_thm (rty, qty) in - (snd oo Local_Theory.note) ((Binding.empty, [register_code_eq_attrib]), - [encoded_code_eq]) lthy + if no_no_code lthy (rty, qty) then + (snd oo Local_Theory.note) ((Binding.empty, [register_code_eq_attrib]), [encoded_code_eq]) lthy + else + lthy end end diff -r cffd1d6ae1e5 -r b590fcd03a4a src/HOL/Tools/Lifting/lifting_info.ML --- a/src/HOL/Tools/Lifting/lifting_info.ML Thu Jul 24 19:01:06 2014 +0200 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Thu Jul 24 20:21:34 2014 +0200 @@ -34,10 +34,14 @@ pos_distr_rules: thm list, neg_distr_rules: thm list} val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option + val add_no_code_type: string -> Context.generic -> Context.generic + val is_no_code_type: Proof.context -> string -> bool + val get_quot_maps : Proof.context -> quot_map Symtab.table val get_quotients : Proof.context -> quotient Symtab.table val get_relator_distr_data : Proof.context -> relator_distr_data Symtab.table val get_restore_data : Proof.context -> restore_data Symtab.table + val get_no_code_types : Proof.context -> unit Symtab.table val setup: theory -> theory end @@ -82,52 +86,61 @@ quotients : quotient Symtab.table, reflexivity_rules : thm Item_Net.T, relator_distr_data : relator_distr_data Symtab.table, - restore_data : restore_data Symtab.table + restore_data : restore_data Symtab.table, + no_code_types : unit Symtab.table } val empty = { quot_maps = Symtab.empty, quotients = Symtab.empty, reflexivity_rules = Thm.full_rules, relator_distr_data = Symtab.empty, - restore_data = Symtab.empty + restore_data = Symtab.empty, + no_code_types = Symtab.empty } val extend = I fun merge ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1, - restore_data = rd1 }, + restore_data = rd1, no_code_types = nct1 }, { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2, - restore_data = rd2 } ) = + restore_data = rd2, no_code_types = nct2 } ) = { quot_maps = Symtab.merge (K true) (qm1, qm2), quotients = Symtab.merge (K true) (q1, q2), reflexivity_rules = Item_Net.merge (rr1, rr2), relator_distr_data = Symtab.merge (K true) (rdd1, rdd2), - restore_data = Symtab.join join_restore_data (rd1, rd2) } + restore_data = Symtab.join join_restore_data (rd1, rd2), + no_code_types = Symtab.merge (K true) (nct1, nct2) + } ) -fun map_data f1 f2 f3 f4 f5 - { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data } = +fun map_data f1 f2 f3 f4 f5 f6 + { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data, no_code_types } = { quot_maps = f1 quot_maps, quotients = f2 quotients, reflexivity_rules = f3 reflexivity_rules, relator_distr_data = f4 relator_distr_data, - restore_data = f5 restore_data } + restore_data = f5 restore_data, + no_code_types = f6 no_code_types + } -fun map_quot_maps f = map_data f I I I I -fun map_quotients f = map_data I f I I I -fun map_reflexivity_rules f = map_data I I f I I -fun map_relator_distr_data f = map_data I I I f I -fun map_restore_data f = map_data I I I I f +fun map_quot_maps f = map_data f I I I I I +fun map_quotients f = map_data I f I I I I +fun map_reflexivity_rules f = map_data I I f I I I +fun map_relator_distr_data f = map_data I I I f I I +fun map_restore_data f = map_data I I I I f I +fun map_no_code_types f = map_data I I I I I f val get_quot_maps' = #quot_maps o Data.get val get_quotients' = #quotients o Data.get val get_reflexivity_rules' = #reflexivity_rules o Data.get val get_relator_distr_data' = #relator_distr_data o Data.get val get_restore_data' = #restore_data o Data.get +val get_no_code_types' = #no_code_types o Data.get fun get_quot_maps ctxt = get_quot_maps' (Context.Proof ctxt) fun get_quotients ctxt = get_quotients' (Context.Proof ctxt) fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt) fun get_restore_data ctxt = get_restore_data' (Context.Proof ctxt) +fun get_no_code_types ctxt = get_no_code_types' (Context.Proof ctxt) (* info about Quotient map theorems *) @@ -500,6 +513,13 @@ #> Global_Theory.add_thms_dynamic (@{binding relator_mono_raw}, get_mono_rules_raw) +(* no_code types *) + +fun add_no_code_type type_name ctxt = + Data.map (map_no_code_types (Symtab.update (type_name, ()))) ctxt; + +fun is_no_code_type ctxt type_name = (Symtab.defined o get_no_code_types) ctxt type_name + (* theory setup *) val setup = diff -r cffd1d6ae1e5 -r b590fcd03a4a src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Thu Jul 24 19:01:06 2014 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Thu Jul 24 20:21:34 2014 +0200 @@ -234,7 +234,7 @@ fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy = let val _ = quot_thm_sanity_check lthy quot_thm - val (_, qtyp) = quot_thm_rty_qty quot_thm + val (_, qty) = quot_thm_rty_qty quot_thm val (pcrel_def, lthy) = define_pcrel (quot_thm_crel quot_thm) lthy (**) val pcrel_def = Option.map (Morphism.thm (Local_Theory.target_morphism lthy)) pcrel_def @@ -246,7 +246,7 @@ SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq } | NONE => NONE val quotients = { quot_thm = quot_thm, pcr_info = pcr_info } - val qty_full_name = (fst o dest_Type) qtyp + val qty_full_name = (fst o dest_Type) qty fun quot_info phi = Lifting_Info.transform_quotient phi quotients val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute) val lthy = case opt_reflp_thm of @@ -256,11 +256,14 @@ |> define_code_constr gen_code quot_thm | NONE => lthy |> define_abs_type gen_code quot_thm + fun declare_no_code qty = Local_Theory.declaration {syntax = false, pervasive = true} + (fn phi => Lifting_Info.add_no_code_type (Morphism.typ phi qty |> Tname)) in lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi)) |> lifting_bundle qty_full_name quotients + |> (if not gen_code then declare_no_code qty else I) end local diff -r cffd1d6ae1e5 -r b590fcd03a4a src/HOL/Tools/Lifting/lifting_term.ML --- a/src/HOL/Tools/Lifting/lifting_term.ML Thu Jul 24 19:01:06 2014 +0200 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Thu Jul 24 20:21:34 2014 +0200 @@ -11,6 +11,8 @@ exception MERGE_TRANSFER_REL of Pretty.T exception CHECK_RTY of typ * typ + val instantiate_rtys: Proof.context -> typ * typ -> typ * typ + val prove_quot_thm: Proof.context -> typ * typ -> thm val abs_fun: Proof.context -> typ * typ -> term