prefer indexes user for pattern matching to print concrete names for symbols, do not rely on printable unique identifiers
authorhaftmann
Sun Jan 19 11:05:38 2014 +0100 (2014-01-19)
changeset 55043acefda71629b
parent 55042 29e1657b7389
child 55044 5f4d5f6876f1
child 55049 327eafb594ba
prefer indexes user for pattern matching to print concrete names for symbols, do not rely on printable unique identifiers
src/Tools/nbe.ML
     1.1 --- a/src/Tools/nbe.ML	Sun Jan 19 11:05:37 2014 +0100
     1.2 +++ b/src/Tools/nbe.ML	Sun Jan 19 11:05:38 2014 +0100
     1.3 @@ -249,8 +249,11 @@
     1.4  
     1.5  val univs_cookie = (Univs.get, put_result, name_put);
     1.6  
     1.7 -fun nbe_fun 0 "" = "nbe_value"
     1.8 -  | nbe_fun i c = "c_" ^ translate_string (fn "." => "_" | c => c) c ^ "_" ^ string_of_int i;
     1.9 +val sloppy_name = Long_Name.base_name o Long_Name.qualifier
    1.10 +
    1.11 +fun nbe_fun idx_of 0 "" = "nbe_value"
    1.12 +  | nbe_fun idx_of i c = "c_" ^ string_of_int (idx_of c)
    1.13 +      ^ "_" ^ sloppy_name c ^ "_" ^ string_of_int i;
    1.14  fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
    1.15  fun nbe_bound v = "v_" ^ v;
    1.16  fun nbe_bound_optional NONE = "_"
    1.17 @@ -260,10 +263,10 @@
    1.18  (*note: these three are the "turning spots" where proper argument order is established!*)
    1.19  fun nbe_apps t [] = t
    1.20    | nbe_apps t ts = name_apps `$$` [t, ml_list (rev ts)];
    1.21 -fun nbe_apps_local i c ts = nbe_fun i c `$` ml_list (rev ts);
    1.22 +fun nbe_apps_local idx_of i c ts = nbe_fun idx_of i c `$` ml_list (rev ts);
    1.23  fun nbe_apps_constr idx_of c ts =
    1.24    let
    1.25 -    val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ c ^ "*)"
    1.26 +    val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ sloppy_name c ^ "*)"
    1.27        else string_of_int (idx_of c);
    1.28    in name_const `$` ("(" ^ c' ^ ", " ^ ml_list (rev ts) ^ ")") end;
    1.29  
    1.30 @@ -294,10 +297,10 @@
    1.31        in case AList.lookup (op =) eqnss' c
    1.32         of SOME (num_args, _) => if num_args <= length ts'
    1.33              then let val (ts1, ts2) = chop num_args ts'
    1.34 -            in nbe_apps (nbe_apps_local 0 c ts1) ts2
    1.35 -            end else nbe_apps (nbe_abss num_args (nbe_fun 0 c)) ts'
    1.36 +            in nbe_apps (nbe_apps_local idx_of 0 c ts1) ts2
    1.37 +            end else nbe_apps (nbe_abss num_args (nbe_fun idx_of 0 c)) ts'
    1.38          | NONE => if member (op =) deps c
    1.39 -            then nbe_apps (nbe_fun 0 c) ts'
    1.40 +            then nbe_apps (nbe_fun idx_of 0 c) ts'
    1.41              else nbe_apps_constr idx_of c ts'
    1.42        end
    1.43      and assemble_classrels classrels =
    1.44 @@ -352,9 +355,8 @@
    1.45  
    1.46      fun assemble_eqn c dicts default_args (i, (args, rhs)) =
    1.47        let
    1.48 -        val is_eval = (c = "");
    1.49 -        val default_rhs = nbe_apps_local (i+1) c (dicts @ default_args);
    1.50 -        val match_cont = if is_eval then NONE else SOME default_rhs;
    1.51 +        val match_cont = if c = "" then NONE
    1.52 +          else SOME (nbe_apps_local idx_of (i + 1) c (dicts @ default_args));
    1.53          val assemble_arg = assemble_iterm
    1.54            (fn c => fn dss => fn ts => nbe_apps_constr idx_of c ((maps o map) (K "_") dss @ ts)) NONE;
    1.55          val assemble_rhs = assemble_iterm assemble_constapp match_cont;
    1.56 @@ -362,26 +364,26 @@
    1.57          val s_args = map assemble_arg args';
    1.58          val s_rhs = if null samepairs then assemble_rhs rhs
    1.59            else ml_if (ml_and (map nbe_same samepairs))
    1.60 -            (assemble_rhs rhs) default_rhs;
    1.61 -        val eqns = if is_eval then
    1.62 -            [([ml_list (rev (dicts @ s_args))], s_rhs)]
    1.63 -          else
    1.64 -            [([ml_list (rev (dicts @ map2 ml_as default_args s_args))], s_rhs),
    1.65 -              ([ml_list (rev (dicts @ default_args))], default_rhs)]
    1.66 -      in (nbe_fun i c, eqns) end;
    1.67 +            (assemble_rhs rhs) (the match_cont);
    1.68 +        val eqns = case match_cont
    1.69 +         of NONE => [([ml_list (rev (dicts @ s_args))], s_rhs)]
    1.70 +          | SOME default_rhs =>
    1.71 +              [([ml_list (rev (dicts @ map2 ml_as default_args s_args))], s_rhs),
    1.72 +                ([ml_list (rev (dicts @ default_args))], default_rhs)]
    1.73 +      in (nbe_fun idx_of i c, eqns) end;
    1.74  
    1.75      fun assemble_eqns (c, (num_args, (dicts, eqns))) =
    1.76        let
    1.77          val default_args = map nbe_default
    1.78            (Name.invent Name.context "a" (num_args - length dicts));
    1.79          val eqns' = map_index (assemble_eqn c dicts default_args) eqns
    1.80 -          @ (if c = "" then [] else [(nbe_fun (length eqns) c,
    1.81 +          @ (if c = "" then [] else [(nbe_fun idx_of (length eqns) c,
    1.82              [([ml_list (rev (dicts @ default_args))],
    1.83                nbe_apps_constr idx_of c (dicts @ default_args))])]);
    1.84 -      in (eqns', nbe_abss num_args (nbe_fun 0 c)) end;
    1.85 +      in (eqns', nbe_abss num_args (nbe_fun idx_of 0 c)) end;
    1.86  
    1.87      val (fun_vars, fun_vals) = map_split assemble_eqns eqnss';
    1.88 -    val deps_vars = ml_list (map (nbe_fun 0) deps);
    1.89 +    val deps_vars = ml_list (map (nbe_fun idx_of 0) deps);
    1.90    in ml_abs deps_vars (ml_Let (ml_fundefs (flat fun_vars)) (ml_list fun_vals)) end;
    1.91  
    1.92