From 5462948747cca234512fd998678cb9315785d68c Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 7 Jun 2005 06:44:39 +0000 Subject: [PATCH] My two pennies. --- helm/ocaml/paramodulation/indexing.ml | 40 +++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 helm/ocaml/paramodulation/indexing.ml diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml new file mode 100644 index 000000000..8ed8f49a1 --- /dev/null +++ b/helm/ocaml/paramodulation/indexing.ml @@ -0,0 +1,40 @@ +(* type naif_indexing = + (Cic.term * ((bool * Inference.equality) list)) list +;; *) + +type pos = Left | Right +;; + +let head_of_term = + function + | Cic.Appl hd::tl -> hd + | t -> t +;; + +let index table eq = + let (_,(_,l,r,ordering),_,_) = eq in + let hl = head_of_term l in + let hr = head_of_term r in + let index x pos = + let x_entry = + try Hashtbl.find table x + with Not_found -> [] in + Hashtbl.replace table x (pos,eq)::x_entry in + (match ordering with + | Utils.Gt -> + index hl Left + | Utils.Lt -> + index hr Right + | _ -> index hl Left; + index hr Right); + table +;; + +let demodulate_term env table cmp term = + let hd_term = head_of_term term in + let candidates = Hashtbl.find table hd_term in + + + + + -- 2.39.2