src/Pure/interpretation.ML
author wenzelm
Wed Jan 21 23:21:44 2009 +0100 (2009-01-21)
changeset 29606 fedb8be05f24
parent 24857 2dde4189a055
child 33314 53d49370f7af
permissions -rw-r--r--
removed Ids;
wenzelm@24667
     1
(*  Title:      Pure/interpretation.ML
wenzelm@24667
     2
    Author:     Florian Haftmann and Makarius
wenzelm@24667
     3
wenzelm@24667
     4
Generic interpretation of theory data.
wenzelm@24667
     5
*)
wenzelm@24667
     6
wenzelm@24711
     7
signature INTERPRETATION =
wenzelm@24667
     8
sig
wenzelm@24667
     9
  type T
wenzelm@24711
    10
  val result: theory -> T list
wenzelm@24711
    11
  val interpretation: (T -> theory -> theory) -> theory -> theory
wenzelm@24711
    12
  val data: T -> theory -> theory
wenzelm@24667
    13
  val init: theory -> theory
wenzelm@24667
    14
end;
wenzelm@24667
    15
wenzelm@24711
    16
functor InterpretationFun(type T val eq: T * T -> bool): INTERPRETATION =
wenzelm@24667
    17
struct
wenzelm@24667
    18
wenzelm@24711
    19
type T = T;
wenzelm@24667
    20
wenzelm@24711
    21
structure Interp = TheoryDataFun
wenzelm@24667
    22
(
wenzelm@24711
    23
  type T = T list * (((T -> theory -> theory) * stamp) * T list) list;
wenzelm@24711
    24
  val empty = ([], []);
wenzelm@24667
    25
  val extend = I;
wenzelm@24667
    26
  val copy = I;
wenzelm@24711
    27
  fun merge _ ((data1, interps1), (data2, interps2)) : T =
wenzelm@24711
    28
    (Library.merge eq (data1, data2),
wenzelm@24711
    29
     AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
wenzelm@24667
    30
);
wenzelm@24667
    31
wenzelm@24711
    32
val result = #1 o Interp.get;
wenzelm@24711
    33
wenzelm@24667
    34
fun consolidate thy =
wenzelm@24711
    35
  let
wenzelm@24711
    36
    val (data, interps) = Interp.get thy;
wenzelm@24857
    37
    val unfinished = interps |> map (fn ((f, _), xs) =>
wenzelm@24857
    38
      (f, if eq_list eq (xs, data) then [] else subtract eq xs data));
wenzelm@24857
    39
    val finished = interps |> map (fn (interp, _) => (interp, data));
wenzelm@24711
    40
  in
wenzelm@24711
    41
    if forall (null o #2) unfinished then NONE
wenzelm@24711
    42
    else SOME (thy |> fold_rev (uncurry fold_rev) unfinished |> Interp.put (data, finished))
wenzelm@24711
    43
  end;
wenzelm@24711
    44
wenzelm@24711
    45
fun interpretation f = Interp.map (apsnd (cons ((f, stamp ()), []))) #> perhaps consolidate;
wenzelm@24711
    46
fun data x = Interp.map (apfst (cons x)) #> perhaps consolidate;
wenzelm@24667
    47
wenzelm@24667
    48
val init = Theory.at_begin consolidate;
wenzelm@24667
    49
wenzelm@24667
    50
end;
wenzelm@24667
    51