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)
20 let all_positions t f =
21 let rec aux pos ctx = function
22 | Terms.Leaf a as t -> f t pos ctx
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
39 let superposition_right table varlist subterm pos context =
40 let cands = IDX.DT.retrieve_unifiables table subterm in
42 (fun (dir, (id,lit,vl,_)) ->
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
49 Unif.unification (varlist@vl) [] subterm side
51 Some (context newside, subst, varlist, id, pos, dir)
52 with FoUnif.UnificationFailure _ -> None)
53 (IDX.ClauseSet.elements cands)
56 let superposition_right_step bag (id,selected,vl,_) table =
58 | Terms.Predicate _ -> assert false
59 | Terms.Equation (l,r,ty,Terms.Lt) ->
60 let res = all_positions r (superposition_right table vl) in
63 (fun (r,subst,vl,id2,pos,dir) ->
65 Terms.Step(Terms.SuperpositionRight,id,id2, dir, pos, subst)
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))
73 (* fresh ID and metas and compute orientataion of new_clauses *)
75 | Terms.Equation (l,r,_,Terms.Gt) -> assert false