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           (* FIXME : if we can have a variable we can also have a term
  53             | Terms.Node (Terms.Node _::_) as t -> assert false  *)
  54           | Terms.Node (hd::tl) ->
  55               aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl)
  56         in
  57           aux 0
  58       ;;
  59
  60       let compare e1 e2 =
  61         match e1,e2 with
  62         | Constant (a1,ar1), Constant (a2,ar2) ->
  63             let c = B.compare a1 a2 in
  64             if c <> 0 then c else Pervasives.compare ar1 ar2
  65         | Variable, Variable -> 0
  66         | Constant _, Variable -> ~-1
  67         | Variable, Constant _ -> 1
  68         | Proposition, _ | _, Proposition
  69         | Datatype, _ | _, Datatype
  70         | Dead, _ | _, Dead
  71         | Bound _, _ | _, Bound _ -> assert false
  72       ;;
  73
  74       let string_of_path l = String.concat "." (List.map (fun _ -> "*") l) ;;
  75
  76     end
  77
  78     module DT : DiscriminationTree with
  79       type constant_name = B.t and
  80       type input = B.t Terms.foterm and
  81       type data = ClauseSet.elt and
  82       type dataset = ClauseSet.t
  83     = Make(FotermIndexable)(ClauseSet)
  84
  85   let process op t = function
  86     | (_,Terms.Equation (l,_,_,Terms.Gt),_,_) as c ->
  87         op t l (Terms.Left2Right, c)
  88     | (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c ->
  89         op t r (Terms.Right2Left, c)
  90     | (_,Terms.Equation (l,r,_,Terms.Incomparable),vl,_) as c ->
  91         op (op t l (Terms.Left2Right, c))
  92           r (Terms.Right2Left, c)
  93     | (_,Terms.Equation (l,r,_,Terms.Invertible),vl,_) as c ->
  94         op t l (Terms.Left2Right, c)
  95     | (_,Terms.Equation (_,r,_,Terms.Eq),_,_)  -> assert false
  96     | (_,Terms.Predicate p,_,_) as c ->
  97         op t p (Terms.Nodir, c)
  98   ;;
  99
 100   let index_unit_clause =
 101     process DT.index
 102
 103   let remove_unit_clause =
 104     process DT.remove_index
 105
 106   let fold = DT.fold
 107
 108   let elems index =
 109     DT.fold index (fun _ dataset acc -> ClauseSet.union dataset acc)
 110       ClauseSet.empty
 111
 112   type active_set = B.t Terms.unit_clause list * DT.t
 113
 114 end