src/Tools/nbe.ML

 (** assembling and compiling ML code from terms **)
 
 (* abstract ML syntax *)
 
 infix 9 `$` `$$`;
-fun e1 `$` e2 = "(" ^ e1 ^ " " ^ e2 ^ ")";
+infix 8 `*`;
+fun e1 `$` e2 = enclose "(" ")" (e1 ^ " " ^ e2);
 fun e `$$` [] = e
-  | e `$$` es = "(" ^ e ^ " " ^ implode_space es ^ ")";
-fun ml_abs v e = "(fn " ^ v ^ " => " ^ e ^ ")";
-
-fun ml_cases t cs =
-  "(case " ^ t ^ " of " ^ space_implode " | " (map (fn (p, t) => p ^ " => " ^ t) cs) ^ ")";
+  | e `$$` es = enclose "(" ")" (e ^ " " ^ implode_space es);
+fun ml_abs v e = enclose "(" ")" ("fn " ^ v ^ " => " ^ e);
+
+fun ml_cases e cs = enclose "(" ")"
+  ("case " ^ e ^ " of " ^ space_implode " | " (map (fn (p, e) => p ^ " => " ^ e) cs));
 fun ml_Let d e = "let\n" ^ d ^ " in " ^ e ^ " end";
-fun ml_as v t = "(" ^ v ^ " as " ^ t ^ ")";
+fun ml_as v t = enclose "(" ")" (v ^ " as " ^ t);
 
 fun ml_and [] = "true"
-  | ml_and [x] = x
-  | ml_and xs = "(" ^ space_implode " andalso " xs ^ ")";
-fun ml_if b x y = "(if " ^ b ^ " then " ^ x ^ " else " ^ y ^ ")";
-
-fun ml_list es = "[" ^ commas es ^ "]";
+  | ml_and [e] = e
+  | ml_and es = enclose "(" ")" (space_implode " andalso " es);
+fun ml_if b e1 e2 = enclose "(" ")" ("if" ^ b ^ " then " ^ e1 ^ " else " ^ e2);
+
+fun e1 `*` e2 = enclose "(" ")" (e1 ^ ", " ^ e2);
+fun ml_list es = enclose "[" "]" (commas es);
 
 fun ml_fundefs ([(name, [([], e)])]) =
       "val " ^ name ^ " = " ^ e ^ "\n"
   | ml_fundefs (eqs :: eqss) =
       let

   val name_same = prefix ^ "same";
 in
 
 val univs_cookie = (get_result, put_result, name_put);
 
-fun nbe_type n ts = name_type `$` ("(" ^ quote n ^ ", " ^ ml_list ts ^ ")")
 fun nbe_tparam v = "t_" ^ v;
 fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
 fun nbe_bound v = "v_" ^ v;
 fun nbe_bound_optional NONE = "_"
   | nbe_bound_optional (SOME v) = nbe_bound v;
 fun nbe_default v = "w_" ^ v;
+fun nbe_type n ts = name_type `$` (quote n `*` ml_list ts);
+fun nbe_fun c tys = c `$` ml_list tys;
 
 (*note: these three are the "turning spots" where proper argument order is established!*)
 fun nbe_apps t [] = t
   | nbe_apps t ts = name_apps `$$` [t, ml_list (rev ts)];
-fun nbe_apps_local c tys ts = c `$` ml_list tys `$` ml_list (rev ts);
-fun nbe_apps_constr c tys ts = name_const `$` ("((" ^ c ^ ", " ^ ml_list tys ^ "), " ^ ml_list (rev ts) ^ ")");
-fun nbe_apps_constmatch c ts = name_const `$` ("((" ^ c ^ ", _), " ^ ml_list (rev ts) ^ ")");
+fun nbe_apps_fun c tys ts = nbe_fun c tys `$` ml_list (rev ts);
+fun nbe_apps_constr c tys ts = name_const `$` ((c `*` ml_list tys) `*` ml_list (rev ts));
+fun nbe_apps_constmatch c ts = name_const `$` ((c `*` "_") `*` ml_list (rev ts));
 
 fun nbe_abss 0 f = f `$` ml_list []
   | nbe_abss n f = name_abss `$$` [string_of_int n, f];
 
-fun nbe_same (v1, v2) = "(" ^ name_same ^ " (" ^ nbe_bound v1 ^ ", " ^ nbe_bound v2 ^ "))";
+fun nbe_same (v1, v2) = enclose "(" ")" (name_same `$` (nbe_bound v1 `*` nbe_bound v2));
 
 end;
 
 open Basic_Code_Symbol;
 open Basic_Code_Thingol;

 fun assemble_preprocessed_eqnss ctxt idx_of_const deps eqnss =
   let
     fun fun_ident 0 (Code_Symbol.Constant "") = "nbe_value" 
       | fun_ident i sym = "c_" ^ string_of_int (idx_of_const sym)
           ^ "_" ^ Code_Symbol.default_base sym ^ "_" ^ string_of_int i;
-    fun constr_fun_ident c =
+    fun constr_ident c =
       if Config.get ctxt trace
       then string_of_int (idx_of_const c) ^ " (*" ^ Code_Symbol.default_base c ^ "*)"
       else string_of_int (idx_of_const c);
 
