(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.      
     \ /   This software is distributed as is, NO WARRANTY.     
      V_______________________________________________________________ *)

(* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)

module Superposition (B : Terms.Blob) = 
  struct
    module IDX = Index.Index(B)
    module Unif = FoUnif.Founif(B)
    module Subst = FoSubst.Subst(B)
    module Order = Orderings.Orderings(B)

    let all_positions t f =
      let rec aux pos ctx = function
      | Terms.Leaf a as t -> f t pos ctx 
      | Terms.Var i -> []
      | Terms.Node l as t-> 
          let acc, _, _ = 
            List.fold_left
            (fun (acc,pre,post) t -> (* Invariant: pre @ [t] @ post = l *)
                let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
                let acc = aux (List.length pre :: pos) newctx t @ acc in
                if post = [] then acc, l, []
                else acc, pre @ [t], List.tl post)
             (f t pos ctx, [], List.tl l) l
          in
           acc
      in
        aux [] (fun x -> x) t
    ;;

    let superposition_right table varlist subterm pos context =
      let cands = IDX.DT.retrieve_unifiables table subterm in
      HExtlib.filter_map
        (fun (dir, (id,lit,vl,_)) ->
           match lit with
           | Terms.Predicate _ -> assert false
           | Terms.Equation (l,r,_,o) ->
               let side, newside = if dir=Terms.Left2Right then l,r else r,l in
               try 
                 let subst, varlist = 
                   Unif.unification (varlist@vl) [] subterm side 
                 in
                 Some (context newside, subst, varlist, id, pos, dir)
               with FoUnif.UnificationFailure _ -> None)
        (IDX.ClauseSet.elements cands)
    ;;

    let superposition_right_step bag (id,selected,vl,_) table =
      match selected with 
      | Terms.Predicate _ -> assert false
      | Terms.Equation (l,r,ty,Terms.Lt) -> 
          let res = all_positions r (superposition_right table vl) in
          let _new_clauses = 
            List.map
              (fun (r,subst,vl,id2,pos,dir) -> 
                 let proof = 
                   Terms.Step(Terms.SuperpositionRight,id,id2, dir, pos, subst)
                 in
                 let r = Subst.apply_subst subst r in
                 let l = Subst.apply_subst subst l in
                 let ty = Subst.apply_subst subst ty in
                 let o = Order.compare_terms l r in
                 (* can unif compute the right vl for both sides? *)
                 (0, Terms.Equation (l,r,ty,o), vl, proof))
              res
          in
          (* fresh ID and metas and compute orientataion of new_clauses *)
          assert false
      | Terms.Equation (l,r,_,Terms.Gt) -> assert false
      | _ -> assert false
    ;;
          
  end