src/Pure/Tools/codegen_serializer.ML

 target languages (like ML or Haskell).
 *)
 
 signature CODEGEN_SERIALIZER =
 sig
+  include BASIC_CODEGEN_THINGOL;
   type 'a pretty_syntax;
   type serializer =
       string list list
       -> OuterParse.token list ->
       ((string -> (string * (string -> string option)) option)

     -> ((string -> string) * (string -> string)) option
     -> int * string -> CodegenThingol.iterm pretty_syntax;
   val pretty_ml_string: string -> string -> (string -> string) -> (string -> string)
     -> string -> CodegenThingol.iterm pretty_syntax;
   val serializers: {
-    ml: string * (string -> serializer),
-    haskell: string * (string * string list -> serializer)
+    SML: string * (string -> serializer),
+    Haskell: string * (string * string list -> serializer)
   };
   val mk_flat_ml_resolver: string list -> string -> string;
   val eval_term: string -> string -> string list list
     -> (string -> CodegenThingol.itype pretty_syntax option)
           * (string -> CodegenThingol.iterm pretty_syntax option)

   val eval_verbose: bool ref;
   val ml_fun_datatype: string
     -> ((string -> CodegenThingol.itype pretty_syntax option)
         * (string -> CodegenThingol.iterm pretty_syntax option))
     -> (string -> string)
-    -> ((string * CodegenThingol.funn) list -> Pretty.T)
-        * ((string * CodegenThingol.datatyp) list -> Pretty.T);
+    -> ((string * ((iterm list * iterm) list * CodegenThingol.typscheme)) list -> Pretty.T)
+        * ((string * ((vname * sort) list * (string * itype list) list)) list -> Pretty.T);
 end;
 
 structure CodegenSerializer: CODEGEN_SERIALIZER =
 struct
 

       case parse_mixfix reader s ctxt
        of ([Pretty _], _) =>
             error ("Mixfix contains just one pretty element; either declare as "
               ^ quote atomK ^ " or consider adding a break")
         | x => x;
-    val parse = OuterParse.$$$ "(" |-- (
+    val parse = (
            OuterParse.$$$ infixK  |-- OuterParse.nat
             >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X)))
         || OuterParse.$$$ infixlK |-- OuterParse.nat
             >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L)))
         || OuterParse.$$$ infixrK |-- OuterParse.nat
             >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R)))
         || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR)
         || pair (parse_nonatomic, BR)
-      ) -- OuterParse.string --| OuterParse.$$$ ")" >> (fn ((p, fxy), s) => (p s, fxy));
+      ) -- OuterParse.string >> (fn ((p, fxy), s) => (p s, fxy));
     fun mk fixity mfx ctxt =
       let
         val i = (length o List.filter is_arg) mfx;
         val _ = if i > num_args ctxt then error "Too many arguments in codegen syntax" else ();
       in (((i, i), fillin_mixfix fixity mfx), ctxt) end;

                of [class] => mk_class class
                 | _ => Pretty.enum " *" "" "" (map mk_class sort),
             str ")"
             ]
           end;
