(*
  Redirect TSTP proofs and write all the intermediate FOF formulas as axioms to stdout
 *)

(*
 In order to compile, load with recent isabelle (55102:761e40ce91bc is known to work) and compile with:
  cc -o redirect redirect.o
    -L ~/.isabelle/contrib/polyml-5.5.1-1/x86_64-linux
    -lpolymain -lpolyml -lstdc++ -lpthread -ldl -lgmp -lm
*)

theory redirect imports Main begin

ML {*
open ATP_Util
open ATP_Problem
open ATP_Proof
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
open Sledgehammer_Util
open Sledgehammer_Reconstructor
open Sledgehammer_Proof
open Sledgehammer_Annotate
open Sledgehammer_Print
open Sledgehammer_Preplay
open Sledgehammer_Compress
open Sledgehammer_Try0
open Sledgehammer_Minimize_Isar;
structure String_Redirect = ATP_Proof_Redirect(
  type key = ATP_Proof.atp_step_name
  val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
  val string_of = fst);
open String_Redirect;
fun maybe_mk_Trueprop t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
*}

ML {*
fun raw_label_of_num num = (num, 0)

fun label_of_clause [(num, _)] = raw_label_of_num num
  | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0)

fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
  | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))

fun replace_one_dependency (old, new) dep =
  if is_same_atp_step dep old then new else [dep]
fun replace_dependencies_in_line p (name, role, t, rule, deps) =
  (name, role, t, rule, fold (union (op =) o replace_one_dependency p) deps [])

fun is_only_type_information t = t aconv @{term True}

fun s_maybe_not role = role <> Conjecture ? s_not

fun is_same_inference (role, t) (_, role', t', _, _) =
  s_maybe_not role t aconv s_maybe_not role' t'

