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