24667

1 
(* Title: Pure/interpretation.ML


2 
ID: $Id$


3 
Author: Florian Haftmann and Makarius


4 


5 
Generic interpretation of theory data.


6 
*)


7 

24711

8 
signature INTERPRETATION =

24667

9 
sig


10 
type T

24711

11 
val result: theory > T list


12 
val interpretation: (T > theory > theory) > theory > theory


13 
val data: T > theory > theory

24667

14 
val init: theory > theory


15 
end;


16 

24711

17 
functor InterpretationFun(type T val eq: T * T > bool): INTERPRETATION =

24667

18 
struct


19 

24711

20 
type T = T;

24667

21 

24711

22 
structure Interp = TheoryDataFun

24667

23 
(

24711

24 
type T = T list * (((T > theory > theory) * stamp) * T list) list;


25 
val empty = ([], []);

24667

26 
val extend = I;


27 
val copy = I;

24711

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));

24667

31 
);


32 

24711

33 
val result = #1 o Interp.get;


34 

24667

35 
fun consolidate thy =

24711

36 
let


37 
val (data, interps) = Interp.get thy;


38 
val unfinished = map (fn ((f, _), xs) => (f, subtract eq xs data)) interps;


39 
val finished = map (fn (interp, _) => (interp, data)) interps;


40 
in


41 
if forall (null o #2) unfinished then NONE


42 
else SOME (thy > fold_rev (uncurry fold_rev) unfinished > Interp.put (data, finished))


43 
end;


44 


45 
fun interpretation f = Interp.map (apsnd (cons ((f, stamp ()), []))) #> perhaps consolidate;


46 
fun data x = Interp.map (apfst (cons x)) #> perhaps consolidate;

24667

47 


48 
val init = Theory.at_begin consolidate;


49 


50 
end;


51 
