# HG changeset patch # User haftmann # Date 1743955972 -7200 # Node ID f9e6cbc6bf22947f5b8bf10c0ff578088a3c9a02 # Parent 8b575e1fef3b88ee84f09527afb5158c8be4b00a tuned diff -r 8b575e1fef3b -r f9e6cbc6bf22 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Sun Apr 06 14:21:18 2025 +0200 +++ b/src/Tools/nbe.ML Sun Apr 06 18:12:52 2025 +0200 @@ -214,22 +214,24 @@ (* 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 ^ ")"; + | e `$$` es = enclose "(" ")" (e ^ " " ^ implode_space es); +fun ml_abs v e = enclose "(" ")" ("fn " ^ v ^ " => " ^ e); -fun ml_cases t cs = - "(case " ^ t ^ " of " ^ space_implode " | " (map (fn (p, t) => p ^ " => " ^ t) cs) ^ ")"; +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 ^ ")"; + | 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 ml_list es = "[" ^ commas es ^ "]"; +fun e1 `*` e2 = enclose "(" ")" (e1 ^ ", " ^ e2); +fun ml_list es = enclose "[" "]" (commas es); fun ml_fundefs ([(name, [([], e)])]) = "val " ^ name ^ " = " ^ e ^ "\n" @@ -269,25 +271,26 @@ 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; @@ -335,14 +338,15 @@ 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 @@ -351,11 +355,11 @@ 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 @@ -367,7 +371,7 @@ 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 @@ -390,7 +394,7 @@ 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)) @@ -401,7 +405,7 @@ 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, @@ -411,7 +415,7 @@ (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);