src/Pure/Tools/codegen_serializer.ML
author haftmann
Wed Aug 30 15:11:17 2006 +0200 (2006-08-30)
changeset 20439 1bf42b262a38
parent 20428 67fa1c6ba89e
child 20456 42be3a46dcd8
permissions -rw-r--r--
code refinements
haftmann@18169
     1
(*  Title:      Pure/Tools/codegen_serializer.ML
haftmann@18169
     2
    ID:         $Id$
haftmann@18169
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@18169
     4
haftmann@18169
     5
Serializer from intermediate language ("Thin-gol") to
haftmann@18216
     6
target languages (like ML or Haskell).
haftmann@18169
     7
*)
haftmann@18169
     8
haftmann@18169
     9
signature CODEGEN_SERIALIZER =
haftmann@18169
    10
sig
haftmann@18702
    11
  type 'a pretty_syntax;
haftmann@20191
    12
  type serializer =
haftmann@18702
    13
      string list list
haftmann@18756
    14
      -> OuterParse.token list ->
haftmann@20428
    15
      ((string -> (string * (string -> string option)) option)
haftmann@18865
    16
        * (string -> CodegenThingol.itype pretty_syntax option)
haftmann@20105
    17
        * (string -> CodegenThingol.iterm pretty_syntax option)
haftmann@19884
    18
      -> string list * string list option
haftmann@18756
    19
      -> CodegenThingol.module -> unit)
haftmann@18756
    20
      * OuterParse.token list;
haftmann@19042
    21
  val parse_syntax: ('b -> int) -> (string -> 'b -> 'a * 'b) -> OuterParse.token list ->
haftmann@18702
    22
    ('b -> 'a pretty_syntax * 'b) * OuterParse.token list;
haftmann@20401
    23
  val pretty_list: string -> string -> (Pretty.T list -> Pretty.T)
haftmann@20401
    24
    -> ((string -> string) * (string -> string)) option
haftmann@20401
    25
    -> int * string -> CodegenThingol.iterm pretty_syntax;
haftmann@20401
    26
  val pretty_ml_string: string -> string -> (string -> string) -> (string -> string)
haftmann@20401
    27
    -> string -> CodegenThingol.iterm pretty_syntax;
haftmann@18702
    28
  val serializers: {
haftmann@20183
    29
    ml: string * (string -> serializer),
haftmann@19953
    30
    haskell: string * (string * string list -> serializer)
haftmann@19042
    31
  };
haftmann@19150
    32
  val mk_flat_ml_resolver: string list -> string -> string;
haftmann@20216
    33
  val eval_term: string -> string -> string list list
haftmann@20428
    34
    -> (string -> CodegenThingol.itype pretty_syntax option)
haftmann@20428
    35
          * (string -> CodegenThingol.iterm pretty_syntax option)
haftmann@20428
    36
    -> string list
haftmann@20428
    37
    -> (string * 'a ref) * CodegenThingol.iterm -> CodegenThingol.module
haftmann@20428
    38
    -> 'a;
haftmann@20389
    39
  val eval_verbose: bool ref;
haftmann@20183
    40
  val ml_fun_datatype: string
haftmann@19042
    41
    -> ((string -> CodegenThingol.itype pretty_syntax option)
haftmann@20105
    42
        * (string -> CodegenThingol.iterm pretty_syntax option))
haftmann@19042
    43
    -> (string -> string)
haftmann@19042
    44
    -> ((string * CodegenThingol.funn) list -> Pretty.T)
haftmann@19042
    45
        * ((string * CodegenThingol.datatyp) list -> Pretty.T);
haftmann@18169
    46
end;
haftmann@18169
    47
haftmann@18169
    48
structure CodegenSerializer: CODEGEN_SERIALIZER =
haftmann@18169
    49
struct
haftmann@18169
    50
haftmann@19167
    51
open BasicCodegenThingol;
haftmann@19341
    52
val debug_msg = CodegenThingol.debug_msg;
haftmann@18850
    53
haftmann@18216
    54
(** generic serialization **)
haftmann@18216
    55
haftmann@18702
    56
(* precedences *)
haftmann@18702
    57
haftmann@18216
    58
datatype lrx = L | R | X;
haftmann@18216
    59
haftmann@18516
    60
datatype fixity =
haftmann@18216
    61
    BR
haftmann@18216
    62
  | NOBR
haftmann@18216
    63
  | INFX of (int * lrx);
haftmann@18216
    64
haftmann@18702
    65
datatype 'a mixfix =
haftmann@18702
    66
    Arg of fixity
haftmann@18702
    67
  | Ignore
haftmann@18702
    68
  | Pretty of Pretty.T
haftmann@18702
    69
  | Quote of 'a;
haftmann@18516
    70
haftmann@18865
    71
type 'a pretty_syntax = (int * int) * (fixity -> (fixity -> 'a -> Pretty.T)
haftmann@18865
    72
  -> 'a list -> Pretty.T);
haftmann@18516
    73
haftmann@18216
    74
fun eval_lrx L L = false
haftmann@18216
    75
  | eval_lrx R R = false
haftmann@18216
    76
  | eval_lrx _ _ = true;
haftmann@18216
    77
haftmann@18704
    78
fun eval_fxy NOBR _ = false
haftmann@18704
    79
  | eval_fxy _ BR = true
haftmann@18704
    80
  | eval_fxy _ NOBR = false
haftmann@18704
    81
  | eval_fxy (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) =
haftmann@18704
    82
      pr < pr_ctxt
haftmann@18704
    83
      orelse pr = pr_ctxt
haftmann@18704
    84
        andalso eval_lrx lr lr_ctxt
haftmann@18704
    85
  | eval_fxy _ (INFX _) = false;
haftmann@18216
    86
haftmann@18702
    87
val str = setmp print_mode [] Pretty.str;
haftmann@18216
    88
haftmann@18704
    89
fun gen_brackify _ [p] = p
haftmann@18704
    90
  | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps
haftmann@18704
    91
  | gen_brackify false (ps as _::_) = Pretty.block ps;
haftmann@18704
    92
haftmann@18704
    93
fun brackify fxy_ctxt ps =
haftmann@18704
    94
  gen_brackify (eval_fxy BR fxy_ctxt) (Pretty.breaks ps);
haftmann@18704
    95
haftmann@18704
    96
fun brackify_infix infx fxy_ctxt ps =
haftmann@18704
    97
  gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps);
haftmann@18216
    98
haftmann@19607
    99
fun from_app mk_app from_expr const_syntax fxy (const as (c, _), es) =
haftmann@20191
   100
  case const_syntax c
haftmann@19607
   101
   of NONE => brackify fxy (mk_app c es)
haftmann@19607
   102
    | SOME ((i, k), pr) =>
haftmann@19607
   103
        if i <= length es
haftmann@19607
   104
          then case chop k es of (es1, es2) =>
haftmann@19607
   105
            brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2)
haftmann@19607
   106
          else from_expr fxy (CodegenThingol.eta_expand (const, es) i);
haftmann@18865
   107
haftmann@18704
   108
fun fillin_mixfix fxy_this ms fxy_ctxt pr args =
haftmann@18702
   109
  let
haftmann@18702
   110
    fun fillin [] [] =
haftmann@19008
   111
          []
haftmann@18702
   112
      | fillin (Arg fxy :: ms) (a :: args) =
haftmann@18702
   113
          pr fxy a :: fillin ms args
haftmann@18702
   114
      | fillin (Ignore :: ms) args =
haftmann@18702
   115
          fillin ms args
haftmann@18702
   116
      | fillin (Pretty p :: ms) args =
haftmann@18702
   117
          p :: fillin ms args
haftmann@18702
   118
      | fillin (Quote q :: ms) args =
haftmann@19008
   119
          pr BR q :: fillin ms args
haftmann@19008
   120
      | fillin [] _ =
haftmann@20389
   121
          error ("Inconsistent mixfix: too many arguments")
haftmann@19008
   122
      | fillin _ [] =
haftmann@20389
   123
          error ("Inconsistent mixfix: too less arguments");
haftmann@18704
   124
  in gen_brackify (eval_fxy fxy_this fxy_ctxt) (fillin ms args) end;
haftmann@18702
   125
haftmann@18702
   126
haftmann@18702
   127
(* user-defined syntax *)
haftmann@18702
   128
haftmann@18702
   129
val (atomK, infixK, infixlK, infixrK) =
haftmann@18756
   130
  ("target_atom", "infix", "infixl", "infixr");
haftmann@18756
   131
val _ = OuterSyntax.add_keywords [atomK, infixK, infixlK, infixrK];
haftmann@18216
   132
haftmann@18702
   133
fun parse_infix (fixity as INFX (i, x)) s =
haftmann@18702
   134
  let
haftmann@18702
   135
    val l = case x of L => fixity
haftmann@18702
   136
                    | _ => INFX (i, X);
haftmann@18702
   137
    val r = case x of R => fixity
haftmann@18702
   138
                    | _ => INFX (i, X);
haftmann@18702
   139
  in
