src/Tools/nbe.ML
changeset 41037 6d6f23b3a879
parent 40730 2aa0390a2da7
child 41068 7e643e07be7f
     1.1 --- a/src/Tools/nbe.ML	Mon Dec 06 14:17:35 2010 -0800
     1.2 +++ b/src/Tools/nbe.ML	Tue Dec 07 09:36:12 2010 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    val apps: Univ -> Univ list -> Univ        (*explicit applications*)
     1.5    val abss: int -> (Univ list -> Univ) -> Univ
     1.6                                               (*abstractions as closures*)
     1.7 -  val eq_Univ: Univ * Univ -> bool
     1.8 +  val same: Univ * Univ -> bool
     1.9  
    1.10    val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
    1.11    val trace: bool Unsynchronized.ref
    1.12 @@ -183,27 +183,10 @@
    1.13    | apps (Const (name, xs)) ys = Const (name, ys @ xs)
    1.14    | apps (BVar (n, xs)) ys = BVar (n, ys @ xs);
    1.15  
    1.16 -fun satisfy_abs (abs as ((n, f), xs)) some_k =
    1.17 -  let
    1.18 -    val ys = case some_k
    1.19 -     of NONE => replicate n (BVar (0, []))
    1.20 -      | SOME k => map_range (fn l => BVar (k + l, [])) n;
    1.21 -  in (apps (Abs abs) ys, ys) end;
    1.22 -
    1.23 -fun maxidx (Const (_, xs)) = fold maxidx xs
    1.24 -  | maxidx (DFree _) = I
    1.25 -  | maxidx (BVar (l, xs)) = fold maxidx xs #> Integer.max (l + 1)
    1.26 -  | maxidx (Abs abs) = maxidx (fst (satisfy_abs abs NONE));
    1.27 -
    1.28 -fun eq_Univ (Const (k, xs), Const (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys)
    1.29 -  | eq_Univ (DFree (s, k), DFree (t, l)) = s = t andalso k = l
    1.30 -  | eq_Univ (BVar (k, xs), BVar (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys)
    1.31 -  | eq_Univ (x as Abs abs, y) =
    1.32 -      let
    1.33 -        val (x, ys) = satisfy_abs abs ((SOME o maxidx x o maxidx y) 0)
    1.34 -      in eq_Univ (x, apps y ys) end
    1.35 -  | eq_Univ (x, y as Abs _) = eq_Univ (y, x)
    1.36 -  | eq_Univ _ = false;
    1.37 +fun same (Const (k, xs), Const (l, ys)) = k = l andalso eq_list same (xs, ys)
    1.38 +  | same (DFree (s, k), DFree (t, l)) = s = t andalso k = l
    1.39 +  | same (BVar (k, xs), BVar (l, ys)) = k = l andalso eq_list same (xs, ys)
    1.40 +  | same _ = false;
    1.41  
    1.42  
    1.43  (** assembling and compiling ML code from terms **)
    1.44 @@ -258,7 +241,7 @@
    1.45    val name_const =  prefix ^ "Const";
    1.46    val name_abss =   prefix ^ "abss";
    1.47    val name_apps =   prefix ^ "apps";
    1.48 -  val name_eq =     prefix ^ "eq_Univ";
    1.49 +  val name_same =     prefix ^ "same";
    1.50  in
    1.51  
    1.52  val univs_cookie = (Univs.get, put_result, name_put);
    1.53 @@ -284,7 +267,7 @@
    1.54  fun nbe_abss 0 f = f `$` ml_list []
    1.55    | nbe_abss n f = name_abss `$$` [string_of_int n, f];
    1.56  
    1.57 -fun nbe_eq (v1, v2) = "(" ^ name_eq ^ " (" ^ nbe_bound v1 ^ ", " ^ nbe_bound v2 ^ "))";
    1.58 +fun nbe_same (v1, v2) = "(" ^ name_same ^ " (" ^ nbe_bound v1 ^ ", " ^ nbe_bound v2 ^ "))";
    1.59  
    1.60  end;
    1.61  
    1.62 @@ -370,7 +353,7 @@
    1.63          val (samepairs, args') = subst_nonlin_vars args;
    1.64          val s_args = map assemble_arg args';
    1.65          val s_rhs = if null samepairs then assemble_rhs rhs
    1.66 -          else ml_if (ml_and (map nbe_eq samepairs))
    1.67 +          else ml_if (ml_and (map nbe_same samepairs))
    1.68              (assemble_rhs rhs) default_rhs;
    1.69          val eqns = if is_eval then
    1.70              [([ml_list (rev (dicts @ s_args))], s_rhs)]