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