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