src/HOL/Tools/ATP/atp_translate.ML
changeset 44774 72785558a6ff
parent 44773 e701dabbfe37
child 44782 ba4c0205267f
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 09:10:41 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 09:10:41 2011 +0200
     1.3 @@ -710,23 +710,22 @@
     1.4      level_of_type_enc type_enc = All_Types
     1.5  
     1.6  fun type_arg_policy type_enc s =
     1.7 -  if s = type_tag_name then
     1.8 -    if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
     1.9 -      Mangled_Type_Args
    1.10 -    else
    1.11 -      Explicit_Type_Args false
    1.12 -  else case type_enc of
    1.13 -    Tags (_, All_Types) => No_Type_Args
    1.14 -  | _ =>
    1.15 -    let val level = level_of_type_enc type_enc in
    1.16 -      if level = No_Types orelse s = @{const_name HOL.eq} orelse
    1.17 -         (s = app_op_name andalso level = Const_Arg_Types) then
    1.18 -        No_Type_Args
    1.19 -      else if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
    1.20 -        Mangled_Type_Args
    1.21 -      else
    1.22 -        Explicit_Type_Args (should_drop_arg_type_args type_enc)
    1.23 -    end
    1.24 +  let val mangled = (polymorphism_of_type_enc type_enc = Mangled_Monomorphic) in
    1.25 +    if s = type_tag_name then
    1.26 +      if mangled then Mangled_Type_Args else Explicit_Type_Args false
    1.27 +    else case type_enc of
    1.28 +      Tags (_, All_Types) => No_Type_Args
    1.29 +    | _ =>
    1.30 +      let val level = level_of_type_enc type_enc in
    1.31 +        if level = No_Types orelse s = @{const_name HOL.eq} orelse
    1.32 +           (s = app_op_name andalso level = Const_Arg_Types) then
    1.33 +          No_Type_Args
    1.34 +        else if mangled then
    1.35 +          Mangled_Type_Args
    1.36 +        else
    1.37 +          Explicit_Type_Args (should_drop_arg_type_args type_enc)
    1.38 +      end
    1.39 +  end
    1.40  
    1.41  (* Make atoms for sorted type variables. *)
    1.42  fun generic_add_sorts_on_type (_, []) = I
    1.43 @@ -955,13 +954,32 @@
    1.44        | intro _ _ tm = tm
    1.45    in intro true [] end
    1.46  
    1.47 +fun mangle_type_args_in_iterm format type_enc =
    1.48 +  if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
    1.49 +    let
    1.50 +      fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
    1.51 +        | mangle (tm as IConst (_, _, [])) = tm
    1.52 +        | mangle (tm as IConst (name as (s, _), T, T_args)) =
    1.53 +          (case strip_prefix_and_unascii const_prefix s of
    1.54 +             NONE => tm
    1.55 +           | SOME s'' =>
    1.56 +             case type_arg_policy type_enc (invert_const s'') of
    1.57 +               Mangled_Type_Args =>
    1.58 +               IConst (mangled_const_name format type_enc T_args name, T, [])
    1.59 +             | _ => tm)
    1.60 +        | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
    1.61 +        | mangle tm = tm
    1.62 +    in mangle end
    1.63 +  else
    1.64 +    I
    1.65 +
    1.66  fun chop_fun 0 T = ([], T)
    1.67    | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
    1.68      chop_fun (n - 1) ran_T |>> cons dom_T
    1.69    | chop_fun _ T = ([], T)
    1.70  
    1.71 -fun filter_type_args _ _ _ [] = []
    1.72 -  | filter_type_args thy s ary T_args =
    1.73 +fun filter_const_type_args _ _ _ [] = []
    1.74 +  | filter_const_type_args thy s ary T_args =
    1.75      let
    1.76        val U = robust_const_type thy s
    1.77        val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
    1.78 @@ -973,31 +991,33 @@
    1.79      end
    1.80      handle TYPE _ => T_args
    1.81  
    1.82 -fun enforce_type_arg_policy_in_iterm ctxt format type_enc =
    1.83 +fun filter_type_args_in_iterm thy type_enc =
    1.84    let
    1.85 -    val thy = Proof_Context.theory_of ctxt
    1.86 -    fun aux ary (IApp (tm1, tm2)) = IApp (aux (ary + 1) tm1, aux 0 tm2)
    1.87 -      | aux ary (IConst (name as (s, _), T, T_args)) =
    1.88 +    fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
    1.89 +      | filt _ (tm as IConst (_, _, [])) = tm
    1.90 +      | filt ary (IConst (name as (s, _), T, T_args)) =
    1.91          (case strip_prefix_and_unascii const_prefix s of
    1.92             NONE =>
    1.93 -           (name, if level_of_type_enc type_enc = No_Types orelse s = tptp_choice
    1.94 -                  then [] else T_args)
    1.95 +           (name,
    1.96 +            if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then
    1.97 +              []
    1.98 +            else
    1.99 +              T_args)
   1.100           | SOME s'' =>
   1.101             let
   1.102               val s'' = invert_const s''
   1.103               fun filter_T_args false = T_args
   1.104 -               | filter_T_args true = filter_type_args thy s'' ary T_args
   1.105 +               | filter_T_args true = filter_const_type_args thy s'' ary T_args
   1.106             in
   1.107               case type_arg_policy type_enc s'' of
   1.108                 Explicit_Type_Args drop_args => (name, filter_T_args drop_args)
   1.109 -             | Mangled_Type_Args =>
   1.110 -               (mangled_const_name format type_enc T_args name, [])
   1.111               | No_Type_Args => (name, [])
   1.112 +             | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
   1.113             end)
   1.114          |> (fn (name, T_args) => IConst (name, T, T_args))
   1.115 -      | aux _ (IAbs (bound, tm)) = IAbs (bound, aux 0 tm)
   1.116 -      | aux _ tm = tm
   1.117 -  in aux 0 end
   1.118 +      | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
   1.119 +      | filt _ tm = tm
   1.120 +  in filt 0 end
   1.121  
   1.122  fun iformula_from_prop ctxt format type_enc eq_as_iff =
   1.123    let
   1.124 @@ -1005,7 +1025,7 @@
   1.125      fun do_term bs t atomic_types =
   1.126        iterm_from_term thy format bs (Envir.eta_contract t)
   1.127        |>> (introduce_proxies_in_iterm type_enc
   1.128 -           #> enforce_type_arg_policy_in_iterm ctxt format type_enc
   1.129 +           #> mangle_type_args_in_iterm format type_enc
   1.130             #> AAtom)
   1.131        ||> union (op =) atomic_types
   1.132      fun do_quant bs q pos s T t' =
   1.133 @@ -1393,7 +1413,7 @@
   1.134  fun list_app head args = fold (curry (IApp o swap)) args head
   1.135  fun predicator tm = IApp (predicator_combconst, tm)
   1.136  
   1.137 -fun firstorderize_fact ctxt format type_enc sym_tab =
   1.138 +fun firstorderize_fact thy format type_enc sym_tab =
   1.139    let
   1.140      fun do_app arg head =
   1.141        let
   1.142 @@ -1401,7 +1421,7 @@
   1.143          val (arg_T, res_T) = dest_funT head_T
   1.144          val app =
   1.145            IConst (app_op, head_T --> head_T, [arg_T, res_T])
   1.146 -          |> enforce_type_arg_policy_in_iterm ctxt format type_enc
   1.147 +          |> mangle_type_args_in_iterm format type_enc
   1.148        in list_app app [head, arg] end
   1.149      fun list_app_ops head args = fold do_app args head
   1.150      fun introduce_app_ops tm =
   1.151 @@ -1420,6 +1440,7 @@
   1.152      val do_iterm =
   1.153        not (is_type_enc_higher_order type_enc)
   1.154        ? (introduce_app_ops #> introduce_predicators)
   1.155 +      #> filter_type_args_in_iterm thy type_enc
   1.156    in update_iformula (formula_map do_iterm) end
   1.157  
   1.158  (** Helper facts **)
   1.159 @@ -1621,9 +1642,9 @@
   1.160  
   1.161  val type_guard = `(make_fixed_const NONE) type_guard_name
   1.162  
   1.163 -fun type_guard_iterm ctxt format type_enc T tm =
   1.164 +fun type_guard_iterm format type_enc T tm =
   1.165    IApp (IConst (type_guard, T --> @{typ bool}, [T])
   1.166 -        |> enforce_type_arg_policy_in_iterm ctxt format type_enc, tm)
   1.167 +        |> mangle_type_args_in_iterm format type_enc, tm)
   1.168  
   1.169  fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
   1.170    | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
   1.171 @@ -1644,7 +1665,7 @@
   1.172  
   1.173  fun tag_with_type ctxt format mono type_enc pos T tm =
   1.174    IConst (type_tag, T --> T, [T])
   1.175 -  |> enforce_type_arg_policy_in_iterm ctxt format type_enc
   1.176 +  |> mangle_type_args_in_iterm format type_enc
   1.177    |> ho_term_from_iterm ctxt format mono type_enc (Top_Level pos)
   1.178    |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
   1.179         | _ => raise Fail "unexpected lambda-abstraction")
   1.180 @@ -1692,7 +1713,7 @@
   1.181        if should_guard_type ctxt mono type_enc
   1.182               (fn () => should_guard_var pos phi universal name) T then
   1.183          IVar (name, T)
   1.184 -        |> type_guard_iterm ctxt format type_enc T
   1.185 +        |> type_guard_iterm format type_enc T
   1.186          |> do_term pos |> AAtom |> SOME
   1.187        else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
   1.188          let
   1.189 @@ -1950,7 +1971,7 @@
   1.190             ascii_of (mangled_type format type_enc T),
   1.191             Axiom,
   1.192             IConst (`make_bound_var "X", T, [])
   1.193 -           |> type_guard_iterm ctxt format type_enc T
   1.194 +           |> type_guard_iterm format type_enc T
   1.195             |> AAtom
   1.196             |> formula_from_iformula ctxt format mono type_enc
   1.197                                      (K (K (K (K true)))) (SOME true)
   1.198 @@ -2026,7 +2047,7 @@
   1.199               (if n > 1 then "_" ^ string_of_int j else ""), kind,
   1.200               IConst ((s, s'), T, T_args)
   1.201               |> fold (curry (IApp o swap)) bounds
   1.202 -             |> type_guard_iterm ctxt format type_enc res_T
   1.203 +             |> type_guard_iterm format type_enc res_T
   1.204               |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
   1.205               |> formula_from_iformula ctxt format mono type_enc
   1.206                                        (K (K (K (K true)))) (SOME true)
   1.207 @@ -2156,6 +2177,7 @@
   1.208  fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
   1.209          lambda_trans readable_names preproc hyp_ts concl_t facts =
   1.210    let
   1.211 +    val thy = Proof_Context.theory_of ctxt
   1.212      val type_enc = type_enc |> adjust_type_enc format
   1.213      val lambda_trans =
   1.214        if lambda_trans = smartN then
   1.215 @@ -2189,7 +2211,7 @@
   1.216                           hyp_ts concl_t facts
   1.217      val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
   1.218      val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
   1.219 -    val firstorderize = firstorderize_fact ctxt format type_enc sym_tab
   1.220 +    val firstorderize = firstorderize_fact thy format type_enc sym_tab
   1.221      val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
   1.222      val sym_tab = conjs @ facts |> sym_table_for_facts ctxt (SOME false)
   1.223      val helpers =