started work on ghost type arg encoding
authorblanchet
Wed Sep 07 21:31:21 2011 +0200 (2011-09-07)
changeset 448110bff1a4228b3
parent 44810 c1c05a578c1a
child 44812 9e177ffe4745
started work on ghost type arg encoding
src/HOL/Tools/ATP/atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 21:31:21 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 21:31:21 2011 +0200
     1.3 @@ -20,11 +20,11 @@
     1.4  
     1.5    datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
     1.6    datatype soundness = Sound_Modulo_Infiniteness | Sound
     1.7 -  datatype heaviness = Heavy | Ann_Light | Arg_Light
     1.8 +  datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
     1.9    datatype type_level =
    1.10      All_Types |
    1.11 -    Noninf_Nonmono_Types of soundness * heaviness |
    1.12 -    Fin_Nonmono_Types of heaviness |
    1.13 +    Noninf_Nonmono_Types of soundness * granularity |
    1.14 +    Fin_Nonmono_Types of granularity |
    1.15      Const_Arg_Types |
    1.16      No_Types
    1.17    type type_enc
    1.18 @@ -530,11 +530,11 @@
    1.19  datatype order = First_Order | Higher_Order
    1.20  datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
    1.21  datatype soundness = Sound_Modulo_Infiniteness | Sound
    1.22 -datatype heaviness = Heavy | Ann_Light | Arg_Light
    1.23 +datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
    1.24  datatype type_level =
    1.25    All_Types |
    1.26 -  Noninf_Nonmono_Types of soundness * heaviness |
    1.27 -  Fin_Nonmono_Types of heaviness |
    1.28 +  Noninf_Nonmono_Types of soundness * granularity |
    1.29 +  Fin_Nonmono_Types of granularity |
    1.30    Const_Arg_Types |
    1.31    No_Types
    1.32  
    1.33 @@ -554,9 +554,9 @@
    1.34    | level_of_type_enc (Guards (_, level)) = level
    1.35    | level_of_type_enc (Tags (_, level)) = level
    1.36  
    1.37 -fun heaviness_of_level (Noninf_Nonmono_Types (_, heaviness)) = heaviness
    1.38 -  | heaviness_of_level (Fin_Nonmono_Types heaviness) = heaviness
    1.39 -  | heaviness_of_level _ = Heavy
    1.40 +fun granularity_of_type_level (Noninf_Nonmono_Types (_, grain)) = grain
    1.41 +  | granularity_of_type_level (Fin_Nonmono_Types grain) = grain
    1.42 +  | granularity_of_type_level _ = All_Vars
    1.43  
    1.44  fun is_type_level_quasi_sound All_Types = true
    1.45    | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
    1.46 @@ -584,15 +584,16 @@
    1.47    case try_unsuffixes suffixes s of
    1.48      SOME s =>
    1.49      (case try_unsuffixes suffixes s of
    1.50 -       SOME s => (constr Ann_Light, s)
    1.51 +       SOME s => (constr Positively_Naked_Vars, s)
    1.52       | NONE =>
    1.53         case try_unsuffixes ats s of
    1.54 -         SOME s => (constr Arg_Light, s)
    1.55 -       | NONE => (constr Heavy, s))
    1.56 +         SOME s => (constr Ghost_Type_Arg_Vars, s)
    1.57 +       | NONE => (constr All_Vars, s))
    1.58    | NONE => fallback s
    1.59  
    1.60 -fun is_mangled_arg_light poly level =
    1.61 -  poly = Mangled_Monomorphic andalso heaviness_of_level level = Arg_Light
    1.62 +fun is_incompatible_type_level poly level =
    1.63 +  poly = Mangled_Monomorphic andalso
    1.64 +  granularity_of_type_level level = Ghost_Type_Arg_Vars
    1.65  
    1.66  fun type_enc_from_string soundness s =
    1.67    (case try (unprefix "poly_") s of
    1.68 @@ -614,7 +615,7 @@
    1.69                (Polymorphic, All_Types) =>
    1.70                Simple_Types (First_Order, Polymorphic, All_Types)
    1.71              | (Mangled_Monomorphic, _) =>
    1.72 -              if heaviness_of_level level = Heavy then
    1.73 +              if granularity_of_type_level level = All_Vars then
    1.74                  Simple_Types (First_Order, Mangled_Monomorphic, level)
    1.75                else
    1.76                  raise Same.SAME
    1.77 @@ -625,16 +626,16 @@
    1.78                Simple_Types (Higher_Order, Polymorphic, All_Types)
    1.79              | (_, Noninf_Nonmono_Types _) => raise Same.SAME
    1.80              | (Mangled_Monomorphic, _) =>
    1.81 -              if heaviness_of_level level = Heavy then
    1.82 +              if granularity_of_type_level level = All_Vars then
    1.83                  Simple_Types (Higher_Order, Mangled_Monomorphic, level)
    1.84                else
    1.85                  raise Same.SAME
    1.86              | _ => raise Same.SAME)
    1.87           | ("guards", (SOME poly, _)) =>
    1.88 -           if is_mangled_arg_light poly level then raise Same.SAME
    1.89 +           if is_incompatible_type_level poly level then raise Same.SAME
    1.90             else Guards (poly, level)
    1.91           | ("tags", (SOME poly, _)) =>
    1.92 -           if is_mangled_arg_light poly level then raise Same.SAME
    1.93 +           if is_incompatible_type_level poly level then raise Same.SAME
    1.94             else Tags (poly, level)
    1.95           | ("args", (SOME poly, All_Types (* naja *))) =>
    1.96             Guards (poly, Const_Arg_Types)
    1.97 @@ -706,10 +707,6 @@
    1.98    Mangled_Type_Args |
    1.99    No_Type_Args
   1.100  
   1.101 -fun should_drop_arg_type_args (Simple_Types _) = false
   1.102 -  | should_drop_arg_type_args type_enc =
   1.103 -    level_of_type_enc type_enc = All_Types
   1.104 -
   1.105  fun type_arg_policy type_enc s =
   1.106    let val mangled = (polymorphism_of_type_enc type_enc = Mangled_Monomorphic) in
   1.107      if s = type_tag_name then
   1.108 @@ -724,7 +721,9 @@
   1.109          else if mangled then
   1.110            Mangled_Type_Args
   1.111          else
   1.112 -          Explicit_Type_Args (should_drop_arg_type_args type_enc)
   1.113 +          Explicit_Type_Args
   1.114 +              (level = All_Types orelse
   1.115 +               granularity_of_type_level level = Ghost_Type_Arg_Vars)
   1.116        end
   1.117    end
   1.118  
   1.119 @@ -1227,23 +1226,25 @@
   1.120  fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
   1.121    | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
   1.122                               maybe_nonmono_Ts, ...}
   1.123 -                       (Noninf_Nonmono_Types (soundness, _)) T =
   1.124 -    exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
   1.125 -    not (exists (type_instance ctxt T) surely_infinite_Ts orelse
   1.126 -         (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
   1.127 -          is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts T))
   1.128 +                       (Noninf_Nonmono_Types (soundness, grain)) T =
   1.129 +    grain = Ghost_Type_Arg_Vars orelse
   1.130 +    (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
   1.131 +     not (exists (type_instance ctxt T) surely_infinite_Ts orelse
   1.132 +          (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
   1.133 +           is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts
   1.134 +                                           T)))
   1.135    | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
   1.136                               maybe_nonmono_Ts, ...}
   1.137 -                       (Fin_Nonmono_Types _) T =
   1.138 -    exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
   1.139 -    (exists (type_generalization ctxt T) surely_finite_Ts orelse
   1.140 -     (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
   1.141 -      is_type_surely_finite ctxt T))
   1.142 +                       (Fin_Nonmono_Types grain) T =
   1.143 +    grain = Ghost_Type_Arg_Vars orelse
   1.144 +    (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
   1.145 +     (exists (type_generalization ctxt T) surely_finite_Ts orelse
   1.146 +      (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
   1.147 +       is_type_surely_finite ctxt T)))
   1.148    | should_encode_type _ _ _ _ = false
   1.149  
   1.150  fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
   1.151 -    (heaviness_of_level level = Heavy orelse should_guard_var ()) andalso
   1.152 -    should_encode_type ctxt mono level T
   1.153 +    should_guard_var () andalso should_encode_type ctxt mono level T
   1.154    | should_guard_type _ _ _ _ _ = false
   1.155  
   1.156  fun is_maybe_universal_var (IConst ((s, _), _, _)) =
   1.157 @@ -1259,7 +1260,7 @@
   1.158  
   1.159  fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
   1.160    | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
   1.161 -    (if heaviness_of_level level = Heavy then
   1.162 +    (if granularity_of_type_level level = All_Vars then
   1.163         should_encode_type ctxt mono level T
   1.164       else case (site, is_maybe_universal_var u) of
   1.165         (Eq_Arg _, true) => should_encode_type ctxt mono level T
   1.166 @@ -1652,13 +1653,60 @@
   1.167      accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
   1.168    | is_var_positively_naked_in_term _ _ _ _ = true
   1.169  
   1.170 -fun should_guard_var_in_formula pos phi (SOME true) name =
   1.171 -    formula_fold pos (is_var_positively_naked_in_term name) phi false
   1.172 -  | should_guard_var_in_formula _ _ _ _ = true
   1.173 +fun tvar_footprint thy s ary =
   1.174 +  (case strip_prefix_and_unascii const_prefix s of
   1.175 +     SOME s =>
   1.176 +     s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
   1.177 +       |> map (fn T => Term.add_tvarsT T [] |> map fst)
   1.178 +   | NONE => [])
   1.179 +  handle TYPE _ => []
   1.180 +
   1.181 +fun ghost_type_args thy s ary =
   1.182 +  let
   1.183 +    val footprint = tvar_footprint thy s ary
   1.184 +    fun ghosts _ [] = []
   1.185 +      | ghosts seen ((i, tvars) :: args) =
   1.186 +        ghosts (union (op =) seen tvars) args
   1.187 +        |> exists (not o member (op =) seen) tvars ? cons i
   1.188 +  in
   1.189 +    if forall null footprint then
   1.190 +      []
   1.191 +    else
   1.192 +      0 upto length footprint - 1 ~~ footprint
   1.193 +      |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
   1.194 +      |> ghosts []
   1.195 +  end
   1.196 +
   1.197 +fun is_var_ghost_type_arg_in_term thy name pos tm accum =
   1.198 +  is_var_positively_naked_in_term name pos tm accum orelse
   1.199 +  let
   1.200 +    val var = ATerm (name, [])
   1.201 +    fun is_nasty_in_term (ATerm (_, [])) = false
   1.202 +      | is_nasty_in_term (ATerm ((s, _), tms)) =
   1.203 +        (member (op =) tms var andalso
   1.204 +         let val ary = length tms in
   1.205 +           case ghost_type_args thy s ary of
   1.206 +             [] => false
   1.207 +           | ghosts =>
   1.208 +             exists (fn (j, tm) => tm = var andalso member (op =) ghosts j)
   1.209 +                    (0 upto length tms - 1 ~~ tms)
   1.210 +         end) orelse
   1.211 +        exists is_nasty_in_term tms
   1.212 +      | is_nasty_in_term _ = true
   1.213 +  in is_nasty_in_term tm end
   1.214 +
   1.215 +fun should_guard_var_in_formula thy level pos phi (SOME true) name =
   1.216 +    (case granularity_of_type_level level of
   1.217 +       All_Vars => true
   1.218 +     | Positively_Naked_Vars =>
   1.219 +       formula_fold pos (is_var_positively_naked_in_term name) phi false
   1.220 +     | Ghost_Type_Arg_Vars =>
   1.221 +       formula_fold pos (is_var_ghost_type_arg_in_term thy name) phi false)
   1.222 +  | should_guard_var_in_formula _ _ _ _ _ _ = true
   1.223  
   1.224  fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
   1.225    | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
   1.226 -    heaviness_of_level level <> Heavy andalso
   1.227 +    granularity_of_type_level level <> All_Vars andalso
   1.228      should_encode_type ctxt mono level T
   1.229    | should_generate_tag_bound_decl _ _ _ _ _ = false
   1.230  
   1.231 @@ -1705,15 +1753,17 @@
   1.232    in aux end
   1.233  and formula_from_iformula ctxt format mono type_enc should_guard_var =
   1.234    let
   1.235 +    val thy = Proof_Context.theory_of ctxt
   1.236 +    val level = level_of_type_enc type_enc
   1.237      val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level
   1.238      val do_bound_type =
   1.239        case type_enc of
   1.240 -        Simple_Types (_, _, level) => fused_type ctxt mono level 0
   1.241 +        Simple_Types _ => fused_type ctxt mono level 0
   1.242          #> ho_type_from_typ format type_enc false 0 #> SOME
   1.243        | _ => K NONE
   1.244      fun do_out_of_bound_type pos phi universal (name, T) =
   1.245        if should_guard_type ctxt mono type_enc
   1.246 -             (fn () => should_guard_var pos phi universal name) T then
   1.247 +             (fn () => should_guard_var thy level pos phi universal name) T then
   1.248          IVar (name, T)
   1.249          |> type_guard_iterm format type_enc T
   1.250          |> do_term pos |> AAtom |> SOME
   1.251 @@ -1964,9 +2014,12 @@
   1.252  fun add_fact_monotonic_types ctxt mono type_enc =
   1.253    add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
   1.254  fun monotonic_types_for_facts ctxt mono type_enc facts =
   1.255 -  [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
   1.256 -         is_type_level_monotonicity_based (level_of_type_enc type_enc))
   1.257 -        ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
   1.258 +  let val level = level_of_type_enc type_enc in
   1.259 +    [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
   1.260 +           is_type_level_monotonicity_based level andalso
   1.261 +           granularity_of_type_level level <> Ghost_Type_Arg_Vars)
   1.262 +          ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
   1.263 +  end
   1.264  
   1.265  fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
   1.266    Formula (guards_sym_formula_prefix ^
   1.267 @@ -1976,7 +2029,7 @@
   1.268             |> type_guard_iterm format type_enc T
   1.269             |> AAtom
   1.270             |> formula_from_iformula ctxt format mono type_enc
   1.271 -                                    (K (K (K (K true)))) (SOME true)
   1.272 +                                    (K (K (K (K (K (K true)))))) (SOME true)
   1.273             |> bound_tvars type_enc (atyps_of T)
   1.274             |> close_formula_universally type_enc,
   1.275             isabelle_info introN, NONE)
   1.276 @@ -2029,6 +2082,7 @@
   1.277  fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
   1.278                                       j (s', T_args, T, _, ary, in_conj) =
   1.279    let
   1.280 +    val thy = Proof_Context.theory_of ctxt
   1.281      val (kind, maybe_negate) =
   1.282        if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
   1.283        else (Axiom, I)
   1.284 @@ -2038,12 +2092,20 @@
   1.285        1 upto num_args |> map (`I o make_bound_var o string_of_int)
   1.286      val bounds =
   1.287        bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
   1.288 -    val sym_needs_arg_types = exists (curry (op =) dummyT) T_args
   1.289 -    fun should_keep_arg_type T =
   1.290 -      sym_needs_arg_types andalso
   1.291 -      should_guard_type ctxt mono type_enc (K true) T
   1.292      val bound_Ts =
   1.293 -      arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
   1.294 +      if exists (curry (op =) dummyT) T_args then
   1.295 +        case level_of_type_enc type_enc of
   1.296 +          All_Types => map SOME arg_Ts
   1.297 +        | level =>
   1.298 +          if granularity_of_type_level level = Ghost_Type_Arg_Vars then
   1.299 +            let val ghosts = ghost_type_args thy s ary in
   1.300 +              map2 (fn j => if member (op =) ghosts j then SOME else K NONE)
   1.301 +                   (0 upto num_args - 1) arg_Ts
   1.302 +            end
   1.303 +          else
   1.304 +            replicate num_args NONE
   1.305 +      else
   1.306 +        replicate num_args NONE
   1.307    in
   1.308      Formula (guards_sym_formula_prefix ^ s ^
   1.309               (if n > 1 then "_" ^ string_of_int j else ""), kind,
   1.310 @@ -2052,15 +2114,15 @@
   1.311               |> type_guard_iterm format type_enc res_T
   1.312               |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
   1.313               |> formula_from_iformula ctxt format mono type_enc
   1.314 -                                      (K (K (K (K true)))) (SOME true)
   1.315 +                                      (K (K (K (K (K (K true)))))) (SOME true)
   1.316               |> n > 1 ? bound_tvars type_enc (atyps_of T)
   1.317               |> close_formula_universally type_enc
   1.318               |> maybe_negate,
   1.319               isabelle_info introN, NONE)
   1.320    end
   1.321  
   1.322 -fun formula_lines_for_nonuniform_tags_sym_decl ctxt format conj_sym_kind mono
   1.323 -        type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   1.324 +fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
   1.325 +        (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   1.326    let
   1.327      val ident_base =
   1.328        tags_sym_formula_prefix ^ s ^
   1.329 @@ -2133,13 +2195,13 @@
   1.330                                                   type_enc n s)
   1.331      end
   1.332    | Tags (_, level) =>
   1.333 -    if heaviness_of_level level = Heavy then
   1.334 +    if granularity_of_type_level level = All_Vars then
   1.335        []
   1.336      else
   1.337        let val n = length decls in
   1.338          (0 upto n - 1 ~~ decls)
   1.339 -        |> maps (formula_lines_for_nonuniform_tags_sym_decl ctxt format
   1.340 -                     conj_sym_kind mono type_enc n s)
   1.341 +        |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono
   1.342 +                                                 type_enc n s)
   1.343        end
   1.344  
   1.345  fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc