(*
This file is part of the first order theorem prover Darwin
Copyright (C) 2006
              The University of Iowa

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
*)


type term = Term.term
type literal = Term.literal
module LiteralTable = Term.LiteralTable


(* pseudo-context literal to regress,
   used to mark the regression task of the closing clause. *)
let close_literal =
  Term.request_literal
    true
    (Term.request_const Symbol.lemma_root)


(* accepts a list of literal lists,
   where each literal is the class of all regressed instances of the same context literal.

   simplifies by trying to unify and reduce all instances of a class to a singleton *)
let simplify (regressed: literal list list) : literal list =

  let rec simplify (simplified: literal list) (classes: literal list list) =
    match classes with
      | [] ->
          simplified
            
      | literals :: tail ->
          begin
            try
              (* try to unify all literals in this class by unifying its literals pairwise *)
              let unifier =
                let rec unify' unifier literals =
                  match literals with
                    | [] ->
                        failwith "Lemma: simplifying empty class"
                        
                    | _ :: [] ->
                        unifier
                        
                    | l1 :: l2 :: tail ->
                        let unifier' =
                          Unification.unify_literals_ ~recompute:false unifier l1 0 l2 0
                        in
                          unify' unifier' (l2 :: tail)
                in
                  unify' Subst.empty literals
              in
                (* already a singleton, or only constants *)
                if Subst.is_empty unifier then begin
                  simplify (literals @ simplified) tail
                end
                  
                (* apply unifier to all literals -
                   have to avoid independent normalization *)
                else begin
                  (* only need to use one literal of the unified class *)
                  let simplified' =
                    List.map
                      (fun literal ->
                         Subst.apply_to_literal ~normalize:false unifier literal 0
                      )
                      ((List.hd literals) :: simplified)
                  in

                  let classes' =
                    List.map
                      (fun literals ->
                         List.map
                           (fun literal ->
                              Subst.apply_to_literal ~normalize:false unifier literal 0
                           )
                           literals
                      )
                      tail
                  in
                    simplify simplified' classes'
                end
                  
            with
              | Unification.UNIFICATION_FAIL ->
                  (* simplification of this class failed *)
                  simplify (literals @ simplified) tail
          end
  in
    
    simplify [] regressed