src/Pure/Tools/codegen_serializer.ML

 
 fun eval_lrx L L = false
   | eval_lrx R R = false
   | eval_lrx _ _ = true;
 
-fun eval_fxy NOBR _ = false
-  | eval_fxy _ BR = true
-  | eval_fxy _ NOBR = false
+fun eval_fxy NOBR NOBR = false
+  | eval_fxy BR NOBR = false
+  | eval_fxy NOBR BR = false
   | eval_fxy (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) =
       pr < pr_ctxt
       orelse pr = pr_ctxt
         andalso eval_lrx lr lr_ctxt
-  | eval_fxy _ (INFX _) = false;
+  | eval_fxy _ (INFX _) = false
+  | eval_fxy _ _ = true;
 
 fun gen_brackify _ [p] = p
   | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps
   | gen_brackify false (ps as _::_) = Pretty.block ps;
 

   case const_syntax c
    of NONE => brackify fxy (mk_app' app)
     | SOME (i, pr) =>
         let
           val k = if i < 0 then (length o fst o CodegenThingol.unfold_fun) ty else i
-        in if k <= length ts
-          then case chop i ts of (ts1, ts2) =>
-            brackify fxy (pr fxy from_expr ts1 :: map (from_expr BR) ts2)
+        in if k = length ts
+          then 
+            pr fxy from_expr ts
+          else if k < length ts
+          then case chop k ts of (ts1, ts2) =>
+            brackify fxy (pr NOBR from_expr ts1 :: map (from_expr BR) ts2)
           else from_expr fxy (CodegenThingol.eta_expand app k)
         end;
 
 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
 

 
 fun mk_mixfix (fixity_this, mfx) =
   let
     fun is_arg (Arg _) = true
       | is_arg _ = false;
-    val i = (length o List.filter is_arg) mfx;
+    val i = (length o filter is_arg) mfx;
     fun fillin _ [] [] =
           []
       | fillin pr (Arg fxy :: mfx) (a :: args) =
           pr fxy a :: fillin pr mfx args
       | fillin pr (Pretty p :: mfx) args =

    of ((_, p as [_]), []) => mk_mixfix (NOBR, p)
     | ((b, p as _ :: _ :: _), []) => mk_mixfix (if b then NOBR else BR, p)
     | _ => Scan.!! (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
   end;
 
-(*FIXME: use Args.syntax ???*)
 fun parse_args f args =
   case f args
    of (x, []) => x
     | (_, _) => error "bad serializer arguments";
 

       | pretty _ _ _ = error "bad arguments for imperative monad bind";
   in (2, pretty) end;
 
 
 (* misc *)
-
-fun constructive_fun (name, (eqs, ty)) =
-  let
-    val is_cons = CodegenNames.has_nsp CodegenNames.nsp_dtco;
-    fun is_pat (IConst (c, _)) = is_cons c
-      | is_pat (IVar _) = true
-      | is_pat (t1 `$ t2) =
-          is_pat t1 andalso is_pat t2
-      | is_pat (INum _) = true
-      | is_pat (IChar _) = true
-      | is_pat _ = false;
-    fun check_eq (eq as (lhs, rhs)) =
-      if forall is_pat lhs
-      then SOME eq
-      else (warning ("In function " ^ quote name ^ ", throwing away one "
-        ^ "non-executable function clause"); NONE)
-  in case map_filter check_eq eqs
-   of [] => error ("In function " ^ quote name ^ ", no "
-        ^ "executable function clauses found")
-    | eqs => (name, (eqs, ty))
-  end;
 
 fun dest_name name =
   let
     val (names, name_base) = (split_last o NameSpace.explode) name;
     val (names_mod, name_shallow) = split_last names;

         | ps =>
             if (is_none o const_syntax) c then
               brackify fxy ((str o deresolv) c :: (ps @ map (pr_term vars BR) ts))
             else
               error ("Cannot apply user defined serialization for function expecting dictionaries: " ^ quote c)
-    fun eta_expand_poly_fun (funn as (_, (_::_, _))) =
-          funn
-      | eta_expand_poly_fun (funn as (_, ([_], ([], _)))) =
-          funn
-      | eta_expand_poly_fun (funn as (_, ([(_::_, _)], _))) =
-          funn
-      | eta_expand_poly_fun (funn as (_, ([(_, _ `|-> _)], _))) =
-          funn
-      | eta_expand_poly_fun (funn as (name, ([([], t)], tysm as (vs, ty)))) =
-          if (null o fst o CodegenThingol.unfold_fun) ty
-              orelse (not o null o filter_out (null o snd)) vs
-            then funn
-            else (name, ([([IVar "x"], t `$ IVar "x")], tysm));
-    fun pr_def (MLFuns raw_funns) =
-          let
-            val funns as (funn :: funns') = map (eta_expand_poly_fun o constructive_fun) raw_funns;
+    fun pr_def (MLFuns (funns as (funn :: funns'))) =
+          let
             val definer =
               let
                 fun mk [] [] = "val"
                   | mk (_::_) _ = "fun"
                   | mk [] vs = if (null o filter_out (null o snd)) vs then "val" else "fun";

                   str (deresolv co)
               | pr_co (co, tys) =
                   (Pretty.block o Pretty.breaks) [
                     str (deresolv co),
                     str "of",
-                    Pretty.enum " *" "" "" (map (pr_typ (INFX (2, L))) tys)
+                    Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
                   ];
             fun pr_data definer (tyco, (vs, cos)) =
               (Pretty.block o Pretty.breaks) (
                 str definer
                 :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)

       | eta_expand_poly_fun (funn as (name, ([([], t)], tysm as (vs, ty)))) =
           if (null o fst o CodegenThingol.unfold_fun) ty
               orelse (not o null o filter_out (null o snd)) vs
             then funn
             else (name, ([([IVar "x"], t `$ IVar "x")], tysm));
