# HG changeset patch
# User haftmann
# Date 1276783187 -7200
# Node ID 034ebe92f0905f71b968ccdce5418baf5429f830
# Parent  3bd4b3809bee96b6eeb3feaaea181d1f9a59672a
more precise code

diff -r 3bd4b3809bee -r 034ebe92f090 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Thu Jun 17 15:59:46 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Jun 17 15:59:47 2010 +0200
@@ -75,7 +75,7 @@
                 then print_case tyvars some_thm vars fxy cases
                 else print_app tyvars some_thm vars fxy c_ts
             | NONE => print_case tyvars some_thm vars fxy cases)
-    and print_app_expr tyvars some_thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
+    and print_app_expr tyvars some_thm vars ((c, (_, function_typs)), ts) = case contr_classparam_typs c
      of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
       | fingerprint => let
           val ts_fingerprint = ts ~~ take (length ts) fingerprint;
@@ -86,7 +86,7 @@
                 brackets [print_term tyvars some_thm vars NOBR t, str "::", print_typ tyvars NOBR ty];
         in
           if needs_annotation then
-            (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) tys)
+            (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs)
           else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
         end
     and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) syntax_const
@@ -163,7 +163,7 @@
               print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
             ]
           end
-      | print_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
+      | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
           in
@@ -179,7 +179,7 @@
       | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
-            fun print_co (co, tys) =
+            fun print_co ((co, _), tys) =
               concat (
                 (str o deresolve_base) co
                 :: map (print_typ tyvars BR) tys
@@ -214,7 +214,7 @@
               str "};"
             ) (map print_classparam classparams)
           end
-      | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_instances))) =
+      | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
             fun print_classparam_instance ((classparam, const), (thm, _)) = case syntax_const classparam
diff -r 3bd4b3809bee -r 034ebe92f090 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Jun 17 15:59:46 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Jun 17 15:59:47 2010 +0200
@@ -33,13 +33,13 @@
     ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
   | ML_Instance of string * ((class * (string * (vname * sort) list))
         * ((class * (string * (string * dict list list))) list
-      * ((string * const) * (thm * bool)) list));
+      * (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list)));
 
 datatype ml_stmt =
     ML_Exc of string * (typscheme * int)
   | ML_Val of ml_binding
   | ML_Funs of ml_binding list * string list
-  | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list
+  | ML_Datas of (string * ((vname * sort) list * ((string * vname list) * itype list) list)) list
   | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
 
 fun stmt_name_of_binding (ML_Function (name, _)) = name
@@ -121,9 +121,9 @@
                 then print_case is_pseudo_fun some_thm vars fxy cases
                 else print_app is_pseudo_fun some_thm vars fxy c_ts
             | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
-    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
+    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), function_typs)), ts)) =
       if is_cons c then
-        let val k = length tys in
+        let val k = length function_typs in
           if k < 2 orelse length ts = k
           then (str o deresolve) c
             :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
@@ -174,8 +174,8 @@
       [str "val", str (deresolve name), str ":", print_typscheme typscheme];
     fun print_datatype_decl definer (tyco, (vs, cos)) =
       let
-        fun print_co (co, []) = str (deresolve co)
-          | print_co (co, tys) = concat [str (deresolve co), str "of",
+        fun print_co ((co, _), []) = str (deresolve co)
+          | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
               enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
       in
         concat (
@@ -219,7 +219,7 @@
             ))
           end
       | print_def is_pseudo_fun _ definer
-          (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
+          (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
           let
             fun print_super_instance (_, (classrel, dss)) =
               concat [
@@ -466,8 +466,8 @@
       [str "val", str (deresolve name), str ":", print_typscheme typscheme];
     fun print_datatype_decl definer (tyco, (vs, cos)) =
       let
-        fun print_co (co, []) = str (deresolve co)
-          | print_co (co, tys) = concat [str (deresolve co), str "of",
+        fun print_co ((co, _), []) = str (deresolve co)
+          | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
               enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
       in
         concat (
@@ -554,7 +554,7 @@
             ))
           end
       | print_def is_pseudo_fun _ definer
-            (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
+            (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
           let
             fun print_super_instance (_, (classrel, dss)) =
               concat [
diff -r 3bd4b3809bee -r 034ebe92f090 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Thu Jun 17 15:59:46 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Thu Jun 17 15:59:47 2010 +0200
@@ -256,12 +256,12 @@
   fold_map (Code_Thingol.ensure_declared_const thy) cs naming
   |-> (fn cs' => pair (n, f literals cs'));
 
-fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, tys)), ts)) =
+fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, function_typs)), ts)) =
   case syntax_const c
    of NONE => brackify fxy (print_app_expr thm vars app)
     | SOME (k, print) =>
         let
-          fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k tys);
+          fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k function_typs);
         in if k = length ts
           then print' fxy ts
         else if k < length ts
diff -r 3bd4b3809bee -r 034ebe92f090 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Thu Jun 17 15:59:46 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Thu Jun 17 15:59:47 2010 +0200
@@ -51,8 +51,8 @@
 
 fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
       ss addsimps (map_filter (fst o snd)) eqs addcongs (the_list some_cong)
-  | add_stmt (Code_Thingol.Classinst (_, (_, classparam_insts))) ss =
-      ss addsimps (map (fst o snd) classparam_insts)
+  | add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss =
+      ss addsimps (map (fst o snd) classparam_instances)
   | add_stmt _ ss = ss;
 
 val add_program = Graph.fold (add_stmt o fst o snd)
diff -r 3bd4b3809bee -r 034ebe92f090 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu Jun 17 15:59:46 2010 +0200
+++ b/src/Tools/nbe.ML	Thu Jun 17 15:59:47 2010 +0200
@@ -417,7 +417,7 @@
       []
   | eqns_of_stmt (_, Code_Thingol.Classparam _) =
       []
-  | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, classparam_instances))) =
+  | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
       [(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
         map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
         @ map (IConst o snd o fst) classparam_instances)]))];