929 else t |> Envir.eta_contract |> do_lambdas ctxt Ts |
929 else t |> Envir.eta_contract |> do_lambdas ctxt Ts |
930 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single |
930 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single |
931 in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end |
931 in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end |
932 end |
932 end |
933 |
933 |
934 fun do_conceal_lambdas Ts (t1 $ t2) = |
934 fun do_cheaply_conceal_lambdas Ts (t1 $ t2) = |
935 do_conceal_lambdas Ts t1 $ do_conceal_lambdas Ts t2 |
935 do_cheaply_conceal_lambdas Ts t1 |
936 | do_conceal_lambdas Ts (Abs (_, T, t)) = |
936 $ do_cheaply_conceal_lambdas Ts t2 |
937 (* slightly unsound because of hash collisions *) |
937 | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) = |
938 Free (polymorphic_free_prefix ^ serial_string (), T --> fastype_of1 (Ts, t)) |
938 Free (polymorphic_free_prefix ^ serial_string (), |
939 | do_conceal_lambdas _ t = t |
939 T --> fastype_of1 (T :: Ts, t)) |
|
940 | do_cheaply_conceal_lambdas _ t = t |
940 |
941 |
941 fun do_introduce_combinators ctxt Ts t = |
942 fun do_introduce_combinators ctxt Ts t = |
942 let val thy = Proof_Context.theory_of ctxt in |
943 let val thy = Proof_Context.theory_of ctxt in |
943 t |> conceal_bounds Ts |
944 t |> conceal_bounds Ts |
944 |> cterm_of thy |
945 |> cterm_of thy |
945 |> Meson_Clausify.introduce_combinators_in_cterm |
946 |> Meson_Clausify.introduce_combinators_in_cterm |
946 |> prop_of |> Logic.dest_equals |> snd |
947 |> prop_of |> Logic.dest_equals |> snd |
947 |> reveal_bounds Ts |
948 |> reveal_bounds Ts |
948 end |
949 end |
949 (* A type variable of sort "{}" will make abstraction fail. *) |
950 (* A type variable of sort "{}" will make abstraction fail. *) |
950 handle THM _ => t |> do_conceal_lambdas Ts |
951 handle THM _ => t |> do_cheaply_conceal_lambdas Ts |
951 val introduce_combinators = simple_translate_lambdas do_introduce_combinators |
952 val introduce_combinators = simple_translate_lambdas do_introduce_combinators |
952 |
953 |
953 fun preprocess_abstractions_in_terms trans_lambdas facts = |
954 fun preprocess_abstractions_in_terms trans_lambdas facts = |
954 let |
955 let |
955 val (facts, lambda_ts) = |
956 val (facts, lambda_ts) = |