removed experimental equality checking of closures; acknowledge underapproximation of equality in function name
--- a/src/HOL/ex/Normalization_by_Evaluation.thy Mon Dec 06 14:17:35 2010 -0800
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy Tue Dec 07 09:36:12 2010 +0100
@@ -66,7 +66,7 @@
lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
- by normalization
+ by normalization rule
lemma "rev [a, b, c] = [c, b, a]" by normalization
value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
--- a/src/Tools/nbe.ML Mon Dec 06 14:17:35 2010 -0800
+++ b/src/Tools/nbe.ML Tue Dec 07 09:36:12 2010 +0100
@@ -18,7 +18,7 @@
val apps: Univ -> Univ list -> Univ (*explicit applications*)
val abss: int -> (Univ list -> Univ) -> Univ
(*abstractions as closures*)
- val eq_Univ: Univ * Univ -> bool
+ val same: Univ * Univ -> bool
val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
val trace: bool Unsynchronized.ref
@@ -183,27 +183,10 @@
| apps (Const (name, xs)) ys = Const (name, ys @ xs)
| apps (BVar (n, xs)) ys = BVar (n, ys @ xs);
-fun satisfy_abs (abs as ((n, f), xs)) some_k =
- let
- val ys = case some_k
- of NONE => replicate n (BVar (0, []))
- | SOME k => map_range (fn l => BVar (k + l, [])) n;
- in (apps (Abs abs) ys, ys) end;
-
-fun maxidx (Const (_, xs)) = fold maxidx xs
- | maxidx (DFree _) = I
- | maxidx (BVar (l, xs)) = fold maxidx xs #> Integer.max (l + 1)
- | maxidx (Abs abs) = maxidx (fst (satisfy_abs abs NONE));
-
-fun eq_Univ (Const (k, xs), Const (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys)
- | eq_Univ (DFree (s, k), DFree (t, l)) = s = t andalso k = l
- | eq_Univ (BVar (k, xs), BVar (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys)
- | eq_Univ (x as Abs abs, y) =
- let
- val (x, ys) = satisfy_abs abs ((SOME o maxidx x o maxidx y) 0)
- in eq_Univ (x, apps y ys) end
- | eq_Univ (x, y as Abs _) = eq_Univ (y, x)
- | eq_Univ _ = false;
+fun same (Const (k, xs), Const (l, ys)) = k = l andalso eq_list same (xs, ys)
+ | same (DFree (s, k), DFree (t, l)) = s = t andalso k = l
+ | same (BVar (k, xs), BVar (l, ys)) = k = l andalso eq_list same (xs, ys)
+ | same _ = false;
(** assembling and compiling ML code from terms **)
@@ -258,7 +241,7 @@
val name_const = prefix ^ "Const";
val name_abss = prefix ^ "abss";
val name_apps = prefix ^ "apps";
- val name_eq = prefix ^ "eq_Univ";
+ val name_same = prefix ^ "same";
in
val univs_cookie = (Univs.get, put_result, name_put);
@@ -284,7 +267,7 @@
fun nbe_abss 0 f = f `$` ml_list []
| nbe_abss n f = name_abss `$$` [string_of_int n, f];
-fun nbe_eq (v1, v2) = "(" ^ name_eq ^ " (" ^ nbe_bound v1 ^ ", " ^ nbe_bound v2 ^ "))";
+fun nbe_same (v1, v2) = "(" ^ name_same ^ " (" ^ nbe_bound v1 ^ ", " ^ nbe_bound v2 ^ "))";
end;
@@ -370,7 +353,7 @@
val (samepairs, args') = subst_nonlin_vars args;
val s_args = map assemble_arg args';
val s_rhs = if null samepairs then assemble_rhs rhs
- else ml_if (ml_and (map nbe_eq samepairs))
+ else ml_if (ml_and (map nbe_same samepairs))
(assemble_rhs rhs) default_rhs;
val eqns = if is_eval then
[([ml_list (rev (dicts @ s_args))], s_rhs)]