fixed de Bruijn index bug
authorblanchet
Tue May 24 00:01:33 2011 +0200 (2011-05-24)
changeset 42958034fc4d0c909
parent 42957 c693f9b7674a
child 42959 ee829022381d
fixed de Bruijn index bug
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue May 24 00:01:33 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue May 24 00:01:33 2011 +0200
     1.3 @@ -1068,8 +1068,10 @@
     1.4      end
     1.5    | s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) =
     1.6      (s_let Ts s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
     1.7 -              (curry betapply t1) t2
     1.8 -     handle TERM _ => betapply (t1, t2)) (* FIXME: fix all uses *)
     1.9 +           (curry betapply t1) t2
    1.10 +     (* FIXME: fix all "s_betapply []" calls *)
    1.11 +     handle TERM _ => betapply (t1, t2)
    1.12 +          | General.Subscript => betapply (t1, t2))
    1.13    | s_betapply _ (t1, t2) = t1 $ t2
    1.14  fun s_betapplys Ts = Library.foldl (s_betapply Ts)
    1.15  
    1.16 @@ -1504,9 +1506,9 @@
    1.17  
    1.18  (** Constant unfolding **)
    1.19  
    1.20 -fun constr_case_body ctxt stds (func_t, (x as (_, T))) =
    1.21 +fun constr_case_body ctxt stds Ts (func_t, (x as (_, T))) =
    1.22    let val arg_Ts = binder_types T in
    1.23 -    s_betapplys [] (func_t, map2 (select_nth_constr_arg ctxt stds x (Bound 0))
    1.24 +    s_betapplys Ts (func_t, map2 (select_nth_constr_arg ctxt stds x (Bound 0))
    1.25                                   (index_seq 0 (length arg_Ts)) arg_Ts)
    1.26    end
    1.27  fun add_constr_case res_T (body_t, guard_t) res_t =
    1.28 @@ -1515,13 +1517,14 @@
    1.29    else
    1.30      Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
    1.31      $ guard_t $ body_t $ res_t
    1.32 -fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) dataT res_T func_ts =
    1.33 +fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) Ts dataT res_T func_ts =
    1.34    let
    1.35      val xs = datatype_constrs hol_ctxt dataT
    1.36      val cases =
    1.37        func_ts ~~ xs
    1.38        |> map (fn (func_t, x) =>
    1.39 -                 (constr_case_body ctxt stds (incr_boundvars 1 func_t, x),
    1.40 +                 (constr_case_body ctxt stds (dataT :: Ts)
    1.41 +                                   (incr_boundvars 1 func_t, x),
    1.42                    discriminate_value hol_ctxt x (Bound 0)))
    1.43        |> AList.group (op aconv)
    1.44        |> map (apsnd (List.foldl s_disj @{const False}))
    1.45 @@ -1685,7 +1688,7 @@
    1.46                    val (dataT, res_T) = nth_range_type n T
    1.47                                         |> pairf domain_type range_type
    1.48                  in
    1.49 -                  (optimized_case_def hol_ctxt dataT res_T
    1.50 +                  (optimized_case_def hol_ctxt Ts dataT res_T
    1.51                                        (map (do_term depth Ts) (take n ts)),
    1.52                     drop n ts)
    1.53                  end
    1.54 @@ -1966,7 +1969,7 @@
    1.55    in
    1.56      [HOLogic.mk_imp
    1.57         (HOLogic.mk_disj (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T,
    1.58 -            s_betapply [] (optimized_case_def hol_ctxt T bool_T
    1.59 +            s_betapply [] (optimized_case_def hol_ctxt [] T bool_T
    1.60                                                (map case_func xs), x_var)),
    1.61          bisim_const T $ n_var $ x_var $ y_var),
    1.62       HOLogic.eq_const set_T $ (bisim_const T $ bisim_max $ x_var)