# HG changeset patch
# User haftmann
# Date 1411058884 -7200
# Node ID 1c036d6216d38da65adccd007ecf1c53d606b110
# Parent  7b60e4e74430f2b82a9d847f24a194343aa024c8
tuned data structure

diff -r 7b60e4e74430 -r 1c036d6216d3 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Sep 19 14:24:03 2014 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Sep 18 18:48:04 2014 +0200
@@ -658,7 +658,7 @@
     val unitT = @{type_name unit} `%% [];
     val unitt =
       IConst { sym = Code_Symbol.Constant @{const_name Unity}, typargs = [], dicts = [], dom = [],
-        range = unitT, annotate = false };
+        annotation = NONE };
     fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
       | dest_abs (t, ty) =
           let
diff -r 7b60e4e74430 -r 1c036d6216d3 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Fri Sep 19 14:24:03 2014 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Sep 18 18:48:04 2014 +0200
@@ -90,14 +90,12 @@
                 then print_case tyvars some_thm vars fxy case_expr
                 else print_app tyvars some_thm vars fxy app
             | NONE => print_case tyvars some_thm vars fxy case_expr)
-    and print_app_expr tyvars some_thm vars ({ sym, dom, range, annotate, ... }, ts) =
+    and print_app_expr tyvars some_thm vars ({ sym, annotation, ... }, ts) =
       let
-        val ty = Library.foldr (op `->) (dom, range)
         val printed_const =
-          if annotate then
-            brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty]
-          else
-            (str o deresolve) sym
+          case annotation of
+            SOME ty => brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty]
+          | NONE => (str o deresolve) sym
       in 
         printed_const :: map (print_term tyvars some_thm vars BR) ts
       end
@@ -241,7 +239,7 @@
                   ]
               | SOME (k, Code_Printer.Complex_printer _) =>
                   let
-                    val { sym = Constant c, dom, range, ... } = const;
+                    val { sym = Constant c, dom, ... } = const;
                     val (vs, rhs) = (apfst o map) fst
                       (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
                     val s = if (is_some o const_syntax) c
@@ -249,7 +247,7 @@
                     val vars = reserved
                       |> intro_vars (map_filter I (s :: vs));
                     val lhs = IConst { sym = Constant classparam, typargs = [],
-                      dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
+                      dicts = [], dom = dom, annotation = NONE } `$$ map IVar vs;
                       (*dictionaries are not relevant at this late stage,
                         and these consts never need type annotations for disambiguation *)
                   in
diff -r 7b60e4e74430 -r 1c036d6216d3 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Sep 19 14:24:03 2014 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu Sep 18 18:48:04 2014 +0200
@@ -24,7 +24,7 @@
       `%% of string * itype list
     | ITyVar of vname;
   type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
-    dom: itype list, range: itype, annotate: bool };
+    dom: itype list, annotation: itype option };
   datatype iterm =
       IConst of const
     | IVar of vname option
@@ -152,7 +152,7 @@
   in (tys3, ty3) end;
 
 type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
-  dom: itype list, range: itype, annotate: bool };
+  dom: itype list, annotation: itype option };
 
 datatype iterm =
     IConst of const
@@ -646,10 +646,11 @@
     ensure_const ctxt algbr eqngr permissive c
     ##>> fold_map (translate_typ ctxt algbr eqngr permissive) typargs
     ##>> fold_map (translate_dicts ctxt algbr eqngr permissive some_thm) (typargs ~~ sorts)
-    ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (range :: dom)
-    #>> (fn (((c, typargs), dss), range :: dom) =>
+    ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (ty' :: dom)
+    #>> (fn (((c, typargs), dss), annotation :: dom) =>
       IConst { sym = Constant c, typargs = typargs, dicts = dss,
-        dom = dom, range = range, annotate = annotate })
+        dom = dom, annotation =
+          if annotate then SOME annotation else NONE })
   end
 and translate_app_const ctxt algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
   translate_const ctxt algbr eqngr permissive some_thm (c_ty, some_abs)
diff -r 7b60e4e74430 -r 1c036d6216d3 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Fri Sep 19 14:24:03 2014 +0200
+++ b/src/Tools/nbe.ML	Thu Sep 18 18:48:04 2014 +0200
@@ -416,7 +416,7 @@
 
 fun dummy_const sym dss =
   IConst { sym = sym, typargs = [], dicts = dss,
-    dom = [], range = ITyVar "", annotate = false };
+    dom = [], annotation = NONE };
 
 fun eqns_of_stmt (_, Code_Thingol.NoStmt) =
       []