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.
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_______________________________________________________________ *)
12 (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
14 module Superposition (B : Terms.Blob) =
16 module IDX = Index.Index(B)
17 module Unif = FoUnif.Founif(B)
18 module Subst = FoSubst.Subst(B)
19 module Order = Orderings.Orderings(B)
21 let all_positions t f =
22 let rec aux pos ctx = function
23 | Terms.Leaf a as t -> f t pos ctx
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
40 let superposition_right table varlist subterm pos context =
41 let cands = IDX.DT.retrieve_unifiables table subterm in
43 (fun (dir, (id,lit,vl,_)) ->
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
50 Unif.unification (varlist@vl) [] subterm side
52 Some (context newside, subst, varlist, id, pos, dir)
53 with FoUnif.UnificationFailure _ -> None)
54 (IDX.ClauseSet.elements cands)
57 let superposition_right_step bag (id,selected,vl,_) table =
59 | Terms.Predicate _ -> assert false
60 | Terms.Equation (l,r,ty,Terms.Lt) ->
61 let res = all_positions r (superposition_right table vl) in
64 (fun (r,subst,vl,id2,pos,dir) ->
66 Terms.Step(Terms.SuperpositionRight,id,id2, dir, pos, subst)
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))
76 (* fresh ID and metas and compute orientataion of new_clauses *)
78 | Terms.Equation (l,r,_,Terms.Gt) -> assert false