src/HOL/Tools/Ctr_Sugar/local_interpretation.ML
author blanchet
Thu Sep 04 11:20:59 2014 +0200 (2014-09-04)
changeset 58182 82478e6c60cb
parent 58178 695ba3101b37
child 58185 e6e3b20340be
permissions -rw-r--r--
tweaked setup for datatype realizer
blanchet@58177
     1
(*  Title:      HOL/Tools/Ctr_Sugar/local_interpretation.ML
blanchet@58177
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@58177
     3
blanchet@58177
     4
Generic interpretation of local theory data -- ad hoc. Based on
blanchet@58177
     5
blanchet@58177
     6
    Title:      Pure/interpretation.ML
blanchet@58177
     7
    Author:     Florian Haftmann and Makarius
blanchet@58177
     8
*)
blanchet@58177
     9
blanchet@58177
    10
signature LOCAL_INTERPRETATION =
blanchet@58177
    11
sig
blanchet@58177
    12
  type T
blanchet@58177
    13
  val result: theory -> T list
blanchet@58177
    14
  val interpretation: (T -> theory -> theory) -> (T -> local_theory -> local_theory) -> theory ->
blanchet@58177
    15
    theory
blanchet@58177
    16
  val data: T -> local_theory -> local_theory
blanchet@58177
    17
  val data_global: T -> theory -> theory
blanchet@58177
    18
  val init: theory -> theory
blanchet@58177
    19
end;
blanchet@58177
    20
blanchet@58177
    21
functor Local_Interpretation(type T val eq: T * T -> bool): LOCAL_INTERPRETATION =
blanchet@58177
    22
struct
blanchet@58177
    23
blanchet@58177
    24
type T = T;
blanchet@58177
    25
blanchet@58177
    26
structure Interp = Theory_Data
blanchet@58177
    27
(
blanchet@58177
    28
  type T =
blanchet@58177
    29
    T list
blanchet@58177
    30
    * ((((T -> theory -> theory) * (T -> local_theory -> local_theory)) * stamp) * T list) list;
blanchet@58177
    31
  val empty = ([], []);
blanchet@58177
    32
  val extend = I;
blanchet@58177
    33
  fun merge ((data1, interps1), (data2, interps2)) : T =
blanchet@58177
    34
    (Library.merge eq (data1, data2),
blanchet@58177
    35
     AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
blanchet@58177
    36
);
blanchet@58177
    37
blanchet@58177
    38
val result = #1 o Interp.get;
blanchet@58177
    39
blanchet@58178
    40
fun consolidate_common g_or_f lift_lthy thy thy_or_lthy =
blanchet@58177
    41
  let
blanchet@58177
    42
    val (data, interps) = Interp.get thy;
blanchet@58178
    43
    val unfinished = interps |> map (fn ((gf, _), xs) =>
blanchet@58178
    44
      (g_or_f gf, if eq_list eq (xs, data) then [] else subtract eq xs data));
blanchet@58182
    45
    val finished = interps |> map (apsnd (K data));
blanchet@58177
    46
  in
blanchet@58182
    47
    if forall (null o #2) unfinished then
blanchet@58182
    48
      NONE
blanchet@58182
    49
    else
blanchet@58182
    50
      SOME (thy_or_lthy |> fold_rev (uncurry fold_rev) unfinished
blanchet@58182
    51
        |> lift_lthy (Interp.put (data, finished)))
blanchet@58177
    52
  end;
blanchet@58177
    53
blanchet@58178
    54
fun consolidate lthy =
blanchet@58178
    55
  consolidate_common snd Local_Theory.background_theory (Proof_Context.theory_of lthy) lthy;
blanchet@58178
    56
fun consolidate_global thy = consolidate_common fst I thy thy;
blanchet@58177
    57
blanchet@58177
    58
fun interpretation g f =
blanchet@58177
    59
  Interp.map (apsnd (cons (((g, f), stamp ()), []))) #> perhaps consolidate_global;
blanchet@58177
    60
blanchet@58177
    61
fun data x = Local_Theory.background_theory (Interp.map (apfst (cons x))) #> perhaps consolidate;
blanchet@58177
    62
fun data_global x = Interp.map (apfst (cons x)) #> perhaps consolidate_global;
blanchet@58177
    63
blanchet@58177
    64
val init = Theory.at_begin consolidate_global;
blanchet@58177
    65
blanchet@58177
    66
end;