]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_paramodulation/stats.ml
update in basic_2
[helm.git] / matita / components / ng_paramodulation / stats.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: stats.ml 9822 2009-06-03 15:37:06Z denes $ *)
13
14 module Stats (B : Terms.Blob) = 
15   struct
16
17     module SymbMap = Map.Make(B)
18
19     let rec occ_nbr t acc = function
20         | Terms.Leaf u when B.eq t u -> 1+acc
21         | Terms.Node l -> List.fold_left (occ_nbr t) acc l
22         | _ -> acc
23     ;;
24
25     let occ_nbr t = occ_nbr t 0;;
26
27     let goal_occ_nbr t = function
28       | (_,Terms.Equation (l,r,_,_),_,_) ->
29           occ_nbr t l + occ_nbr t r
30       | _ -> assert false
31     ;;
32
33     let rec parse_symbols acc l =
34       let rec aux acc = function
35         | Terms.Leaf t ->
36             (try
37                let (occ,ar) = SymbMap.find t acc in
38                  SymbMap.add t (occ+1,ar) acc
39              with Not_found -> SymbMap.add t (1,0) acc)
40         | Terms.Var _ -> acc
41         | Terms.Node (Terms.Leaf hd::tl) ->
42             let acc =
43               try let (occ,ar) = SymbMap.find hd acc in
44                 SymbMap.add hd (occ+1,ar) acc
45               with Not_found -> SymbMap.add hd (1,List.length tl) acc
46               in List.fold_left aux acc tl
47         | _ -> assert false
48       in
49         match l with
50           | [] -> acc
51           | (_,hd,_,_)::tl ->
52               match hd with
53                 | Terms.Equation (l,r,_,_) ->
54                     parse_symbols (aux (aux acc l) r) tl
55                 | Terms.Predicate _ -> assert false;
56     ;;
57
58     let goal_pos t goal =
59       let rec aux path = function
60        | Terms.Var _ -> [] 
61        | Terms.Leaf x ->
62            if B.eq t x then path else []
63        | Terms.Node l ->
64            match 
65              HExtlib.list_findopt
66                (fun x i -> 
67                   let p = aux (i::path) x in
68                   if p = [] then None else Some p)
69                l
70            with
71            | None -> []
72            | Some p -> p
73       in 
74         aux [] 
75           (match goal with
76           | _,Terms.Equation (l,r,ty,_),_,_ -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ]
77           | _,Terms.Predicate p,_,_ -> p)
78     ;;
79
80     let parse_symbols l goal = 
81       let res = parse_symbols (parse_symbols SymbMap.empty [goal]) l in
82         SymbMap.fold (fun t (occ,ar) acc ->
83                         (t,occ,ar,goal_occ_nbr t goal,goal_pos t goal)::acc) res []
84     ;;
85
86     let rec leaf_count = function
87       | Terms.Node l -> List.fold_left (fun acc x -> acc + (leaf_count x)) 0 l
88       | Terms.Leaf _ -> 1
89       | _ -> 0
90     ;;
91
92     let rec dependencies op clauses acc =
93       match clauses with
94         | [] -> acc
95         | (_,lit,_,_)::tl ->
96             match lit with
97               | Terms.Predicate _ -> assert false
98               | Terms.Equation (l,r,_,_) ->
99                   match l,r with
100                     | (Terms.Node (Terms.Leaf op1::_),Terms.Node
101                          (Terms.Leaf op2::_)) ->
102                         if (B.eq op1 op) && not (B.eq op2 op) then
103                           let already = List.exists (B.eq op2) acc in
104                           let occ_l = occ_nbr op l in
105                           let occ_r = occ_nbr op r in
106                             if not already && occ_r > occ_l then
107                               dependencies op tl (op2::acc)
108                             else dependencies op tl acc
109                         else if not (B.eq op1 op) && (B.eq op2 op) then
110                           let already = List.exists (B.eq op1) acc in
111                           let occ_l = occ_nbr op l in
112                           let occ_r = occ_nbr op r in
113                             if not already && occ_l > occ_r then
114                               dependencies op tl (op1::acc)
115                             else
116                               dependencies op tl acc
117                         else dependencies op tl acc
118                     | ((Terms.Node (Terms.Leaf op1::t) as x),y)
119                     | (y,(Terms.Node (Terms.Leaf op1::t) as x)) when leaf_count x > leaf_count y ->
120                          let rec term_leaves = function
121                            | Terms.Node l -> List.fold_left (fun acc x -> acc @ (term_leaves x)) [] l
122                            | Terms.Leaf x -> [x]
123                            | _ -> []
124                          in
125                          if List.mem op (List.filter (fun z -> not (B.eq op1 z)) (term_leaves x)) then 
126                            dependencies op tl (op1::acc)
127                          else
128                            dependencies op tl acc
129                     | _ -> dependencies op tl acc
130     ;;
131
132     let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));;
133
134     (* let max_weight_hyp = *)
135
136   end