diff -r aa750e3a581c -r eb9067371342 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Nov 06 13:12:53 2007 +0100
+++ b/src/Pure/Isar/code.ML	Tue Nov 06 13:12:55 2007 +0100
@@ -3,7 +3,7 @@
     Author:     Florian Haftmann, TU Muenchen
 
 Abstract executable content of theory.  Management of data dependent on
-executable content.
+executable content.  Cache assumes non-concurrent processing of a singly theory.
 *)
 
 signature CODE =
@@ -78,9 +78,37 @@
 structure Code : PRIVATE_CODE =
 struct
 
-(** preliminaries **)
+(** code attributes **)
+
+structure CodeAttr = TheoryDataFun (
+  type T = (string * (Args.T list -> attribute * Args.T list)) list;
+  val empty = [];
+  val copy = I;
+  val extend = I;
+  fun merge _ = AList.merge (op =) (K true);
+);
 
-(* certificate theorems *)
+fun add_attribute (attr as (name, _)) =
+  let
+    fun add_parser ("", parser) attrs = attrs @ [("", parser)]
+      | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
+    fun error "" = error ("Code attribute already declared")
+      | error name = error ("Code attribute " ^ name ^ " already declared")
+  in CodeAttr.map (fn attrs => if AList.defined (op =) attrs name
+    then error name else add_parser attr attrs)
+  end;
+
+val _ =
+  let
+    val code_attr = Attrib.syntax (Scan.peek (fn context =>
+      List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))));
+  in
+    Context.add_setup (Attrib.add_attributes
+      [("code", code_attr, "declare theorems for code generation")])
+  end;
+
+
+(** certificate theorems **)
 
 fun string_of_lthms r = case Susp.peek r
  of SOME thms => (map string_of_thm o rev) thms
@@ -97,27 +125,8 @@
         val thy_ref = Theory.check_thy thy;
       in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
 
-fun merge' _ ([], []) = (false, [])
-  | merge' _ ([], ys) = (true, ys)
-  | merge' eq (xs, ys) = fold_rev
-      (fn y => fn (t, xs) => (t orelse not (member eq xs y), insert eq y xs)) ys (false, xs);
 
-fun merge_alist eq_key eq (xys as (xs, ys)) =
-  if eq_list (eq_pair eq_key eq) (xs, ys)
-  then (false, xs)
-  else (true, AList.merge eq_key eq xys);
-
-val merge_thms = merge' Thm.eq_thm_prop;
-
-fun merge_lthms (r1, r2) =
-  if Susp.same (r1, r2)
-    then (false, r1)
-  else case Susp.peek r1
-   of SOME [] => (true, r2)
-    | _ => case Susp.peek r2
-       of SOME [] => (true, r1)
-        | _ => (apsnd (Susp.delay o K)) (merge_thms (Susp.force r1, Susp.force r2));
-
+(** logical and syntactical specification of executable code **)
 
 (* pairs of (selected, deleted) defining equations *)
 
@@ -152,108 +161,72 @@
 
 fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels;
 
-fun merge_sdthms ((sels1, dels1), (sels2, dels2)) =
+
+(* fundamental melting operations *)
+
+fun melt _ ([], []) = (false, [])
+  | melt _ ([], ys) = (true, ys)
+  | melt eq (xs, ys) = fold_rev
+      (fn y => fn (t, xs) => (t orelse not (member eq xs y), insert eq y xs)) ys (false, xs);
+
+fun melt_alist eq_key eq (xys as (xs, ys)) =
+  if eq_list (eq_pair eq_key eq) (xs, ys)
+  then (false, xs)
+  else (true, AList.merge eq_key eq xys);
+
+val melt_thms = melt Thm.eq_thm_prop;
+
+fun melt_lthms (r1, r2) =
+  if Susp.same (r1, r2)
+    then (false, r1)
+  else case Susp.peek r1
+   of SOME [] => (true, r2)
+    | _ => case Susp.peek r2
+       of SOME [] => (true, r1)
+        | _ => (apsnd (Susp.delay o K)) (melt_thms (Susp.force r1, Susp.force r2));
+
+fun melt_sdthms ((sels1, dels1), (sels2, dels2)) =
   let
-    val (dels_t, dels) = merge_thms (dels1, dels2);
+    val (dels_t, dels) = melt_thms (dels1, dels2);
   in if dels_t
     then let
-      val (_, sels) = merge_thms
+      val (_, sels) = melt_thms
         (subtract Thm.eq_thm_prop dels2 (Susp.force sels1), Susp.force sels2);
