src/HOL/Tools/ATP/atp_translate.ML
changeset 43677 2cd0b478d1b6
parent 43676 3b0b448b4d69
child 43678 56d352659500
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 05 17:09:59 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 05 17:09:59 2011 +0100
     1.3 @@ -442,11 +442,13 @@
     1.4  datatype combterm =
     1.5    CombConst of name * typ * typ list |
     1.6    CombVar of name * typ |
     1.7 -  CombApp of combterm * combterm
     1.8 +  CombApp of combterm * combterm |
     1.9 +  CombAbs of (name * typ) * combterm
    1.10  
    1.11  fun combtyp_of (CombConst (_, T, _)) = T
    1.12    | combtyp_of (CombVar (_, T)) = T
    1.13    | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))
    1.14 +  | combtyp_of (CombAbs ((_, T), tm)) = T --> combtyp_of tm
    1.15  
    1.16  (*gets the head of a combinator application, along with the list of arguments*)
    1.17  fun strip_combterm_comb u =
    1.18 @@ -490,7 +492,11 @@
    1.19    | combterm_from_term _ bs (Bound j) =
    1.20      nth bs j
    1.21      |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
    1.22 -  | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
    1.23 +  | combterm_from_term thy bs (Abs (s, T, t)) =
    1.24 +    let val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t in
    1.25 +      (CombAbs ((`make_bound_var s, T), tm),
    1.26 +       union (op =) atomic_Ts (atyps_of T))
    1.27 +    end
    1.28  
    1.29  datatype locality =
    1.30    General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
    1.31 @@ -697,6 +703,7 @@
    1.32  fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
    1.33    | combterm_vars (CombConst _) = I
    1.34    | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
    1.35 +  | combterm_vars (CombAbs (_, tm)) = combterm_vars tm
    1.36  fun close_combformula_universally phi = close_universally combterm_vars phi
    1.37  
    1.38  fun term_vars bounds (ATerm (name as (s, _), tms)) =
    1.39 @@ -760,7 +767,7 @@
    1.40        | to_ho _ = raise Fail "unexpected type abstraction"
    1.41    in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
    1.42  
    1.43 -fun mangled_type format type_enc pred_sym ary =
    1.44 +fun ho_type_from_typ format type_enc pred_sym ary =
    1.45    ho_type_from_ho_term type_enc pred_sym ary
    1.46    o ho_term_from_typ format type_enc
    1.47  
    1.48 @@ -818,6 +825,7 @@
    1.49               (proxy_base |>> prefix const_prefix, T_args)
    1.50            | NONE => (name, T_args))
    1.51          |> (fn (name, T_args) => CombConst (name, T, T_args))
    1.52 +      | intro _ (CombAbs (bound, tm)) = CombAbs (bound, intro false tm)
    1.53        | intro _ tm = tm
    1.54    in intro true end
    1.55  
    1.56 @@ -929,7 +937,7 @@
    1.57        | aux t = t
    1.58    in t |> exists_subterm is_Var t ? aux end
    1.59  
    1.60 -fun preprocess_prop ctxt presimp_consts kind t =
    1.61 +fun preprocess_prop ctxt type_enc presimp_consts kind t =
    1.62    let
    1.63      val thy = Proof_Context.theory_of ctxt
    1.64      val t = t |> Envir.beta_eta_contract
    1.65 @@ -942,7 +950,8 @@
    1.66        |> extensionalize_term ctxt
    1.67        |> presimplify_term ctxt presimp_consts
    1.68        |> perhaps (try (HOLogic.dest_Trueprop))
    1.69 -      |> introduce_combinators_in_term ctxt kind
    1.70 +      |> not (is_type_enc_higher_order type_enc)
    1.71 +         ? introduce_combinators_in_term ctxt kind
    1.72    end
    1.73  
    1.74  (* making fact and conjecture formulas *)
    1.75 @@ -958,7 +967,7 @@
    1.76  fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts
    1.77                ((name, loc), t) =
    1.78    let val thy = Proof_Context.theory_of ctxt in
    1.79 -    case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
    1.80 +    case t |> preproc ? preprocess_prop ctxt type_enc presimp_consts Axiom
    1.81             |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
    1.82                             loc Axiom of
    1.83        formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
    1.84 @@ -982,7 +991,7 @@
    1.85                      else I)
    1.86                in
    1.87                  t |> preproc ?
    1.88 -                     (preprocess_prop ctxt presimp_consts kind #> freeze_term)
    1.89 +                     (preprocess_prop ctxt type_enc presimp_consts kind #> freeze_term)
    1.90                    |> make_formula thy type_enc (format <> CNF) (string_of_int j)
    1.91                                    Local kind
    1.92                    |> maybe_negate
    1.93 @@ -1260,6 +1269,7 @@
    1.94               | No_Type_Args => (name, [])
    1.95             end)
    1.96          |> (fn (name, T_args) => CombConst (name, T, T_args))
    1.97 +      | aux _ (CombAbs (bound, tm)) = CombAbs (bound, aux 0 tm)
    1.98        | aux _ tm = tm
    1.99    in aux 0 end
   1.100  
   1.101 @@ -1455,32 +1465,36 @@
   1.102      formula_fold pos (is_var_positively_naked_in_term name) phi false
   1.103    | should_predicate_on_var_in_formula _ _ _ _ = true
   1.104  
   1.105 -fun mk_const_aterm format type_enc x T_args args =
   1.106 -  ATerm (x, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
   1.107 +fun mk_aterm format type_enc name T_args args =
   1.108 +  ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
   1.109  
   1.110  fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
   1.111    CombConst (type_tag, T --> T, [T])
   1.112    |> enforce_type_arg_policy_in_combterm ctxt format type_enc
   1.113 -  |> term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
   1.114 +  |> ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
   1.115    |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
   1.116 -and term_from_combterm ctxt format nonmono_Ts type_enc =
   1.117 +and ho_term_from_combterm ctxt format nonmono_Ts type_enc =
   1.118    let
   1.119      fun aux site u =
   1.120        let
   1.121          val (head, args) = strip_combterm_comb u
   1.122 -        val (x as (s, _), T_args) =
   1.123 -          case head of
   1.124 -            CombConst (name, _, T_args) => (name, T_args)
   1.125 -          | CombVar (name, _) => (name, [])
   1.126 -          | CombApp _ => raise Fail "impossible \"CombApp\""
   1.127 -        val (pos, arg_site) =
   1.128 +        val pos =
   1.129            case site of
   1.130 -            Top_Level pos =>
   1.131 -            (pos, if is_tptp_equal s then Eq_Arg pos else Elsewhere)
   1.132 -          | Eq_Arg pos => (pos, Elsewhere)
   1.133 -          | Elsewhere => (NONE, Elsewhere)
   1.134 -        val t = mk_const_aterm format type_enc x T_args
   1.135 -                    (map (aux arg_site) args)
   1.136 +            Top_Level pos => pos
   1.137 +          | Eq_Arg pos => pos
   1.138 +          | Elsewhere => NONE
   1.139 +        val t =
   1.140 +          case head of
   1.141 +            CombConst (name as (s, _), _, T_args) =>
   1.142 +            let
   1.143 +              val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
   1.144 +            in
   1.145 +              mk_aterm format type_enc name T_args (map (aux arg_site) args)
   1.146 +            end
   1.147 +          | CombVar (name, _) => mk_aterm format type_enc name [] []
   1.148 +          | CombAbs ((name, T), tm) =>
   1.149 +            AAbs ((name, ho_type_from_typ format type_enc true 0 T), aux Elsewhere tm)
   1.150 +          | CombApp _ => raise Fail "impossible \"CombApp\""
   1.151          val T = combtyp_of u
   1.152        in
   1.153          t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
   1.154 @@ -1493,12 +1507,12 @@
   1.155                               should_predicate_on_var =
   1.156    let
   1.157      fun do_term pos =
   1.158 -      term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
   1.159 +      ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
   1.160      val do_bound_type =
   1.161        case type_enc of
   1.162          Simple_Types (_, level) =>
   1.163          homogenized_type ctxt nonmono_Ts level 0
   1.164 -        #> mangled_type format type_enc false 0 #> SOME
   1.165 +        #> ho_type_from_typ format type_enc false 0 #> SOME
   1.166        | _ => K NONE
   1.167      fun do_out_of_bound_type pos phi universal (name, T) =
   1.168        if should_predicate_on_type ctxt nonmono_Ts type_enc
   1.169 @@ -1673,7 +1687,7 @@
   1.170    in
   1.171      Decl (sym_decl_prefix ^ s, (s, s'),
   1.172            (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
   1.173 -          |> mangled_type format type_enc pred_sym (length T_arg_Ts + ary))
   1.174 +          |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
   1.175    end
   1.176  
   1.177  fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
   1.178 @@ -1723,7 +1737,7 @@
   1.179      val bound_names =
   1.180        1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
   1.181      val bounds = bound_names |> map (fn name => ATerm (name, []))
   1.182 -    val cst = mk_const_aterm format type_enc (s, s') T_args
   1.183 +    val cst = mk_aterm format type_enc (s, s') T_args
   1.184      val atomic_Ts = atyps_of T
   1.185      fun eq tms =
   1.186        (if pred_sym then AConn (AIff, map AAtom tms)