haftmann@18702
   140
    pair [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]
haftmann@18702
   141
  end;
haftmann@18702
   142
haftmann@18702
   143
fun parse_mixfix reader s ctxt =
haftmann@18335
   144
  let
haftmann@18702
   145
    fun sym s = Scan.lift ($$ s);
haftmann@18702
   146
    fun lift_reader ctxt s =
haftmann@18702
   147
      ctxt
haftmann@18702
   148
      |> reader s
haftmann@18702
   149
      |-> (fn x => pair (Quote x));
haftmann@18702
   150
    val sym_any = Scan.lift (Scan.one Symbol.not_eof);
haftmann@18702
   151
    val parse = Scan.repeat (
haftmann@18702
   152
         (sym "_" -- sym "_" >> K (Arg NOBR))
haftmann@18702
   153
      || (sym "_" >> K (Arg BR))
haftmann@18702
   154
      || (sym "?" >> K Ignore)
haftmann@18702
   155
      || (sym "/" |-- Scan.repeat (sym " ") >> (Pretty o Pretty.brk o length))
haftmann@18702
   156
      || Scan.depend (fn ctxt => $$ "{" |-- $$ "*" |-- Scan.repeat1
haftmann@18702
   157
           (   $$ "'" |-- Scan.one Symbol.not_eof
haftmann@18702
   158
            || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
haftmann@18702
   159
         $$ "*" --| $$ "}" >> (implode #> lift_reader ctxt #> swap))
haftmann@18702
   160
      || (Scan.repeat1
haftmann@18702
   161
           (   sym "'" |-- sym_any
haftmann@18702
   162
            || Scan.unless (sym "_" || sym "?" || sym "/" || sym "{" |-- sym "*")
haftmann@18702
   163
                 sym_any) >> (Pretty o str o implode)));
haftmann@18702
   164
  in case Scan.finite' Symbol.stopper parse (ctxt, Symbol.explode s)
haftmann@18702
   165
   of (p, (ctxt, [])) => (p, ctxt)
haftmann@18702
   166
    | _ => error ("Malformed mixfix annotation: " ^ quote s)
haftmann@18702
   167
  end;
haftmann@18702
   168
haftmann@20439
   169
fun parse_syntax num_args reader =
haftmann@18335
   170
  let
haftmann@18702
   171
    fun is_arg (Arg _) = true
haftmann@18702
   172
      | is_arg Ignore = true
haftmann@18702
   173
      | is_arg _ = false;
haftmann@20439
   174
    fun parse_nonatomic s ctxt =
haftmann@20439
   175
      case parse_mixfix reader s ctxt
haftmann@20439
   176
       of ([Pretty _], _) =>
haftmann@20439
   177
            error ("Mixfix contains just one pretty element; either declare as "
haftmann@20439
   178
              ^ quote atomK ^ " or consider adding a break")
haftmann@20439
   179
        | x => x;
haftmann@20439
   180
    val parse = OuterParse.$$$ "(" |-- (
haftmann@20439
   181
           OuterParse.$$$ infixK  |-- OuterParse.nat
haftmann@20439
   182
            >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X)))
haftmann@20439
   183
        || OuterParse.$$$ infixlK |-- OuterParse.nat
haftmann@20439
   184
            >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L)))
haftmann@20439
   185
        || OuterParse.$$$ infixrK |-- OuterParse.nat
haftmann@20439
   186
            >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R)))
haftmann@20439
   187
        || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR)
haftmann@20439
   188
        || pair (parse_nonatomic, BR)
haftmann@20439
   189
      ) -- OuterParse.string --| OuterParse.$$$ ")" >> (fn ((p, fxy), s) => (p s, fxy));
haftmann@19042
   190
    fun mk fixity mfx ctxt =
haftmann@18702
   191
      let
haftmann@19042
   192
        val i = (length o List.filter is_arg) mfx;
haftmann@20439
   193
        val _ = if i > num_args ctxt then error "Too many arguments in codegen syntax" else ();
haftmann@19042
   194
      in (((i, i), fillin_mixfix fixity mfx), ctxt) end;
haftmann@18702
   195
  in
haftmann@20439
   196
    parse
haftmann@19042
   197
    #-> (fn (mfx_reader, fixity) =>
haftmann@19042
   198
      pair (mfx_reader #-> (fn mfx => mk fixity mfx))
haftmann@18702
   199
    )
haftmann@18702
   200
  end;
haftmann@18702
   201
haftmann@18702
   202
haftmann@19607
   203
(* generic abstract serializer *)
haftmann@18282
   204
haftmann@20191
   205
type serializer =
haftmann@18702
   206
    string list list
haftmann@18756
   207
    -> OuterParse.token list ->
haftmann@20428
   208
    ((string -> (string * (string -> string option)) option)
haftmann@18963
   209
      * (string -> itype pretty_syntax option)
haftmann@20105
   210
      * (string -> iterm pretty_syntax option)
haftmann@19884
   211
    -> string list * string list option
haftmann@19167
   212
    -> CodegenThingol.module -> unit)
haftmann@18756
   213
    * OuterParse.token list;
haftmann@18702
   214
haftmann@18919
   215
fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator, postproc)
haftmann@20428
   216
    postprocess (class_syntax : string -> (string * (string -> string option)) option, tyco_syntax, const_syntax)
haftmann@19884
   217
    (drop: string list, select) module =
haftmann@18702
   218
  let
haftmann@19341
   219
    fun from_module' resolv imps ((name_qual, name), defs) =
haftmann@19341
   220
      from_module resolv imps ((name_qual, name), defs)
haftmann@19341
   221
      |> postprocess (resolv name_qual);
haftmann@18702
   222
  in
haftmann@18702
   223
    module
haftmann@20191
   224
    |> debug_msg (fn _ => "dropping shadowed defintions...")
haftmann@20191
   225
    |> CodegenThingol.delete_garbage drop
haftmann@19341
   226
    |> debug_msg (fn _ => "selecting submodule...")
haftmann@19341
   227
    |> (if is_some select then (CodegenThingol.project_module o the) select else I)
haftmann@19341
   228
    |> debug_msg (fn _ => "serializing...")
haftmann@20428
   229
    |> CodegenThingol.serialize (from_defs (class_syntax, tyco_syntax, const_syntax))
haftmann@18919
   230
         from_module' validator postproc nspgrp name_root
haftmann@18850
   231
    |> K ()
haftmann@18702
   232
  end;
haftmann@18702
   233
haftmann@18702
   234
fun abstract_validator keywords name =
haftmann@18702
   235
  let
wenzelm@20203
   236
    fun replace_invalid c =  (* FIXME *)
wenzelm@20203
   237
      if Symbol.is_ascii_letter c orelse Symbol.is_ascii_digit c orelse c = "'"
haftmann@18702
   238
      andalso not (NameSpace.separator = c)
haftmann@18702
   239
      then c
haftmann@18702
   240
      else "_"
haftmann@20191
   241
    fun suffix_it name=
haftmann@18702
   242
      name
haftmann@18702
   243
      |> member (op =) keywords ? suffix "'"