-      val (_, dels) = merge_thms
+      val (_, dels) = melt_thms
         (subtract Thm.eq_thm_prop (Susp.force sels2) dels1, dels2);
     in (true, ((Susp.delay o K) sels, dels)) end
     else let
-      val (sels_t, sels) = merge_lthms (sels1, sels2);
+      val (sels_t, sels) = melt_lthms (sels1, sels2);
     in (sels_t, (sels, dels)) end
   end;
 
 
-(* code attributes *)
-
-structure CodeAttr = TheoryDataFun (
-  type T = (string * (Args.T list -> attribute * Args.T list)) list;
-  val empty = [];
-  val copy = I;
-  val extend = I;
-  fun merge _ = AList.merge (op =) (K true);
-);
-
-fun add_attribute (attr as (name, _)) =
-  let
-    fun add_parser ("", parser) attrs = attrs @ [("", parser)]
-      | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
-    fun error "" = error ("Code attribute already declared")
-      | error name = error ("Code attribute " ^ name ^ " already declared")
-  in CodeAttr.map (fn attrs => if AList.defined (op =) attrs name
-    then error name else add_parser attr attrs)
-  end;
-
-val _ =
-  let
-    val code_attr = Attrib.syntax (Scan.peek (fn context =>
-      List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))));
-  in
-    Context.add_setup (Attrib.add_attributes
-      [("code", code_attr, "declare theorems for code generation")])
-  end;
-
-
-
-(** exeuctable content **)
+(* specification data *)
 
-datatype thmproc = Preproc of {
-  inlines: thm list,
-  inline_procs: (string * (serial * (theory -> cterm list -> thm list))) list,
-  preprocs: (string * (serial * (theory -> thm list -> thm list))) list,
-  posts: thm list
-};
-
-fun mk_thmproc (((inlines, inline_procs), preprocs), posts) =
-  Preproc { inlines = inlines, inline_procs = inline_procs, preprocs = preprocs,
-    posts = posts };
-fun map_thmproc f (Preproc { inlines, inline_procs, preprocs, posts }) =
-  mk_thmproc (f (((inlines, inline_procs), preprocs), posts));
-fun merge_thmproc (Preproc { inlines = inlines1, inline_procs = inline_procs1,
-    preprocs = preprocs1, posts = posts1 },
-  Preproc { inlines = inlines2, inline_procs = inline_procs2,
-      preprocs = preprocs2, posts= posts2 }) =
-    let
-      val (touched1, inlines) = merge_thms (inlines1, inlines2);
-      val (touched2, inline_procs) = merge_alist (op =) (eq_fst (op =)) (inline_procs1, inline_procs2);
-      val (touched3, preprocs) = merge_alist (op =) (eq_fst (op =)) (preprocs1, preprocs2);
-      val (_, posts) = merge_thms (posts1, posts2);
-    in (touched1 orelse touched2 orelse touched3,
-      mk_thmproc (((inlines, inline_procs), preprocs), posts)) end;
-
-fun join_func_thms (tabs as (tab1, tab2)) =
+fun melt_funcs tabs =
   let
