helm/ocaml/paramodulation/indexing.ml

   1 (* type naif_indexing =
   2     (Cic.term * ((bool * Inference.equality) list)) list
   3 ;; *)
   4
   5 type pos = Left | Right
   6 ;;
   7
   8 let head_of_term =
   9   function
  10     | Cic.Appl hd::tl -> hd
  11     | t -> t
  12 ;;
  13
  14 let index table eq =
  15   let (_,(_,l,r,ordering),_,_) = eq in
  16   let hl = head_of_term l in
  17   let hr = head_of_term r in
  18   let index x pos =
  19     let x_entry =
  20       try Hashtbl.find table x
  21       with Not_found -> [] in
  22       Hashtbl.replace table x (pos,eq)::x_entry in
  23   (match ordering with
  24     | Utils.Gt ->
  25         index hl Left
  26     | Utils.Lt ->
  27         index hr Right
  28     | _ -> index hl Left;
  29         index hr Right);
  30   table
  31 ;;
  32
  33 let demodulate_term env table cmp term =
  34   let hd_term = head_of_term term in
  35   let candidates = Hashtbl.find table hd_term in
  36
  37
  38
  39
  40