src/Pure/interpretation.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 24711 e8bba7723858
child 24857 2dde4189a055
permissions -rw-r--r--
filtering out some package theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24667
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/interpretation.ML
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
     3
    Author:     Florian Haftmann and Makarius
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
     4
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
     5
Generic interpretation of theory data.
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
     6
*)
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
     7
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
     8
signature INTERPRETATION =
24667
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
     9
sig
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    10
  type T
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    11
  val result: theory -> T list
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    12
  val interpretation: (T -> theory -> theory) -> theory -> theory
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    13
  val data: T -> theory -> theory
24667
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    14
  val init: theory -> theory
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    15
end;
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    16
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    17
functor InterpretationFun(type T val eq: T * T -> bool): INTERPRETATION =
24667
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    18
struct
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    19
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    20
type T = T;
24667
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    21
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    22
structure Interp = TheoryDataFun
24667
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    23
(
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    24
  type T = T list * (((T -> theory -> theory) * stamp) * T list) list;
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    25
  val empty = ([], []);
24667
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    26
  val extend = I;
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    27
  val copy = I;
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    28
  fun merge _ ((data1, interps1), (data2, interps2)) : T =
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    29
    (Library.merge eq (data1, data2),
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    30
     AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
24667
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    31
);
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    32
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    33
val result = #1 o Interp.get;
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    34
24667
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    35
fun consolidate thy =
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    36
  let
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    37
    val (data, interps) = Interp.get thy;
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    38
    val unfinished = map (fn ((f, _), xs) => (f, subtract eq xs data)) interps;
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    39
    val finished = map (fn (interp, _) => (interp, data)) interps;
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    40
  in
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    41
    if forall (null o #2) unfinished then NONE
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    42
    else SOME (thy |> fold_rev (uncurry fold_rev) unfinished |> Interp.put (data, finished))
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    43
  end;
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    44
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    45
fun interpretation f = Interp.map (apsnd (cons ((f, stamp ()), []))) #> perhaps consolidate;
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24667
diff changeset
    46
fun data x = Interp.map (apfst (cons x)) #> perhaps consolidate;
24667
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    47
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    48
val init = Theory.at_begin consolidate;
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    49
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    50
end;
9f29588d57d5 Generic interpretation of theory data.
wenzelm
parents:
diff changeset
    51