fun add_line (name as (_, ss), role, t, rule, []) lines =
    (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
       definitions. *)
    if role = Conjecture orelse role = Negated_Conjecture orelse role = Hypothesis then
      (name, role, t, rule, []) :: lines
    else if role = Axiom then
      (* Facts are not proof lines. *)
      lines |> is_only_type_information t ? map (replace_dependencies_in_line (name, []))
    else
      map (replace_dependencies_in_line (name, [])) lines
  | add_line (line as (name, role, t, _, _)) lines =
    (* Type information will be deleted later; skip repetition test. *)
    if is_only_type_information t then
      line :: lines
    (* Is there a repetition? If so, replace later line by earlier one. *)
    else case take_prefix (not o is_same_inference (role, t)) lines of
      (_, []) => line :: lines
    | (pre, (name', _, _, _, _) :: post) =>
      line :: pre @ map (replace_dependencies_in_line (name', [name])) post

fun add_nontrivial_line (line as (name, _, t, _, [])) lines =
    if is_only_type_information t then delete_dependency name lines else line :: lines
  | add_nontrivial_line line lines = line :: lines
and delete_dependency name lines =
  fold_rev add_nontrivial_line
           (map (replace_dependencies_in_line (name, [])) lines) []

val e_skolemize_rule = "skolemize"
val vampire_skolemisation_rule = "skolemisation"

val is_skolemize_rule =
  member (op =) [e_skolemize_rule, vampire_skolemisation_rule]

fun add_desired_line (name as (_, ss), role, t, rule, deps) (j, lines) =
  (j + 1,
   if role <> Plain orelse is_skolemize_rule rule orelse
      (* the last line must be kept *)
      j = 0 orelse
      (not (is_only_type_information t) andalso
       null (Term.add_tvars t []) andalso
       length deps >= 2 andalso
       (* kill next to last line, which usually results in a trivial step *)
       j <> 1) then
     (name, role, t, rule, deps) :: lines  (* keep line *)
   else
     map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)

*}
ML {* val con = ATP_Systems.get_atp @{theory} "e" () *}
ML {*
fun fname_to_ap f =
  let
   val content = File.read (Path.explode f)
   val (s, st) = extract_tstplike_proof_and_outcome true (#proof_delims con) (#known_failures con) content
   val ap = atp_proof_of_tstplike_proof [] s
   val atp_proof = termify_atp_proof @{context} Symtab.empty [] Symtab.empty ap
   val atp_proof2 =
      atp_proof
      |> rpair [] |-> fold_rev add_line
      |> rpair [] |-> fold_rev add_nontrivial_line
      |> rpair (0, [])
      |-> fold_rev add_desired_line
      |> snd
  in (atp_proof2, atp_proof) end
*}
ML {* print_depth 100 *}

(*
ML {* val (atp_proof,atp_proof_whole) = fname_to_ap "/home/cek/obt3.proof";
  val bot = atp_proof |> List.last |> #1;
  val conjs =
    atp_proof |> map_filter (fn (name, role, _, _, _) =>
      if role = Conjecture orelse role = Negated_Conjecture then SOME name else NONE);
  val ap1 = map (fn (name, _, _, _, from) => (from, name)) atp_proof;
  val ap2 = String_Redirect.make_refute_graph bot ap1;
  val refute_graph = fold (String_Redirect.Atom_Graph.default_node o rpair ()) conjs ap2
  *}
ML {* val axioms = (String_Redirect.axioms_of_refute_graph refute_graph conjs); *}
ML {* val noskolem =
      map (fn tm => Term.add_frees tm []) ((atp_proof |> map_filter (fn (_, role, tm, _, _) =>
      if role = Conjecture then SOME tm else NONE)) @
      (atp_proof_whole |> map_filter (fn (name, _, tm, _, _) =>
      if member (op =) axioms name then SOME tm else NONE))) *}
*)

ML {*
fun ap_to_ip (atp_proof, atp_proof_whole) =
  let
  val bot = atp_proof |> List.last |> #1;
  val conjs =
    atp_proof |> map_filter (fn (name, role, _, _, _) =>
      if role = Conjecture orelse role = Negated_Conjecture then SOME name else NONE)
  val ap1 = map (fn (name, _, _, _, from) => (from, name)) atp_proof;
  val ap2 = String_Redirect.make_refute_graph bot ap1;
  val refute_graph = fold (String_Redirect.Atom_Graph.default_node o rpair ()) conjs ap2
  val axioms = (String_Redirect.axioms_of_refute_graph refute_graph conjs);
  val noskolem =
      map fst (flat (map (fn tm => Term.add_frees tm []) ((atp_proof |> map_filter (fn (_, role, tm, _, _) =>
      if role = Conjecture then SOME tm else NONE)) @
      (atp_proof_whole |> map_filter (fn (name, _, tm, _, _) =>
      if member (op =) axioms name then SOME tm else NONE)))));
  val tainted = String_Redirect.tainted_atoms_of_refute_graph refute_graph conjs;
  val rg = String_Redirect.redirect_graph axioms tainted bot refute_graph;
  val is_clause_tainted = exists (member (op =) tainted);
  val steps =
     Symtab.empty
     |> fold (fn (name as (s, _), role, t, rule, _) =>
                 Symtab.update_new (s, (rule,
                   t |> (if is_clause_tainted [name] then
                           s_maybe_not role
                           #> fold exists_of (map Var (Term.add_vars t []))
                         else
                           I))))
             atp_proof
   fun is_clause_skolemize_rule [(s, _)] =
       Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) = SOME true
     | is_clause_skolemize_rule _ = false;
   fun prop_of_clause [(num, _)] =
       Symtab.lookup steps num |> the |> snd |> maybe_mk_Trueprop |> close_form
     | prop_of_clause names =
       let
         val lits = map snd (map_filter (Symtab.lookup steps o fst) names)
       in
         case List.partition (can HOLogic.dest_not) lits of
           (negs as _ :: _, pos as _ :: _) =>
           s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos)
         | _ => fold (curry s_disj) lits @{term False}
       end
       |> HOLogic.mk_Trueprop |> close_form
       fun isar_proof_of_direct_proof infs =
          let
            fun maybe_show outer c =
              (outer andalso length c = 1 andalso subset (op =) (c, conjs)) ? cons Show
            val is_fixed = Variable.is_declared @{context} orf can Name.dest_skolem orf member (op =) noskolem
            fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
            fun do_steps outer predecessor accum [] =
                accum
                |> (if tainted = [] then
                      cons (Sledgehammer_Proof.Prove (if outer then [Sledgehammer_Proof.Show] else [], Sledgehammer_Proof.Fix [], no_label, @{prop g}, [],
                                   Sledgehammer_Proof.By (([the predecessor], []), Sledgehammer_Proof.MetisM)))
                    else
                      I)
                |> rev
              | do_steps outer _ accum (Have (gamma, c) :: infs) =
                let
                  val l = label_of_clause c
                  val t = prop_of_clause c
                  val by = Sledgehammer_Proof.By (fold add_fact_of_dependencies gamma no_facts, Sledgehammer_Proof.MetisM)
                  fun prove sub by = Sledgehammer_Proof.Prove (maybe_show outer c [], Sledgehammer_Proof.Fix [], l, t, sub, by)
                  fun do_rest l step = do_steps outer (SOME l) (step :: accum) infs
                in
                  if is_clause_tainted c then
                    case gamma of
                      [g] =>
                      if is_clause_skolemize_rule g andalso is_clause_tainted g then
                        let
                          val subproof =
                            Proof (Fix (skolems_of (prop_of_clause g)), Assume [], rev accum)
                        in
                          do_steps outer (SOME l) [prove [subproof] (By (no_facts, Sledgehammer_Proof.MetisM))] []
                        end
                      else
                        do_rest l (prove [] by)
                    | _ => do_rest l (prove [] by)
                  else
                    if is_clause_skolemize_rule c then
                      do_rest l (Sledgehammer_Proof.Prove ([], Fix (skolems_of t), l, t, [], by))
                    else
                      do_rest l (prove [] by)
                end
              | do_steps outer predecessor accum (Cases cases :: infs) =
                let
                  fun do_case (c, infs) =
                    do_proof false [] [(label_of_clause c, prop_of_clause c)] infs
                  val c = succedent_of_cases cases
                  val l = label_of_clause c
                  val t = prop_of_clause c
                  val step =
                    Sledgehammer_Proof.Prove (maybe_show outer c [], Sledgehammer_Proof.Fix [], l, t,  map do_case cases,
                      Sledgehammer_Proof.By ((the_list predecessor, []), Sledgehammer_Proof.MetisM))
                in
                  do_steps outer (SOME l) (step :: accum) infs
                end
            and do_proof outer fix assms infs =
              Sledgehammer_Proof.Proof (Sledgehammer_Proof.Fix fix, Assume assms, do_steps outer NONE [] infs)
          in
            do_proof true [] [] infs
          end
  in
    isar_proof_of_direct_proof rg
end
*}

ML {*
  fun defix (Fix l) = (map fst l)
  fun mp2 (Proof (_,_,l)) = map (fn Prove (q,f,l,t,sl,b) => (q,defix f,l,cterm_of @{theory} t, sl, b)) l   fun mp1 (Proof (_,_,l)) = map (fn Prove (q,f,l,t,sl,b) => (q,defix f,l,cterm_of @{theory} t, (map mp2 sl), b)) l
  fun mp (Proof (_,_,l)) = map (fn Prove (q,f,l,t,sl,b) => (q,defix f,l,cterm_of @{theory} t, (map mp1 sl), b)) l
*}

ML {*
fun t2s rn bs (Const ("HOL.conj", _) $ l $ r) = "(" ^ t2s rn bs l ^ " & " ^ t2s rn bs r ^ ")"
  | t2s rn bs (Const ("HOL.disj", _) $ l $ r) = "(" ^ t2s rn bs l ^ " | " ^ t2s rn bs r ^ ")"
  | t2s rn bs (Const ("HOL.implies", _) $ l $ r) = "(" ^ t2s rn bs l ^ " => " ^ t2s rn bs r ^ ")"
  | t2s rn bs (Const ("HOL.eq", _) $ l $ r) =
      if fastype_of l = @{typ bool} then "(" ^ t2s rn bs l ^ " <=> " ^ t2s rn bs r ^ ")"
      else  "(" ^ t2s rn bs l ^ " = " ^ t2s rn bs r ^ ")"
  | t2s rn bs (Const ("HOL.Not", _) $ t) = "~(" ^ t2s rn bs t ^ ")"
  | t2s rn bs (Const ("HOL.Ex", _) $ Abs (v, _, t)) = "?[B" ^ v ^ "]:(" ^ t2s rn (v :: bs) t ^ ")"
  | t2s rn bs (Const ("HOL.All", _) $ Abs (v, _, t)) = "![B" ^ v ^ "]:(" ^ t2s rn (v :: bs) t ^ ")"
  | t2s rn bs (Const ("all", _) $ Abs (v, _, t)) = "![B" ^ v ^ "]:(" ^ t2s rn (v :: bs) t ^ ")"
  | t2s _ bs (Bound n) = "B" ^ nth bs n
  | t2s rn _ (Free (n, _)) = if member (op =) rn n then "B" ^ n else n
  | t2s rn _ (Const (n, _)) = if member (op =) rn n then "B" ^ n else n
  | t2s rn bs (Const ("HOL.Trueprop", _) $ t) = t2s rn bs t
  | t2s rn bs (l $ r) = let val (l, r) = strip_comb (l $ r) in t2s rn bs l ^ "(" ^ commas (map (t2s rn bs) r) ^ ")" end
  | t2s _ _ t = "FAILURE: " ^ PolyML.makestring t;
fun t2s2 rn t = t2s rn [] t
*}

ML {*
fun ex_const T = Const ("HOL.Ex", (T --> HOLogic.boolT) --> HOLogic.boolT);
fun list_ex xs t = fold_rev (fn (x, T) => fn P =>
  if member (op =) (map fst (Term.add_frees P [])) x then ex_const T $ Abs (x, T, P) else P) xs t;
fun all_const T = Const ("HOL.All", (T --> HOLogic.boolT) --> HOLogic.boolT);
fun list_all xs t = fold_rev (fn (x, T) => fn P =>
  if member (op =) (map fst (Term.add_frees P [])) x then all_const T $ Abs (x, T, P) else P) xs t;
*}

ML {*
fun redirects (Prove (_, Fix obt, l, t, ipl, By ((labs, stringi), _))) (tr, rn) =
  let
    val (tr2, rn2) = if obt = [] then (tr, rn) else
      let val obt1 = map (fn (of1, _) => (of1, HOLogic.boolT)) obt in
      ((fn t => tr (list_ex obt1 t)), map fst obt @ rn) end;
    fun l2l (l1, b) = l1 ^ "_" ^ (Int.toString b);
    val _ = tracing ("fof(" ^ (l2l l) ^ ", plain, " ^ t2s2 rn2 (tr2 t) ^ ", inference(bla, status(thm), [" ^ (String.concatWith ", " (map l2l labs @ stringi)) ^ "])).")
    val _ = map (fn p => redirectp p (tr2, rn2)) ipl
  in
    (tr2, rn2)
  end
and redirectp (Proof (Fix f, Assume a, l)) (tr, rn) =
  let
(*    val _ = tracing "<proof>";*)
    val (tr2, rn2) = if f = [] then (tr, rn) else
      let val f1 = map (fn (of1, _) => (of1, HOLogic.boolT)) f in
      ((fn t => (tr (list_all f1 t))), map fst f @ rn) end;
    fun doasms [] tr = tr
      | doasms ((_, h) :: t) tr = (fn tm => (doasms t tr (HOLogic.mk_imp (h, tm))))
    val tr3 = doasms a tr2;
    val _ = fold redirects l (tr3, rn2)
  in
    ()
  end;
fun redirect p = redirectp p (fn t => t, [])
*}

ML {* fun f () = redirect (ap_to_ip (fname_to_ap (hd (CommandLine.arguments ())))) *}

ML {* PolyML.export ("redirect", f) *}

end