-    fun ml_from_sortlookup fxy lss =
+    fun ml_from_insts fxy lss =
       let
         fun from_label l =
           Pretty.block [str "#",
             if (is_some o Int.fromString) l then str l
             else ml_from_label l

           | from_lookup fxy ls p =
               brackify fxy [
                 Pretty.enum " o" "(" ")" (map from_label ls),
                 p
               ];
-        fun from_classlookup fxy (Instance (inst, lss)) =
+        fun from_inst fxy (Instance (inst, lss)) =
               brackify fxy (
                 (str o resolv) inst
-                :: map (ml_from_sortlookup BR) lss
+                :: map (ml_from_insts BR) lss
               )
-          | from_classlookup fxy (Lookup (classes, (v, ~1))) =
+          | from_inst fxy (Context (classes, (v, ~1))) =
               from_lookup BR classes
                 ((str o ml_from_dictvar) v)
-          | from_classlookup fxy (Lookup (classes, (v, i))) =
+          | from_inst fxy (Context (classes, (v, i))) =
               from_lookup BR (string_of_int (i+1) :: classes)
                 ((str o ml_from_dictvar) v)
       in case lss
        of [] => str "()"
-        | [ls] => from_classlookup fxy ls
-        | lss => (Pretty.list "(" ")" o map (from_classlookup NOBR)) lss
+        | [ls] => from_inst fxy ls
+        | lss => (Pretty.list "(" ")" o map (from_inst NOBR)) lss
       end;
     fun ml_from_tycoexpr fxy (tyco, tys) =
       let
         val tyco' = (str o resolv) tyco
       in case map (ml_from_type BR) tys

       if is_cons f andalso length es > 1 then
         [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
       else
         (str o resolv) f :: map (ml_from_expr BR) es
     and ml_from_app fxy (app_expr as ((c, (lss, ty)), es)) =
-      case map (ml_from_sortlookup BR) lss
+      case (map (ml_from_insts BR) o filter_out null) lss
        of [] =>
             from_app ml_mk_app ml_from_expr const_syntax fxy app_expr
         | lss =>
-            brackify fxy (
-              (str o resolv) c
-              :: (lss
-              @ map (ml_from_expr BR) es)
-            );
-  in (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) end;
+            if (is_none o const_syntax) c then
+              brackify fxy (
+                (str o resolv) c
+                :: (lss
+                @ map (ml_from_expr BR) es)
+              )
+            else error ("Can't apply user defined serilization for function expecting dicitonaries: " ^ quote c)
+  in (ml_from_label, ml_from_tyvar, ml_from_insts, ml_from_tycoexpr, ml_from_type, ml_from_expr) end;
 
 fun ml_fun_datatyp is_cons (tyco_syntax, const_syntax) resolv =
   let
-    val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
+    val (ml_from_label, ml_from_tyvar, ml_from_insts, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
       ml_expr_seri is_cons (tyco_syntax, const_syntax) resolv;
     fun chunk_defs ps =
       let
         val (p_init, p_last) = split_last ps
       in
         Pretty.chunks (p_init @ [Pretty.block ([p_last, str ";"])])
       end;
     fun eta_expand_poly_fun (funn as (_, (_::_, _))) =
           funn
-      | eta_expand_poly_fun (funn as (eqs, sctxt_ty as (_, ty))) =
+      | eta_expand_poly_fun (funn as (eqs, tysm as (_, ty))) =
           let
             fun no_eta (_::_, _) = I
               | no_eta (_, _ `|-> _) = I
               | no_eta ([], e) = K false;
             fun has_tyvars (_ `%% tys) =

                   has_tyvars ty1 orelse has_tyvars ty2;
           in if (null o fst o CodegenThingol.unfold_fun) ty
               orelse (not o has_tyvars) ty
               orelse fold no_eta eqs true
             then funn
-            else (map (fn ([], rhs) => ([IVar "x"], rhs `$ IVar "x")) eqs, sctxt_ty)
+            else (map (fn ([], rhs) => ([IVar "x"], rhs `$ IVar "x")) eqs, tysm)
           end;
     fun ml_from_funs (defs as def::defs_tl) =
       let
         fun mk_definer [] [] = "val"
-          | mk_definer _ _ = "fun";
-        fun check_args (_, ((pats, _)::_, (sortctxt, _))) NONE =
-              SOME (mk_definer pats sortctxt)
-          | check_args (_, ((pats, _)::_, (sortctxt, _))) (SOME definer) =
-              if mk_definer pats sortctxt = definer
+          | mk_definer (_::_) _ = "fun"
+          | mk_definer [] vs = if (null o filter_out (null o snd)) vs then "val" else "fun";
+        fun check_args (_, ((pats, _)::_, (vs, _))) NONE =
+              SOME (mk_definer pats vs)
+          | check_args (_, ((pats, _)::_, (vs, _))) (SOME definer) =
+              if mk_definer pats vs = definer
               then SOME definer
               else error ("Mixing simultaneous vals and funs not implemented");
-        fun mk_fun definer (name, (eqs as eq::eq_tl, (sortctxt, ty))) =
-          let
+        fun mk_fun definer (name, (eqs as eq::eq_tl, (raw_vs, ty))) =
+          let
+            val vs = filter_out (null o snd) raw_vs;
             val shift = if null eq_tl then I else
               map (Pretty.block o single o Pretty.block o single);
-            fun mk_arg e ty =
-              ml_from_expr BR e
             fun mk_eq definer (pats, expr) =
               (Pretty.block o Pretty.breaks) (
                 [str definer, (str o resolv) name]
-                @ (if null pats andalso null sortctxt
+                @ (if null pats andalso null vs
+                     andalso not (ty = ITyVar "_")(*for evaluation*)
                    then [str ":", ml_from_type NOBR ty]
                    else
-                     map ml_from_tyvar sortctxt
-                     @ map2 mk_arg pats
-                         ((curry Library.take (length pats) o fst o CodegenThingol.unfold_fun) ty))
+                     map ml_from_tyvar vs
+                     @ map (ml_from_expr BR) pats)
              @ [str "=", ml_from_expr NOBR expr]
               )
           in
             (Pretty.block o Pretty.fbreaks o shift) (
               mk_eq definer eq

 
 fun ml_from_defs is_cons
     (_, tyco_syntax, const_syntax) resolver prefix defs =
   let
     val resolv = resolver prefix;
-    val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
+    val (ml_from_label, ml_from_tyvar, ml_from_insts, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
       ml_expr_seri is_cons (tyco_syntax, const_syntax) resolv;
     val (ml_from_funs, ml_from_datatypes) =
       ml_fun_datatyp is_cons (tyco_syntax, const_syntax) resolv;
     val filter_datatype =
       map_filter

             Pretty.brk 1,
             str ("'" ^ v),
             Pretty.brk 1,
             (str o resolv) class
           ];
-        fun from_membr (m, (_, ty)) =
+        fun from_membr (m, ty) =
           Pretty.block [
             ml_from_label m,
             str ":",
             Pretty.brk 1,
             ml_from_type NOBR ty

             val definer = if null arity then "val" else "fun"
             fun from_supclass (supclass, ls) =
               (Pretty.block o Pretty.breaks) [
                 ml_from_label supclass,
                 str "=",
-                ml_from_sortlookup NOBR ls
+                ml_from_insts NOBR ls
               ];
             fun from_memdef (m, e) =
               (Pretty.block o Pretty.breaks) [
                 ml_from_label m,
                 str "=",

     val serializer = ml_serializer struct_name "ml" nsp_dtcon nspgrp
       (fn "" => (fn p => (use_text Context.ml_output (!eval_verbose) (output p); NONE))
         | _ => SOME) (K NONE, syntax_tyco, syntax_const) (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]);
     val _ = serializer modl';
     val val_name_struct = NameSpace.append struct_name val_name;
-    val _ = use_text Context.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ "())");
+    val _ = use_text Context.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ ")");
     val value = ! reff;
   in value end;
 
 fun mk_flat_ml_resolver names =
   let

     fun hs_from_classop_name cls clsop = case class_syntax cls
      of NONE => NameSpace.base clsop
       | SOME (_, classop_syntax) => case classop_syntax clsop
          of NONE => NameSpace.base clsop
           | SOME clsop => clsop;
-    fun hs_from_sctxt vs =
+    fun hs_from_typparms vs =
       let
-        fun from_sctxt [] = str ""
-          | from_sctxt vs =
+        fun from_typparms [] = str ""
+          | from_typparms vs =
               vs
               |> map (fn (v, cls) => str (hs_from_class cls ^ " " ^ v))
               |> Pretty.enum "," "(" ")"
               |> (fn p => Pretty.block [p, str " => "])
       in
         vs
         |> map (fn (v, sort) => map (pair v) sort)
         |> flat
-        |> from_sctxt
+        |> from_typparms
       end;
     fun hs_from_tycoexpr fxy (tyco, tys) =
       brackify fxy (str tyco :: map (hs_from_type BR) tys)
     and hs_from_type fxy (tycoexpr as tyco `%% tys) =
           (case tyco_syntax tyco

             str "->",
             hs_from_type (INFX (1, R)) t2
           ]
       | hs_from_type fxy (ITyVar v) =
           str v;
-    fun hs_from_sctxt_tycoexpr (sctxt, tycoexpr) =
-      Pretty.block [hs_from_sctxt sctxt, hs_from_tycoexpr NOBR tycoexpr]
-    fun hs_from_sctxt_type (sctxt, ty) =
-      Pretty.block [hs_from_sctxt sctxt, hs_from_type NOBR ty]
+    fun hs_from_typparms_tycoexpr (vs, tycoexpr) =
+      Pretty.block [hs_from_typparms vs, hs_from_tycoexpr NOBR tycoexpr]
+    fun hs_from_typparms_type (vs, ty) =
+      Pretty.block [hs_from_typparms vs, hs_from_type NOBR ty]
     fun hs_from_expr fxy (e as IConst x) =
           hs_from_app fxy (x, [])
       | hs_from_expr fxy (e as (e1 `$ e2)) =
           (case CodegenThingol.unfold_const_app e
            of SOME x => hs_from_app fxy x

             str ("="),
             Pretty.brk 1,
             hs_from_expr NOBR rhs
           ]
       in Pretty.chunks ((map from_eq o fst o snd o constructive_fun is_cons) def) end;
-    fun hs_from_def (name, CodegenThingol.Fun (def as (_, (sctxt, ty)))) =
+    fun hs_from_def (name, CodegenThingol.Fun (def as (_, (vs, ty)))) =
           let
             val body = hs_from_funeqs (name, def);
           in if with_typs then
             Pretty.chunks [
               Pretty.block [
                 (str o suffix " ::" o resolv_here) name,
                 Pretty.brk 1,
-                hs_from_sctxt_type (sctxt, ty)
+                hs_from_typparms_type (vs, ty)
               ],
               body
             ] |> SOME
           else SOME body end
-      | hs_from_def (name, CodegenThingol.Typesyn (sctxt, ty)) =
+      | hs_from_def (name, CodegenThingol.Typesyn (vs, ty)) =
           (Pretty.block o Pretty.breaks) [
             str "type",
-            hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt)),
+            hs_from_typparms_tycoexpr (vs, (resolv_here name, map (ITyVar o fst) vs)),
             str "=",
-            hs_from_sctxt_type ([], ty)
+            hs_from_typparms_type ([], ty)
           ] |> SOME
