src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 40998 bcd23ddeecef
parent 40997 67e11a73532a
child 40999 69d0d445c46a
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:30:36 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:30:38 2010 +0100
     1.3 @@ -244,6 +244,8 @@
     1.4                  $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
     1.5    | fin_fun_body _ _ _ = NONE
     1.6  
     1.7 +(* ### FIXME: make sure wellformed! *)
     1.8 +
     1.9  fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus
    1.10                              T1 T2 =
    1.11    let
    1.12 @@ -404,9 +406,7 @@
    1.13      SOME (insert (op =) (aa1, aa2, cmp, xs) comps, clauses)
    1.14  
    1.15  fun add_annotation_atom_comp cmp xs aa1 aa2 (comps, clauses) =
    1.16 -  (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom aa1 ^ " " ^
    1.17 -                       string_for_comp_op cmp ^ " " ^
    1.18 -                       string_for_annotation_atom aa2);
    1.19 +  (trace_msg (fn () => "*** Add " ^ string_for_comp (aa1, aa2, cmp, xs));
    1.20     case do_annotation_atom_comp cmp xs aa1 aa2 (comps, clauses) of
    1.21       NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
    1.22     | SOME cset => cset)
    1.23 @@ -602,45 +602,51 @@
    1.24        end
    1.25    end
    1.26  
    1.27 -type mtype_schema = mtyp * constraint_set
    1.28 -type mtype_context =
    1.29 +type mcontext =
    1.30    {bound_Ts: typ list,
    1.31     bound_Ms: mtyp list,
    1.32 -   bound_frame: (int * annotation_atom) list,
    1.33 +   frame: (int * annotation_atom) list,
    1.34     frees: (styp * mtyp) list,
    1.35     consts: (styp * mtyp) list}
    1.36  
    1.37 -type accumulator = mtype_context * constraint_set
    1.38 +fun string_for_bound ctxt Ms (j, aa) =
    1.39 +  Syntax.string_of_term ctxt (Bound (length Ms - j - 1)) ^ " :\<^bsup>" ^
    1.40 +  string_for_annotation_atom aa ^ "\<^esup> " ^
    1.41 +  string_for_mtype (nth Ms (length Ms - j - 1))
    1.42 +fun string_for_free relevant_frees ((s, _), M) =
    1.43 +  if member (op =) relevant_frees s then SOME (s ^ " : " ^ string_for_mtype M)
    1.44 +  else NONE
    1.45 +fun string_for_mcontext ctxt t {bound_Ms, frame, frees, ...} =
    1.46 +  (map_filter (string_for_free (Term.add_free_names t [])) frees @
    1.47 +   map (string_for_bound ctxt bound_Ms) frame)
    1.48 +  |> commas |> enclose "[" "]"
    1.49  
    1.50  val initial_gamma =
    1.51 -  {bound_Ts = [], bound_Ms = [], bound_frame = [], frees = [], consts = []}
    1.52 +  {bound_Ts = [], bound_Ms = [], frame = [], frees = [], consts = []}
    1.53  
    1.54 -fun push_bound aa T M {bound_Ts, bound_Ms, bound_frame, frees, consts} =
    1.55 +fun push_bound aa T M {bound_Ts, bound_Ms, frame, frees, consts} =
    1.56    {bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms,
    1.57 -   bound_frame = (length bound_Ts, aa) :: bound_frame, frees = frees,
    1.58 -   consts = consts}
    1.59 -fun pop_bound {bound_Ts, bound_Ms, bound_frame, frees, consts} =
    1.60 +   frame = frame @ [(length bound_Ts, aa)], frees = frees, consts = consts}
    1.61 +fun pop_bound {bound_Ts, bound_Ms, frame, frees, consts} =
    1.62    {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms,
    1.63 -   bound_frame = bound_frame
    1.64 -                 |> filter_out (fn (j, _) => j = length bound_Ts - 1),
    1.65 +   frame = frame |> filter_out (fn (j, _) => j = length bound_Ts - 1),
    1.66     frees = frees, consts = consts}
    1.67    handle List.Empty => initial_gamma (* FIXME: needed? *)
    1.68  
    1.69 -fun set_frame bound_frame ({bound_Ts, bound_Ms, frees, consts, ...}
    1.70 -                           : mtype_context) =
    1.71 -  {bound_Ts = bound_Ts, bound_Ms = bound_Ms, bound_frame = bound_frame,
    1.72 -   frees = frees, consts = consts}
    1.73 +fun set_frame frame ({bound_Ts, bound_Ms, frees, consts, ...} : mcontext) =
    1.74 +  {bound_Ts = bound_Ts, bound_Ms = bound_Ms, frame = frame, frees = frees,
    1.75 +   consts = consts}
    1.76  
    1.77  (* FIXME: make sure tracing messages are complete *)
    1.78  
    1.79 -fun add_comp_frame a cmp = fold (add_annotation_atom_comp cmp [] (A a) o snd)
    1.80 +fun add_comp_frame aa cmp = fold (add_annotation_atom_comp cmp [] aa o snd)
    1.81  
    1.82  fun add_bound_frame j frame =
    1.83    let
    1.84      val (new_frame, gen_frame) = List.partition (curry (op =) j o fst) frame
    1.85    in
    1.86 -    add_comp_frame New Leq new_frame
    1.87 -    #> add_comp_frame Gen Eq gen_frame
    1.88 +    add_comp_frame (A New) Leq new_frame
    1.89 +    #> add_comp_frame (A Gen) Eq gen_frame
    1.90    end
    1.91  
    1.92  fun fresh_frame ({max_fresh, ...} : mdata) fls tru =
    1.93 @@ -684,10 +690,9 @@
    1.94              else (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
    1.95    | V x => SOME (x, (sign_for_comp_op cmp, a))
    1.96  
    1.97 -val annotation_clause_from_quasi_clause =
    1.98 +val assign_clause_from_quasi_clause =
    1.99    map_filter annotation_literal_from_quasi_literal
   1.100 -
   1.101 -val add_quasi_clause = annotation_clause_from_quasi_clause #> add_assign_clause
   1.102 +val add_quasi_clause = assign_clause_from_quasi_clause #> add_assign_clause
   1.103  
   1.104  fun add_connective_var conn mk_quasi_clauses res_aa aa1 aa2 =
   1.105    (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom res_aa ^ " = " ^
   1.106 @@ -700,6 +705,41 @@
   1.107                     add_connective_var conn mk_quasi_clauses res_aa aa1 aa2)
   1.108                 res_frame frame1 frame2)
   1.109  
   1.110 +fun kill_unused_in_frame is_in (accum as ({frame, ...}, _)) =
   1.111 +  let val (used_frame, unused_frame) = List.partition is_in frame in
   1.112 +    accum |>> set_frame used_frame
   1.113 +          ||> add_comp_frame (A Gen) Eq unused_frame
   1.114 +  end
   1.115 +
   1.116 +fun split_frame is_in_fun (gamma as {frame, ...}, cset) =
   1.117 +  let
   1.118 +    fun bubble fun_frame arg_frame [] cset =
   1.119 +        ((rev fun_frame, rev arg_frame), cset)
   1.120 +      | bubble fun_frame arg_frame ((bound as (_, aa)) :: rest) cset =
   1.121 +        if is_in_fun bound then
   1.122 +          bubble (bound :: fun_frame) arg_frame rest
   1.123 +                 (cset |> add_comp_frame aa Leq arg_frame)
   1.124 +        else
   1.125 +          bubble fun_frame (bound :: arg_frame) rest cset
   1.126 +  in cset |> bubble [] [] frame ||> pair gamma end
   1.127 +
   1.128 +fun add_annotation_atom_comp_alt _ (A Gen) _ _ = I
   1.129 +  | add_annotation_atom_comp_alt _ (A _) _ _ =
   1.130 +    (trace_msg (K "*** Expected G"); raise UNSOLVABLE ())
   1.131 +  | add_annotation_atom_comp_alt cmp (V x) aa1 aa2 =
   1.132 +    add_annotation_atom_comp cmp [x] aa1 aa2
   1.133 +
   1.134 +fun add_arg_order1 ((_, aa), (_, prev_aa)) =
   1.135 +  add_annotation_atom_comp_alt Neq prev_aa (A Gen) aa
   1.136 +fun add_app1 fun_aa ((_, res_aa), (_, arg_aa)) =
   1.137 +  add_annotation_atom_comp_alt Leq arg_aa fun_aa res_aa
   1.138 +  ##> add_quasi_clause [(arg_aa, (Neq, Gen)), (res_aa, (Eq, Gen))]
   1.139 +fun add_app _ [] [] = I
   1.140 +  | add_app fun_aa res_frame arg_frame =
   1.141 +    add_comp_frame (A New) Leq arg_frame
   1.142 +    #> fold add_arg_order1 (tl arg_frame ~~ (fst (split_last arg_frame)))
   1.143 +    #> fold (add_app1 fun_aa) (res_frame ~~ arg_frame)
   1.144 +
   1.145  fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
   1.146                               max_fresh, ...}) =
   1.147    let
   1.148 @@ -779,28 +819,29 @@
   1.149                                   MApp (bound_m, MRaw (Bound 0, M1))),
   1.150                             body_m))), accum)
   1.151        end
   1.152 -    and do_connect conn mk_quasi_clauses t0 t1 t2
   1.153 -                   (accum as ({bound_frame, ...}, _)) =
   1.154 +    and do_connect conn mk_quasi_clauses t0 t1 t2 (accum as ({frame, ...}, _)) =
   1.155        let
   1.156 -        val frame1 = fresh_frame mdata (SOME Tru) NONE bound_frame
   1.157 -        val frame2 = fresh_frame mdata (SOME Fls) NONE bound_frame
   1.158 +        val frame1 = fresh_frame mdata (SOME Tru) NONE frame
   1.159 +        val frame2 = fresh_frame mdata (SOME Fls) NONE frame
   1.160          val (m1, accum) = accum |>> set_frame frame1 |> do_term t1
   1.161          val (m2, accum) = accum |>> set_frame frame2 |> do_term t2
   1.162        in
   1.163          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
   1.164 -         accum |>> set_frame bound_frame
   1.165 +         accum |>> set_frame frame
   1.166                 ||> apsnd (add_connective_frames conn mk_quasi_clauses
   1.167 -                                                bound_frame frame1 frame2))
   1.168 +                                                frame frame1 frame2))
   1.169        end
   1.170 -    and do_term t (accum as ({bound_Ts, bound_Ms, bound_frame, frees, consts},
   1.171 -                             cset)) =
   1.172 -      (trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
   1.173 -                           Syntax.string_of_term ctxt t ^ " : _?");
   1.174 +    and do_term t
   1.175 +            (accum as (gamma as {bound_Ts, bound_Ms, frame, frees, consts},
   1.176 +                       cset)) =
   1.177 +      (trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
   1.178 +                           " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
   1.179 +                           " : _?");
   1.180         case t of
   1.181           @{const False} =>
   1.182 -         (MRaw (t, bool_M), accum ||> add_comp_frame Fls Leq bound_frame)
   1.183 +         (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
   1.184         | @{const True} =>
   1.185 -         (MRaw (t, bool_M), accum ||> add_comp_frame Tru Leq bound_frame)
   1.186 +         (MRaw (t, bool_M), accum ||> add_comp_frame (A Tru) Leq frame)
   1.187         | Const (x as (s, T)) =>
   1.188           (case AList.lookup (op =) consts x of
   1.189              SOME M => (M, accum)
   1.190 @@ -900,26 +941,24 @@
   1.191                  (fresh_mtype_for_type mdata true T, accum)
   1.192                else
   1.193                  let val M = mtype_for T in
   1.194 -                  (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
   1.195 -                        bound_frame = bound_frame, frees = frees,
   1.196 -                        consts = (x, M) :: consts}, cset))
   1.197 +                  (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms, frame = frame,
   1.198 +                        frees = frees, consts = (x, M) :: consts}, cset))
   1.199                  end)
   1.200             |>> curry MRaw t
   1.201 -           ||> apsnd (add_comp_frame Gen Eq bound_frame)
   1.202 +           ||> apsnd (add_comp_frame (A Gen) Eq frame)
   1.203           | Free (x as (_, T)) =>
   1.204             (case AList.lookup (op =) frees x of
   1.205                SOME M => (M, accum)
   1.206              | NONE =>
   1.207                let val M = mtype_for T in
   1.208 -                (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
   1.209 -                      bound_frame = bound_frame, frees = (x, M) :: frees,
   1.210 -                      consts = consts}, cset))
   1.211 +                (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms, frame = frame,
   1.212 +                      frees = (x, M) :: frees, consts = consts}, cset))
   1.213                end)
   1.214 -           |>> curry MRaw t ||> apsnd (add_comp_frame Gen Eq bound_frame)
   1.215 +           |>> curry MRaw t ||> apsnd (add_comp_frame (A Gen) Eq frame)
   1.216           | Var _ => (trace_msg (K "*** Var"); raise UNSOLVABLE ())
   1.217           | Bound j =>
   1.218             (MRaw (t, nth bound_Ms j),
   1.219 -            accum ||> add_bound_frame (length bound_Ts - j - 1) bound_frame)
   1.220 +            accum ||> add_bound_frame (length bound_Ts - j - 1) frame)
   1.221           | Abs (s, T, t') =>
   1.222             (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
   1.223                SOME t' =>
   1.224 @@ -967,16 +1006,31 @@
   1.225             do_term (betapply (t2, t1)) accum
   1.226           | t1 $ t2 =>
   1.227             let
   1.228 -             val (m1, accum) = do_term t1 accum
   1.229 -             val (m2, accum) = do_term t2 accum
   1.230 +             fun is_in t (j, _) = loose_bvar1 (t, length bound_Ts - j - 1)
   1.231 +             val accum as ({frame, ...}, _) =
   1.232 +               accum |> kill_unused_in_frame (is_in t)
   1.233 +             val ((frame1a, frame1b), accum) = accum |> split_frame (is_in t1)
   1.234 +             val frame2a = frame1a |> map (apsnd (K (A Gen)))
   1.235 +             val frame2b =
   1.236 +               frame1b |> map (apsnd (fn _ => V (Unsynchronized.inc max_fresh)))
   1.237 +             val frame2 = frame2a @ frame2b
   1.238 +             val (m1, accum) = accum |>> set_frame frame1a |> do_term t1
   1.239 +             val (m2, accum) = accum |>> set_frame frame2 |> do_term t2
   1.240             in
   1.241               let
   1.242 -               val M11 = mtype_of_mterm m1 |> dest_MFun |> #1
   1.243 +               val (M11, aa, _) = mtype_of_mterm m1 |> dest_MFun
   1.244                 val M2 = mtype_of_mterm m2
   1.245 -             in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
   1.246 +             in
   1.247 +               (MApp (m1, m2),
   1.248 +                accum |>> set_frame frame
   1.249 +                      ||> add_is_sub_mtype M2 M11
   1.250 +                      ||> add_app aa frame1b frame2b)
   1.251 +             end
   1.252             end)
   1.253 -        |> tap (fn (m, _) => trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
   1.254 -                                                 string_for_mterm ctxt m))
   1.255 +        |> tap (fn (m, (gamma, _)) =>
   1.256 +                   trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
   1.257 +                                       " \<turnstile> " ^
   1.258 +                                       string_for_mterm ctxt m))
   1.259    in do_term end
   1.260  
   1.261  fun force_minus_funs 0 _ = I
   1.262 @@ -1007,7 +1061,7 @@
   1.263    let
   1.264      val mtype_for = fresh_mtype_for_type mdata false
   1.265      val do_term = consider_term mdata
   1.266 -    fun do_formula sn t accum =
   1.267 +    fun do_formula sn t (accum as (gamma, _)) =
   1.268          let
   1.269            fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
   1.270              let
   1.271 @@ -1029,9 +1083,9 @@
   1.272                Plus => do_term t accum
   1.273              | Minus => consider_general_equals mdata false x t1 t2 accum
   1.274          in
   1.275 -          (trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
   1.276 -                               Syntax.string_of_term ctxt t ^ " : o\<^sup>" ^
   1.277 -                               string_for_sign sn ^ "?");
   1.278 +          (trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
   1.279 +                               " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
   1.280 +                               " : o\<^sup>" ^ string_for_sign sn ^ "?");
   1.281             case t of
   1.282               Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
   1.283               do_quantifier x s1 T1 t1
   1.284 @@ -1081,8 +1135,9 @@
   1.285                 do_term t accum
   1.286             | _ => do_term t accum)
   1.287          end
   1.288 -        |> tap (fn (m, _) =>
   1.289 -                   trace_msg (fn () => "\<Gamma> \<turnstile> " ^
   1.290 +        |> tap (fn (m, (gamma, _)) =>
   1.291 +                   trace_msg (fn () => string_for_mcontext ctxt t gamma ^
   1.292 +                                       " \<turnstile> " ^
   1.293                                         string_for_mterm ctxt m ^ " : o\<^sup>" ^
   1.294                                         string_for_sign sn))
   1.295    in do_formula end
   1.296 @@ -1166,7 +1221,7 @@
   1.297  fun string_for_mtype_of_term ctxt asgs t M =
   1.298    Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype asgs M)
   1.299  
   1.300 -fun print_mtype_context ctxt asgs ({frees, consts, ...} : mtype_context) =
   1.301 +fun print_mcontext ctxt asgs ({frees, consts, ...} : mcontext) =
   1.302    trace_msg (fn () =>
   1.303        map (fn (x, M) => string_for_mtype_of_term ctxt asgs (Free x) M) frees @
   1.304        map (fn (x, M) => string_for_mtype_of_term ctxt asgs (Const x) M) consts
   1.305 @@ -1192,7 +1247,7 @@
   1.306        ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
   1.307    in
   1.308      case solve calculus (!max_fresh) cset of
   1.309 -      SOME asgs => (print_mtype_context ctxt asgs gamma;
   1.310 +      SOME asgs => (print_mcontext ctxt asgs gamma;
   1.311                      SOME (asgs, (nondef_ms, def_ms), !constr_mcache))
   1.312      | _ => NONE
   1.313    end