haftmann@18702
   244
      |> (fn name' => if name = name' then name else suffix_it name')
haftmann@18702
   245
  in
haftmann@18702
   246
    name
haftmann@18702
   247
    |> translate_string replace_invalid
haftmann@18702
   248
    |> suffix_it
haftmann@18702
   249
    |> (fn name' => if name = name' then NONE else SOME name')
haftmann@18702
   250
  end;
haftmann@18702
   251
haftmann@18850
   252
fun write_file mkdir path p = (
haftmann@18850
   253
    if mkdir
haftmann@18850
   254
      then
haftmann@18850
   255
        File.mkdir (Path.dir path)
haftmann@18850
   256
      else ();
haftmann@18850
   257
      File.write path (Pretty.output p ^ "\n");
haftmann@18850
   258
      p
haftmann@18850
   259
  );
haftmann@18850
   260
haftmann@18850
   261
fun mk_module_file postprocess_module ext path name p =
haftmann@18850
   262
  let
haftmann@18850
   263
    val prfx = Path.dir path;
haftmann@18850
   264
    val name' = case name
haftmann@18850
   265
     of "" => Path.base path
haftmann@18850
   266
      | _ => (Path.ext ext o Path.unpack o implode o separate "/" o NameSpace.unpack) name;
haftmann@18850
   267
  in
haftmann@18850
   268
    p
haftmann@18850
   269
    |> write_file true (Path.append prfx name')
haftmann@18850
   270
    |> postprocess_module name
haftmann@18850
   271
  end;
haftmann@18850
   272
haftmann@19953
   273
fun constructive_fun is_cons (name, (eqs, ty)) =
haftmann@19202
   274
  let
haftmann@19202
   275
    fun check_eq (eq as (lhs, rhs)) =
haftmann@19953
   276
      if forall (CodegenThingol.is_pat is_cons) lhs
haftmann@19202
   277
      then SOME eq
haftmann@20389
   278
      else (warning ("In function " ^ quote name ^ ", throwing away one "
haftmann@19202
   279
        ^ "non-executable function clause"); NONE)
wenzelm@19482
   280
  in case map_filter check_eq eqs
haftmann@20389
   281
   of [] => error ("In function " ^ quote name ^ ", no "
haftmann@19202
   282
        ^ "executable function clauses found")
haftmann@19202
   283
    | eqs => (name, (eqs, ty))
haftmann@19202
   284
  end;
haftmann@19202
   285
haftmann@18756
   286
fun parse_single_file serializer =
haftmann@18850
   287
  OuterParse.path
haftmann@18850
   288
  >> (fn path => serializer
haftmann@18850
   289
        (fn "" => write_file false path #> K NONE
haftmann@18850
   290
          | _ => SOME));
haftmann@18850
   291
haftmann@18850
   292
fun parse_multi_file postprocess_module ext serializer =
haftmann@18850
   293
  OuterParse.path
haftmann@18850
   294
  >> (fn path => (serializer o mk_module_file postprocess_module ext) path);
haftmann@18702
   295
haftmann@18756
   296
fun parse_internal serializer =
haftmann@18756
   297
  OuterParse.name
haftmann@18850
   298
  >> (fn "-" => serializer
haftmann@18850
   299
        (fn "" => (fn p => (use_text Context.ml_output false (Pretty.output p); NONE))
haftmann@18850
   300
          | _ => SOME)
haftmann@18756
   301
       | _ => Scan.fail ());
haftmann@18702
   302
haftmann@20105
   303
fun parse_stdout serializer =
haftmann@20105
   304
  OuterParse.name
haftmann@20105
   305
  >> (fn "_" => serializer
haftmann@20105
   306
        (fn "" => (fn p => (Pretty.writeln p; NONE))
haftmann@20105
   307
          | _ => SOME)
haftmann@20105
   308
       | _ => Scan.fail ());
haftmann@18282
   309
haftmann@18704
   310
haftmann@20401
   311
(* list and string serializers *)
haftmann@20401
   312
haftmann@20401
   313
fun implode_list c_nil c_cons e =
haftmann@18704
   314
  let
haftmann@19202
   315
    fun dest_cons (IConst (c, _) `$ e1 `$ e2) =
haftmann@20401
   316
          if c = c_cons
haftmann@18704
   317
          then SOME (e1, e2)
haftmann@18704
   318
          else NONE
haftmann@18704
   319
      | dest_cons  _ = NONE;
haftmann@20401
   320
    val (es, e') = CodegenThingol.unfoldr dest_cons e;
haftmann@20401
   321
  in case e'
haftmann@20401
   322
   of IConst (c, _) => if c = c_nil then SOME es else NONE
haftmann@20401
   323
    | _ => NONE
haftmann@20401
   324
  end;
haftmann@20401
   325
haftmann@20401
   326
fun implode_string mk_char mk_string es =
haftmann@20401
   327
  if forall (fn IChar _ => true | _ => false) es
haftmann@20401
   328
  then (SOME o str o mk_string o implode o map (fn IChar (c, _) => mk_char c)) es
haftmann@20401
   329
  else NONE;
haftmann@20401
   330
haftmann@20401
   331
fun pretty_ml_string c_nil c_cons mk_char mk_string target_implode =
haftmann@20401
   332
  let
haftmann@20401
   333
    fun pretty fxy pr [e] =
haftmann@20401
   334
      case implode_list c_nil c_cons e
haftmann@20401
   335
       of SOME es => (case implode_string mk_char mk_string es
haftmann@20401
   336
           of SOME p => p
haftmann@20401
   337
            | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr BR e])
haftmann@20401
   338
        | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr BR e]
haftmann@20401
   339
  in ((1, 1), pretty) end;
haftmann@20401
   340
haftmann@20401
   341
fun pretty_list c_nil c_cons mk_list mk_char_string (target_fxy, target_cons) =
haftmann@20401
   342
  let
haftmann@20401
   343
    fun default fxy pr e1 e2 =
haftmann@20401
   344
      brackify_infix (target_fxy, R) fxy [
haftmann@20401
   345
        pr (INFX (target_fxy, X)) e1,
haftmann@18704
   346
        str target_cons,
haftmann@20401
   347
        pr (INFX (target_fxy, R)) e2
haftmann@18704
   348
      ];
haftmann@20401
   349
    fun pretty fxy pr [e1, e2] =
haftmann@20401
   350
      case Option.map (cons e1) (implode_list c_nil c_cons e2)
haftmann@20401
   351
       of SOME es =>
haftmann@20401
   352
            (case mk_char_string
haftmann@20401
   353
             of SOME (mk_char, mk_string) =>
haftmann@20401
   354
                  (case implode_string mk_char mk_string es
haftmann@20401
   355
                   of SOME p => p
haftmann@20401
   356
                    | NONE => mk_list (map (pr NOBR) es))
haftmann@20401
   357
              | NONE => mk_list (map (pr NOBR) es))
haftmann@20401
   358
        | NONE => default fxy pr e1 e2;
haftmann@20401
   359
  in ((2, 2), pretty) end;
haftmann@18704
   360
haftmann@18704
   361
haftmann@18216
   362
haftmann@18216
   363
(** ML serializer **)
haftmann@18216
   364
haftmann@18216
   365
local
haftmann@18216
   366
haftmann@19150
   367
val reserved_ml = ThmDatabase.ml_reserved @ [
haftmann@20401
   368
  "bool", "int", "list", "unit", "option", "true", "false", "not", "NONE", "SOME",
haftmann@20401
   369
  "o", "string", "char", "String", "Term"
haftmann@20401
   370
];
haftmann@19150
   371
haftmann@19150
   372
structure NameMangler = NameManglerFun (
haftmann@19150
   373
  type ctxt = string list;
haftmann@19150
   374
  type src = string;
haftmann@19150
   375
  val ord = string_ord;
wenzelm@20203
   376
  fun mk reserved_ml (name, i) =
wenzelm@20203
   377
    (Symbol.alphanum o NameSpace.base) name ^ replicate_string i "'";
haftmann@19607
   378
  fun is_valid (reserved_ml : string list) = not o member (op =) reserved_ml;
haftmann@19150
   379
  fun maybe_unique _ _ = NONE;
haftmann@20389
   380
  fun re_mangle _ dst = error ("No such definition name: " ^ quote dst);
haftmann@19150
   381
);
haftmann@19150
   382
haftmann@20428
   383
fun first_upper s =
haftmann@20428
   384
  implode (nth_map 0 (Symbol.to_ascii_upper) (explode s));
haftmann@20428
   385
haftmann@20428
   386
fun ml_from_dictvar v = 
haftmann@20428
   387
  first_upper v ^ "_";
haftmann@20428
   388
haftmann@20183
   389
fun ml_expr_seri is_cons (tyco_syntax, const_syntax) resolv =
haftmann@18216
   390
  let
haftmann@18865
   391
    val ml_from_label =
haftmann@19042
   392
      str o translate_string (fn "_" => "__" | "." => "_" | c => c)
haftmann@19042
   393
        o NameSpace.base o resolv;
haftmann@19953
   394
    fun ml_from_tyvar (v, []) =
haftmann@19953
   395
          str "()"
haftmann@19953
   396
      | ml_from_tyvar (v, sort) =
haftmann@19953
   397
          let
haftmann@19953
   398
            fun mk_class class =
haftmann@19953
   399
              str (prefix "'" v ^ " " ^ resolv class);
haftmann@19953
   400
          in
haftmann@19953
   401
            Pretty.block [
haftmann@19953
   402
              str "(",
haftmann@20428
   403
              (str o ml_from_dictvar) v,
haftmann@19953
   404
              str ":",
haftmann@19953
   405
              case sort
haftmann@19953
   406
               of [class] => mk_class class
haftmann@19953
   407
                | _ => Pretty.enum " *" "" "" (map mk_class sort),
haftmann@20191
   408
            str ")"
haftmann@19953
   409
            ]
haftmann@19953
   410
          end;
haftmann@19280
   411
    fun ml_from_sortlookup fxy lss =
haftmann@18885
   412
      let
haftmann@19042
   413
        fun from_label l =
haftmann@19341
   414
          Pretty.block [str "#",
haftmann@19341
   415
            if (is_some o Int.fromString) l then str l
haftmann@19341
   416
            else ml_from_label l
haftmann@19341
   417
          ];
haftmann@20401
   418
        fun from_lookup fxy [] p =
haftmann@20401
   419
              p
haftmann@20401
   420
          | from_lookup fxy [l] p =
haftmann@19042
   421
              brackify fxy [
haftmann@19042
   422
                from_label l,
haftmann@20401
   423
                p
haftmann@19042
   424
              ]
haftmann@20401
   425
          | from_lookup fxy ls p =
haftmann@19042
   426
              brackify fxy [
haftmann@19042
   427
                Pretty.enum " o" "(" ")" (map from_label ls),
haftmann@20401
   428
                p
haftmann@19042
   429
              ];
haftmann@18885
   430
        fun from_classlookup fxy (Instance (inst, lss)) =
haftmann@18885
   431
              brackify fxy (
haftmann@18885
   432
                (str o resolv) inst
haftmann@18885
   433
                :: map (ml_from_sortlookup BR) lss
haftmann@18885
   434
              )
haftmann@18885
   435
          | from_classlookup fxy (Lookup (classes, (v, ~1))) =
haftmann@19953
   436
              from_lookup BR classes
haftmann@20428
   437
                ((str o ml_from_dictvar) v)
haftmann@18885
   438
          | from_classlookup fxy (Lookup (classes, (v, i))) =
haftmann@19953
   439
              from_lookup BR (string_of_int (i+1) :: classes)
haftmann@20428
   440
                ((str o ml_from_dictvar) v)
haftmann@19280
   441
      in case lss
haftmann@19253
   442
       of [] => str "()"
haftmann@19280
   443
        | [ls] => from_classlookup fxy ls
haftmann@19280
   444
        | lss => (Pretty.list "(" ")" o map (from_classlookup NOBR)) lss
haftmann@18885
   445
      end;
haftmann@18963
   446
    fun ml_from_tycoexpr fxy (tyco, tys) =
haftmann@18963
   447
      let
haftmann@18963
   448
        val tyco' = (str o resolv) tyco
haftmann@18963
   449
      in case map (ml_from_type BR) tys
haftmann@18963
   450
       of [] => tyco'
haftmann@18963
   451
        | [p] => Pretty.block [p, Pretty.brk 1, tyco']
haftmann@18963
   452
        | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
haftmann@18963
   453
      end
haftmann@19167
   454
    and ml_from_type fxy (tycoexpr as tyco `%% tys) =
haftmann@18702
   455
          (case tyco_syntax tyco
haftmann@18963
   456
           of NONE => ml_from_tycoexpr fxy (tyco, tys)
haftmann@18702
   457
            | SOME ((i, k), pr) =>
haftmann@18702
   458
                if not (i <= length tys andalso length tys <= k)
haftmann@20389
   459
                then error ("Number of argument mismatch in customary serialization: "
haftmann@18865
   460
                  ^ (string_of_int o length) tys ^ " given, "
haftmann@18865
   461
                  ^ string_of_int i ^ " to " ^ string_of_int k
haftmann@18702
   462
                  ^ " expected")
haftmann@18702
   463
                else pr fxy ml_from_type tys)
haftmann@19167
   464
      | ml_from_type fxy (t1 `-> t2) =
haftmann@18216
   465
          let
haftmann@18704
   466
            val brackify = gen_brackify
haftmann@18704
   467
              (case fxy
haftmann@18704
   468
                of BR => false
haftmann@18704
   469
                 | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks;
haftmann@18216
   470
          in
haftmann@18704
   471
            brackify [
haftmann@18702
   472
              ml_from_type (INFX (1, X)) t1,
haftmann@18702
   473
              str "->",
haftmann@18702
   474
              ml_from_type (INFX (1, R)) t2
haftmann@18702
   475
            ]
haftmann@18216
   476
          end
haftmann@19167
   477
      | ml_from_type fxy (ITyVar v) =
haftmann@18885
   478
          str ("'" ^ v);
haftmann@19167
   479
    fun ml_from_expr fxy (e as IConst x) =
haftmann@19167
   480
          ml_from_app fxy (x, [])
haftmann@19167
   481
      | ml_from_expr fxy (IVar v) =
haftmann@19167
   482
          str v
haftmann@19167
   483
      | ml_from_expr fxy (e as e1 `$ e2) =
haftmann@19167
   484
          (case CodegenThingol.unfold_const_app e
haftmann@18885
   485
           of SOME x => ml_from_app fxy x
haftmann@18865
   486
            | NONE =>
haftmann@18704
   487
                brackify fxy [
haftmann@18885
   488
                  ml_from_expr NOBR e1,
haftmann@18885
   489
                  ml_from_expr BR e2
haftmann@18216
   490
                ])
haftmann@20105
   491
      | ml_from_expr fxy (e as _ `|-> _) =
haftmann@20105
   492
          let
haftmann@20105
   493
            val (es, be) = CodegenThingol.unfold_abs e;
haftmann@20105
   494
            fun mk_abs (e, ty) = (Pretty.block o Pretty.breaks) [
haftmann@20105
   495
                str "fn",
haftmann@20183
   496
                ml_from_expr NOBR e,
haftmann@20105
   497
                str "=>"
haftmann@20105
   498
              ];
haftmann@20105
   499
          in brackify BR (map mk_abs es @ [ml_from_expr NOBR be]) end
haftmann@19607
   500
      | ml_from_expr fxy (INum (n, _)) =
haftmann@19213
   501
          brackify BR [
haftmann@19202
   502
            (str o IntInf.toString) n,
haftmann@19884
   503
            str ":",
haftmann@19884
   504
            str "IntInf.int"
haftmann@19202
   505
          ]
haftmann@19607
   506
      | ml_from_expr _ (IChar (c, _)) =
haftmann@19607
   507
          (str o prefix "#" o quote)
wenzelm@20203
   508
            (let val i = ord c
haftmann@20191
   509
              in if i < 32
haftmann@20105
   510
                then prefix "\\" (string_of_int i)
haftmann@19607
   511
                else c
haftmann@19607
   512
              end)
haftmann@19167
   513
      | ml_from_expr fxy (e as ICase ((_, [_]), _)) =
haftmann@18216
   514
          let
haftmann@19167
   515
            val (ves, be) = CodegenThingol.unfold_let e;
haftmann@19167
   516
            fun mk_val ((ve, vty), se) = Pretty.block [
haftmann@19167
   517
                (Pretty.block o Pretty.breaks) [
haftmann@19167
   518
                  str "val",
haftmann@20191
   519
            ml_from_expr NOBR ve,
haftmann@19167
   520
                  str "=",
haftmann@19167
   521
                  ml_from_expr NOBR se
haftmann@19167
   522
                ],
haftmann@18702
   523
                str ";"
haftmann@19167
   524
              ];
haftmann@18216
   525
          in Pretty.chunks [
haftmann@19167
   526
            [str ("let"), Pretty.fbrk, map mk_val ves |> Pretty.chunks] |> Pretty.block,
haftmann@19167
   527
            [str ("in"), Pretty.fbrk, ml_from_expr NOBR be] |> Pretty.block,
haftmann@18702
   528
            str ("end")
haftmann@18216
   529
          ] end
haftmann@19167
   530
      | ml_from_expr fxy (ICase (((de, dty), bse::bses), _)) =
haftmann@18216
   531
          let
haftmann@19167
   532
            fun mk_clause definer (se, be) =
haftmann@19167
   533
              (Pretty.block o Pretty.breaks) [
haftmann@18702
   534
                str definer,
haftmann@19167
   535
                ml_from_expr NOBR se,
haftmann@19167
   536
                str "=>",
haftmann@19167
   537
                ml_from_expr NOBR be
haftmann@18216
   538
              ]
haftmann@18704
   539
          in brackify fxy (
haftmann@19341
   540
            str "(case"
haftmann@20183
   541
            :: ml_from_expr NOBR de
haftmann@19167
   542
            :: mk_clause "of" bse
haftmann@19167
   543
            :: map (mk_clause "|") bses
haftmann@19341
   544
            @ [str ")"]
haftmann@18216
   545
          ) end
haftmann@18885
   546
      | ml_from_expr _ e =
haftmann@20389
   547
          error ("Dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iterm) e)
haftmann@18885
   548
    and ml_mk_app f es =
haftmann@19136
   549
      if is_cons f andalso length es > 1 then
haftmann@19038
   550
        [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
haftmann@18702
   551
      else
haftmann@18885
   552
        (str o resolv) f :: map (ml_from_expr BR) es
haftmann@19607
   553
    and ml_from_app fxy (app_expr as ((c, (lss, ty)), es)) =
haftmann@18885
   554
      case map (ml_from_sortlookup BR) lss
haftmann@18885
   555
       of [] =>
haftmann@19607
   556
            from_app ml_mk_app ml_from_expr const_syntax fxy app_expr
haftmann@18885
   557
        | lss =>
haftmann@18885
   558
            brackify fxy (
haftmann@18885
   559
              (str o resolv) c
haftmann@18885
   560
              :: (lss
haftmann@18885
   561
              @ map (ml_from_expr BR) es)
haftmann@18885
   562
            );
haftmann@20183
   563
  in (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) end;
haftmann@19042
   564
haftmann@20183
   565
fun ml_fun_datatyp is_cons (tyco_syntax, const_syntax) resolv =
haftmann@19042
   566
  let
haftmann@20183
   567
    val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
haftmann@20183
   568
      ml_expr_seri is_cons (tyco_syntax, const_syntax) resolv;
haftmann@19042
   569
    fun chunk_defs ps =
haftmann@19042
   570
      let
haftmann@19042
   571
        val (p_init, p_last) = split_last ps
haftmann@19042
   572
      in
haftmann@19042
   573
        Pretty.chunks (p_init @ [Pretty.block ([p_last, str ";"])])
haftmann@19042
   574
      end;
haftmann@19607
   575
    fun eta_expand_poly_fun (funn as (_, (_::_, _))) =
haftmann@19607
   576
          funn
haftmann@19607
   577
      | eta_expand_poly_fun (funn as (eqs, sctxt_ty as (_, ty))) =
haftmann@19607
   578
          let
haftmann@19607
   579
            fun no_eta (_::_, _) = I
haftmann@19607
   580
              | no_eta (_, _ `|-> _) = I
haftmann@19607
   581
              | no_eta ([], e) = K false;
haftmann@19607
   582
            fun has_tyvars (_ `%% tys) =
haftmann@19607
   583
                  exists has_tyvars tys
haftmann@19607
   584
              | has_tyvars (ITyVar _) =
haftmann@19607
   585
                  true
haftmann@19607
   586
              | has_tyvars (ty1 `-> ty2) =
haftmann@19607
   587
                  has_tyvars ty1 orelse has_tyvars ty2;
haftmann@19622
   588
          in if (null o fst o CodegenThingol.unfold_fun) ty
haftmann@19622
   589
              orelse (not o has_tyvars) ty
haftmann@19622
   590
              orelse fold no_eta eqs true
haftmann@19607
   591
            then funn
haftmann@19607
   592
            else (map (fn ([], rhs) => ([IVar "x"], rhs `$ IVar "x")) eqs, sctxt_ty)
haftmann@19607
   593
          end;
haftmann@18912
   594
    fun ml_from_funs (defs as def::defs_tl) =
haftmann@18216
   595
      let
haftmann@19213
   596
        fun mk_definer [] [] = "val"
haftmann@19213
   597
          | mk_definer _ _ = "fun";
haftmann@19213
   598
        fun check_args (_, ((pats, _)::_, (sortctxt, _))) NONE =
haftmann@19213
   599
              SOME (mk_definer pats sortctxt)
haftmann@19213
   600
          | check_args (_, ((pats, _)::_, (sortctxt, _))) (SOME definer) =
haftmann@19213
   601
              if mk_definer pats sortctxt = definer
haftmann@18216
   602
              then SOME definer
haftmann@20389
   603
              else error ("Mixing simultaneous vals and funs not implemented");
haftmann@19042
   604
        fun mk_fun definer (name, (eqs as eq::eq_tl, (sortctxt, ty))) =
haftmann@18216
   605
          let
haftmann@19136
   606
            val shift = if null eq_tl then I else
haftmann@19136
   607
              map (Pretty.block o single o Pretty.block o single);
haftmann@19167
   608
            fun mk_arg e ty =
haftmann@19167
   609
              ml_from_expr BR e
haftmann@18912
   610
            fun mk_eq definer (pats, expr) =
haftmann@18912
   611
              (Pretty.block o Pretty.breaks) (
haftmann@18912
   612
                [str definer, (str o resolv) name]
haftmann@19213
   613
                @ (if null pats andalso null sortctxt
haftmann@18912
   614
                   then [str ":", ml_from_type NOBR ty]
haftmann@19167
   615
                   else
haftmann@19213
   616
                     map ml_from_tyvar sortctxt
haftmann@19167
   617
                     @ map2 mk_arg pats
haftmann@19167
   618
                         ((curry Library.take (length pats) o fst o CodegenThingol.unfold_fun) ty))
haftmann@20191
   619
             @ [str "=", ml_from_expr NOBR expr]
haftmann@18912
   620
              )
haftmann@18216
   621
          in
haftmann@18912
   622
            (Pretty.block o Pretty.fbreaks o shift) (
haftmann@18912
   623
              mk_eq definer eq
haftmann@18912
   624
              :: map (mk_eq "|") eq_tl
haftmann@18912
   625
            )
haftmann@18380
   626
          end;
haftmann@19953
   627
        val def' :: defs' = map (apsnd eta_expand_poly_fun o constructive_fun is_cons) defs
haftmann@18216
   628
      in
haftmann@18216
   629
        chunk_defs (
haftmann@19607
   630
          (mk_fun (the (fold check_args defs NONE))) def'
haftmann@19607
   631
          :: map (mk_fun "and") defs'
haftmann@19042
   632
        )
haftmann@18216
   633
      end;
haftmann@19042
   634
    fun ml_from_datatypes (defs as (def::defs_tl)) =
haftmann@18216
   635
      let
haftmann@18702
   636
        fun mk_cons (co, []) =
haftmann@18702
   637
              str (resolv co)
haftmann@18702
   638
          | mk_cons (co, tys) =
haftmann@19136
   639
              Pretty.block [
haftmann@19136
   640
                str (resolv co),
haftmann@19136
   641
                str " of",
haftmann@19136
   642
                Pretty.brk 1,
haftmann@19136
   643
                Pretty.enum " *" "" "" (map (ml_from_type NOBR) tys)
haftmann@19136
   644
              ]
haftmann@19038
   645
        fun mk_datatype definer (t, (vs, cs)) =
haftmann@18912
   646
          (Pretty.block o Pretty.breaks) (
haftmann@18702
   647
            str definer
haftmann@19167
   648
            :: ml_from_tycoexpr NOBR (t, map (ITyVar o fst) vs)
haftmann@18912
   649
            :: str "="
haftmann@18912
   650
            :: separate (str "|") (map mk_cons cs)
haftmann@18380
   651
          )
haftmann@18380
   652
      in
haftmann@19042
   653
        chunk_defs (
haftmann@19042
   654
          mk_datatype "datatype" def
haftmann@19042
   655
          :: map (mk_datatype "and") defs_tl
haftmann@19042
   656
        )
haftmann@19042
   657
      end;
haftmann@19042
   658
  in (ml_from_funs, ml_from_datatypes) end;
haftmann@19042
   659
haftmann@20183
   660
fun ml_from_defs is_cons
haftmann@19816
   661
    (_, tyco_syntax, const_syntax) resolver prefix defs =
haftmann@19042
   662
  let
haftmann@19042
   663
    val resolv = resolver prefix;
haftmann@20183
   664
    val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
haftmann@20183
   665
      ml_expr_seri is_cons (tyco_syntax, const_syntax) resolv;
haftmann@19042
   666
    val (ml_from_funs, ml_from_datatypes) =
haftmann@20183
   667
      ml_fun_datatyp is_cons (tyco_syntax, const_syntax) resolv;
haftmann@19042
   668
    val filter_datatype =
wenzelm@19482
   669
      map_filter
haftmann@19167
   670
        (fn (name, CodegenThingol.Datatype info) => SOME (name, info)
haftmann@19167
   671
          | (name, CodegenThingol.Datatypecons _) => NONE
haftmann@20389
   672
          | (name, def) => error ("Datatype block containing illegal def: "
haftmann@19167
   673
                ^ (Pretty.output o CodegenThingol.pretty_def) def));
haftmann@20191
   674
    fun filter_class defs =
wenzelm@19482
   675
      case map_filter
haftmann@19167
   676
        (fn (name, CodegenThingol.Class info) => SOME (name, info)
haftmann@19167
   677
          | (name, CodegenThingol.Classmember _) => NONE
haftmann@20389
   678
          | (name, def) => error ("Class block containing illegal def: "
haftmann@19167
   679
                ^ (Pretty.output o CodegenThingol.pretty_def) def)) defs
haftmann@19136
   680
       of [class] => class
haftmann@20389
   681
        | _ => error ("Class block without class: " ^ (commas o map (quote o fst)) defs)
haftmann@19136
   682
    fun ml_from_class (name, (supclasses, (v, membrs))) =
haftmann@19136
   683
      let
haftmann@20428
   684
        val w = ml_from_dictvar v;
haftmann@19136
   685
        fun from_supclass class =
haftmann@19136
   686
          Pretty.block [
haftmann@19136
   687
            ml_from_label class,
haftmann@19136
   688
            str ":",
haftmann@19136
   689
            Pretty.brk 1,
haftmann@19136
   690
            str ("'" ^ v),
haftmann@19136
   691
            Pretty.brk 1,
haftmann@19136
   692
            (str o resolv) class
haftmann@19136
   693
          ];
haftmann@19136
   694
        fun from_membr (m, (_, ty)) =
haftmann@19136
   695
          Pretty.block [
haftmann@19136
   696
            ml_from_label m,
haftmann@19136
   697
            str ":",
haftmann@19136
   698
            Pretty.brk 1,
haftmann@19136
   699
            ml_from_type NOBR ty
haftmann@19136
   700
          ];
haftmann@19136
   701
        fun from_membr_fun (m, _) =
haftmann@19136
   702
          (Pretty.block o Pretty.breaks) [
haftmann@19136
   703
            str "fun",
haftmann@20191
   704
            (str o resolv) m,
haftmann@19953
   705
            Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ resolv name)],
haftmann@19136
   706
            str "=",
haftmann@19136
   707
            Pretty.block [str "#", ml_from_label m],
haftmann@19953
   708
            str (w ^ ";")
haftmann@19136
   709
          ];
haftmann@19136
   710
      in
haftmann@19136
   711
        Pretty.chunks (
haftmann@19136
   712
          (Pretty.block o Pretty.breaks) [
haftmann@19136
   713
            str "type",
haftmann@19136
   714
            str ("'" ^ v),
haftmann@19136
   715
            (str o resolv) name,
haftmann@19136
   716
            str "=",
haftmann@19136
   717
            Pretty.enum "," "{" "};" (
haftmann@19136
   718
              map from_supclass supclasses @ map from_membr membrs
haftmann@19136
   719
            )
haftmann@19136
   720
          ]
haftmann@19136
   721
        :: map from_membr_fun membrs)
haftmann@19136
   722
      end
haftmann@19816
   723
    fun ml_from_def (name, CodegenThingol.Typesyn (vs, ty)) =
haftmann@18865
   724
        (map (fn (vname, []) => () | _ =>
haftmann@20389
   725
            error "Can't serialize sort constrained type declaration to ML") vs;
haftmann@18702
   726
          Pretty.block [
haftmann@18702
   727
            str "type ",
haftmann@19167
   728
            ml_from_tycoexpr NOBR (name, map (ITyVar o fst) vs),
haftmann@18702
   729
            str " =",
haftmann@18380
   730
            Pretty.brk 1,
haftmann@18380
   731
            ml_from_type NOBR ty,
haftmann@18702
   732
            str ";"
haftmann@18380
   733
            ]
haftmann@20191
   734
       ) |> SOME
haftmann@20389
   735
      | ml_from_def (name, CodegenThingol.Classinst ((class, (tyco, arity)), (suparities, memdefs))) =
haftmann@18865
   736
          let
haftmann@18865
   737
            val definer = if null arity then "val" else "fun"
haftmann@19953
   738
            fun from_supclass (supclass, ls) =
haftmann@19953
   739
              (Pretty.block o Pretty.breaks) [
haftmann@19953
   740
                ml_from_label supclass,
haftmann@19953
   741
                str "=",
haftmann@19953
   742
                ml_from_sortlookup NOBR ls
haftmann@19953
   743
              ];
haftmann@20389
   744
            fun from_memdef (m, e) =
haftmann@20389
   745
              (Pretty.block o Pretty.breaks) [
haftmann@20389
   746
                ml_from_label m,
haftmann@20389
   747
                str "=",
haftmann@20389
   748
                ml_from_expr NOBR e
haftmann@20389
   749
              ];
haftmann@19253
   750
            fun mk_corp rhs =
haftmann@19253
   751
              (Pretty.block o Pretty.breaks) (
haftmann@19253
   752
                str definer
haftmann@19253
   753
                :: (str o resolv) name
haftmann@19253
   754
                :: map ml_from_tyvar arity
haftmann@19253
   755
                @ [str "=", rhs]
haftmann@19253
   756
              );
haftmann@20389
   757
            fun mk_memdefs supclassexprs memdefs =
haftmann@20389
   758
              (mk_corp o Pretty.block o Pretty.breaks) [
haftmann@20389
   759
                Pretty.enum "," "{" "}" (supclassexprs @ memdefs),
haftmann@20389
   760
                str ":",
haftmann@20389
   761
                ml_from_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
haftmann@20389
   762
              ];
haftmann@18865
   763
          in
haftmann@20389
   764
            mk_memdefs (map from_supclass suparities) (map from_memdef memdefs) |> SOME
haftmann@19213
   765
          end
haftmann@20389
   766
      | ml_from_def (name, def) = error ("Illegal definition for " ^ quote name ^ ": " ^
haftmann@20353
   767
          (Pretty.output o CodegenThingol.pretty_def) def);
haftmann@18850
   768
  in case defs
haftmann@20353
   769
   of (_, CodegenThingol.Fun _)::_ => ((*writeln "FUN";*) (SOME o ml_from_funs o map (fn (name, CodegenThingol.Fun info) => (name, info))) defs)
haftmann@20353
   770
    | (_, CodegenThingol.Datatypecons _)::_ => ((*writeln "DTCO";*) (SOME o ml_from_datatypes o filter_datatype) defs)
haftmann@20353
   771
    | (_, CodegenThingol.Datatype _)::_ => ((*writeln "DT";*) (SOME o ml_from_datatypes o filter_datatype) defs)
haftmann@19167
   772
    | (_, CodegenThingol.Class _)::_ => (SOME o ml_from_class o filter_class) defs
haftmann@19167
   773
    | (_, CodegenThingol.Classmember _)::_ => (SOME o ml_from_class o filter_class) defs
haftmann@18850
   774
    | [def] => ml_from_def def
haftmann@20389
   775
    | defs => error ("Illegal mutual dependencies: " ^ (commas o map fst) defs)
haftmann@18216
   776
  end;
haftmann@18216
   777
haftmann@20183
   778
fun ml_annotators nsp_dtcon =
haftmann@19042
   779
  let
haftmann@19167
   780
    fun is_cons c = CodegenThingol.has_nsp c nsp_dtcon;
haftmann@20183
   781
  in is_cons end;
haftmann@19042
   782
haftmann@20191
   783
fun ml_serializer root_name target nsp_dtcon nspgrp =
haftmann@18216
   784
  let
haftmann@19341
   785
    fun ml_from_module resolv _ ((_, name), ps) =
haftmann@18756
   786
      Pretty.chunks ([
haftmann@18702
   787
        str ("structure " ^ name ^ " = "),
haftmann@18702
   788
        str "struct",
haftmann@18702
   789
        str ""
haftmann@18702
   790
      ] @ separate (str "") ps @ [
haftmann@18702
   791
        str "",
haftmann@18702
   792
        str ("end; (* struct " ^ name ^ " *)")
haftmann@18756
   793
      ]);
haftmann@20183
   794
    val is_cons = ml_annotators nsp_dtcon;
haftmann@20401
   795
    fun postproc (shallow, n) =
haftmann@20401
   796
      let
haftmann@20401
   797
        fun ch_first f = String.implode o nth_map 0 f o String.explode;
haftmann@20401
   798
      in if shallow = nsp_dtcon
haftmann@20401
   799
        then ch_first Char.toUpper n
haftmann@20401
   800
        else n
haftmann@20401
   801
      end;
haftmann@20191
   802
  in abstract_serializer (target, nspgrp)
haftmann@20191
   803
    root_name (ml_from_defs is_cons, ml_from_module,
haftmann@20401
   804
     abstract_validator reserved_ml, postproc) end;
haftmann@20191
   805
haftmann@20191
   806
in
haftmann@20191
   807
haftmann@20191
   808
fun ml_from_thingol target nsp_dtcon nspgrp =
haftmann@20191
   809
  let
haftmann@20191
   810
    val serializer = ml_serializer "ROOT" target nsp_dtcon nspgrp
haftmann@18850
   811
    val parse_multi =
haftmann@18850
   812
      OuterParse.name
haftmann@20191
   813
      #-> (fn "dir" =>
haftmann@18850
   814
               parse_multi_file
haftmann@18850
   815
                 (K o SOME o str o suffix ";" o prefix "val _ = use "
haftmann@18850
   816
                  o quote o suffix ".ML" o translate_string (fn "." => "/" | s => s)) "ML" serializer
haftmann@18850
   817
            | _ => Scan.fail ());
haftmann@18282
   818
  in
haftmann@19884
   819
    parse_multi
haftmann@19884
   820
    || parse_internal serializer
haftmann@20105
   821
    || parse_stdout serializer
haftmann@19884
   822
    || parse_single_file serializer
haftmann@18216
   823
  end;
haftmann@18216
   824
haftmann@20389
   825
val eval_verbose = ref false;
haftmann@20389
   826
haftmann@20216
   827
fun eval_term nsp_eval nsp_dtcon nspgrp (syntax_tyco, syntax_const) hidden ((ref_name, reff), e) modl =
haftmann@20191
   828
  let
haftmann@20216
   829
    val (val_name, modl') = CodegenThingol.add_eval_def (nsp_eval, e) modl;
haftmann@20191
   830
    val struct_name = "EVAL";
haftmann@20401
   831
    fun output p = if !eval_verbose then (Pretty.writeln p; Pretty.output p)
haftmann@20401
   832
      else Pretty.output p;
haftmann@20191
   833
    val serializer = ml_serializer struct_name "ml" nsp_dtcon nspgrp
haftmann@20401
   834
      (fn "" => (fn p => (use_text Context.ml_output (!eval_verbose) (output p); NONE))
haftmann@20216
   835
        | _ => SOME) (K NONE, syntax_tyco, syntax_const) (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]);
haftmann@20191
   836
    val _ = serializer modl';
haftmann@20191
   837
    val val_name_struct = NameSpace.append struct_name val_name;
haftmann@20389
   838
    val _ = use_text Context.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ "())");
