src/Pure/interpretation.ML
author wenzelm
Fri May 28 20:41:23 2010 +0200 (2010-05-28)
changeset 37174 6feaab4fc27d
parent 33522 737589bb9bb8
child 58177 166131276380
permissions -rw-r--r--
assume given SCALA_HOME, e.g. from component settings or external setup;
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@33314
    16
functor Interpretation(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@33522
    21
structure Interp = Theory_Data
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@33522
    26
  fun merge ((data1, interps1), (data2, interps2)) : T =
wenzelm@24711
    27
    (Library.merge eq (data1, data2),
wenzelm@24711
    28
     AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
wenzelm@24667
    29
);
wenzelm@24667
    30
wenzelm@24711
    31
val result = #1 o Interp.get;
wenzelm@24711
    32
wenzelm@24667
    33
fun consolidate thy =
wenzelm@24711
    34
  let
wenzelm@24711
    35
    val (data, interps) = Interp.get thy;
wenzelm@24857
    36
    val unfinished = interps |> map (fn ((f, _), xs) =>
wenzelm@24857
    37
      (f, if eq_list eq (xs, data) then [] else subtract eq xs data));
wenzelm@24857
    38
    val finished = interps |> map (fn (interp, _) => (interp, data));
wenzelm@24711
    39
  in
wenzelm@24711
    40
    if forall (null o #2) unfinished then NONE
wenzelm@24711
    41
    else SOME (thy |> fold_rev (uncurry fold_rev) unfinished |> Interp.put (data, finished))
wenzelm@24711
    42
  end;
wenzelm@24711
    43
wenzelm@24711
    44
fun interpretation f = Interp.map (apsnd (cons ((f, stamp ()), []))) #> perhaps consolidate;
wenzelm@24711
    45
fun data x = Interp.map (apfst (cons x)) #> perhaps consolidate;
wenzelm@24667
    46
wenzelm@24667
    47
val init = Theory.at_begin consolidate;
wenzelm@24667
    48
wenzelm@24667
    49
end;
wenzelm@24667
    50