-    fun apply_local i sym = nbe_apps_local (fun_ident i sym);
-    fun apply_constr sym = nbe_apps_constr (constr_fun_ident sym);
-    fun apply_constmatch sym = nbe_apps_constmatch (constr_fun_ident sym);
+    fun assemble_fun i sym = nbe_fun (fun_ident i sym);
+    fun assemble_app_fun i sym = nbe_apps_fun (fun_ident i sym);
+    fun assemble_app_constr sym = nbe_apps_constr (constr_ident sym);
+    fun assemble_app_constmatch sym = nbe_apps_constmatch (constr_ident sym);
 
     fun assemble_constapp sym tys dictss ts =
       let
         val s_tys = map (assemble_type) tys;
         val ts' = (maps o map) assemble_dict (map2 (fn ty => map (fn dict => (ty, dict))) tys dictss) @ ts;
       in case AList.lookup (op =) eqnss sym
        of SOME (num_args, _) => if num_args <= length ts'
             then let val (ts1, ts2) = chop num_args ts'
-            in nbe_apps (apply_local 0 sym s_tys ts1) ts2
-            end else nbe_apps (nbe_abss num_args (fun_ident 0 sym `$` ml_list s_tys)) ts'
+            in nbe_apps (assemble_app_fun 0 sym s_tys ts1) ts2
+            end else nbe_apps (nbe_abss num_args (assemble_fun 0 sym s_tys)) ts'
         | NONE => if member (op =) deps sym
-            then nbe_apps (fun_ident 0 sym `$` ml_list s_tys) ts'
-            else apply_constr sym s_tys ts'
+            then nbe_apps (assemble_fun 0 sym s_tys) ts'
+            else assemble_app_constr sym s_tys ts'
       end
     and assemble_classrels classrels =
       fold_rev (fn classrel => assemble_constapp (Class_Relation classrel) [] [] o single) classrels
     and assemble_dict (ty, Dict (classrels, x)) =
           assemble_classrels classrels (assemble_plain_dict ty x)

           assemble_constapp (Class_Instance inst) tys (map snd dictss) []
       | assemble_plain_dict _ (Dict_Var { var, index, ... }) =
           nbe_dict var index
 
     fun assemble_constmatch sym _ dictss ts =
-      apply_constmatch sym ((maps o map) (K "_") dictss @ ts);
+      assemble_app_constmatch sym ((maps o map) (K "_") dictss @ ts);
 
     fun assemble_iterm constapp =
       let
         fun of_iterm match_continuation t =
           let

     val assemble_args = map (assemble_iterm assemble_constmatch NONE);
     val assemble_rhs = assemble_iterm assemble_constapp;
 
     fun assemble_eqn sym s_tparams dict_params default_params (i, ((samepairs, args), rhs)) =
       let
-        val default_rhs = apply_local (i + 1) sym s_tparams (dict_params @ default_params);
+        val default_rhs = assemble_app_fun (i + 1) sym s_tparams (dict_params @ default_params);
         val s_args = assemble_args args;
         val s_rhs = if null samepairs then assemble_rhs (SOME default_rhs) rhs
           else ml_if (ml_and (map nbe_same samepairs))
             (assemble_rhs (SOME default_rhs) rhs) default_rhs;
         val eqns = [([ml_list s_tparams, ml_list (rev (dict_params @ map2 ml_as default_params s_args))], s_rhs),
           ([ml_list s_tparams, ml_list (rev (dict_params @ default_params))], default_rhs)]
       in (fun_ident i sym, eqns) end;
 
     fun assemble_default_eqn sym s_tparams dict_params default_params i =
       (fun_ident i sym,
-        [([ml_list s_tparams, ml_list (rev (dict_params @ default_params))], apply_constr sym s_tparams (dict_params @ default_params))])
+        [([ml_list s_tparams, ml_list (rev (dict_params @ default_params))], assemble_app_constr sym s_tparams (dict_params @ default_params))])
 
     fun assemble_value_eqn sym s_tparams dict_params (([], args), rhs) =
       (fun_ident 0 sym,
         [([ml_list s_tparams, ml_list (rev (dict_params @ assemble_args args))], assemble_rhs NONE rhs)]);
 
     fun assemble_eqns (sym, (num_args, (s_tparams, dict_params, eqns, default_params))) =
       (if Code_Symbol.is_value sym then [assemble_value_eqn sym s_tparams dict_params (the_single eqns)]
       else map_index (assemble_eqn sym s_tparams dict_params default_params) eqns
         @ [assemble_default_eqn sym s_tparams dict_params default_params (length eqns)],
-      ml_abs (ml_list s_tparams) (nbe_abss num_args (fun_ident 0 sym `$` ml_list s_tparams)));
+      ml_abs (ml_list s_tparams) (nbe_abss num_args (assemble_fun 0 sym s_tparams)));
 
     val (fun_vars, fun_vals) = map_split assemble_eqns eqnss;
     val deps_vars = ml_list (map (fun_ident 0) deps);
   in ml_abs deps_vars (ml_Let (ml_fundefs (flat fun_vars)) (ml_list fun_vals)) end;