src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 40995 3cae30b60577
parent 40994 3bdb8df0daf0
child 40996 63112be4a469
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:26:23 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:26:27 2010 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  datatype annotation = Gen | New | Fls | Tru
     1.5  datatype annotation_atom = A of annotation | V of var
     1.6  
     1.7 -type assign = var * annotation
     1.8 +type assign_literal = var * annotation
     1.9  
    1.10  datatype mtyp =
    1.11    MAlpha |
    1.12 @@ -82,7 +82,7 @@
    1.13  fun string_for_annotation_atom (A a) = string_for_annotation a
    1.14    | string_for_annotation_atom (V x) = string_for_var x
    1.15  
    1.16 -fun string_for_assign (x, a) =
    1.17 +fun string_for_assign_literal (x, a) =
    1.18    string_for_var x ^ " = " ^ string_for_annotation a
    1.19  
    1.20  val bool_M = MType (@{type_name bool}, [])
    1.21 @@ -349,7 +349,7 @@
    1.22  datatype comp_op = Eq | Leq
    1.23  
    1.24  type comp = annotation_atom * annotation_atom * comp_op * var list
    1.25 -type assign_clause = assign list
    1.26 +type assign_clause = assign_literal list
    1.27  
    1.28  type constraint_set = comp list * assign_clause list
    1.29  
    1.30 @@ -362,9 +362,9 @@
    1.31  
    1.32  fun string_for_assign_clause [] = "\<bot>"
    1.33    | string_for_assign_clause asgs =
    1.34 -    space_implode " \<or> " (map string_for_assign asgs)
    1.35 +    space_implode " \<or> " (map string_for_assign_literal asgs)
    1.36  
    1.37 -fun add_assign (x, a) clauses =
    1.38 +fun add_assign_literal (x, a) clauses =
    1.39    if exists (fn [(x', a')] => x = x' andalso a <> a' | _ => false) clauses then
    1.40      NONE
    1.41    else
    1.42 @@ -377,7 +377,7 @@
    1.43      (case (aa1, aa2) of
    1.44         (A a1, A a2) => if a1 = a2 then SOME cset else NONE
    1.45       | (V x1, A a2) =>
    1.46 -       clauses |> add_assign (x1, a2) |> Option.map (pair comps)
    1.47 +       clauses |> add_assign_literal (x1, a2) |> Option.map (pair comps)
    1.48       | (V _, V _) => SOME (insert (op =) (aa1, aa2, Eq, []) comps, clauses)
    1.49       | _ => do_annotation_atom_comp Eq [] aa2 aa1 cset)
    1.50    | do_annotation_atom_comp Leq [] aa1 aa2 (cset as (comps, clauses)) =
    1.51 @@ -441,7 +441,7 @@
    1.52    | do_notin_mtype_fv Minus _ MAlpha cset = cset
    1.53    | do_notin_mtype_fv Plus [] MAlpha _ = NONE
    1.54    | do_notin_mtype_fv Plus [(x, a)] MAlpha (SOME clauses) =
    1.55 -    clauses |> add_assign (x, a)
    1.56 +    clauses |> add_assign_literal (x, a)
    1.57    | do_notin_mtype_fv Plus clause MAlpha (SOME clauses) =
    1.58      SOME (insert (op =) clause clauses)
    1.59    | do_notin_mtype_fv sn clause (MFun (M1, A a, M2)) cset =
    1.60 @@ -495,28 +495,28 @@
    1.61  fun prop_for_bool_var_equality (v1, v2) =
    1.62    PL.And (PL.Or (PL.BoolVar v1, PL.Not (PL.BoolVar v2)),
    1.63            PL.Or (PL.Not (PL.BoolVar v1), PL.BoolVar v2))
    1.64 -fun prop_for_assign (x, a) =
    1.65 +fun prop_for_assign_literal (x, a) =
    1.66    let val (b1, b2) = bools_from_annotation a in
    1.67      PL.And (PL.BoolVar (fst_var x) |> not b1 ? PL.Not,
    1.68              PL.BoolVar (snd_var x) |> not b2 ? PL.Not)
    1.69    end
    1.70  fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a')
    1.71 -  | prop_for_atom_assign (V x, a) = prop_for_assign (x, a)
    1.72 +  | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, a)
    1.73  fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2)
    1.74    | prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1)
    1.75    | prop_for_atom_equality (V x1, V x2) =
    1.76      PL.And (prop_for_bool_var_equality (pairself fst_var (x1, x2)),
    1.77              prop_for_bool_var_equality (pairself snd_var (x1, x2)))
    1.78 -val prop_for_assign_clause = PL.exists o map prop_for_assign
    1.79 -fun prop_for_exists_var_assign xs a =
    1.80 -  PL.exists (map (fn x => prop_for_assign (x, a)) xs)
    1.81 +val prop_for_assign_clause = PL.exists o map prop_for_assign_literal
    1.82 +fun prop_for_exists_var_assign_literal xs a =
    1.83 +  PL.exists (map (fn x => prop_for_assign_literal (x, a)) xs)
    1.84  fun prop_for_comp (aa1, aa2, Eq, []) =
    1.85      PL.SAnd (prop_for_comp (aa1, aa2, Leq, []),
    1.86               prop_for_comp (aa2, aa1, Leq, []))
    1.87    | prop_for_comp (aa1, aa2, Leq, []) =
    1.88      PL.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen))
    1.89    | prop_for_comp (aa1, aa2, cmp, xs) =
    1.90 -    PL.SOr (prop_for_exists_var_assign xs Gen,
    1.91 +    PL.SOr (prop_for_exists_var_assign_literal xs Gen,
    1.92              prop_for_comp (aa1, aa2, cmp, []))
    1.93  
    1.94  (* The "calculus" parameter may be 1, 2, or 3, corresponding approximately to
    1.95 @@ -526,7 +526,7 @@
    1.96    @ (if calculus > 2 then [New, Tru] else [])
    1.97  
    1.98  fun prop_for_variable_domain calculus x =
    1.99 -  PL.exists (map (curry prop_for_assign x) (variable_domain calculus))
   1.100 +  PL.exists (map (curry prop_for_assign_literal x) (variable_domain calculus))
   1.101  
   1.102  fun extract_assigns max_var assigns asgs =
   1.103    fold (fn x => fn accum =>
   1.104 @@ -593,8 +593,9 @@
   1.105     consts: (styp * mtyp) list}
   1.106  
   1.107  val string_for_frame =
   1.108 -  commas o map (fn (j, aa) => "#" ^ string_of_int j ^ " |-> " ^
   1.109 -                              string_for_annotation_atom aa)
   1.110 +  map (fn (j, aa) => "#" ^ string_of_int j ^ " |-> " ^
   1.111 +                     string_for_annotation_atom aa)
   1.112 +  #> commas #> enclose "[" "]"
   1.113  
   1.114  type accumulator = mtype_context * constraint_set
   1.115  
   1.116 @@ -620,8 +621,8 @@
   1.117  (* FIXME: make sure tracing messages are complete *)
   1.118  
   1.119  fun add_comp_frame a cmp frame =
   1.120 -  (trace_msg (fn () => "*** Add " ^ string_for_annotation a ^
   1.121 -                       string_for_comp_op cmp ^ " frame " ^
   1.122 +  (trace_msg (fn () => "*** Add " ^ string_for_annotation a ^ " " ^
   1.123 +                       string_for_comp_op cmp ^ " " ^
   1.124                         string_for_frame frame);
   1.125     fold (add_annotation_atom_comp cmp [] (A a) o snd) frame)
   1.126  
   1.127 @@ -640,13 +641,32 @@
   1.128        | do_var (j, _) = (j, V (Unsynchronized.inc max_fresh))
   1.129    in map do_var end
   1.130  
   1.131 -fun add_imp_frames res_frame frame1 frame2 = I
   1.132 -(*###
   1.133 -  let
   1.134 -    fun do_var_pair (j, aa0) (_, aa1) (_, aa2) =
   1.135 -  in map3 do_var_pair res_frame frame1 frame2 end
   1.136 +fun do_not_var j aa0 aa1 _ = I
   1.137 +(*
   1.138 +x1 ~= T | x0 = F
   1.139 +x1 ~= F | x0 = T
   1.140 +x1 ~= G | x0 = G
   1.141 +x1 ~= N | x0 = G
   1.142  *)
   1.143  
   1.144 +fun do_conj_var j aa0 aa1 aa2 = I
   1.145 +(*
   1.146 +  (x1 ≠ T | x2 ≠ T | x0 = T) &
   1.147 +  (x1 ≠ F | x0 = F) &
   1.148 +  (x2 ≠ F | x0 = F) &
   1.149 +  (x1 ≠ G | x2 = F | x0 = G) &
   1.150 +  (x1 ≠ N | x2 = F | x0 = G) &
   1.151 +  (x1 = F | x2 ≠ G | x0 = G) &
   1.152 +  (x1 = F | x2 ≠ N | x0 = G)"
   1.153 +*)
   1.154 +
   1.155 +fun do_disj_var j aa0 aa1 aa2 = I
   1.156 +fun do_imp_var j aa0 aa1 aa2 = I
   1.157 +
   1.158 +fun add_connective_frames do_var res_frame frame1 frame2 =
   1.159 +  fold I (map3 (fn (j, aa0) => fn (_, aa1) => fn (_, aa2) =>
   1.160 +                   do_var j aa0 aa1 aa2) res_frame frame1 frame2)
   1.161 +
   1.162  fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
   1.163                               max_fresh, ...}) =
   1.164    let
   1.165 @@ -723,6 +743,17 @@
   1.166                                   MApp (bound_m, MRaw (Bound 0, M1))),
   1.167                             body_m))), accum)
   1.168        end
   1.169 +    and do_connect do_var t0 t1 t2 (accum as ({bound_frame, ...}, _)) =
   1.170 +      let
   1.171 +        val frame1 = fresh_imp_frame mdata Minus bound_frame
   1.172 +        val frame2 = fresh_imp_frame mdata Plus bound_frame
   1.173 +        val (m1, accum) = accum |>> set_frame frame1 |> do_term t1
   1.174 +        val (m2, accum) = accum |>> set_frame frame2 |> do_term t2
   1.175 +      in
   1.176 +        (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
   1.177 +         accum |>> set_frame bound_frame
   1.178 +               ||> add_connective_frames do_var bound_frame frame1 frame2)
   1.179 +      end
   1.180      and do_term t (accum as ({bound_Ts, bound_Ms, bound_frame, frees, consts},
   1.181                               cset)) =
   1.182        (trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
   1.183 @@ -879,18 +910,6 @@
   1.184                          val (m', accum) =
   1.185                            do_term t' (accum |>> push_bound aa T M)
   1.186                        in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end))
   1.187 -         | (t0 as @{const implies}) $ t1 $ t2 =>
   1.188 -           let
   1.189 -             val frame1 = fresh_imp_frame mdata Minus bound_frame
   1.190 -             val frame2 = fresh_imp_frame mdata Plus bound_frame
   1.191 -             val (m0, accum) = accum |> do_term t0
   1.192 -             val (m1, accum) = accum |>> set_frame frame1 |> do_term t1
   1.193 -             val (m2, accum) = accum |>> set_frame frame2 |> do_term t2
   1.194 -           in
   1.195 -             (MApp (MApp (m0, m1), m2),
   1.196 -              accum |>> set_frame bound_frame
   1.197 -                    ||> add_imp_frames bound_frame frame1 frame2)
   1.198 -           end
   1.199           | (t0 as Const (@{const_name All}, _))
   1.200             $ Abs (s', T', (t10 as @{const HOL.implies})
   1.201                            $ (t11 $ Bound 0) $ t12) =>
   1.202 @@ -899,6 +918,22 @@
   1.203             $ Abs (s', T', (t10 as @{const HOL.conj})
   1.204                            $ (t11 $ Bound 0) $ t12) =>
   1.205             do_bounded_quantifier t0 s' T' t10 t11 t12 accum
   1.206 +         | (t0 as @{const Not}) $ t1 =>
   1.207 +           let
   1.208 +             val frame1 = fresh_imp_frame mdata Minus bound_frame
   1.209 +             val (m1, accum) = accum |>> set_frame frame1 |> do_term t1
   1.210 +           in
   1.211 +             (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1),
   1.212 +              accum |>> set_frame bound_frame
   1.213 +                    ||> add_connective_frames do_not_var bound_frame frame1
   1.214 +                                                         frame1)
   1.215 +           end
   1.216 +         | (t0 as @{const conj}) $ t1 $ t2 =>
   1.217 +           do_connect do_conj_var t0 t1 t2 accum
   1.218 +         | (t0 as @{const disj}) $ t1 $ t2 =>
   1.219 +           do_connect do_disj_var t0 t1 t2 accum
   1.220 +         | (t0 as @{const implies}) $ t1 $ t2 =>
   1.221 +           do_connect do_imp_var t0 t1 t2 accum
   1.222           | Const (@{const_name Let}, _) $ t1 $ t2 =>
   1.223             do_term (betapply (t2, t1)) accum
   1.224           | t1 $ t2 =>