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