-    val cs1 = Symtab.keys tab1;
-    val cs2 = Symtab.keys tab2;
-    val cs' = filter (member (op =) cs2) cs1;
-    val cs'' = subtract (op =) cs' cs1 @ subtract (op =) cs' cs2;
-    val cs''' = ref [] : string list ref;
-    fun merge c x = let val (touched, thms') = merge_sdthms x in
-      (if touched then cs''' := cons c (!cs''') else (); thms') end;
-  in (cs'' @ !cs''', Symtab.join merge tabs) end;
+    val tab' = Symtab.join (fn _ => fn ((_, a), (_, b)) => melt_sdthms (a, b)) tabs;
+    val touched = Symtab.fold (fn (c, (true, _)) => insert (op =) c | _ => I) tab' [];
+  in (touched, tab') end;
 
 val eq_string = op = : string * string -> bool;
 fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = 
   gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
     andalso gen_eq_set (eq_fst eq_string) (cs1, cs2);
-fun merge_dtyps (tabs as (tab1, tab2)) =
+fun melt_dtyps (tabs as (tab1, tab2)) =
   let
     val tycos1 = Symtab.keys tab1;
     val tycos2 = Symtab.keys tab2;
     val tycos' = filter (member eq_string tycos2) tycos1;
-    val new_types = not (gen_eq_set (op =) (tycos1, tycos2));
-    val diff_types = not (gen_eq_set (eq_pair (op =) eq_dtyp)
+    val touched = not (gen_eq_set (op =) (tycos1, tycos2)
+      andalso gen_eq_set (eq_pair (op =) eq_dtyp)
       (AList.make (the o Symtab.lookup tab1) tycos',
        AList.make (the o Symtab.lookup tab2) tycos'));
     fun join _ (cos as (_, cos2)) = if eq_dtyp cos
       then raise Symtab.SAME else cos2;
-  in ((new_types, diff_types), Symtab.join join tabs) end;
+  in (touched, Symtab.join join tabs) end;
 
-fun merge_cases ((cases1, undefs1), (cases2, undefs2)) =
+fun melt_cases ((cases1, undefs1), (cases2, undefs2)) =
   let
     val touched1 = subtract (op =) (Symtab.keys cases1) (Symtab.keys cases2)
       @ subtract (op =) (Symtab.keys cases2) (Symtab.keys cases1);
@@ -266,7 +239,7 @@
   end;
 
 datatype spec = Spec of {
-  funcs: sdthms Symtab.table,
+  funcs: (bool * sdthms) Symtab.table,
   dtyps: ((string * sort) list * (string * typ list) list) Symtab.table,
   cases: (int * string list) Symtab.table * unit Symtab.table
 };
@@ -275,16 +248,43 @@
   Spec { funcs = funcs, dtyps = dtyps, cases = cases };
 fun map_spec f (Spec { funcs = funcs, dtyps = dtyps, cases = cases }) =
   mk_spec (f (funcs, (dtyps, cases)));
-fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 },
+fun melt_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = cases1 },
   Spec { funcs = funcs2, dtyps = dtyps2, cases = cases2 }) =
   let
-    val (touched_cs, funcs) = join_func_thms (funcs1, funcs2);
-    val ((new_types, diff_types), dtyps) = merge_dtyps (dtyps1, dtyps2);
-    val (touched_cases, cases) = merge_cases (cases1, cases2);
-    val touched = if new_types orelse diff_types then NONE else
-      SOME (fold (insert (op =)) touched_cases touched_cs);
+    val (touched_funcs, funcs) = melt_funcs (funcs1, funcs2);
+    val (touched_dtyps, dtyps) = melt_dtyps (dtyps1, dtyps2);
+    val (touched_cases, cases) = melt_cases (cases1, cases2);
+    val touched = if touched_dtyps then NONE else
+      SOME (fold (insert (op =)) touched_cases touched_funcs);
   in (touched, mk_spec (funcs, (dtyps, cases))) end;
 
+
+(* pre- and postprocessor *)
+
+datatype thmproc = Thmproc of {
+  inlines: thm list,
+  inline_procs: (string * (serial * (theory -> cterm list -> thm list))) list,
+  preprocs: (string * (serial * (theory -> thm list -> thm list))) list,
+  posts: thm list
+};
+
+fun mk_thmproc (((inlines, inline_procs), preprocs), posts) =
+  Thmproc { inlines = inlines, inline_procs = inline_procs, preprocs = preprocs,
+    posts = posts };
+fun map_thmproc f (Thmproc { inlines, inline_procs, preprocs, posts }) =
+  mk_thmproc (f (((inlines, inline_procs), preprocs), posts));
+fun melt_thmproc (Thmproc { inlines = inlines1, inline_procs = inline_procs1,
+    preprocs = preprocs1, posts = posts1 },
+  Thmproc { inlines = inlines2, inline_procs = inline_procs2,
+      preprocs = preprocs2, posts= posts2 }) =
+    let
+      val (touched1, inlines) = melt_thms (inlines1, inlines2);
+      val (touched2, inline_procs) = melt_alist (op =) (eq_fst (op =)) (inline_procs1, inline_procs2);
+      val (touched3, preprocs) = melt_alist (op =) (eq_fst (op =)) (preprocs1, preprocs2);
+      val (_, posts) = melt_thms (posts1, posts2);
+    in (touched1 orelse touched2 orelse touched3,
+      mk_thmproc (((inlines, inline_procs), preprocs), posts)) end;
+
 datatype exec = Exec of {
   thmproc: thmproc,
   spec: spec
@@ -294,17 +294,17 @@
   Exec { thmproc = thmproc, spec = spec };
 fun map_exec f (Exec { thmproc = thmproc, spec = spec }) =
   mk_exec (f (thmproc, spec));
-fun merge_exec (Exec { thmproc = thmproc1, spec = spec1 },
+fun melt_exec (Exec { thmproc = thmproc1, spec = spec1 },
   Exec { thmproc = thmproc2, spec = spec2 }) =
   let
-    val (touched', thmproc) = merge_thmproc (thmproc1, thmproc2);
-    val (touched_cs, spec) = merge_spec (spec1, spec2);
+    val (touched', thmproc) = melt_thmproc (thmproc1, thmproc2);
+    val (touched_cs, spec) = melt_spec (spec1, spec2);
     val touched = if touched' then NONE else touched_cs;
   in (touched, mk_exec (thmproc, spec)) end;
 val empty_exec = mk_exec (mk_thmproc ((([], []), []), []),
   mk_spec (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty))));
 
-fun the_thmproc (Exec { thmproc = Preproc x, ...}) = x;
+fun the_thmproc (Exec { thmproc = Thmproc x, ...}) = x;
 fun the_spec (Exec { spec = Spec x, ...}) = x;
 val the_funcs = #funcs o the_spec;
 val the_dtyps = #dtyps o the_spec;
@@ -357,7 +357,7 @@
 end; (*local*)
 
 
-(* theory store *)
+(** theory store **)
 
 local
 
@@ -371,7 +371,7 @@
   val extend = copy;
   fun merge pp ((exec1, data1), (exec2, data2)) =
     let
-      val (touched, exec) = merge_exec (exec1, exec2);
+      val (touched, exec) = melt_exec (exec1, exec2);
       val data1' = invoke_purge_all NONE touched (! data1);
       val data2' = invoke_purge_all NONE touched (! data2);
       val data = invoke_merge_all pp (data1', data2');
@@ -452,6 +452,7 @@
     val preprocs = (map fst o #preprocs o the_thmproc) exec;
     val funs = the_funcs exec
       |> Symtab.dest
+      |> (map o apsnd) snd
       |> (map o apfst) (CodeUnit.string_of_const thy)
       |> sort (string_ord o pairself fst);
     val dtyps = the_dtyps exec
@@ -549,7 +550,7 @@
     val funcs = classparams
       |> map (fn c => Class.inst_const thy (c, tyco))
       |> map (Symtab.lookup ((the_funcs o the_exec) thy))
-      |> (map o Option.map) (Susp.force o fst)
+      |> (map o Option.map) (Susp.force o fst o snd)
       |> maps these
       |> map (Thm.transfer thy)
     fun sorts_of [Type (_, tys)] = map (snd o dest_TVar) tys
@@ -710,7 +711,7 @@
       else ();
   in
     (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default
-      (c, (Susp.value [], [])) (add_thm func)) thy
+      (c, (false, (Susp.value [], []))) (apsnd (add_thm func))) thy
   end;
 
 fun add_liberal_func thm thy =
@@ -722,7 +723,7 @@
           then thy
           else map_exec_purge (SOME [c]) (map_funcs
             (Symtab.map_default
-              (c, (Susp.value [], [])) (add_thm func))) thy
+              (c, (false, (Susp.value [], []))) (apsnd (add_thm func)))) thy
         end
     | NONE => thy;
 
@@ -735,7 +736,7 @@
           then thy
           else map_exec_purge (SOME [c]) (map_funcs
           (Symtab.map_default
-            (c, (Susp.value [], [])) (add_thm func))) thy
+            (c, (false, (Susp.value [], []))) (apsnd (add_thm func)))) thy
         end
     | NONE => thy;
 
@@ -744,7 +745,7 @@
    of SOME func => let
           val c = const_of_func thy func;
         in map_exec_purge (SOME [c]) (map_funcs
-          (Symtab.map_entry c (del_thm func))) thy
+          (Symtab.map_entry c (apsnd (del_thm func)))) thy
         end
     | NONE => thy;
 
@@ -754,8 +755,9 @@
       (*FIXME must check compatibility with sort algebra;
         alas, naive checking results in non-termination!*)
   in
-    map_exec_purge (SOME [const]) (map_funcs (Symtab.map_default (const, (Susp.value [], []))
-      (add_lthms lthms'))) thy
+    map_exec_purge (SOME [const])
+      (map_funcs (Symtab.map_default (const, (false, (Susp.value [], [])))
+      (apsnd (add_lthms lthms')))) thy
   end;
 
 val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute
@@ -925,7 +927,7 @@
 
 fun get_funcs thy const =
   Symtab.lookup ((the_funcs o the_exec) thy) const
-  |> Option.map (Susp.force o fst)
+  |> Option.map (Susp.force o fst o snd)
   |> these
   |> map (Thm.transfer thy);