src/Tools/nbe.ML
changeset 55043 acefda71629b
parent 54889 4121d64fde90
child 55147 bce3dbc11f95
     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