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