helm/software/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 : Terms.Blob) = struct
  15   module U = Terms.Utils(B)
  16
  17   module ClauseOT =
  18     struct
  19       type t = Terms.direction * B.t Terms.unit_clause
  20
  21       let compare (d1,uc1) (d2,uc2) =
  22         let c = Pervasives.compare d1 d2 in
  23         if c <> 0 then c else U.compare_unit_clause uc1 uc2
  24       ;;
  25     end
  26
  27   module ClauseSet :
  28     Set.S with type elt = Terms.direction * B.t Terms.unit_clause
  29     = Set.Make(ClauseOT)
  30
  31   open Discrimination_tree
  32
  33   module FotermIndexable : Indexable with
  34     type constant_name = B.t and
  35     type input = B.t Terms.foterm
  36   =
  37     struct
  38
  39       type input = B.t Terms.foterm
  40       type constant_name = B.t
  41
  42       let path_string_of =
  43         let rec aux arity = function
  44           | Terms.Leaf a -> [Constant (a, arity)]
  45           | Terms.Var i -> assert (arity = 0); [Variable]
  46           | Terms.Node (Terms.Var _::_) -> assert false
  47           | Terms.Node ([] | [ _ ] ) -> assert false
  48           | Terms.Node (Terms.Node _::_) -> assert false
  49           | Terms.Node (hd::tl) ->
  50               aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl)
  51         in
  52           aux 0
  53       ;;
  54
  55       let compare e1 e2 =
  56         match e1,e2 with
  57         | Constant (a1,ar1), Constant (a2,ar2) ->
  58             let c = B.compare a1 a2 in
  59             if c <> 0 then c else Pervasives.compare ar1 ar2
  60         | Variable, Variable -> 0
  61         | Constant _, Variable -> ~-1
  62         | Variable, Constant _ -> 1
  63         | Proposition, _ | _, Proposition
  64         | Datatype, _ | _, Datatype
  65         | Dead, _ | _, Dead
  66         | Bound _, _ | _, Bound _ -> assert false
  67       ;;
  68
  69       let string_of_path l = String.concat "." (List.map (fun _ -> "*") l) ;;
  70
  71     end
  72
  73     module DT : DiscriminationTree with
  74       type constant_name = B.t and
  75       type input = B.t Terms.foterm and
  76       type data = ClauseSet.elt and
  77       type dataset = ClauseSet.t
  78     = Make(FotermIndexable)(ClauseSet)
  79
  80 end