haftmann@20191
   839
    val value = ! reff;
haftmann@20191
   840
  in value end;
haftmann@20191
   841
haftmann@19150
   842
fun mk_flat_ml_resolver names =
haftmann@19150
   843
  let
haftmann@19150
   844
    val mangler =
haftmann@19150
   845
      NameMangler.empty
haftmann@19150
   846
      |> fold_map (NameMangler.declare reserved_ml) names
haftmann@19150
   847
      |-> (fn _ => I)
haftmann@19150
   848
  in NameMangler.get reserved_ml mangler end;
haftmann@19150
   849
haftmann@20183
   850
fun ml_fun_datatype nsp_dtcon =
haftmann@20183
   851
  ml_fun_datatyp (ml_annotators nsp_dtcon);
haftmann@19042
   852
haftmann@18216
   853
end; (* local *)
haftmann@18216
   854
haftmann@20191
   855
haftmann@20191
   856
(** haskell serializer **)
haftmann@20191
   857
haftmann@18282
   858
local
haftmann@18282
   859
haftmann@19953
   860
fun hs_from_defs (is_cons, with_typs) (class_syntax, tyco_syntax, const_syntax)
haftmann@19038
   861
    resolver prefix defs =
haftmann@18282
   862
  let
haftmann@19341
   863
    val resolv = resolver "";
