obsolete;
authorwenzelm
Mon Oct 13 20:51:48 2014 +0200 (2014-10-13)
changeset 586644e4a4c758f9c
parent 58663 93d177cd03e2
child 58665 50b229a5a097
obsolete;
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/interpretation.ML
     1.1 --- a/src/Pure/ROOT	Mon Oct 13 20:29:30 2014 +0200
     1.2 +++ b/src/Pure/ROOT	Mon Oct 13 20:51:48 2014 +0200
     1.3 @@ -228,7 +228,6 @@
     1.4      "global_theory.ML"
     1.5      "goal.ML"
     1.6      "goal_display.ML"
     1.7 -    "interpretation.ML"
     1.8      "item_net.ML"
     1.9      "library.ML"
    1.10      "logic.ML"
     2.1 --- a/src/Pure/ROOT.ML	Mon Oct 13 20:29:30 2014 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Mon Oct 13 20:51:48 2014 +0200
     2.3 @@ -181,7 +181,6 @@
     2.4  use "pattern.ML";
     2.5  use "unify.ML";
     2.6  use "theory.ML";
     2.7 -use "interpretation.ML";
     2.8  use "proofterm.ML";
     2.9  use "thm.ML";
    2.10  use "more_thm.ML";
     3.1 --- a/src/Pure/interpretation.ML	Mon Oct 13 20:29:30 2014 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,49 +0,0 @@
     3.4 -(*  Title:      Pure/interpretation.ML
     3.5 -    Author:     Florian Haftmann and Makarius
     3.6 -
     3.7 -Generic interpretation of theory data.
     3.8 -*)
     3.9 -
    3.10 -signature INTERPRETATION =
    3.11 -sig
    3.12 -  type T
    3.13 -  val result: theory -> T list
    3.14 -  val interpretation: (T -> theory -> theory) -> theory -> theory
    3.15 -  val data: T -> theory -> theory
    3.16 -  val init: theory -> theory
    3.17 -end;
    3.18 -
    3.19 -functor Interpretation(type T val eq: T * T -> bool): INTERPRETATION =
    3.20 -struct
    3.21 -
    3.22 -type T = T;
    3.23 -
    3.24 -structure Interp = Theory_Data
    3.25 -(
    3.26 -  type T = T list * (((T -> theory -> theory) * stamp) * T list) list;
    3.27 -  val empty = ([], []);
    3.28 -  val extend = I;
    3.29 -  fun merge ((data1, interps1), (data2, interps2)) : T =
    3.30 -    (Library.merge eq (data1, data2),
    3.31 -     AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
    3.32 -);
    3.33 -
    3.34 -val result = #1 o Interp.get;
    3.35 -
    3.36 -fun consolidate thy =
    3.37 -  let
    3.38 -    val (data, interps) = Interp.get thy;
    3.39 -    val unfinished = interps |> map (fn ((f, _), xs) =>
    3.40 -      (f, if eq_list eq (xs, data) then [] else subtract eq xs data));
    3.41 -    val finished = interps |> map (fn (interp, _) => (interp, data));
    3.42 -  in
    3.43 -    if forall (null o #2) unfinished then NONE
    3.44 -    else SOME (thy |> fold_rev (uncurry fold_rev) unfinished |> Interp.put (data, finished))
    3.45 -  end;
    3.46 -
    3.47 -fun interpretation f = Interp.map (apsnd (cons ((f, stamp ()), []))) #> perhaps consolidate;
    3.48 -fun data x = Interp.map (apfst (cons x)) #> perhaps consolidate;
    3.49 -
    3.50 -val init = Theory.at_begin consolidate;
    3.51 -
    3.52 -end;