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 list * ((string * vname list) * itype list) list)) list

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

    42 fun print_product _ [] = NONE

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

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

    46 fun tuplify _ _ [] = NONE

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

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

    51 (** SML serializer **)

    53 fun print_sml_stmt tyco_syntax const_syntax reserved is_cons deresolve =

    54   let

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

    56       | print_tyco_expr (tyco, [ty]) =

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

    58       | print_tyco_expr (tyco, tys) =

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

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

    61          of NONE => print_tyco_expr (tyco, tys)

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

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

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

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

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

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

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

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

    70     fun print_classrels fxy [] ps = brackify fxy ps

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

    72       | print_classrels fxy classrels ps =

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

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

    75       print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)

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

    77           ((str o deresolve) inst ::

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

    79             else map_filter (print_dicts is_pseudo_fun BR) dss))

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

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

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

    83     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);

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

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

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

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

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

    89           str "_"

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

    91           str (lookup_var vars v)

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

    93           (case Code_Thingol.unfold_const_app t

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

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

    96                 print_term is_pseudo_fun some_thm vars BR t2])

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

    98           let

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

   100             fun print_abs (pat, ty) =

   101               print_bind is_pseudo_fun some_thm NOBR pat

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

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

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

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

   106           (case Code_Thingol.unfold_const_app t0

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

   108                 then print_case is_pseudo_fun some_thm vars fxy cases

   109                 else print_app is_pseudo_fun some_thm vars fxy c_ts

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

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

   112       if is_cons c then

   113         let val k = length arg_tys in

   114           if k < 2 orelse length ts = k

   115           then (str o deresolve) c

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

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

   118         end

   119       else if is_pseudo_fun c

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

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

   122         @ map (print_term is_pseudo_fun some_thm vars BR) ts

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

   124       (print_term is_pseudo_fun) const_syntax some_thm vars

   125     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)

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

   127           let

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

   129             fun print_match ((pat, _), t) vars =

   130               vars

   131               |> print_bind is_pseudo_fun some_thm NOBR pat

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

   133                     print_term is_pseudo_fun some_thm vars NOBR t])

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

   135           in

   136             Pretty.chunks [

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

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

   139               str "end"

   140             ]

   141           end

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

   143           let

   144             fun print_select delim (pat, body) =

   145               let

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

   147               in

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

   149               end;

   150           in

   151             brackets (

   152               str "case"

   153               :: print_term is_pseudo_fun some_thm vars NOBR t

   154               :: print_select "of" clause

   155               :: map (print_select "|") clauses

   156             )

   157           end

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

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

   160     fun print_val_decl print_typscheme (name, typscheme) = concat

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

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

   163       let

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

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

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

   167       in

   168         concat (

   169           str definer

   170           :: print_tyco_expr (tyco, map ITyVar vs)

   171           :: str "="

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

   173         )

   174       end;

   175     fun print_def is_pseudo_fun needs_typ definer

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

   177           let

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

   179               let

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

   181                 val vars = reserved

   182                   |> intro_base_names

   183                        (is_none o const_syntax) deresolve consts

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

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

   186                 val prolog = if needs_typ then

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

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

   189               in

   190                 concat (

   191                   prolog

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

   193                       else print_dict_args vs

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

   195                   @ str "="

   196                   @@ print_term is_pseudo_fun some_thm vars NOBR t

   197                 )

   198               end

   199             val shift = if null eqs then I else

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

   201           in pair

   202             (print_val_decl print_typscheme (name, vs_ty))

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

   204               print_eqn definer eq

   205               :: map (print_eqn "|") eqs

   206             ))

   207           end

   208       | print_def is_pseudo_fun _ definer

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

   210           let

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

   212               concat [

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

   214                 str "=",

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

   216               ];

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

   218               concat [

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

   220                 str "=",

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

   222               ];

   223           in pair

   224             (print_val_decl print_dicttypscheme

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

   226             (concat (

   227               str definer

   228               :: (str o deresolve) inst

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

   230                   else print_dict_args vs)

   231               @ str "="

   232               :: enum "," "{" "}"

   233                 (map print_super_instance super_instances

   234                   @ map print_classparam_instance classparam_instances)

   235               :: str ":"

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

   237             ))

   238           end;

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

   240           [print_val_decl print_typscheme (name, vs_ty)]

   241           ((semicolon o map str) (

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

   243             :: deresolve name

   244             :: replicate n "_"

   245             @ "="

   246             :: "raise"

   247             :: "Fail"

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

   249           ))

   250       | print_stmt (ML_Val binding) =

   251           let

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

   253           in pair

   254             [sig_p]

   255             (semicolon [p])

   256           end

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

   258           let

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

   260             fun print_pseudo_fun name = concat [

   261                 str "val",

   262                 (str o deresolve) name,

   263                 str "=",

   264                 (str o deresolve) name,

   265                 str "();"

   266               ];

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

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

   269             val pseudo_ps = map print_pseudo_fun pseudo_funs;

   270           in pair

   271             sig_ps

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

   273           end

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

   275           let

   276             val ty_p = print_tyco_expr (tyco, map ITyVar vs);

   277           in

   278             pair

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

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

   281           end

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

   283           let

   284             val sig_ps = print_datatype_decl "datatype" data

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

   286             val (ps, p) = split_last sig_ps;

   287           in pair

   288             sig_ps

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

   290           end

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

   292           let

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

   294             fun print_proj s p = semicolon

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

   296             fun print_super_class_decl (super_class, classrel) =

   297               print_val_decl print_dicttypscheme

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

   299             fun print_super_class_field (super_class, classrel) =

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

   301             fun print_super_class_proj (super_class, classrel) =

   302               print_proj (deresolve classrel)

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

   304             fun print_classparam_decl (classparam, ty) =

   305               print_val_decl print_typscheme

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

   307             fun print_classparam_field (classparam, ty) =

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

   309             fun print_classparam_proj (classparam, ty) =

   310               print_proj (deresolve classparam)

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

   312           in pair

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

   314               :: map print_super_class_decl super_classes

   315               @ map print_classparam_decl classparams)

   316             (Pretty.chunks (

   317               concat [

   318                 str ("type '" ^ v),

   319                 (str o deresolve) class,

   320                 str "=",

   321                 enum "," "{" "};" (

   322                   map print_super_class_field super_classes

   323                   @ map print_classparam_field classparams

   324                 )

   325               ]

   326               :: map print_super_class_proj super_classes

   327               @ map print_classparam_proj classparams

   328             ))

   329           end;

   330   in print_stmt end;

   332 fun print_sml_module name some_decls body =

   333   Pretty.chunks2 (

   334     Pretty.chunks (

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

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

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

   338     )

   339     :: body

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

   341   );

   343 val literals_sml = Literals {

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

   345   literal_string = quote o translate_string ML_Syntax.print_char,

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

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

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

   349   literal_naive_numeral = string_of_int,

   350   literal_list = enum "," "[" "]",

   351   infix_cons = (7, "::")

   352 };

   355 (** OCaml serializer **)

   357 fun print_ocaml_stmt tyco_syntax const_syntax reserved is_cons deresolve =

   358   let

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

   360       | print_tyco_expr (tyco, [ty]) =

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

   362       | print_tyco_expr (tyco, tys) =

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

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

   365          of NONE => print_tyco_expr (tyco, tys)

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

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

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

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

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

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

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

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

   374     val print_classrels =

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

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

   377       print_plain_dict is_pseudo_fun fxy x

   378       |> print_classrels classrels

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

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

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

   382             else map_filter (print_dicts is_pseudo_fun BR) dss))

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

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

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

   386     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);

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

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

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

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

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

   392           str "_"

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

   394           str (lookup_var vars v)

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

   396           (case Code_Thingol.unfold_const_app t

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

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

   399                 print_term is_pseudo_fun some_thm vars BR t2])

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

   401           let

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

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

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

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

   406           (case Code_Thingol.unfold_const_app t0

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

   408                 then print_case is_pseudo_fun some_thm vars fxy cases

   409                 else print_app is_pseudo_fun some_thm vars fxy c_ts

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

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

   412       if is_cons c then

   413         let val k = length tys in

   414           if length ts = k

   415           then (str o deresolve) c

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

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

   418         end

   419       else if is_pseudo_fun c

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

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

   422         @ map (print_term is_pseudo_fun some_thm vars BR) ts

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

   424       (print_term is_pseudo_fun) const_syntax some_thm vars

   425     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)

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

   427           let

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

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

   430               vars

   431               |> print_bind is_pseudo_fun some_thm NOBR pat

   432               |>> (fn p => concat

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

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

   435           in

   436             brackify_block fxy (Pretty.chunks ps) []

   437               (print_term is_pseudo_fun some_thm vars' NOBR body)

   438           end

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

   440           let

   441             fun print_select delim (pat, body) =

   442               let

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

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

   445           in

   446             brackets (

   447               str "match"

   448               :: print_term is_pseudo_fun some_thm vars NOBR t

   449               :: print_select "with" clause

   450               :: map (print_select "|") clauses

   451             )

   452           end

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

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

   455     fun print_val_decl print_typscheme (name, typscheme) = concat

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

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

   458       let

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

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

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

   462       in

   463         concat (

   464           str definer

   465           :: print_tyco_expr (tyco, map ITyVar vs)

   466           :: str "="

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

   468         )

   469       end;

   470     fun print_def is_pseudo_fun needs_typ definer

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

   472           let

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

   474               let

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

   476                 val vars = reserved

   477                   |> intro_base_names

   478                       (is_none o const_syntax) deresolve consts

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

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

   481               in concat [

   482                 (Pretty.block o commas)

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

   484                 str "->",

   485                 print_term is_pseudo_fun some_thm vars NOBR t

   486               ] end;

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

   488                   let

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

   490                     val vars = reserved

   491                       |> intro_base_names

   492                           (is_none o const_syntax) deresolve consts

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

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

   495                   in

   496                     concat (

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

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

   499                       @ str "="

   500                       @@ print_term is_pseudo_fun some_thm vars NOBR t

   501                     )

   502                   end

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

   504                   Pretty.block (

   505                     str "="

   506                     :: Pretty.brk 1

   507                     :: str "function"

   508                     :: Pretty.brk 1

   509                     :: print_eqn eq

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

   511                           o single o print_eqn) eqs

   512                   )

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

   514                   let

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

   516                     val vars = reserved

   517                       |> intro_base_names

   518                           (is_none o const_syntax) deresolve consts;

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

   520                   in

   521                     Pretty.block (

   522                       Pretty.breaks dummy_parms

   523                       @ Pretty.brk 1

   524                       :: str "="

   525                       :: Pretty.brk 1

   526                       :: str "match"

   527                       :: Pretty.brk 1

   528                       :: (Pretty.block o commas) dummy_parms

   529                       :: Pretty.brk 1

   530                       :: str "with"

   531                       :: Pretty.brk 1

   532                       :: print_eqn eq

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

   534                            o single o print_eqn) eqs'

   535                     )

   536                   end;

   537             val prolog = if needs_typ then

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

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

   540           in pair

   541             (print_val_decl print_typscheme (name, vs_ty))

   542             (concat (

   543               prolog

   544               :: print_dict_args vs

   545               @| print_eqns (is_pseudo_fun name) eqs

   546             ))

   547           end

   548       | print_def is_pseudo_fun _ definer

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

   550           let

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

   552               concat [

   553                 (str o deresolve) classrel,

   554                 str "=",

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

   556               ];

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

   558               concat [

   559                 (str o deresolve) classparam,

   560                 str "=",

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

   562               ];

   563           in pair

   564             (print_val_decl print_dicttypscheme

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

   566             (concat (

   567               str definer

   568               :: (str o deresolve) inst

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

   570                   else print_dict_args vs)

   571               @ str "="

   572               @@ brackets [

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

   574                   @ map print_classparam_instance classparam_instances),

   575                 str ":",

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

   577               ]

   578             ))

   579           end;

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

   581           [print_val_decl print_typscheme (name, vs_ty)]

   582           ((doublesemicolon o map str) (

   583             "let"

   584             :: deresolve name

   585             :: replicate n "_"

   586             @ "="

   587             :: "failwith"

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

   589           ))

   590       | print_stmt (ML_Val binding) =

   591           let

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

   593           in pair

   594             [sig_p]

   595             (doublesemicolon [p])

   596           end

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

   598           let

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

   600             fun print_pseudo_fun name = concat [

   601                 str "let",

   602                 (str o deresolve) name,

   603                 str "=",

   604                 (str o deresolve) name,

   605                 str "();;"

   606               ];

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

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

   609             val pseudo_ps = map print_pseudo_fun pseudo_funs;

   610           in pair

   611             sig_ps

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

   613           end

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

   615           let

   616             val ty_p = print_tyco_expr (tyco, map ITyVar vs);

   617           in

   618             pair

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

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

   621           end

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

   623           let

   624             val sig_ps = print_datatype_decl "type" data

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

   626             val (ps, p) = split_last sig_ps;

   627           in pair

   628             sig_ps

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

   630           end

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

   632           let

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

   634             fun print_super_class_field (super_class, classrel) =

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

   636             fun print_classparam_decl (classparam, ty) =

   637               print_val_decl print_typscheme

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

   639             fun print_classparam_field (classparam, ty) =

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

   641             val w = "_" ^ first_upper v;

   642             fun print_classparam_proj (classparam, _) =

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

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

   645             val type_decl_p = concat [

   646                 str ("type '" ^ v),

   647                 (str o deresolve) class,

   648                 str "=",

   649                 enum_default "unit" ";" "{" "}" (

   650                   map print_super_class_field super_classes

   651                   @ map print_classparam_field classparams

   652                 )

   653               ];

   654           in pair

   655             (type_decl_p :: map print_classparam_decl classparams)

   656             (Pretty.chunks (

   657               doublesemicolon [type_decl_p]

   658               :: map print_classparam_proj classparams

   659             ))

   660           end;

   661   in print_stmt end;

   663 fun print_ocaml_module name some_decls body =

   664   Pretty.chunks2 (

   665     Pretty.chunks (

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

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

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

   669     )

   670     :: body

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

   672   );

   674 val literals_ocaml = let

   675   fun chr i =

   676     let

   677       val xs = string_of_int i;

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

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

   680   fun char_ocaml c =

   681     let

   682       val i = ord c;

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

   684         then chr i else c

   685     in s end;

   686   fun numeral_ocaml k = if k < 0

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

   688     else if k <= 1073741823

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

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

   691 in Literals {

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

   693   literal_string = quote o translate_string char_ocaml,

   694   literal_numeral = numeral_ocaml,

   695   literal_positive_numeral = numeral_ocaml,

   696   literal_alternative_numeral = numeral_ocaml,

   697   literal_naive_numeral = numeral_ocaml,

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

   699   infix_cons = (6, "::")

   700 } end;

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

   706 fun ml_program_of_program labelled_name reserved module_alias program =

   707   let

   708     fun namify_const upper base (nsp_const, nsp_type) =

   709       let

   710         val (base', nsp_const') =

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

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

   713     fun namify_type base (nsp_const, nsp_type) =

   714       let

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

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

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

   718       | namify_stmt (Code_Thingol.Datatype _) = namify_type

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

   720       | namify_stmt (Code_Thingol.Class _) = namify_type

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

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

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

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

   725           let

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

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

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

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

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

   731                 | _ => (eqs, NONE)

   732               else (eqs, NONE)

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

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

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

   736       | ml_binding_of_stmt (name, _) =

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

   738     fun modify_fun (name, stmt) =

   739       let

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

   741         val ml_stmt = case binding

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

   743               ML_Exc (name, ((vs, ty),

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

   745           | _ => case some_value_name

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

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

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

   749       in SOME ml_stmt end;

   750     fun modify_funs stmts = single (SOME

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

   752     fun modify_datatypes stmts = single (SOME

   753       (ML_Datas (map_filter

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

   755     fun modify_class stmts = single (SOME

   756       (ML_Class (the_single (map_filter

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

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

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

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

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

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

   763           modify_datatypes stmts

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

   765           modify_datatypes stmts

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

   767           modify_class stmts

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

   769           modify_class stmts

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

   771           modify_class stmts

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

   773           [modify_fun stmt]

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

   775           modify_funs stmts

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

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

   778   in

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

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

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

   782   end;

   784 fun serialize_ml print_ml_module print_ml_stmt with_signatures

   785     { labelled_name, reserved_syms, includes, module_alias,

   786       class_syntax, tyco_syntax, const_syntax } program =

   787   let

   789     (* build program *)

   790     val { deresolver, hierarchical_program = ml_program } =

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

   793     (* print statements *)

   794     fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt

   795       tyco_syntax const_syntax (make_vars reserved_syms)

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

   797       |> apfst SOME;

   799     (* print modules *)

   800     fun print_module _ base _ xs =

   801       let

   802         val (raw_decls, body) = split_list xs;

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

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

   806     (* serialization *)

   807     val p = Pretty.chunks2 (map snd includes

   808       @ map snd (Code_Namespace.print_hierarchical {

   809         print_module = print_module, print_stmt = print_stmt,

   810         lift_markup = apsnd } ml_program));

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

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

   813   in

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

   815   end;

   817 val serializer_sml : Code_Target.serializer =

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

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

   821 val serializer_ocaml : Code_Target.serializer =

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

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

   826 (** Isar setup **)

   828 val setup =

   829   Code_Target.add_target

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

   831       check = { env_var = "ISABELLE_PROCESS",

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

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

   834   #> Code_Target.add_target

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

   836       check = { env_var = "ISABELLE_OCAML",

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

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

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

   840       brackify_infix (1, R) fxy (

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

   842         str "->",

   843         print_typ (INFX (1, R)) ty2

   844       )))

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

   846       brackify_infix (1, R) fxy (

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

   848         str "->",

   849         print_typ (INFX (1, R)) ty2

   850       )))

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

   852   #> fold (Code_Target.add_reserved target_SML)

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

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

   855   #> fold (Code_Target.add_reserved target_OCaml) [

   856       "and", "as", "assert", "begin", "class",

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

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

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

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

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

   862       "virtual", "when", "while", "with"

   863     ]

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

   866 end; (*struct*)

author	haftmann
	Mon, 28 May 2012 13:38:07 +0200
changeset 49018	1d11af40b106
parent 48472	b3dab1892cda
child 49087	ace701efe203
permissions	-rw-r--r--