src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 40987 7d52af07bff1
parent 40986 cfd91aa80701
child 40988 f7af68bfa66d
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
     1.3 @@ -553,19 +553,21 @@
     1.4  type mtype_context =
     1.5    {bound_Ts: typ list,
     1.6     bound_Ms: mtyp list,
     1.7 +   bound_frame: (int * annotation_atom) list,
     1.8     frees: (styp * mtyp) list,
     1.9     consts: (styp * mtyp) list}
    1.10  
    1.11  type accumulator = mtype_context * constraint_set
    1.12  
    1.13 -val initial_gamma = {bound_Ts = [], bound_Ms = [], frees = [], consts = []}
    1.14 +val initial_gamma =
    1.15 +  {bound_Ts = [], bound_Ms = [], bound_frame = [], frees = [], consts = []}
    1.16  
    1.17 -fun push_bound T M {bound_Ts, bound_Ms, frees, consts} =
    1.18 -  {bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms, frees = frees,
    1.19 -   consts = consts}
    1.20 -fun pop_bound {bound_Ts, bound_Ms, frees, consts} =
    1.21 -  {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms, frees = frees,
    1.22 -   consts = consts}
    1.23 +fun push_bound T M {bound_Ts, bound_Ms, bound_frame, frees, consts} =
    1.24 +  {bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms,
    1.25 +   bound_frame = bound_frame, frees = frees, consts = consts}
    1.26 +fun pop_bound {bound_Ts, bound_Ms, bound_frame, frees, consts} =
    1.27 +  {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms, bound_frame = bound_frame,
    1.28 +   frees = frees, consts = consts}
    1.29    handle List.Empty => initial_gamma (* FIXME: needed? *)
    1.30  
    1.31  fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
    1.32 @@ -643,7 +645,8 @@
    1.33                                   MApp (bound_m, MRaw (Bound 0, M1))),
    1.34                             body_m))), accum)
    1.35        end
    1.36 -    and do_term t (accum as ({bound_Ts, bound_Ms, frees, consts}, cset)) =
    1.37 +    and do_term t (accum as ({bound_Ts, bound_Ms, bound_frame, frees, consts},
    1.38 +                             cset)) =
    1.39          (trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
    1.40                               Syntax.string_of_term ctxt t ^ " : _?");
    1.41           case t of
    1.42 @@ -747,7 +750,8 @@
    1.43                  else
    1.44                    let val M = mtype_for T in
    1.45                      (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
    1.46 -                          frees = frees, consts = (x, M) :: consts}, cset))
    1.47 +                          bound_frame = bound_frame, frees = frees,
    1.48 +                          consts = (x, M) :: consts}, cset))
    1.49                    end) |>> curry MRaw t
    1.50           | Free (x as (_, T)) =>
    1.51             (case AList.lookup (op =) frees x of
    1.52 @@ -755,7 +759,8 @@
    1.53              | NONE =>
    1.54                let val M = mtype_for T in
    1.55                  (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
    1.56 -                      frees = (x, M) :: frees, consts = consts}, cset))
    1.57 +                      bound_frame = bound_frame, frees = (x, M) :: frees,
    1.58 +                      consts = consts}, cset))
    1.59                end) |>> curry MRaw t
    1.60           | Var _ => (trace_msg (K "*** Var"); raise UNSOLVABLE ())
    1.61           | Bound j => (MRaw (t, nth bound_Ms j), accum)