-    fun pr_def (MLFuns raw_funns) =
-          let
-            val funns as (funn :: funns') = map (eta_expand_poly_fun o constructive_fun) raw_funns;
+    fun pr_def (MLFuns (funns as (funn :: funns'))) =
+          let
             fun pr_funn definer (name, (eqs as eq::eqs', (raw_vs, ty))) =
               let
                 val vs = filter_out (null o snd) raw_vs;
                 val dummy_args = map_index (fn (i, _) => str ("x" ^ string_of_int i)) (fst eq);
                 fun pr_eq definer (ts, t) =

                   str (deresolv co)
               | pr_co (co, tys) =
                   (Pretty.block o Pretty.breaks) [
                     str (deresolv co),
                     str "of",
-                    Pretty.enum " *" "" "" (map (pr_typ (INFX (2, L))) tys)
+                    Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
                   ];
             fun pr_data definer (tyco, (vs, cos)) =
               (Pretty.block o Pretty.breaks) (
                 str definer
                 :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)

         |> map_nsp_yield modl' (mk defs)
         |-> (fn (base' :: bases', def') =>
            apsnd (map_node modl' (Graph.new_node (name, (Def (base', SOME def')))
               #> fold2 (fn name' => fn base' => Graph.new_node (name', (Def (base', NONE)))) names' bases')))
         |> apsnd (fold (fn defname => fold (add_dep defname) deps) defnames)
+        |> apsnd (fold (map_node modl' o Graph.add_edge) (product names names))
       end;
     fun group_defs [(_, CodegenThingol.Bot)] =
           I
       | group_defs ((defs as (_, CodegenThingol.Fun _)::_)) =
           add_group mk_funs defs

           end
     and pr_app' vars ((c, _), ts) =
       (str o deresolv) c :: map (pr_term vars BR) ts
     and pr_app vars fxy =
       mk_app (pr_app' vars) (pr_term vars) const_syntax fxy;
-    fun pr_def (name, CodegenThingol.Fun (funn as (eqs, (vs, ty)))) =
+    fun pr_def (name, CodegenThingol.Fun (eqs, (vs, ty))) =
           let
             val tyvars = CodegenThingol.intro_vars (map fst vs) keyword_vars;
             fun pr_eq (ts, t) =
               let
                 val consts = map_filter

               Pretty.block [
                 (str o suffix " ::" o deresolv_here) name,
                 Pretty.brk 1,
                 pr_typscheme tyvars (vs, ty)
               ]
-              :: (map pr_eq o fst o snd o constructive_fun) (name, funn)
+              :: map pr_eq eqs
             )
           end
       | pr_def (name, CodegenThingol.Datatype (vs, [(co, [ty])])) =
           let
             val tyvars = CodegenThingol.intro_vars (map fst vs) keyword_vars;