src/Tools/code/code_haskell.ML
author haftmann
Tue, 03 Feb 2009 19:37:16 +0100
changeset 29731 32d00a2a6f28
parent 29711 64d41ad4ffc2
child 29769 b4919260eaec
permissions -rw-r--r--
added stub about datatype abstraction
     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     raw_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 reserved_names = fold (insert (op =) o fst) includes raw_reserved_names;
   345     val (deresolver, hs_program) = haskell_program_of_program labelled_name
   346       module_name module_prefix reserved_names raw_module_alias program;
   347     val is_cons = Code_Thingol.is_cons program;
   348     val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
   349     fun deriving_show tyco =
   350       let
   351         fun deriv _ "fun" = false
   352           | deriv tycos tyco = member (op =) tycos tyco orelse
   353               case try (Graph.get_node program) tyco
   354                 of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
   355                     (maps snd cs)
   356                  | NONE => true
   357         and deriv' tycos (tyco `%% tys) = deriv tycos tyco
   358               andalso forall (deriv' tycos) tys
   359           | deriv' _ (ITyVar _) = true
   360       in deriv [] tyco end;
   361     val reserved_names = Code_Name.make_vars reserved_names;
   362     fun pr_stmt qualified = pr_haskell_stmt naming labelled_name
   363       syntax_class syntax_tyco syntax_const reserved_names
   364       (if qualified then deresolver else NameSpace.base o deresolver)
   365       is_cons contr_classparam_typs
   366       (if string_classes then deriving_show else K false);
   367     fun pr_module name content =
   368       (name, Pretty.chunks [
   369         str ("module " ^ name ^ " where {"),
   370         str "",
   371         content,
   372         str "",
   373         str "}"
   374       ]);
   375     fun serialize_module1 (module_name', (deps, (stmts, _))) =
   376       let
   377         val stmt_names = map fst stmts;
   378         val deps' = subtract (op =) stmt_names deps
   379           |> distinct (op =)
   380           |> map_filter (try deresolver);
   381         val qualified = is_none module_name andalso
   382           map deresolver stmt_names @ deps'
   383           |> map NameSpace.base
   384           |> has_duplicates (op =);
   385         val imports = deps'
   386           |> map NameSpace.qualifier
   387           |> distinct (op =);
   388         fun pr_import_include (name, _) = str ("import qualified " ^ name ^ ";");
   389         val pr_import_module = str o (if qualified
   390           then prefix "import qualified "
   391           else prefix "import ") o suffix ";";
   392         val content = Pretty.chunks (
   393             map pr_import_include includes
   394             @ map pr_import_module imports
   395             @ str ""
   396             :: separate (str "") (map_filter
   397               (fn (name, (_, SOME stmt)) => SOME (pr_stmt qualified (name, stmt))
   398                 | (_, (_, NONE)) => NONE) stmts)
   399           )
   400       in pr_module module_name' content end;
   401     fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks (
   402       separate (str "") (map_filter
   403         (fn (name, (_, SOME stmt)) => if null stmt_names
   404               orelse member (op =) stmt_names name
   405               then SOME (pr_stmt false (name, stmt))
   406               else NONE
   407           | (_, (_, NONE)) => NONE) stmts));
   408     val serialize_module =
   409       if null stmt_names then serialize_module1 else pair "" o serialize_module2;
   410     fun write_module destination (modlname, content) =
   411       let
   412         val filename = case modlname
   413          of "" => Path.explode "Main.hs"
   414           | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
   415                 o NameSpace.explode) modlname;
   416         val pathname = Path.append destination filename;
   417         val _ = File.mkdir (Path.dir pathname);
   418       in File.write pathname
   419         ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n"
   420           ^ Code_Target.code_of_pretty content)
   421       end
   422   in
   423     Code_Target.mk_serialization target NONE
   424       (fn NONE => K () o map (Code_Target.code_writeln o snd) | SOME file => K () o map (write_module file))
   425       (rpair [] o cat_lines o map (Code_Target.code_of_pretty o snd))
   426       (map (uncurry pr_module) includes
   427         @ map serialize_module (Symtab.dest hs_program))
   428       destination
   429   end;
   430 
   431 val literals = let
   432   fun char_haskell c =
   433     let
   434       val s = ML_Syntax.print_char c;
   435     in if s = "'" then "\\'" else s end;
   436 in Literals {
   437   literal_char = enclose "'" "'" o char_haskell,
   438   literal_string = quote o translate_string char_haskell,
   439   literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
   440     else enclose "(" ")" (signed_string_of_int k),
   441   literal_list = Pretty.enum "," "[" "]",
   442   infix_cons = (5, ":")
   443 } end;
   444 
   445 
   446 (** optional monad syntax **)
   447 
   448 fun pretty_haskell_monad c_bind =
   449   let
   450     fun dest_bind t1 t2 = case Code_Thingol.split_abs t2
   451      of SOME (((v, pat), ty), t') =>
   452           SOME ((SOME (((SOME v, pat), ty), true), t1), t')
   453       | NONE => NONE;
   454     fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
   455           if c = c_bind_name then dest_bind t1 t2
   456           else NONE
   457       | dest_monad _ t = case Code_Thingol.split_let t
   458          of SOME (((pat, ty), tbind), t') =>
   459               SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
   460           | NONE => NONE;
   461     fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
   462     fun pr_monad pr_bind pr (NONE, t) vars =
   463           (semicolon [pr vars NOBR t], vars)
   464       | pr_monad pr_bind pr (SOME (bind, true), t) vars = vars
   465           |> pr_bind NOBR bind
   466           |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
   467       | pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
   468           |> pr_bind NOBR bind
   469           |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
   470     fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
   471      of SOME (bind, t') => let
   472           val (binds, t'') = implode_monad ((the o Code_Thingol.lookup_const naming) c_bind) t'
   473           val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K pr) thm) pr) (bind :: binds) vars;
   474         in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
   475       | NONE => brackify_infix (1, L) fxy
   476           [pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2]
   477   in (2, pretty) end;
   478 
   479 fun add_monad target' raw_c_bind thy =
   480   let
   481     val c_bind = Code_Unit.read_const thy raw_c_bind;
   482   in if target = target' then
   483     thy
   484     |> Code_Target.add_syntax_const target c_bind
   485         (SOME (pretty_haskell_monad c_bind))
   486   else error "Only Haskell target allows for monad syntax" end;
   487 
   488 
   489 (** Isar setup **)
   490 
   491 fun isar_seri_haskell module =
   492   Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
   493     -- Scan.optional (Args.$$$ "string_classes" >> K true) false
   494     >> (fn (module_prefix, string_classes) =>
   495       serialize_haskell module_prefix module string_classes));
   496 
   497 val _ =
   498   OuterSyntax.command "code_monad" "define code syntax for monads" OuterKeyword.thy_decl (
   499     OuterParse.term_group -- OuterParse.name >> (fn (raw_bind, target) =>
   500       Toplevel.theory  (add_monad target raw_bind))
   501   );
   502 
   503 val setup =
   504   Code_Target.add_target (target, (isar_seri_haskell, literals))
   505   #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
   506       brackify_infix (1, R) fxy [
   507         pr_typ (INFX (1, X)) ty1,
   508         str "->",
   509         pr_typ (INFX (1, R)) ty2
   510       ]))
   511   #> fold (Code_Target.add_reserved target) [
   512       "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
   513       "import", "default", "forall", "let", "in", "class", "qualified", "data",
   514       "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
   515     ]
   516   #> fold (Code_Target.add_reserved target) [
   517       "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
   518       "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
   519       "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
   520       "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
   521       "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
   522       "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
   523       "ExitSuccess", "False", "GT", "HeapOverflow",
   524       "IOError", "IOException", "IllegalOperation",
   525       "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
   526       "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
   527       "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
   528       "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
   529       "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
   530       "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
   531       "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
   532       "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
   533       "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
   534       "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
   535       "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
   536       "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
   537       "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
   538       "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
   539       "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
   540       "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
   541       "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
   542       "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
   543       "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
   544       "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
   545       "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
   546       "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
   547       "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
   548       "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
   549       "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
   550       "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred", 
   551       "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
   552       "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
   553       "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
   554       "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
   555       "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
   556       "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
   557       "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
   558       "sequence_", "show", "showChar", "showException", "showField", "showList",
   559       "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
   560       "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
   561       "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
   562       "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
   563       "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
   564       "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
   565     ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);
   566 
   567 end; (*struct*)