(*
    ||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)

    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 subterm pos context =
      let _cands = IDX.DT.retrieve_unifiables table subterm in
      assert false;;
(*
      for every cand in cands 
        let subst = FoUnif.unify l_can t
        (apply_subst subst (c r_cand)), pos, id_cand, subst
*)

    let superposition_right_step bag (_,selected,_,_) table =
      match selected with 
      | Terms.Predicate _ -> assert false
      | Terms.Equation (l,r,_,Terms.Lt) -> 
          let _r's = all_positions r (superposition_right table) in
          assert false
      | Terms.Equation (l,r,_,Terms.Gt) -> assert false
      | _ -> assert false
    ;;
          
  end