src/Tools/code/code_haskell.ML
author haftmann
Wed, 17 Dec 2008 12:10:40 +0100
changeset 29135 20b42397e293
parent 28708 a1a436f09ec6
child 29711 64d41ad4ffc2
permissions -rw-r--r--
GHC ext pragma in generated Haskell modules
     1 (*  Title:      Tools/code/code_haskell.ML
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 
     5 Serializer for Haskell.
     6 *)
     7 
     8 signature CODE_HASKELL =
     9 sig
    10   val setup: theory -> theory
    11 end;
    12 
    13 structure Code_Haskell : CODE_HASKELL =
    14 struct
    15 
    16 val target = "Haskell";
    17 
    18 open Basic_Code_Thingol;
    19 open Code_Printer;
    20 
    21 infixr 5 @@;
    22 infixr 5 @|;
    23 
    24 
    25 (** Haskell serializer **)
    26 
    27 fun pr_haskell_bind pr_term =
    28   let
    29     fun pr_bind ((NONE, NONE), _) = str "_"
    30       | pr_bind ((SOME v, NONE), _) = str v
    31       | pr_bind ((NONE, SOME p), _) = p
    32       | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
    33   in gen_pr_bind pr_bind pr_term end;
    34 
    35 fun pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const
    36     init_syms deresolve is_cons contr_classparam_typs deriving_show =
    37   let
    38     val deresolve_base = NameSpace.base o deresolve;
    39     fun class_name class = case syntax_class class
    40      of NONE => deresolve class
    41       | SOME class => class;
    42     fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
    43      of [] => []
    44       | classbinds => Pretty.enum "," "(" ")" (
    45           map (fn (v, class) =>
    46             str (class_name class ^ " " ^ Code_Name.lookup_var tyvars v)) classbinds)
    47           @@ str " => ";
    48     fun pr_typforall tyvars vs = case map fst vs
    49      of [] => []
    50       | vnames => str "forall " :: Pretty.breaks
    51           (map (str o Code_Name.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
    52     fun pr_tycoexpr tyvars fxy (tyco, tys) =
    53       brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
    54     and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
    55          of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
    56           | SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
    57       | pr_typ tyvars fxy (ITyVar v) = (str o Code_Name.lookup_var tyvars) v;
    58     fun pr_typdecl tyvars (vs, tycoexpr) =
    59       Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
    60     fun pr_typscheme tyvars (vs, ty) =
    61       Pretty.block (pr_typforall tyvars vs @ pr_typcontext tyvars vs @| pr_typ tyvars NOBR ty);
    62     fun pr_term tyvars thm vars fxy (IConst c) =
    63           pr_app tyvars thm vars fxy (c, [])
    64       | pr_term tyvars thm vars fxy (t as (t1 `$ t2)) =
    65           (case Code_Thingol.unfold_const_app t
    66            of SOME app => pr_app tyvars thm vars fxy app
    67             | _ =>
    68                 brackify fxy [
    69                   pr_term tyvars thm vars NOBR t1,
    70                   pr_term tyvars thm vars BR t2
    71                 ])
    72       | pr_term tyvars thm vars fxy (IVar v) =
    73           (str o Code_Name.lookup_var vars) v
    74       | pr_term tyvars thm vars fxy (t as _ `|-> _) =
    75           let
    76             val (binds, t') = Code_Thingol.unfold_abs t;
    77             fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
    78             val (ps, vars') = fold_map pr binds vars;
    79           in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm vars' NOBR t') end
    80       | pr_term tyvars thm vars fxy (ICase (cases as (_, t0))) =
    81           (case Code_Thingol.unfold_const_app t0
    82            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
    83                 then pr_case tyvars thm vars fxy cases
    84                 else pr_app tyvars thm vars fxy c_ts
    85             | NONE => pr_case tyvars thm vars fxy cases)
    86     and pr_app' tyvars thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
    87      of [] => (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
    88       | fingerprint => let
    89           val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
    90           val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
    91             (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
    92           fun pr_term_anno (t, NONE) _ = pr_term tyvars thm vars BR t
    93             | pr_term_anno (t, SOME _) ty =
    94                 brackets [pr_term tyvars thm vars NOBR t, str "::", pr_typ tyvars NOBR ty];
    95         in
    96           if needs_annotation then
    97             (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
    98           else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
    99         end
   100     and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const naming
   101     and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
   102     and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
   103           let
   104             val (binds, t) = Code_Thingol.unfold_let (ICase cases);
   105             fun pr ((pat, ty), t) vars =
   106               vars
   107               |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
   108               |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
   109             val (ps, vars') = fold_map pr binds vars;
   110           in
   111             Pretty.block_enclose (
   112               str "let {",
   113               concat [str "}", str "in", pr_term tyvars thm vars' NOBR t]
   114             ) ps
   115           end
   116       | pr_case tyvars thm vars fxy (((td, ty), bs as _ :: _), _) =
   117           let
   118             fun pr (pat, t) =
   119               let
   120                 val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
   121               in semicolon [p, str "->", pr_term tyvars thm vars' NOBR t] end;
   122           in
   123             Pretty.block_enclose (
   124               concat [str "(case", pr_term tyvars thm vars NOBR td, str "of", str "{"],
   125               str "})"
   126             ) (map pr bs)
   127           end
   128       | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
   129     fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
   130           let
   131             val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
   132             val n = (length o fst o Code_Thingol.unfold_fun) ty;
   133           in
   134             Pretty.chunks [
   135               Pretty.block [
   136                 (str o suffix " ::" o deresolve_base) name,
   137                 Pretty.brk 1,
   138                 pr_typscheme tyvars (vs, ty),
   139                 str ";"
   140               ],
   141               concat (
   142                 (str o deresolve_base) name
   143                 :: map str (replicate n "_")
   144                 @ str "="
   145                 :: str "error"
   146                 @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string
   147                     o NameSpace.base o NameSpace.qualifier) name
   148               )
   149             ]
   150           end
   151       | pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
   152           let
   153             val eqs = filter (snd o snd) raw_eqs;
   154             val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
   155             fun pr_eq ((ts, t), (thm, _)) =
   156               let
   157                 val consts = map_filter
   158                   (fn c => if (is_some o syntax_const) c
   159                     then NONE else (SOME o NameSpace.base o deresolve) c)
   160                     ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
   161                 val vars = init_syms
   162                   |> Code_Name.intro_vars consts
   163                   |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
   164                        (insert (op =)) ts []);
   165               in
   166                 semicolon (
   167                   (str o deresolve_base) name
   168                   :: map (pr_term tyvars thm vars BR) ts
   169                   @ str "="
   170                   @@ pr_term tyvars thm vars NOBR t
   171                 )
   172               end;
   173           in
   174             Pretty.chunks (
   175               Pretty.block [
   176                 (str o suffix " ::" o deresolve_base) name,
   177                 Pretty.brk 1,
   178                 pr_typscheme tyvars (vs, ty),
   179                 str ";"
   180               ]
   181               :: map pr_eq eqs
   182             )
   183           end
   184       | pr_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
   185           let
   186             val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
   187           in
   188             semicolon [
   189               str "data",
   190               pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
   191             ]
   192           end
   193       | pr_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
   194           let
   195             val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
   196           in
   197             semicolon (
   198               str "newtype"
   199               :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
   200               :: str "="
   201               :: (str o deresolve_base) co
   202               :: pr_typ tyvars BR ty
   203               :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
   204             )
   205           end
   206       | pr_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
   207           let
   208             val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
   209             fun pr_co (co, tys) =
   210               concat (
   211                 (str o deresolve_base) co
   212                 :: map (pr_typ tyvars BR) tys
   213               )
   214           in
   215             semicolon (
   216               str "data"
   217               :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
   218               :: str "="
   219               :: pr_co co
   220               :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
   221               @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
   222             )
   223           end
   224       | pr_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
   225           let
   226             val tyvars = Code_Name.intro_vars [v] init_syms;
   227             fun pr_classparam (classparam, ty) =
   228               semicolon [
   229                 (str o deresolve_base) classparam,
   230                 str "::",
   231                 pr_typ tyvars NOBR ty
   232               ]
   233           in
   234             Pretty.block_enclose (
   235               Pretty.block [
   236                 str "class ",
   237                 Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
   238                 str (deresolve_base name ^ " " ^ Code_Name.lookup_var tyvars v),
   239                 str " where {"
   240               ],
   241               str "};"
   242             ) (map pr_classparam classparams)
   243           end
   244       | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
   245           let
   246             val split_abs_pure = (fn (v, _) `|-> t => SOME (v, t) | _ => NONE);
   247             val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
   248             val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
   249             fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
   250              of NONE => semicolon [
   251                     (str o deresolve_base) classparam,
   252                     str "=",
   253                     pr_app tyvars thm init_syms NOBR (c_inst, [])
   254                   ]
   255               | SOME (k, pr) =>
   256                   let
   257                     val (c_inst_name, (_, tys)) = c_inst;
   258                     val const = if (is_some o syntax_const) c_inst_name
   259                       then NONE else (SOME o NameSpace.base o deresolve) c_inst_name;
   260                     val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
   261                     val (vs, rhs) = unfold_abs_pure proto_rhs;
   262                     val vars = init_syms
   263                       |> Code_Name.intro_vars (the_list const)
   264                       |> Code_Name.intro_vars vs;
   265                     val lhs = IConst (classparam, ([], tys)) `$$ map IVar vs;
   266                       (*dictionaries are not relevant at this late stage*)
   267                   in
   268                     semicolon [
   269                       pr_term tyvars thm vars NOBR lhs,
   270                       str "=",
   271                       pr_term tyvars thm vars NOBR rhs
   272                     ]
   273                   end;
   274           in
   275             Pretty.block_enclose (
   276               Pretty.block [
   277                 str "instance ",
   278                 Pretty.block (pr_typcontext tyvars vs),
   279                 str (class_name class ^ " "),
   280                 pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
   281                 str " where {"
   282               ],
   283               str "};"
   284             ) (map pr_instdef classparam_insts)
   285           end;
   286   in pr_stmt end;
   287 
   288 fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program =
   289   let
   290     val module_alias = if is_some module_name then K module_name else raw_module_alias;
   291     val reserved_names = Name.make_context reserved_names;
   292     val mk_name_module = Code_Name.mk_name_module reserved_names module_prefix module_alias program;
   293     fun add_stmt (name, (stmt, deps)) =
   294       let
   295         val (module_name, base) = Code_Name.dest_name name;
   296         val module_name' = mk_name_module module_name;
   297         val mk_name_stmt = yield_singleton Name.variants;
   298         fun add_fun upper (nsp_fun, nsp_typ) =
   299           let
   300             val (base', nsp_fun') =
   301               mk_name_stmt (if upper then Code_Name.first_upper base else base) nsp_fun
   302           in (base', (nsp_fun', nsp_typ)) end;
   303         fun add_typ (nsp_fun, nsp_typ) =
   304           let
   305             val (base', nsp_typ') = mk_name_stmt (Code_Name.first_upper base) nsp_typ
   306           in (base', (nsp_fun, nsp_typ')) end;
   307         val add_name = case stmt
   308          of Code_Thingol.Fun _ => add_fun false
   309           | Code_Thingol.Datatype _ => add_typ
   310           | Code_Thingol.Datatypecons _ => add_fun true
   311           | Code_Thingol.Class _ => add_typ
   312           | Code_Thingol.Classrel _ => pair base
   313           | Code_Thingol.Classparam _ => add_fun false
   314           | Code_Thingol.Classinst _ => pair base;
   315         fun add_stmt' base' = case stmt
   316          of Code_Thingol.Datatypecons _ =>
   317               cons (name, (NameSpace.append module_name' base', NONE))
   318           | Code_Thingol.Classrel _ => I
   319           | Code_Thingol.Classparam _ =>
   320               cons (name, (NameSpace.append module_name' base', NONE))
   321           | _ => cons (name, (NameSpace.append module_name' base', SOME stmt));
   322       in
   323         Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names))))
   324               (apfst (fold (insert (op = : string * string -> bool)) deps))
   325         #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name'))
   326         #-> (fn (base', names) =>
   327               (Symtab.map_entry module_name' o apsnd) (fn (stmts, _) =>
   328               (add_stmt' base' stmts, names)))
   329       end;
   330     val hs_program = fold add_stmt (AList.make (fn name =>
   331       (Graph.get_node program name, Graph.imm_succs program name))
   332       (Graph.strong_conn program |> flat)) Symtab.empty;
   333     fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the
   334       o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Name.dest_name) name))) name
   335       handle Option => error ("Unknown statement name: " ^ labelled_name name);
   336   in (deresolver, hs_program) end;
   337 
   338 fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
   339     reserved_names includes raw_module_alias
   340     syntax_class syntax_tyco syntax_const naming program cs destination =
   341   let
   342     val stmt_names = Code_Target.stmt_names_of_destination destination;
   343     val module_name = if null stmt_names then raw_module_name else SOME "Code";
   344     val (deresolver, hs_program) = haskell_program_of_program labelled_name
   345       module_name module_prefix reserved_names raw_module_alias program;
   346     val is_cons = Code_Thingol.is_cons program;
   347     val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
   348     fun deriving_show tyco =
   349       let
   350         fun deriv _ "fun" = false
   351           | deriv tycos tyco = member (op =) tycos tyco orelse
   352               case try (Graph.get_node program) tyco
   353                 of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
   354                     (maps snd cs)
   355                  | NONE => true
   356         and deriv' tycos (tyco `%% tys) = deriv tycos tyco
   357               andalso forall (deriv' tycos) tys
   358           | deriv' _ (ITyVar _) = true
   359       in deriv [] tyco end;
   360     val reserved_names = Code_Name.make_vars reserved_names;
   361     fun pr_stmt qualified = pr_haskell_stmt naming labelled_name
   362       syntax_class syntax_tyco syntax_const reserved_names
   363       (if qualified then deresolver else NameSpace.base o deresolver)
   364       is_cons contr_classparam_typs
   365       (if string_classes then deriving_show else K false);
   366     fun pr_module name content =
   367       (name, Pretty.chunks [
   368         str ("module " ^ name ^ " where {"),
   369         str "",
   370         content,
   371         str "",
   372         str "}"
   373       ]);
   374     fun serialize_module1 (module_name', (deps, (stmts, _))) =
   375       let
   376         val stmt_names = map fst stmts;
   377         val deps' = subtract (op =) stmt_names deps
   378           |> distinct (op =)
   379           |> map_filter (try deresolver);
   380         val qualified = is_none module_name andalso
   381           map deresolver stmt_names @ deps'
   382           |> map NameSpace.base
   383           |> has_duplicates (op =);
   384         val imports = deps'
   385           |> map NameSpace.qualifier
   386           |> distinct (op =);
   387         fun pr_import_include (name, _) = str ("import " ^ name ^ ";");
   388         val pr_import_module = str o (if qualified
   389           then prefix "import qualified "
   390           else prefix "import ") o suffix ";";
   391         val content = Pretty.chunks (
   392             map pr_import_include includes
   393             @ map pr_import_module imports
   394             @ str ""
   395             :: separate (str "") (map_filter
   396               (fn (name, (_, SOME stmt)) => SOME (pr_stmt qualified (name, stmt))
   397                 | (_, (_, NONE)) => NONE) stmts)
   398           )
   399       in pr_module module_name' content end;
   400     fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks (
   401       separate (str "") (map_filter
   402         (fn (name, (_, SOME stmt)) => if null stmt_names
   403               orelse member (op =) stmt_names name
   404               then SOME (pr_stmt false (name, stmt))
   405               else NONE
   406           | (_, (_, NONE)) => NONE) stmts));
   407     val serialize_module =
   408       if null stmt_names then serialize_module1 else pair "" o serialize_module2;
   409     fun write_module destination (modlname, content) =
   410       let
   411         val filename = case modlname
   412          of "" => Path.explode "Main.hs"
   413           | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
   414                 o NameSpace.explode) modlname;
   415         val pathname = Path.append destination filename;
   416         val _ = File.mkdir (Path.dir pathname);
   417       in File.write pathname
   418         ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n"
   419           ^ Code_Target.code_of_pretty content)
   420       end
   421   in
   422     Code_Target.mk_serialization target NONE
   423       (fn NONE => K () o map (Code_Target.code_writeln o snd) | SOME file => K () o map (write_module file))
   424       (rpair [] o cat_lines o map (Code_Target.code_of_pretty o snd))
   425       (map (uncurry pr_module) includes
   426         @ map serialize_module (Symtab.dest hs_program))
   427       destination
   428   end;
   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 = enclose "'" "'" o char_haskell,
   437   literal_string = quote o translate_string char_haskell,
   438   literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
   439     else enclose "(" ")" (signed_string_of_int k),
   440   literal_list = Pretty.enum "," "[" "]",
   441   infix_cons = (5, ":")
   442 } end;
   443 
   444 
   445 (** optional monad syntax **)
   446 
   447 fun pretty_haskell_monad c_bind =
   448   let
   449     fun dest_bind t1 t2 = case Code_Thingol.split_abs t2
   450      of SOME (((v, pat), ty), t') =>
   451           SOME ((SOME (((SOME v, pat), ty), true), t1), t')
   452       | NONE => NONE;
   453     fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
   454           if c = c_bind_name then dest_bind t1 t2
   455           else NONE
   456       | dest_monad _ t = case Code_Thingol.split_let t
   457          of SOME (((pat, ty), tbind), t') =>
   458               SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
   459           | NONE => NONE;
   460     fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
   461     fun pr_monad pr_bind pr (NONE, t) vars =
   462           (semicolon [pr vars NOBR t], vars)
   463       | pr_monad pr_bind pr (SOME (bind, true), t) vars = vars
   464           |> pr_bind NOBR bind
   465           |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
   466       | pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
   467           |> pr_bind NOBR bind
   468           |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
   469     fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
   470      of SOME (bind, t') => let
   471           val (binds, t'') = implode_monad ((the o Code_Thingol.lookup_const naming) c_bind) t'
   472           val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K pr) thm) pr) (bind :: binds) vars;
   473         in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
   474       | NONE => brackify_infix (1, L) fxy
   475           [pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2]
   476   in (2, pretty) end;
   477 
   478 fun add_monad target' raw_c_bind thy =
   479   let
   480     val c_bind = Code_Unit.read_const thy raw_c_bind;
   481   in if target = target' then
   482     thy
   483     |> Code_Target.add_syntax_const target c_bind
   484         (SOME (pretty_haskell_monad c_bind))
   485   else error "Only Haskell target allows for monad syntax" end;
   486 
   487 
   488 (** Isar setup **)
   489 
   490 fun isar_seri_haskell module =
   491   Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
   492     -- Scan.optional (Args.$$$ "string_classes" >> K true) false
   493     >> (fn (module_prefix, string_classes) =>
   494       serialize_haskell module_prefix module string_classes));
   495 
   496 val _ =
   497   OuterSyntax.command "code_monad" "define code syntax for monads" OuterKeyword.thy_decl (
   498     OuterParse.term_group -- OuterParse.name >> (fn (raw_bind, target) =>
   499       Toplevel.theory  (add_monad target raw_bind))
   500   );
   501 
   502 val setup =
   503   Code_Target.add_target (target, (isar_seri_haskell, literals))
   504   #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
   505       brackify_infix (1, R) fxy [
   506         pr_typ (INFX (1, X)) ty1,
   507         str "->",
   508         pr_typ (INFX (1, R)) ty2
   509       ]))
   510   #> fold (Code_Target.add_reserved target) [
   511       "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
   512       "import", "default", "forall", "let", "in", "class", "qualified", "data",
   513       "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
   514     ]
   515   #> fold (Code_Target.add_reserved target) [
   516       "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
   517       "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
   518       "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
   519       "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
   520       "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
   521       "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
   522       "ExitSuccess", "False", "GT", "HeapOverflow",
   523       "IOError", "IOException", "IllegalOperation",
   524       "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
   525       "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
   526       "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
   527       "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
   528       "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
   529       "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
   530       "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
   531       "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
   532       "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
   533       "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
   534       "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
   535       "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
   536       "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
   537       "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
   538       "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
   539       "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
   540       "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
   541       "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
   542       "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
   543       "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
   544       "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
   545       "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
   546       "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
   547       "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
   548       "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
   549       "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred", 
   550       "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
   551       "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
   552       "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
   553       "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
   554       "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
   555       "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
   556       "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
   557       "sequence_", "show", "showChar", "showException", "showField", "showList",
   558       "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
   559       "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
   560       "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
   561       "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
   562       "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
   563       "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
   564     ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);
   565 
   566 end; (*struct*)