added 'ctr_sugar' interpretation hook
authorblanchet
Tue Apr 01 10:51:29 2014 +0200 (2014-04-01)
changeset 56345228e30cb111d
parent 56344 1014f44c62a2
child 56346 42533f8f4729
added 'ctr_sugar' interpretation hook
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Apr 01 10:04:05 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Apr 01 10:51:29 2014 +0200
     1.3 @@ -38,6 +38,7 @@
     1.4    val ctr_sugar_of: Proof.context -> string -> ctr_sugar option
     1.5    val ctr_sugars_of: Proof.context -> ctr_sugar list
     1.6    val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
     1.7 +  val ctr_sugar_interpretation: (ctr_sugar -> theory -> theory) -> theory -> theory
     1.8    val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
     1.9    val default_register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
    1.10  
    1.11 @@ -151,12 +152,28 @@
    1.12  fun ctr_sugar_of_case ctxt s =
    1.13    find_first (fn {casex = Const (s', _), ...} => s' = s | _ => false) (ctr_sugars_of ctxt);
    1.14  
    1.15 +structure Ctr_Sugar_Interpretation = Interpretation
    1.16 +(
    1.17 +  type T = ctr_sugar;
    1.18 +  val eq: T * T -> bool = op = o pairself #ctrs;
    1.19 +);
    1.20 +
    1.21 +val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation;
    1.22 +
    1.23  fun register_ctr_sugar key ctr_sugar =
    1.24    Local_Theory.declaration {syntax = false, pervasive = true}
    1.25 -    (fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar)));
    1.26 +    (fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar)))
    1.27 +  #> Local_Theory.background_theory (Ctr_Sugar_Interpretation.data ctr_sugar);
    1.28  
    1.29 -fun default_register_ctr_sugar_global key ctr_sugar =
    1.30 -  Context.theory_map (Data.map (Symtab.default (key, ctr_sugar)));
    1.31 +fun default_register_ctr_sugar_global key ctr_sugar thy =
    1.32 +  let val tab = Data.get (Context.Theory thy) in
    1.33 +    if Symtab.defined tab key then
    1.34 +      thy
    1.35 +    else
    1.36 +      thy
    1.37 +      |> Context.theory_map (Data.put (Symtab.update_new (key, ctr_sugar) tab))
    1.38 +      |> Ctr_Sugar_Interpretation.data ctr_sugar
    1.39 +  end;
    1.40  
    1.41  val isN = "is_";
    1.42  val unN = "un_";