src/Tools/Code/code_ml.ML
author haftmann
Thu Mar 14 13:54:31 2019 +0000 (3 months ago)
changeset 69910 0c0f7b4a72bf
parent 69906 55534affe445
child 69926 110fff287217
permissions -rw-r--r--
dedicated environment setting for ocaml environment: ISABELLE_OPAM_ROOT is always present even if no envionrment is available
     1 (*  Title:      Tools/Code/code_ml.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Serializer for SML and OCaml.
     5 *)
     6 
     7 signature CODE_ML =
     8 sig
     9   val target_SML: string
    10   val target_OCaml: string
    11 end;
    12 
    13 structure Code_ML : CODE_ML =
    14 struct
    15 
    16 open Basic_Code_Symbol;
    17 open Basic_Code_Thingol;
    18 open Code_Printer;
    19 
    20 infixr 5 @@;
    21 infixr 5 @|;
    22 
    23 
    24 (** generic **)
    25 
    26 val target_SML = "SML";
    27 val target_OCaml = "OCaml";
    28 
    29 datatype ml_binding =
    30     ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
    31   | ML_Instance of (string * class) * { class: class, tyco: string, vs: (vname * sort) list,
    32         superinsts: (class * dict list list) list,
    33         inst_params: ((string * (const * int)) * (thm * bool)) list,
    34         superinst_params: ((string * (const * int)) * (thm * bool)) list };
    35 
    36 datatype ml_stmt =
    37     ML_Exc of string * (typscheme * int)
    38   | ML_Val of ml_binding
    39   | ML_Funs of (Code_Namespace.export * ml_binding) list * Code_Symbol.T list
    40   | ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list
    41   | ML_Class of string * (vname * ((class * class) list * (string * itype) list));
    42 
    43 fun print_product _ [] = NONE
    44   | print_product print [x] = SOME (print x)
    45   | print_product print xs = (SOME o enum " *" "" "") (map print xs);
    46 
    47 fun tuplify _ _ [] = NONE
    48   | tuplify print fxy [x] = SOME (print fxy x)
    49   | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
    50 
    51 
    52 (** SML serializer **)
    53 
    54 fun print_sml_char c =
    55   if c = "\\"
    56   then "\\092" (*produce strings suitable for both SML as well as Isabelle/ML*)
    57   else if Symbol.is_ascii c
    58   then ML_Syntax.print_symbol_char c
    59   else error "non-ASCII byte in SML string literal";
    60 
    61 val print_sml_string = quote o translate_string print_sml_char;
    62 
    63 fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
    64   let
    65     val deresolve_const = deresolve o Constant;
    66     val deresolve_classrel = deresolve o Class_Relation;
    67     val deresolve_inst = deresolve o Class_Instance;
    68     fun print_tyco_expr (sym, []) = (str o deresolve) sym
    69       | print_tyco_expr (sym, [ty]) =
    70           concat [print_typ BR ty, (str o deresolve) sym]
    71       | print_tyco_expr (sym, tys) =
    72           concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
    73     and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
    74          of NONE => print_tyco_expr (Type_Constructor tyco, tys)
    75           | SOME (_, print) => print print_typ fxy tys)
    76       | print_typ fxy (ITyVar v) = str ("'" ^ v);
    77     fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
    78     fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
    79       (map_filter (fn (v, sort) =>
    80         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
    81     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
    82     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
    83     fun print_classrels fxy [] ps = brackify fxy ps
    84       | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve_classrel) classrel, brackify BR ps]
    85       | print_classrels fxy classrels ps =
    86           brackify fxy [enum " o" "(" ")" (map (str o deresolve_classrel) classrels), brackify BR ps]
    87     fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
    88       print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)
    89     and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
    90           ((str o deresolve_inst) inst ::
    91             (if is_pseudo_fun (Class_Instance inst) then [str "()"]
    92             else map_filter (print_dicts is_pseudo_fun BR) dss))
    93       | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) =
    94           [str (if length = 1 then Name.enforce_case true var ^ "_"
    95             else Name.enforce_case true var ^ string_of_int (index + 1) ^ "_")]
    96     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    97     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    98       (map_index (fn (i, _) => Dict ([],
    99          Dict_Var { var = v, index = i, length = length sort, class = nth sort i, unique = true })) sort));
   100     fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
   101           print_app is_pseudo_fun some_thm vars fxy (const, [])
   102       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
   103           str "_"
   104       | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
   105           str (lookup_var vars v)
   106       | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
   107           (case Code_Thingol.unfold_const_app t
   108            of SOME app => print_app is_pseudo_fun some_thm vars fxy app
   109             | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
   110                 print_term is_pseudo_fun some_thm vars BR t2])
   111       | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
   112           let
   113             val (binds, t') = Code_Thingol.unfold_pat_abs t;
   114             fun print_abs (pat, ty) =
   115               print_bind is_pseudo_fun some_thm NOBR pat
   116               #>> (fn p => concat [str "fn", p, str "=>"]);
   117             val (ps, vars') = fold_map print_abs binds vars;
   118           in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
   119       | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
   120           (case Code_Thingol.unfold_const_app (#primitive case_expr)
   121            of SOME (app as ({ sym = Constant const, ... }, _)) =>
   122                 if is_none (const_syntax const)
   123                 then print_case is_pseudo_fun some_thm vars fxy case_expr
   124                 else print_app is_pseudo_fun some_thm vars fxy app
   125             | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
   126     and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
   127       if is_constr sym then
   128         let val k = length dom in
   129           if k < 2 orelse length ts = k
   130           then (str o deresolve) sym
   131             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
   132           else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
   133         end
   134       else if is_pseudo_fun sym
   135         then (str o deresolve) sym @@ str "()"
   136       else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
   137         @ map (print_term is_pseudo_fun some_thm vars BR) ts
   138     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   139       (print_term is_pseudo_fun) const_syntax some_thm vars
   140     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
   141     and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
   142           (concat o map str) ["raise", "Fail", "\"empty case\""]
   143       | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
   144           let
   145             val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
   146             fun print_match ((pat, _), t) vars =
   147               vars
   148               |> print_bind is_pseudo_fun some_thm NOBR pat
   149               |>> (fn p => semicolon [str "val", p, str "=",
   150                     print_term is_pseudo_fun some_thm vars NOBR t])
   151             val (ps, vars') = fold_map print_match binds vars;
   152           in
   153             Pretty.chunks [
   154               Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps],
   155               Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body],
   156               str "end"
   157             ]
   158           end
   159       | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
   160           let
   161             fun print_select delim (pat, body) =
   162               let
   163                 val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
   164               in
   165                 concat [str delim, p, str "=>", print_term is_pseudo_fun some_thm vars' NOBR body]
   166               end;
   167           in
   168             brackets (
   169               str "case"
   170               :: print_term is_pseudo_fun some_thm vars NOBR t
   171               :: print_select "of" clause
   172               :: map (print_select "|") clauses
   173             )
   174           end;
   175     fun print_val_decl print_typscheme (sym, typscheme) = concat
   176       [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
   177     fun print_datatype_decl definer (tyco, (vs, cos)) =
   178       let
   179         fun print_co ((co, _), []) = str (deresolve_const co)
   180           | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
   181               enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
   182       in
   183         concat (
   184           str definer
   185           :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
   186           :: str "="
   187           :: separate (str "|") (map print_co cos)
   188         )
   189       end;
   190     fun print_def is_pseudo_fun needs_typ definer
   191           (ML_Function (const, (vs_ty as (vs, ty), eq :: eqs))) =
   192           let
   193             fun print_eqn definer ((ts, t), (some_thm, _)) =
   194               let
   195                 val vars = reserved
   196                   |> intro_base_names_for (is_none o const_syntax)
   197                        deresolve (t :: ts)
   198                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
   199                        (insert (op =)) ts []);
   200                 val prolog = if needs_typ then
   201                   concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
   202                     else (concat o map str) [definer, deresolve_const const];
   203               in
   204                 concat (
   205                   prolog
   206                   :: (if is_pseudo_fun (Constant const) then [str "()"]
   207                       else print_dict_args vs
   208                         @ map (print_term is_pseudo_fun some_thm vars BR) ts)
   209                   @ str "="
   210                   @@ print_term is_pseudo_fun some_thm vars NOBR t
   211                 )
   212               end
   213             val shift = if null eqs then I else
   214               map (Pretty.block o single o Pretty.block o single);
   215           in pair
   216             (print_val_decl print_typscheme (Constant const, vs_ty))
   217             ((Pretty.block o Pretty.fbreaks o shift) (
   218               print_eqn definer eq
   219               :: map (print_eqn "|") eqs
   220             ))
   221           end
   222       | print_def is_pseudo_fun _ definer
   223           (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) =
   224           let
   225             fun print_super_instance (super_class, x) =
   226               concat [
   227                 (str o Long_Name.base_name o deresolve_classrel) (class, super_class),
   228                 str "=",
   229                 print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
   230               ];
   231             fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
   232               concat [
   233                 (str o Long_Name.base_name o deresolve_const) classparam,
   234                 str "=",
   235                 print_app (K false) (SOME thm) reserved NOBR (const, [])
   236               ];
   237           in pair
   238             (print_val_decl print_dicttypscheme
   239               (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   240             (concat (
   241               str definer
   242               :: (str o deresolve_inst) inst
   243               :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
   244                   else print_dict_args vs)
   245               @ str "="
   246               :: enum "," "{" "}"
   247                 (map print_super_instance superinsts
   248                   @ map print_classparam_instance inst_params)
   249               :: str ":"
   250               @@ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
   251             ))
   252           end;
   253     fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair
   254           [print_val_decl print_typscheme (Constant const, vs_ty)]
   255           ((semicolon o map str) (
   256             (if n = 0 then "val" else "fun")
   257             :: deresolve_const const
   258             :: replicate n "_"
   259             @ "="
   260             :: "raise"
   261             :: "Fail"
   262             @@ print_sml_string const
   263           ))
   264       | print_stmt _ (ML_Val binding) =
   265           let
   266             val (sig_p, p) = print_def (K false) true "val" binding
   267           in pair
   268             [sig_p]
   269             (semicolon [p])
   270           end
   271       | print_stmt _ (ML_Funs ((export, binding) :: exports_bindings, pseudo_funs)) =
   272           let
   273             val print_def' = print_def (member (op =) pseudo_funs) false;
   274             fun print_pseudo_fun sym = concat [
   275                 str "val",
   276                 (str o deresolve) sym,
   277                 str "=",
   278                 (str o deresolve) sym,
   279                 str "();"
   280               ];
   281             val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
   282               (print_def' "fun" binding :: map (print_def' "and" o snd) exports_bindings);
   283             val pseudo_ps = map print_pseudo_fun pseudo_funs;
   284           in pair
   285             (map_filter (fn (export, p) => if Code_Namespace.not_private export then SOME p else NONE)
   286               ((export :: map fst exports_bindings) ~~ sig_ps))
   287             (Pretty.chunks (ps @ semicolon [p] :: pseudo_ps))
   288           end
   289      | print_stmt _ (ML_Datas [(tyco, (vs, []))]) =
   290           let
   291             val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
   292           in
   293             pair
   294             [concat [str "type", ty_p]]
   295             (semicolon [str "datatype", ty_p, str "=", str "EMPTY__"])
   296           end
   297      | print_stmt export (ML_Datas (data :: datas)) = 
   298           let
   299             val decl_ps = print_datatype_decl "datatype" data
   300               :: map (print_datatype_decl "and") datas;
   301             val (ps, p) = split_last decl_ps;
   302           in pair
   303             (if Code_Namespace.is_public export
   304               then decl_ps
   305               else map (fn (tyco, (vs, _)) =>
   306                 concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
   307                 (data :: datas))
   308             (Pretty.chunks (ps @| semicolon [p]))
   309           end
   310      | print_stmt export (ML_Class (class, (v, (classrels, classparams)))) =
   311           let
   312             fun print_field s p = concat [str s, str ":", p];
   313             fun print_proj s p = semicolon
   314               (map str ["val", s, "=", "#" ^ s, ":"] @| p);
   315             fun print_super_class_decl (classrel as (_, super_class)) =
   316               print_val_decl print_dicttypscheme
   317                 (Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
   318             fun print_super_class_field (classrel as (_, super_class)) =
   319               print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
   320             fun print_super_class_proj (classrel as (_, super_class)) =
   321               print_proj (deresolve_classrel classrel)
   322                 (print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
   323             fun print_classparam_decl (classparam, ty) =
   324               print_val_decl print_typscheme
   325                 (Constant classparam, ([(v, [class])], ty));
   326             fun print_classparam_field (classparam, ty) =
   327               print_field (deresolve_const classparam) (print_typ NOBR ty);
   328             fun print_classparam_proj (classparam, ty) =
   329               print_proj (deresolve_const classparam)
   330                 (print_typscheme ([(v, [class])], ty));
   331           in pair
   332             (concat [str "type", print_dicttyp (class, ITyVar v)]
   333               :: (if Code_Namespace.is_public export
   334                  then map print_super_class_decl classrels
   335                    @ map print_classparam_decl classparams
   336                  else []))
   337             (Pretty.chunks (
   338               concat [
   339                 str "type",
   340                 print_dicttyp (class, ITyVar v),
   341                 str "=",
   342                 enum "," "{" "};" (
   343                   map print_super_class_field classrels
   344                   @ map print_classparam_field classparams
   345                 )
   346               ]
   347               :: map print_super_class_proj classrels
   348               @ map print_classparam_proj classparams
   349             ))
   350           end;
   351   in print_stmt end;
   352 
   353 fun print_sml_module name decls body =
   354   Pretty.chunks2 (
   355     Pretty.chunks [
   356       str ("structure " ^ name ^ " : sig"),
   357       (indent 2 o Pretty.chunks) decls,
   358       str "end = struct"
   359     ]
   360     :: body
   361     @| str ("end; (*struct " ^ name ^ "*)")
   362   );
   363 
   364 val literals_sml = Literals {
   365   literal_string = print_sml_string,
   366   literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
   367   literal_list = enum "," "[" "]",
   368   infix_cons = (7, "::")
   369 };
   370 
   371 
   372 (** OCaml serializer **)
   373 
   374 val print_ocaml_string =
   375   let
   376     fun chr i =
   377       let
   378         val xs = string_of_int i;
   379         val ys = replicate_string (3 - length (raw_explode xs)) "0";
   380       in "\\" ^ ys ^ xs end;
   381     fun char c =
   382       let
   383         val i = ord c;
   384         val s =
   385           if i >= 128 then error "non-ASCII byte in OCaml string literal"
   386           else if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
   387           then chr i else c
   388       in s end;
   389   in quote o translate_string char end;
   390 
   391 fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   392   let
   393     val deresolve_const = deresolve o Constant;
   394     val deresolve_classrel = deresolve o Class_Relation;
   395     val deresolve_inst = deresolve o Class_Instance;
   396     fun print_tyco_expr (sym, []) = (str o deresolve) sym
   397       | print_tyco_expr (sym, [ty]) =
   398           concat [print_typ BR ty, (str o deresolve) sym]
   399       | print_tyco_expr (sym, tys) =
   400           concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
   401     and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
   402          of NONE => print_tyco_expr (Type_Constructor tyco, tys)
   403           | SOME (_, print) => print print_typ fxy tys)
   404       | print_typ fxy (ITyVar v) = str ("'" ^ v);
   405     fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
   406     fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
   407       (map_filter (fn (v, sort) =>
   408         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
   409     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
   410     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
   411     val print_classrels =
   412       fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve_classrel) classrel])
   413     fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
   414       print_plain_dict is_pseudo_fun fxy x
   415       |> print_classrels classrels
   416     and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
   417           brackify BR ((str o deresolve_inst) inst ::
   418             (if is_pseudo_fun (Class_Instance inst) then [str "()"]
   419             else map_filter (print_dicts is_pseudo_fun BR) dss))
   420       | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) =
   421           str (if length = 1 then "_" ^ Name.enforce_case true var
   422             else "_" ^ Name.enforce_case true var ^ string_of_int (index + 1))
   423     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
   424     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
   425       (map_index (fn (i, _) => Dict ([],
   426          Dict_Var { var = v, index = i, length = length sort, class = nth sort i, unique = true })) sort));
   427     fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
   428           print_app is_pseudo_fun some_thm vars fxy (const, [])
   429       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
   430           str "_"
   431       | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
   432           str (lookup_var vars v)
   433       | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
   434           (case Code_Thingol.unfold_const_app t
   435            of SOME app => print_app is_pseudo_fun some_thm vars fxy app
   436             | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
   437                 print_term is_pseudo_fun some_thm vars BR t2])
   438       | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
   439           let
   440             val (binds, t') = Code_Thingol.unfold_pat_abs t;
   441             val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
   442           in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
   443       | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
   444           (case Code_Thingol.unfold_const_app (#primitive case_expr)
   445            of SOME (app as ({ sym = Constant const, ... }, _)) =>
   446                 if is_none (const_syntax const)
   447                 then print_case is_pseudo_fun some_thm vars fxy case_expr
   448                 else print_app is_pseudo_fun some_thm vars fxy app
   449             | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
   450     and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
   451       if is_constr sym then
   452         let val k = length dom in
   453           if length ts = k
   454           then (str o deresolve) sym
   455             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
   456           else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
   457         end
   458       else if is_pseudo_fun sym
   459         then (str o deresolve) sym @@ str "()"
   460       else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
   461         @ map (print_term is_pseudo_fun some_thm vars BR) ts
   462     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   463       (print_term is_pseudo_fun) const_syntax some_thm vars
   464     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
   465     and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
   466           (concat o map str) ["failwith", "\"empty case\""]
   467       | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
   468           let
   469             val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
   470             fun print_let ((pat, _), t) vars =
   471               vars
   472               |> print_bind is_pseudo_fun some_thm NOBR pat
   473               |>> (fn p => concat
   474                   [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"])
   475             val (ps, vars') = fold_map print_let binds vars;
   476           in
   477             brackets [Pretty.chunks ps, print_term is_pseudo_fun some_thm vars' NOBR body]
   478           end
   479       | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
   480           let
   481             fun print_select delim (pat, body) =
   482               let
   483                 val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
   484               in concat [str delim, p, str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end;
   485           in
   486             brackets (
   487               str "match"
   488               :: print_term is_pseudo_fun some_thm vars NOBR t
   489               :: print_select "with" clause
   490               :: map (print_select "|") clauses
   491             )
   492           end;
   493     fun print_val_decl print_typscheme (sym, typscheme) = concat
   494       [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
   495     fun print_datatype_decl definer (tyco, (vs, cos)) =
   496       let
   497         fun print_co ((co, _), []) = str (deresolve_const co)
   498           | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
   499               enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
   500       in
   501         concat (
   502           str definer
   503           :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
   504           :: str "="
   505           :: separate (str "|") (map print_co cos)
   506         )
   507       end;
   508     fun print_def is_pseudo_fun needs_typ definer
   509           (ML_Function (const, (vs_ty as (vs, ty), eqs))) =
   510           let
   511             fun print_eqn ((ts, t), (some_thm, _)) =
   512               let
   513                 val vars = reserved
   514                   |> intro_base_names_for (is_none o const_syntax)
   515                       deresolve (t :: ts)
   516                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
   517                       (insert (op =)) ts []);
   518               in concat [
   519                 (Pretty.block o commas)
   520                   (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
   521                 str "->",
   522                 print_term is_pseudo_fun some_thm vars NOBR t
   523               ] end;
   524             fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =
   525                   let
   526                     val vars = reserved
   527                       |> intro_base_names_for (is_none o const_syntax)
   528                           deresolve (t :: ts)
   529                       |> intro_vars ((fold o Code_Thingol.fold_varnames)
   530                           (insert (op =)) ts []);
   531                   in
   532                     concat (
   533                       (if is_pseudo then [str "()"]
   534                         else map (print_term is_pseudo_fun some_thm vars BR) ts)
   535                       @ str "="
   536                       @@ print_term is_pseudo_fun some_thm vars NOBR t
   537                     )
   538                   end
   539               | print_eqns _ ((eq as (([_], _), _)) :: eqs) =
   540                   Pretty.block (
   541                     str "="
   542                     :: Pretty.brk 1
   543                     :: str "function"
   544                     :: Pretty.brk 1
   545                     :: print_eqn eq
   546                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   547                           o single o print_eqn) eqs
   548                   )
   549               | print_eqns _ (eqs as eq :: eqs') =
   550                   let
   551                     val vars = reserved
   552                       |> intro_base_names_for (is_none o const_syntax)
   553                            deresolve (map (snd o fst) eqs)
   554                     val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
   555                   in
   556                     Pretty.block (
   557                       Pretty.breaks dummy_parms
   558                       @ Pretty.brk 1
   559                       :: str "="
   560                       :: Pretty.brk 1
   561                       :: str "match"
   562                       :: Pretty.brk 1
   563                       :: (Pretty.block o commas) dummy_parms
   564                       :: Pretty.brk 1
   565                       :: str "with"
   566                       :: Pretty.brk 1
   567                       :: print_eqn eq
   568                       :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   569                            o single o print_eqn) eqs'
   570                     )
   571                   end;
   572             val prolog = if needs_typ then
   573               concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
   574                 else (concat o map str) [definer, deresolve_const const];
   575           in pair
   576             (print_val_decl print_typscheme (Constant const, vs_ty))
   577             (concat (
   578               prolog
   579               :: print_dict_args vs
   580               @| print_eqns (is_pseudo_fun (Constant const)) eqs
   581             ))
   582           end
   583       | print_def is_pseudo_fun _ definer
   584           (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) =
   585           let
   586             fun print_super_instance (super_class, x) =
   587               concat [
   588                 (str o deresolve_classrel) (class, super_class),
   589                 str "=",
   590                 print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
   591               ];
   592             fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
   593               concat [
   594                 (str o deresolve_const) classparam,
   595                 str "=",
   596                 print_app (K false) (SOME thm) reserved NOBR (const, [])
   597               ];
   598           in pair
   599             (print_val_decl print_dicttypscheme
   600               (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   601             (concat (
   602               str definer
   603               :: (str o deresolve_inst) inst
   604               :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
   605                   else print_dict_args vs)
   606               @ str "="
   607               @@ brackets [
   608                 enum_default "()" ";" "{" "}" (map print_super_instance superinsts
   609                   @ map print_classparam_instance inst_params),
   610                 str ":",
   611                 print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
   612               ]
   613             ))
   614           end;
   615      fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair
   616           [print_val_decl print_typscheme (Constant const, vs_ty)]
   617           ((doublesemicolon o map str) (
   618             "let"
   619             :: deresolve_const const
   620             :: replicate n "_"
   621             @ "="
   622             :: "failwith"
   623             @@ print_ocaml_string const
   624           ))
   625       | print_stmt _ (ML_Val binding) =
   626           let
   627             val (sig_p, p) = print_def (K false) true "let" binding
   628           in pair
   629             [sig_p]
   630             (doublesemicolon [p])
   631           end
   632       | print_stmt _ (ML_Funs ((export, binding) :: exports_bindings, pseudo_funs)) =
   633           let
   634             val print_def' = print_def (member (op =) pseudo_funs) false;
   635             fun print_pseudo_fun sym = concat [
   636                 str "let",
   637                 (str o deresolve) sym,
   638                 str "=",
   639                 (str o deresolve) sym,
   640                 str "();;"
   641               ];
   642             val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
   643               (print_def' "let rec" binding :: map (print_def' "and" o snd) exports_bindings);
   644             val pseudo_ps = map print_pseudo_fun pseudo_funs;
   645           in pair
   646             (map_filter (fn (export, p) => if Code_Namespace.not_private export then SOME p else NONE)
   647               ((export :: map fst exports_bindings) ~~ sig_ps))
   648             (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))
   649           end
   650      | print_stmt _ (ML_Datas [(tyco, (vs, []))]) =
   651           let
   652             val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
   653           in
   654             pair
   655             [concat [str "type", ty_p]]
   656             (doublesemicolon [str "type", ty_p, str "=", str "EMPTY__"])
   657           end
   658      | print_stmt export (ML_Datas (data :: datas)) = 
   659           let
   660             val decl_ps = print_datatype_decl "type" data
   661               :: map (print_datatype_decl "and") datas;
   662             val (ps, p) = split_last decl_ps;
   663           in pair
   664             (if Code_Namespace.is_public export
   665               then decl_ps
   666               else map (fn (tyco, (vs, _)) =>
   667                 concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
   668                 (data :: datas))
   669             (Pretty.chunks (ps @| doublesemicolon [p]))
   670           end
   671      | print_stmt export (ML_Class (class, (v, (classrels, classparams)))) =
   672           let
   673             fun print_field s p = concat [str s, str ":", p];
   674             fun print_super_class_field (classrel as (_, super_class)) =
   675               print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
   676             fun print_classparam_decl (classparam, ty) =
   677               print_val_decl print_typscheme
   678                 (Constant classparam, ([(v, [class])], ty));
   679             fun print_classparam_field (classparam, ty) =
   680               print_field (deresolve_const classparam) (print_typ NOBR ty);
   681             val w = "_" ^ Name.enforce_case true v;
   682             fun print_classparam_proj (classparam, _) =
   683               (concat o map str) ["let", deresolve_const classparam, w, "=",
   684                 w ^ "." ^ deresolve_const classparam ^ ";;"];
   685             val type_decl_p = concat [
   686                 str "type",
   687                 print_dicttyp (class, ITyVar v),
   688                 str "=",
   689                 enum_default "unit" ";" "{" "}" (
   690                   map print_super_class_field classrels
   691                   @ map print_classparam_field classparams
   692                 )
   693               ];
   694           in pair
   695            (if Code_Namespace.is_public export
   696               then type_decl_p :: map print_classparam_decl classparams
   697               else if null classrels andalso null classparams
   698               then [type_decl_p] (*work around weakness in export calculation*)
   699               else [concat [str "type", print_dicttyp (class, ITyVar v)]])
   700             (Pretty.chunks (
   701               doublesemicolon [type_decl_p]
   702               :: map print_classparam_proj classparams
   703             ))
   704           end;
   705   in print_stmt end;
   706 
   707 fun print_ocaml_module name decls body =
   708   Pretty.chunks2 (
   709     Pretty.chunks [
   710       str ("module " ^ name ^ " : sig"),
   711       (indent 2 o Pretty.chunks) decls,
   712       str "end = struct"
   713     ]
   714     :: body
   715     @| str ("end;; (*struct " ^ name ^ "*)")
   716   );
   717 
   718 val literals_ocaml = let
   719   fun numeral_ocaml k = if k < 0
   720     then "(Z.neg " ^ numeral_ocaml (~ k) ^ ")"
   721     else if k <= 1073741823
   722       then "(Z.of_int " ^ string_of_int k ^ ")"
   723       else "(Z.of_string " ^ quote (string_of_int k) ^ ")"
   724 in Literals {
   725   literal_string = print_ocaml_string,
   726   literal_numeral = numeral_ocaml,
   727   literal_list = enum ";" "[" "]",
   728   infix_cons = (6, "::")
   729 } end;
   730 
   731 
   732 
   733 (** SML/OCaml generic part **)
   734 
   735 fun ml_program_of_program ctxt module_name reserved identifiers =
   736   let
   737     fun namify_const upper base (nsp_const, nsp_type) =
   738       let
   739         val (base', nsp_const') = Name.variant (Name.enforce_case upper base) nsp_const
   740       in (base', (nsp_const', nsp_type)) end;
   741     fun namify_type base (nsp_const, nsp_type) =
   742       let
   743         val (base', nsp_type') = Name.variant (Name.enforce_case false base) nsp_type
   744       in (base', (nsp_const, nsp_type')) end;
   745     fun namify_stmt (Code_Thingol.Fun _) = namify_const false
   746       | namify_stmt (Code_Thingol.Datatype _) = namify_type
   747       | namify_stmt (Code_Thingol.Datatypecons _) = namify_const true
   748       | namify_stmt (Code_Thingol.Class _) = namify_type
   749       | namify_stmt (Code_Thingol.Classrel _) = namify_const false
   750       | namify_stmt (Code_Thingol.Classparam _) = namify_const false
   751       | namify_stmt (Code_Thingol.Classinst _) = namify_const false;
   752     fun ml_binding_of_stmt (sym as Constant const, (export, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _))) =
   753           let
   754             val eqs = filter (snd o snd) raw_eqs;
   755             val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs
   756                of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
   757                   then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
   758                   else (eqs, SOME (sym, member (op =) (Code_Thingol.add_constsyms t []) sym))
   759                 | _ => (eqs, NONE)
   760               else (eqs, NONE)
   761           in ((export, ML_Function (const, (tysm, eqs'))), some_sym) end
   762       | ml_binding_of_stmt (sym as Class_Instance inst, (export, Code_Thingol.Classinst (stmt as { vs, ... }))) =
   763           ((export, ML_Instance (inst, stmt)),
   764             if forall (null o snd) vs then SOME (sym, false) else NONE)
   765       | ml_binding_of_stmt (sym, _) =
   766           error ("Binding block containing illegal statement: " ^ 
   767             Code_Symbol.quote ctxt sym)
   768     fun modify_fun (sym, (export, stmt)) =
   769       let
   770         val ((export', binding), some_value_sym) = ml_binding_of_stmt (sym, (export, stmt));
   771         val ml_stmt = case binding
   772          of ML_Function (const, ((vs, ty), [])) =>
   773               ML_Exc (const, ((vs, ty),
   774                 (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
   775           | _ => case some_value_sym
   776              of NONE => ML_Funs ([(export', binding)], [])
   777               | SOME (sym, true) => ML_Funs ([(export, binding)], [sym])
   778               | SOME (sym, false) => ML_Val binding
   779       in SOME (export, ml_stmt) end;
   780     fun modify_funs stmts = single (SOME
   781       (Code_Namespace.Opaque, ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
   782     fun modify_datatypes stmts =
   783       let
   784         val datas = map_filter
   785           (fn (Type_Constructor tyco, (export, Code_Thingol.Datatype stmt)) => SOME (export, (tyco, stmt)) | _ => NONE) stmts
   786       in
   787         if null datas then [] (*for abstract types wrt. code_reflect*)
   788         else datas
   789           |> split_list
   790           |> apfst Code_Namespace.join_exports
   791           |> apsnd ML_Datas
   792           |> SOME
   793           |> single
   794       end;
   795     fun modify_class stmts =
   796       the_single (map_filter
   797         (fn (Type_Class class, (export, Code_Thingol.Class stmt)) => SOME (export, (class, stmt)) | _ => NONE) stmts)
   798       |> apsnd ML_Class
   799       |> SOME
   800       |> single;
   801     fun modify_stmts ([stmt as (_, (_, stmt' as Code_Thingol.Fun _))]) =
   802           if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
   803       | modify_stmts ((stmts as (_, (_, Code_Thingol.Fun _)) :: _)) =
   804           modify_funs (filter_out (Code_Thingol.is_case o snd o snd) stmts)
   805       | modify_stmts ((stmts as (_, (_, Code_Thingol.Datatypecons _)) :: _)) =
   806           modify_datatypes stmts
   807       | modify_stmts ((stmts as (_, (_, Code_Thingol.Datatype _)) :: _)) =
   808           modify_datatypes stmts
   809       | modify_stmts ((stmts as (_, (_, Code_Thingol.Class _)) :: _)) =
   810           modify_class stmts
   811       | modify_stmts ((stmts as (_, (_, Code_Thingol.Classrel _)) :: _)) =
   812           modify_class stmts
   813       | modify_stmts ((stmts as (_, (_, Code_Thingol.Classparam _)) :: _)) =
   814           modify_class stmts
   815       | modify_stmts ([stmt as (_, (_, Code_Thingol.Classinst _))]) =
   816           [modify_fun stmt]
   817       | modify_stmts ((stmts as (_, (_, Code_Thingol.Classinst _)) :: _)) =
   818           modify_funs stmts
   819       | modify_stmts stmts = error ("Illegal mutual dependencies: " ^
   820           (Library.commas o map (Code_Symbol.quote ctxt o fst)) stmts);
   821   in
   822     Code_Namespace.hierarchical_program ctxt {
   823       module_name = module_name, reserved = reserved, identifiers = identifiers,
   824       empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
   825       cyclic_modules = false, class_transitive = true,
   826       class_relation_public = true, empty_data = (),
   827       memorize_data = K I, modify_stmts = modify_stmts }
   828   end;
   829 
   830 fun serialize_ml print_ml_module print_ml_stmt ml_extension ctxt
   831     { module_name, reserved_syms, identifiers, includes,
   832       class_syntax, tyco_syntax, const_syntax } program exports =
   833   let
   834 
   835     (* build program *)
   836     val { deresolver, hierarchical_program = ml_program } =
   837       ml_program_of_program ctxt module_name (Name.make_context reserved_syms)
   838         identifiers exports program;
   839 
   840     (* print statements *)
   841     fun print_stmt prefix_fragments (_, (export, stmt)) = print_ml_stmt
   842       tyco_syntax const_syntax (make_vars reserved_syms)
   843       (Code_Thingol.is_constr program) (deresolver prefix_fragments) export stmt
   844       |> apfst (fn decl => if Code_Namespace.not_private export then SOME decl else NONE);
   845 
   846     (* print modules *)
   847     fun print_module _ base _ xs =
   848       let
   849         val (raw_decls, body) = split_list xs;
   850         val decls = maps these raw_decls
   851       in (NONE, print_ml_module base decls body) end;
   852 
   853     (* serialization *)
   854     val p = Pretty.chunks2 (map snd includes
   855       @ map snd (Code_Namespace.print_hierarchical {
   856         print_module = print_module, print_stmt = print_stmt,
   857         lift_markup = apsnd } ml_program));
   858   in
   859     (Code_Target.Singleton (ml_extension, p), try (deresolver []))
   860   end;
   861 
   862 val serializer_sml : Code_Target.serializer =
   863   Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_sml_module print_sml_stmt "ML");
   864 
   865 val serializer_ocaml : Code_Target.serializer =
   866   Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_ocaml_module print_ocaml_stmt "ocaml");
   867 
   868 
   869 (** Isar setup **)
   870 
   871 fun fun_syntax print_typ fxy [ty1, ty2] =
   872   brackify_infix (1, R) fxy (
   873     print_typ (INFX (1, X)) ty1,
   874     str "->",
   875     print_typ (INFX (1, R)) ty2
   876   );
   877 
   878 val _ = Theory.setup
   879   (Code_Target.add_language
   880     (target_SML, {serializer = serializer_sml, literals = literals_sml,
   881       check = {env_var = "",
   882         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   883         make_command = fn _ =>
   884           "isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure"},
   885       evaluation_args = []})
   886   #> Code_Target.add_language
   887     (target_OCaml, {serializer = serializer_ocaml, literals = literals_ocaml,
   888       check = {env_var = "ISABELLE_OCAMLEXEC",
   889         make_destination = fn p => Path.append p (Path.explode "ROOT.ml")
   890           (*extension demanded by OCaml compiler*),
   891         make_command = fn _ =>
   892           "\"$ISABELLE_OCAMLEXEC\" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml"},
   893       evaluation_args = []})
   894   #> Code_Target.set_printings (Type_Constructor ("fun",
   895     [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
   896   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   897   #> fold (Code_Target.add_reserved target_SML)
   898       ["ref" (*rebinding is illegal*), "o" (*dictionary projections use it already*),
   899         "Fail", "div", "mod" (*standard infixes*), "IntInf"]
   900   #> fold (Code_Target.add_reserved target_OCaml) [
   901       "and", "as", "assert", "begin", "class",
   902       "constraint", "do", "done", "downto", "else", "end", "exception",
   903       "external", "false", "for", "fun", "function", "functor", "if",
   904       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
   905       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
   906       "sig", "struct", "then", "to", "true", "try", "type", "val",
   907       "virtual", "when", "while", "with"
   908     ]
   909   #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Z"]);
   910 
   911 end; (*struct*)