src/Tools/code/code_haskell.ML
changeset 31775 2b04504fcb69
parent 31774 5c8cfaed32e6
child 31776 151c3f5f28f9
child 31781 861e675f01e6
equal deleted inserted replaced
31774:5c8cfaed32e6 31775:2b04504fcb69
     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 setup: theory -> theory
       
    10 end;
       
    11 
       
    12 structure Code_Haskell : CODE_HASKELL =
       
    13 struct
       
    14 
       
    15 val target = "Haskell";
       
    16 
       
    17 open Basic_Code_Thingol;
       
    18 open Code_Printer;
       
    19 
       
    20 infixr 5 @@;
       
    21 infixr 5 @|;
       
    22 
       
    23 
       
    24 (** Haskell serializer **)
       
    25 
       
    26 fun pr_haskell_bind pr_term =
       
    27   let
       
    28     fun pr_bind ((NONE, NONE), _) = str "_"
       
    29       | pr_bind ((SOME v, NONE), _) = str v
       
    30       | pr_bind ((NONE, SOME p), _) = p
       
    31       | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
       
    32   in gen_pr_bind pr_bind pr_term end;
       
    33 
       
    34 fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
       
    35     init_syms deresolve is_cons contr_classparam_typs deriving_show =
       
    36   let
       
    37     val deresolve_base = Long_Name.base_name o deresolve;
       
    38     fun class_name class = case syntax_class class
       
    39      of NONE => deresolve class
       
    40       | SOME class => class;
       
    41     fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
       
    42      of [] => []
       
    43       | classbinds => Pretty.enum "," "(" ")" (
       
    44           map (fn (v, class) =>
       
    45             str (class_name class ^ " " ^ Code_Printer.lookup_var tyvars v)) classbinds)
       
    46           @@ str " => ";
       
    47     fun pr_typforall tyvars vs = case map fst vs
       
    48      of [] => []
       
    49       | vnames => str "forall " :: Pretty.breaks
       
    50           (map (str o Code_Printer.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
       
    51     fun pr_tycoexpr tyvars fxy (tyco, tys) =
       
    52       brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
       
    53     and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
       
    54          of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
       
    55           | SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
       
    56       | pr_typ tyvars fxy (ITyVar v) = (str o Code_Printer.lookup_var tyvars) v;
       
    57     fun pr_typdecl tyvars (vs, tycoexpr) =
       
    58       Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
       
    59     fun pr_typscheme tyvars (vs, ty) =
       
    60       Pretty.block (pr_typforall tyvars vs @ pr_typcontext tyvars vs @| pr_typ tyvars NOBR ty);
       
    61     fun pr_term tyvars thm vars fxy (IConst c) =
       
    62           pr_app tyvars thm vars fxy (c, [])
       
    63       | pr_term tyvars thm vars fxy (t as (t1 `$ t2)) =
       
    64           (case Code_Thingol.unfold_const_app t
       
    65            of SOME app => pr_app tyvars thm vars fxy app
       
    66             | _ =>
       
    67                 brackify fxy [
       
    68                   pr_term tyvars thm vars NOBR t1,
       
    69                   pr_term tyvars thm vars BR t2
       
    70                 ])
       
    71       | pr_term tyvars thm vars fxy (IVar v) =
       
    72           (str o Code_Printer.lookup_var vars) v
       
    73       | pr_term tyvars thm vars fxy (t as _ `|=> _) =
       
    74           let
       
    75             val (binds, t') = Code_Thingol.unfold_abs t;
       
    76             fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
       
    77             val (ps, vars') = fold_map pr binds vars;
       
    78           in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm vars' NOBR t') end
       
    79       | pr_term tyvars thm vars fxy (ICase (cases as (_, t0))) =
       
    80           (case Code_Thingol.unfold_const_app t0
       
    81            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
       
    82                 then pr_case tyvars thm vars fxy cases
       
    83                 else pr_app tyvars thm vars fxy c_ts
       
    84             | NONE => pr_case tyvars thm vars fxy cases)
       
    85     and pr_app' tyvars thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
       
    86      of [] => (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
       
    87       | fingerprint => let
       
    88           val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
       
    89           val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
       
    90             (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
       
    91           fun pr_term_anno (t, NONE) _ = pr_term tyvars thm vars BR t
       
    92             | pr_term_anno (t, SOME _) ty =
       
    93                 brackets [pr_term tyvars thm vars NOBR t, str "::", pr_typ tyvars NOBR ty];
       
    94         in
       
    95           if needs_annotation then
       
    96             (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
       
    97           else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
       
    98         end
       
    99     and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const
       
   100     and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
       
   101     and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
       
   102           let
       
   103             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
       
   104             fun pr ((pat, ty), t) vars =
       
   105               vars
       
   106               |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
       
   107               |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
       
   108             val (ps, vars') = fold_map pr binds vars;
       
   109           in brackify_block fxy (str "let {")
       
   110             ps
       
   111             (concat [str "}", str "in", pr_term tyvars thm vars' NOBR body])
       
   112           end
       
   113       | pr_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
       
   114           let
       
   115             fun pr (pat, body) =
       
   116               let
       
   117                 val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
       
   118               in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end;
       
   119           in brackify_block fxy
       
   120             (concat [str "case", pr_term tyvars thm vars NOBR t, str "of", str "{"])
       
   121             (map pr clauses)
       
   122             (str "}") 
       
   123           end
       
   124       | pr_case tyvars thm vars fxy ((_, []), _) =
       
   125           (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
       
   126     fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
       
   127           let
       
   128             val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
       
   129             val n = (length o fst o Code_Thingol.unfold_fun) ty;
       
   130           in
       
   131             Pretty.chunks [
       
   132               Pretty.block [
       
   133                 (str o suffix " ::" o deresolve_base) name,
       
   134                 Pretty.brk 1,
       
   135                 pr_typscheme tyvars (vs, ty),
       
   136                 str ";"
       
   137               ],
       
   138               concat (
       
   139                 (str o deresolve_base) name
       
   140                 :: map str (replicate n "_")
       
   141                 @ str "="
       
   142                 :: str "error"
       
   143                 @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string
       
   144                     o Long_Name.base_name o Long_Name.qualifier) name
       
   145               )
       
   146             ]
       
   147           end
       
   148       | pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
       
   149           let
       
   150             val eqs = filter (snd o snd) raw_eqs;
       
   151             val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
       
   152             fun pr_eq ((ts, t), (thm, _)) =
       
   153               let
       
   154                 val consts = map_filter
       
   155                   (fn c => if (is_some o syntax_const) c
       
   156                     then NONE else (SOME o Long_Name.base_name o deresolve) c)
       
   157                     ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
       
   158                 val vars = init_syms
       
   159                   |> Code_Printer.intro_vars consts
       
   160                   |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
       
   161                        (insert (op =)) ts []);
       
   162               in
       
   163                 semicolon (
       
   164                   (str o deresolve_base) name
       
   165                   :: map (pr_term tyvars thm vars BR) ts
       
   166                   @ str "="
       
   167                   @@ pr_term tyvars thm vars NOBR t
       
   168                 )
       
   169               end;
       
   170           in
       
   171             Pretty.chunks (
       
   172               Pretty.block [
       
   173                 (str o suffix " ::" o deresolve_base) name,
       
   174                 Pretty.brk 1,
       
   175                 pr_typscheme tyvars (vs, ty),
       
   176                 str ";"
       
   177               ]
       
   178               :: map pr_eq eqs
       
   179             )
       
   180           end
       
   181       | pr_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
       
   182           let
       
   183             val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
       
   184           in
       
   185             semicolon [
       
   186               str "data",
       
   187               pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
       
   188             ]
       
   189           end
       
   190       | pr_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
       
   191           let
       
   192             val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
       
   193           in
       
   194             semicolon (
       
   195               str "newtype"
       
   196               :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
       
   197               :: str "="
       
   198               :: (str o deresolve_base) co
       
   199               :: pr_typ tyvars BR ty
       
   200               :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
       
   201             )
       
   202           end
       
   203       | pr_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
       
   204           let
       
   205             val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
       
   206             fun pr_co (co, tys) =
       
   207               concat (
       
   208                 (str o deresolve_base) co
       
   209                 :: map (pr_typ tyvars BR) tys
       
   210               )
       
   211           in
       
   212             semicolon (
       
   213               str "data"
       
   214               :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
       
   215               :: str "="
       
   216               :: pr_co co
       
   217               :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
       
   218               @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
       
   219             )
       
   220           end
       
   221       | pr_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
       
   222           let
       
   223             val tyvars = Code_Printer.intro_vars [v] init_syms;
       
   224             fun pr_classparam (classparam, ty) =
       
   225               semicolon [
       
   226                 (str o deresolve_base) classparam,
       
   227                 str "::",
       
   228                 pr_typ tyvars NOBR ty
       
   229               ]
       
   230           in
       
   231             Pretty.block_enclose (
       
   232               Pretty.block [
       
   233                 str "class ",
       
   234                 Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
       
   235                 str (deresolve_base name ^ " " ^ Code_Printer.lookup_var tyvars v),
       
   236                 str " where {"
       
   237               ],
       
   238               str "};"
       
   239             ) (map pr_classparam classparams)
       
   240           end
       
   241       | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
       
   242           let
       
   243             val split_abs_pure = (fn (v, _) `|=> t => SOME (v, t) | _ => NONE);
       
   244             val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
       
   245             val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
       
   246             fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
       
   247              of NONE => semicolon [
       
   248                     (str o deresolve_base) classparam,
       
   249                     str "=",
       
   250                     pr_app tyvars thm init_syms NOBR (c_inst, [])
       
   251                   ]
       
   252               | SOME (k, pr) =>
       
   253                   let
       
   254                     val (c_inst_name, (_, tys)) = c_inst;
       
   255                     val const = if (is_some o syntax_const) c_inst_name
       
   256                       then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name;
       
   257                     val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
       
   258                     val (vs, rhs) = unfold_abs_pure proto_rhs;
       
   259                     val vars = init_syms
       
   260                       |> Code_Printer.intro_vars (the_list const)
       
   261                       |> Code_Printer.intro_vars vs;
       
   262                     val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
       
   263                       (*dictionaries are not relevant at this late stage*)
       
   264                   in
       
   265                     semicolon [
       
   266                       pr_term tyvars thm vars NOBR lhs,
       
   267                       str "=",
       
   268                       pr_term tyvars thm vars NOBR rhs
       
   269                     ]
       
   270                   end;
       
   271           in
       
   272             Pretty.block_enclose (
       
   273               Pretty.block [
       
   274                 str "instance ",
       
   275                 Pretty.block (pr_typcontext tyvars vs),
       
   276                 str (class_name class ^ " "),
       
   277                 pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
       
   278                 str " where {"
       
   279               ],
       
   280               str "};"
       
   281             ) (map pr_instdef classparam_insts)
       
   282           end;
       
   283   in pr_stmt end;
       
   284 
       
   285 fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program =
       
   286   let
       
   287     val module_alias = if is_some module_name then K module_name else raw_module_alias;
       
   288     val reserved_names = Name.make_context reserved_names;
       
   289     val mk_name_module = Code_Printer.mk_name_module reserved_names module_prefix module_alias program;
       
   290     fun add_stmt (name, (stmt, deps)) =
       
   291       let
       
   292         val (module_name, base) = Code_Printer.dest_name name;
       
   293         val module_name' = mk_name_module module_name;
       
   294         val mk_name_stmt = yield_singleton Name.variants;
       
   295         fun add_fun upper (nsp_fun, nsp_typ) =
       
   296           let
       
   297             val (base', nsp_fun') =
       
   298               mk_name_stmt (if upper then Code_Printer.first_upper base else base) nsp_fun
       
   299           in (base', (nsp_fun', nsp_typ)) end;
       
   300         fun add_typ (nsp_fun, nsp_typ) =
       
   301           let
       
   302             val (base', nsp_typ') = mk_name_stmt (Code_Printer.first_upper base) nsp_typ
       
   303           in (base', (nsp_fun, nsp_typ')) end;
       
   304         val add_name = case stmt
       
   305          of Code_Thingol.Fun _ => add_fun false
       
   306           | Code_Thingol.Datatype _ => add_typ
       
   307           | Code_Thingol.Datatypecons _ => add_fun true
       
   308           | Code_Thingol.Class _ => add_typ
       
   309           | Code_Thingol.Classrel _ => pair base
       
   310           | Code_Thingol.Classparam _ => add_fun false
       
   311           | Code_Thingol.Classinst _ => pair base;
       
   312         fun add_stmt' base' = case stmt
       
   313          of Code_Thingol.Datatypecons _ =>
       
   314               cons (name, (Long_Name.append module_name' base', NONE))
       
   315           | Code_Thingol.Classrel _ => I
       
   316           | Code_Thingol.Classparam _ =>
       
   317               cons (name, (Long_Name.append module_name' base', NONE))
       
   318           | _ => cons (name, (Long_Name.append module_name' base', SOME stmt));
       
   319       in
       
   320         Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names))))
       
   321               (apfst (fold (insert (op = : string * string -> bool)) deps))
       
   322         #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name'))
       
   323         #-> (fn (base', names) =>
       
   324               (Symtab.map_entry module_name' o apsnd) (fn (stmts, _) =>
       
   325               (add_stmt' base' stmts, names)))
       
   326       end;
       
   327     val hs_program = fold add_stmt (AList.make (fn name =>
       
   328       (Graph.get_node program name, Graph.imm_succs program name))
       
   329       (Graph.strong_conn program |> flat)) Symtab.empty;
       
   330     fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the
       
   331       o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Printer.dest_name) name))) name
       
   332       handle Option => error ("Unknown statement name: " ^ labelled_name name);
       
   333   in (deresolver, hs_program) end;
       
   334 
       
   335 fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
       
   336     raw_reserved_names includes raw_module_alias
       
   337     syntax_class syntax_tyco syntax_const program cs destination =
       
   338   let
       
   339     val stmt_names = Code_Target.stmt_names_of_destination destination;
       
   340     val module_name = if null stmt_names then raw_module_name else SOME "Code";
       
   341     val reserved_names = fold (insert (op =) o fst) includes raw_reserved_names;
       
   342     val (deresolver, hs_program) = haskell_program_of_program labelled_name
       
   343       module_name module_prefix reserved_names raw_module_alias program;
       
   344     val is_cons = Code_Thingol.is_cons program;
       
   345     val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
       
   346     fun deriving_show tyco =
       
   347       let
       
   348         fun deriv _ "fun" = false
       
   349           | deriv tycos tyco = member (op =) tycos tyco orelse
       
   350               case try (Graph.get_node program) tyco
       
   351                 of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
       
   352                     (maps snd cs)
       
   353                  | NONE => true
       
   354         and deriv' tycos (tyco `%% tys) = deriv tycos tyco
       
   355               andalso forall (deriv' tycos) tys
       
   356           | deriv' _ (ITyVar _) = true
       
   357       in deriv [] tyco end;
       
   358     val reserved_names = Code_Printer.make_vars reserved_names;
       
   359     fun pr_stmt qualified = pr_haskell_stmt labelled_name
       
   360       syntax_class syntax_tyco syntax_const reserved_names
       
   361       (if qualified then deresolver else Long_Name.base_name o deresolver)
       
   362       is_cons contr_classparam_typs
       
   363       (if string_classes then deriving_show else K false);
       
   364     fun pr_module name content =
       
   365       (name, Pretty.chunks [
       
   366         str ("module " ^ name ^ " where {"),
       
   367         str "",
       
   368         content,
       
   369         str "",
       
   370         str "}"
       
   371       ]);
       
   372     fun serialize_module1 (module_name', (deps, (stmts, _))) =
       
   373       let
       
   374         val stmt_names = map fst stmts;
       
   375         val deps' = subtract (op =) stmt_names deps
       
   376           |> distinct (op =)
       
   377           |> map_filter (try deresolver);
       
   378         val qualified = is_none module_name andalso
       
   379           map deresolver stmt_names @ deps'
       
   380           |> map Long_Name.base_name
       
   381           |> has_duplicates (op =);
       
   382         val imports = deps'
       
   383           |> map Long_Name.qualifier
       
   384           |> distinct (op =);
       
   385         fun pr_import_include (name, _) = str ("import qualified " ^ name ^ ";");
       
   386         val pr_import_module = str o (if qualified
       
   387           then prefix "import qualified "
       
   388           else prefix "import ") o suffix ";";
       
   389         val content = Pretty.chunks (
       
   390             map pr_import_include includes
       
   391             @ map pr_import_module imports
       
   392             @ str ""
       
   393             :: separate (str "") (map_filter
       
   394               (fn (name, (_, SOME stmt)) => SOME (pr_stmt qualified (name, stmt))
       
   395                 | (_, (_, NONE)) => NONE) stmts)
       
   396           )
       
   397       in pr_module module_name' content end;
       
   398     fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks (
       
   399       separate (str "") (map_filter
       
   400         (fn (name, (_, SOME stmt)) => if null stmt_names
       
   401               orelse member (op =) stmt_names name
       
   402               then SOME (pr_stmt false (name, stmt))
       
   403               else NONE
       
   404           | (_, (_, NONE)) => NONE) stmts));
       
   405     val serialize_module =
       
   406       if null stmt_names then serialize_module1 else pair "" o serialize_module2;
       
   407     fun check_destination destination =
       
   408       (File.check destination; destination);
       
   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 Long_Name.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
       
   424         (write_module (check_destination 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 _ [c_bind'] pr thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
       
   471      of SOME (bind, t') => let
       
   472           val (binds, t'') = implode_monad 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, ([c_bind], pretty)) end;
       
   478 
       
   479 fun add_monad target' raw_c_bind thy =
       
   480   let
       
   481     val c_bind = Code.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*)