src/Tools/Code/code_haskell.ML

--- a/src/Tools/Code/code_haskell.ML	Tue Aug 31 13:15:35 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Tue Aug 31 13:29:38 2010 +0200
@@ -24,11 +24,11 @@
 
 (** Haskell serializer **)
 
-fun print_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
+fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax
     reserved deresolve contr_classparam_typs deriving_show =
   let
     val deresolve_base = Long_Name.base_name o deresolve;
-    fun class_name class = case syntax_class class
+    fun class_name class = case class_syntax class
      of NONE => deresolve class
       | SOME class => class;
     fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
@@ -43,7 +43,7 @@
           (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
     fun print_tyco_expr tyvars fxy (tyco, tys) =
       brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
-    and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
+    and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case tyco_syntax tyco
          of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
           | SOME (i, print) => print (print_typ tyvars) fxy tys)
       | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
@@ -72,7 +72,7 @@
           in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
       | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
           (case Code_Thingol.unfold_const_app t0
-           of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
+           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
                 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)
@@ -90,7 +90,7 @@
             (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
+    and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
     and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
     and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
           let
@@ -133,7 +133,7 @@
                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                 val vars = reserved
                   |> intro_base_names
-                      (is_none o syntax_const) deresolve consts
+                      (is_none o const_syntax) deresolve consts
                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
                       (insert (op =)) ts []);
               in
@@ -218,7 +218,7 @@
       | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
-            fun requires_args classparam = case syntax_const classparam
+            fun requires_args classparam = case const_syntax classparam
              of NONE => 0
               | SOME (Code_Printer.Plain_const_syntax _) => 0
               | SOME (Code_Printer.Complex_const_syntax (k,_ )) => k;
@@ -234,7 +234,7 @@
                       val (c, (_, tys)) = const;
                       val (vs, rhs) = (apfst o map) fst
                         (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
-                      val s = if (is_some o syntax_const) c
+                      val s = if (is_some o const_syntax) c
                         then NONE else (SOME o Long_Name.base_name o deresolve) c;
                       val vars = reserved
                         |> intro_vars (map_filter I (s :: vs));
@@ -315,7 +315,7 @@
 
 fun serialize_haskell module_prefix module_name string_classes labelled_name
     raw_reserved includes module_alias
-    syntax_class syntax_tyco syntax_const program
+    class_syntax tyco_syntax const_syntax program
     (stmt_names, presentation_stmt_names) =
   let
     val reserved = fold (insert (op =) o fst) includes raw_reserved;
@@ -337,7 +337,7 @@
       in deriv [] tyco end;
     val reserved = make_vars reserved;
     fun print_stmt qualified = print_haskell_stmt labelled_name
-      syntax_class syntax_tyco syntax_const reserved
+      class_syntax tyco_syntax const_syntax reserved
       (if qualified then deresolver else Long_Name.base_name o deresolver)
       contr_classparam_typs
       (if string_classes then deriving_show else K false);
@@ -458,7 +458,7 @@
     val c_bind = Code.read_const thy raw_c_bind;
   in if target = target' then
     thy
-    |> Code_Target.add_syntax_const target c_bind
+    |> Code_Target.add_const_syntax target c_bind
         (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
   else error "Only Haskell target allows for monad syntax" end;
 
@@ -483,7 +483,7 @@
       check = { env_var = "EXEC_GHC", make_destination = I,
         make_command = fn ghc => fn module_name =>
           ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
-  #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
+  #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy (
         print_typ (INFX (1, X)) ty1,
         str "->",