tuned

--- a/src/HOL/Tools/datatype_codegen.ML	Fri Oct 13 16:52:46 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Fri Oct 13 16:52:47 2006 +0200
@@ -336,8 +336,6 @@
     val abs = Name.names Name.context "a" (Library.drop (length ts, tys));
     val (ts', t) = split_last (ts @ map Free abs);
     val (tys', sty) = split_last tys;
-    fun freenames_of t = fold_aterms
-      (fn Free (v, _) => insert (op =) v | _ => I) t [];
     fun dest_case ((c, tys_decl), ty) t =
       let
         val (vs, t') = Term.strip_abs_eta (length tys_decl) t;

--- a/src/Pure/Tools/codegen_package.ML	Fri Oct 13 16:52:46 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Fri Oct 13 16:52:47 2006 +0200
@@ -21,6 +21,8 @@
     -> ((string * typ) list * ((term * typ) * (term * term) list)) option)
     -> appgen;
   val appgen_let: appgen;
+
+  val timing: bool ref;
 end;
 
 structure CodegenPackage : CODEGEN_PACKAGE =
@@ -173,6 +175,7 @@
             |-> (fn (tyco, tys) => pair (tyco `%% tys));
 
 exception CONSTRAIN of (string * typ) * typ;
+val timing = ref false;
 
 fun exprgen_typinst thy (algbr as ((proj_sort, algebra), consts)) funcgr strct (ty_ctxt, sort_decl) trns =
   let
@@ -271,6 +274,8 @@
         (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) (c, tys))
        of eq_thms as eq_thm :: _ =>
             let
+              val timeap = if !timing then Output.timeap_msg ("time for " ^ c')
+                else I;
               val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
               val ty = (Logic.unvarifyT o CodegenData.typ_func thy) eq_thm;
               val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
@@ -283,7 +288,7 @@
             in
               trns
               |> CodegenThingol.message msg (fn trns => trns
-              |> fold_map (exprgen_eq o dest_eqthm) eq_thms
+              |> timeap (fold_map (exprgen_eq o dest_eqthm) eq_thms)
               ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
               ||>> exprgen_type thy algbr funcgr strct ty
               |-> (fn ((eqs, vs), ty) => succeed (CodegenThingol.Fun (eqs, (vs, ty)))))
@@ -397,8 +402,7 @@
   case try (int_of_numeral thy) (list_comb (Const c, ts))
    of SOME i =>
         trns
-        |> appgen_default thy algbr funcgr strct app
-        |-> (fn t => pair (CodegenThingol.INum (i, t)))
+        |> pair (CodegenThingol.INum i)
     | NONE =>
         trns
         |> appgen_default thy algbr funcgr strct app;
@@ -408,14 +412,16 @@
    of SOME i =>
         trns
         |> exprgen_type thy algbr funcgr strct ty
-        ||>> appgen_default thy algbr funcgr strct app
-        |-> (fn (_, t0) => pair (IChar (chr i, t0)))
+        |-> (fn _ => pair (IChar (chr i)))
     | NONE =>
         trns
         |> appgen_default thy algbr funcgr strct app;
 
+val debug_term = ref (Bound 0);
+
 fun appgen_case dest_case_expr thy algbr funcgr strct (app as (c_ty, ts)) trns =
   let
+    val _ = debug_term := list_comb (Const c_ty, ts);
     val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
     fun fold_map_aterms f (t $ u) s =
           s
@@ -427,16 +433,23 @@
           |> fold_map_aterms f t
           |-> (fn t' => pair (Abs (v, ty, t')))
       | fold_map_aterms f a s = f a s;
-    fun purify_term_frees (Free (v, ty)) ctxt = 
+    fun purify_term_frees (Free (v, ty)) (renaming, ctxt) = 
           let
             val ([v'], ctxt') = Name.variants [CodegenNames.purify_var v] ctxt;
-          in (Free (v, ty), ctxt') end
+            val renaming' = if v <> v' then Symtab.update (v, v') renaming else renaming;
+          in (Free (v', ty), (renaming', ctxt')) end
       | purify_term_frees t ctxt = (t, ctxt);
     fun clausegen (raw_dt, raw_bt) trns =
       let
-        val ((dt, bt), _) = Name.context
-          |> fold_map_aterms purify_term_frees raw_dt
-          ||>> fold_map_aterms purify_term_frees raw_bt;
+        val d_vs = map fst (Term.add_frees raw_dt []);
+        val b_vs = map fst (Term.add_frees raw_bt []);
+        val (dt, (renaming, ctxt)) =
+          Name.context
+          |> fold Name.declare (subtract (op =) d_vs b_vs)
+          |> pair Symtab.empty
+          |> fold_map_aterms purify_term_frees raw_dt;
+        val bt = map_aterms (fn t as Free (v, ty) => Free (perhaps (Symtab.lookup renaming) v, ty)
+                              | t => t) raw_bt;
       in
         trns
         |> exprgen_term thy algbr funcgr strct dt
@@ -447,21 +460,19 @@
     |> exprgen_term thy algbr funcgr strct st
     ||>> exprgen_type thy algbr funcgr strct sty
     ||>> fold_map clausegen ds
-    ||>> appgen_default thy algbr funcgr strct app
-    |-> (fn (((se, sty), ds), e0) => pair (ICase (((se, sty), ds), e0)))
+    |-> (fn ((se, sty), ds) => pair (ICase ((se, sty), ds)))
   end;
 
 fun appgen_let thy algbr funcgr strct (app as (_, [st, ct])) trns =
   trns
   |> exprgen_term thy algbr funcgr strct ct
   ||>> exprgen_term thy algbr funcgr strct st
-  ||>> appgen_default thy algbr funcgr strct app
-  |-> (fn (((v, ty) `|-> be, se), e0) =>
-            pair (ICase (((se, ty), case be
-              of ICase (((IVar w, _), ds), _) => if v = w then ds else [(IVar v, be)]
+  |-> (fn ((v, ty) `|-> be, se) =>
+            pair (ICase ((se, ty), case be
+              of ICase ((IVar w, _), ds) => if v = w then ds else [(IVar v, be)]
                | _ => [(IVar v, be)]
-            ), e0))
-        | (_, e0) => pair e0);
+            ))
+        | _ => appgen_default thy algbr funcgr strct app);
 
 fun add_appconst (c, appgen) thy =
   let
@@ -630,7 +641,7 @@
      of [] => NONE
       | xs => SOME xs;
     val seris' = map_filter (fn (target, args as _ :: _) =>
-      SOME (CodegenSerializer.get_serializer thy (target, args)) | _ => NONE) seris;
+      SOME (CodegenSerializer.get_serializer thy target args) | _ => NONE) seris;
     fun generate' thy = case cs
      of [] => []
       | _ =>

--- a/src/Pure/Tools/codegen_thingol.ML	Fri Oct 13 16:52:46 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Fri Oct 13 16:52:47 2006 +0200
@@ -28,12 +28,11 @@
     | IVar of vname
     | `$ of iterm * iterm
     | `|-> of (vname * itype) * iterm
-    | INum of IntInf.int * iterm
-    | IChar of string (*length one!*) * iterm
-    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
-        (*((discriminendum term (td), discriminendum type (ty)),
-                [(selector pattern (p), body term (t))] (bs)),
-                pure term (t0))*)
+    | INum of IntInf.int
+    | IChar of string (*length one!*)
+    | ICase of (iterm * itype) * (iterm * iterm) list;
+        (*(discriminendum term (td), discriminendum type (ty)),
+                [(selector pattern (p), body term (t))] (bs))*)
   val `--> : itype list * itype -> itype;
   val `$$ : iterm * iterm list -> iterm;
   val `|--> : (vname * itype) list * iterm -> iterm;
@@ -47,11 +46,10 @@
   val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
   val unfold_fun: itype -> itype list * itype;
   val unfold_app: iterm -> iterm * iterm list;
-  val unfold_abs: iterm -> (iterm * itype) list * iterm;
+  val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm;
   val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
   val unfold_const_app: iterm ->
     ((string * (inst list list * itype)) * iterm list) option;
-  val map_pure: (iterm -> 'a) -> iterm -> 'a;
   val eta_expand: (string * (inst list list * itype)) * iterm list -> int -> iterm;
   val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
   val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
@@ -72,9 +70,10 @@
   val empty_code: code;
   val get_def: code -> string -> def;
   val merge_code: code * code -> code;
-  val project_code: string list -> code -> code;
+  val project_code: string list (*hidden*) -> string list option (*selected*)
+    -> code -> code;
   val add_eval_def: string (*shallow name space*) * iterm -> code -> string * code;
-  val delete_garbage: string list (*hidden definitions*) -> code -> code;
+
 
   val ensure_def: (transact -> def * code) -> bool -> string
     -> string -> transact -> transact;
@@ -85,7 +84,6 @@
 
   val trace: bool ref;
   val tracing: ('a -> string) -> 'a -> 'a;
-  val soft_exc: bool ref;
 end;
 
 structure CodegenThingol: CODEGEN_THINGOL =
@@ -95,7 +93,6 @@
 
 val trace = ref false;
 fun tracing f x = (if !trace then Output.tracing (f x) else (); x);
-val soft_exc = ref true;
 
 fun unfoldl dest x =
   case dest x
@@ -131,9 +128,9 @@
   | IVar of vname
   | `$ of iterm * iterm
   | `|-> of (vname * itype) * iterm
-  | INum of IntInf.int * iterm
-  | IChar of string * iterm
-  | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
+  | INum of IntInf.int
+  | IChar of string
+  | ICase of (iterm * itype) * (iterm * iterm) list;
     (*see also signature*)
 
 (*
@@ -174,13 +171,13 @@
     | _ => NONE);
 
 val unfold_abs = unfoldr
-  (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
-        if v = w then SOME ((p, ty), t') else SOME ((IVar v, ty), t)
-    | (v, ty) `|-> t => SOME ((IVar v, ty), t)
+  (fn (v, ty) `|-> (t as ICase ((IVar w, _), [(p, t')])) =>
+        if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
+    | (v, ty) `|-> t => SOME (((v, NONE), ty), t)
     | _ => NONE)
 
 val unfold_let = unfoldr
-  (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
+  (fn ICase ((td, ty), [(p, t)]) => SOME (((p, ty), td), t)
     | _ => NONE);
 
 fun unfold_const_app t =
@@ -188,21 +185,6 @@
   of (IConst c, ts) => SOME (c, ts)
    | _ => NONE;
 
-fun map_pure f (t as IConst _) =
-      f t
-  | map_pure f (t as IVar _) =
-      f t
-  | map_pure f (t as _ `$ _) =
-      f t
-  | map_pure f (t as _ `|-> _) =
-      f t
-  | map_pure f (INum (_, t0)) =
-      f t0
-  | map_pure f (IChar (_, t0)) =
-      f t0
-  | map_pure f (ICase (_, t0)) =
-      f t0;
-
 fun fold_aiterms f (t as IConst _) =
       f t
   | fold_aiterms f (t as IVar _) =
@@ -211,12 +193,12 @@
       fold_aiterms f t1 #> fold_aiterms f t2
   | fold_aiterms f (t as _ `|-> t') =
       f t #> fold_aiterms f t'
-  | fold_aiterms f (INum (_, t0)) =
-      fold_aiterms f t0
-  | fold_aiterms f (IChar (_, t0)) =
-      fold_aiterms f t0
-  | fold_aiterms f (ICase (_, t0)) =
-      fold_aiterms f t0;
+  | fold_aiterms f (t as INum _) =
+      f t
+  | fold_aiterms f (t as IChar _) =
+      f t
+  | fold_aiterms f (ICase ((td, _), bs)) =
+      fold_aiterms f td #> fold (fn (p, t) => fold_aiterms f p #> fold_aiterms f t) bs;
 
 fun fold_constnames f =
   let
@@ -241,12 +223,12 @@
           add vs t1 #> add vs t2
       | add vs ((v, _) `|-> t) =
           add (insert (op =) v vs) t
-      | add vs (INum (_, t)) =
-          add vs t
-      | add vs (IChar (_, t)) =
-          add vs t
-      | add vs (ICase (_, t0)) =
-          add vs t0
+      | add vs (INum _) =
+          I
+      | add vs (IChar _) =
+          I
+      | add vs (ICase ((td, _), bs)) =
+          add vs td #> fold (fn (p, t) => add vs p #> add vs t) bs;
   in add [] end;
 
 fun eta_expand (c as (_, (_, ty)), ts) k =
@@ -278,7 +260,7 @@
 
 type code = def Graph.T;
 type transact = Graph.key option * code;
-exception FAIL of string list * exn option;
+exception FAIL of string list;
 
 
 (* abstract code *)
@@ -307,19 +289,24 @@
 
 val merge_code = Graph.join (fn _ => fn def12 => if eq_def def12 then fst def12 else Bot);
 
-fun project_code names code =
-  Graph.project (member (op =) (Graph.all_succs code names)) code;
-
-fun delete_garbage hidden code =
+fun project_code hidden raw_selected code =
   let
     fun is_bot name = case get_def code name
      of Bot => true
       | _ => false;
     val names = subtract (op =) hidden (Graph.keys code);
-    val names' = subtract (op =)
-      (Graph.all_preds code (filter is_bot names)) names;
+    val deleted = Graph.all_preds code (filter is_bot names);
+    val selected = case raw_selected
+     of NONE => names |> subtract (op =) deleted 
+      | SOME sel => sel
+          |> subtract (op =) deleted
+          |> subtract (op =) hidden
+          |> Graph.all_succs code
+          |> subtract (op =) deleted
+          |> subtract (op =) hidden;
   in
-    Graph.project (member (op =) names') code
+    code
+    |> Graph.project (member (op =) selected)
   end;
 
 fun check_samemodule names =
@@ -406,17 +393,10 @@
     fun prep_def def modl =
       (check_prep_def modl def, modl);
     fun invoke_generator name defgen modl =
-      if ! soft_exc (*that "!" isn't a "not"...*)
-      then defgen (SOME name, modl)
-        handle FAIL (msgs, exc) =>
-                if strict then raise FAIL (msg' :: msgs, exc)
-                else (Bot, modl)
-             | e => raise
-                FAIL (["definition generator for " ^ quote name, msg'], SOME e)
-      else defgen (SOME name, modl)
-        handle FAIL (msgs, exc) =>
-              if strict then raise FAIL (msg' :: msgs, exc)
-              else (Bot, modl);
+      defgen (SOME name, modl)
+        handle FAIL msgs =>
+          if strict then raise FAIL (msg' :: msgs)
+          else (Bot, modl);
   in
     modl
     |> (if can (get_def modl) name
@@ -442,20 +422,18 @@
 
 fun succeed some (_, modl) = (some, modl);
 
-fun fail msg (_, modl) = raise FAIL ([msg], NONE);
+fun fail msg (_, modl) = raise FAIL [msg];
 
 fun message msg f trns =
-  f trns handle FAIL (msgs, exc) =>
-    raise FAIL (msg :: msgs, exc);
+  f trns handle FAIL msgs =>
+    raise FAIL (msg :: msgs);
 
 fun start_transact init f modl =
   let
     fun handle_fail f x =
       (f x
-      handle FAIL (msgs, NONE) =>
+      handle FAIL msgs =>
         (error o cat_lines) ("Code generation failed, while:" :: msgs))
-      handle FAIL (msgs, SOME e) =>
-        ((Output.error_msg o cat_lines) ("Code generation failed, while:" :: msgs); raise e);
   in
     modl
     |> (if is_some init then ensure_bot (the init) else I)