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     module Unif = FoUnif.Founif(B)
  18     module Subst = FoSubst.Subst(B)
  19     module Order = Orderings.Orderings(B)
  20
  21     let all_positions t f =
  22       let rec aux pos ctx = function
  23       | Terms.Leaf a as t -> f t pos ctx
  24       | Terms.Var i -> []
  25       | Terms.Node l as t->
  26           let acc, _, _ =
  27             List.fold_left
  28             (fun (acc,pre,post) t -> (* Invariant: pre @ [t] @ post = l *)
  29                 let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
  30                 let acc = aux (List.length pre :: pos) newctx t @ acc in
  31                 if post = [] then acc, l, []
  32                 else acc, pre @ [t], List.tl post)
  33              (f t pos ctx, [], List.tl l) l
  34           in
  35            acc
  36       in
  37         aux [] (fun x -> x) t
  38     ;;
  39
  40     let superposition_right table varlist subterm pos context =
  41       let cands = IDX.DT.retrieve_unifiables table subterm in
  42       HExtlib.filter_map
  43         (fun (dir, (id,lit,vl,_)) ->
  44            match lit with
  45            | Terms.Predicate _ -> assert false
  46            | Terms.Equation (l,r,_,o) ->
  47                let side, newside = if dir=Terms.Left2Right then l,r else r,l in
  48                try
  49                  let subst, varlist =
  50                    Unif.unification (varlist@vl) [] subterm side
  51                  in
  52                  Some (context newside, subst, varlist, id, pos, dir)
  53                with FoUnif.UnificationFailure _ -> None)
  54         (IDX.ClauseSet.elements cands)
  55     ;;
  56
  57     let superposition_right_step bag (id,selected,vl,_) table =
  58       match selected with
  59       | Terms.Predicate _ -> assert false
  60       | Terms.Equation (l,r,ty,Terms.Lt) ->
  61           let res = all_positions r (superposition_right table vl) in
  62           let _new_clauses =
  63             List.map
  64               (fun (r,subst,vl,id2,pos,dir) ->
  65                  let proof =
  66                    Terms.Step(Terms.SuperpositionRight,id,id2, dir, pos, subst)
  67                  in
  68                  let r = Subst.apply_subst subst r in
  69                  let l = Subst.apply_subst subst l in
  70                  let ty = Subst.apply_subst subst ty in
  71                  let o = Order.compare_terms l r in
  72                  (* can unif compute the right vl for both sides? *)
  73                  (0, Terms.Equation (l,r,ty,o), vl, proof))
  74               res
  75           in
  76           (* fresh ID and metas and compute orientataion of new_clauses *)
  77           assert false
  78       | Terms.Equation (l,r,_,Terms.Gt) -> assert false
  79       | _ -> assert false
  80     ;;
  81
  82   end
  83
  84
  85