1.1 --- a/src/Tools/Code/code_haskell.ML Tue Aug 31 13:15:35 2010 +0200
1.2 +++ b/src/Tools/Code/code_haskell.ML Tue Aug 31 13:29:38 2010 +0200
1.3 @@ -24,11 +24,11 @@
1.4
1.5 (** Haskell serializer **)
1.6
1.7 -fun print_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
1.8 +fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax
1.9 reserved deresolve contr_classparam_typs deriving_show =
1.10 let
1.11 val deresolve_base = Long_Name.base_name o deresolve;
1.12 - fun class_name class = case syntax_class class
1.13 + fun class_name class = case class_syntax class
1.14 of NONE => deresolve class
1.15 | SOME class => class;
1.16 fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
1.17 @@ -43,7 +43,7 @@
1.18 (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
1.19 fun print_tyco_expr tyvars fxy (tyco, tys) =
1.20 brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
1.21 - and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
1.22 + and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case tyco_syntax tyco
1.23 of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
1.24 | SOME (i, print) => print (print_typ tyvars) fxy tys)
1.25 | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
1.26 @@ -72,7 +72,7 @@
1.27 in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
1.28 | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
1.29 (case Code_Thingol.unfold_const_app t0
1.30 - of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
1.31 + of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
1.32 then print_case tyvars some_thm vars fxy cases
1.33 else print_app tyvars some_thm vars fxy c_ts
1.34 | NONE => print_case tyvars some_thm vars fxy cases)
1.35 @@ -90,7 +90,7 @@
1.36 (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs)
1.37 else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
1.38 end
1.39 - and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) syntax_const
1.40 + and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
1.41 and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
1.42 and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
1.43 let
1.44 @@ -133,7 +133,7 @@
1.45 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
1.46 val vars = reserved
1.47 |> intro_base_names
1.48 - (is_none o syntax_const) deresolve consts
1.49 + (is_none o const_syntax) deresolve consts
1.50 |> intro_vars ((fold o Code_Thingol.fold_varnames)
1.51 (insert (op =)) ts []);
1.52 in
1.53 @@ -218,7 +218,7 @@
1.54 | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
1.55 let
1.56 val tyvars = intro_vars (map fst vs) reserved;
1.57 - fun requires_args classparam = case syntax_const classparam
1.58 + fun requires_args classparam = case const_syntax classparam
1.59 of NONE => 0
1.60 | SOME (Code_Printer.Plain_const_syntax _) => 0
1.61 | SOME (Code_Printer.Complex_const_syntax (k,_ )) => k;
1.62 @@ -234,7 +234,7 @@
1.63 val (c, (_, tys)) = const;
1.64 val (vs, rhs) = (apfst o map) fst
1.65 (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
1.66 - val s = if (is_some o syntax_const) c
1.67 + val s = if (is_some o const_syntax) c
1.68 then NONE else (SOME o Long_Name.base_name o deresolve) c;
1.69 val vars = reserved
1.70 |> intro_vars (map_filter I (s :: vs));
1.71 @@ -315,7 +315,7 @@
1.72
1.73 fun serialize_haskell module_prefix module_name string_classes labelled_name
1.74 raw_reserved includes module_alias
1.75 - syntax_class syntax_tyco syntax_const program
1.76 + class_syntax tyco_syntax const_syntax program
1.77 (stmt_names, presentation_stmt_names) =
1.78 let
1.79 val reserved = fold (insert (op =) o fst) includes raw_reserved;
1.80 @@ -337,7 +337,7 @@
1.81 in deriv [] tyco end;
1.82 val reserved = make_vars reserved;
1.83 fun print_stmt qualified = print_haskell_stmt labelled_name
1.84 - syntax_class syntax_tyco syntax_const reserved
1.85 + class_syntax tyco_syntax const_syntax reserved
1.86 (if qualified then deresolver else Long_Name.base_name o deresolver)
1.87 contr_classparam_typs
1.88 (if string_classes then deriving_show else K false);
1.89 @@ -458,7 +458,7 @@
1.90 val c_bind = Code.read_const thy raw_c_bind;
1.91 in if target = target' then
1.92 thy
1.93 - |> Code_Target.add_syntax_const target c_bind
1.94 + |> Code_Target.add_const_syntax target c_bind
1.95 (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
1.96 else error "Only Haskell target allows for monad syntax" end;
1.97
1.98 @@ -483,7 +483,7 @@
1.99 check = { env_var = "EXEC_GHC", make_destination = I,
1.100 make_command = fn ghc => fn module_name =>
1.101 ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
1.102 - #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
1.103 + #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
1.104 brackify_infix (1, R) fxy (
1.105 print_typ (INFX (1, X)) ty1,
1.106 str "->",