]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_paramodulation/index.ml
Use matita/lib as the new standard library in place of matita/nlibrary.
[helm.git] / matita / components / ng_paramodulation / index.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$ *)
13
14 module Index(B : Orderings.Blob) = struct
15   module U = FoUtils.Utils(B)
16   module Unif = FoUnif.Founif(B)
17   module Pp = Pp.Pp(B)
18
19   module ClauseOT =
20     struct 
21       type t = Terms.direction * B.t Terms.unit_clause
22  
23       let compare (d1,uc1) (d2,uc2) = 
24         let c = Pervasives.compare d1 d2 in
25         if c <> 0 then c else U.compare_unit_clause uc1 uc2
26       ;;
27     end
28
29   module ClauseSet : 
30     Set.S with type elt = Terms.direction * B.t Terms.unit_clause
31     = Set.Make(ClauseOT)
32
33   open Discrimination_tree
34
35   module FotermIndexable : Indexable with
36     type constant_name = B.t and
37     type input = B.t Terms.foterm 
38   =
39     struct
40
41       type input = B.t Terms.foterm
42       type constant_name = B.t
43
44       let path_string_of =
45         let rec aux arity = function
46           | Terms.Leaf a -> [Constant (a, arity)]
47           | Terms.Var i -> (* assert (arity = 0); *) [Variable]
48           (* FIXME : should this be allowed or not ? 
49           | Terms.Node (Terms.Var _::_) ->
50               assert false *)
51           | Terms.Node ([] | [ _ ] ) -> assert false
52           | Terms.Node (Terms.Node _::_) -> assert false              
53           | Terms.Node (hd::tl) ->
54               aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) 
55         in 
56           aux 0
57       ;;
58
59       let compare e1 e2 = 
60         match e1,e2 with 
61         | Constant (a1,ar1), Constant (a2,ar2) ->
62             let c = B.compare a1 a2 in
63             if c <> 0 then c else Pervasives.compare ar1 ar2
64         | Variable, Variable -> 0
65         | Constant _, Variable -> ~-1
66         | Variable, Constant _ -> 1
67         | Proposition, _ | _, Proposition
68         | Datatype, _ | _, Datatype
69         | Dead, _ | _, Dead
70         | Bound _, _ | _, Bound _ -> assert false
71       ;;
72
73       let string_of_path l = String.concat "." (List.map (fun _ -> "*") l) ;;
74
75     end
76
77     module DT : DiscriminationTree with
78       type constant_name = B.t and 
79       type input = B.t Terms.foterm and 
80       type data = ClauseSet.elt and 
81       type dataset = ClauseSet.t
82     = Make(FotermIndexable)(ClauseSet)
83   
84   let process op t = function
85     | (_,Terms.Equation (l,_,_,Terms.Gt),_,_) as c -> 
86         op t l (Terms.Left2Right, c)
87     | (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c -> 
88         op t r (Terms.Right2Left, c)
89     | (_,Terms.Equation (l,r,_,Terms.Incomparable),vl,_) as c ->
90         op (op t l (Terms.Left2Right, c))
91           r (Terms.Right2Left, c)
92     | (_,Terms.Equation (l,r,_,Terms.Invertible),vl,_) as c ->
93         op t l (Terms.Left2Right, c)
94     | (_,Terms.Equation (_,r,_,Terms.Eq),_,_)  -> assert false
95     | (_,Terms.Predicate p,_,_) as c ->
96         op t p (Terms.Nodir, c)
97   ;;
98
99   let index_unit_clause = 
100     process DT.index 
101  
102   let remove_unit_clause =
103     process DT.remove_index 
104
105   let fold = DT.fold 
106
107   let elems index =
108     DT.fold index (fun _ dataset acc -> ClauseSet.union dataset acc)
109       ClauseSet.empty
110     
111   type active_set = B.t Terms.unit_clause list * DT.t
112
113 end