From: Alberto Griggio Date: Sun, 19 Jun 2005 10:08:55 +0000 (+0000) Subject: path indexing integration X-Git-Tag: INDEXING_NO_PROOFS~114 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a89f7271e79dc7dc81dc868a75125669c8decc16;p=helm.git path indexing integration --- diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile index d1d4c0427..be59fc135 100644 --- a/helm/ocaml/paramodulation/Makefile +++ b/helm/ocaml/paramodulation/Makefile @@ -4,16 +4,9 @@ TEST_REQUIRES = \ helm-registry \ helm-tactics \ helm-cic_transformations \ - helm-cic_textual_parser2 \ -# helm-mathql_interpreter \ -# helm-mathql_generator \ -# helm-xmldiff -# lablgtk2 \ -# mathml-editor \ -# lablgtkmathview \ -# mysql + helm-cic_textual_parser2 -REQUIRES = $(TEST_REQUIRES) #gdome2-xslt helm-hbugs lablgtk2.init lablgtk2.glade +REQUIRES = $(TEST_REQUIRES) OCAMLOPTIONS = \ -package "$(REQUIRES)" -predicates "$(PREDICATES)" #-pp camlp4o -thread @@ -32,26 +25,24 @@ TEST_LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $ all: saturation opt: saturation.opt -start: - $(MAKE) -C ../hbugs/ start -stop: - $(MAKE) -C ../hbugs/ stop - INTERFACE_FILES = \ utils.mli \ inference.mli DEPOBJS = \ $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \ + path_indexing.ml \ indexing.ml \ - saturation.ml + saturation.ml \ + test_path_indexing.ml TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) \ + path_indexing.cmo \ indexing.cmo \ saturation.cmo -# TESTOBJS = \ -# disambiguatingParser.cmo \ -# batchParser.cmo +TESTOBJS = $(INTERFACE_FILES:%.mli=%.cmo) \ + path_indexing.cmo \ + test_path_indexing.cmo # REGTESTOBJS = $(TESTOBJS) regtest.cmo # TESTLIBOBJS = $(TESTOBJS) testlibrary.cmo @@ -66,6 +57,9 @@ saturation: $(TOPLEVELOBJS) $(LIBRARIES) saturation.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) $(OCAMLOPT) -thread -linkpkg -o $@ $(TOPLEVELOBJS:.cmo=.cmx) +test_path_indexing: $(TESTOBJS) $(TEST_LIBRARIES) + $(OCAMLC) -linkpkg -o $@ $(TESTOBJS) + .SUFFIXES: .ml .mli .cmo .cmi .cmx .ml.cmo: $(OCAMLC) -c $< @@ -79,53 +73,6 @@ $(TOPLEVELOBJS:.cmo=.cmx)): $(LIBRARIES_OPT) clean: rm -f *.cm[iox] *.o saturation{,.opt} regtest{,.opt} testlibrary{,.opt} -install: - cp gTopLevel gTopLevel.opt $(BIN_DIR) -uninstall: - rm -f $(BIN_DIR)/gTopLevel $(BIN_DIR)/gTopLevel.opt - -.PHONY: install uninstall clean test - -INTESTS := $(wildcard tests/*.cic) -OUTTESTS := $(patsubst %, %.test, $(INTESTS)) -gentest: $(OUTTESTS) -cleantest: - rm -f $(OUTTESTS) -tests/%.cic.test: tests/%.cic regtest - time ./regtest -gen $< -test: regtest - ./regtest $(INTESTS) 2> /dev/null -test.opt: regtest.opt - ./regtest.opt $(INTESTS) 2> /dev/null -envtest: regtest - ./regtest -dump $(INTESTS) 2> /dev/null -envtest.opt: regtest.opt - ./regtest.opt -dump $(INTESTS) 2> /dev/null -librarytest: testlibrary - ./testlibrary -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG -librarytest.opt: testlibrary.opt - ./testlibrary.opt -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG -typecheck_uri: typecheck_uri.ml - $(OCAMLFIND) ocamlc -thread -package helm-cic_proof_checking -linkpkg -o $@ $< -typecheck_uri.opt: typecheck_uri.ml - $(OCAMLFIND) opt -thread -package helm-cic_proof_checking -linkpkg -o $@ $< - -MAIN = ./gTopLevel -ARGS = -debug: - echo "load_printer \"threads.cma\"" > .debug_script - $(OCAMLFIND) query -recursive -predicates "mt,byte" -a-format \ - helm-cic_unification | \ - sed 's/\(.*\)/load_printer "\1"/' \ - >> .debug_script - echo "install_printer CicMetaSubst.fppsubst" >> .debug_script - echo "install_printer CicMetaSubst.fppterm" >> .debug_script - echo "install_printer CicMetaSubst.fppmetasenv" >> .debug_script - ledit $(OCAMLDEBUG) \ - -source .debug_script \ - -I +threads \ - $(shell $(OCAMLFIND) query -recursive -i-format $(REQUIRES)) \ - $(MAIN) $(ARGS) ifneq ($(MAKECMDGOALS), depend) include .depend diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 055314676..84559b222 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -1,8 +1,3 @@ -(** settable by the command line (-i switch) *) -let use_index = ref true;; - - -type pos = Left | Right ;; let head_of_term = function | Cic.Appl (hd::tl) -> hd @@ -10,6 +5,12 @@ let head_of_term = function ;; +(* +let empty_table () = + Hashtbl.create 10 +;; + + let index table eq = let _, (_, l, r, ordering), _, _ = eq in let hl = head_of_term l in @@ -21,13 +22,13 @@ let index table eq = let _ = match ordering with | Utils.Gt -> - index hl Left + index hl Utils.Left | Utils.Lt -> - index hr Right - | _ -> index hl Left; index hr Right + index hr Utils.Right + | _ -> index hl Utils.Left; index hr Utils.Right in -(* index hl Left; *) -(* index hr Right; *) +(* index hl Utils.Left; *) +(* index hr Utils.Right; *) table ;; @@ -41,11 +42,20 @@ let remove_index table eq = let newentry = List.filter (fun e -> e <> (pos, eq)) x_entry in Hashtbl.replace table x newentry in - remove_index hl Left; - remove_index hr Right; + remove_index hl Utils.Left; + remove_index hr Utils.Right; table ;; +*) + + +let empty_table () = + Path_indexing.PSTrie.empty +;; +let index = Path_indexing.index +and remove_index = Path_indexing.remove_index;; + let rec find_matches metasenv context ugraph lift_amount term = let module C = Cic in @@ -55,47 +65,26 @@ let rec find_matches metasenv context ugraph lift_amount term = let module HL = HelmLibraryObjects in let cmp = !Utils.compare_terms in let names = Utils.names_of_context context in -(* Printf.printf "CHIAMO find_matches (%s) su: %s\n" *) -(* (if unif_fun == Inference.matching then "MATCHING" *) -(* else if unif_fun == CicUnification.fo_unif then "UNIFICATION" *) -(* else "??????????") *) -(* (CicPp.pp term names); *) function | [] -> None | candidate::tl -> let pos, (proof, (ty, left, right, o), metas, args) = candidate in let do_match c other eq_URI = -(* Printf.printf "provo con %s: %s, %s\n\n" *) -(* (if unif_fun == Inference.matching then "MATCHING" *) -(* else if unif_fun == CicUnification.fo_unif then "UNIFICATION" *) -(* else "??????????") *) -(* (CicPp.pp term names) *) -(* (CicPp.pp (S.lift lift_amount c) names); *) let subst', metasenv', ugraph' = -(* Inference.matching (metasenv @ metas) context term *) -(* (S.lift lift_amount c) ugraph *) Inference.matching (metasenv @ metas) context term (S.lift lift_amount c) ugraph in -(* let names = U.names_of_context context in *) -(* Printf.printf "MATCH FOUND: %s, %s\n" *) -(* (CicPp.pp term names) (CicPp.pp (S.lift lift_amount c) names); *) Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph', (candidate, eq_URI)) -(* (proof, ty, c, other, eq_URI)) *) in let c, other, eq_URI = - if pos = Left then left, right, HL.Logic.eq_ind_URI + if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI else right, left, HL.Logic.eq_ind_r_URI in if o <> U.Incomparable then try -(* print_endline "SONO QUI!"; *) - let res = do_match c other eq_URI in -(* print_endline "RITORNO RES"; *) - res + do_match c other eq_URI with e -> -(* Printf.printf "ERRORE!: %s\n" (Printexc.to_string e); *) find_matches metasenv context ugraph lift_amount term tl else let res = try do_match c other eq_URI with e -> None in @@ -105,10 +94,6 @@ let rec find_matches metasenv context ugraph lift_amount term = and other' = M.apply_subst s other in let order = cmp c' other' in let names = U.names_of_context context in -(* Printf.printf "c': %s\nother': %s\norder: %s\n\n" *) -(* (CicPp.pp c' names) (CicPp.pp other' names) *) -(* (U.string_of_comparison order); *) -(* if cmp (M.apply_subst s c) (M.apply_subst s other) = U.Gt then *) if order = U.Gt then res else @@ -118,11 +103,131 @@ let rec find_matches metasenv context ugraph lift_amount term = ;; -let get_candidates table term = - if !use_index then - try Hashtbl.find table (head_of_term term) with Not_found -> [] - else - Hashtbl.fold (fun k v l -> v @ l) table [] +let rec find_all_matches ?(unif_fun=CicUnification.fo_unif) + metasenv context ugraph lift_amount term = + let module C = Cic in + let module U = Utils in + let module S = CicSubstitution in + let module M = CicMetaSubst in + let module HL = HelmLibraryObjects in + let cmp = !Utils.compare_terms in + let names = Utils.names_of_context context in + function + | [] -> [] + | candidate::tl -> + let pos, (proof, (ty, left, right, o), metas, args) = candidate in + let do_match c other eq_URI = + let subst', metasenv', ugraph' = + unif_fun (metasenv @ metas) context + term (S.lift lift_amount c) ugraph + in + (C.Rel (1 + lift_amount), subst', metasenv', ugraph', + (candidate, eq_URI)) + in + let c, other, eq_URI = + if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI + else right, left, HL.Logic.eq_ind_r_URI + in + if o <> U.Incomparable then + try + let res = do_match c other eq_URI in + res::(find_all_matches ~unif_fun metasenv context ugraph + lift_amount term tl) + with e -> + find_all_matches ~unif_fun metasenv context ugraph + lift_amount term tl + else + try + let res = do_match c other eq_URI in + match res with + | _, s, _, _, _ -> + let c' = M.apply_subst s c + and other' = M.apply_subst s other in + let order = cmp c' other' in + let names = U.names_of_context context in + if order <> U.Lt && order <> U.Le then + res::(find_all_matches ~unif_fun metasenv context ugraph + lift_amount term tl) + else + find_all_matches ~unif_fun metasenv context ugraph + lift_amount term tl + with e -> + find_all_matches ~unif_fun metasenv context ugraph + lift_amount term tl +;; + + +type retrieval_mode = Matching | Unification;; + +(* +let get_candidates mode table term = + try Hashtbl.find table (head_of_term term) with Not_found -> [] +;; +*) + + +let get_candidates mode trie term = + let s = + match mode with + | Matching -> + Path_indexing.retrieve_generalizations trie term + | Unification -> + Path_indexing.retrieve_unifiables trie term + in + Path_indexing.PosEqSet.elements s +;; + + +let subsumption env table target = + let _, (ty, tl, tr, _), tmetas, _ = target in + let metasenv, context, ugraph = env in + let metasenv = metasenv @ tmetas in + let samesubst subst subst' = + let tbl = Hashtbl.create (List.length subst) in + List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst; + List.for_all + (fun (m, (c, t1, t2)) -> + try + let c', t1', t2' = Hashtbl.find tbl m in + if (c = c') && (t1 = t1') && (t2 = t2') then true + else false + with Not_found -> + true) + subst' + in + let subsaux left right = + let leftc = get_candidates Matching table left in + let leftr = + find_all_matches ~unif_fun:Inference.matching + metasenv context ugraph 0 left leftc + in + let ok what (_, subst, menv, ug, ((pos, (_, (_, l, r, o), _, _)), _)) = + try + let other = if pos = Utils.Left then r else l in + let subst', menv', ug' = + Inference.matching metasenv context what other ugraph in + samesubst subst subst' + with e -> + false + in + let r = List.exists (ok right) leftr in + if r then + true + else + let rightc = get_candidates Matching table right in + let rightr = + find_all_matches ~unif_fun:Inference.matching + metasenv context ugraph 0 right rightc + in + List.exists (ok left) rightr + in + let res = subsaux tl tr in + if res then ( + Printf.printf "subsumption!:\ntarget: %s\n" + (Inference.string_of_equality ~env target); + print_newline (); + ); + res ;; @@ -131,7 +236,7 @@ let rec demodulate_term metasenv context ugraph table lift_amount term = let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in - let candidates = get_candidates table term in + let candidates = get_candidates Matching table term in match term with | C.Meta _ -> None | term -> @@ -184,8 +289,6 @@ let rec demodulate_term metasenv context ugraph table lift_amount term = subst, menv, ug, eq_found) ) | t -> -(* Printf.printf "Ne` Appl ne` Prod: %s\n" *) -(* (CicPp.pp t (Utils.names_of_context context)); *) None ;; @@ -197,15 +300,10 @@ let rec demodulation newmeta env table target = let module HL = HelmLibraryObjects in let metasenv, context, ugraph = env in let proof, (eq_ty, left, right, order), metas, args = target in -(* let _ = *) -(* let names = Utils.names_of_context context in *) -(* Printf.printf "demodulation %s = %s\n" *) -(* (CicPp.pp left names) (CicPp.pp right names) *) -(* in *) let metasenv' = metasenv @ metas in let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) = let pos, (proof', (ty, what, other, _), menv', args') = eq_found in - let what, other = if pos = Left then what, other else other, what in + let what, other = if pos = Utils.Left then what, other else other, what in let newterm, newproof = let bo = M.apply_subst subst (S.subst other t) in let bo'' = @@ -232,14 +330,22 @@ let rec demodulation newmeta env table target = newmeta, (newproof, (eq_ty, left, right, ordering), newmetasenv, newargs) in let res = demodulate_term metasenv' context ugraph table 0 left in + let build_identity (p, (t, l, r, o), m, a) = + match o with + | Utils.Gt -> (p, (t, r, r, Utils.Eq), m, a) + | _ -> (p, (t, l, l, Utils.Eq), m, a) + in match res with | Some t -> let newmeta, newtarget = build_newtarget true t in if (Inference.is_identity (metasenv', context, ugraph) newtarget) || (Inference.meta_convertibility_eq target newtarget) then newmeta, newtarget - else - demodulation newmeta env table newtarget + else + if subsumption env table newtarget then + newmeta, build_identity newtarget + else + demodulation newmeta env table newtarget | None -> let res = demodulate_term metasenv' context ugraph table 0 right in match res with @@ -248,68 +354,22 @@ let rec demodulation newmeta env table target = if (Inference.is_identity (metasenv', context, ugraph) newtarget) || (Inference.meta_convertibility_eq target newtarget) then newmeta, newtarget - else - demodulation newmeta env table newtarget + else + if subsumption env table newtarget then + newmeta, build_identity newtarget + else + demodulation newmeta env table newtarget | None -> newmeta, target ;; -let rec find_all_matches metasenv context ugraph lift_amount term = - let module C = Cic in - let module U = Utils in - let module S = CicSubstitution in - let module M = CicMetaSubst in - let module HL = HelmLibraryObjects in - let cmp = !Utils.compare_terms in - let names = Utils.names_of_context context in - function - | [] -> [] - | candidate::tl -> - let pos, (proof, (ty, left, right, o), metas, args) = candidate in - let do_match c other eq_URI = - let subst', metasenv', ugraph' = - CicUnification.fo_unif (metasenv @ metas) context - term (S.lift lift_amount c) ugraph - in - (C.Rel (1 + lift_amount), subst', metasenv', ugraph', - (candidate, eq_URI)) - in - let c, other, eq_URI = - if pos = Left then left, right, HL.Logic.eq_ind_URI - else right, left, HL.Logic.eq_ind_r_URI - in - if o <> U.Incomparable then - try - let res = do_match c other eq_URI in - res::(find_all_matches metasenv context ugraph lift_amount term tl) - with e -> - find_all_matches metasenv context ugraph lift_amount term tl - else - try - let res = do_match c other eq_URI in - match res with - | _, s, _, _, _ -> - let c' = M.apply_subst s c - and other' = M.apply_subst s other in - let order = cmp c' other' in - let names = U.names_of_context context in - if order <> U.Lt && order <> U.Le then - res::(find_all_matches metasenv context ugraph - lift_amount term tl) - else - find_all_matches metasenv context ugraph lift_amount term tl - with e -> - find_all_matches metasenv context ugraph lift_amount term tl -;; - - let rec betaexpand_term metasenv context ugraph table lift_amount term = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in - let candidates = get_candidates table term in + let candidates = get_candidates Unification table term in let res, lifted_term = match term with | C.Meta (i, l) -> @@ -396,18 +456,10 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = match term with | C.Meta _ -> res, lifted_term | term -> -(* let names = Utils.names_of_context context in *) -(* Printf.printf "CHIAMO find_all_matches su: %s\n" (CicPp.pp term names); *) let r = find_all_matches metasenv context ugraph lift_amount term candidates in r @ res, lifted_term -(* match *) -(* find_all_matches metasenv context ugraph lift_amount term candidates *) -(* with *) -(* | None -> res, lifted_term *) -(* | Some r -> *) -(* r::res, lifted_term *) ;; @@ -418,7 +470,6 @@ let superposition_left (metasenv, context, ugraph) table target = let module HL = HelmLibraryObjects in let module CR = CicReduction in let module U = Utils in -(* print_endline "superposition_left"; *) let proof, (eq_ty, left, right, ordering), _, _ = target in let expansions, _ = let term = if ordering = U.Gt then left else right in @@ -426,7 +477,7 @@ let superposition_left (metasenv, context, ugraph) table target = in let build_new (bo, s, m, ug, (eq_found, eq_URI)) = let pos, (proof', (ty, what, other, _), menv', args') = eq_found in - let what, other = if pos = Left then what, other else other, what in + let what, other = if pos = Utils.Left then what, other else other, what in let newgoal, newproof = let bo' = M.apply_subst s (S.subst other bo) in let bo'' = @@ -458,7 +509,6 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let module HL = HelmLibraryObjects in let module CR = CicReduction in let module U = Utils in -(* print_endline "superposition_right"; *) let eqproof, (eq_ty, left, right, ordering), newmetas, args = target in let metasenv' = metasenv @ newmetas in let maxmeta = ref newmeta in @@ -479,7 +529,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = in let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) = let pos, (proof', (ty, what, other, _), menv', args') = eq_found in - let what, other = if pos = Left then what, other else other, what in + let what, other = if pos = Utils.Left then what, other else other, what in let newgoal, newproof = let bo' = M.apply_subst s (S.subst other bo) in let bo'' = @@ -503,11 +553,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = and newargs = args @ args' in let eq' = (newproof, (eq_ty, left, right, neworder), newmenv, newargs) and env = (metasenv, context, ugraph) in -(* Printf.printf "eq' prima di fix_metas: %s\n" *) -(* (Inference.string_of_equality eq' ~env); *) let newm, eq' = Inference.fix_metas !maxmeta eq' in -(* Printf.printf "eq' dopo fix_metas: %s\n" *) -(* (Inference.string_of_equality eq' ~env); *) newm, eq' in maxmeta := newmeta; diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index 4a20f5c3d..f2c475799 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -406,3 +406,10 @@ let string_of_sign = function | Positive -> "Positive" ;; + +type pos = Left | Right + +let string_of_pos = function + | Left -> "Left" + | Right -> "Right" +;; diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli index 295d1aa4d..71f2fc1b5 100644 --- a/helm/ocaml/paramodulation/utils.mli +++ b/helm/ocaml/paramodulation/utils.mli @@ -36,3 +36,6 @@ type equality_sign = Negative | Positive val string_of_sign: equality_sign -> string +type pos = Left | Right + +val string_of_pos: pos -> string