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 print_product _ [] = NONE

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

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

    49 fun tuplify _ _ [] = NONE

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

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

    54 (** SML serializer **)

    56 fun print_sml_stmt tyco_syntax const_syntax reserved is_cons deresolve =

    57   let

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

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

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

    61       | print_tyco_expr fxy (tyco, tys) =

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

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

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

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

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

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

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

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

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

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

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

    73     fun print_classrels fxy [] ps = brackify fxy ps

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

    75       | print_classrels fxy classrels ps =

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

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

    78       print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)

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

    80           ((str o deresolve) inst ::

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

    82             else map_filter (print_dicts is_pseudo_fun BR) dss))

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

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

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

    86     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);

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

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

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

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

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

    92           str "_"

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

    94           str (lookup_var vars v)

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

    96           (case Code_Thingol.unfold_const_app t

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

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

    99                 print_term is_pseudo_fun some_thm vars BR t2])

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

   101           let

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

   103             fun print_abs (pat, ty) =

   104               print_bind is_pseudo_fun some_thm NOBR pat

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

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

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

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

   109           (case Code_Thingol.unfold_const_app t0

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

   111                 then print_case is_pseudo_fun some_thm vars fxy cases

   112                 else print_app is_pseudo_fun some_thm vars fxy c_ts

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

   114     and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (arg_tys, _)), _)), ts)) =

   115       if is_cons c then

   116         let val k = length arg_tys in

   117           if k < 2 orelse length ts = k

   118           then (str o deresolve) c

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

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

   121         end

   122       else if is_pseudo_fun c

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

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

   125         @ map (print_term is_pseudo_fun some_thm vars BR) ts

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

   127       (print_term is_pseudo_fun) const_syntax some_thm vars

   128     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)

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

   130           let

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

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

   133               vars

   134               |> print_bind is_pseudo_fun some_thm NOBR pat

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

   136                     print_term is_pseudo_fun some_thm vars NOBR t])

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

   138           in

   139             Pretty.chunks [

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

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

   142               str "end"

   143             ]

   144           end

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

   146           let

   147             fun print_select delim (pat, body) =

   148               let

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

   150               in

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

   152               end;

   153           in

   154             brackets (

   155               str "case"

   156               :: print_term is_pseudo_fun some_thm vars NOBR t

   157               :: print_select "of" clause

   158               :: map (print_select "|") clauses

   159             )

   160           end

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

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

   163     fun print_val_decl print_typscheme (name, typscheme) = concat

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

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

   166       let

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

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

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

   170       in

   171         concat (

   172           str definer

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

   174           :: str "="

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

   176         )

   177       end;

   178     fun print_def is_pseudo_fun needs_typ definer

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

   180           let

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

   182               let

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

   184                 val vars = reserved

   185                   |> intro_base_names

   186                        (is_none o const_syntax) deresolve consts

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

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

   189                 val prolog = if needs_typ then

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

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

   192               in

   193                 concat (

   194                   prolog

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

   196                       else print_dict_args vs

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

   198                   @ str "="

   199                   @@ print_term is_pseudo_fun some_thm vars NOBR t

   200                 )

   201               end

   202             val shift = if null eqs then I else

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

   204           in pair

   205             (print_val_decl print_typscheme (name, vs_ty))

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

   207               print_eqn definer eq

   208               :: map (print_eqn "|") eqs

   209             ))

   210           end

   211       | print_def is_pseudo_fun _ definer

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

   213           let

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

   215               concat [

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

   217                 str "=",

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

   219               ];

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

   221               concat [

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

   223                 str "=",

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

   225               ];

   226           in pair

   227             (print_val_decl print_dicttypscheme

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

   229             (concat (

   230               str definer

   231               :: (str o deresolve) inst

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

   233                   else print_dict_args vs)

   234               @ str "="

   235               :: enum "," "{" "}"

   236                 (map print_super_instance super_instances

   237                   @ map print_classparam_instance classparam_instances)

   238               :: str ":"

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

   240             ))

   241           end;

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

   243           [print_val_decl print_typscheme (name, vs_ty)]

   244           ((semicolon o map str) (

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

   246             :: deresolve name

   247             :: replicate n "_"

   248             @ "="

   249             :: "raise"

   250             :: "Fail"

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

   252           ))

   253       | print_stmt (ML_Val binding) =

   254           let

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

   256           in pair

   257             [sig_p]

   258             (semicolon [p])

   259           end

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

   261           let

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

   263             fun print_pseudo_fun name = concat [

   264                 str "val",

   265                 (str o deresolve) name,

   266                 str "=",

   267                 (str o deresolve) name,

   268                 str "();"

   269               ];

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

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

   272             val pseudo_ps = map print_pseudo_fun pseudo_funs;

   273           in pair

   274             sig_ps

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

   276           end

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

   278           let

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

   280           in

   281             pair

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

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

   284           end

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

   286           let

   287             val sig_ps = print_datatype_decl "datatype" data

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

   289             val (ps, p) = split_last sig_ps;

   290           in pair

   291             sig_ps

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

   293           end

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

   295           let

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

   297             fun print_proj s p = semicolon

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

   299             fun print_super_class_decl (super_class, classrel) =

   300               print_val_decl print_dicttypscheme

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

   302             fun print_super_class_field (super_class, classrel) =

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

   304             fun print_super_class_proj (super_class, classrel) =

   305               print_proj (deresolve classrel)

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

   307             fun print_classparam_decl (classparam, ty) =

   308               print_val_decl print_typscheme

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

   310             fun print_classparam_field (classparam, ty) =

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

   312             fun print_classparam_proj (classparam, ty) =

   313               print_proj (deresolve classparam)

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

   315           in pair

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

   317               :: map print_super_class_decl super_classes

   318               @ map print_classparam_decl classparams)

   319             (Pretty.chunks (

   320               concat [

   321                 str ("type '" ^ v),

   322                 (str o deresolve) class,

   323                 str "=",

   324                 enum "," "{" "};" (

   325                   map print_super_class_field super_classes

   326                   @ map print_classparam_field classparams

   327                 )

   328               ]

   329               :: map print_super_class_proj super_classes

   330               @ map print_classparam_proj classparams

   331             ))

   332           end;

   333   in print_stmt end;

   335 fun print_sml_module name some_decls body =

   336   Pretty.chunks2 (

   337     Pretty.chunks (

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

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

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

   341     )

   342     :: body

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

   344   );

   346 val literals_sml = Literals {

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

   348   literal_string = quote o translate_string ML_Syntax.print_char,

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

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

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

   352   literal_naive_numeral = string_of_int,

   353   literal_list = enum "," "[" "]",

   354   infix_cons = (7, "::")

   355 };

   358 (** OCaml serializer **)

   360 fun print_ocaml_stmt tyco_syntax const_syntax reserved is_cons deresolve =

   361   let

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

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

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

   365       | print_tyco_expr fxy (tyco, tys) =

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

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

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

   369           | SOME (_, print) => print print_typ fxy tys)

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

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

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

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

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

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

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

   377     val print_classrels =

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

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

   380       print_plain_dict is_pseudo_fun fxy x

   381       |> print_classrels classrels

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

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

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

   385             else map_filter (print_dicts is_pseudo_fun BR) dss))

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

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

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

   389     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);

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

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

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

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

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

   395           str "_"

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

   397           str (lookup_var vars v)

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

   399           (case Code_Thingol.unfold_const_app t

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

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

   402                 print_term is_pseudo_fun some_thm vars BR t2])

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

   404           let

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

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

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

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

   409           (case Code_Thingol.unfold_const_app t0

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

   411                 then print_case is_pseudo_fun some_thm vars fxy cases

   412                 else print_app is_pseudo_fun some_thm vars fxy c_ts

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

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

   415       if is_cons c then

   416         let val k = length tys in

   417           if length ts = k

   418           then (str o deresolve) c

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

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

   421         end

   422       else if is_pseudo_fun c

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

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

   425         @ map (print_term is_pseudo_fun some_thm vars BR) ts

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

   427       (print_term is_pseudo_fun) const_syntax some_thm vars

   428     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)

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

   430           let

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

   432             fun print_let ((pat, _), t) vars =

   433               vars

   434               |> print_bind is_pseudo_fun some_thm NOBR pat

   435               |>> (fn p => concat

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

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

   438           in

   439             brackify_block fxy (Pretty.chunks ps) []

   440               (print_term is_pseudo_fun some_thm vars' NOBR body)

   441           end

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

   443           let

   444             fun print_select delim (pat, body) =

   445               let

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

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

   448           in

   449             brackets (

   450               str "match"

   451               :: print_term is_pseudo_fun some_thm vars NOBR t

   452               :: print_select "with" clause

   453               :: map (print_select "|") clauses

   454             )

   455           end

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

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

   458     fun print_val_decl print_typscheme (name, typscheme) = concat

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

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

   461       let

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

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

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

   465       in

   466         concat (

   467           str definer

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

   469           :: str "="

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

   471         )

   472       end;

   473     fun print_def is_pseudo_fun needs_typ definer

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

   475           let

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

   477               let

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

   479                 val vars = reserved

   480                   |> intro_base_names

   481                       (is_none o const_syntax) deresolve consts

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

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

   484               in concat [

   485                 (Pretty.block o commas)

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

   487                 str "->",

   488                 print_term is_pseudo_fun some_thm vars NOBR t

   489               ] end;

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

   491                   let

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

   493                     val vars = reserved

   494                       |> intro_base_names

   495                           (is_none o const_syntax) deresolve consts

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

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

   498                   in

   499                     concat (

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

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

   502                       @ str "="

   503                       @@ print_term is_pseudo_fun some_thm vars NOBR t

   504                     )

   505                   end

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

   507                   Pretty.block (

   508                     str "="

   509                     :: Pretty.brk 1

   510                     :: str "function"

   511                     :: Pretty.brk 1

   512                     :: print_eqn eq

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

   514                           o single o print_eqn) eqs

   515                   )

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

   517                   let

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

   519                     val vars = reserved

   520                       |> intro_base_names

   521                           (is_none o const_syntax) deresolve consts;

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

   523                   in

   524                     Pretty.block (

   525                       Pretty.breaks dummy_parms

   526                       @ Pretty.brk 1

   527                       :: str "="

   528                       :: Pretty.brk 1

   529                       :: str "match"

   530                       :: Pretty.brk 1

   531                       :: (Pretty.block o commas) dummy_parms

   532                       :: Pretty.brk 1

   533                       :: str "with"

   534                       :: Pretty.brk 1

   535                       :: print_eqn eq

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

   537                            o single o print_eqn) eqs'

   538                     )

   539                   end;

   540             val prolog = if needs_typ then

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

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

   543           in pair

   544             (print_val_decl print_typscheme (name, vs_ty))

   545             (concat (

   546               prolog

   547               :: print_dict_args vs

   548               @| print_eqns (is_pseudo_fun name) eqs

   549             ))

   550           end

   551       | print_def is_pseudo_fun _ definer

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

   553           let

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

   555               concat [

   556                 (str o deresolve) classrel,

   557                 str "=",

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

   559               ];

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

   561               concat [

   562                 (str o deresolve) classparam,

   563                 str "=",

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

   565               ];

   566           in pair

   567             (print_val_decl print_dicttypscheme

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

   569             (concat (

   570               str definer

   571               :: (str o deresolve) inst

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

   573                   else print_dict_args vs)

   574               @ str "="

   575               @@ brackets [

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

   577                   @ map print_classparam_instance classparam_instances),

   578                 str ":",

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

   580               ]

   581             ))

   582           end;

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

   584           [print_val_decl print_typscheme (name, vs_ty)]

   585           ((doublesemicolon o map str) (

   586             "let"

   587             :: deresolve name

   588             :: replicate n "_"

   589             @ "="

   590             :: "failwith"

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

   592           ))

   593       | print_stmt (ML_Val binding) =

   594           let

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

   596           in pair

   597             [sig_p]

   598             (doublesemicolon [p])

   599           end

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

   601           let

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

   603             fun print_pseudo_fun name = concat [

   604                 str "let",

   605                 (str o deresolve) name,

   606                 str "=",

   607                 (str o deresolve) name,

   608                 str "();;"

   609               ];

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

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

   612             val pseudo_ps = map print_pseudo_fun pseudo_funs;

   613           in pair

   614             sig_ps

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

   616           end

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

   618           let

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

   620           in

   621             pair

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

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

   624           end

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

   626           let

   627             val sig_ps = print_datatype_decl "type" data

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

   629             val (ps, p) = split_last sig_ps;

   630           in pair

   631             sig_ps

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

   633           end

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

   635           let

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

   637             fun print_super_class_field (super_class, classrel) =

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

   639             fun print_classparam_decl (classparam, ty) =

   640               print_val_decl print_typscheme

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

   642             fun print_classparam_field (classparam, ty) =

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

   644             val w = "_" ^ first_upper v;

   645             fun print_classparam_proj (classparam, _) =

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

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

   648             val type_decl_p = concat [

   649                 str ("type '" ^ v),

   650                 (str o deresolve) class,

   651                 str "=",

   652                 enum_default "unit" ";" "{" "}" (

   653                   map print_super_class_field super_classes

   654                   @ map print_classparam_field classparams

   655                 )

   656               ];

   657           in pair

   658             (type_decl_p :: map print_classparam_decl classparams)

   659             (Pretty.chunks (

   660               doublesemicolon [type_decl_p]

   661               :: map print_classparam_proj classparams

   662             ))

   663           end;

   664   in print_stmt end;

   666 fun print_ocaml_module name some_decls body =

   667   Pretty.chunks2 (

   668     Pretty.chunks (

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

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

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

   672     )

   673     :: body

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

   675   );

   677 val literals_ocaml = let

   678   fun chr i =

   679     let

   680       val xs = string_of_int i;

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

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

   683   fun char_ocaml c =

   684     let

   685       val i = ord c;

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

   687         then chr i else c

   688     in s end;

   689   fun numeral_ocaml k = if k < 0

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

   691     else if k <= 1073741823

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

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

   694 in Literals {

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

   696   literal_string = quote o translate_string char_ocaml,

   697   literal_numeral = numeral_ocaml,

   698   literal_positive_numeral = numeral_ocaml,

   699   literal_alternative_numeral = numeral_ocaml,

   700   literal_naive_numeral = numeral_ocaml,

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

   702   infix_cons = (6, "::")

   703 } end;

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

   709 fun ml_program_of_program labelled_name reserved module_alias program =

   710   let

   711     fun namify_const upper base (nsp_const, nsp_type) =

   712       let

   713         val (base', nsp_const') =

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

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

   716     fun namify_type base (nsp_const, nsp_type) =

   717       let

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

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

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

   721       | namify_stmt (Code_Thingol.Datatype _) = namify_type

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

   723       | namify_stmt (Code_Thingol.Class _) = namify_type

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

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

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

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

   728           let

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

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

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

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

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

   734                 | _ => (eqs, NONE)

   735               else (eqs, NONE)

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

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

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

   739       | ml_binding_of_stmt (name, _) =

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

   741     fun modify_fun (name, stmt) =

   742       let

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

   744         val ml_stmt = case binding

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

   746               ML_Exc (name, ((vs, ty),

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

   748           | _ => case some_value_name

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

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

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

   752       in SOME ml_stmt end;

   753     fun modify_funs stmts = single (SOME

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

   755     fun modify_datatypes stmts = single (SOME

   756       (ML_Datas (map_filter

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

   758     fun modify_class stmts = single (SOME

   759       (ML_Class (the_single (map_filter

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

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

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

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

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

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

   766           modify_datatypes stmts

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

   768           modify_datatypes stmts

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

   770           modify_class stmts

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

   772           modify_class stmts

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

   774           modify_class stmts

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

   776           [modify_fun stmt]

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

   778           modify_funs stmts

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

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

   781   in

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

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

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

   785   end;

   787 fun serialize_ml print_ml_module print_ml_stmt with_signatures

   788     { labelled_name, reserved_syms, includes, module_alias,

   789       class_syntax, tyco_syntax, const_syntax } program =

   790   let

   792     (* build program *)

   793     val { deresolver, hierarchical_program = ml_program } =

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

   796     (* print statements *)

   797     fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt

   798       tyco_syntax const_syntax (make_vars reserved_syms)

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

   800       |> apfst SOME;

   802     (* print modules *)

   803     fun print_module _ base _ xs =

   804       let

   805         val (raw_decls, body) = split_list xs;

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

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

   809     (* serialization *)

   810     val p = Pretty.chunks2 (map snd includes

   811       @ map snd (Code_Namespace.print_hierarchical {

   812         print_module = print_module, print_stmt = print_stmt,

   813         lift_markup = apsnd } ml_program));

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

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

   816   in

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

   818   end;

   820 val serializer_sml : Code_Target.serializer =

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

   822   >> (fn with_signatures => serialize_ml print_sml_module print_sml_stmt with_signatures));

   824 val serializer_ocaml : Code_Target.serializer =

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

   826   >> (fn with_signatures => serialize_ml print_ocaml_module print_ocaml_stmt with_signatures));

   829 (** Isar setup **)

   831 val setup =

   832   Code_Target.add_target

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

   834       check = { env_var = "ISABELLE_PROCESS",

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

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

   837   #> Code_Target.add_target

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

   839       check = { env_var = "ISABELLE_OCAML",

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

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

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

   843       brackify_infix (1, R) fxy (

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

   845         str "->",

   846         print_typ (INFX (1, R)) ty2

   847       )))

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

   849       brackify_infix (1, R) fxy (

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

   851         str "->",

   852         print_typ (INFX (1, R)) ty2

   853       )))

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

   855   #> fold (Code_Target.add_reserved target_SML)

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

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

   858   #> fold (Code_Target.add_reserved target_OCaml) [

   859       "and", "as", "assert", "begin", "class",

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

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

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

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

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

   865       "virtual", "when", "while", "with"

   866     ]

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

   869 end; (*struct*)

author	haftmann
	Thu, 19 Apr 2012 10:16:51 +0200
changeset 48447	b32aae03e3d6
parent 45880	99e1965f9c21
child 48472	b3dab1892cda
permissions	-rw-r--r--