-      | hs_from_def (name, CodegenThingol.Datatype (sctxt, [(co, [ty])])) =
+      | hs_from_def (name, CodegenThingol.Datatype (vs, [(co, [ty])])) =
           (Pretty.block o Pretty.breaks) [
             str "newtype",
-            hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt)),
+            hs_from_typparms_tycoexpr (vs, (resolv_here name, map (ITyVar o fst) vs)),
             str "=",
             (str o resolv_here) co,
             hs_from_type BR ty
           ] |> SOME
-      | hs_from_def (name, CodegenThingol.Datatype (sctxt, constrs)) =
+      | hs_from_def (name, CodegenThingol.Datatype (vs, constrs)) =
           let
             fun mk_cons (co, tys) =
               (Pretty.block o Pretty.breaks) (
                 (str o resolv_here) co
                 :: map (hs_from_type BR) tys
               )
           in
             (Pretty.block o Pretty.breaks) [
               str "data",
-              hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt)),
+              hs_from_typparms_tycoexpr (vs, (resolv_here name, map (ITyVar o fst) vs)),
               str "=",
               Pretty.block (separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs))
             ]
           end |> SOME
       | hs_from_def (_, CodegenThingol.Datatypecons _) =
           NONE
       | hs_from_def (name, CodegenThingol.Class (supclasss, (v, membrs))) =
           let
