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