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 type Comparable =
  15   sig
  16     type t
  17     val is_eq : t -> t -> bool
  18   end
  19
  20 module C : Comparable =
  21   struct
  22     type t = NCic.term
  23     let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *)
  24   end
  25
  26   (*
  27 module C : Comparable =
  28   struct
  29     type t = Cic.term
  30     let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *)
  31   end
  32 *)
  33
  34 open Discrimination_tree
  35
  36 module ClauseOT : Set.OrderedType
  37                 with type t = Terms.direction * C.t Terms.unit_clause =
  38  struct
  39   type t = Terms.direction * C.t Terms.unit_clause
  40   let compare (d1,(id1,_,_,_)) (d2,(id2,_,_,_)) =
  41           Pervasives.compare (d1,id1) (d2,id2)
  42  end
  43
  44 module ClauseSet = Set.Make(ClauseOT)
  45
  46 module FotermIndexable : Indexable
  47 with type input = C.t Terms.foterm and
  48      type constant_name = C.t = struct
  49
  50 type input = C.t Terms.foterm
  51 type constant_name = C.t
  52
  53 let path_string_of =
  54   let rec aux arity = function
  55     | Terms.Leaf a -> [Constant (a, arity)]
  56     | Terms.Var i -> assert (arity = 0); [Variable]
  57     | Terms.Node (Terms.Var _::_) -> assert false
  58     | Terms.Node ([] | [ _ ] ) -> assert false
  59     | Terms.Node (Terms.Node _::_) -> assert false
  60     | Terms.Node (hd::tl) ->
  61         aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl)
  62   in
  63     aux 0
  64 ;;
  65
  66 let compare e1 e2 =
  67   match e1,e2 with
  68   | Constant (a1,ar1), Constant (a2,ar2) ->
  69       if C.is_eq a1 a2 then Pervasives.compare ar1 ar2
  70       else Pervasives.compare e1 e2 (* TODO: OPTIMIZE *)
  71   | _ -> Pervasives.compare e1 e2
  72 ;;
  73
  74 let string_of_path l = String.concat "." (List.map (fun _ -> "*") l) ;;
  75
  76 end
  77
  78 module DiscriminationTree = Make(FotermIndexable)(ClauseSet)