helm/software/components/ng_paramodulation/superposition.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
  13
  14 module Superposition (B : Terms.Blob) =
  15   struct
  16     module IDX = Index.Index(B)
  17
  18     let all_positions t f =
  19       let rec aux pos ctx = function
  20       | Terms.Leaf a as t -> f t pos ctx
  21       | Terms.Var i -> []
  22       | Terms.Node l as t->
  23           let acc, _, _ =
  24             List.fold_left
  25             (fun (acc,pre,post) t -> (* Invariant: pre @ [t] @ post = l *)
  26                 let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
  27                 let acc = aux (List.length pre :: pos) newctx t @ acc in
  28                 if post = [] then acc, l, []
  29                 else acc, pre @ [t], List.tl post)
  30              (f t pos ctx, [], List.tl l) l
  31           in
  32            acc
  33       in
  34         aux [] (fun x -> x) t
  35     ;;
  36
  37     let superposition_right table subterm pos context =
  38       let _cands = IDX.DT.retrieve_unifiables table subterm in
  39       assert false;;
  40 (*
  41       for every cand in cands
  42         let subst = FoUnif.unify l_can t
  43         (apply_subst subst (c r_cand)), pos, id_cand, subst
  44 *)
  45
  46     let superposition_right_step bag (_,selected,_,_) table =
  47       match selected with
  48       | Terms.Predicate _ -> assert false
  49       | Terms.Equation (l,r,_,Terms.Lt) ->
  50           let _r's = all_positions r (superposition_right table) in
  51           assert false
  52       | Terms.Equation (l,r,_,Terms.Gt) -> assert false
  53       | _ -> assert false
  54     ;;
  55
  56   end
  57
  58
  59