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