tuned
authorhaftmann
Mon Jan 21 08:43:35 2008 +0100 (2008-01-21)
changeset 25935ce3cd5f0c4ee
parent 25934 7b8f3a9efa03
child 25936 f43bac9def6e
tuned
src/Tools/code/code_package.ML
src/Tools/nbe.ML
     1.1 --- a/src/Tools/code/code_package.ML	Mon Jan 21 08:43:34 2008 +0100
     1.2 +++ b/src/Tools/code/code_package.ML	Mon Jan 21 08:43:35 2008 +0100
     1.3 @@ -129,7 +129,7 @@
     1.4  
     1.5  fun satisfies thy t witnesses =
     1.6    let
     1.7 -    fun evl code ((vs, ty), t) deps ct =
     1.8 +    fun evl code ((vs, ty), t) deps _ =
     1.9        CodeTarget.eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
    1.10          code (t, ty) witnesses;
    1.11    in eval_term thy evl t end;
     2.1 --- a/src/Tools/nbe.ML	Mon Jan 21 08:43:34 2008 +0100
     2.2 +++ b/src/Tools/nbe.ML	Mon Jan 21 08:43:35 2008 +0100
     2.3 @@ -123,11 +123,10 @@
     2.4    val name_apps =       prefix ^ "apps";
     2.5  in
     2.6  
     2.7 -fun nbe_fun' c = "c_" ^ translate_string (fn "." => "_" | c => c) c;
     2.8 -val nbe_fun = nbe_fun'; (*FIXME!*)
     2.9 +fun nbe_fun "" = "nbe_value"
    2.10 +  | nbe_fun c = "c_" ^ translate_string (fn "." => "_" | c => c) c;
    2.11  fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
    2.12  fun nbe_bound v = "v_" ^ v;
    2.13 -val nbe_value = "";
    2.14  
    2.15  (*note: these three are the "turning spots" where proper argument order is established!*)
    2.16  fun nbe_apps t [] = t
    2.17 @@ -136,7 +135,6 @@
    2.18  fun nbe_apps_constr c ts =
    2.19    name_const `$` ("(" ^ ML_Syntax.print_string c ^ ", " ^ ml_list (rev ts) ^ ")");
    2.20  
    2.21 -
    2.22  fun nbe_abss 0 f = f `$` ml_list []
    2.23    | nbe_abss n f = name_abs `$$` [string_of_int n, f];
    2.24  
    2.25 @@ -199,7 +197,7 @@
    2.26        ([ml_list (rev (dict_args @ map assemble_arg args))], assemble_rhs rhs);
    2.27      val default_args = dict_args @ map nbe_bound (Name.invent_list [] "a" ((length o fst o hd) eqns));
    2.28      val default_eqn = ([ml_list (rev default_args)], nbe_apps_constr c default_args);
    2.29 -  in (nbe_fun' c, map assemble_eqn eqns @ [default_eqn]) end;
    2.30 +  in (nbe_fun c, map assemble_eqn eqns @ [default_eqn]) end;
    2.31  
    2.32  fun assemble_eqnss gr deps [] = ([], ("", []))
    2.33    | assemble_eqnss gr deps eqnss =
    2.34 @@ -212,7 +210,7 @@
    2.35            | NONE => if (is_some o Option.join o try (Graph.get_node gr)) c
    2.36                then Global else Constr;
    2.37          val deps' = filter (is_some o Option.join o try (Graph.get_node gr)) deps;
    2.38 -        val bind_deps = ml_list (map nbe_fun' deps');
    2.39 +        val bind_deps = ml_list (map nbe_fun deps');
    2.40          val bind_locals = ml_fundefs (map (assemble_eqns kind) eqnss);
    2.41          val result = ml_list (map (fn (c, n) => nbe_abss n (nbe_fun c)) num_args);
    2.42          val arg_deps = map (the o Graph.get_node gr) deps';
    2.43 @@ -279,7 +277,7 @@
    2.44      val frees' = map (fn v => Free (v, [])) frees;
    2.45      val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
    2.46    in
    2.47 -    (nbe_value, (vs, [(map IVar frees, t)]))
    2.48 +    ("", (vs, [(map IVar frees, t)]))
    2.49      |> singleton (compile_eqnss gr deps)
    2.50      |> snd
    2.51      |> (fn t => apps t (rev (dict_frees @ frees')))