src/Pure/interpretation.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 24711 e8bba7723858
child 24857 2dde4189a055
permissions -rw-r--r--
filtering out some package theorems

(*  Title:      Pure/interpretation.ML
    ID:         $Id$
    Author:     Florian Haftmann and Makarius

Generic interpretation of theory data.
*)

signature INTERPRETATION =
sig
  type T
  val result: theory -> T list
  val interpretation: (T -> theory -> theory) -> theory -> theory
  val data: T -> theory -> theory
  val init: theory -> theory
end;

functor InterpretationFun(type T val eq: T * T -> bool): INTERPRETATION =
struct

type T = T;

structure Interp = TheoryDataFun
(
  type T = T list * (((T -> theory -> theory) * stamp) * T list) list;
  val empty = ([], []);
  val extend = I;
  val copy = I;
  fun merge _ ((data1, interps1), (data2, interps2)) : T =
    (Library.merge eq (data1, data2),
     AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
);

val result = #1 o Interp.get;

fun consolidate thy =
  let
    val (data, interps) = Interp.get thy;
    val unfinished = map (fn ((f, _), xs) => (f, subtract eq xs data)) interps;
    val finished = map (fn (interp, _) => (interp, data)) interps;
  in
    if forall (null o #2) unfinished then NONE
    else SOME (thy |> fold_rev (uncurry fold_rev) unfinished |> Interp.put (data, finished))
  end;

fun interpretation f = Interp.map (apsnd (cons ((f, stamp ()), []))) #> perhaps consolidate;
fun data x = Interp.map (apfst (cons x)) #> perhaps consolidate;

val init = Theory.at_begin consolidate;

end;