src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42549 b9754f26c7bc
parent 42544 75cb06eee990
child 42551 cd99d6d3027a
equal deleted inserted replaced
42548:ea2a28b1938f 42549:b9754f26c7bc
   354               @{const True}
   354               @{const True}
   355             else
   355             else
   356               list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
   356               list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
   357           end
   357           end
   358         | SOME b =>
   358         | SOME b =>
   359           if b = boolify_base then
   359           let val (b, mangled_us) = b |> unmangled_const |>> invert_const in
   360             aux (SOME @{typ bool}) [] (hd us)
   360             if b = boolify_base then
   361           else if b = explicit_app_base then
   361               aux (SOME @{typ bool}) [] (hd us)
   362             aux opt_T (nth us 1 :: extra_us) (hd us)
   362             else if b = explicit_app_base then
   363           else
   363               aux opt_T (nth us 1 :: extra_us) (hd us)
   364             let
   364             else if b = type_pred_base then
   365               val (c, mangled_us) = b |> unmangled_const |>> invert_const
   365               @{const True}
   366               val num_ty_args = num_atp_type_args thy type_sys c
   366             else
   367               val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
   367               let
   368               (* Extra args from "hAPP" come after any arguments given directly
   368                 val num_ty_args = num_atp_type_args thy type_sys b
   369                  to the constant. *)
   369                 val (type_us, term_us) =
   370               val term_ts = map (aux NONE []) term_us
   370                   chop num_ty_args us |>> append mangled_us
   371               val extra_ts = map (aux NONE []) extra_us
   371                 (* Extra args from "hAPP" come after any arguments given
   372               val T =
   372                    directly to the constant. *)
   373                 case opt_T of
   373                 val term_ts = map (aux NONE []) term_us
   374                   SOME T => map fastype_of term_ts ---> T
   374                 val extra_ts = map (aux NONE []) extra_us
   375                 | NONE =>
   375                 val T =
   376                   if num_type_args thy c = length type_us then
   376                   case opt_T of
   377                     Sign.const_instance thy (c,
   377                     SOME T => map fastype_of term_ts ---> T
   378                         map (type_from_fo_term tfrees) type_us)
   378                   | NONE =>
   379                   else
   379                     if num_type_args thy b = length type_us then
   380                     HOLogic.typeT
   380                       Sign.const_instance thy
   381             in list_comb (Const (c, T), term_ts @ extra_ts) end
   381                           (b, map (type_from_fo_term tfrees) type_us)
       
   382                     else
       
   383                       HOLogic.typeT
       
   384               in list_comb (Const (b, T), term_ts @ extra_ts) end
       
   385           end
   382         | NONE => (* a free or schematic variable *)
   386         | NONE => (* a free or schematic variable *)
   383           let
   387           let
   384             val ts = map (aux NONE []) (us @ extra_us)
   388             val ts = map (aux NONE []) (us @ extra_us)
   385             val T = map fastype_of ts ---> HOLogic.typeT
   389             val T = map fastype_of ts ---> HOLogic.typeT
   386             val t =
   390             val t =