# File recon_translate_proof.ML

    (*  ID:         $Id: recon_translate_proof.ML,v 1.22 2005/09/19 16:30:23 paulson Exp $
        Author:     Claire Quigley
        Copyright   2004  University of Cambridge
    *)

    structure ReconTranslateProof =
    struct

    fun add_in_order (x:string) [] = [x]
    |   add_in_order (x:string) ((y:string)::ys) = if (x < y)
                                 then
                                      (x::(y::ys))
                                 else
                                      (y::(add_in_order x ys))
    fun add_once x [] = [x]
    |   add_once x (y::ys) = if x mem (y::ys) then (y::ys)
                             else add_in_order x (y::ys)

    fun thm_vars thm = map (fn ((name,ix),_) => name) (Drule.vars_of thm);

    exception Reflex_equal;

    (********************************)
    (* Proofstep datatype           *)
    (********************************)
    (* Assume rewrite steps have only two clauses in them just now, but lcl109-5 has Rew[5,3,5,3]  *)

    datatype Side = Left |Right

    datatype Proofstep =  ExtraAxiom
                         | OrigAxiom
      		     | VampInput
                         | Axiom
                         | Binary of (int * int) * (int * int)   (* (clause1,lit1), (clause2, lit2) *)
                         | MRR of (int * int) * (int * int)
                         | Factor of (int * int * int)           (* (clause,lit1, lit2) *)
                         | Para of (int * int) * (int * int)
    		     | Super_l of (int * int) * (int * int)
    		     | Super_r of (int * int) * (int * int)
                         (*| Rewrite of (int * int) * (int * int)  *)
                         | Rewrite of (int * int) list
    		     | SortSimp of (int * int) * (int * int)
    		     | UnitConf of (int * int) * (int * int)
                         | Obvious of (int * int)
      		     | AED of (int*int)
      		     | EqualRes of (int*int)
        		     | Condense of (int*int)
                         (*| Hyper of int list*)
                         | Unusedstep of unit

    datatype Clausesimp = Binary_s of int * int
                          | Factor_s of unit
                          | Demod_s of (int * int) list
                          | Hyper_s of int list
                          | Unusedstep_s of unit

    datatype Step_label = T_info
                         |P_info

    fun is_alpha_space_digit_or_neg ch =
        (ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse
        (ReconOrderClauses.is_digit ch) orelse ( ch = " ");

    fun string_of_term (Const(s,_)) = s
      | string_of_term (Free(s,_)) = s
      | string_of_term (Var(ix,_)) = Term.string_of_vname ix
      | string_of_term (Bound i) = string_of_int i
      | string_of_term (Abs(x,_,t)) = "%" ^ x ^ ". " ^ string_of_term t
      | string_of_term (s $ t) =
          "(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")"

    fun lit_string_with_nums t = let val termstr = string_of_term t
                                     val exp_term = explode termstr
                                 in
                                     implode(List.filter is_alpha_space_digit_or_neg exp_term)
                                 end

    fun reconstruction_failed fname = error (fname ^ ": reconstruction failed")

    (************************************************)
    (* Reconstruct an axiom resolution step         *)
    (* clauses is a list of (clausenum,clause) pairs*)
    (************************************************)

    fun follow_axiom clauses  allvars (clausenum:int) thml clause_strs =
        let val this_axiom = (the o AList.lookup (op =) clauses) clausenum
    	val (res, numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause this_axiom clause_strs allvars)
    	val thmvars = thm_vars res
        in
    	(res, (Axiom,clause_strs,thmvars )  )
        end
        handle Option => reconstruction_failed "follow_axiom"

    (****************************************)
    (* Reconstruct a binary resolution step *)
    (****************************************)

                     (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
    fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs =
        let val thm1 =  select_literal (lit1 + 1) ((the o AList.lookup (op =) thml) clause1)
    	val thm2 =  (the o AList.lookup (op =) thml) clause2
    	val res =   thm1 RSN ((lit2 +1), thm2)
    	val (res', numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause res clause_strs allvars)
    	val thmvars = thm_vars res
        in
           (res',  ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
        end
        handle Option => reconstruction_failed "follow_binary"

    (******************************************************)
    (* Reconstruct a matching replacement resolution step *)
    (******************************************************)

    fun follow_mrr ((clause1, lit1), (clause2 , lit2))  allvars thml clause_strs =
        let val thm1 =  select_literal (lit1 + 1) ((the o AList.lookup (op =) thml) clause1)
    	val thm2 =  (the o AList.lookup (op =) thml) clause2
    	val res =   thm1 RSN ((lit2 +1), thm2)
    	val (res', numlist, symlist, nsymlist) =
    	    (ReconOrderClauses.rearrange_clause res clause_strs allvars)
    	val thmvars = thm_vars res
        in
           (res',  ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
        end
        handle Option => reconstruction_failed "follow_mrr"

    (*******************************************)
    (* Reconstruct a factoring resolution step *)
    (*******************************************)

    fun mksubstlist [] sublist = sublist
       |mksubstlist ((a, (_, b)) :: rest) sublist =
           let val vartype = type_of b
    	   val avar = Var(a,vartype)
    	   val newlist = ((avar,b)::sublist)
           in
    	   mksubstlist rest newlist
           end;

    (* based on Tactic.distinct_subgoals_tac *)

    fun delete_assump_tac state lit =
        let val (frozth,thawfn) = freeze_thaw state
            val froz_prems = cprems_of frozth
            val assumed = implies_elim_list frozth (map assume froz_prems)
            val new_prems = ReconOrderClauses.remove_nth lit froz_prems
            val implied = implies_intr_list new_prems assumed
        in
            Seq.single (thawfn implied)
        end

    (*************************************)
    (* Reconstruct a factoring step      *)
    (*************************************)

    fun getnewenv seq = fst (fst (the (Seq.pull seq)));

    (*FIXME: share code with that in Tools/reconstruction.ML*)
    fun follow_factor clause lit1 lit2 allvars thml clause_strs =
        let
          val th =  (the o AList.lookup (op =) thml) clause
          val prems = prems_of th
          val sign = sign_of_thm th
          val fac1 = ReconOrderClauses.get_nth (lit1+1) prems
          val fac2 = ReconOrderClauses.get_nth (lit2+1) prems
          val unif_env = Unify.unifiers (sign,Envir.empty 0, [(fac1, fac2)])
          val newenv = getnewenv unif_env
          val envlist = Envir.alist_of newenv

          val (t1,t2)::_ = mksubstlist envlist []
        in
          if (is_Var t1)
          then
    	  let
    	     val str1 = lit_string_with_nums t1;
    	     val str2 = lit_string_with_nums t2;
    	     val facthm = read_instantiate [(str1,str2)] th;
    	     val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
    	     val (res', numlist, symlist, nsymlist) =
    	         ReconOrderClauses.rearrange_clause res clause_strs allvars
    	     val thmvars = thm_vars res'
    	  in
    		 (res',((Factor (clause,  lit1, lit2)),clause_strs,thmvars))
    	  end
          else
    	  let
    	     val str2 = lit_string_with_nums t1;
    	     val str1 = lit_string_with_nums t2;
    	     val facthm = read_instantiate [(str1,str2)] th;
    	     val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
    	     val (res', numlist, symlist, nsymlist) =
    	         ReconOrderClauses.rearrange_clause res clause_strs allvars
    	     val thmvars = thm_vars res'
    	  in
    		 (res', ((Factor (clause,  lit1, lit2)),clause_strs, thmvars))
    	  end
       end
       handle Option => reconstruction_failed "follow_factor"

    fun get_unif_comb t eqterm =
        if ((type_of t) = (type_of eqterm))
        then t
        else
            let val _ $ rand = t
            in get_unif_comb rand eqterm end;

    fun get_unif_lit t eqterm =
        if (can HOLogic.dest_eq t)
        then
    	let val (lhs,rhs) = HOLogic.dest_eq(HOLogic.dest_Trueprop eqterm)
    	in lhs end
        else
    	get_unif_comb t eqterm;

    (*************************************)
    (* Reconstruct a paramodulation step *)
    (*************************************)

    val rev_subst = rotate_prems 1 subst;
    val rev_ssubst = rotate_prems 1 ssubst;

    fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs =
        let
          val th1 =  (the o AList.lookup (op =) thml) clause1
          val th2 =  (the o AList.lookup (op =) thml) clause2
          val eq_lit_th = select_literal (lit1+1) th1
          val mod_lit_th = select_literal (lit2+1) th2
          val eqsubst = eq_lit_th RSN (2,rev_subst)
          val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
          val newth' =negate_head newth
          val (res, numlist, symlist, nsymlist)  =
              (ReconOrderClauses.rearrange_clause newth' clause_strs allvars
    	   handle Not_in_list =>
    	       let val mod_lit_th' = mod_lit_th RS not_sym
    		   val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst)
    		   val newth' =negate_head newth
    		in
    		   ReconOrderClauses.rearrange_clause newth' clause_strs allvars
    		end)
          val thmvars = thm_vars res
       in
         (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
       end
       handle Option => reconstruction_failed "follow_standard_para"

    (********************************)
    (* Reconstruct a rewriting step *)
    (********************************)

    (*

    val rev_subst = rotate_prems 1 subst;

    fun paramod_rule ((cl1, lit1), (cl2 , lit2)) =
         let  val eq_lit_th = select_literal (lit1+1) cl1
              val mod_lit_th = select_literal (lit2+1) cl2
              val eqsubst = eq_lit_th RSN (2,rev_subst)
              val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1
    eqsubst)
         in Meson.negated_asm_of_head newth end;

    val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1
    eqsubst)

    val mod_lit_th' = mod_lit_th RS not_sym

    *)

    fun delete_assumps 0 th = th
    |   delete_assumps n th = let val th_prems = length (prems_of th)
                                  val th' = hd (Seq.list_of(delete_assump_tac  th (th_prems -1)))
                              in
                                  delete_assumps (n-1) th'
                              end

    (* extra conditions from the equality turn up as 2nd to last literals of result.  Need to delete them *)
    (* changed negate_nead to negate_head here too*)
                        (* clause1, lit1 is thing to rewrite with *)
    (*fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs =
          let val th1 =  (the o AList.lookup (op =) thml) clause1
    	  val th2 = (the o AList.lookup (op =) thml) clause2
    	  val eq_lit_th = select_literal (lit1+1) th1
    	  val mod_lit_th = select_literal (lit2+1) th2
    	  val eqsubst = eq_lit_th RSN (2,rev_subst)
    	  val eq_lit_prem_num = length (prems_of eq_lit_th)
    	  val sign = Theory.merge (sign_of_thm th1, sign_of_thm th2)
    	  val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
         	  val newthm = negate_head newth
    	  val newthm' = delete_assumps eq_lit_prem_num newthm
    	  val (res, numlist, symlist, nsymlist) =
    	      ReconOrderClauses.rearrange_clause newthm clause_strs allvars
    	  val thmvars = thm_vars res
           in
    	   (res, ((Rewrite ((clause1, lit1),  (clause2, lit2))),clause_strs,thmvars))
           end
           handle Option => reconstruction_failed "follow_rewrite"

    *)

    (*****************************************)
    (* Reconstruct an obvious reduction step *)
    (*****************************************)

    fun follow_obvious  (clause1, lit1)  allvars thml clause_strs =
        let val th1 =  (the o AList.lookup (op =) thml) clause1
    	val prems1 = prems_of th1
    	val newthm = refl RSN ((lit1+ 1), th1)
    		     handle THM _ =>  hd (Seq.list_of(delete_assump_tac  th1 (lit1 + 1)))
    	val (res, numlist, symlist, nsymlist) =
    	    ReconOrderClauses.rearrange_clause newthm clause_strs allvars
    	val thmvars = thm_vars res
        in
    	(res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
        end
        handle Option => reconstruction_failed "follow_obvious"

    (**************************************************************************************)
    (* reconstruct a single line of the res. proof - depending on what sort of proof step it was*)
    (**************************************************************************************)

     fun follow_proof clauses allvars  clausenum thml  (Axiom ) clause_strs
            = follow_axiom clauses allvars  clausenum thml clause_strs

          | follow_proof clauses  allvars clausenum  thml (Binary (a, b)) clause_strs
            = follow_binary  (a, b)  allvars thml clause_strs

          | follow_proof clauses  allvars clausenum  thml (MRR (a, b)) clause_strs
            = follow_mrr (a, b)  allvars thml clause_strs

          | follow_proof clauses  allvars clausenum  thml (Factor (a, b, c)) clause_strs
             = follow_factor a b c  allvars thml clause_strs

          | follow_proof clauses  allvars clausenum  thml (Para (a, b)) clause_strs
            = follow_standard_para (a, b) allvars  thml clause_strs

        (*  | follow_proof clauses  allvars clausenum thml (Rewrite (a,b)) clause_strs
            = follow_rewrite (a,b)  allvars thml clause_strs*)

          | follow_proof clauses  allvars clausenum thml (Obvious (a,b)) clause_strs
            = follow_obvious (a,b)  allvars thml clause_strs

          (*| follow_proof clauses  clausenum thml (Hyper l)
            = follow_hyper l thml*)
          | follow_proof clauses  allvars clausenum  thml _ _ =
              error "proof step not implemented"

    (**************************************************************************************)
    (* reconstruct a single line of the res. proof - at the moment do only inference steps*)
    (**************************************************************************************)

        fun follow_line clauses  allvars thml (clause_num, proof_step, clause_strs) recons =
          let
    	val (thm, recon_fun) = follow_proof clauses allvars clause_num thml proof_step clause_strs
          in
    	((clause_num, thm)::thml, (clause_num,recon_fun)::recons)
          end

    (***************************************************************)
    (* follow through the res. proof, creating an Isabelle theorem *)
    (***************************************************************)

    fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126)) orelse (ch = " ")

    fun proofstring x = let val exp = explode x
                        in
                            List.filter (is_proof_char ) exp
                        end

    fun replace_clause_strs [] recons newrecons = (newrecons)
    |   replace_clause_strs ((thmnum, thm)::thml)
                      ((clausenum,(step,clause_strs,thmvars))::recons) newrecons =
        let val new_clause_strs = ReconOrderClauses.get_meta_lits_bracket thm
        in
    	replace_clause_strs thml recons
    	    ((clausenum,(step,new_clause_strs,thmvars))::newrecons)
        end

    fun follow clauses [] allvars thml recons =
          let
    	  val new_recons = replace_clause_strs thml recons []
          in
    	   (#2(hd thml), new_recons)
          end
     | follow clauses (h::t) allvars thml recons =
          let
    	val (thml', recons') = follow_line clauses allvars  thml h recons
    	val  (thm, recons_list) = follow clauses t  allvars thml' recons'
          in
    	 (thm,recons_list)
          end

    (* Assume we have the cnf clauses as a list of (clauseno, clause) *)
     (* and the proof as a list of the proper datatype *)
    (* take the cnf clauses of the goal and the proof from the res. prover *)
    (* as a list of type Proofstep and return the thm goal ==> False *)

    (* takes original axioms, proof_steps parsed from spass, variables *)

    fun translate_proof clauses proof allvars
            = let val (thm, recons) = follow clauses proof allvars [] []
              in
                 (thm, (recons))
              end

    end;