(*  Title:      HOL/Tools/ATP/atp_proof_reconstruct.ML

     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory

     Author:     Claire Quigley, Cambridge University Computer Laboratory

     Author:     Jasmin Blanchette, TU Muenchen

 Basic proof reconstruction from ATP proofs.

 *)

 signature ATP_PROOF_RECONSTRUCT =

 sig

   type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term

   type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula

   type stature = ATP_Problem_Generate.stature

   type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step

   type 'a atp_proof = 'a ATP_Proof.atp_proof

   val metisN : string

   val full_typesN : string

   val partial_typesN : string

   val no_typesN : string

   val really_full_type_enc : string

   val full_type_enc : string

   val partial_type_enc : string

   val no_type_enc : string

   val full_type_encs : string list

   val partial_type_encs : string list

   val default_metis_lam_trans : string

   val metis_call : string -> string -> string

   val forall_of : term -> term -> term

   val exists_of : term -> term -> term

   val unalias_type_enc : string -> string list

   val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option ->

     (string, string) atp_term -> term

   val prop_of_atp : Proof.context -> bool -> int Symtab.table ->

     (string, string, (string, string) atp_term, string) atp_formula -> term

   val used_facts_in_atp_proof :

     Proof.context -> (string * stature) list vector -> string atp_proof -> (string * stature) list

   val used_facts_in_unsound_atp_proof : Proof.context -> (string * stature) list vector ->

     'a atp_proof -> string list option

   val lam_trans_of_atp_proof : string atp_proof -> string -> string

   val is_typed_helper_used_in_atp_proof : string atp_proof -> bool

   val termify_atp_proof : Proof.context -> string Symtab.table -> (string * term) list ->

     int Symtab.table -> string atp_proof -> (term, string) atp_step list

   val factify_atp_proof : (string * 'a) list vector -> term list -> term ->

     (term, string) atp_step list -> (term, string) atp_step list

 end;

 structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT =

 struct

 open ATP_Util

 open ATP_Problem

 open ATP_Proof

 open ATP_Problem_Generate

 val metisN = "metis"

 val full_typesN = "full_types"

 val partial_typesN = "partial_types"

 val no_typesN = "no_types"

 val really_full_type_enc = "mono_tags"

 val full_type_enc = "poly_guards_query"

 val partial_type_enc = "poly_args"

 val no_type_enc = "erased"

 val full_type_encs = [full_type_enc, really_full_type_enc]

 val partial_type_encs = partial_type_enc :: full_type_encs

 val type_enc_aliases =

   [(full_typesN, full_type_encs),

    (partial_typesN, partial_type_encs),

    (no_typesN, [no_type_enc])]

 fun unalias_type_enc s =

   AList.lookup (op =) type_enc_aliases s |> the_default [s]

 val default_metis_lam_trans = combsN

 fun metis_call type_enc lam_trans =

   let

     val type_enc =

       case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases

                       type_enc of

         [alias] => alias

       | _ => type_enc

     val opts = [] |> type_enc <> partial_typesN ? cons type_enc

                   |> lam_trans <> default_metis_lam_trans ? cons lam_trans

   in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end

 fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s

   | term_name' _ = ""

 fun lambda' v = Term.lambda_name (term_name' v, v)

 fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda' v t

 fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda' v t

 fun make_tfree ctxt w =

   let val ww = "'" ^ w in

     TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))

   end

 exception ATP_TERM of (string, string) atp_term list

 exception ATP_FORMULA of

     (string, string, (string, string) atp_term, string) atp_formula list

 exception SAME of unit

 (* Type variables are given the basic sort "HOL.type". Some will later be

    constrained by information from type literals, or by type inference. *)

 fun typ_of_atp ctxt (u as ATerm ((a, _), us)) =

   let val Ts = map (typ_of_atp ctxt) us in

     case unprefix_and_unascii type_const_prefix a of

       SOME b => Type (invert_const b, Ts)

     | NONE =>

       if not (null us) then

         raise ATP_TERM [u]  (* only "tconst"s have type arguments *)

       else case unprefix_and_unascii tfree_prefix a of

         SOME b => make_tfree ctxt b

       | NONE =>

         (* Could be an Isabelle variable or a variable from the ATP, say "X1"

            or "_5018". Sometimes variables from the ATP are indistinguishable

            from Isabelle variables, which forces us to use a type parameter in

            all cases. *)

         (a |> perhaps (unprefix_and_unascii tvar_prefix), HOLogic.typeS)

         |> Type_Infer.param 0

   end

 (* Type class literal applied to a type. Returns triple of polarity, class,

    type. *)

 fun type_constraint_of_term ctxt (u as ATerm ((a, _), us)) =

   case (unprefix_and_unascii class_prefix a, map (typ_of_atp ctxt) us) of

     (SOME b, [T]) => (b, T)

   | _ => raise ATP_TERM [u]

 (* Accumulate type constraints in a formula: negative type literals. *)

 fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)

 fun add_type_constraint false (cl, TFree (a ,_)) = add_var ((a, ~1), cl)

   | add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)

   | add_type_constraint _ _ = I

 fun repair_var_name s =

   let

     fun subscript_name s n = s ^ nat_subscript n

     val s = s |> String.map Char.toLower

   in

     case space_explode "_" s of

       [_] => (case take_suffix Char.isDigit (String.explode s) of

                 (cs1 as _ :: _, cs2 as _ :: _) =>

                 subscript_name (String.implode cs1)

                                (the (Int.fromString (String.implode cs2)))

               | (_, _) => s)

     | [s1, s2] => (case Int.fromString s2 of

                      SOME n => subscript_name s1 n

                    | NONE => s)

     | _ => s

   end

 (* The number of type arguments of a constant, zero if it's monomorphic. For

    (instances of) Skolem pseudoconstants, this information is encoded in the

    constant name. *)

 fun robust_const_num_type_args thy s =

   if String.isPrefix skolem_const_prefix s then

     s |> Long_Name.explode |> List.last |> Int.fromString |> the

   else if String.isPrefix lam_lifted_prefix s then

     if String.isPrefix lam_lifted_poly_prefix s then 2 else 0

   else

     (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length

 fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT

 (* Cope with "tt(X) = X" atoms, where "X" is existentially quantified. *)

 fun loose_aconv (Free (s, _), Free (s', _)) = s = s'

   | loose_aconv (t, t') = t aconv t'

 val vampire_skolem_prefix = "sK"

 (* First-order translation. No types are known for variables. "HOLogic.typeT"

    should allow them to be inferred. *)

 fun term_of_atp ctxt textual sym_tab =

   let

     val thy = Proof_Context.theory_of ctxt

     (* For Metis, we use 1 rather than 0 because variable references in clauses

        may otherwise conflict with variable constraints in the goal. At least,

        type inference often fails otherwise. See also "axiom_inference" in

        "Metis_Reconstruct". *)

     val var_index = if textual then 0 else 1

     fun do_term extra_ts opt_T u =

       case u of

         ATerm ((s, _), us) =>

         if s = ""

           then error "Isar proof reconstruction failed because the ATP proof \

                      \contains unparsable material."

         else if String.isPrefix native_type_prefix s then

           @{const True} (* ignore TPTP type information *)

         else if s = tptp_equal then

           let val ts = map (do_term [] NONE) us in

             if textual andalso length ts = 2 andalso

                loose_aconv (hd ts, List.last ts) then

               @{const True}

             else

               list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)

           end

         else case unprefix_and_unascii const_prefix s of

           SOME s' =>

           let

             val ((s', s''), mangled_us) =

               s' |> unmangled_const |>> `invert_const

           in

             if s' = type_tag_name then

               case mangled_us @ us of

                 [typ_u, term_u] =>

                 do_term extra_ts (SOME (typ_of_atp ctxt typ_u)) term_u

               | _ => raise ATP_TERM us

             else if s' = predicator_name then

               do_term [] (SOME @{typ bool}) (hd us)

             else if s' = app_op_name then

               let val extra_t = do_term [] NONE (List.last us) in

                 do_term (extra_t :: extra_ts)

                         (case opt_T of

                            SOME T => SOME (slack_fastype_of extra_t --> T)

                          | NONE => NONE)

                         (nth us (length us - 2))

               end

             else if s' = type_guard_name then

               @{const True} (* ignore type predicates *)

             else

               let

                 val new_skolem = String.isPrefix new_skolem_const_prefix s''

                 val num_ty_args =

                   length us - the_default 0 (Symtab.lookup sym_tab s)

                 val (type_us, term_us) =

                   chop num_ty_args us |>> append mangled_us

                 val term_ts = map (do_term [] NONE) term_us

                 val T =

                   (if not (null type_us) andalso

                       robust_const_num_type_args thy s' = length type_us then

                      let val Ts = type_us |> map (typ_of_atp ctxt) in

                        if new_skolem then

                          SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts))

                        else if textual then

                          try (Sign.const_instance thy) (s', Ts)

                        else

                          NONE

                      end

                    else

                      NONE)

                   |> (fn SOME T => T

                        | NONE => map slack_fastype_of term_ts --->

                                  (case opt_T of

                                     SOME T => T

                                   | NONE => HOLogic.typeT))

                 val t =

                   if new_skolem then

                     Var ((new_skolem_var_name_of_const s'', var_index), T)

                   else

                     Const (unproxify_const s', T)

               in list_comb (t, term_ts @ extra_ts) end

           end

         | NONE => (* a free or schematic variable *)

           let

             (* This assumes that distinct names are mapped to distinct names by

                "Variable.variant_frees". This does not hold in general but

                should hold for ATP-generated Skolem function names, since these

                end with a digit and "variant_frees" appends letters. *)

             fun fresh_up s =

               [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst

             val term_ts =

               map (do_term [] NONE) us

               (* Vampire (2.6) passes arguments to Skolem functions in reverse

                  order *)

               |> String.isPrefix vampire_skolem_prefix s ? rev

             val ts = term_ts @ extra_ts

             val T =

               case opt_T of

                 SOME T => map slack_fastype_of term_ts ---> T

               | NONE => map slack_fastype_of ts ---> HOLogic.typeT

             val t =

               case unprefix_and_unascii fixed_var_prefix s of

                 SOME s => Free (s, T)

               | NONE =>

                 case unprefix_and_unascii schematic_var_prefix s of

                   SOME s => Var ((s, var_index), T)

                 | NONE =>

                   if textual andalso not (is_tptp_variable s) then

                     Free (s |> textual ? (repair_var_name #> fresh_up), T)

                   else

                     Var ((s |> textual ? repair_var_name, var_index), T)

           in list_comb (t, ts) end

   in do_term [] end

 fun term_of_atom ctxt textual sym_tab pos (u as ATerm ((s, _), _)) =

   if String.isPrefix class_prefix s then

     add_type_constraint pos (type_constraint_of_term ctxt u)

     #> pair @{const True}

   else

     pair (term_of_atp ctxt textual sym_tab (SOME @{typ bool}) u)

 (* Update schematic type variables with detected sort constraints. It's not

    totally clear whether this code is necessary. *)

 fun repair_tvar_sorts (t, tvar_tab) =

   let

     fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)

       | do_type (TVar (xi, s)) =

         TVar (xi, the_default s (Vartab.lookup tvar_tab xi))

       | do_type (TFree z) = TFree z

     fun do_term (Const (a, T)) = Const (a, do_type T)

       | do_term (Free (a, T)) = Free (a, do_type T)

       | do_term (Var (xi, T)) = Var (xi, do_type T)

       | do_term (t as Bound _) = t

       | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)

       | do_term (t1 $ t2) = do_term t1 $ do_term t2

   in t |> not (Vartab.is_empty tvar_tab) ? do_term end

 fun quantify_over_var quant_of var_s t =

   let

     val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)

     val normTs = vars |> AList.group (op =) |> map (apsnd hd)

     fun norm_var_types (Var (x, T)) =

         Var (x, case AList.lookup (op =) normTs x of

                   NONE => T

                 | SOME T' => T')

       | norm_var_types t = t

   in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end

 (* Interpret an ATP formula as a HOL term, extracting sort constraints as they

    appear in the formula. *)

 fun prop_of_atp ctxt textual sym_tab phi =

   let

     fun do_formula pos phi =

       case phi of

         AQuant (_, [], phi) => do_formula pos phi

       | AQuant (q, (s, _) :: xs, phi') =>

         do_formula pos (AQuant (q, xs, phi'))

         (* FIXME: TFF *)

         #>> quantify_over_var

               (case q of AForall => forall_of | AExists => exists_of)

               (s |> textual ? repair_var_name)

       | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not

       | AConn (c, [phi1, phi2]) =>

         do_formula (pos |> c = AImplies ? not) phi1

         ##>> do_formula pos phi2

         #>> (case c of

                AAnd => s_conj

              | AOr => s_disj

              | AImplies => s_imp

              | AIff => s_iff

              | ANot => raise Fail "impossible connective")

       | AAtom tm => term_of_atom ctxt textual sym_tab pos tm

       | _ => raise ATP_FORMULA [phi]

   in repair_tvar_sorts (do_formula true phi Vartab.empty) end

 fun find_first_in_list_vector vec key =

   Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key

                  | (_, value) => value) NONE vec

 val unprefix_fact_number = space_implode "_" o tl o space_explode "_"

 fun resolve_one_named_fact fact_names s =

   case try (unprefix fact_prefix) s of

     SOME s' =>

     let val s' = s' |> unprefix_fact_number |> unascii_of in

       s' |> find_first_in_list_vector fact_names |> Option.map (pair s')

     end

   | NONE => NONE

 fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names)

 fun resolve_one_named_conjecture s =

   case try (unprefix conjecture_prefix) s of

     SOME s' => Int.fromString s'

   | NONE => NONE

 val resolve_conjecture = map_filter resolve_one_named_conjecture

 fun is_axiom_used_in_proof pred =

   exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)

 fun add_non_rec_defs fact_names accum =

   Vector.foldl (fn (facts, facts') =>

       union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts)

             facts')

     accum fact_names

 val isa_ext = Thm.get_name_hint @{thm ext}

 val isa_short_ext = Long_Name.base_name isa_ext

 fun ext_name ctxt =

   if Thm.eq_thm_prop (@{thm ext},

        singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then

     isa_short_ext

   else

     isa_ext

 val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"

 val leo2_unfold_def_rule = "unfold_def"

 fun add_fact ctxt fact_names ((_, ss), _, _, rule, deps) =

   (if rule = leo2_extcnf_equal_neg_rule then

      insert (op =) (ext_name ctxt, (Global, General))

    else if rule = leo2_unfold_def_rule then

      (* LEO 1.3.3 does not record definitions properly, leading to missing

         dependencies in the TSTP proof. Remove the next line once this is

         fixed. *)

      add_non_rec_defs fact_names

    else if rule = agsyhol_coreN orelse rule = satallax_coreN then

      (fn [] =>

          (* agsyHOL and Satallax don't include definitions in their

             unsatisfiable cores, so we assume the worst and include them all

             here. *)

          [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names

        | facts => facts)

    else

      I)

   #> (if null deps then union (op =) (resolve_fact fact_names ss) else I)

 fun used_facts_in_atp_proof ctxt fact_names atp_proof =

   if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names

   else fold (add_fact ctxt fact_names) atp_proof []

 fun used_facts_in_unsound_atp_proof _ _ [] = NONE

   | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =

     let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in

       if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso

          not (is_axiom_used_in_proof (not o null o resolve_conjecture o single) atp_proof) then

         SOME (map fst used_facts)

       else

         NONE

     end

 val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix

 (* overapproximation (good enough) *)

 fun is_lam_lifted s =

   String.isPrefix fact_prefix s andalso

   String.isSubstring ascii_of_lam_fact_prefix s

 val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix)

 fun lam_trans_of_atp_proof atp_proof default =

   case (is_axiom_used_in_proof is_combinator_def atp_proof,

         is_axiom_used_in_proof is_lam_lifted atp_proof) of

     (false, false) => default

   | (false, true) => liftingN

 (*  | (true, true) => combs_and_liftingN -- not supported by "metis" *)

   | (true, _) => combsN

 val is_typed_helper_name =

   String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix

 fun is_typed_helper_used_in_atp_proof atp_proof =

   is_axiom_used_in_proof is_typed_helper_name atp_proof

 fun repair_name "$true" = "c_True"

   | repair_name "$false" = "c_False"

   | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *)

   | repair_name s =

     if is_tptp_equal s orelse

        (* seen in Vampire proofs *)

        (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then

       tptp_equal

     else

       s

 fun infer_formula_types ctxt =

   Type.constraint HOLogic.boolT

   #> Syntax.check_term

          (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)

 val combinator_table =

   [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}),

    (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}),

    (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}),

    (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}),

    (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})]

 fun uncombine_term thy =

   let

     fun aux (t1 $ t2) = betapply (pairself aux (t1, t2))

       | aux (Abs (s, T, t')) = Abs (s, T, aux t')

       | aux (t as Const (x as (s, _))) =

         (case AList.lookup (op =) combinator_table s of

            SOME thm => thm |> prop_of |> specialize_type thy x

                            |> Logic.dest_equals |> snd

          | NONE => t)

       | aux t = t

   in aux end

 fun unlift_term lifted =

   map_aterms (fn t as Const (s, _) =>

                  if String.isPrefix lam_lifted_prefix s then

                    case AList.lookup (op =) lifted s of

                      SOME t =>

                      (* FIXME: do something about the types *)

                      unlift_term lifted t

                    | NONE => t

                  else

                    t

                | t => t)

 fun decode_line ctxt lifted sym_tab (name, role, u, rule, deps) =

   let

     val thy = Proof_Context.theory_of ctxt

     val t =

       u |> prop_of_atp ctxt true sym_tab

         |> uncombine_term thy

         |> unlift_term lifted

         |> infer_formula_types ctxt

   in (name, role, t, rule, deps) end

 val waldmeister_conjecture_num = "1.0.0.0"

 fun repair_waldmeister_endgame arg =

   let

     fun do_tail (name, _, t, rule, deps) =

       (name, Negated_Conjecture, s_not t, rule, deps)

     fun do_body [] = []

       | do_body ((line as ((num, _), _, _, _, _)) :: lines) =

         if num = waldmeister_conjecture_num then map do_tail (line :: lines)

         else line :: do_body lines

   in do_body arg end

 fun termify_atp_proof ctxt pool lifted sym_tab =

   clean_up_atp_proof_dependencies

   #> nasty_atp_proof pool

   #> map_term_names_in_atp_proof repair_name

   #> map (decode_line ctxt lifted sym_tab)

   #> repair_waldmeister_endgame

 fun factify_atp_proof fact_names hyp_ts concl_t atp_proof =

   let

     fun factify_step ((num, ss), role, t, rule, deps) =

       let

         val (ss', role', t') =

           (case resolve_conjecture ss of

             [j] =>

             if j = length hyp_ts then ([], Conjecture, concl_t) else ([], Hypothesis, nth hyp_ts j)

            | _ =>

              (case resolve_fact fact_names ss of

                [] => (ss, Plain, t)

              | facts => (map fst facts, Axiom, t)))

       in

         ((num, ss'), role', t', rule, deps)

       end

     val atp_proof = map factify_step atp_proof

     val names = map #1 atp_proof

     fun repair_dep (num, ss) = (num, the_default ss (AList.lookup (op =) names num))

     fun repair_deps (name, role, t, rule, deps) = (name, role, t, rule, map repair_dep deps)

   in map repair_deps atp_proof end

 end;