src/Pure/interpretation.ML
author wenzelm
Thu Sep 20 20:56:54 2007 +0200 (2007-09-20)
changeset 24667 9f29588d57d5
child 24711 e8bba7723858
permissions -rw-r--r--
Generic interpretation of theory data.
     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 THEORY_INTERPRETATOR =
     9 sig
    10   type T
    11   type interpretator = T list -> theory -> theory
    12   val add_those: T list -> theory -> theory
    13   val all_those: theory -> T list
    14   val add_interpretator: interpretator -> theory -> theory
    15   val init: theory -> theory
    16 end;
    17 
    18 signature THEORY_INTERPRETATOR_KEY =
    19 sig
    20   type T
    21   val eq: T * T -> bool
    22 end;
    23 
    24 functor TheoryInterpretatorFun(Key: THEORY_INTERPRETATOR_KEY) : THEORY_INTERPRETATOR =
    25 struct
    26 
    27 open Key;
    28 
    29 type interpretator = T list -> theory -> theory;
    30 
    31 fun apply ips x = fold_rev (fn (_, f) => f x) ips;
    32 
    33 structure InterpretatorData = TheoryDataFun
    34 (
    35   type T = ((serial * interpretator) list * T list) * (theory -> theory) list;
    36   val empty = (([], []), []);
    37   val extend = I;
    38   val copy = I;
    39   fun merge pp (((interpretators1, done1), upd1), ((interpretators2, done2), upd2)) =
    40     let
    41       fun diff (interpretators1 : (serial * interpretator) list, done1)
    42         (interpretators2, done2) = let
    43           val interpretators = subtract (eq_fst (op =)) interpretators1 interpretators2;
    44           val undone = subtract eq done2 done1;
    45         in if null interpretators then [] else [apply interpretators undone] end;
    46       val interpretators = AList.merge (op =) (K true) (interpretators1, interpretators2);
    47       val done = Library.merge eq (done1, done2);
    48       val upd_new = diff (interpretators2, done2) (interpretators1, done1)
    49         @ diff (interpretators1, done1) (interpretators2, done2);
    50       val upd = upd1 @ upd2 @ upd_new;
    51     in ((interpretators, done), upd) end;
    52 );
    53 
    54 fun consolidate thy =
    55   (case #2 (InterpretatorData.get thy) of
    56     [] => NONE
    57   | upd => SOME (thy |> Library.apply upd |> (InterpretatorData.map o apsnd) (K [])));
    58 
    59 val init = Theory.at_begin consolidate;
    60 
    61 fun add_those xs thy =
    62   let
    63     val ((interpretators, _), _) = InterpretatorData.get thy;
    64   in
    65     thy
    66     |> apply interpretators xs
    67     |> (InterpretatorData.map o apfst o apsnd) (append xs)
    68   end;
    69 
    70 val all_those = snd o fst o InterpretatorData.get;
    71 
    72 fun add_interpretator interpretator thy =
    73   let
    74     val ((interpretators, xs), _) = InterpretatorData.get thy;
    75   in
    76     thy
    77     |> interpretator (rev xs)
    78     |> (InterpretatorData.map o apfst o apfst) (cons (serial (), interpretator))
    79   end;
    80 
    81 end;
    82