haftmann@19341
   864
    val resolv_here = resolver prefix;
haftmann@20428
   865
    fun hs_from_class cls = case class_syntax cls
haftmann@20428
   866
     of NONE => resolv cls
haftmann@20428
   867
      | SOME (cls, _) => cls;
haftmann@20428
   868
    fun hs_from_classop_name cls clsop = case class_syntax cls
haftmann@20428
   869
     of NONE => NameSpace.base clsop
haftmann@20428
   870
      | SOME (_, classop_syntax) => case classop_syntax clsop
haftmann@20428
   871
         of NONE => NameSpace.base clsop
haftmann@20428
   872
          | SOME clsop => clsop;
haftmann@18704
   873
    fun hs_from_sctxt vs =
haftmann@18282
   874
      let
haftmann@18702
   875
        fun from_sctxt [] = str ""
haftmann@18282
   876
          | from_sctxt vs =
haftmann@18282
   877
              vs
haftmann@20428
   878
              |> map (fn (v, cls) => str (hs_from_class cls ^ " " ^ v))
wenzelm@18812
   879
              |> Pretty.enum "," "(" ")"
haftmann@18702
   880
              |> (fn p => Pretty.block [p, str " => "])
haftmann@20191
   881
      in
haftmann@18282
   882
        vs
