src/Pure/interpretation.ML
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24711 e8bba7723858
child 24857 2dde4189a055
permissions -rw-r--r--
Name.uu, Name.aT;
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@24711
    38
    val unfinished = map (fn ((f, _), xs) => (f, subtract eq xs data)) interps;
wenzelm@24711
    39
    val finished = map (fn (interp, _) => (interp, data)) interps;
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