src/Tools/Code/code_haskell.ML
author haftmann
Fri Dec 05 19:35:36 2014 +0100 (2014-12-05)
changeset 59104 a14475f044b2
parent 58454 271829a473ed
child 59323 468bd3aedfa1
permissions -rw-r--r--
allow multiple inheritance of targets
     1 (*  Title:      Tools/Code/code_haskell.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Serializer for Haskell.
     5 *)
     6 
     7 signature CODE_HASKELL =
     8 sig
     9   val language_params: string
    10   val target: string
    11   val print_numeral: string -> int -> string
    12   val setup: theory -> theory
    13 end;
    14 
    15 structure Code_Haskell : CODE_HASKELL =
    16 struct
    17 
    18 val target = "Haskell";
    19 
    20 val language_extensions =
    21   ["EmptyDataDecls", "RankNTypes", "ScopedTypeVariables"];
    22 
    23 val language_pragma =
    24   "{-# LANGUAGE " ^ commas language_extensions ^ " #-}";
    25 
    26 val language_params =
    27   space_implode " " (map (prefix "-X") language_extensions);
    28 
    29 open Basic_Code_Symbol;
    30 open Basic_Code_Thingol;
    31 open Code_Printer;
    32 
    33 infixr 5 @@;
    34 infixr 5 @|;
    35 
    36 
    37 (** Haskell serializer **)
    38 
    39 fun print_haskell_stmt class_syntax tyco_syntax const_syntax
    40     reserved deresolve deriving_show =
    41   let
    42     val deresolve_const = deresolve o Constant;
    43     val deresolve_tyco = deresolve o Type_Constructor;
    44     val deresolve_class = deresolve o Type_Class;
    45     fun class_name class = case class_syntax class
    46      of NONE => deresolve_class class
    47       | SOME class => class;
    48     fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
    49      of [] => []
    50       | constraints => enum "," "(" ")" (
    51           map (fn (v, class) =>
    52             str (class_name class ^ " " ^ lookup_var tyvars v)) constraints)
    53           @@ str " => ";
    54     fun print_typforall tyvars vs = case map fst vs
    55      of [] => []
    56       | vnames => str "forall " :: Pretty.breaks
    57           (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
    58     fun print_tyco_expr tyvars fxy (tyco, tys) =
    59       brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
    60     and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
    61          of NONE => print_tyco_expr tyvars fxy (deresolve_tyco tyco, tys)
    62           | SOME (_, print) => print (print_typ tyvars) fxy tys)
    63       | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
    64     fun print_typdecl tyvars (tyco, vs) =
    65       print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
    66     fun print_typscheme tyvars (vs, ty) =
    67       Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
    68     fun print_term tyvars some_thm vars fxy (IConst const) =
    69           print_app tyvars some_thm vars fxy (const, [])
    70       | print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
    71           (case Code_Thingol.unfold_const_app t
    72            of SOME app => print_app tyvars some_thm vars fxy app
    73             | _ =>
    74                 brackify fxy [
    75                   print_term tyvars some_thm vars NOBR t1,
    76                   print_term tyvars some_thm vars BR t2
    77                 ])
    78       | print_term tyvars some_thm vars fxy (IVar NONE) =
    79           str "_"
    80       | print_term tyvars some_thm vars fxy (IVar (SOME v)) =
    81           (str o lookup_var vars) v
    82       | print_term tyvars some_thm vars fxy (t as _ `|=> _) =
    83           let
    84             val (binds, t') = Code_Thingol.unfold_pat_abs t;
    85             val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
    86           in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
    87       | print_term tyvars some_thm vars fxy (ICase case_expr) =
    88           (case Code_Thingol.unfold_const_app (#primitive case_expr)
    89            of SOME (app as ({ sym = Constant const, ... }, _)) =>
    90                 if is_none (const_syntax const)
    91                 then print_case tyvars some_thm vars fxy case_expr
    92                 else print_app tyvars some_thm vars fxy app
    93             | NONE => print_case tyvars some_thm vars fxy case_expr)
    94     and print_app_expr tyvars some_thm vars ({ sym, annotation, ... }, ts) =
    95       let
    96         val printed_const =
    97           case annotation of
    98             SOME ty => brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty]
    99           | NONE => (str o deresolve) sym
   100       in 
   101         printed_const :: map (print_term tyvars some_thm vars BR) ts
   102       end
   103     and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
   104     and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
   105     and print_case tyvars some_thm vars fxy { clauses = [], ... } =
   106           (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]
   107       | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
   108           let
   109             val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
   110             fun print_match ((pat, _), t) vars =
   111               vars
   112               |> print_bind tyvars some_thm BR pat
   113               |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t])
   114             val (ps, vars') = fold_map print_match binds vars;
   115           in brackify_block fxy (str "let {")
   116             ps
   117             (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
   118           end
   119       | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
   120           let
   121             fun print_select (pat, body) =
   122               let
   123                 val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
   124               in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
   125           in Pretty.block_enclose
   126             (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
   127             (map print_select clauses)
   128           end;
   129     fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
   130           let
   131             val tyvars = intro_vars (map fst vs) reserved;
   132             fun print_err n =
   133               (semicolon o map str) (
   134                 deresolve_const const
   135                 :: replicate n "_"
   136                 @ "="
   137                 :: "error"
   138                 @@ ML_Syntax.print_string const
   139               );
   140             fun print_eqn ((ts, t), (some_thm, _)) =
   141               let
   142                 val vars = reserved
   143                   |> intro_base_names_for (is_none o const_syntax)
   144                       deresolve (t :: ts)
   145                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
   146                       (insert (op =)) ts []);
   147               in
   148                 semicolon (
   149                   (str o deresolve_const) const
   150                   :: map (print_term tyvars some_thm vars BR) ts
   151                   @ str "="
   152                   @@ print_term tyvars some_thm vars NOBR t
   153                 )
   154               end;
   155           in
   156             Pretty.chunks (
   157               semicolon [
   158                 (str o suffix " ::" o deresolve_const) const,
   159                 print_typscheme tyvars (vs, ty)
   160               ]
   161               :: (case filter (snd o snd) raw_eqs
   162                of [] => [print_err ((length o fst o Code_Thingol.unfold_fun) ty)]
   163                 | eqs => map print_eqn eqs)
   164             )
   165           end
   166       | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) =
   167           let
   168             val tyvars = intro_vars vs reserved;
   169           in
   170             semicolon [
   171               str "data",
   172               print_typdecl tyvars (deresolve_tyco tyco, vs)
   173             ]
   174           end
   175       | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) =
   176           let
   177             val tyvars = intro_vars vs reserved;
   178           in
   179             semicolon (
   180               str "newtype"
   181               :: print_typdecl tyvars (deresolve_tyco tyco, vs)
   182               :: str "="
   183               :: (str o deresolve_const) co
   184               :: print_typ tyvars BR ty
   185               :: (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else [])
   186             )
   187           end
   188       | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
   189           let
   190             val tyvars = intro_vars vs reserved;
   191             fun print_co ((co, _), tys) =
   192               concat (
   193                 (str o deresolve_const) co
   194                 :: map (print_typ tyvars BR) tys
   195               )
   196           in
   197             semicolon (
   198               str "data"
   199               :: print_typdecl tyvars (deresolve_tyco tyco, vs)
   200               :: str "="
   201               :: print_co co
   202               :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
   203               @ (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else [])
   204             )
   205           end
   206       | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
   207           let
   208             val tyvars = intro_vars [v] reserved;
   209             fun print_classparam (classparam, ty) =
   210               semicolon [
   211                 (str o deresolve_const) classparam,
   212                 str "::",
   213                 print_typ tyvars NOBR ty
   214               ]
   215           in
   216             Pretty.block_enclose (
   217               Pretty.block [
   218                 str "class ",
   219                 Pretty.block (print_typcontext tyvars [(v, map snd classrels)]),
   220                 str (deresolve_class class ^ " " ^ lookup_var tyvars v),
   221                 str " where {"
   222               ],
   223               str "};"
   224             ) (map print_classparam classparams)
   225           end
   226       | print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) =
   227           let
   228             val tyvars = intro_vars (map fst vs) reserved;
   229             fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
   230               case const_syntax classparam of
   231                 NONE => semicolon [
   232                     (str o Long_Name.base_name o deresolve_const) classparam,
   233                     str "=",
   234                     print_app tyvars (SOME thm) reserved NOBR (const, [])
   235                   ]
   236               | SOME (_, Code_Printer.Plain_printer s) => semicolon [
   237                     (str o Long_Name.base_name) s,
   238                     str "=",
   239                     print_app tyvars (SOME thm) reserved NOBR (const, [])
   240                   ]
   241               | SOME (k, Code_Printer.Complex_printer _) =>
   242                   let
   243                     val { sym = Constant c, dom, ... } = const;
   244                     val (vs, rhs) = (apfst o map) fst
   245                       (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
   246                     val s = if (is_some o const_syntax) c
   247                       then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
   248                     val vars = reserved
   249                       |> intro_vars (map_filter I (s :: vs));
   250                     val lhs = IConst { sym = Constant classparam, typargs = [],
   251                       dicts = [], dom = dom, annotation = NONE } `$$ map IVar vs;
   252                       (*dictionaries are not relevant at this late stage,
   253                         and these consts never need type annotations for disambiguation *)
   254                   in
   255                     semicolon [
   256                       print_term tyvars (SOME thm) vars NOBR lhs,
   257                       str "=",
   258                       print_term tyvars (SOME thm) vars NOBR rhs
   259                     ]
   260                   end;
   261           in
   262             Pretty.block_enclose (
   263               Pretty.block [
   264                 str "instance ",
   265                 Pretty.block (print_typcontext tyvars vs),
   266                 str (class_name class ^ " "),
   267                 print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
   268                 str " where {"
   269               ],
   270               str "};"
   271             ) (map print_classparam_instance inst_params)
   272           end;
   273   in print_stmt end;
   274 
   275 fun haskell_program_of_program ctxt module_prefix module_name reserved identifiers =
   276   let
   277     fun namify_fun upper base (nsp_fun, nsp_typ) =
   278       let
   279         val (base', nsp_fun') = Name.variant (Name.enforce_case upper base) nsp_fun;
   280       in (base', (nsp_fun', nsp_typ)) end;
   281     fun namify_typ base (nsp_fun, nsp_typ) =
   282       let
   283         val (base', nsp_typ') = Name.variant (Name.enforce_case true base) nsp_typ;
   284       in (base', (nsp_fun, nsp_typ')) end;
   285     fun namify_stmt (Code_Thingol.Fun (_, SOME _)) = pair
   286       | namify_stmt (Code_Thingol.Fun _) = namify_fun false
   287       | namify_stmt (Code_Thingol.Datatype _) = namify_typ
   288       | namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true
   289       | namify_stmt (Code_Thingol.Class _) = namify_typ
   290       | namify_stmt (Code_Thingol.Classrel _) = pair
   291       | namify_stmt (Code_Thingol.Classparam _) = namify_fun false
   292       | namify_stmt (Code_Thingol.Classinst _) = pair;
   293     fun select_stmt (Code_Thingol.Fun (_, SOME _)) = false
   294       | select_stmt (Code_Thingol.Fun _) = true
   295       | select_stmt (Code_Thingol.Datatype _) = true
   296       | select_stmt (Code_Thingol.Datatypecons _) = false
   297       | select_stmt (Code_Thingol.Class _) = true
   298       | select_stmt (Code_Thingol.Classrel _) = false
   299       | select_stmt (Code_Thingol.Classparam _) = false
   300       | select_stmt (Code_Thingol.Classinst _) = true;
   301   in
   302     Code_Namespace.flat_program ctxt
   303       { module_prefix = module_prefix, module_name = module_name, reserved = reserved,
   304         identifiers = identifiers, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt,
   305         modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE }
   306   end;
   307 
   308 val prelude_import_operators = [
   309   "==", "/=", "<", "<=", ">=", ">", "+", "-", "*", "/", "**", ">>=", ">>", "=<<", "&&", "||", "^", "^^", ".", "$", "$!", "++", "!!"
   310 ];
   311 
   312 val prelude_import_unqualified = [
   313   "Eq",
   314   "error",
   315   "id",
   316   "return",
   317   "not",
   318   "fst", "snd",
   319   "map", "filter", "concat", "concatMap", "reverse", "zip", "null", "takeWhile", "dropWhile", "all", "any",
   320   "Integer", "negate", "abs", "divMod",
   321   "String"
   322 ];
   323 
   324 val prelude_import_unqualified_constr = [
   325   ("Bool", ["True", "False"]),
   326   ("Maybe", ["Nothing", "Just"])
   327 ];
   328 
   329 fun serialize_haskell module_prefix string_classes ctxt { module_name,
   330     reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } exports program =
   331   let
   332 
   333     (* build program *)
   334     val reserved = fold (insert (op =) o fst) includes reserved_syms;
   335     val { deresolver, flat_program = haskell_program } = haskell_program_of_program
   336       ctxt module_prefix module_name (Name.make_context reserved) identifiers exports program;
   337 
   338     (* print statements *)
   339     fun deriving_show tyco =
   340       let
   341         fun deriv _ "fun" = false
   342           | deriv tycos tyco = member (op =) tycos tyco
   343               orelse case try (Code_Symbol.Graph.get_node program) (Type_Constructor tyco)
   344                 of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
   345                     (maps snd cs)
   346                  | NONE => true
   347         and deriv' tycos (tyco `%% tys) = deriv tycos tyco
   348               andalso forall (deriv' tycos) tys
   349           | deriv' _ (ITyVar _) = true
   350       in deriv [] tyco end;
   351     fun print_stmt deresolve = print_haskell_stmt
   352       class_syntax tyco_syntax const_syntax (make_vars reserved)
   353       deresolve (if string_classes then deriving_show else K false);
   354 
   355     (* print modules *)
   356     fun print_module_frame module_name exports ps =
   357       (module_name, Pretty.chunks2 (
   358         concat [str "module",
   359           case exports of
   360             SOME ps => Pretty.block [str module_name, enclose "(" ")" (commas ps)]
   361           | NONE => str module_name,
   362           str "where {"
   363         ]
   364         :: ps
   365         @| str "}"
   366       ));
   367     fun print_qualified_import module_name =
   368       semicolon [str "import qualified", str module_name];
   369     val import_common_ps =
   370       enclose "import Prelude (" ");" (commas (map str
   371         (map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified)
   372           @ map (fn (tyco, constrs) => (enclose (tyco ^ "(") ")" o commas o map str) constrs) prelude_import_unqualified_constr))
   373       :: print_qualified_import "Prelude"
   374       :: map (print_qualified_import o fst) includes;
   375     fun print_module module_name (gr, imports) =
   376       let
   377         val deresolve = deresolver module_name;
   378         val deresolve_import = SOME o str o deresolve;
   379         val deresolve_import_attached = SOME o str o suffix "(..)" o deresolve;
   380         fun print_import (sym, (_, Code_Thingol.Fun _)) = deresolve_import sym
   381           | print_import (sym, (Code_Namespace.Public, Code_Thingol.Datatype _)) = deresolve_import_attached sym
   382           | print_import (sym, (Code_Namespace.Opaque, Code_Thingol.Datatype _)) = deresolve_import sym
   383           | print_import (sym, (Code_Namespace.Public, Code_Thingol.Class _)) = deresolve_import_attached sym
   384           | print_import (sym, (Code_Namespace.Opaque, Code_Thingol.Class _)) = deresolve_import sym
   385           | print_import (sym, (_, Code_Thingol.Classinst _)) = NONE;
   386         val import_ps = import_common_ps @ map (print_qualified_import o fst) imports;
   387         fun print_stmt' sym = case Code_Symbol.Graph.get_node gr sym
   388          of (_, NONE) => NONE
   389           | (_, SOME (export, stmt)) =>
   390               SOME (if Code_Namespace.not_private export then print_import (sym, (export, stmt)) else NONE, markup_stmt sym (print_stmt deresolve (sym, stmt)));
   391         val (export_ps, body_ps) = (flat o rev o Code_Symbol.Graph.strong_conn) gr
   392           |> map_filter print_stmt'
   393           |> split_list
   394           |> apfst (map_filter I);
   395       in
   396         print_module_frame module_name (SOME export_ps)
   397           ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
   398       end;
   399 
   400     (*serialization*)
   401     fun write_module width (SOME destination) (module_name, content) =
   402           let
   403             val _ = File.check_dir destination;
   404             val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
   405               o separate "/" o Long_Name.explode) module_name;
   406             val _ = Isabelle_System.mkdirs (Path.dir filepath);
   407           in
   408             (File.write filepath o format [] width o Pretty.chunks2)
   409               [str language_pragma, content]
   410           end
   411       | write_module width NONE (_, content) = writeln (format [] width content);
   412   in
   413     Code_Target.serialization
   414       (fn width => fn destination => K () o map (write_module width destination))
   415       (fn present => fn width => rpair (try (deresolver ""))
   416         o (map o apsnd) (format present width))
   417       (map (fn (module_name, content) => print_module_frame module_name NONE [content]) includes
   418         @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
   419           ((flat o rev o Graph.strong_conn) haskell_program))
   420   end;
   421 
   422 val serializer : Code_Target.serializer =
   423   Code_Target.parse_args (Scan.optional (Args.$$$ "root" -- Args.colon |-- Args.name) ""
   424     -- Scan.optional (Args.$$$ "string_classes" >> K true) false
   425     >> (fn (module_prefix, string_classes) =>
   426       serialize_haskell module_prefix string_classes));
   427 
   428 fun print_numeral typ = Library.enclose "(" (" :: " ^ typ ^ ")") o signed_string_of_int;
   429 
   430 val literals = let
   431   fun char_haskell c =
   432     let
   433       val s = ML_Syntax.print_char c;
   434     in if s = "'" then "\\'" else s end;
   435 in Literals {
   436   literal_char = Library.enclose "'" "'" o char_haskell,
   437   literal_string = quote o translate_string char_haskell,
   438   literal_numeral = print_numeral "Integer",
   439   literal_list = enum "," "[" "]",
   440   infix_cons = (5, ":")
   441 } end;
   442 
   443 
   444 (** optional monad syntax **)
   445 
   446 fun pretty_haskell_monad c_bind =
   447   let
   448     fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2
   449      of SOME ((pat, ty), t') =>
   450           SOME ((SOME ((pat, ty), true), t1), t')
   451       | NONE => NONE;
   452     fun dest_monad (IConst { sym = Constant c, ... } `$ t1 `$ t2) =
   453           if c = c_bind then dest_bind t1 t2
   454           else NONE
   455       | dest_monad t = case Code_Thingol.split_let t
   456          of SOME (((pat, ty), tbind), t') =>
   457               SOME ((SOME ((pat, ty), false), tbind), t')
   458           | NONE => NONE;
   459     val implode_monad = Code_Thingol.unfoldr dest_monad;
   460     fun print_monad print_bind print_term (NONE, t) vars =
   461           (semicolon [print_term vars NOBR t], vars)
   462       | print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars
   463           |> print_bind NOBR bind
   464           |>> (fn p => semicolon [p, str "<-", print_term vars NOBR t])
   465       | print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars
   466           |> print_bind NOBR bind
   467           |>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]);
   468     fun pretty _ print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
   469      of SOME (bind, t') => let
   470           val (binds, t'') = implode_monad t'
   471           val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
   472             (bind :: binds) vars;
   473         in
   474           brackify_block fxy (str "do { ")
   475             (ps @| print_term vars' NOBR t'')
   476             (str " }")
   477         end
   478       | NONE => brackify_infix (1, L) fxy
   479           (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
   480   in (2, pretty) end;
   481 
   482 fun add_monad target' raw_c_bind thy =
   483   let
   484     val c_bind = Code.read_const thy raw_c_bind;
   485   in
   486     if target = target' then
   487       thy
   488       |> Code_Target.set_printings (Constant (c_bind, [(target,
   489         SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))]))
   490     else error "Only Haskell target allows for monad syntax"
   491   end;
   492 
   493 
   494 (** Isar setup **)
   495 
   496 val _ =
   497   Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
   498     (Parse.term -- Parse.name >> (fn (raw_bind, target) =>
   499       Toplevel.theory (add_monad target raw_bind)));
   500 
   501 val setup =
   502   Code_Target.add_language
   503     (target, { serializer = serializer, literals = literals,
   504       check = { env_var = "ISABELLE_GHC", make_destination = I,
   505         make_command = fn module_name =>
   506           "\"$ISABELLE_GHC\" " ^ language_params  ^ " -odir build -hidir build -stubdir build -e \"\" " ^
   507             module_name ^ ".hs" } })
   508   #> Code_Target.set_printings (Type_Constructor ("fun",
   509     [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   510       brackify_infix (1, R) fxy (
   511         print_typ (INFX (1, X)) ty1,
   512         str "->",
   513         print_typ (INFX (1, R)) ty2
   514       )))]))
   515   #> fold (Code_Target.add_reserved target) [
   516       "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
   517       "import", "default", "forall", "let", "in", "class", "qualified", "data",
   518       "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
   519     ]
   520   #> fold (Code_Target.add_reserved target) prelude_import_unqualified
   521   #> fold (Code_Target.add_reserved target o fst) prelude_import_unqualified_constr
   522   #> fold (fold (Code_Target.add_reserved target) o snd) prelude_import_unqualified_constr;
   523 
   524 end; (*struct*)