haftmann@18282
   883
        |> map (fn (v, sort) => map (pair v) sort)
wenzelm@19466
   884
        |> flat
haftmann@18282
   885
        |> from_sctxt
haftmann@18282
   886
      end;
haftmann@18963
   887
    fun hs_from_tycoexpr fxy (tyco, tys) =
haftmann@19341
   888
      brackify fxy (str tyco :: map (hs_from_type BR) tys)
haftmann@19167
   889
    and hs_from_type fxy (tycoexpr as tyco `%% tys) =
haftmann@18865
   890
          (case tyco_syntax tyco
haftmann@18335
   891
           of NONE =>
haftmann@19341
   892
                hs_from_tycoexpr fxy (resolv tyco, tys)
haftmann@18702
   893
            | SOME ((i, k), pr) =>
haftmann@18865
   894
                if not (i <= length tys andalso length tys <= k)
haftmann@20389
   895
                then error ("Number of argument mismatch in customary serialization: "
haftmann@18865
   896
                  ^ (string_of_int o length) tys ^ " given, "
haftmann@18865
   897
                  ^ string_of_int i ^ " to " ^ string_of_int k
haftmann@18702
   898
                  ^ " expected")
haftmann@18865
   899
                else pr fxy hs_from_type tys)
haftmann@19167
   900
      | hs_from_type fxy (t1 `-> t2) =
