src/Tools/code/code_ml.ML
author haftmann
Wed Oct 22 14:15:45 2008 +0200 (2008-10-22)
changeset 28663 bd8438543bf2
parent 28350 715163ec93c0
child 28673 d746a8c12c43
permissions -rw-r--r--
code identifier namings are no longer imperative
     1 (*  Title:      Tools/code/code_ml.ML
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 
     5 Serializer for SML and OCaml.
     6 *)
     7 
     8 signature CODE_ML =
     9 sig
    10   val eval_conv: string * (unit -> thm) option ref
    11     -> theory -> cterm -> string list -> thm;
    12   val eval_term: string * (unit -> 'a) option ref
    13     -> theory -> term -> string list -> 'a;
    14   val setup: theory -> theory
    15 end;
    16 
    17 structure Code_ML : CODE_ML =
    18 struct
    19 
    20 open Basic_Code_Thingol;
    21 open Code_Printer;
    22 
    23 infixr 5 @@;
    24 infixr 5 @|;
    25 
    26 val target_SML = "SML";
    27 val target_OCaml = "OCaml";
    28 
    29 datatype ml_stmt =
    30     MLFuns of (string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)) list
    31   | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
    32   | MLClass of string * (vname * ((class * string) list * (string * itype) list))
    33   | MLClassinst of string * ((class * (string * (vname * sort) list))
    34         * ((class * (string * (string * dict list list))) list
    35       * ((string * const) * (thm * bool)) list));
    36 
    37 fun stmt_names_of (MLFuns fs) = map fst fs
    38   | stmt_names_of (MLDatas ds) = map fst ds
    39   | stmt_names_of (MLClass (c, _)) = [c]
    40   | stmt_names_of (MLClassinst (i, _)) = [i];
    41 
    42 
    43 (** SML serailizer **)
    44 
    45 fun pr_sml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
    46   let
    47     val pr_label_classrel = translate_string (fn "." => "__" | c => c)
    48       o NameSpace.qualifier;
    49     val pr_label_classparam = NameSpace.base o NameSpace.qualifier;
    50     fun pr_dicts fxy ds =
    51       let
    52         fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_"
    53           | pr_dictvar (v, (i, _)) = Code_Name.first_upper v ^ string_of_int (i+1) ^ "_";
    54         fun pr_proj [] p =
    55               p
    56           | pr_proj [p'] p =
    57               brackets [p', p]
    58           | pr_proj (ps as _ :: _) p =
    59               brackets [Pretty.enum " o" "(" ")" ps, p];
    60         fun pr_dict fxy (DictConst (inst, dss)) =
    61               brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
    62           | pr_dict fxy (DictVar (classrels, v)) =
    63               pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v)
    64       in case ds
    65        of [] => str "()"
    66         | [d] => pr_dict fxy d
    67         | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
    68       end;
    69     fun pr_tyvar_dicts vs =
    70       vs
    71       |> map (fn (v, sort) => map_index (fn (i, _) =>
    72            DictVar ([], (v, (i, length sort)))) sort)
    73       |> map (pr_dicts BR);
    74     fun pr_tycoexpr fxy (tyco, tys) =
    75       let
    76         val tyco' = (str o deresolve) tyco
    77       in case map (pr_typ BR) tys
    78        of [] => tyco'
    79         | [p] => Pretty.block [p, Pretty.brk 1, tyco']
    80         | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
    81       end
    82     and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
    83          of NONE => pr_tycoexpr fxy (tyco, tys)
    84           | SOME (i, pr) => pr pr_typ fxy tys)
    85       | pr_typ fxy (ITyVar v) = str ("'" ^ v);
    86     fun pr_term thm pat vars fxy (IConst c) =
    87           pr_app thm pat vars fxy (c, [])
    88       | pr_term thm pat vars fxy (IVar v) =
    89           str (Code_Name.lookup_var vars v)
    90       | pr_term thm pat vars fxy (t as t1 `$ t2) =
    91           (case Code_Thingol.unfold_const_app t
    92            of SOME c_ts => pr_app thm pat vars fxy c_ts
    93             | NONE =>
    94                 brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
    95       | pr_term thm pat vars fxy (t as _ `|-> _) =
    96           let
    97             val (binds, t') = Code_Thingol.unfold_abs t;
    98             fun pr ((v, pat), ty) =
    99               pr_bind thm NOBR ((SOME v, pat), ty)
   100               #>> (fn p => concat [str "fn", p, str "=>"]);
   101             val (ps, vars') = fold_map pr binds vars;
   102           in brackets (ps @ [pr_term thm pat vars' NOBR t']) end
   103       | pr_term thm pat vars fxy (ICase (cases as (_, t0))) =
   104           (case Code_Thingol.unfold_const_app t0
   105            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   106                 then pr_case thm vars fxy cases
   107                 else pr_app thm pat vars fxy c_ts
   108             | NONE => pr_case thm vars fxy cases)
   109     and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
   110       if is_cons c then let
   111         val k = length tys
   112       in if k < 2 then 
   113         (str o deresolve) c :: map (pr_term thm pat vars BR) ts
   114       else if k = length ts then
   115         [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm pat vars NOBR) ts)]
   116       else [pr_term thm pat vars BR (Code_Thingol.eta_expand k app)] end else
   117         (str o deresolve) c
   118           :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
   119     and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
   120     and pr_bind' ((NONE, NONE), _) = str "_"
   121       | pr_bind' ((SOME v, NONE), _) = str v
   122       | pr_bind' ((NONE, SOME p), _) = p
   123       | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
   124     and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
   125     and pr_case thm vars fxy (cases as ((_, [_]), _)) =
   126           let
   127             val (binds, t') = Code_Thingol.unfold_let (ICase cases);
   128             fun pr ((pat, ty), t) vars =
   129               vars
   130               |> pr_bind thm NOBR ((NONE, SOME pat), ty)
   131               |>> (fn p => semicolon [str "val", p, str "=", pr_term thm false vars NOBR t])
   132             val (ps, vars') = fold_map pr binds vars;
   133           in
   134             Pretty.chunks [
   135               [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
   136               [str ("in"), Pretty.fbrk, pr_term thm false vars' NOBR t'] |> Pretty.block,
   137               str ("end")
   138             ]
   139           end
   140       | pr_case thm vars fxy (((td, ty), b::bs), _) =
   141           let
   142             fun pr delim (pat, t) =
   143               let
   144                 val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
   145               in
   146                 concat [str delim, p, str "=>", pr_term thm false vars' NOBR t]
   147               end;
   148           in
   149             (Pretty.enclose "(" ")" o single o brackify fxy) (
   150               str "case"
   151               :: pr_term thm false vars NOBR td
   152               :: pr "of" b
   153               :: map (pr "|") bs
   154             )
   155           end
   156       | pr_case thm vars fxy ((_, []), _) = str "raise Fail \"empty case\"";
   157     fun pr_stmt (MLFuns (funns as (funn :: funns'))) =
   158           let
   159             val definer =
   160               let
   161                 fun no_args _ (((ts, _), _) :: _) = length ts
   162                   | no_args ty [] = (length o fst o Code_Thingol.unfold_fun) ty;
   163                 fun mk 0 [] = "val"
   164                   | mk 0 vs = if (null o filter_out (null o snd)) vs
   165                       then "val" else "fun"
   166                   | mk k _ = "fun";
   167                 fun chk (_, ((vs, ty), eqs)) NONE = SOME (mk (no_args ty eqs) vs)
   168                   | chk (_, ((vs, ty), eqs)) (SOME defi) =
   169                       if defi = mk (no_args ty eqs) vs then SOME defi
   170                       else error ("Mixing simultaneous vals and funs not implemented: "
   171                         ^ commas (map (labelled_name o fst) funns));
   172               in the (fold chk funns NONE) end;
   173             fun pr_funn definer (name, ((vs, ty), [])) =
   174                   let
   175                     val vs_dict = filter_out (null o snd) vs;
   176                     val n = length vs_dict + (length o fst o Code_Thingol.unfold_fun) ty;
   177                     val exc_str =
   178                       (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
   179                   in
   180                     concat (
   181                       str definer
   182                       :: (str o deresolve) name
   183                       :: map str (replicate n "_")
   184                       @ str "="
   185                       :: str "raise"
   186                       :: str "(Fail"
   187                       @@ str (exc_str ^ ")")
   188                     )
   189                   end
   190               | pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) =
   191                   let
   192                     val vs_dict = filter_out (null o snd) vs;
   193                     val shift = if null eqs' then I else
   194                       map (Pretty.block o single o Pretty.block o single);
   195                     fun pr_eq definer ((ts, t), (thm, _)) =
   196                       let
   197                         val consts = map_filter
   198                           (fn c => if (is_some o syntax_const) c
   199                             then NONE else (SOME o NameSpace.base o deresolve) c)
   200                             ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
   201                         val vars = reserved_names
   202                           |> Code_Name.intro_vars consts
   203                           |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
   204                                (insert (op =)) ts []);
   205                       in
   206                         concat (
   207                           [str definer, (str o deresolve) name]
   208                           @ (if null ts andalso null vs_dict
   209                              then [str ":", pr_typ NOBR ty]
   210                              else
   211                                pr_tyvar_dicts vs_dict
   212                                @ map (pr_term thm true vars BR) ts)
   213                        @ [str "=", pr_term thm false vars NOBR t]
   214                         )
   215                       end
   216                   in
   217                     (Pretty.block o Pretty.fbreaks o shift) (
   218                       pr_eq definer eq
   219                       :: map (pr_eq "|") eqs'
   220                     )
   221                   end;
   222             val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns');
   223           in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
   224      | pr_stmt (MLDatas (datas as (data :: datas'))) =
   225           let
   226             fun pr_co (co, []) =
   227                   str (deresolve co)
   228               | pr_co (co, tys) =
   229                   concat [
   230                     str (deresolve co),
   231                     str "of",
   232                     Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
   233                   ];
   234             fun pr_data definer (tyco, (vs, [])) =
   235                   concat (
   236                     str definer
   237                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   238                     :: str "="
   239                     @@ str "EMPTY__" 
   240                   )
   241               | pr_data definer (tyco, (vs, cos)) =
   242                   concat (
   243                     str definer
   244                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   245                     :: str "="
   246                     :: separate (str "|") (map pr_co cos)
   247                   );
   248             val (ps, p) = split_last
   249               (pr_data "datatype" data :: map (pr_data "and") datas');
   250           in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
   251      | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
   252           let
   253             val w = Code_Name.first_upper v ^ "_";
   254             fun pr_superclass_field (class, classrel) =
   255               (concat o map str) [
   256                 pr_label_classrel classrel, ":", "'" ^ v, deresolve class
   257               ];
   258             fun pr_classparam_field (classparam, ty) =
   259               concat [
   260                 (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty
   261               ];
   262             fun pr_classparam_proj (classparam, _) =
   263               semicolon [
   264                 str "fun",
   265                 (str o deresolve) classparam,
   266                 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
   267                 str "=",
   268                 str ("#" ^ pr_label_classparam classparam),
   269                 str w
   270               ];
   271             fun pr_superclass_proj (_, classrel) =
   272               semicolon [
   273                 str "fun",
   274                 (str o deresolve) classrel,
   275                 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
   276                 str "=",
   277                 str ("#" ^ pr_label_classrel classrel),
   278                 str w
   279               ];
   280           in
   281             Pretty.chunks (
   282               concat [
   283                 str ("type '" ^ v),
   284                 (str o deresolve) class,
   285                 str "=",
   286                 Pretty.enum "," "{" "};" (
   287                   map pr_superclass_field superclasses @ map pr_classparam_field classparams
   288                 )
   289               ]
   290               :: map pr_superclass_proj superclasses
   291               @ map pr_classparam_proj classparams
   292             )
   293           end
   294      | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
   295           let
   296             fun pr_superclass (_, (classrel, dss)) =
   297               concat [
   298                 (str o pr_label_classrel) classrel,
   299                 str "=",
   300                 pr_dicts NOBR [DictConst dss]
   301               ];
   302             fun pr_classparam ((classparam, c_inst), (thm, _)) =
   303               concat [
   304                 (str o pr_label_classparam) classparam,
   305                 str "=",
   306                 pr_app thm false reserved_names NOBR (c_inst, [])
   307               ];
   308           in
   309             semicolon ([
   310               str (if null arity then "val" else "fun"),
   311               (str o deresolve) inst ] @
   312               pr_tyvar_dicts arity @ [
   313               str "=",
   314               Pretty.enum "," "{" "}"
   315                 (map pr_superclass superarities @ map pr_classparam classparam_insts),
   316               str ":",
   317               pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
   318             ])
   319           end;
   320   in pr_stmt end;
   321 
   322 fun pr_sml_module name content =
   323   Pretty.chunks (
   324     str ("structure " ^ name ^ " = ")
   325     :: str "struct"
   326     :: str ""
   327     :: content
   328     @ str ""
   329     @@ str ("end; (*struct " ^ name ^ "*)")
   330   );
   331 
   332 val literals_sml = Literals {
   333   literal_char = prefix "#" o quote o ML_Syntax.print_char,
   334   literal_string = quote o translate_string ML_Syntax.print_char,
   335   literal_numeral = fn unbounded => fn k =>
   336     if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
   337     else string_of_int k,
   338   literal_list = Pretty.enum "," "[" "]",
   339   infix_cons = (7, "::")
   340 };
   341 
   342 
   343 (** OCaml serializer **)
   344 
   345 fun pr_ocaml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
   346   let
   347     fun pr_dicts fxy ds =
   348       let
   349         fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Name.first_upper v
   350           | pr_dictvar (v, (i, _)) = "_" ^ Code_Name.first_upper v ^ string_of_int (i+1);
   351         fun pr_proj ps p =
   352           fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
   353         fun pr_dict fxy (DictConst (inst, dss)) =
   354               brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
   355           | pr_dict fxy (DictVar (classrels, v)) =
   356               pr_proj (map deresolve classrels) ((str o pr_dictvar) v)
   357       in case ds
   358        of [] => str "()"
   359         | [d] => pr_dict fxy d
   360         | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
   361       end;
   362     fun pr_tyvar_dicts vs =
   363       vs
   364       |> map (fn (v, sort) => map_index (fn (i, _) =>
   365            DictVar ([], (v, (i, length sort)))) sort)
   366       |> map (pr_dicts BR);
   367     fun pr_tycoexpr fxy (tyco, tys) =
   368       let
   369         val tyco' = (str o deresolve) tyco
   370       in case map (pr_typ BR) tys
   371        of [] => tyco'
   372         | [p] => Pretty.block [p, Pretty.brk 1, tyco']
   373         | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
   374       end
   375     and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
   376          of NONE => pr_tycoexpr fxy (tyco, tys)
   377           | SOME (i, pr) => pr pr_typ fxy tys)
   378       | pr_typ fxy (ITyVar v) = str ("'" ^ v);
   379     fun pr_term thm pat vars fxy (IConst c) =
   380           pr_app thm pat vars fxy (c, [])
   381       | pr_term thm pat vars fxy (IVar v) =
   382           str (Code_Name.lookup_var vars v)
   383       | pr_term thm pat vars fxy (t as t1 `$ t2) =
   384           (case Code_Thingol.unfold_const_app t
   385            of SOME c_ts => pr_app thm pat vars fxy c_ts
   386             | NONE =>
   387                 brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
   388       | pr_term thm pat vars fxy (t as _ `|-> _) =
   389           let
   390             val (binds, t') = Code_Thingol.unfold_abs t;
   391             fun pr ((v, pat), ty) = pr_bind thm BR ((SOME v, pat), ty);
   392             val (ps, vars') = fold_map pr binds vars;
   393           in brackets (str "fun" :: ps @ str "->" @@ pr_term thm pat vars' NOBR t') end
   394       | pr_term thm pat vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
   395            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   396                 then pr_case thm vars fxy cases
   397                 else pr_app thm pat vars fxy c_ts
   398             | NONE => pr_case thm vars fxy cases)
   399     and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
   400       if is_cons c then
   401         if length tys = length ts
   402         then case ts
   403          of [] => [(str o deresolve) c]
   404           | [t] => [(str o deresolve) c, pr_term thm pat vars BR t]
   405           | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
   406                     (map (pr_term thm pat vars NOBR) ts)]
   407         else [pr_term thm pat vars BR (Code_Thingol.eta_expand (length tys) app)]
   408       else (str o deresolve) c
   409         :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
   410     and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
   411     and pr_bind' ((NONE, NONE), _) = str "_"
   412       | pr_bind' ((SOME v, NONE), _) = str v
   413       | pr_bind' ((NONE, SOME p), _) = p
   414       | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
   415     and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
   416     and pr_case thm vars fxy (cases as ((_, [_]), _)) =
   417           let
   418             val (binds, t') = Code_Thingol.unfold_let (ICase cases);
   419             fun pr ((pat, ty), t) vars =
   420               vars
   421               |> pr_bind thm NOBR ((NONE, SOME pat), ty)
   422               |>> (fn p => concat
   423                   [str "let", p, str "=", pr_term thm false vars NOBR t, str "in"])
   424             val (ps, vars') = fold_map pr binds vars;
   425           in Pretty.chunks (ps @| pr_term thm false vars' NOBR t') end
   426       | pr_case thm vars fxy (((td, ty), b::bs), _) =
   427           let
   428             fun pr delim (pat, t) =
   429               let
   430                 val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
   431               in concat [str delim, p, str "->", pr_term thm false vars' NOBR t] end;
   432           in
   433             (Pretty.enclose "(" ")" o single o brackify fxy) (
   434               str "match"
   435               :: pr_term thm false vars NOBR td
   436               :: pr "with" b
   437               :: map (pr "|") bs
   438             )
   439           end
   440       | pr_case thm vars fxy ((_, []), _) = str "failwith \"empty case\"";
   441     fun fish_params vars eqs =
   442       let
   443         fun fish_param _ (w as SOME _) = w
   444           | fish_param (IVar v) NONE = SOME v
   445           | fish_param _ NONE = NONE;
   446         fun fillup_param _ (_, SOME v) = v
   447           | fillup_param x (i, NONE) = x ^ string_of_int i;
   448         val fished1 = fold (map2 fish_param) eqs (replicate (length (hd eqs)) NONE);
   449         val x = Name.variant (map_filter I fished1) "x";
   450         val fished2 = map_index (fillup_param x) fished1;
   451         val (fished3, _) = Name.variants fished2 Name.context;
   452         val vars' = Code_Name.intro_vars fished3 vars;
   453       in map (Code_Name.lookup_var vars') fished3 end;
   454     fun pr_stmt (MLFuns (funns as funn :: funns')) =
   455           let
   456             fun pr_eq ((ts, t), (thm, _)) =
   457               let
   458                 val consts = map_filter
   459                   (fn c => if (is_some o syntax_const) c
   460                     then NONE else (SOME o NameSpace.base o deresolve) c)
   461                     ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
   462                 val vars = reserved_names
   463                   |> Code_Name.intro_vars consts
   464                   |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
   465                       (insert (op =)) ts []);
   466               in concat [
   467                 (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
   468                 str "->",
   469                 pr_term thm false vars NOBR t
   470               ] end;
   471             fun pr_eqs name ty [] =
   472                   let
   473                     val n = (length o fst o Code_Thingol.unfold_fun) ty;
   474                     val exc_str =
   475                       (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
   476                   in
   477                     concat (
   478                       map str (replicate n "_")
   479                       @ str "="
   480                       :: str "failwith"
   481                       @@ str exc_str
   482                     )
   483                   end
   484               | pr_eqs _ _ [((ts, t), (thm, _))] =
   485                   let
   486                     val consts = map_filter
   487                       (fn c => if (is_some o syntax_const) c
   488                         then NONE else (SOME o NameSpace.base o deresolve) c)
   489                         ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
   490                     val vars = reserved_names
   491                       |> Code_Name.intro_vars consts
   492                       |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
   493                           (insert (op =)) ts []);
   494                   in
   495                     concat (
   496                       map (pr_term thm true vars BR) ts
   497                       @ str "="
   498                       @@ pr_term thm false vars NOBR t
   499                     )
   500                   end
   501               | pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') =
   502                   Pretty.block (
   503                     str "="
   504                     :: Pretty.brk 1
   505                     :: str "function"
   506                     :: Pretty.brk 1
   507                     :: pr_eq eq
   508                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   509                           o single o pr_eq) eqs'
   510                   )
   511               | pr_eqs _ _ (eqs as eq :: eqs') =
   512                   let
   513                     val consts = map_filter
   514                       (fn c => if (is_some o syntax_const) c
   515                         then NONE else (SOME o NameSpace.base o deresolve) c)
   516                         ((fold o Code_Thingol.fold_constnames)
   517                           (insert (op =)) (map (snd o fst) eqs) []);
   518                     val vars = reserved_names
   519                       |> Code_Name.intro_vars consts;
   520                     val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
   521                   in
   522                     Pretty.block (
   523                       Pretty.breaks dummy_parms
   524                       @ Pretty.brk 1
   525                       :: str "="
   526                       :: Pretty.brk 1
   527                       :: str "match"
   528                       :: Pretty.brk 1
   529                       :: (Pretty.block o Pretty.commas) dummy_parms
   530                       :: Pretty.brk 1
   531                       :: str "with"
   532                       :: Pretty.brk 1
   533                       :: pr_eq eq
   534                       :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   535                            o single o pr_eq) eqs'
   536                     )
   537                   end;
   538             fun pr_funn definer (name, ((vs, ty), eqs)) =
   539               concat (
   540                 str definer
   541                 :: (str o deresolve) name
   542                 :: pr_tyvar_dicts (filter_out (null o snd) vs)
   543                 @| pr_eqs name ty eqs
   544               );
   545             val (ps, p) = split_last
   546               (pr_funn "let rec" funn :: map (pr_funn "and") funns');
   547           in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
   548      | pr_stmt (MLDatas (datas as (data :: datas'))) =
   549           let
   550             fun pr_co (co, []) =
   551                   str (deresolve co)
   552               | pr_co (co, tys) =
   553                   concat [
   554                     str (deresolve co),
   555                     str "of",
   556                     Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
   557                   ];
   558             fun pr_data definer (tyco, (vs, [])) =
   559                   concat (
   560                     str definer
   561                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   562                     :: str "="
   563                     @@ str "EMPTY_"
   564                   )
   565               | pr_data definer (tyco, (vs, cos)) =
   566                   concat (
   567                     str definer
   568                     :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
   569                     :: str "="
   570                     :: separate (str "|") (map pr_co cos)
   571                   );
   572             val (ps, p) = split_last
   573               (pr_data "type" data :: map (pr_data "and") datas');
   574           in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
   575      | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
   576           let
   577             val w = "_" ^ Code_Name.first_upper v;
   578             fun pr_superclass_field (class, classrel) =
   579               (concat o map str) [
   580                 deresolve classrel, ":", "'" ^ v, deresolve class
   581               ];
   582             fun pr_classparam_field (classparam, ty) =
   583               concat [
   584                 (str o deresolve) classparam, str ":", pr_typ NOBR ty
   585               ];
   586             fun pr_classparam_proj (classparam, _) =
   587               concat [
   588                 str "let",
   589                 (str o deresolve) classparam,
   590                 str w,
   591                 str "=",
   592                 str (w ^ "." ^ deresolve classparam ^ ";;")
   593               ];
   594           in Pretty.chunks (
   595             concat [
   596               str ("type '" ^ v),
   597               (str o deresolve) class,
   598               str "=",
   599               enum_default "();;" ";" "{" "};;" (
   600                 map pr_superclass_field superclasses
   601                 @ map pr_classparam_field classparams
   602               )
   603             ]
   604             :: map pr_classparam_proj classparams
   605           ) end
   606      | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
   607           let
   608             fun pr_superclass (_, (classrel, dss)) =
   609               concat [
   610                 (str o deresolve) classrel,
   611                 str "=",
   612                 pr_dicts NOBR [DictConst dss]
   613               ];
   614             fun pr_classparam_inst ((classparam, c_inst), (thm, _)) =
   615               concat [
   616                 (str o deresolve) classparam,
   617                 str "=",
   618                 pr_app thm false reserved_names NOBR (c_inst, [])
   619               ];
   620           in
   621             concat (
   622               str "let"
   623               :: (str o deresolve) inst
   624               :: pr_tyvar_dicts arity
   625               @ str "="
   626               @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
   627                 enum_default "()" ";" "{" "}" (map pr_superclass superarities
   628                   @ map pr_classparam_inst classparam_insts),
   629                 str ":",
   630                 pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
   631               ]
   632             )
   633           end;
   634   in pr_stmt end;
   635 
   636 fun pr_ocaml_module name content =
   637   Pretty.chunks (
   638     str ("module " ^ name ^ " = ")
   639     :: str "struct"
   640     :: str ""
   641     :: content
   642     @ str ""
   643     @@ str ("end;; (*struct " ^ name ^ "*)")
   644   );
   645 
   646 val literals_ocaml = let
   647   fun chr i =
   648     let
   649       val xs = string_of_int i;
   650       val ys = replicate_string (3 - length (explode xs)) "0";
   651     in "\\" ^ ys ^ xs end;
   652   fun char_ocaml c =
   653     let
   654       val i = ord c;
   655       val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
   656         then chr i else c
   657     in s end;
   658 in Literals {
   659   literal_char = enclose "'" "'" o char_ocaml,
   660   literal_string = quote o translate_string char_ocaml,
   661   literal_numeral = fn unbounded => fn k => if k >= 0 then
   662       if unbounded then
   663         "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
   664       else string_of_int k
   665     else
   666       if unbounded then
   667         "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
   668           o string_of_int o op ~) k ^ ")"
   669       else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
   670   literal_list = Pretty.enum ";" "[" "]",
   671   infix_cons = (6, "::")
   672 } end;
   673 
   674 
   675 
   676 (** SML/OCaml generic part **)
   677 
   678 local
   679 
   680 datatype ml_node =
   681     Dummy of string
   682   | Stmt of string * ml_stmt
   683   | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
   684 
   685 in
   686 
   687 fun ml_node_of_program labelled_name module_name reserved_names raw_module_alias program =
   688   let
   689     val module_alias = if is_some module_name then K module_name else raw_module_alias;
   690     val reserved_names = Name.make_context reserved_names;
   691     val empty_module = ((reserved_names, reserved_names), Graph.empty);
   692     fun map_node [] f = f
   693       | map_node (m::ms) f =
   694           Graph.default_node (m, Module (m, empty_module))
   695           #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
   696                Module (module_name, (nsp, map_node ms f nodes)));
   697     fun map_nsp_yield [] f (nsp, nodes) =
   698           let
   699             val (x, nsp') = f nsp
   700           in (x, (nsp', nodes)) end
   701       | map_nsp_yield (m::ms) f (nsp, nodes) =
   702           let
   703             val (x, nodes') =
   704               nodes
   705               |> Graph.default_node (m, Module (m, empty_module))
   706               |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) => 
   707                   let
   708                     val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
   709                   in (x, Module (d_module_name, nsp_nodes')) end)
   710           in (x, (nsp, nodes')) end;
   711     fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
   712       let
   713         val (x, nsp_fun') = f nsp_fun
   714       in (x, (nsp_fun', nsp_typ)) end;
   715     fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
   716       let
   717         val (x, nsp_typ') = f nsp_typ
   718       in (x, (nsp_fun, nsp_typ')) end;
   719     val mk_name_module = Code_Name.mk_name_module reserved_names NONE module_alias program;
   720     fun mk_name_stmt upper name nsp =
   721       let
   722         val (_, base) = Code_Name.dest_name name;
   723         val base' = if upper then Code_Name.first_upper base else base;
   724         val ([base''], nsp') = Name.variants [base'] nsp;
   725       in (base'', nsp') end;
   726     fun add_funs stmts =
   727       fold_map
   728         (fn (name, Code_Thingol.Fun (_, stmt)) =>
   729               map_nsp_fun_yield (mk_name_stmt false name) #>>
   730                 rpair (name, stmt |> apsnd (filter (snd o snd)))
   731           | (name, _) =>
   732               error ("Function block containing illegal statement: " ^ labelled_name name)
   733         ) stmts
   734       #>> (split_list #> apsnd MLFuns);
   735     fun add_datatypes stmts =
   736       fold_map
   737         (fn (name, Code_Thingol.Datatype (_, stmt)) =>
   738               map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   739           | (name, Code_Thingol.Datatypecons _) =>
   740               map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
   741           | (name, _) =>
   742               error ("Datatype block containing illegal statement: " ^ labelled_name name)
   743         ) stmts
   744       #>> (split_list #> apsnd (map_filter I
   745         #> (fn [] => error ("Datatype block without data statement: "
   746                   ^ (commas o map (labelled_name o fst)) stmts)
   747              | stmts => MLDatas stmts)));
   748     fun add_class stmts =
   749       fold_map
   750         (fn (name, Code_Thingol.Class (_, stmt)) =>
   751               map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   752           | (name, Code_Thingol.Classrel _) =>
   753               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   754           | (name, Code_Thingol.Classparam _) =>
   755               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   756           | (name, _) =>
   757               error ("Class block containing illegal statement: " ^ labelled_name name)
   758         ) stmts
   759       #>> (split_list #> apsnd (map_filter I
   760         #> (fn [] => error ("Class block without class statement: "
   761                   ^ (commas o map (labelled_name o fst)) stmts)
   762              | [stmt] => MLClass stmt)));
   763     fun add_inst [(name, Code_Thingol.Classinst stmt)] =
   764       map_nsp_fun_yield (mk_name_stmt false name)
   765       #>> (fn base => ([base], MLClassinst (name, stmt)));
   766     fun add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
   767           add_funs stmts
   768       | add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
   769           add_datatypes stmts
   770       | add_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
   771           add_datatypes stmts
   772       | add_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
   773           add_class stmts
   774       | add_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
   775           add_class stmts
   776       | add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
   777           add_class stmts
   778       | add_stmts ((stmts as [(_, Code_Thingol.Classinst _)])) =
   779           add_inst stmts
   780       | add_stmts stmts = error ("Illegal mutual dependencies: " ^
   781           (commas o map (labelled_name o fst)) stmts);
   782     fun add_stmts' stmts nsp_nodes =
   783       let
   784         val names as (name :: names') = map fst stmts;
   785         val deps =
   786           []
   787           |> fold (fold (insert (op =)) o Graph.imm_succs program) names
   788           |> subtract (op =) names;
   789         val (module_names, _) = (split_list o map Code_Name.dest_name) names;
   790         val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
   791           handle Empty =>
   792             error ("Different namespace prefixes for mutual dependencies:\n"
   793               ^ commas (map labelled_name names)
   794               ^ "\n"
   795               ^ commas module_names);
   796         val module_name_path = NameSpace.explode module_name;
   797         fun add_dep name name' =
   798           let
   799             val module_name' = (mk_name_module o fst o Code_Name.dest_name) name';
   800           in if module_name = module_name' then
   801             map_node module_name_path (Graph.add_edge (name, name'))
   802           else let
   803             val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
   804               (module_name_path, NameSpace.explode module_name');
   805           in
   806             map_node common
   807               (fn node => Graph.add_edge_acyclic (diff1, diff2) node
   808                 handle Graph.CYCLES _ => error ("Dependency "
   809                   ^ quote name ^ " -> " ^ quote name'
   810                   ^ " would result in module dependency cycle"))
   811           end end;
   812       in
   813         nsp_nodes
   814         |> map_nsp_yield module_name_path (add_stmts stmts)
   815         |-> (fn (base' :: bases', stmt') =>
   816            apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
   817               #> fold2 (fn name' => fn base' =>
   818                    Graph.new_node (name', (Dummy base'))) names' bases')))
   819         |> apsnd (fold (fn name => fold (add_dep name) deps) names)
   820         |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
   821       end;
   822     val (_, nodes) = empty_module
   823       |> fold add_stmts' (map (AList.make (Graph.get_node program))
   824           (rev (Graph.strong_conn program)));
   825     fun deresolver prefix name = 
   826       let
   827         val module_name = (fst o Code_Name.dest_name) name;
   828         val module_name' = (NameSpace.explode o mk_name_module) module_name;
   829         val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
   830         val stmt_name =
   831           nodes
   832           |> fold (fn name => fn node => case Graph.get_node node name
   833               of Module (_, (_, node)) => node) module_name'
   834           |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
   835                | Dummy stmt_name => stmt_name);
   836       in
   837         NameSpace.implode (remainder @ [stmt_name])
   838       end handle Graph.UNDEF _ =>
   839         error ("Unknown statement name: " ^ labelled_name name);
   840   in (deresolver, nodes) end;
   841 
   842 fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
   843   _ syntax_tyco syntax_const naming program cs destination =
   844   let
   845     val is_cons = Code_Thingol.is_cons program;
   846     val stmt_names = Code_Target.stmt_names_of_destination destination;
   847     val module_name = if null stmt_names then raw_module_name else SOME "Code";
   848     val (deresolver, nodes) = ml_node_of_program labelled_name module_name
   849       reserved_names raw_module_alias program;
   850     val reserved_names = Code_Name.make_vars reserved_names;
   851     fun pr_node prefix (Dummy _) =
   852           NONE
   853       | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
   854           (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME
   855             (pr_stmt naming labelled_name syntax_tyco syntax_const reserved_names
   856               (deresolver prefix) is_cons stmt)
   857           else NONE
   858       | pr_node prefix (Module (module_name, (_, nodes))) =
   859           separate (str "")
   860             ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)
   861               o rev o flat o Graph.strong_conn) nodes)
   862           |> (if null stmt_names then pr_module module_name else Pretty.chunks)
   863           |> SOME;
   864     val cs' = (map o try)
   865       (deresolver (if is_some module_name then the_list module_name else [])) cs;
   866     val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
   867       (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
   868   in
   869     Code_Target.mk_serialization target
   870       (case compile of SOME compile => SOME (compile o Code_Target.code_of_pretty) | NONE => NONE)
   871       (fn NONE => Code_Target.code_writeln | SOME file => File.write file o Code_Target.code_of_pretty)
   872       (rpair cs' o Code_Target.code_of_pretty) p destination
   873   end;
   874 
   875 end; (*local*)
   876 
   877 
   878 (** ML (system language) code for evaluation and instrumentalization **)
   879 
   880 fun ml_code_of thy = Code_Target.serialize_custom thy (target_SML,
   881     (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""),
   882   literals_sml));
   883 
   884 
   885 (* evaluation *)
   886 
   887 fun eval eval'' term_of reff thy ct args =
   888   let
   889     val ctxt = ProofContext.init thy;
   890     val _ = if null (term_frees (term_of ct)) then () else error ("Term "
   891       ^ quote (Syntax.string_of_term_global thy (term_of ct))
   892       ^ " to be evaluated contains free variables");
   893     fun eval' naming program ((vs, ty), t) deps =
   894       let
   895         val _ = if Code_Thingol.contains_dictvar t then
   896           error "Term to be evaluated constains free dictionaries" else ();
   897         val value_name = "Value.VALUE.value"
   898         val program' = program
   899           |> Graph.new_node (value_name,
   900               Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
   901           |> fold (curry Graph.add_edge value_name) deps;
   902         val (value_code, [SOME value_name']) = ml_code_of thy naming program' [value_name];
   903         val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
   904           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
   905       in ML_Context.evaluate ctxt Output.ml_output false reff sml_code end;
   906   in eval'' thy (fn t => (t, eval')) ct end;
   907 
   908 fun eval_conv reff = eval Code_Thingol.eval_conv Thm.term_of reff;
   909 fun eval_term reff = eval Code_Thingol.eval_term I reff;
   910 
   911 
   912 (* instrumentalization by antiquotation *)
   913 
   914 local
   915 
   916 structure CodeAntiqData = ProofDataFun
   917 (
   918   type T = string list * (bool * (string * (string * (string * string) list) Susp.T));
   919   fun init _ = ([], (true, ("", Susp.value ("", []))));
   920 );
   921 
   922 val is_first_occ = fst o snd o CodeAntiqData.get;
   923 
   924 fun delayed_code thy consts () =
   925   let
   926     val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
   927     val (ml_code, consts'') = ml_code_of thy naming program consts';
   928     val const_tab = map2 (fn const => fn NONE =>
   929       error ("Constant " ^ (quote o Code_Unit.string_of_const thy) const
   930         ^ "\nhas a user-defined serialization")
   931       | SOME const' => (const, const')) consts consts''
   932   in (ml_code, const_tab) end;
   933 
   934 fun register_const const ctxt =
   935   let
   936     val (consts, (_, (struct_name, _))) = CodeAntiqData.get ctxt;
   937     val consts' = insert (op =) const consts;
   938     val (struct_name', ctxt') = if struct_name = ""
   939       then ML_Antiquote.variant "Code" ctxt
   940       else (struct_name, ctxt);
   941     val acc_code = Susp.delay (delayed_code (ProofContext.theory_of ctxt) consts');
   942   in CodeAntiqData.put (consts', (false, (struct_name', acc_code))) ctxt' end;
   943 
   944 fun print_code struct_name is_first const ctxt =
   945   let
   946     val (consts, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
   947     val (raw_ml_code, consts_map) = Susp.force acc_code;
   948     val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)
   949       ((the o AList.lookup (op =) consts_map) const);
   950     val ml_code = if is_first then "\nstructure " ^ struct_code_name
   951         ^ " =\nstruct\n\n" ^ raw_ml_code ^ "\nend;\n\n"
   952       else "";
   953   in (ml_code, const'') end;
   954 
   955 in
   956 
   957 fun ml_code_antiq raw_const {struct_name, background} =
   958   let
   959     val const = Code_Unit.check_const (ProofContext.theory_of background) raw_const;
   960     val is_first = is_first_occ background;
   961     val background' = register_const const background;
   962   in (print_code struct_name is_first const, background') end;
   963 
   964 end; (*local*)
   965 
   966 
   967 (** Isar setup **)
   968 
   969 val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
   970 
   971 fun isar_seri_sml module_name =
   972   Code_Target.parse_args (Scan.succeed ())
   973   #> (fn () => serialize_ml target_SML
   974       (SOME (use_text ML_Context.name_space (1, "generated code") Output.ml_output false))
   975       pr_sml_module pr_sml_stmt module_name);
   976 
   977 fun isar_seri_ocaml module_name =
   978   Code_Target.parse_args (Scan.succeed ())
   979   #> (fn () => serialize_ml target_OCaml NONE
   980       pr_ocaml_module pr_ocaml_stmt module_name);
   981 
   982 val setup =
   983   Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
   984   #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
   985   #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
   986       brackify_infix (1, R) fxy [
   987         pr_typ (INFX (1, X)) ty1,
   988         str "->",
   989         pr_typ (INFX (1, R)) ty2
   990       ]))
   991   #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
   992       brackify_infix (1, R) fxy [
   993         pr_typ (INFX (1, X)) ty1,
   994         str "->",
   995         pr_typ (INFX (1, R)) ty2
   996       ]))
   997   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   998   #> fold (Code_Target.add_reserved target_SML)
   999       ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
  1000   #> fold (Code_Target.add_reserved target_OCaml) [
  1001       "and", "as", "assert", "begin", "class",
  1002       "constraint", "do", "done", "downto", "else", "end", "exception",
  1003       "external", "false", "for", "fun", "function", "functor", "if",
  1004       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
  1005       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
  1006       "sig", "struct", "then", "to", "true", "try", "type", "val",
  1007       "virtual", "when", "while", "with"
  1008     ]
  1009   #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod"];
  1010 
  1011 end; (*struct*)