started generalizing monotonicity code to accommodate new calculus
authorblanchet
Mon Dec 06 13:18:25 2010 +0100 (2010-12-06)
changeset 409858b870370c26f
parent 40984 ef119e33dc06
child 40986 cfd91aa80701
started generalizing monotonicity code to accommodate new calculus
src/HOL/Tools/Nitpick/nitpick_mono.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:17:26 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
     1.3 @@ -23,23 +23,25 @@
     1.4  open Nitpick_Util
     1.5  open Nitpick_HOL
     1.6  
     1.7 +datatype sign = Plus | Minus
     1.8 +
     1.9  type var = int
    1.10  
    1.11 -datatype sign = Plus | Minus
    1.12 -datatype sign_atom = S of sign | V of var
    1.13 +datatype annotation = Gen | New | Fls | Tru
    1.14 +datatype annotation_atom = A of annotation | V of var
    1.15  
    1.16 -type literal = var * sign
    1.17 +type literal = var * annotation
    1.18  
    1.19  datatype mtyp =
    1.20    MAlpha |
    1.21 -  MFun of mtyp * sign_atom * mtyp |
    1.22 +  MFun of mtyp * annotation_atom * mtyp |
    1.23    MPair of mtyp * mtyp |
    1.24    MType of string * mtyp list |
    1.25    MRec of string * typ list
    1.26  
    1.27  datatype mterm =
    1.28    MRaw of term * mtyp |
    1.29 -  MAbs of string * typ * mtyp * sign_atom * mterm |
    1.30 +  MAbs of string * typ * mtyp * annotation_atom * mterm |
    1.31    MApp of mterm * mterm
    1.32  
    1.33  type mdata =
    1.34 @@ -58,22 +60,28 @@
    1.35  val trace = Unsynchronized.ref false
    1.36  fun trace_msg msg = if !trace then tracing (msg ()) else ()
    1.37  
    1.38 +fun string_for_sign Plus = "+"
    1.39 +  | string_for_sign Minus = "-"
    1.40 +
    1.41 +fun negate_sign Plus = Minus
    1.42 +  | negate_sign Minus = Plus
    1.43 +
    1.44  val string_for_var = signed_string_of_int
    1.45  fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>"
    1.46    | string_for_vars sep xs = space_implode sep (map string_for_var xs)
    1.47  fun subscript_string_for_vars sep xs =
    1.48    if null xs then "" else "\<^bsub>" ^ string_for_vars sep xs ^ "\<^esub>"
    1.49  
    1.50 -fun string_for_sign Plus = "+"
    1.51 -  | string_for_sign Minus = "-"
    1.52 +fun string_for_annotation Gen = "G"
    1.53 +  | string_for_annotation New = "N"
    1.54 +  | string_for_annotation Fls = "F"
    1.55 +  | string_for_annotation Tru = "T"
    1.56  
    1.57 -fun xor sn1 sn2 = if sn1 = sn2 then Plus else Minus
    1.58 -val negate = xor Minus
    1.59 +fun string_for_annotation_atom (A a) = string_for_annotation a
    1.60 +  | string_for_annotation_atom (V x) = string_for_var x
    1.61  
    1.62 -fun string_for_sign_atom (S sn) = string_for_sign sn
    1.63 -  | string_for_sign_atom (V x) = string_for_var x
    1.64 -
    1.65 -fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn
    1.66 +fun string_for_literal (x, a) =
    1.67 +  string_for_var x ^ " = " ^ string_for_annotation a
    1.68  
    1.69  val bool_M = MType (@{type_name bool}, [])
    1.70  val dummy_M = MType (nitpick_prefix ^ "dummy", [])
    1.71 @@ -103,7 +111,7 @@
    1.72               MAlpha => "\<alpha>"
    1.73             | MFun (M1, a, M2) =>
    1.74               aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
    1.75 -             string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2
    1.76 +             string_for_annotation_atom a ^ "\<^esup> " ^ aux prec M2
    1.77             | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
    1.78             | MType (s, []) =>
    1.79               if s = @{type_name prop} orelse s = @{type_name bool} then "o"
    1.80 @@ -135,7 +143,7 @@
    1.81             MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
    1.82           | MAbs (s, _, M, a, m) =>
    1.83             "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
    1.84 -           string_for_sign_atom a ^ "\<^esup> " ^ aux prec m
    1.85 +           string_for_annotation_atom a ^ "\<^esup> " ^ aux prec m
    1.86           | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^
    1.87          (if need_parens then ")" else "")
    1.88        end
    1.89 @@ -185,7 +193,7 @@
    1.90    | exists_alpha_sub_mtype_fresh (MRec _) = true
    1.91  
    1.92  fun constr_mtype_for_binders z Ms =
    1.93 -  fold_rev (fn M => curry3 MFun M (S Minus)) Ms (MRec z)
    1.94 +  fold_rev (fn M => curry3 MFun M (A Gen)) Ms (MRec z)
    1.95  
    1.96  fun repair_mtype _ _ MAlpha = MAlpha
    1.97    | repair_mtype cache seen (MFun (M1, a, M2)) =
    1.98 @@ -242,7 +250,7 @@
    1.99                 is_fin_fun_supported_type (body_type T2) then
   1.100                V (Unsynchronized.inc max_fresh)
   1.101              else
   1.102 -              S Minus
   1.103 +              A Gen
   1.104    in (M1, a, M2) end
   1.105  and fresh_mtype_for_type (mdata as {hol_ctxt as {ctxt, ...}, binarize, alpha_T,
   1.106                                      datatype_mcache, constr_mcache, ...})
   1.107 @@ -301,7 +309,7 @@
   1.108    | curried_strip_mtype M = ([], M)
   1.109  fun sel_mtype_from_constr_mtype s M =
   1.110    let val (arg_Ms, dataM) = curried_strip_mtype M in
   1.111 -    MFun (dataM, S Minus,
   1.112 +    MFun (dataM, A Gen,
   1.113            case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
   1.114    end
   1.115  
   1.116 @@ -323,13 +331,14 @@
   1.117    x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
   1.118      |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
   1.119  
   1.120 -fun resolve_sign_atom lits (V x) =
   1.121 -    x |> AList.lookup (op =) lits |> Option.map S |> the_default (V x)
   1.122 -  | resolve_sign_atom _ a = a
   1.123 +fun resolve_annotation_atom lits (V x) =
   1.124 +    x |> AList.lookup (op =) lits |> Option.map A |> the_default (V x)
   1.125 +  | resolve_annotation_atom _ a = a
   1.126  fun resolve_mtype lits =
   1.127    let
   1.128      fun aux MAlpha = MAlpha
   1.129 -      | aux (MFun (M1, a, M2)) = MFun (aux M1, resolve_sign_atom lits a, aux M2)
   1.130 +      | aux (MFun (M1, a, M2)) =
   1.131 +        MFun (aux M1, resolve_annotation_atom lits a, aux M2)
   1.132        | aux (MPair Mp) = MPair (pairself aux Mp)
   1.133        | aux (MType (s, Ms)) = MType (s, map aux Ms)
   1.134        | aux (MRec z) = MRec z
   1.135 @@ -337,55 +346,55 @@
   1.136  
   1.137  datatype comp_op = Eq | Leq
   1.138  
   1.139 -type comp = sign_atom * sign_atom * comp_op * var list
   1.140 -type sign_expr = literal list
   1.141 +type comp = annotation_atom * annotation_atom * comp_op * var list
   1.142 +type annotation_expr = literal list
   1.143  
   1.144 -type constraint_set = literal list * comp list * sign_expr list
   1.145 +type constraint_set = literal list * comp list * annotation_expr list
   1.146  
   1.147  fun string_for_comp_op Eq = "="
   1.148    | string_for_comp_op Leq = "\<le>"
   1.149  
   1.150 -fun string_for_sign_expr [] = "\<bot>"
   1.151 -  | string_for_sign_expr lits =
   1.152 +fun string_for_annotation_expr [] = "\<bot>"
   1.153 +  | string_for_annotation_expr lits =
   1.154      space_implode " \<or> " (map string_for_literal lits)
   1.155  
   1.156  fun do_literal _ NONE = NONE
   1.157 -  | do_literal (x, sn) (SOME lits) =
   1.158 +  | do_literal (x, a) (SOME lits) =
   1.159      case AList.lookup (op =) lits x of
   1.160 -      SOME sn' => if sn = sn' then SOME lits else NONE
   1.161 -    | NONE => SOME ((x, sn) :: lits)
   1.162 +      SOME a' => if a = a' then SOME lits else NONE
   1.163 +    | NONE => SOME ((x, a) :: lits)
   1.164  
   1.165 -fun do_sign_atom_comp Eq [] a1 a2 (accum as (lits, comps)) =
   1.166 +fun do_annotation_atom_comp Eq [] a1 a2 (accum as (lits, comps)) =
   1.167      (case (a1, a2) of
   1.168 -       (S sn1, S sn2) => if sn1 = sn2 then SOME accum else NONE
   1.169 -     | (V x1, S sn2) =>
   1.170 +       (A sn1, A sn2) => if sn1 = sn2 then SOME accum else NONE
   1.171 +     | (V x1, A sn2) =>
   1.172         Option.map (rpair comps) (do_literal (x1, sn2) (SOME lits))
   1.173       | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Eq, []) comps)
   1.174 -     | _ => do_sign_atom_comp Eq [] a2 a1 accum)
   1.175 -  | do_sign_atom_comp Leq [] a1 a2 (accum as (lits, comps)) =
   1.176 +     | _ => do_annotation_atom_comp Eq [] a2 a1 accum)
   1.177 +  | do_annotation_atom_comp Leq [] a1 a2 (accum as (lits, comps)) =
   1.178      (case (a1, a2) of
   1.179 -       (_, S Minus) => SOME accum
   1.180 -     | (S Plus, _) => SOME accum
   1.181 -     | (S Minus, S Plus) => NONE
   1.182 +       (_, A Gen) => SOME accum
   1.183 +     | (A Fls, _) => SOME accum
   1.184 +     | (A Gen, A Fls) => NONE
   1.185       | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps)
   1.186 -     | _ => do_sign_atom_comp Eq [] a1 a2 accum)
   1.187 -  | do_sign_atom_comp cmp xs a1 a2 (lits, comps) =
   1.188 +     | _ => do_annotation_atom_comp Eq [] a1 a2 accum)
   1.189 +  | do_annotation_atom_comp cmp xs a1 a2 (lits, comps) =
   1.190      SOME (lits, insert (op =) (a1, a2, cmp, xs) comps)
   1.191  
   1.192  fun do_mtype_comp _ _ _ _ NONE = NONE
   1.193    | do_mtype_comp _ _ MAlpha MAlpha accum = accum
   1.194    | do_mtype_comp Eq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
   1.195                    (SOME accum) =
   1.196 -     accum |> do_sign_atom_comp Eq xs a1 a2 |> do_mtype_comp Eq xs M11 M21
   1.197 +     accum |> do_annotation_atom_comp Eq xs a1 a2 |> do_mtype_comp Eq xs M11 M21
   1.198             |> do_mtype_comp Eq xs M12 M22
   1.199    | do_mtype_comp Leq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
   1.200                    (SOME accum) =
   1.201      (if exists_alpha_sub_mtype M11 then
   1.202 -       accum |> do_sign_atom_comp Leq xs a1 a2
   1.203 +       accum |> do_annotation_atom_comp Leq xs a1 a2
   1.204               |> do_mtype_comp Leq xs M21 M11
   1.205               |> (case a2 of
   1.206 -                   S Minus => I
   1.207 -                 | S Plus => do_mtype_comp Leq xs M11 M21
   1.208 +                   A Gen => I
   1.209 +                 | A Fls => do_mtype_comp Leq xs M11 M21
   1.210                   | V x => do_mtype_comp Leq (x :: xs) M11 M21)
   1.211       else
   1.212         SOME accum)
   1.213 @@ -418,24 +427,20 @@
   1.214      SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps)
   1.215    | do_notin_mtype_fv Plus sexp MAlpha (SOME (lits, sexps)) =
   1.216      SOME (lits, insert (op =) sexp sexps)
   1.217 -  | do_notin_mtype_fv sn sexp (MFun (M1, S sn', M2)) accum =
   1.218 -    accum |> (if sn' = Plus andalso sn = Plus then
   1.219 -                do_notin_mtype_fv Plus sexp M1
   1.220 -              else
   1.221 -                I)
   1.222 -          |> (if sn' = Minus orelse sn = Plus then
   1.223 -                do_notin_mtype_fv Minus sexp M1
   1.224 -              else
   1.225 -                I)
   1.226 +  | do_notin_mtype_fv sn sexp (MFun (M1, A a, M2)) accum =
   1.227 +    accum |> (if a = Fls andalso sn = Plus then do_notin_mtype_fv Plus sexp M1
   1.228 +              else I)
   1.229 +          |> (if a = Gen orelse sn = Plus then do_notin_mtype_fv Minus sexp M1
   1.230 +              else I)
   1.231            |> do_notin_mtype_fv sn sexp M2
   1.232    | do_notin_mtype_fv Plus sexp (MFun (M1, V x, M2)) accum =
   1.233 -    accum |> (case do_literal (x, Minus) (SOME sexp) of
   1.234 +    accum |> (case do_literal (x, Gen) (SOME sexp) of
   1.235                  NONE => I
   1.236                | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
   1.237            |> do_notin_mtype_fv Minus sexp M1
   1.238            |> do_notin_mtype_fv Plus sexp M2
   1.239    | do_notin_mtype_fv Minus sexp (MFun (M1, V x, M2)) accum =
   1.240 -    accum |> (case do_literal (x, Plus) (SOME sexp) of
   1.241 +    accum |> (case do_literal (x, Fls) (SOME sexp) of
   1.242                  NONE => I
   1.243                | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
   1.244            |> do_notin_mtype_fv Minus sexp M2
   1.245 @@ -447,37 +452,37 @@
   1.246      raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
   1.247  
   1.248  fun add_notin_mtype_fv sn M ((lits, comps, sexps) : constraint_set) =
   1.249 -    (trace_msg (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^
   1.250 -                         (case sn of Minus => "concrete" | Plus => "complete"));
   1.251 -     case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
   1.252 -       NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
   1.253 -     | SOME (lits, sexps) => (lits, comps, sexps))
   1.254 +  (trace_msg (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^
   1.255 +                       (case sn of Minus => "concrete" | Plus => "complete"));
   1.256 +   case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
   1.257 +     NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
   1.258 +   | SOME (lits, sexps) => (lits, comps, sexps))
   1.259  
   1.260  val add_mtype_is_concrete = add_notin_mtype_fv Minus
   1.261  val add_mtype_is_complete = add_notin_mtype_fv Plus
   1.262  
   1.263  val bool_from_minus = true
   1.264  
   1.265 -fun bool_from_sign Plus = not bool_from_minus
   1.266 -  | bool_from_sign Minus = bool_from_minus
   1.267 -fun sign_from_bool b = if b = bool_from_minus then Minus else Plus
   1.268 +fun bool_from_annotation Fls = not bool_from_minus
   1.269 +  | bool_from_annotation Gen = bool_from_minus
   1.270 +fun sign_from_bool b = if b = bool_from_minus then Gen else Fls
   1.271  
   1.272 -fun prop_for_literal (x, sn) =
   1.273 -  (not (bool_from_sign sn) ? PropLogic.Not) (PropLogic.BoolVar x)
   1.274 -fun prop_for_sign_atom_eq (S sn', sn) =
   1.275 -    if sn = sn' then PropLogic.True else PropLogic.False
   1.276 -  | prop_for_sign_atom_eq (V x, sn) = prop_for_literal (x, sn)
   1.277 -fun prop_for_sign_expr xs = PropLogic.exists (map prop_for_literal xs)
   1.278 -fun prop_for_exists_eq xs sn =
   1.279 -  PropLogic.exists (map (fn x => prop_for_literal (x, sn)) xs)
   1.280 +fun prop_for_literal (x, a) =
   1.281 +  PropLogic.BoolVar x |> not (bool_from_annotation a) ? PropLogic.Not
   1.282 +fun prop_for_annotation_atom_eq (A a', a) =
   1.283 +    if a = a' then PropLogic.True else PropLogic.False
   1.284 +  | prop_for_annotation_atom_eq (V x, a) = prop_for_literal (x, a)
   1.285 +fun prop_for_annotation_expr xs = PropLogic.exists (map prop_for_literal xs)
   1.286 +fun prop_for_exists_eq xs a =
   1.287 +  PropLogic.exists (map (fn x => prop_for_literal (x, a)) xs)
   1.288  fun prop_for_comp (a1, a2, Eq, []) =
   1.289      PropLogic.SAnd (prop_for_comp (a1, a2, Leq, []),
   1.290                      prop_for_comp (a2, a1, Leq, []))
   1.291    | prop_for_comp (a1, a2, Leq, []) =
   1.292 -    PropLogic.SOr (prop_for_sign_atom_eq (a1, Plus),
   1.293 -                   prop_for_sign_atom_eq (a2, Minus))
   1.294 +    PropLogic.SOr (prop_for_annotation_atom_eq (a1, Fls),
   1.295 +                   prop_for_annotation_atom_eq (a2, Gen))
   1.296    | prop_for_comp (a1, a2, cmp, xs) =
   1.297 -    PropLogic.SOr (prop_for_exists_eq xs Minus, prop_for_comp (a1, a2, cmp, []))
   1.298 +    PropLogic.SOr (prop_for_exists_eq xs Gen, prop_for_comp (a1, a2, cmp, []))
   1.299  
   1.300  fun literals_from_assignments max_var assigns lits =
   1.301    fold (fn x => fn accum =>
   1.302 @@ -488,20 +493,20 @@
   1.303             | NONE => accum) (max_var downto 1) lits
   1.304  
   1.305  fun string_for_comp (a1, a2, cmp, xs) =
   1.306 -  string_for_sign_atom a1 ^ " " ^ string_for_comp_op cmp ^
   1.307 -  subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_sign_atom a2
   1.308 +  string_for_annotation_atom a1 ^ " " ^ string_for_comp_op cmp ^
   1.309 +  subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_annotation_atom a2
   1.310  
   1.311  fun print_problem lits comps sexps =
   1.312    trace_msg (fn () => "*** Problem:\n" ^
   1.313                        cat_lines (map string_for_literal lits @
   1.314                                   map string_for_comp comps @
   1.315 -                                 map string_for_sign_expr sexps))
   1.316 +                                 map string_for_annotation_expr sexps))
   1.317  
   1.318  fun print_solution lits =
   1.319 -  let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in
   1.320 +  let val (fs, gs) = List.partition (curry (op =) Fls o snd) lits in
   1.321      trace_msg (fn () => "*** Solution:\n" ^
   1.322 -                        "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
   1.323 -                        "-: " ^ commas (map (string_for_var o fst) neg))
   1.324 +                        "F: " ^ commas (map (string_for_var o fst) fs) ^ "\n" ^
   1.325 +                        "G: " ^ commas (map (string_for_var o fst) gs))
   1.326    end
   1.327  
   1.328  fun solve max_var (lits, comps, sexps) =
   1.329 @@ -512,8 +517,8 @@
   1.330      val _ = print_problem lits comps sexps
   1.331      val prop = PropLogic.all (map prop_for_literal lits @
   1.332                                map prop_for_comp comps @
   1.333 -                              map prop_for_sign_expr sexps)
   1.334 -    val default_val = bool_from_sign Minus
   1.335 +                              map prop_for_annotation_expr sexps)
   1.336 +    val default_val = bool_from_annotation Gen
   1.337    in
   1.338      if PropLogic.eval (K default_val) prop then
   1.339        do_assigns (K (SOME default_val))
   1.340 @@ -558,19 +563,19 @@
   1.341        | _ => true
   1.342      val mtype_for = fresh_mtype_for_type mdata false
   1.343      fun plus_set_mtype_for_dom M =
   1.344 -      MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
   1.345 +      MFun (M, A (if exists_alpha_sub_mtype M then Fls else Gen), bool_M)
   1.346      fun do_all T (gamma, cset) =
   1.347        let
   1.348          val abs_M = mtype_for (domain_type (domain_type T))
   1.349          val body_M = mtype_for (body_type T)
   1.350        in
   1.351 -        (MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M),
   1.352 +        (MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M),
   1.353           (gamma, cset |> add_mtype_is_complete abs_M))
   1.354        end
   1.355      fun do_equals T (gamma, cset) =
   1.356        let val M = mtype_for (domain_type T) in
   1.357 -        (MFun (M, S Minus, MFun (M, V (Unsynchronized.inc max_fresh),
   1.358 -                                 mtype_for (nth_range_type 2 T))),
   1.359 +        (MFun (M, A Gen, MFun (M, V (Unsynchronized.inc max_fresh),
   1.360 +                               mtype_for (nth_range_type 2 T))),
   1.361           (gamma, cset |> add_mtype_is_concrete M))
   1.362        end
   1.363      fun do_robust_set_operation T (gamma, cset) =
   1.364 @@ -580,7 +585,7 @@
   1.365          val M2 = mtype_for set_T
   1.366          val M3 = mtype_for set_T
   1.367        in
   1.368 -        (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
   1.369 +        (MFun (M1, A Gen, MFun (M2, A Gen, M3)),
   1.370           (gamma, cset |> add_is_sub_mtype M1 M3 |> add_is_sub_mtype M2 M3))
   1.371        end
   1.372      fun do_fragile_set_operation T (gamma, cset) =
   1.373 @@ -589,7 +594,7 @@
   1.374          val set_M = mtype_for set_T
   1.375          fun custom_mtype_for (T as Type (@{type_name fun}, [T1, T2])) =
   1.376              if T = set_T then set_M
   1.377 -            else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2)
   1.378 +            else MFun (custom_mtype_for T1, A Gen, custom_mtype_for T2)
   1.379            | custom_mtype_for T = mtype_for T
   1.380        in
   1.381          (custom_mtype_for T, (gamma, cset |> add_mtype_is_concrete set_M))
   1.382 @@ -597,12 +602,12 @@
   1.383      fun do_pair_constr T accum =
   1.384        case mtype_for (nth_range_type 2 T) of
   1.385          M as MPair (a_M, b_M) =>
   1.386 -        (MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum)
   1.387 +        (MFun (a_M, A Gen, MFun (b_M, A Gen, M)), accum)
   1.388        | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M], [])
   1.389      fun do_nth_pair_sel n T =
   1.390        case mtype_for (domain_type T) of
   1.391          M as MPair (a_M, b_M) =>
   1.392 -        pair (MFun (M, S Minus, if n = 0 then a_M else b_M))
   1.393 +        pair (MFun (M, A Gen, if n = 0 then a_M else b_M))
   1.394        | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
   1.395      fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
   1.396        let
   1.397 @@ -616,7 +621,7 @@
   1.398          val bound_M = mtype_of_mterm bound_m
   1.399          val (M1, a, _) = dest_MFun bound_M
   1.400        in
   1.401 -        (MApp (MRaw (t0, MFun (bound_M, S Minus, bool_M)),
   1.402 +        (MApp (MRaw (t0, MFun (bound_M, A Gen, bool_M)),
   1.403                 MAbs (abs_s, abs_T, M1, a,
   1.404                       MApp (MApp (MRaw (connective_t,
   1.405                                         mtype_for (fastype_of connective_t)),
   1.406 @@ -653,12 +658,12 @@
   1.407                  (trace_msg (K "*** Eps"); raise UNSOLVABLE ())
   1.408                | @{const_name If} =>
   1.409                  do_robust_set_operation (range_type T) accum
   1.410 -                |>> curry3 MFun bool_M (S Minus)
   1.411 +                |>> curry3 MFun bool_M (A Gen)
   1.412                | @{const_name Pair} => do_pair_constr T accum
   1.413                | @{const_name fst} => do_nth_pair_sel 0 T accum
   1.414                | @{const_name snd} => do_nth_pair_sel 1 T accum
   1.415                | @{const_name Id} =>
   1.416 -                (MFun (mtype_for (domain_type T), S Minus, bool_M), accum)
   1.417 +                (MFun (mtype_for (domain_type T), A Gen, bool_M), accum)
   1.418                | @{const_name converse} =>
   1.419                  let
   1.420                    val x = Unsynchronized.inc max_fresh
   1.421 @@ -666,7 +671,7 @@
   1.422                      MFun (mtype_for (domain_type T), V x, bool_M)
   1.423                    val ab_set_M = domain_type T |> mtype_for_set
   1.424                    val ba_set_M = range_type T |> mtype_for_set
   1.425 -                in (MFun (ab_set_M, S Minus, ba_set_M), accum) end
   1.426 +                in (MFun (ab_set_M, A Gen, ba_set_M), accum) end
   1.427                | @{const_name trancl} => do_fragile_set_operation T accum
   1.428                | @{const_name rel_comp} =>
   1.429                  let
   1.430 @@ -677,7 +682,7 @@
   1.431                    val ab_set_M = domain_type (range_type T) |> mtype_for_set
   1.432                    val ac_set_M = nth_range_type 2 T |> mtype_for_set
   1.433                  in
   1.434 -                  (MFun (bc_set_M, S Minus, MFun (ab_set_M, S Minus, ac_set_M)),
   1.435 +                  (MFun (bc_set_M, A Gen, MFun (ab_set_M, A Gen, ac_set_M)),
   1.436                     accum)
   1.437                  end
   1.438                | @{const_name image} =>
   1.439 @@ -685,13 +690,13 @@
   1.440                    val a_M = mtype_for (domain_type (domain_type T))
   1.441                    val b_M = mtype_for (range_type (domain_type T))
   1.442                  in
   1.443 -                  (MFun (MFun (a_M, S Minus, b_M), S Minus,
   1.444 -                         MFun (plus_set_mtype_for_dom a_M, S Minus,
   1.445 +                  (MFun (MFun (a_M, A Gen, b_M), A Gen,
   1.446 +                         MFun (plus_set_mtype_for_dom a_M, A Gen,
   1.447                                 plus_set_mtype_for_dom b_M)), accum)
   1.448                  end
   1.449                | @{const_name finite} =>
   1.450                  let val M1 = mtype_for (domain_type (domain_type T)) in
   1.451 -                  (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum)
   1.452 +                  (MFun (plus_set_mtype_for_dom M1, A Gen, bool_M), accum)
   1.453                  end
   1.454                | @{const_name Sigma} =>
   1.455                  let
   1.456 @@ -703,18 +708,18 @@
   1.457                    val b_set_M = mtype_for_set (range_type (domain_type
   1.458                                                                 (range_type T)))
   1.459                    val a_set_M = mtype_for_set a_set_T
   1.460 -                  val a_to_b_set_M = MFun (a_M, S Minus, b_set_M)
   1.461 +                  val a_to_b_set_M = MFun (a_M, A Gen, b_set_M)
   1.462                    val ab_set_M = mtype_for_set (nth_range_type 2 T)
   1.463                  in
   1.464 -                  (MFun (a_set_M, S Minus,
   1.465 -                         MFun (a_to_b_set_M, S Minus, ab_set_M)), accum)
   1.466 +                  (MFun (a_set_M, A Gen, MFun (a_to_b_set_M, A Gen, ab_set_M)),
   1.467 +                   accum)
   1.468                  end
   1.469                | _ =>
   1.470                  if s = @{const_name safe_The} then
   1.471                    let
   1.472                      val a_set_M = mtype_for (domain_type T)
   1.473                      val a_M = dest_MFun a_set_M |> #1
   1.474 -                  in (MFun (a_set_M, S Minus, a_M), accum) end
   1.475 +                  in (MFun (a_set_M, A Gen, a_M), accum) end
   1.476                  else if s = @{const_name ord_class.less_eq} andalso
   1.477                          is_set_type (domain_type T) then
   1.478                    do_fragile_set_operation T accum
   1.479 @@ -765,9 +770,7 @@
   1.480                        let
   1.481                          val M = mtype_for T
   1.482                          val (m', accum) = do_term t' (accum |>> push_bound T M)
   1.483 -                      in
   1.484 -                        (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound)
   1.485 -                      end))
   1.486 +                      in (MAbs (s, T, M, A Gen, m'), accum |>> pop_bound) end))
   1.487           | (t0 as Const (@{const_name All}, _))
   1.488             $ Abs (s', T', (t10 as @{const HOL.implies}) $ (t11 $ Bound 0) $ t12) =>
   1.489             do_bounded_quantifier t0 s' T' t10 t11 t12 accum
   1.490 @@ -792,8 +795,7 @@
   1.491  
   1.492  fun force_minus_funs 0 _ = I
   1.493    | force_minus_funs n (M as MFun (M1, _, M2)) =
   1.494 -    add_mtypes_equal M (MFun (M1, S Minus, M2))
   1.495 -    #> force_minus_funs (n - 1) M2
   1.496 +    add_mtypes_equal M (MFun (M1, A Gen, M2)) #> force_minus_funs (n - 1) M2
   1.497    | force_minus_funs _ M =
   1.498      raise MTYPE ("Nitpick_Mono.force_minus_funs", [M], [])
   1.499  fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum =
   1.500 @@ -805,7 +807,7 @@
   1.501      val accum = accum ||> add_mtypes_equal M1 M2
   1.502      val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T)
   1.503      val m = MApp (MApp (MRaw (Const x,
   1.504 -                MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2)
   1.505 +                           MFun (M1, A Gen, MFun (M2, A Gen, body_M))), m1), m2)
   1.506    in
   1.507      (m, if def then
   1.508            let val (head_m, arg_ms) = strip_mcomb m1 in
   1.509 @@ -831,9 +833,8 @@
   1.510                val body_M = mtype_of_mterm body_m
   1.511              in
   1.512                (MApp (MRaw (Const quant_x,
   1.513 -                           MFun (MFun (abs_M, S Minus, body_M), S Minus,
   1.514 -                                 body_M)),
   1.515 -                     MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
   1.516 +                           MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M)),
   1.517 +                     MAbs (abs_s, abs_T, abs_M, A Gen, body_m)),
   1.518                 accum |>> pop_bound)
   1.519              end
   1.520            fun do_equals x t1 t2 =
   1.521 @@ -854,7 +855,7 @@
   1.522                        m1), accum)
   1.523               end
   1.524             | @{const Not} $ t1 =>
   1.525 -             let val (m1, accum) = do_formula (negate sn) t1 accum in
   1.526 +             let val (m1, accum) = do_formula (negate_sign sn) t1 accum in
   1.527                 (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
   1.528                  accum)
   1.529               end
   1.530 @@ -882,7 +883,8 @@
   1.531                 let
   1.532                   val impl = (s0 = @{const_name "==>"} orelse
   1.533                               s0 = @{const_name HOL.implies})
   1.534 -                 val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
   1.535 +                 val (m1, accum) =
   1.536 +                   do_formula (sn |> impl ? negate_sign) t1 accum
   1.537                   val (m2, accum) = do_formula sn t2 accum
   1.538                 in
   1.539                   (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
   1.540 @@ -931,9 +933,9 @@
   1.541              accum |>> push_bound abs_T abs_M |> do_formula body_t
   1.542            val body_M = mtype_of_mterm body_m
   1.543          in
   1.544 -          (MApp (MRaw (quant_t,
   1.545 -                       MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M)),
   1.546 -                 MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
   1.547 +          (MApp (MRaw (quant_t, MFun (MFun (abs_M, A Gen, body_M), A Gen,
   1.548 +                       body_M)),
   1.549 +                 MAbs (abs_s, abs_T, abs_M, A Gen, body_m)),
   1.550             accum |>> pop_bound)
   1.551          end
   1.552        and do_conjunction t0 t1 t2 accum =
   1.553 @@ -1023,14 +1025,14 @@
   1.554                    binarize finitizes alpha_T tsp =
   1.555    case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
   1.556      SOME (lits, msp, constr_mtypes) =>
   1.557 -    if forall (curry (op =) Minus o snd) lits then
   1.558 +    if forall (curry (op =) Gen o snd) lits then
   1.559        tsp
   1.560      else
   1.561        let
   1.562          fun should_finitize T a =
   1.563            case triple_lookup (type_match thy) finitizes T of
   1.564              SOME (SOME false) => false
   1.565 -          | _ => resolve_sign_atom lits a = S Plus
   1.566 +          | _ => resolve_annotation_atom lits a = A Fls
   1.567          fun type_from_mtype T M =
   1.568            case (M, T) of
   1.569              (MAlpha, _) => T