haftmann@18865
   901
          brackify_infix (1, R) fxy [
haftmann@18865
   902
            hs_from_type (INFX (1, X)) t1,
haftmann@18865
   903
            str "->",
haftmann@18865
   904
            hs_from_type (INFX (1, R)) t2
haftmann@18865
   905
          ]
haftmann@19167
   906
      | hs_from_type fxy (ITyVar v) =
haftmann@18919
   907
          str v;
haftmann@18963
   908
    fun hs_from_sctxt_tycoexpr (sctxt, tycoexpr) =
haftmann@18963
   909
      Pretty.block [hs_from_sctxt sctxt, hs_from_tycoexpr NOBR tycoexpr]
haftmann@18865
   910
    fun hs_from_sctxt_type (sctxt, ty) =
haftmann@18865
   911
      Pretty.block [hs_from_sctxt sctxt, hs_from_type NOBR ty]
haftmann@19167
   912
    fun hs_from_expr fxy (e as IConst x) =
haftmann@19167
   913
          hs_from_app fxy (x, [])
haftmann@19167
   914
      | hs_from_expr fxy (e as (e1 `$ e2)) =
haftmann@19167
   915
          (case CodegenThingol.unfold_const_app e
haftmann@18865
   916
           of SOME x => hs_from_app fxy x
haftmann@18282
   917
            | _ =>
haftmann@18704
   918
                brackify fxy [
haftmann@18704
   919
                  hs_from_expr NOBR e1,
haftmann@18704
   920
                  hs_from_expr BR e2
haftmann@18282
   921
                ])
haftmann@19167
   922
      | hs_from_expr fxy (IVar v) =
haftmann@20175
   923
          str v
haftmann@19167
   924
      | hs_from_expr fxy (e as _ `|-> _) =
haftmann@18282
   925
          let
haftmann@19167
   926
            val (es, e) = CodegenThingol.unfold_abs e
haftmann@18282
   927
          in
haftmann@19038
   928
            brackify BR (
haftmann@18702
   929
              str "\\"
haftmann@19167
   930
              :: map (hs_from_expr BR o fst) es @ [
haftmann@18702
   931
              str "->",
haftmann@19038
   932
              hs_from_expr NOBR e
haftmann@18282
   933
            ])
haftmann@18282
   934
          end
haftmann@19607
   935
      | hs_from_expr fxy (INum (n, _)) =
haftmann@19607
   936
          (str o IntInf.toString) n
haftmann@19607
   937
      | hs_from_expr fxy (IChar (c, _)) =
haftmann@19607
   938
          (str o enclose "'" "'")
haftmann@19607
   939
            (let val i = (Char.ord o the o Char.fromString) c
haftmann@20191
   940
              in if i < 32
haftmann@20105
   941
                then Library.prefix "\\" (string_of_int i)
haftmann@19607
   942
                else c
haftmann@19607
   943
              end)
haftmann@19167
   944
      | hs_from_expr fxy (e as ICase ((_, [_]), _)) =
haftmann@19167
   945
          let
haftmann@19167
   946
            val (ps, body) = CodegenThingol.unfold_let e;
haftmann@19167
   947
            fun mk_bind ((p, _), e) = (Pretty.block o Pretty.breaks) [
haftmann@18865
   948
                hs_from_expr BR p,
haftmann@19167
   949
                str "=",
haftmann@18704
   950
                hs_from_expr NOBR e
haftmann@18282
   951
              ];
haftmann@18282
   952
          in Pretty.chunks [
haftmann@18702
   953
            [str ("let"), Pretty.fbrk, map mk_bind ps |> Pretty.chunks] |> Pretty.block,
haftmann@18704
   954
            [str ("in "), hs_from_expr NOBR body] |> Pretty.block
haftmann@18282
   955
          ] end
haftmann@19167
   956
      | hs_from_expr fxy (ICase (((de, _), bses), _)) =
haftmann@18282
   957
          let
haftmann@19167
   958
            fun mk_clause (se, be) =
haftmann@19167
   959
              (Pretty.block o Pretty.breaks) [
haftmann@19167
   960
                hs_from_expr NOBR se,
haftmann@19167
   961
                str "->",
haftmann@19167
   962
                hs_from_expr NOBR be
haftmann@18282
   963
              ]
haftmann@18850
   964
          in Pretty.block [
haftmann@18850
   965
            str "case",
haftmann@18850
   966
            Pretty.brk 1,
haftmann@19167
   967
            hs_from_expr NOBR de,
haftmann@18850
   968
            Pretty.brk 1,
haftmann@18850
   969
            str "of",
haftmann@18850
   970
            Pretty.fbrk,
haftmann@19167
   971
            (Pretty.chunks o map mk_clause) bses
haftmann@18850
   972
          ] end
haftmann@18865
   973
    and hs_mk_app c es =
haftmann@18919
   974
      (str o resolv) c :: map (hs_from_expr BR) es
haftmann@19607
   975
    and hs_from_app fxy =
haftmann@19607
   976
      from_app hs_mk_app hs_from_expr const_syntax fxy
haftmann@19202
   977
    fun hs_from_funeqs (def as (name, _)) =
haftmann@18865
   978
      let
haftmann@19202
   979
        fun from_eq (args, rhs) =
haftmann@18865
   980
          Pretty.block [
haftmann@19038
   981
            (str o resolv_here) name,
haftmann@18865
   982
            Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, hs_from_expr BR p]) args),
