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