-            fun mk_member (m, (sctxt, ty)) =
+            fun mk_member (m, ty) =
               Pretty.block [
                 str (resolv_here m ^ " ::"),
                 Pretty.brk 1,
-                hs_from_sctxt_type (sctxt, ty)
+                hs_from_type NOBR ty
               ]
           in
             Pretty.block [
               str "class ",
-              hs_from_sctxt [(v, supclasss)],
+              hs_from_typparms [(v, supclasss)],
               str (resolv_here name ^ " " ^ v),
               str " where",
               Pretty.fbrk,
               Pretty.chunks (map mk_member membrs)
             ] |> SOME

       | hs_from_def (_, CodegenThingol.Classmember _) =
           NONE
       | hs_from_def (_, CodegenThingol.Classinst ((clsname, (tyco, arity)), (_, memdefs))) =
           Pretty.block [
             str "instance ",
-            hs_from_sctxt arity,
+            hs_from_typparms arity,
             str (hs_from_class clsname ^ " "),
             hs_from_type BR (tyco `%% map (ITyVar o fst) arity),
             str " where",
             Pretty.fbrk,
             Pretty.chunks (map (fn (m, e) =>

 
 val serializers =
   let
     fun seri s f = (s, f s);
   in {
-    ml = seri "ml" ml_from_thingol,
-    haskell = seri "haskell" hs_from_thingol
+    SML = seri "SML" ml_from_thingol,
+    Haskell = seri "Haskell" hs_from_thingol
   } end;
 
 end; (* struct *)