1.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Thu Jul 24 19:01:06 2014 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Thu Jul 24 20:21:34 2014 +0200
     1.3 @@ -34,10 +34,14 @@
     1.4      pos_distr_rules: thm list, neg_distr_rules: thm list}
     1.5    val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option
     1.6  
     1.7 +  val add_no_code_type: string -> Context.generic -> Context.generic
     1.8 +  val is_no_code_type: Proof.context -> string -> bool
     1.9 +
    1.10    val get_quot_maps           : Proof.context -> quot_map Symtab.table
    1.11    val get_quotients           : Proof.context -> quotient Symtab.table
    1.12    val get_relator_distr_data  : Proof.context -> relator_distr_data Symtab.table
    1.13    val get_restore_data        : Proof.context -> restore_data Symtab.table
    1.14 +  val get_no_code_types       : Proof.context -> unit Symtab.table
    1.15  
    1.16    val setup: theory -> theory
    1.17  end
    1.18 @@ -82,52 +86,61 @@
    1.19        quotients : quotient Symtab.table,
    1.20        reflexivity_rules : thm Item_Net.T,
    1.21        relator_distr_data : relator_distr_data Symtab.table,
    1.22 -      restore_data : restore_data Symtab.table
    1.23 +      restore_data : restore_data Symtab.table,
    1.24 +      no_code_types : unit Symtab.table
    1.25      }
    1.26    val empty =
    1.27      { quot_maps = Symtab.empty,
    1.28        quotients = Symtab.empty,
    1.29        reflexivity_rules = Thm.full_rules,
    1.30        relator_distr_data = Symtab.empty,
    1.31 -      restore_data = Symtab.empty
    1.32 +      restore_data = Symtab.empty,
    1.33 +      no_code_types = Symtab.empty
    1.34      }
    1.35    val extend = I
    1.36    fun merge
    1.37      ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1, 
    1.38 -        restore_data = rd1 },
    1.39 +        restore_data = rd1, no_code_types = nct1 },
    1.40        { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2,
    1.41 -        restore_data = rd2 } ) =
    1.42 +        restore_data = rd2, no_code_types = nct2 } ) =
    1.43      { quot_maps = Symtab.merge (K true) (qm1, qm2),
    1.44        quotients = Symtab.merge (K true) (q1, q2),
    1.45        reflexivity_rules = Item_Net.merge (rr1, rr2),
    1.46        relator_distr_data = Symtab.merge (K true) (rdd1, rdd2),
    1.47 -      restore_data = Symtab.join join_restore_data (rd1, rd2) }
    1.48 +      restore_data = Symtab.join join_restore_data (rd1, rd2),
    1.49 +      no_code_types = Symtab.merge (K true) (nct1, nct2)
    1.50 +    }
    1.51  )
    1.52  
    1.53 -fun map_data f1 f2 f3 f4 f5
    1.54 -  { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data } =
    1.55 +fun map_data f1 f2 f3 f4 f5 f6
    1.56 +  { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data, no_code_types } =
    1.57    { quot_maps = f1 quot_maps,
    1.58      quotients = f2 quotients,
    1.59      reflexivity_rules = f3 reflexivity_rules,
    1.60      relator_distr_data = f4 relator_distr_data,
    1.61 -    restore_data = f5 restore_data }
    1.62 +    restore_data = f5 restore_data,
    1.63 +    no_code_types = f6 no_code_types
    1.64 +  }
    1.65  
    1.66 -fun map_quot_maps           f = map_data f I I I I
    1.67 -fun map_quotients           f = map_data I f I I I
    1.68 -fun map_reflexivity_rules   f = map_data I I f I I
    1.69 -fun map_relator_distr_data  f = map_data I I I f I
    1.70 -fun map_restore_data        f = map_data I I I I f
    1.71 +fun map_quot_maps           f = map_data f I I I I I
    1.72 +fun map_quotients           f = map_data I f I I I I
    1.73 +fun map_reflexivity_rules   f = map_data I I f I I I
    1.74 +fun map_relator_distr_data  f = map_data I I I f I I
    1.75 +fun map_restore_data        f = map_data I I I I f I
    1.76 +fun map_no_code_types       f = map_data I I I I I f
    1.77    
    1.78  val get_quot_maps'           = #quot_maps o Data.get
    1.79  val get_quotients'           = #quotients o Data.get
    1.80  val get_reflexivity_rules'   = #reflexivity_rules o Data.get
    1.81  val get_relator_distr_data'  = #relator_distr_data o Data.get
    1.82  val get_restore_data'        = #restore_data o Data.get
    1.83 +val get_no_code_types'       = #no_code_types o Data.get
    1.84  
    1.85  fun get_quot_maps          ctxt = get_quot_maps' (Context.Proof ctxt)
    1.86  fun get_quotients          ctxt = get_quotients' (Context.Proof ctxt)
    1.87  fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt)
    1.88  fun get_restore_data       ctxt = get_restore_data' (Context.Proof ctxt)
    1.89 +fun get_no_code_types      ctxt = get_no_code_types' (Context.Proof ctxt)
    1.90  
    1.91  (* info about Quotient map theorems *)
    1.92  
    1.93 @@ -500,6 +513,13 @@
    1.94    #> Global_Theory.add_thms_dynamic
    1.95       (@{binding relator_mono_raw}, get_mono_rules_raw)
    1.96  
    1.97 +(* no_code types *)
    1.98 +
    1.99 +fun add_no_code_type type_name ctxt = 
   1.100 +  Data.map (map_no_code_types (Symtab.update (type_name, ()))) ctxt;
   1.101 +
   1.102 +fun is_no_code_type ctxt type_name = (Symtab.defined o get_no_code_types) ctxt type_name
   1.103 +
   1.104  (* theory setup *)
   1.105  
   1.106  val setup =