src/Pure/interpretation.ML
author wenzelm
Fri Apr 12 14:54:14 2013 +0200 (2013-04-12)
changeset 51700 c8f2bad67dbb
parent 33522 737589bb9bb8
child 58177 166131276380
permissions -rw-r--r--
tuned signature;
tuned comments;
     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 Interpretation(type T val eq: T * T -> bool): INTERPRETATION =
    17 struct
    18 
    19 type T = T;
    20 
    21 structure Interp = Theory_Data
    22 (
    23   type T = T list * (((T -> theory -> theory) * stamp) * T list) list;
    24   val empty = ([], []);
    25   val extend = I;
    26   fun merge ((data1, interps1), (data2, interps2)) : T =
    27     (Library.merge eq (data1, data2),
    28      AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
    29 );
    30 
    31 val result = #1 o Interp.get;
    32 
    33 fun consolidate thy =
    34   let
    35     val (data, interps) = Interp.get thy;
    36     val unfinished = interps |> map (fn ((f, _), xs) =>
    37       (f, if eq_list eq (xs, data) then [] else subtract eq xs data));
    38     val finished = interps |> map (fn (interp, _) => (interp, data));
    39   in
    40     if forall (null o #2) unfinished then NONE
    41     else SOME (thy |> fold_rev (uncurry fold_rev) unfinished |> Interp.put (data, finished))
    42   end;
    43 
    44 fun interpretation f = Interp.map (apsnd (cons ((f, stamp ()), []))) #> perhaps consolidate;
    45 fun data x = Interp.map (apfst (cons x)) #> perhaps consolidate;
    46 
    47 val init = Theory.at_begin consolidate;
    48 
    49 end;
    50