wneuper/isa: src/Tools/Code/code

     1 (*  Title:      Tools/Code/code_ml.ML

     2     Author:     Florian Haftmann, TU Muenchen

     4 Serializer for SML and OCaml.

     5 *)

     7 signature CODE_ML =

     8 sig

     9   val target_SML: string

    10   val target_OCaml: string

    11   val setup: theory -> theory

    12 end;

    14 structure Code_ML : CODE_ML =

    15 struct

    17 open Basic_Code_Thingol;

    18 open Code_Printer;

    20 infixr 5 @@;

    21 infixr 5 @|;

    24 (** generic **)

    26 val target_SML = "SML";

    27 val target_OCaml = "OCaml";

    29 datatype ml_binding =

    30     ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)

    31   | ML_Instance of string * ((class * (string * (vname * sort) list))

    32         * ((class * (string * (string * dict list list))) list

    33       * (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list)));

    35 datatype ml_stmt =

    36     ML_Exc of string * (typscheme * int)

    37   | ML_Val of ml_binding

    38   | ML_Funs of ml_binding list * string list

    39   | ML_Datas of (string * ((vname * sort) list * ((string * vname list) * itype list) list)) list

    40   | ML_Class of string * (vname * ((class * string) list * (string * itype) list));

    42 fun stmt_name_of_binding (ML_Function (name, _)) = name

    43   | stmt_name_of_binding (ML_Instance (name, _)) = name;

    45 fun stmt_names_of (ML_Exc (name, _)) = [name]

    46   | stmt_names_of (ML_Val binding) = [stmt_name_of_binding binding]

    47   | stmt_names_of (ML_Funs (bindings, _)) = map stmt_name_of_binding bindings

    48   | stmt_names_of (ML_Datas ds) = map fst ds

    49   | stmt_names_of (ML_Class (name, _)) = [name];

    51 fun print_product _ [] = NONE

    52   | print_product print [x] = SOME (print x)

    53   | print_product print xs = (SOME o enum " *" "" "") (map print xs);

    55 fun tuplify _ _ [] = NONE

    56   | tuplify print fxy [x] = SOME (print fxy x)

    57   | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));

    60 (** SML serializer **)

    62 fun print_sml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve =

    63   let

    64     fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco

    65       | print_tyco_expr fxy (tyco, [ty]) =

    66           concat [print_typ BR ty, (str o deresolve) tyco]

    67       | print_tyco_expr fxy (tyco, tys) =

    68           concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]

    69     and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco

    70          of NONE => print_tyco_expr fxy (tyco, tys)

    71           | SOME (i, print) => print print_typ fxy tys)

    72       | print_typ fxy (ITyVar v) = str ("'" ^ v);

    73     fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);

    74     fun print_typscheme_prefix (vs, p) = enum " ->" "" ""

    75       (map_filter (fn (v, sort) =>

    76         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);

    77     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);

    78     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);

    79     fun print_classrels fxy [] ps = brackify fxy ps

    80       | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve) classrel, brackify BR ps]

    81       | print_classrels fxy classrels ps =

    82           brackify fxy [enum " o" "(" ")" (map (str o deresolve) classrels), brackify BR ps]

    83     fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =

    84       print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)

    85     and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =

    86           ((str o deresolve) inst ::

    87             (if is_pseudo_fun inst then [str "()"]

    88             else map_filter (print_dicts is_pseudo_fun BR) dss))

    89       | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =

    90           [str (if k = 1 then first_upper v ^ "_"

    91             else first_upper v ^ string_of_int (i+1) ^ "_")]

    92     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);

    93     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR

    94       (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));

    95     fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =

    96           print_app is_pseudo_fun some_thm vars fxy (c, [])

    97       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =

    98           str "_"

    99       | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =

   100           str (lookup_var vars v)

   101       | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =

   102           (case Code_Thingol.unfold_const_app t

   103            of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts

   104             | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,

   105                 print_term is_pseudo_fun some_thm vars BR t2])

   106       | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =

   107           let

   108             val (binds, t') = Code_Thingol.unfold_pat_abs t;

   109             fun print_abs (pat, ty) =

   110               print_bind is_pseudo_fun some_thm NOBR pat

   111               #>> (fn p => concat [str "fn", p, str "=>"]);

   112             val (ps, vars') = fold_map print_abs binds vars;

   113           in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end

   114       | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =

   115           (case Code_Thingol.unfold_const_app t0

   116            of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)

   117                 then print_case is_pseudo_fun some_thm vars fxy cases

   118                 else print_app is_pseudo_fun some_thm vars fxy c_ts

   119             | NONE => print_case is_pseudo_fun some_thm vars fxy cases)

   120     and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), function_typs)), ts)) =

   121       if is_cons c then

   122         let val k = length function_typs in

   123           if k < 2 orelse length ts = k

   124           then (str o deresolve) c

   125             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)

   126           else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]

   127         end

   128       else if is_pseudo_fun c

   129         then (str o deresolve) c @@ str "()"

   130       else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss

   131         @ map (print_term is_pseudo_fun some_thm vars BR) ts

   132     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)

   133       (print_term is_pseudo_fun) const_syntax some_thm vars

   134     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)

   135     and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =

   136           let

   137             val (binds, body) = Code_Thingol.unfold_let (ICase cases);

   138             fun print_match ((pat, ty), t) vars =

   139               vars

   140               |> print_bind is_pseudo_fun some_thm NOBR pat

   141               |>> (fn p => semicolon [str "val", p, str "=",

   142                     print_term is_pseudo_fun some_thm vars NOBR t])

   143             val (ps, vars') = fold_map print_match binds vars;

   144           in

   145             Pretty.chunks [

   146               Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps],

   147               Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body],

   148               str "end"

   149             ]

   150           end

   151       | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =

   152           let

   153             fun print_select delim (pat, body) =

   154               let

   155                 val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;

   156               in

   157                 concat [str delim, p, str "=>", print_term is_pseudo_fun some_thm vars' NOBR body]

   158               end;

   159           in

   160             brackets (

   161               str "case"

   162               :: print_term is_pseudo_fun some_thm vars NOBR t

   163               :: print_select "of" clause

   164               :: map (print_select "|") clauses

   165             )

   166           end

   167       | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =

   168           (concat o map str) ["raise", "Fail", "\"empty case\""];

   169     fun print_val_decl print_typscheme (name, typscheme) = concat

   170       [str "val", str (deresolve name), str ":", print_typscheme typscheme];

   171     fun print_datatype_decl definer (tyco, (vs, cos)) =

   172       let

   173         fun print_co ((co, _), []) = str (deresolve co)

   174           | print_co ((co, _), tys) = concat [str (deresolve co), str "of",

   175               enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];

   176       in

   177         concat (

   178           str definer

   179           :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)

   180           :: str "="

   181           :: separate (str "|") (map print_co cos)

   182         )

   183       end;

   184     fun print_def is_pseudo_fun needs_typ definer

   185           (ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) =

   186           let

   187             fun print_eqn definer ((ts, t), (some_thm, _)) =

   188               let

   189                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];

   190                 val vars = reserved

   191                   |> intro_base_names

   192                        (is_none o const_syntax) deresolve consts

   193                   |> intro_vars ((fold o Code_Thingol.fold_varnames)

   194                        (insert (op =)) ts []);

   195                 val prolog = if needs_typ then

   196                   concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]

   197                     else (concat o map str) [definer, deresolve name];

   198               in

   199                 concat (

   200                   prolog

   201                   :: (if is_pseudo_fun name then [str "()"]

   202                       else print_dict_args vs

   203                         @ map (print_term is_pseudo_fun some_thm vars BR) ts)

   204                   @ str "="

   205                   @@ print_term is_pseudo_fun some_thm vars NOBR t

   206                 )

   207               end

   208             val shift = if null eqs then I else

   209               map (Pretty.block o single o Pretty.block o single);

   210           in pair

   211             (print_val_decl print_typscheme (name, vs_ty))

   212             ((Pretty.block o Pretty.fbreaks o shift) (

   213               print_eqn definer eq

   214               :: map (print_eqn "|") eqs

   215             ))

   216           end

   217       | print_def is_pseudo_fun _ definer

   218           (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =

   219           let

   220             fun print_super_instance (_, (classrel, x)) =

   221               concat [

   222                 (str o Long_Name.base_name o deresolve) classrel,

   223                 str "=",

   224                 print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))

   225               ];

   226             fun print_classparam_instance ((classparam, const), (thm, _)) =

   227               concat [

   228                 (str o Long_Name.base_name o deresolve) classparam,

   229                 str "=",

   230                 print_app (K false) (SOME thm) reserved NOBR (const, [])

   231               ];

   232           in pair

   233             (print_val_decl print_dicttypscheme

   234               (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))

   235             (concat (

   236               str definer

   237               :: (str o deresolve) inst

   238               :: (if is_pseudo_fun inst then [str "()"]

   239                   else print_dict_args vs)

   240               @ str "="

   241               :: enum "," "{" "}"

   242                 (map print_super_instance super_instances

   243                   @ map print_classparam_instance classparam_instances)

   244               :: str ":"

   245               @@ print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])

   246             ))

   247           end;

   248     fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair

   249           [print_val_decl print_typscheme (name, vs_ty)]

   250           ((semicolon o map str) (

   251             (if n = 0 then "val" else "fun")

   252             :: deresolve name

   253             :: replicate n "_"

   254             @ "="

   255             :: "raise"

   256             :: "Fail"

   257             @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name

   258           ))

   259       | print_stmt (ML_Val binding) =

   260           let

   261             val (sig_p, p) = print_def (K false) true "val" binding

   262           in pair

   263             [sig_p]

   264             (semicolon [p])

   265           end

   266       | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =

   267           let

   268             val print_def' = print_def (member (op =) pseudo_funs) false;

   269             fun print_pseudo_fun name = concat [

   270                 str "val",

   271                 (str o deresolve) name,

   272                 str "=",

   273                 (str o deresolve) name,

   274                 str "();"

   275               ];

   276             val (sig_ps, (ps, p)) = (apsnd split_last o split_list)

   277               (print_def' "fun" binding :: map (print_def' "and") bindings);

   278             val pseudo_ps = map print_pseudo_fun pseudo_funs;

   279           in pair

   280             sig_ps

   281             (Pretty.chunks (ps @ semicolon [p] :: pseudo_ps))

   282           end

   283      | print_stmt (ML_Datas [(tyco, (vs, []))]) =

   284           let

   285             val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);

   286           in

   287             pair

   288             [concat [str "type", ty_p]]

   289             (concat [str "datatype", ty_p, str "=", str "EMPTY__"])

   290           end

   291      | print_stmt (ML_Datas (data :: datas)) =

   292           let

   293             val sig_ps = print_datatype_decl "datatype" data

   294               :: map (print_datatype_decl "and") datas;

   295             val (ps, p) = split_last sig_ps;

   296           in pair

   297             sig_ps

   298             (Pretty.chunks (ps @| semicolon [p]))

   299           end

   300      | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =

   301           let

   302             fun print_field s p = concat [str s, str ":", p];

   303             fun print_proj s p = semicolon

   304               (map str ["val", s, "=", "#" ^ s, ":"] @| p);

   305             fun print_super_class_decl (super_class, classrel) =

   306               print_val_decl print_dicttypscheme

   307                 (classrel, ([(v, [class])], (super_class, ITyVar v)));

   308             fun print_super_class_field (super_class, classrel) =

   309               print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));

   310             fun print_super_class_proj (super_class, classrel) =

   311               print_proj (deresolve classrel)

   312                 (print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));

   313             fun print_classparam_decl (classparam, ty) =

   314               print_val_decl print_typscheme

   315                 (classparam, ([(v, [class])], ty));

   316             fun print_classparam_field (classparam, ty) =

   317               print_field (deresolve classparam) (print_typ NOBR ty);

   318             fun print_classparam_proj (classparam, ty) =

   319               print_proj (deresolve classparam)

   320                 (print_typscheme ([(v, [class])], ty));

   321           in pair

   322             (concat [str "type", print_dicttyp (class, ITyVar v)]

   323               :: map print_super_class_decl super_classes

   324               @ map print_classparam_decl classparams)

   325             (Pretty.chunks (

   326               concat [

   327                 str ("type '" ^ v),

   328                 (str o deresolve) class,

   329                 str "=",

   330                 enum "," "{" "};" (

   331                   map print_super_class_field super_classes

   332                   @ map print_classparam_field classparams

   333                 )

   334               ]

   335               :: map print_super_class_proj super_classes

   336               @ map print_classparam_proj classparams

   337             ))

   338           end;

   339   in print_stmt end;

   341 fun print_sml_module name some_decls body =

   342   Pretty.chunks2 (

   343     Pretty.chunks (

   344       str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))

   345       :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls

   346       @| (if is_some some_decls then str "end = struct" else str "struct")

   347     )

   348     :: body

   349     @| str ("end; (*struct " ^ name ^ "*)")

   350   );

   352 val literals_sml = Literals {

   353   literal_char = prefix "#" o quote o ML_Syntax.print_char,

   354   literal_string = quote o translate_string ML_Syntax.print_char,

   355   literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",

   356   literal_positive_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",

   357   literal_alternative_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",

   358   literal_naive_numeral = string_of_int,

   359   literal_list = enum "," "[" "]",

   360   infix_cons = (7, "::")

   361 };

   364 (** OCaml serializer **)

   366 fun print_ocaml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve =

   367   let

   368     fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco

   369       | print_tyco_expr fxy (tyco, [ty]) =

   370           concat [print_typ BR ty, (str o deresolve) tyco]

   371       | print_tyco_expr fxy (tyco, tys) =

   372           concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]

   373     and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco

   374          of NONE => print_tyco_expr fxy (tyco, tys)

   375           | SOME (i, print) => print print_typ fxy tys)

   376       | print_typ fxy (ITyVar v) = str ("'" ^ v);

   377     fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);

   378     fun print_typscheme_prefix (vs, p) = enum " ->" "" ""

   379       (map_filter (fn (v, sort) =>

   380         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);

   381     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);

   382     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);

   383     val print_classrels =

   384       fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve) classrel])

   385     fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =

   386       print_plain_dict is_pseudo_fun fxy x

   387       |> print_classrels classrels

   388     and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =

   389           brackify BR ((str o deresolve) inst ::

   390             (if is_pseudo_fun inst then [str "()"]

   391             else map_filter (print_dicts is_pseudo_fun BR) dss))

   392       | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =

   393           str (if k = 1 then "_" ^ first_upper v

   394             else "_" ^ first_upper v ^ string_of_int (i+1))

   395     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);

   396     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR

   397       (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));

   398     fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =

   399           print_app is_pseudo_fun some_thm vars fxy (c, [])

   400       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =

   401           str "_"

   402       | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =

   403           str (lookup_var vars v)

   404       | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =

   405           (case Code_Thingol.unfold_const_app t

   406            of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts

   407             | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,

   408                 print_term is_pseudo_fun some_thm vars BR t2])

   409       | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =

   410           let

   411             val (binds, t') = Code_Thingol.unfold_pat_abs t;

   412             val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;

   413           in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end

   414       | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =

   415           (case Code_Thingol.unfold_const_app t0

   416            of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)

   417                 then print_case is_pseudo_fun some_thm vars fxy cases

   418                 else print_app is_pseudo_fun some_thm vars fxy c_ts

   419             | NONE => print_case is_pseudo_fun some_thm vars fxy cases)

   420     and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =

   421       if is_cons c then

   422         let val k = length tys in

   423           if length ts = k

   424           then (str o deresolve) c

   425             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)

   426           else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]

   427         end

   428       else if is_pseudo_fun c

   429         then (str o deresolve) c @@ str "()"

   430       else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss

   431         @ map (print_term is_pseudo_fun some_thm vars BR) ts

   432     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)

   433       (print_term is_pseudo_fun) const_syntax some_thm vars

   434     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)

   435     and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =

   436           let

   437             val (binds, body) = Code_Thingol.unfold_let (ICase cases);

   438             fun print_let ((pat, ty), t) vars =

   439               vars

   440               |> print_bind is_pseudo_fun some_thm NOBR pat

   441               |>> (fn p => concat

   442                   [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"])

   443             val (ps, vars') = fold_map print_let binds vars;

   444           in

   445             brackify_block fxy (Pretty.chunks ps) []

   446               (print_term is_pseudo_fun some_thm vars' NOBR body)

   447           end

   448       | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =

   449           let

   450             fun print_select delim (pat, body) =

   451               let

   452                 val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;

   453               in concat [str delim, p, str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end;

   454           in

   455             brackets (

   456               str "match"

   457               :: print_term is_pseudo_fun some_thm vars NOBR t

   458               :: print_select "with" clause

   459               :: map (print_select "|") clauses

   460             )

   461           end

   462       | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =

   463           (concat o map str) ["failwith", "\"empty case\""];

   464     fun print_val_decl print_typscheme (name, typscheme) = concat

   465       [str "val", str (deresolve name), str ":", print_typscheme typscheme];

   466     fun print_datatype_decl definer (tyco, (vs, cos)) =

   467       let

   468         fun print_co ((co, _), []) = str (deresolve co)

   469           | print_co ((co, _), tys) = concat [str (deresolve co), str "of",

   470               enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];

   471       in

   472         concat (

   473           str definer

   474           :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)

   475           :: str "="

   476           :: separate (str "|") (map print_co cos)

   477         )

   478       end;

   479     fun print_def is_pseudo_fun needs_typ definer

   480           (ML_Function (name, (vs_ty as (vs, ty), eqs))) =

   481           let

   482             fun print_eqn ((ts, t), (some_thm, _)) =

   483               let

   484                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];

   485                 val vars = reserved

   486                   |> intro_base_names

   487                       (is_none o const_syntax) deresolve consts

   488                   |> intro_vars ((fold o Code_Thingol.fold_varnames)

   489                       (insert (op =)) ts []);

   490               in concat [

   491                 (Pretty.block o commas)

   492                   (map (print_term is_pseudo_fun some_thm vars NOBR) ts),

   493                 str "->",

   494                 print_term is_pseudo_fun some_thm vars NOBR t

   495               ] end;

   496             fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =

   497                   let

   498                     val consts = fold Code_Thingol.add_constnames (t :: ts) [];

   499                     val vars = reserved

   500                       |> intro_base_names

   501                           (is_none o const_syntax) deresolve consts

   502                       |> intro_vars ((fold o Code_Thingol.fold_varnames)

   503                           (insert (op =)) ts []);

   504                   in

   505                     concat (

   506                       (if is_pseudo then [str "()"]

   507                         else map (print_term is_pseudo_fun some_thm vars BR) ts)

   508                       @ str "="

   509                       @@ print_term is_pseudo_fun some_thm vars NOBR t

   510                     )

   511                   end

   512               | print_eqns _ ((eq as (([_], _), _)) :: eqs) =

   513                   Pretty.block (

   514                     str "="

   515                     :: Pretty.brk 1

   516                     :: str "function"

   517                     :: Pretty.brk 1

   518                     :: print_eqn eq

   519                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]

   520                           o single o print_eqn) eqs

   521                   )

   522               | print_eqns _ (eqs as eq :: eqs') =

   523                   let

   524                     val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];

   525                     val vars = reserved

   526                       |> intro_base_names

   527                           (is_none o const_syntax) deresolve consts;

   528                     val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;

   529                   in

   530                     Pretty.block (

   531                       Pretty.breaks dummy_parms

   532                       @ Pretty.brk 1

   533                       :: str "="

   534                       :: Pretty.brk 1

   535                       :: str "match"

   536                       :: Pretty.brk 1

   537                       :: (Pretty.block o commas) dummy_parms

   538                       :: Pretty.brk 1

   539                       :: str "with"

   540                       :: Pretty.brk 1

   541                       :: print_eqn eq

   542                       :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]

   543                            o single o print_eqn) eqs'

   544                     )

   545                   end;

   546             val prolog = if needs_typ then

   547               concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]

   548                 else (concat o map str) [definer, deresolve name];

   549           in pair

   550             (print_val_decl print_typscheme (name, vs_ty))

   551             (concat (

   552               prolog

   553               :: print_dict_args vs

   554               @| print_eqns (is_pseudo_fun name) eqs

   555             ))

   556           end

   557       | print_def is_pseudo_fun _ definer

   558             (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =

   559           let

   560             fun print_super_instance (_, (classrel, x)) =

   561               concat [

   562                 (str o deresolve) classrel,

   563                 str "=",

   564                 print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))

   565               ];

   566             fun print_classparam_instance ((classparam, const), (thm, _)) =

   567               concat [

   568                 (str o deresolve) classparam,

   569                 str "=",

   570                 print_app (K false) (SOME thm) reserved NOBR (const, [])

   571               ];

   572           in pair

   573             (print_val_decl print_dicttypscheme

   574               (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))

   575             (concat (

   576               str definer

   577               :: (str o deresolve) inst

   578               :: print_dict_args vs

   579               @ str "="

   580               @@ brackets [

   581                 enum_default "()" ";" "{" "}" (map print_super_instance super_instances

   582                   @ map print_classparam_instance classparam_instances),

   583                 str ":",

   584                 print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])

   585               ]

   586             ))

   587           end;

   588      fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair

   589           [print_val_decl print_typscheme (name, vs_ty)]

   590           ((doublesemicolon o map str) (

   591             "let"

   592             :: deresolve name

   593             :: replicate n "_"

   594             @ "="

   595             :: "failwith"

   596             @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name

   597           ))

   598       | print_stmt (ML_Val binding) =

   599           let

   600             val (sig_p, p) = print_def (K false) true "let" binding

   601           in pair

   602             [sig_p]

   603             (doublesemicolon [p])

   604           end

   605       | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =

   606           let

   607             val print_def' = print_def (member (op =) pseudo_funs) false;

   608             fun print_pseudo_fun name = concat [

   609                 str "let",

   610                 (str o deresolve) name,

   611                 str "=",

   612                 (str o deresolve) name,

   613                 str "();;"

   614               ];

   615             val (sig_ps, (ps, p)) = (apsnd split_last o split_list)

   616               (print_def' "let rec" binding :: map (print_def' "and") bindings);

   617             val pseudo_ps = map print_pseudo_fun pseudo_funs;

   618           in pair

   619             sig_ps

   620             (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))

   621           end

   622      | print_stmt (ML_Datas [(tyco, (vs, []))]) =

   623           let

   624             val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);

   625           in

   626             pair

   627             [concat [str "type", ty_p]]

   628             (concat [str "type", ty_p, str "=", str "EMPTY__"])

   629           end

   630      | print_stmt (ML_Datas (data :: datas)) =

   631           let

   632             val sig_ps = print_datatype_decl "type" data

   633               :: map (print_datatype_decl "and") datas;

   634             val (ps, p) = split_last sig_ps;

   635           in pair

   636             sig_ps

   637             (Pretty.chunks (ps @| doublesemicolon [p]))

   638           end

   639      | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =

   640           let

   641             fun print_field s p = concat [str s, str ":", p];

   642             fun print_super_class_field (super_class, classrel) =

   643               print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));

   644             fun print_classparam_decl (classparam, ty) =

   645               print_val_decl print_typscheme

   646                 (classparam, ([(v, [class])], ty));

   647             fun print_classparam_field (classparam, ty) =

   648               print_field (deresolve classparam) (print_typ NOBR ty);

   649             val w = "_" ^ first_upper v;

   650             fun print_classparam_proj (classparam, _) =

   651               (concat o map str) ["let", deresolve classparam, w, "=",

   652                 w ^ "." ^ deresolve classparam ^ ";;"];

   653             val type_decl_p = concat [

   654                 str ("type '" ^ v),

   655                 (str o deresolve) class,

   656                 str "=",

   657                 enum_default "unit" ";" "{" "}" (

   658                   map print_super_class_field super_classes

   659                   @ map print_classparam_field classparams

   660                 )

   661               ];

   662           in pair

   663             (type_decl_p :: map print_classparam_decl classparams)

   664             (Pretty.chunks (

   665               doublesemicolon [type_decl_p]

   666               :: map print_classparam_proj classparams

   667             ))

   668           end;

   669   in print_stmt end;

   671 fun print_ocaml_module name some_decls body =

   672   Pretty.chunks2 (

   673     Pretty.chunks (

   674       str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))

   675       :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls

   676       @| (if is_some some_decls then str "end = struct" else str "struct")

   677     )

   678     :: body

   679     @| str ("end;; (*struct " ^ name ^ "*)")

   680   );

   682 val literals_ocaml = let

   683   fun chr i =

   684     let

   685       val xs = string_of_int i;

   686       val ys = replicate_string (3 - length (raw_explode xs)) "0";

   687     in "\\" ^ ys ^ xs end;

   688   fun char_ocaml c =

   689     let

   690       val i = ord c;

   691       val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126

   692         then chr i else c

   693     in s end;

   694   fun numeral_ocaml k = if k < 0

   695     then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")"

   696     else if k <= 1073741823

   697       then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"

   698       else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"

   699 in Literals {

   700   literal_char = Library.enclose "'" "'" o char_ocaml,

   701   literal_string = quote o translate_string char_ocaml,

   702   literal_numeral = numeral_ocaml,

   703   literal_positive_numeral = numeral_ocaml,

   704   literal_alternative_numeral = numeral_ocaml,

   705   literal_naive_numeral = numeral_ocaml,

   706   literal_list = enum ";" "[" "]",

   707   infix_cons = (6, "::")

   708 } end;

   712 (** SML/OCaml generic part **)

   714 fun ml_program_of_program labelled_name reserved module_alias program =

   715   let

   716     fun namify_const upper base (nsp_const, nsp_type) =

   717       let

   718         val (base', nsp_const') =

   719           Name.variant (if upper then first_upper base else base) nsp_const

   720       in (base', (nsp_const', nsp_type)) end;

   721     fun namify_type base (nsp_const, nsp_type) =

   722       let

   723         val (base', nsp_type') = Name.variant base nsp_type

   724       in (base', (nsp_const, nsp_type')) end;

   725     fun namify_stmt (Code_Thingol.Fun _) = namify_const false

   726       | namify_stmt (Code_Thingol.Datatype _) = namify_type

   727       | namify_stmt (Code_Thingol.Datatypecons _) = namify_const true

   728       | namify_stmt (Code_Thingol.Class _) = namify_type

   729       | namify_stmt (Code_Thingol.Classrel _) = namify_const false

   730       | namify_stmt (Code_Thingol.Classparam _) = namify_const false

   731       | namify_stmt (Code_Thingol.Classinst _) = namify_const false;

   732     fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =

   733           let

   734             val eqs = filter (snd o snd) raw_eqs;

   735             val (eqs', some_value_name) = if null (filter_out (null o snd) vs) then case eqs

   736                of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty

   737                   then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)

   738                   else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))

   739                 | _ => (eqs, NONE)

   740               else (eqs, NONE)

   741           in (ML_Function (name, (tysm, eqs')), some_value_name) end

   742       | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =

   743           (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)

   744       | ml_binding_of_stmt (name, _) =

   745           error ("Binding block containing illegal statement: " ^ labelled_name name)

   746     fun modify_fun (name, stmt) =

   747       let

   748         val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);

   749         val ml_stmt = case binding

   750          of ML_Function (name, ((vs, ty), [])) =>

   751               ML_Exc (name, ((vs, ty),

   752                 (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))

   753           | _ => case some_value_name

   754              of NONE => ML_Funs ([binding], [])

   755               | SOME (name, true) => ML_Funs ([binding], [name])

   756               | SOME (name, false) => ML_Val binding

   757       in SOME ml_stmt end;

   758     fun modify_funs stmts = single (SOME

   759       (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))

   760     fun modify_datatypes stmts = single (SOME

   761       (ML_Datas (map_filter

   762         (fn (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))

   763     fun modify_class stmts = single (SOME

   764       (ML_Class (the_single (map_filter

   765         (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))))

   766     fun modify_stmts ([stmt as (name, stmt' as Code_Thingol.Fun _)]) =

   767           if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]

   768       | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =

   769           modify_funs (filter_out (Code_Thingol.is_case o snd) stmts)

   770       | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =

   771           modify_datatypes stmts

   772       | modify_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =

   773           modify_datatypes stmts

   774       | modify_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =

   775           modify_class stmts

   776       | modify_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =

   777           modify_class stmts

   778       | modify_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =

   779           modify_class stmts

   780       | modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =

   781           [modify_fun stmt]

   782       | modify_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =

   783           modify_funs stmts

   784       | modify_stmts stmts = error ("Illegal mutual dependencies: " ^

   785           (Library.commas o map (labelled_name o fst)) stmts);

   786   in

   787     Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,

   788       empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,

   789       cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program

   790   end;

   792 fun serialize_ml target print_ml_module print_ml_stmt with_signatures

   793     { labelled_name, reserved_syms, includes, module_alias,

   794       class_syntax, tyco_syntax, const_syntax } program =

   795   let

   797     (* build program *)

   798     val { deresolver, hierarchical_program = ml_program } =

   799       ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;

   801     (* print statements *)

   802     fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt

   803       labelled_name tyco_syntax const_syntax (make_vars reserved_syms)

   804       (Code_Thingol.is_cons program) (deresolver prefix_fragments) stmt

   805       |> apfst SOME;

   807     (* print modules *)

   808     fun print_module prefix_fragments base _ xs =

   809       let

   810         val (raw_decls, body) = split_list xs;

   811         val decls = if with_signatures then SOME (maps these raw_decls) else NONE

   812       in (NONE, print_ml_module base decls body) end;

   814     (* serialization *)

   815     val p = Pretty.chunks2 (map snd includes

   816       @ map snd (Code_Namespace.print_hierarchical {

   817         print_module = print_module, print_stmt = print_stmt,

   818         lift_markup = apsnd } ml_program));

   819     fun write width NONE = writeln o format [] width

   820       | write width (SOME p) = File.write p o format [] width;

   821   in

   822     Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p

   823   end;

   825 val serializer_sml : Code_Target.serializer =

   826   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true

   827   >> (fn with_signatures => serialize_ml target_SML

   828       print_sml_module print_sml_stmt with_signatures));

   830 val serializer_ocaml : Code_Target.serializer =

   831   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true

   832   >> (fn with_signatures => serialize_ml target_OCaml

   833       print_ocaml_module print_ocaml_stmt with_signatures));

   836 (** Isar setup **)

   838 val setup =

   839   Code_Target.add_target

   840     (target_SML, { serializer = serializer_sml, literals = literals_sml,

   841       check = { env_var = "ISABELLE_PROCESS",

   842         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),

   843         make_command = fn _ => "\"$ISABELLE_PROCESS\" -r -q -u Pure" } })

   844   #> Code_Target.add_target

   845     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,

   846       check = { env_var = "ISABELLE_OCAML",

   847         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),

   848         make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })

   849   #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>

   850       brackify_infix (1, R) fxy (

   851         print_typ (INFX (1, X)) ty1,

   852         str "->",

   853         print_typ (INFX (1, R)) ty2

   854       )))

   855   #> Code_Target.add_tyco_syntax target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>

   856       brackify_infix (1, R) fxy (

   857         print_typ (INFX (1, X)) ty1,

   858         str "->",

   859         print_typ (INFX (1, R)) ty2

   860       )))

   861   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names

   862   #> fold (Code_Target.add_reserved target_SML)

   863       ["ref" (*rebinding is illegal*), "o" (*dictionary projections use it already*),

   864         "Fail", "div", "mod" (*standard infixes*), "IntInf"]

   865   #> fold (Code_Target.add_reserved target_OCaml) [

   866       "and", "as", "assert", "begin", "class",

   867       "constraint", "do", "done", "downto", "else", "end", "exception",

   868       "external", "false", "for", "fun", "function", "functor", "if",

   869       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",

   870       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",

   871       "sig", "struct", "then", "to", "true", "try", "type", "val",

   872       "virtual", "when", "while", "with"

   873     ]

   874   #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"];

   876 end; (*struct*)

author	wenzelm
	Thu, 09 Jun 2011 17:51:49 +0200
changeset 44208	47cf4bc789aa
parent 43470	1a82b0400b2a
child 44216	165188299a25
permissions	-rw-r--r--