src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 40988 f7af68bfa66d
parent 40987 7d52af07bff1
child 40989 ff08edbbc182
     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 @@ -109,9 +109,9 @@
     1.4             "_"
     1.5           else case M of
     1.6               MAlpha => "\<alpha>"
     1.7 -           | MFun (M1, a, M2) =>
     1.8 +           | MFun (M1, aa, M2) =>
     1.9               aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
    1.10 -             string_for_annotation_atom a ^ "\<^esup> " ^ aux prec M2
    1.11 +             string_for_annotation_atom aa ^ "\<^esup> " ^ aux prec M2
    1.12             | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
    1.13             | MType (s, []) =>
    1.14               if s = @{type_name prop} orelse s = @{type_name bool} then "o"
    1.15 @@ -141,16 +141,16 @@
    1.16          (if need_parens then "(" else "") ^
    1.17          (case m of
    1.18             MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
    1.19 -         | MAbs (s, _, M, a, m) =>
    1.20 +         | MAbs (s, _, M, aa, m) =>
    1.21             "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
    1.22 -           string_for_annotation_atom a ^ "\<^esup> " ^ aux prec m
    1.23 +           string_for_annotation_atom aa ^ "\<^esup> " ^ aux prec m
    1.24           | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^
    1.25          (if need_parens then ")" else "")
    1.26        end
    1.27    in aux 0 end
    1.28  
    1.29  fun mtype_of_mterm (MRaw (_, M)) = M
    1.30 -  | mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m)
    1.31 +  | mtype_of_mterm (MAbs (_, _, M, aa, m)) = MFun (M, aa, mtype_of_mterm m)
    1.32    | mtype_of_mterm (MApp (m1, _)) =
    1.33      case mtype_of_mterm m1 of
    1.34        MFun (_, _, M12) => M12
    1.35 @@ -196,8 +196,8 @@
    1.36    fold_rev (fn M => curry3 MFun M (A Gen)) Ms (MRec z)
    1.37  
    1.38  fun repair_mtype _ _ MAlpha = MAlpha
    1.39 -  | repair_mtype cache seen (MFun (M1, a, M2)) =
    1.40 -    MFun (repair_mtype cache seen M1, a, repair_mtype cache seen M2)
    1.41 +  | repair_mtype cache seen (MFun (M1, aa, M2)) =
    1.42 +    MFun (repair_mtype cache seen M1, aa, repair_mtype cache seen M2)
    1.43    | repair_mtype cache seen (MPair Mp) =
    1.44      MPair (pairself (repair_mtype cache seen) Mp)
    1.45    | repair_mtype cache seen (MType (s, Ms)) =
    1.46 @@ -246,12 +246,12 @@
    1.47    let
    1.48      val M1 = fresh_mtype_for_type mdata all_minus T1
    1.49      val M2 = fresh_mtype_for_type mdata all_minus T2
    1.50 -    val a = if not all_minus andalso exists_alpha_sub_mtype_fresh M1 andalso
    1.51 -               is_fin_fun_supported_type (body_type T2) then
    1.52 -              V (Unsynchronized.inc max_fresh)
    1.53 -            else
    1.54 -              A Gen
    1.55 -  in (M1, a, M2) end
    1.56 +    val aa = if not all_minus andalso exists_alpha_sub_mtype_fresh M1 andalso
    1.57 +                is_fin_fun_supported_type (body_type T2) then
    1.58 +               V (Unsynchronized.inc max_fresh)
    1.59 +             else
    1.60 +               A Gen
    1.61 +  in (M1, aa, M2) end
    1.62  and fresh_mtype_for_type (mdata as {hol_ctxt as {ctxt, ...}, binarize, alpha_T,
    1.63                                      datatype_mcache, constr_mcache, ...})
    1.64                           all_minus =
    1.65 @@ -333,12 +333,12 @@
    1.66  
    1.67  fun resolve_annotation_atom lits (V x) =
    1.68      x |> AList.lookup (op =) lits |> Option.map A |> the_default (V x)
    1.69 -  | resolve_annotation_atom _ a = a
    1.70 +  | resolve_annotation_atom _ aa = aa
    1.71  fun resolve_mtype lits =
    1.72    let
    1.73      fun aux MAlpha = MAlpha
    1.74 -      | aux (MFun (M1, a, M2)) =
    1.75 -        MFun (aux M1, resolve_annotation_atom lits a, aux M2)
    1.76 +      | aux (MFun (M1, aa, M2)) =
    1.77 +        MFun (aux M1, resolve_annotation_atom lits aa, aux M2)
    1.78        | aux (MPair Mp) = MPair (pairself aux Mp)
    1.79        | aux (MType (s, Ms)) = MType (s, map aux Ms)
    1.80        | aux (MRec z) = MRec z
    1.81 @@ -364,35 +364,35 @@
    1.82        SOME a' => if a = a' then SOME lits else NONE
    1.83      | NONE => SOME ((x, a) :: lits)
    1.84  
    1.85 -fun do_annotation_atom_comp Eq [] a1 a2 (accum as (lits, comps)) =
    1.86 -    (case (a1, a2) of
    1.87 -       (A sn1, A sn2) => if sn1 = sn2 then SOME accum else NONE
    1.88 -     | (V x1, A sn2) =>
    1.89 -       Option.map (rpair comps) (do_literal (x1, sn2) (SOME lits))
    1.90 -     | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Eq, []) comps)
    1.91 -     | _ => do_annotation_atom_comp Eq [] a2 a1 accum)
    1.92 -  | do_annotation_atom_comp Leq [] a1 a2 (accum as (lits, comps)) =
    1.93 -    (case (a1, a2) of
    1.94 +fun do_annotation_atom_comp Eq [] aa1 aa2 (accum as (lits, comps)) =
    1.95 +    (case (aa1, aa2) of
    1.96 +       (A a1, A a2) => if a1 = a2 then SOME accum else NONE
    1.97 +     | (V x1, A a2) =>
    1.98 +       SOME lits |> do_literal (x1, a2) |> Option.map (rpair comps)
    1.99 +     | (V _, V _) => SOME (lits, insert (op =) (aa1, aa2, Eq, []) comps)
   1.100 +     | _ => do_annotation_atom_comp Eq [] aa2 aa1 accum)
   1.101 +  | do_annotation_atom_comp Leq [] aa1 aa2 (accum as (lits, comps)) =
   1.102 +    (case (aa1, aa2) of
   1.103         (_, A Gen) => SOME accum
   1.104       | (A Fls, _) => SOME accum
   1.105       | (A Gen, A Fls) => NONE
   1.106 -     | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps)
   1.107 -     | _ => do_annotation_atom_comp Eq [] a1 a2 accum)
   1.108 -  | do_annotation_atom_comp cmp xs a1 a2 (lits, comps) =
   1.109 -    SOME (lits, insert (op =) (a1, a2, cmp, xs) comps)
   1.110 +     | (V _, V _) => SOME (lits, insert (op =) (aa1, aa2, Leq, []) comps)
   1.111 +     | _ => do_annotation_atom_comp Eq [] aa1 aa2 accum)
   1.112 +  | do_annotation_atom_comp cmp xs aa1 aa2 (lits, comps) =
   1.113 +    SOME (lits, insert (op =) (aa1, aa2, cmp, xs) comps)
   1.114  
   1.115  fun do_mtype_comp _ _ _ _ NONE = NONE
   1.116    | do_mtype_comp _ _ MAlpha MAlpha accum = accum
   1.117 -  | do_mtype_comp Eq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
   1.118 +  | do_mtype_comp Eq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
   1.119                    (SOME accum) =
   1.120 -     accum |> do_annotation_atom_comp Eq xs a1 a2 |> do_mtype_comp Eq xs M11 M21
   1.121 -           |> do_mtype_comp Eq xs M12 M22
   1.122 -  | do_mtype_comp Leq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
   1.123 +     accum |> do_annotation_atom_comp Eq xs aa1 aa2
   1.124 +           |> do_mtype_comp Eq xs M11 M21 |> do_mtype_comp Eq xs M12 M22
   1.125 +  | do_mtype_comp Leq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
   1.126                    (SOME accum) =
   1.127      (if exists_alpha_sub_mtype M11 then
   1.128 -       accum |> do_annotation_atom_comp Leq xs a1 a2
   1.129 +       accum |> do_annotation_atom_comp Leq xs aa1 aa2
   1.130               |> do_mtype_comp Leq xs M21 M11
   1.131 -             |> (case a2 of
   1.132 +             |> (case aa2 of
   1.133                     A Gen => I
   1.134                   | A Fls => do_mtype_comp Leq xs M11 M21
   1.135                   | V x => do_mtype_comp Leq (x :: xs) M11 M21)
   1.136 @@ -427,10 +427,10 @@
   1.137      SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps)
   1.138    | do_notin_mtype_fv Plus sexp MAlpha (SOME (lits, sexps)) =
   1.139      SOME (lits, insert (op =) sexp sexps)
   1.140 -  | do_notin_mtype_fv sn sexp (MFun (M1, A a, M2)) accum =
   1.141 -    accum |> (if a = Fls andalso sn = Plus then do_notin_mtype_fv Plus sexp M1
   1.142 +  | do_notin_mtype_fv sn sexp (MFun (M1, A aa, M2)) accum =
   1.143 +    accum |> (if aa = Fls andalso sn = Plus then do_notin_mtype_fv Plus sexp M1
   1.144                else I)
   1.145 -          |> (if a = Gen orelse sn = Plus then do_notin_mtype_fv Minus sexp M1
   1.146 +          |> (if aa = Gen orelse sn = Plus then do_notin_mtype_fv Minus sexp M1
   1.147                else I)
   1.148            |> do_notin_mtype_fv sn sexp M2
   1.149    | do_notin_mtype_fv Plus sexp (MFun (M1, V x, M2)) accum =
   1.150 @@ -484,14 +484,14 @@
   1.151  fun prop_for_annotation_expr xs = PropLogic.exists (map prop_for_literal xs)
   1.152  fun prop_for_exists_eq xs a =
   1.153    PropLogic.exists (map (fn x => prop_for_literal (x, a)) xs)
   1.154 -fun prop_for_comp (a1, a2, Eq, []) =
   1.155 -    PropLogic.SAnd (prop_for_comp (a1, a2, Leq, []),
   1.156 -                    prop_for_comp (a2, a1, Leq, []))
   1.157 -  | prop_for_comp (a1, a2, Leq, []) =
   1.158 -    PropLogic.SOr (prop_for_annotation_atom_eq (a1, Fls),
   1.159 -                   prop_for_annotation_atom_eq (a2, Gen))
   1.160 -  | prop_for_comp (a1, a2, cmp, xs) =
   1.161 -    PropLogic.SOr (prop_for_exists_eq xs Gen, prop_for_comp (a1, a2, cmp, []))
   1.162 +fun prop_for_comp (aa1, aa2, Eq, []) =
   1.163 +    PropLogic.SAnd (prop_for_comp (aa1, aa2, Leq, []),
   1.164 +                    prop_for_comp (aa2, aa1, Leq, []))
   1.165 +  | prop_for_comp (aa1, aa2, Leq, []) =
   1.166 +    PropLogic.SOr (prop_for_annotation_atom_eq (aa1, Fls),
   1.167 +                   prop_for_annotation_atom_eq (aa2, Gen))
   1.168 +  | prop_for_comp (aa1, aa2, cmp, xs) =
   1.169 +    PropLogic.SOr (prop_for_exists_eq xs Gen, prop_for_comp (aa1, aa2, cmp, []))
   1.170  
   1.171  fun fix_bool_options (NONE, NONE) = (false, false)
   1.172    | fix_bool_options (NONE, SOME b) = (b, b)
   1.173 @@ -507,9 +507,9 @@
   1.174             | bp => (x, annotation_from_bools (fix_bool_options bp)) :: accum)
   1.175         (max_var downto 1) lits
   1.176  
   1.177 -fun string_for_comp (a1, a2, cmp, xs) =
   1.178 -  string_for_annotation_atom a1 ^ " " ^ string_for_comp_op cmp ^
   1.179 -  subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_annotation_atom a2
   1.180 +fun string_for_comp (aa1, aa2, cmp, xs) =
   1.181 +  string_for_annotation_atom aa1 ^ " " ^ string_for_comp_op cmp ^
   1.182 +  subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_annotation_atom aa2
   1.183  
   1.184  fun print_problem lits comps sexps =
   1.185    trace_msg (fn () => "*** Problem:\n" ^
   1.186 @@ -636,10 +636,10 @@
   1.187            accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
   1.188                  |> do_term body_t ||> apfst pop_bound
   1.189          val bound_M = mtype_of_mterm bound_m
   1.190 -        val (M1, a, _) = dest_MFun bound_M
   1.191 +        val (M1, aa, _) = dest_MFun bound_M
   1.192        in
   1.193          (MApp (MRaw (t0, MFun (bound_M, A Gen, bool_M)),
   1.194 -               MAbs (abs_s, abs_T, M1, a,
   1.195 +               MAbs (abs_s, abs_T, M1, aa,
   1.196                       MApp (MApp (MRaw (connective_t,
   1.197                                         mtype_for (fastype_of connective_t)),
   1.198                                   MApp (bound_m, MRaw (Bound 0, M1))),
   1.199 @@ -769,9 +769,9 @@
   1.200                SOME t' =>
   1.201                let
   1.202                  val M = mtype_for T
   1.203 -                val a = V (Unsynchronized.inc max_fresh)
   1.204 +                val aa = V (Unsynchronized.inc max_fresh)
   1.205                  val (m', accum) = do_term t' (accum |>> push_bound T M)
   1.206 -              in (MAbs (s, T, M, a, m'), accum |>> pop_bound) end
   1.207 +              in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end
   1.208              | NONE =>
   1.209                ((case t' of
   1.210                    t1' $ Bound 0 =>
   1.211 @@ -1049,15 +1049,15 @@
   1.212        tsp
   1.213      else
   1.214        let
   1.215 -        fun should_finitize T a =
   1.216 +        fun should_finitize T aa =
   1.217            case triple_lookup (type_match thy) finitizes T of
   1.218              SOME (SOME false) => false
   1.219 -          | _ => resolve_annotation_atom lits a = A Fls
   1.220 +          | _ => resolve_annotation_atom lits aa = A Fls
   1.221          fun type_from_mtype T M =
   1.222            case (M, T) of
   1.223              (MAlpha, _) => T
   1.224 -          | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) =>
   1.225 -            Type (if should_finitize T a then @{type_name fin_fun}
   1.226 +          | (MFun (M1, aa, M2), Type (@{type_name fun}, Ts)) =>
   1.227 +            Type (if should_finitize T aa then @{type_name fin_fun}
   1.228                    else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
   1.229            | (MPair (M1, M2), Type (@{type_name prod}, Ts)) =>
   1.230              Type (@{type_name prod}, map2 type_from_mtype Ts [M1, M2])
   1.231 @@ -1128,14 +1128,14 @@
   1.232                  | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
   1.233                                     [T1], [])
   1.234              in betapply (t1', coerce_term hol_ctxt new_Ts T2' T2 t2) end
   1.235 -          | MAbs (s, old_T, M, a, m') =>
   1.236 +          | MAbs (s, old_T, M, aa, m') =>
   1.237              let
   1.238                val new_T = type_from_mtype old_T M
   1.239                val t' = term_from_mterm (new_T :: new_Ts) (old_T :: old_Ts) m'
   1.240                val T' = fastype_of1 (new_T :: new_Ts, t')
   1.241              in
   1.242                Abs (s, new_T, t')
   1.243 -              |> should_finitize (new_T --> T') a
   1.244 +              |> should_finitize (new_T --> T') aa
   1.245                   ? construct_value ctxt stds (fin_fun_constr new_T T') o single
   1.246              end
   1.247        in