go back to the complicated code equation registration (because of type classes) that was lost in 922586b1bc87; make it even more hackish to get which code equation was used
authorkuncar
Mon Apr 13 15:27:34 2015 +0200 (2015-04-13)
changeset 602304857d553c52c
parent 60229 4cd6462c1fda
child 60231 0daab758e087
go back to the complicated code equation registration (because of type classes) that was lost in 922586b1bc87; make it even more hackish to get which code equation was used
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_def_code_dt.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Dec 05 14:14:36 2014 +0100
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Apr 13 15:27:34 2015 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature LIFTING_DEF =
     1.6  sig
     1.7 -  datatype code_eq = NONE_EQ | ABS_EQ | REP_EQ
     1.8 +  datatype code_eq = UNKNOWN_EQ | NONE_EQ | ABS_EQ | REP_EQ
     1.9    type lift_def
    1.10    val rty_of_lift_def: lift_def -> typ
    1.11    val qty_of_lift_def: lift_def -> typ
    1.12 @@ -59,7 +59,7 @@
    1.13  
    1.14  infix 0 MRSL
    1.15  
    1.16 -datatype code_eq = NONE_EQ | ABS_EQ | REP_EQ
    1.17 +datatype code_eq = UNKNOWN_EQ | NONE_EQ | ABS_EQ | REP_EQ
    1.18  
    1.19  datatype lift_def = LIFT_DEF of {
    1.20    rty: typ,
    1.21 @@ -486,17 +486,68 @@
    1.22            end
    1.23        else
    1.24          true
    1.25 +
    1.26 +  fun encode_code_eq ctxt abs_eq opt_rep_eq (rty, qty) = 
    1.27 +    let
    1.28 +      fun mk_type typ = typ |> Logic.mk_type |> Thm.cterm_of ctxt |> Drule.mk_term
    1.29 +    in
    1.30 +      Conjunction.intr_balanced [abs_eq, (the_default TrueI opt_rep_eq), mk_type rty, mk_type qty]
    1.31 +    end
    1.32 +  
    1.33 +  exception DECODE
    1.34 +    
    1.35 +  fun decode_code_eq thm =
    1.36 +    if Thm.nprems_of thm > 0 then raise DECODE 
    1.37 +    else
    1.38 +      let
    1.39 +        val [abs_eq, rep_eq, rty, qty] = Conjunction.elim_balanced 4 thm
    1.40 +        val opt_rep_eq = if Thm.eq_thm_prop (rep_eq, TrueI) then NONE else SOME rep_eq
    1.41 +        fun dest_type typ = typ |> Drule.dest_term |> Thm.term_of |> Logic.dest_type
    1.42 +      in
    1.43 +        (abs_eq, opt_rep_eq, (dest_type rty, dest_type qty)) 
    1.44 +      end
    1.45 +  
    1.46 +  structure Data = Generic_Data
    1.47 +  (
    1.48 +    type T = code_eq option
    1.49 +    val empty = NONE
    1.50 +    val extend = I
    1.51 +    fun merge _ = NONE
    1.52 +  );
    1.53 +
    1.54 +  fun register_encoded_code_eq thm thy =
    1.55 +    let
    1.56 +      val (abs_eq_thm, opt_rep_eq_thm, (rty, qty)) = decode_code_eq thm
    1.57 +      val (code_eq, thy) = register_code_eq_thy abs_eq_thm opt_rep_eq_thm (rty, qty) thy
    1.58 +    in
    1.59 +      Context.theory_map (Data.put (SOME code_eq)) thy
    1.60 +    end
    1.61 +    handle DECODE => thy
    1.62 +  
    1.63 +  val register_code_eq_attribute = Thm.declaration_attribute
    1.64 +    (fn thm => Context.mapping (register_encoded_code_eq thm) I)
    1.65 +  val register_code_eq_attrib = Attrib.internal (K register_code_eq_attribute)
    1.66 +
    1.67  in
    1.68  
    1.69  fun register_code_eq abs_eq_thm opt_rep_eq_thm (rty, qty) lthy =
    1.70    let
    1.71 -    val mthm = Morphism.thm (Local_Theory.target_morphism lthy)
    1.72 -    val abs_eq_thm =  mthm abs_eq_thm
    1.73 -    val opt_rep_eq_thm = Option.map mthm opt_rep_eq_thm
    1.74 +    val encoded_code_eq = encode_code_eq lthy abs_eq_thm opt_rep_eq_thm (rty, qty)
    1.75    in
    1.76 -    if no_no_code lthy (rty, qty) then 
    1.77 -      Local_Theory.background_theory_result 
    1.78 -        (register_code_eq_thy abs_eq_thm opt_rep_eq_thm (rty, qty)) lthy
    1.79 +    if no_no_code lthy (rty, qty) then
    1.80 +      let
    1.81 +        val lthy = (snd oo Local_Theory.note) 
    1.82 +          ((Binding.empty, [register_code_eq_attrib]), [encoded_code_eq]) lthy
    1.83 +        val opt_code_eq = Data.get (Context.Theory (Proof_Context.theory_of lthy))
    1.84 +        val code_eq = if is_some opt_code_eq then the opt_code_eq 
    1.85 +          else UNKNOWN_EQ (* UNKNOWN_EQ means that we are in a locale and we do not know
    1.86 +            which code equation is going to be used. This is going to be resolved at the
    1.87 +            point when an interpretation of the locale is executed. *)
    1.88 +        val lthy = Local_Theory.declaration {syntax = false, pervasive = true} 
    1.89 +          (K (Data.put NONE)) lthy
    1.90 +      in
    1.91 +        (code_eq, lthy)
    1.92 +      end
    1.93      else
    1.94        (NONE_EQ, lthy)
    1.95    end
     2.1 --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Fri Dec 05 14:14:36 2014 +0100
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Mon Apr 13 15:27:34 2015 +0200
     2.3 @@ -242,7 +242,10 @@
     2.4  
     2.5      val (ret_lift_def, lthy) = add_lift_def (#lift_config config) var qty rhs rsp_thm par_thms lthy
     2.6    in
     2.7 -    if (not (#code_dt config) orelse (code_eq_of_lift_def ret_lift_def <> NONE_EQ))
     2.8 +    if (not (#code_dt config) orelse (code_eq_of_lift_def ret_lift_def <> NONE_EQ)
     2.9 +      andalso (code_eq_of_lift_def ret_lift_def <> UNKNOWN_EQ))
    2.10 +      (* Let us try even in case of UNKNOWN_EQ. If this leads to problems, the user can always
    2.11 +        say that they do not want this workaround. *)
    2.12      then  (ret_lift_def, lthy)
    2.13      else
    2.14        let