src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 40989 ff08edbbc182
parent 40988 f7af68bfa66d
child 40990 a36d4d869439
     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 @@ -30,7 +30,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 literal = var * annotation
     1.8 +type assignment = var * annotation
     1.9  
    1.10  datatype mtyp =
    1.11    MAlpha |
    1.12 @@ -80,7 +80,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_literal (x, a) =
    1.17 +fun string_for_assignment (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 @@ -331,14 +331,14 @@
    1.22    x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
    1.23      |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
    1.24  
    1.25 -fun resolve_annotation_atom lits (V x) =
    1.26 -    x |> AList.lookup (op =) lits |> Option.map A |> the_default (V x)
    1.27 +fun resolve_annotation_atom asgs (V x) =
    1.28 +    x |> AList.lookup (op =) asgs |> Option.map A |> the_default (V x)
    1.29    | resolve_annotation_atom _ aa = aa
    1.30 -fun resolve_mtype lits =
    1.31 +fun resolve_mtype asgs =
    1.32    let
    1.33      fun aux MAlpha = MAlpha
    1.34        | aux (MFun (M1, aa, M2)) =
    1.35 -        MFun (aux M1, resolve_annotation_atom lits aa, aux M2)
    1.36 +        MFun (aux M1, resolve_annotation_atom asgs aa, aux M2)
    1.37        | aux (MPair Mp) = MPair (pairself aux Mp)
    1.38        | aux (MType (s, Ms)) = MType (s, map aux Ms)
    1.39        | aux (MRec z) = MRec z
    1.40 @@ -347,39 +347,38 @@
    1.41  datatype comp_op = Eq | Leq
    1.42  
    1.43  type comp = annotation_atom * annotation_atom * comp_op * var list
    1.44 -type annotation_expr = literal list
    1.45 +type annotation_expr = assignment list
    1.46  
    1.47 -type constraint_set = literal list * comp list * annotation_expr list
    1.48 +type constraint_set = assignment list * comp list * annotation_expr list
    1.49  
    1.50  fun string_for_comp_op Eq = "="
    1.51    | string_for_comp_op Leq = "\<le>"
    1.52  
    1.53  fun string_for_annotation_expr [] = "\<bot>"
    1.54 -  | string_for_annotation_expr lits =
    1.55 -    space_implode " \<or> " (map string_for_literal lits)
    1.56 +  | string_for_annotation_expr asgs =
    1.57 +    space_implode " \<or> " (map string_for_assignment asgs)
    1.58  
    1.59 -fun do_literal _ NONE = NONE
    1.60 -  | do_literal (x, a) (SOME lits) =
    1.61 -    case AList.lookup (op =) lits x of
    1.62 -      SOME a' => if a = a' then SOME lits else NONE
    1.63 -    | NONE => SOME ((x, a) :: lits)
    1.64 +fun do_assignment _ NONE = NONE
    1.65 +  | do_assignment (x, a) (SOME asgs) =
    1.66 +    case AList.lookup (op =) asgs x of
    1.67 +      SOME a' => if a = a' then SOME asgs else NONE
    1.68 +    | NONE => SOME ((x, a) :: asgs)
    1.69  
    1.70 -fun do_annotation_atom_comp Eq [] aa1 aa2 (accum as (lits, comps)) =
    1.71 +fun do_annotation_atom_comp Eq [] aa1 aa2 (accum as (asgs, comps)) =
    1.72      (case (aa1, aa2) of
    1.73         (A a1, A a2) => if a1 = a2 then SOME accum else NONE
    1.74       | (V x1, A a2) =>
    1.75 -       SOME lits |> do_literal (x1, a2) |> Option.map (rpair comps)
    1.76 -     | (V _, V _) => SOME (lits, insert (op =) (aa1, aa2, Eq, []) comps)
    1.77 +       SOME asgs |> do_assignment (x1, a2) |> Option.map (rpair comps)
    1.78 +     | (V _, V _) => SOME (asgs, insert (op =) (aa1, aa2, Eq, []) comps)
    1.79       | _ => do_annotation_atom_comp Eq [] aa2 aa1 accum)
    1.80 -  | do_annotation_atom_comp Leq [] aa1 aa2 (accum as (lits, comps)) =
    1.81 +  | do_annotation_atom_comp Leq [] aa1 aa2 (accum as (asgs, comps)) =
    1.82      (case (aa1, aa2) of
    1.83         (_, A Gen) => SOME accum
    1.84 -     | (A Fls, _) => SOME accum
    1.85 -     | (A Gen, A Fls) => NONE
    1.86 -     | (V _, V _) => SOME (lits, insert (op =) (aa1, aa2, Leq, []) comps)
    1.87 -     | _ => do_annotation_atom_comp Eq [] aa1 aa2 accum)
    1.88 -  | do_annotation_atom_comp cmp xs aa1 aa2 (lits, comps) =
    1.89 -    SOME (lits, insert (op =) (aa1, aa2, cmp, xs) comps)
    1.90 +     | (A Gen, A _) => NONE
    1.91 +     | (A a1, A a2) => if a1 = a2 then SOME accum else NONE
    1.92 +     | _ => SOME (asgs, insert (op =) (aa1, aa2, Leq, []) comps))
    1.93 +  | do_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) =
    1.94 +    SOME (asgs, insert (op =) (aa1, aa2, cmp, xs) comps)
    1.95  
    1.96  fun do_mtype_comp _ _ _ _ NONE = NONE
    1.97    | do_mtype_comp _ _ MAlpha MAlpha accum = accum
    1.98 @@ -394,7 +393,7 @@
    1.99               |> do_mtype_comp Leq xs M21 M11
   1.100               |> (case aa2 of
   1.101                     A Gen => I
   1.102 -                 | A Fls => do_mtype_comp Leq xs M11 M21
   1.103 +                 | A _ => do_mtype_comp Leq xs M11 M21
   1.104                   | V x => do_mtype_comp Leq (x :: xs) M11 M21)
   1.105       else
   1.106         SOME accum)
   1.107 @@ -410,12 +409,12 @@
   1.108      raise MTYPE ("Nitpick_Mono.do_mtype_comp (" ^ string_for_comp_op cmp ^ ")",
   1.109                   [M1, M2], [])
   1.110  
   1.111 -fun add_mtype_comp cmp M1 M2 ((lits, comps, sexps) : constraint_set) =
   1.112 +fun add_mtype_comp cmp M1 M2 ((asgs, comps, sexps) : constraint_set) =
   1.113      (trace_msg (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^
   1.114                           string_for_comp_op cmp ^ " " ^ string_for_mtype M2);
   1.115 -     case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of
   1.116 +     case do_mtype_comp cmp [] M1 M2 (SOME (asgs, comps)) of
   1.117         NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
   1.118 -     | SOME (lits, comps) => (lits, comps, sexps))
   1.119 +     | SOME (asgs, comps) => (asgs, comps, sexps))
   1.120  
   1.121  val add_mtypes_equal = add_mtype_comp Eq
   1.122  val add_is_sub_mtype = add_mtype_comp Leq
   1.123 @@ -423,24 +422,24 @@
   1.124  fun do_notin_mtype_fv _ _ _ NONE = NONE
   1.125    | do_notin_mtype_fv Minus _ MAlpha accum = accum
   1.126    | do_notin_mtype_fv Plus [] MAlpha _ = NONE
   1.127 -  | do_notin_mtype_fv Plus [(x, sn)] MAlpha (SOME (lits, sexps)) =
   1.128 -    SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps)
   1.129 -  | do_notin_mtype_fv Plus sexp MAlpha (SOME (lits, sexps)) =
   1.130 -    SOME (lits, insert (op =) sexp sexps)
   1.131 +  | do_notin_mtype_fv Plus [(x, a)] MAlpha (SOME (asgs, sexps)) =
   1.132 +    SOME asgs |> do_assignment (x, a) |> Option.map (rpair sexps)
   1.133 +  | do_notin_mtype_fv Plus sexp MAlpha (SOME (asgs, sexps)) =
   1.134 +    SOME (asgs, insert (op =) sexp sexps)
   1.135    | do_notin_mtype_fv sn sexp (MFun (M1, A aa, M2)) accum =
   1.136 -    accum |> (if aa = Fls andalso sn = Plus then do_notin_mtype_fv Plus sexp M1
   1.137 +    accum |> (if aa <> Gen andalso sn = Plus then do_notin_mtype_fv Plus sexp M1
   1.138                else I)
   1.139            |> (if aa = Gen orelse sn = Plus then do_notin_mtype_fv Minus sexp M1
   1.140                else I)
   1.141            |> do_notin_mtype_fv sn sexp M2
   1.142    | do_notin_mtype_fv Plus sexp (MFun (M1, V x, M2)) accum =
   1.143 -    accum |> (case do_literal (x, Gen) (SOME sexp) of
   1.144 +    accum |> (case do_assignment (x, Gen) (SOME sexp) of
   1.145                  NONE => I
   1.146                | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
   1.147            |> do_notin_mtype_fv Minus sexp M1
   1.148            |> do_notin_mtype_fv Plus sexp M2
   1.149    | do_notin_mtype_fv Minus sexp (MFun (M1, V x, M2)) accum =
   1.150 -    accum |> (case do_literal (x, Fls) (SOME sexp) of
   1.151 +    accum |> (case do_assignment (x, Fls) (*### FIXME: not Gen *) (SOME sexp) of
   1.152                  NONE => I
   1.153                | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
   1.154            |> do_notin_mtype_fv Minus sexp M2
   1.155 @@ -451,12 +450,12 @@
   1.156    | do_notin_mtype_fv _ _ M _ =
   1.157      raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
   1.158  
   1.159 -fun add_notin_mtype_fv sn M ((lits, comps, sexps) : constraint_set) =
   1.160 +fun add_notin_mtype_fv sn M ((asgs, comps, sexps) : constraint_set) =
   1.161    (trace_msg (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^
   1.162                         (case sn of Minus => "concrete" | Plus => "complete"));
   1.163 -   case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
   1.164 +   case do_notin_mtype_fv sn [] M (SOME (asgs, sexps)) of
   1.165       NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
   1.166 -   | SOME (lits, sexps) => (lits, comps, sexps))
   1.167 +   | SOME (asgs, sexps) => (asgs, comps, sexps))
   1.168  
   1.169  val add_mtype_is_concrete = add_notin_mtype_fv Minus
   1.170  val add_mtype_is_complete = add_notin_mtype_fv Plus
   1.171 @@ -473,21 +472,22 @@
   1.172  val bools_from_annotation = AList.lookup (op =) bool_table #> the
   1.173  val annotation_from_bools = AList.find (op =) bool_table #> the_single
   1.174  
   1.175 -fun prop_for_literal (x, a) =
   1.176 +fun prop_for_assignment (x, a) =
   1.177    let val (b1, b2) = bools_from_annotation a in
   1.178      PropLogic.SAnd (PropLogic.BoolVar (fst_var x) |> not b1 ? PropLogic.Not,
   1.179                      PropLogic.BoolVar (snd_var x) |> not b2 ? PropLogic.Not)
   1.180    end
   1.181  fun prop_for_annotation_atom_eq (A a', a) =
   1.182      if a = a' then PropLogic.True else PropLogic.False
   1.183 -  | prop_for_annotation_atom_eq (V x, a) = prop_for_literal (x, a)
   1.184 -fun prop_for_annotation_expr xs = PropLogic.exists (map prop_for_literal xs)
   1.185 +  | prop_for_annotation_atom_eq (V x, a) = prop_for_assignment (x, a)
   1.186 +fun prop_for_annotation_expr xs = PropLogic.exists (map prop_for_assignment xs)
   1.187  fun prop_for_exists_eq xs a =
   1.188 -  PropLogic.exists (map (fn x => prop_for_literal (x, a)) xs)
   1.189 +  PropLogic.exists (map (fn x => prop_for_assignment (x, a)) xs)
   1.190  fun prop_for_comp (aa1, aa2, Eq, []) =
   1.191      PropLogic.SAnd (prop_for_comp (aa1, aa2, Leq, []),
   1.192                      prop_for_comp (aa2, aa1, Leq, []))
   1.193    | prop_for_comp (aa1, aa2, Leq, []) =
   1.194 +    (* FIXME *)
   1.195      PropLogic.SOr (prop_for_annotation_atom_eq (aa1, Fls),
   1.196                     prop_for_annotation_atom_eq (aa2, Gen))
   1.197    | prop_for_comp (aa1, aa2, cmp, xs) =
   1.198 @@ -498,39 +498,40 @@
   1.199    | fix_bool_options (SOME b, NONE) = (b, b)
   1.200    | fix_bool_options (SOME b1, SOME b2) = (b1, b2)
   1.201  
   1.202 -fun literals_from_assignments max_var assigns lits =
   1.203 +fun extract_assignments max_var assigns asgs =
   1.204    fold (fn x => fn accum =>
   1.205 -           if AList.defined (op =) lits x then
   1.206 +           if AList.defined (op =) asgs x then
   1.207               accum
   1.208             else case (fst_var x, snd_var x) |> pairself assigns of
   1.209               (NONE, NONE) => accum
   1.210             | bp => (x, annotation_from_bools (fix_bool_options bp)) :: accum)
   1.211 -       (max_var downto 1) lits
   1.212 +       (max_var downto 1) asgs
   1.213  
   1.214  fun string_for_comp (aa1, aa2, cmp, xs) =
   1.215    string_for_annotation_atom aa1 ^ " " ^ string_for_comp_op cmp ^
   1.216    subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_annotation_atom aa2
   1.217  
   1.218 -fun print_problem lits comps sexps =
   1.219 +fun print_problem asgs comps sexps =
   1.220    trace_msg (fn () => "*** Problem:\n" ^
   1.221 -                      cat_lines (map string_for_literal lits @
   1.222 +                      cat_lines (map string_for_assignment asgs @
   1.223                                   map string_for_comp comps @
   1.224                                   map string_for_annotation_expr sexps))
   1.225  
   1.226 -fun print_solution lits =
   1.227 -  let val (fs, gs) = List.partition (curry (op =) Fls o snd) lits in
   1.228 -    trace_msg (fn () => "*** Solution:\n" ^
   1.229 -                        "F: " ^ commas (map (string_for_var o fst) fs) ^ "\n" ^
   1.230 -                        "G: " ^ commas (map (string_for_var o fst) gs))
   1.231 -  end
   1.232 +fun print_solution asgs =
   1.233 +  trace_msg (fn () => "*** Solution:\n" ^
   1.234 +      (asgs
   1.235 +       |> map swap
   1.236 +       |> AList.group (op =)
   1.237 +       |> map (fn (a, xs) => string_for_annotation a ^ ": " ^
   1.238 +                             string_for_vars ", " xs)
   1.239 +       |> space_implode "\n"))
   1.240  
   1.241 -fun solve max_var (lits, comps, sexps) =
   1.242 +fun solve max_var (asgs, comps, sexps) =
   1.243    let
   1.244      fun do_assigns assigns =
   1.245 -      SOME (literals_from_assignments max_var assigns lits
   1.246 -            |> tap print_solution)
   1.247 -    val _ = print_problem lits comps sexps
   1.248 -    val prop = PropLogic.all (map prop_for_literal lits @
   1.249 +      SOME (extract_assignments max_var assigns asgs |> tap print_solution)
   1.250 +    val _ = print_problem asgs comps sexps
   1.251 +    val prop = PropLogic.all (map prop_for_assignment asgs @
   1.252                                map prop_for_comp comps @
   1.253                                map prop_for_annotation_expr sexps)
   1.254      val default_val = fst (bools_from_annotation Gen)
   1.255 @@ -996,13 +997,13 @@
   1.256                               \do_formula", [t])
   1.257      in do_formula t end
   1.258  
   1.259 -fun string_for_mtype_of_term ctxt lits t M =
   1.260 -  Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype lits M)
   1.261 +fun string_for_mtype_of_term ctxt asgs t M =
   1.262 +  Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype asgs M)
   1.263  
   1.264 -fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
   1.265 +fun print_mtype_context ctxt asgs ({frees, consts, ...} : mtype_context) =
   1.266    trace_msg (fn () =>
   1.267 -      map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
   1.268 -      map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
   1.269 +      map (fn (x, M) => string_for_mtype_of_term ctxt asgs (Free x) M) frees @
   1.270 +      map (fn (x, M) => string_for_mtype_of_term ctxt asgs (Const x) M) consts
   1.271        |> cat_lines)
   1.272  
   1.273  fun amass f t (ms, accum) =
   1.274 @@ -1025,8 +1026,8 @@
   1.275        ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
   1.276    in
   1.277      case solve (!max_fresh) cset of
   1.278 -      SOME lits => (print_mtype_context ctxt lits gamma;
   1.279 -                    SOME (lits, (nondef_ms, def_ms), !constr_mcache))
   1.280 +      SOME asgs => (print_mtype_context ctxt asgs gamma;
   1.281 +                    SOME (asgs, (nondef_ms, def_ms), !constr_mcache))
   1.282      | _ => NONE
   1.283    end
   1.284    handle UNSOLVABLE () => NONE
   1.285 @@ -1044,15 +1045,15 @@
   1.286  fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...})
   1.287                    binarize finitizes alpha_T tsp =
   1.288    case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
   1.289 -    SOME (lits, msp, constr_mtypes) =>
   1.290 -    if forall (curry (op =) Gen o snd) lits then
   1.291 +    SOME (asgs, msp, constr_mtypes) =>
   1.292 +    if forall (curry (op =) Gen o snd) asgs then
   1.293        tsp
   1.294      else
   1.295        let
   1.296          fun should_finitize T aa =
   1.297            case triple_lookup (type_match thy) finitizes T of
   1.298              SOME (SOME false) => false
   1.299 -          | _ => resolve_annotation_atom lits aa = A Fls
   1.300 +          | _ => resolve_annotation_atom asgs aa = A Fls
   1.301          fun type_from_mtype T M =
   1.302            case (M, T) of
   1.303              (MAlpha, _) => T