haftmann@18865
   983
            Pretty.brk 1,
haftmann@18865
   984
            str ("="),
haftmann@18865
   985
            Pretty.brk 1,
haftmann@18865
   986
            hs_from_expr NOBR rhs
haftmann@18865
   987
          ]
haftmann@19953
   988
      in Pretty.chunks ((map from_eq o fst o snd o constructive_fun is_cons) def) end;
haftmann@19816
   989
    fun hs_from_def (name, CodegenThingol.Fun (def as (_, (sctxt, ty)))) =
haftmann@18963
   990
          let
haftmann@19202
   991
            val body = hs_from_funeqs (name, def);
haftmann@18963
   992
          in if with_typs then
haftmann@18963
   993
            Pretty.chunks [
haftmann@18963
   994
              Pretty.block [
haftmann@19038
   995
                (str o suffix " ::" o resolv_here) name,
haftmann@18963
   996
                Pretty.brk 1,
haftmann@18963
   997
                hs_from_sctxt_type (sctxt, ty)
haftmann@18963
   998
              ],
haftmann@18963
   999
              body
haftmann@18963
  1000
            ] |> SOME
haftmann@18963
  1001
          else SOME body end
haftmann@19167
  1002
      | hs_from_def (name, CodegenThingol.Typesyn (sctxt, ty)) =
haftmann@20401
  1003
          (Pretty.block o Pretty.breaks) [
haftmann@20401
  1004
            str "type",
haftmann@19167
  1005
            hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt)),
haftmann@20401
  1006
            str "=",
haftmann@18865
  1007
            hs_from_sctxt_type ([], ty)
haftmann@18380
  1008
          ] |> SOME
haftmann@20401
  1009
      | hs_from_def (name, CodegenThingol.Datatype (sctxt, [(co, [ty])])) =
haftmann@20386
  1010
          (Pretty.block o Pretty.breaks) [
haftmann@20386
  1011
            str "newtype",
haftmann@20386
  1012
            hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt)),
haftmann@20386
  1013
            str "=",
haftmann@20401
  1014
            (str o resolv_here) co,
haftmann@20401
  1015
            hs_from_type BR ty
haftmann@20386
  1016
          ] |> SOME
haftmann@19167
  1017
      | hs_from_def (name, CodegenThingol.Datatype (sctxt, constrs)) =
haftmann@18380
  1018
          let
haftmann@18380
  1019
            fun mk_cons (co, tys) =
haftmann@18380
  1020
              (Pretty.block o Pretty.breaks) (
haftmann@19038
  1021
                (str o resolv_here) co
haftmann@19597
  1022
                :: map (hs_from_type BR) tys
haftmann@18380
  1023
              )
haftmann@18380
  1024
          in
haftmann@19785
  1025
            (Pretty.block o Pretty.breaks) [
haftmann@19785
  1026
              str "data",
haftmann@19785
  1027
              hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt)),
haftmann@19816
  1028
              str "=",
haftmann@19785
  1029
              Pretty.block (separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs))
haftmann@19785
  1030
            ]
haftmann@18380
  1031
          end |> SOME
haftmann@19167
  1032
      | hs_from_def (_, CodegenThingol.Datatypecons _) =
haftmann@18380
  1033
          NONE
haftmann@19167
  1034
      | hs_from_def (name, CodegenThingol.Class (supclasss, (v, membrs))) =
haftmann@18380
  1035
          let
haftmann@18865
  1036
            fun mk_member (m, (sctxt, ty)) =
haftmann@18380
  1037
              Pretty.block [
haftmann@19038
  1038
                str (resolv_here m ^ " ::"),
haftmann@18380
  1039
                Pretty.brk 1,
haftmann@18865
  1040
                hs_from_sctxt_type (sctxt, ty)
haftmann@18380
  1041
              ]
haftmann@18380
  1042
          in
haftmann@18380
  1043
            Pretty.block [
haftmann@18702
  1044
              str "class ",
haftmann@19213
  1045
              hs_from_sctxt [(v, supclasss)],
haftmann@19038
  1046
              str (resolv_here name ^ " " ^ v),
haftmann@18702
  1047
              str " where",
haftmann@18380
  1048
              Pretty.fbrk,
haftmann@18380
  1049
              Pretty.chunks (map mk_member membrs)
haftmann@18380
  1050
            ] |> SOME
haftmann@18380
  1051
          end
haftmann@19213
  1052
      | hs_from_def (_, CodegenThingol.Classmember _) =
haftmann@18380
  1053
          NONE
haftmann@20389
  1054
      | hs_from_def (_, CodegenThingol.Classinst ((clsname, (tyco, arity)), (_, memdefs))) =
haftmann@18385
  1055
          Pretty.block [
haftmann@18702
  1056
            str "instance ",
haftmann@19213
  1057
            hs_from_sctxt arity,
haftmann@20428
  1058
            str (hs_from_class clsname ^ " "),
haftmann@19213
  1059
            hs_from_type BR (tyco `%% map (ITyVar o fst) arity),
haftmann@18702
  1060
            str " where",
haftmann@18385
  1061
            Pretty.fbrk,
haftmann@20389
  1062
            Pretty.chunks (map (fn (m, e) =>
haftmann@20389
  1063
              (Pretty.block o Pretty.breaks) [
haftmann@20428
  1064
                (str o hs_from_classop_name clsname) m,
haftmann@20389
  1065
                str "=",
haftmann@20389
  1066
                hs_from_expr NOBR e
haftmann@20389
  1067
              ]
haftmann@20389
  1068
            ) memdefs)
haftmann@18380
  1069
          ] |> SOME
haftmann@18380
  1070
  in
wenzelm@19482
  1071
    case map_filter (fn (name, def) => hs_from_def (name, def)) defs
haftmann@18380
  1072
     of [] => NONE
haftmann@18702
  1073
      | l => (SOME o Pretty.chunks o separate (str "")) l
haftmann@18282
  1074
  end;
haftmann@18282
  1075
haftmann@18282
  1076
in
haftmann@18282
  1077
haftmann@19953
  1078
fun hs_from_thingol target (nsp_dtcon, nsps_upper) nspgrp =
haftmann@18282
  1079
  let
haftmann@18704
  1080
    val reserved_hs = [
haftmann@18702
  1081
      "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
haftmann@18702
  1082
      "import", "default", "forall", "let", "in", "class", "qualified", "data",
haftmann@18702
  1083
      "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
haftmann@18702
  1084
    ] @ [
haftmann@20401
  1085
      "Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "not", "negate",
haftmann@20401
  1086
      "String", "Char"
haftmann@18702
  1087
    ];
haftmann@19953
  1088
    fun is_cons c = CodegenThingol.has_nsp c nsp_dtcon;
haftmann@19341
  1089
    fun hs_from_module resolv imps ((_, name), ps) =
haftmann@19038
  1090
      (Pretty.chunks) (
haftmann@19038
  1091
        str ("module " ^ name ^ " where")
haftmann@19038
  1092
        :: map (str o prefix "import qualified ") imps @ (
haftmann@19038
  1093
          str ""
haftmann@19038
  1094
          :: separate (str "") ps
haftmann@19038
  1095
      ));
haftmann@18919
  1096
    fun postproc (shallow, n) =
haftmann@18919
  1097
      let
haftmann@18919
  1098
        fun ch_first f = String.implode o nth_map 0 f o String.explode;
haftmann@18919
  1099
      in if member (op =) nsps_upper shallow
haftmann@18919
  1100
        then ch_first Char.toUpper n
haftmann@18919
  1101
        else ch_first Char.toLower n
haftmann@18919
  1102
      end;
haftmann@18963
  1103
    fun serializer with_typs = abstract_serializer (target, nspgrp)
haftmann@19953
  1104
      "Main" (hs_from_defs (is_cons, with_typs), hs_from_module, abstract_validator reserved_hs, postproc);
haftmann@18282
  1105
  in
haftmann@18963
  1106
    (Scan.optional (OuterParse.name >> (fn "no_typs" => false | s => Scan.fail_with (fn _ => "illegal flag: " ^ quote s) true)) true
haftmann@18963
  1107
    #-> (fn with_typs => parse_multi_file ((K o K) NONE) "hs" (serializer with_typs)))
haftmann@18282
  1108
  end;
haftmann@18282
  1109
haftmann@18282
  1110
end; (* local *)
haftmann@18282
  1111
haftmann@18702
  1112
haftmann@18702
  1113
(** lookup record **)
haftmann@18702
  1114
haftmann@18702
  1115
val serializers =
haftmann@18702
  1116
  let
haftmann@18702
  1117
    fun seri s f = (s, f s);
haftmann@18702
  1118
  in {
haftmann@18702
  1119
    ml = seri "ml" ml_from_thingol,
haftmann@18704
  1120
    haskell = seri "haskell" hs_from_thingol
haftmann@18702
  1121
  } end;
haftmann@18702
  1122
haftmann@18216
  1123
end; (* struct *)