src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42544 75cb06eee990
parent 42541 8938507b2054
child 42549 b9754f26c7bc
equal deleted inserted replaced
42543:f9d402d144d4 42544:75cb06eee990
   339 fun raw_term_from_pred thy type_sys tfrees =
   339 fun raw_term_from_pred thy type_sys tfrees =
   340   let
   340   let
   341     fun aux opt_T extra_us u =
   341     fun aux opt_T extra_us u =
   342       case u of
   342       case u of
   343         ATerm (a, us) =>
   343         ATerm (a, us) =>
   344         if a = boolify_name then
   344         if a = type_tag_name then
   345           aux (SOME @{typ bool}) [] (hd us)
       
   346         else if a = explicit_app_name then
       
   347           aux opt_T (nth us 1 :: extra_us) (hd us)
       
   348         else if a = type_tag_name then
       
   349           case us of
   345           case us of
   350             [typ_u, term_u] =>
   346             [typ_u, term_u] =>
   351             aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
   347             aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
   352           | _ => raise FO_TERM us
   348           | _ => raise FO_TERM us
   353         else case strip_prefix_and_unascii const_prefix a of
   349         else case strip_prefix_and_unascii const_prefix a of
   358               @{const True}
   354               @{const True}
   359             else
   355             else
   360               list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
   356               list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
   361           end
   357           end
   362         | SOME b =>
   358         | SOME b =>
   363           let
   359           if b = boolify_base then
   364             val (c, mangled_us) = b |> unmangled_const |>> invert_const
   360             aux (SOME @{typ bool}) [] (hd us)
   365             val num_ty_args = num_atp_type_args thy type_sys c
   361           else if b = explicit_app_base then
   366             val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
   362             aux opt_T (nth us 1 :: extra_us) (hd us)
   367             (* Extra args from "hAPP" come after any arguments given directly to
   363           else
   368                the constant. *)
   364             let
   369             val term_ts = map (aux NONE []) term_us
   365               val (c, mangled_us) = b |> unmangled_const |>> invert_const
   370             val extra_ts = map (aux NONE []) extra_us
   366               val num_ty_args = num_atp_type_args thy type_sys c
   371             val T =
   367               val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
   372               case opt_T of
   368               (* Extra args from "hAPP" come after any arguments given directly
   373                 SOME T => map fastype_of term_ts ---> T
   369                  to the constant. *)
   374               | NONE =>
   370               val term_ts = map (aux NONE []) term_us
   375                 if num_type_args thy c = length type_us then
   371               val extra_ts = map (aux NONE []) extra_us
   376                   Sign.const_instance thy (c,
   372               val T =
   377                       map (type_from_fo_term tfrees) type_us)
   373                 case opt_T of
   378                 else
   374                   SOME T => map fastype_of term_ts ---> T
   379                   HOLogic.typeT
   375                 | NONE =>
   380           in list_comb (Const (c, T), term_ts @ extra_ts) end
   376                   if num_type_args thy c = length type_us then
       
   377                     Sign.const_instance thy (c,
       
   378                         map (type_from_fo_term tfrees) type_us)
       
   379                   else
       
   380                     HOLogic.typeT
       
   381             in list_comb (Const (c, T), term_ts @ extra_ts) end
   381         | NONE => (* a free or schematic variable *)
   382         | NONE => (* a free or schematic variable *)
   382           let
   383           let
   383             val ts = map (aux NONE []) (us @ extra_us)
   384             val ts = map (aux NONE []) (us @ extra_us)
   384             val T = map fastype_of ts ---> HOLogic.typeT
   385             val T = map fastype_of ts ---> HOLogic.typeT
   385             val t =
   386             val t =