From: Alberto Griggio Date: Thu, 12 May 2005 17:02:22 +0000 (+0000) Subject: first commit of paramodulation-based theorem proving for helm... X-Git-Tag: single_binding~80 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=03cff55eef08d25984bc92080e4cac93889f3ba7;p=helm.git first commit of paramodulation-based theorem proving for helm... --- diff --git a/helm/ocaml/paramodulation/.cvsignore b/helm/ocaml/paramodulation/.cvsignore new file mode 100644 index 000000000..9ef1b560e --- /dev/null +++ b/helm/ocaml/paramodulation/.cvsignore @@ -0,0 +1,2 @@ +*.cm[iaox] *.cmxa +.depend diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile new file mode 100644 index 000000000..fba57a593 --- /dev/null +++ b/helm/ocaml/paramodulation/Makefile @@ -0,0 +1,130 @@ +BIN_DIR = /usr/local/bin + +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 + +REQUIRES = $(TEST_REQUIRES) #gdome2-xslt helm-hbugs lablgtk2.init lablgtk2.glade + +OCAMLOPTIONS = \ + -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o -thread +OCAMLFIND = ocamlfind +OCAMLDEBUGOPTIONS = -g +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) +OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = $(OCAMLFIND) ocamldep -pp camlp4o +OCAMLDEBUG = wowcamldebug + +LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) +LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) +TEST_LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(TEST_REQUIRES)) +TEST_LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(TEST_REQUIRES)) + +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) \ + saturation.ml + +TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) saturation.cmo +# TESTOBJS = \ +# disambiguatingParser.cmo \ +# batchParser.cmo +# REGTESTOBJS = $(TESTOBJS) regtest.cmo +# TESTLIBOBJS = $(TESTOBJS) testlibrary.cmo + +$(INTERFACE_FILES:%.mli=%.cmo): $(LIBRARIES) +$(INTERFACE_FILES:%.mli=%.cmx): $(LIBRARIES_OPT) + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +saturation: $(TOPLEVELOBJS) $(LIBRARIES) + $(OCAMLC) -thread -linkpkg -o $@ $(TOPLEVELOBJS) +saturation.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) + $(OCAMLOPT) -thread -linkpkg -o $@ $(TOPLEVELOBJS:.cmo=.cmx) + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: + $(OCAMLC) -c $< +.mli.cmi: + $(OCAMLC) -c $< +.ml.cmx: + $(OCAMLOPT) -c $< + +$(TOPLEVELOBJS): $(LIBRARIES) +$(TOPLEVELOBJS:.cmo=.cmx)): $(LIBRARIES_OPT) + +clean: + rm -f *.cm[iox] *.o gTopLevel{,.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 +endif + diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml new file mode 100644 index 000000000..5eb89650b --- /dev/null +++ b/helm/ocaml/paramodulation/inference.ml @@ -0,0 +1,800 @@ +open Utils;; + + +exception NotMetaConvertible;; + +let meta_convertibility_aux table t1 t2 = + let module C = Cic in + let rec aux table t1 t2 = + match t1, t2 with + | t1, t2 when t1 = t2 -> table + | C.Meta (m1, tl1), C.Meta (m2, tl2) -> + let m1_binding, table = + try List.assoc m1 table, table + with Not_found -> m2, (m1, m2)::table + in + if m1_binding <> m2 then + raise NotMetaConvertible + else ( + try + List.fold_left2 + (fun res t1 t2 -> + match t1, t2 with + | None, Some _ | Some _, None -> raise NotMetaConvertible + | None, None -> res + | Some t1, Some t2 -> (aux res t1 t2)) + table tl1 tl2 + with Invalid_argument _ -> + raise NotMetaConvertible + ) + | C.Var (u1, ens1), C.Var (u2, ens2) + | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) -> + aux_ens table ens1 ens2 + | C.Cast (s1, t1), C.Cast (s2, t2) + | C.Prod (_, s1, t1), C.Prod (_, s2, t2) + | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2) + | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) -> + let table = aux table s1 s2 in + aux table t1 t2 + | C.Appl l1, C.Appl l2 -> ( + try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2 + with Invalid_argument _ -> raise NotMetaConvertible + ) + | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2) + when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2 + | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2) + when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 -> + aux_ens table ens1 ens2 + | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2) + when (UriManager.eq u1 u2) && i1 = i2 -> + let table = aux table s1 s2 in + let table = aux table t1 t2 in ( + try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2 + with Invalid_argument _ -> raise NotMetaConvertible + ) + | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> ( + try + List.fold_left2 + (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) -> + if i1 <> i2 then raise NotMetaConvertible + else + let res = (aux res s1 s2) in aux res t1 t2) + table il1 il2 + with Invalid_argument _ -> raise NotMetaConvertible + ) + | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> ( + try + List.fold_left2 + (fun res (n1, s1, t1) (n2, s2, t2) -> + let res = aux res s1 s2 in aux res t1 t2) + table il1 il2 + with Invalid_argument _ -> raise NotMetaConvertible + ) + | _, _ -> raise NotMetaConvertible + + and aux_ens table ens1 ens2 = + let cmp (u1, t1) (u2, t2) = + compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2) + in + let ens1 = List.sort cmp ens1 + and ens2 = List.sort cmp ens2 in + try + List.fold_left2 + (fun res (u1, t1) (u2, t2) -> + if not (UriManager.eq u1 u2) then raise NotMetaConvertible + else aux res t1 t2) + table ens1 ens2 + with Invalid_argument _ -> raise NotMetaConvertible + in + aux table t1 t2 +;; + + +let meta_convertibility_eq eq1 eq2 = + let _, (ty, left, right), _, _ = eq1 + and _, (ty', left', right'), _, _ = eq2 in + if ty <> ty' then + false + else + let print_table t w = + Printf.printf "table %s is:\n" w; + List.iter + (fun (k, v) -> Printf.printf "?%d: ?%d\n" k v) + t; + print_newline (); + in + try + let table = meta_convertibility_aux [] left left' in +(* print_table table "before"; *) + let table = meta_convertibility_aux table right right' in +(* print_table table "after"; *) + true + with NotMetaConvertible -> +(* Printf.printf "NotMetaConvertible:\n%s = %s\n%s = %s\n\n" *) +(* (CicPp.ppterm left) (CicPp.ppterm right) *) +(* (CicPp.ppterm left') (CicPp.ppterm right'); *) + false +;; + + +let meta_convertibility t1 t2 = + try + let _ = meta_convertibility_aux [] t1 t2 in + true + with NotMetaConvertible -> + false +;; + + +let beta_expand ?(metas_ok=true) ?(match_only=false) + what type_of_what where context metasenv ugraph = + let module S = CicSubstitution in + let module C = Cic in + (* + return value: + ((list of all possible beta expansions, subst, metasenv, ugraph), + lifted term) + *) + let rec aux lift_amount term context metasenv subst ugraph = +(* Printf.printf "enter aux %s\n" (CicPp.ppterm term); *) + let res, lifted_term = + match term with + | C.Rel m -> + [], if m <= lift_amount then C.Rel m else C.Rel (m+1) + + | C.Var (uri, exp_named_subst) -> + let ens', lifted_ens = + aux_ens lift_amount exp_named_subst context metasenv subst ugraph + in + let expansions = + List.map + (fun (e, s, m, ug) -> + (C.Var (uri, e), s, m, ug)) ens' + in + expansions, C.Var (uri, lifted_ens) + + | C.Meta (i, l) -> + let l', lifted_l = + List.fold_right + (fun arg (res, lifted_tl) -> + match arg with + | Some arg -> + let arg_res, lifted_arg = + aux lift_amount arg context metasenv subst ugraph in + let l1 = + List.map + (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug) + arg_res + in + (l1 @ + (List.map + (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug) + res), + (Some lifted_arg)::lifted_tl) + | None -> + (List.map + (fun (r, s, m, ug) -> None::r, s, m, ug) + res, + None::lifted_tl) + ) l ([], []) + in + let e = + List.map + (fun (l, s, m, ug) -> + (C.Meta (i, l), s, m, ug)) l' + in + e, C.Meta (i, lifted_l) + + | C.Sort _ + | C.Implicit _ as t -> [], t + + | C.Cast (s, t) -> + let l1, lifted_s = + aux lift_amount s context metasenv subst ugraph in + let l2, lifted_t = + aux lift_amount t context metasenv subst ugraph + in + let l1' = + List.map + (fun (t, s, m, ug) -> + C.Cast (t, lifted_t), s, m, ug) l1 in + let l2' = + List.map + (fun (t, s, m, ug) -> + C.Cast (lifted_s, t), s, m, ug) l2 in + l1'@l2', C.Cast (lifted_s, lifted_t) + + | C.Prod (nn, s, t) -> + let l1, lifted_s = + aux lift_amount s context metasenv subst ugraph in + let l2, lifted_t = + aux (lift_amount+1) t ((Some (nn, C.Decl s))::context) + metasenv subst ugraph + in + let l1' = + List.map + (fun (t, s, m, ug) -> + C.Prod (nn, t, lifted_t), s, m, ug) l1 in + let l2' = + List.map + (fun (t, s, m, ug) -> + C.Prod (nn, lifted_s, t), s, m, ug) l2 in + l1'@l2', C.Prod (nn, lifted_s, lifted_t) + + | C.Lambda (nn, s, t) -> + let l1, lifted_s = + aux lift_amount s context metasenv subst ugraph in + let l2, lifted_t = + aux (lift_amount+1) t ((Some (nn, C.Decl s))::context) + metasenv subst ugraph + in + let l1' = + List.map + (fun (t, s, m, ug) -> + C.Lambda (nn, t, lifted_t), s, m, ug) l1 in + let l2' = + List.map + (fun (t, s, m, ug) -> + C.Lambda (nn, lifted_s, t), s, m, ug) l2 in + l1'@l2', C.Lambda (nn, lifted_s, lifted_t) + + | C.LetIn (nn, s, t) -> + let l1, lifted_s = + aux lift_amount s context metasenv subst ugraph in + let l2, lifted_t = + aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context) + metasenv subst ugraph + in + let l1' = + List.map + (fun (t, s, m, ug) -> + C.LetIn (nn, t, lifted_t), s, m, ug) l1 in + let l2' = + List.map + (fun (t, s, m, ug) -> + C.LetIn (nn, lifted_s, t), s, m, ug) l2 in + l1'@l2', C.LetIn (nn, lifted_s, lifted_t) + + | C.Appl l -> + let l', lifted_l = + aux_list lift_amount l context metasenv subst ugraph + in + (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l', + C.Appl lifted_l) + + | C.Const (uri, exp_named_subst) -> + let ens', lifted_ens = + aux_ens lift_amount exp_named_subst context metasenv subst ugraph + in + let expansions = + List.map + (fun (e, s, m, ug) -> + (C.Const (uri, e), s, m, ug)) ens' + in + (expansions, C.Const (uri, lifted_ens)) + + | C.MutInd (uri, i ,exp_named_subst) -> + let ens', lifted_ens = + aux_ens lift_amount exp_named_subst context metasenv subst ugraph + in + let expansions = + List.map + (fun (e, s, m, ug) -> + (C.MutInd (uri, i, e), s, m, ug)) ens' + in + (expansions, C.MutInd (uri, i, lifted_ens)) + + | C.MutConstruct (uri, i, j, exp_named_subst) -> + let ens', lifted_ens = + aux_ens lift_amount exp_named_subst context metasenv subst ugraph + in + let expansions = + List.map + (fun (e, s, m, ug) -> + (C.MutConstruct (uri, i, j, e), s, m, ug)) ens' + in + (expansions, C.MutConstruct (uri, i, j, lifted_ens)) + + | C.MutCase (sp, i, outt, t, pl) -> + let pl_res, lifted_pl = + aux_list lift_amount pl context metasenv subst ugraph + in + let l1, lifted_outt = + aux lift_amount outt context metasenv subst ugraph in + let l2, lifted_t = + aux lift_amount t context metasenv subst ugraph in + + let l1' = + List.map + (fun (outt, s, m, ug) -> + C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in + let l2' = + List.map + (fun (t, s, m, ug) -> + C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in + let l3' = + List.map + (fun (pl, s, m, ug) -> + C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res + in + (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl)) + + | C.Fix (i, fl) -> + let len = List.length fl in + let fl', lifted_fl = + List.fold_right + (fun (nm, idx, ty, bo) (res, lifted_tl) -> + let lifted_ty = S.lift lift_amount ty in + let bo_res, lifted_bo = + aux (lift_amount+len) bo context metasenv subst ugraph in + let l1 = + List.map + (fun (a, s, m, ug) -> + (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug) + bo_res + in + (l1 @ + (List.map + (fun (r, s, m, ug) -> + (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res), + (nm, idx, lifted_ty, lifted_bo)::lifted_tl) + ) fl ([], []) + in + (List.map + (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl', + C.Fix (i, lifted_fl)) + + | C.CoFix (i, fl) -> + let len = List.length fl in + let fl', lifted_fl = + List.fold_right + (fun (nm, ty, bo) (res, lifted_tl) -> + let lifted_ty = S.lift lift_amount ty in + let bo_res, lifted_bo = + aux (lift_amount+len) bo context metasenv subst ugraph in + let l1 = + List.map + (fun (a, s, m, ug) -> + (nm, lifted_ty, a)::lifted_tl, s, m, ug) + bo_res + in + (l1 @ + (List.map + (fun (r, s, m, ug) -> + (nm, lifted_ty, lifted_bo)::r, s, m, ug) res), + (nm, lifted_ty, lifted_bo)::lifted_tl) + ) fl ([], []) + in + (List.map + (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl', + C.CoFix (i, lifted_fl)) + in + let retval = + match term with + | C.Meta _ when (not metas_ok) -> + res, lifted_term + | _ -> + try + let subst', metasenv', ugraph' = + CicUnification.fo_unif metasenv context + (S.lift lift_amount what) term ugraph + in + (* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *) + (* (CicPp.ppterm (S.lift lift_amount what)); *) + (* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *) + (* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *) + (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *) + let term' = CicMetaSubst.apply_subst subst' term in ( + if match_only && not (meta_convertibility term term') then ( +(* Printf.printf "term e term' sono diversi!:\n%s\n%s\n\n" *) +(* (CicPp.ppterm term) (CicPp.ppterm term'); *) + res, lifted_term + ) + else +(* let _ = *) +(* if match_only then *) +(* Printf.printf "OK, trovato match con %s\n" *) +(* (CicPp.ppterm term) *) +(* in *) + ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, + lifted_term) + ) + with _ -> + res, lifted_term + in +(* Printf.printf "exit aux\n"; *) + retval + + and aux_list lift_amount l context metasenv subst ugraph = + List.fold_right + (fun arg (res, lifted_tl) -> + let arg_res, lifted_arg = + aux lift_amount arg context metasenv subst ugraph in + let l1 = List.map + (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res + in + (l1 @ (List.map + (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res), + lifted_arg::lifted_tl) + ) l ([], []) + + and aux_ens lift_amount exp_named_subst context metasenv subst ugraph = + List.fold_right + (fun (u, arg) (res, lifted_tl) -> + let arg_res, lifted_arg = + aux lift_amount arg context metasenv subst ugraph in + let l1 = + List.map + (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res + in + (l1 @ (List.map (fun (r, s, m, ug) -> + (u, lifted_arg)::r, s, m, ug) res), + (u, lifted_arg)::lifted_tl) + ) exp_named_subst ([], []) + + in + let expansions, _ = aux 0 where context metasenv [] ugraph in + List.map + (fun (term, subst, metasenv, ugraph) -> + let term' = C.Lambda (C.Anonymous, type_of_what, term) in +(* Printf.printf "term is: %s\nsubst is:\n%s\n\n" *) +(* (CicPp.ppterm term') (print_subst subst); *) + (term', subst, metasenv, ugraph)) + expansions +;; + + +type equality = + Cic.term * (* proof *) + (Cic.term * (* type *) + Cic.term * (* left side *) + Cic.term) * (* right side *) + Cic.metasenv * (* environment for metas *) + Cic.term list (* arguments *) +;; + + +let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = + let module C = Cic in + let module S = CicSubstitution in + let module T = CicTypeChecker in + let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in + let rec aux index newmeta = function + | [] -> [], newmeta + | (Some (_, C.Decl (term)))::tl -> + let do_find context term = + match term with + | C.Prod (name, s, t) -> +(* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *) + let (head, newmetas, args, _) = + PrimitiveTactics.new_metasenv_for_apply newmeta proof + context (S.lift index term) + in + let newmeta = + List.fold_left + (fun maxm arg -> + match arg with + | C.Meta (i, _) -> (max maxm i) + | _ -> assert false) + newmeta args + in + let p = + if List.length args = 0 then + C.Rel index + else + C.Appl ((C.Rel index)::args) + in ( + match head with + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> + Printf.printf "OK: %s\n" (CicPp.ppterm term); + Some (p, (ty, t1, t2), newmetas, args), (newmeta+1) + | _ -> None, newmeta + ) + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> + Some (C.Rel index, + (ty, S.lift index t1, S.lift index t2), [], []), (newmeta+1) + | _ -> None, newmeta + in ( + match do_find context term with + | Some p, newmeta -> + let tl, newmeta' = (aux (index+1) newmeta tl) in + p::tl, max newmeta newmeta' + | None, _ -> + aux (index+1) newmeta tl + ) + | _::tl -> + aux (index+1) newmeta tl + in + aux 1 newmeta context +;; + + +let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) = + let newargs, _ = + List.fold_right + (fun t (newargs, index) -> + match t with + | Cic.Meta (i, l) -> ((Cic.Meta (index, l))::newargs, index+1) + | _ -> assert false) + args ([], newmeta) + in + let repl where = + ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs + ~where + in + let menv', _ = + List.fold_right + (fun (i, context, term) (menv, index) -> + ((index, context, term)::menv, index+1)) + menv ([], newmeta) + in + (newmeta + (List.length newargs) + 1, + (repl proof, (repl ty, repl left, repl right), menv', newargs)) +;; + + +exception TermIsNotAnEquality;; + +let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function + | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> + (proof, (ty, t1, t2), [], []) + | _ -> + raise TermIsNotAnEquality +;; + + +type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;; + + +let superposition_left (metasenv, context, ugraph) target source = + let module C = Cic in + let module S = CicSubstitution in + let module M = CicMetaSubst in + let module HL = HelmLibraryObjects in + let module CR = CicReduction in + (* we assume that target is ground (does not contain metavariables): this + * should always be the case (I hope, at least) *) + let proof, (eq_ty, left, right), _, _ = target in + let eqproof, (ty, t1, t2), newmetas, args = source in + + (* ALB: TODO check that ty and eq_ty are indeed equal... *) + assert (eq_ty = ty); + + let where, is_left = + match nonrec_kbo left right with + | Lt -> right, false + | Gt -> left, true + | _ -> ( + Printf.printf "????????? %s = %s" (CicPp.ppterm left) + (CicPp.ppterm right); + print_newline (); + assert false (* again, for ground terms this shouldn't happen... *) + ) + in + let metasenv' = newmetas @ metasenv in + let res1 = + List.filter + (fun (t, s, m, ug) -> + nonrec_kbo (M.apply_subst s t1) (M.apply_subst s t2) = Gt) + (beta_expand t1 ty where context metasenv' ugraph) + and res2 = + List.filter + (fun (t, s, m, ug) -> + nonrec_kbo (M.apply_subst s t2) (M.apply_subst s t1) = Gt) + (beta_expand t2 ty where context metasenv' ugraph) + in +(* let what, other = *) +(* if is_left then left, right *) +(* else right, left *) +(* in *) + let build_new what other eq_URI (t, s, m, ug) = + let newgoal, newgoalproof = + match t with + | C.Lambda (nn, ty, bo) -> + let bo' = S.subst (M.apply_subst s other) bo in + let bo'' = + C.Appl ( + [C.MutInd (HL.Logic.eq_URI, 0, []); + S.lift 1 eq_ty] @ + if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo']) + in + let t' = C.Lambda (nn, ty, bo'') in + S.subst (M.apply_subst s other) bo, + M.apply_subst s + (C.Appl [C.Const (eq_URI, []); ty; what; t'; + proof; other; eqproof]) + | _ -> assert false + in + let equation = + if is_left then (eq_ty, newgoal, right) + else (eq_ty, left, newgoal) + in + (eqproof, equation, [], []) + in + let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1 + and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in + new1 @ new2 +;; + + +let superposition_right newmeta (metasenv, context, ugraph) target source = + let module C = Cic in + let module S = CicSubstitution in + let module M = CicMetaSubst in + let module HL = HelmLibraryObjects in + let module CR = CicReduction in + let eqproof, (eq_ty, left, right), newmetas, args = target in + let eqp', (ty', t1, t2), newm', args' = source in + let maxmeta = ref newmeta in + + (* TODO check if ty and ty' are equal... *) + assert (eq_ty = ty'); + +(* let ok term subst other other_eq_side ugraph = *) +(* match term with *) +(* | C.Lambda (nn, ty, bo) -> *) +(* let bo' = S.subst (M.apply_subst subst other) bo in *) +(* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *) +(* not res *) +(* | _ -> assert false *) +(* in *) + let condition left right what other (t, s, m, ug) = + let subst = M.apply_subst s in + let cmp1 = nonrec_kbo (subst what) (subst other) in + let cmp2 = nonrec_kbo (subst left) (subst right) in +(* cmp1 = Gt && cmp2 = Gt *) + cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le +(* && (ok t s other right ug) *) + in + let metasenv' = metasenv @ newmetas @ newm' in + let beta_expand = beta_expand ~metas_ok:false in + let res1 = + List.filter + (condition left right t1 t2) + (beta_expand t1 eq_ty left context metasenv' ugraph) + and res2 = + List.filter + (condition left right t2 t1) + (beta_expand t2 eq_ty left context metasenv' ugraph) + and res3 = + List.filter + (condition right left t1 t2) + (beta_expand t1 eq_ty right context metasenv' ugraph) + and res4 = + List.filter + (condition right left t2 t1) + (beta_expand t2 eq_ty right context metasenv' ugraph) + in + let newmetas = newmetas @ newm' in + let newargs = args @ args' in + let build_new what other is_left eq_URI (t, s, m, ug) = +(* let what, other = *) +(* if is_left then left, right *) +(* else right, left *) +(* in *) + let newterm, neweqproof = + match t with + | C.Lambda (nn, ty, bo) -> + let bo' = M.apply_subst s (S.subst other bo) in + let bo'' = + C.Appl ( + [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @ + if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo']) + in + let t' = C.Lambda (nn, ty, bo'') in + bo', + M.apply_subst s + (C.Appl [C.Const (eq_URI, []); ty; what; t'; eqproof; other; eqp']) + | _ -> assert false + in + let newmeta, newequality = + let left, right = + if is_left then (newterm, M.apply_subst s right) + else (M.apply_subst s left, newterm) in + fix_metas !maxmeta + (neweqproof, (eq_ty, left, right), newmetas, newargs) + in + maxmeta := newmeta; + newequality + in + let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1 + and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2 + and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3 + and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in + let ok = function + | _, (_, left, right), _, _ -> + not (fst (CR.are_convertible context left right ugraph)) + in + !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4)) +;; + + +let demodulation newmeta (metasenv, context, ugraph) target source = + let module C = Cic in + let module S = CicSubstitution in + let module M = CicMetaSubst in + let module HL = HelmLibraryObjects in + let module CR = CicReduction in + + let proof, (eq_ty, left, right), metas, args = target + and proof', (ty, t1, t2), metas', args' = source in + if eq_ty <> ty then + newmeta, target + else + let get_params step = + match step with + | 3 -> true, t1, t2, HL.Logic.eq_ind_URI + | 2 -> false, t1, t2, HL.Logic.eq_ind_URI + | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI + | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI + | _ -> assert false + in + let rec demodulate newmeta step metasenv target = + let proof, (eq_ty, left, right), metas, args = target in + let is_left, what, other, eq_URI = get_params step in +(* Printf.printf *) +(* "demodulate\ntarget: %s = %s\nwhat: %s\nother: %s\nis_left: %s\n" *) +(* (CicPp.ppterm left) (CicPp.ppterm right) (CicPp.ppterm what) *) +(* (CicPp.ppterm other) (string_of_bool is_left); *) +(* Printf.printf "step: %d\n" step; *) +(* print_newline (); *) + let ok (t, s, m, ug) = + nonrec_kbo (M.apply_subst s what) (M.apply_subst s other) = Gt + in + let res = + List.filter ok + (beta_expand ~metas_ok:false ~match_only:true + what ty left context (metasenv @ metas) ugraph) + in + match res with + | [] -> + if step = 0 then newmeta, target + else demodulate newmeta (step-1) metasenv target + | (t, s, m, ug)::_ -> + let newterm, newproof = + match t with + | C.Lambda (nn, ty, bo) -> + let bo' = M.apply_subst s (S.subst other bo) in + let bo'' = + C.Appl ( + [C.MutInd (HL.Logic.eq_URI, 0, []); + S.lift 1 eq_ty] @ + if is_left then [bo'; S.lift 1 right] + else [S.lift 1 left; bo']) + in + let t' = C.Lambda (nn, ty, bo'') in + M.apply_subst s (S.subst other bo), + M.apply_subst s + (C.Appl [C.Const (eq_URI, []); ty; what; t'; + proof; other; proof']) + | _ -> assert false + in + let newmeta, newtarget = + let left, right = + if is_left then (newterm, M.apply_subst s right) + else (M.apply_subst s left, newterm) in + let newmetasenv = metasenv @ metas in + let newargs = args @ args' in + fix_metas newmeta + (newproof, (eq_ty, left, right), newmetasenv, newargs) + in + let _, (_, left, right), _, _ = newtarget + and _, (_, oldleft, oldright), _, _ = target in +(* Printf.printf *) +(* "demodulate, newtarget: %s = %s\ntarget was: %s = %s\n" *) +(* (CicPp.ppterm left) (CicPp.ppterm right) *) +(* (CicPp.ppterm oldleft) (CicPp.ppterm oldright); *) +(* print_newline (); *) + demodulate newmeta step metasenv newtarget + in + demodulate newmeta 3 (metasenv @ metas') target +;; + + +(* +let demodulation newmeta env target source = + newmeta, target +;; +*) + + diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli new file mode 100644 index 000000000..a895340c5 --- /dev/null +++ b/helm/ocaml/paramodulation/inference.mli @@ -0,0 +1,65 @@ +type equality = + Cic.term * (* proof *) + (Cic.term * (* type *) + Cic.term * (* left side *) + Cic.term) * (* right side *) + Cic.metasenv * (* environment for metas *) + Cic.term list (* arguments *) +;; + +type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;; + + +(** + Performs the beta expansion of the term "where" w.r.t. "what", + i.e. returns the list of all the terms t s.t. "(t what) = where". +*) +val beta_expand: + ?metas_ok:bool -> ?match_only:bool -> Cic.term -> Cic.term -> Cic.term -> + Cic.context -> Cic.metasenv -> CicUniv.universe_graph -> + (Cic.term * Cic.substitution * Cic.metasenv * CicUniv.universe_graph) list + + +(** + scans the context to find all Declarations "left = right"; returns a + list of tuples (proof, (type, left, right), newmetas). Uses + PrimitiveTactics.new_metasenv_for_apply to replace bound variables with + fresh metas... +*) +val find_equalities: + ?eq_uri:UriManager.uri -> Cic.context -> ProofEngineTypes.proof -> + equality list * int + + +exception TermIsNotAnEquality;; + +(** + raises TermIsNotAnEquality if term is not an equation. + The first Cic.term is a proof of the equation +*) +val equality_of_term: ?eq_uri:UriManager.uri -> Cic.term -> Cic.term -> + equality + +(** + superposition_left env target source + returns a list of new clauses inferred with a left superposition step + the negative equation "target" and the positive equation "source" +*) +val superposition_left: environment -> equality -> equality -> equality list + +(** + superposition_right newmeta env target source + returns a list of new clauses inferred with a right superposition step + the positive equations "target" and "source" + "newmeta" is the first free meta index, i.e. the first number above the + highest meta index: its updated value is also returned +*) +val superposition_right: + int -> environment -> equality -> equality -> int * equality list + +val demodulation: int -> environment -> equality -> equality -> int * equality + +val meta_convertibility: Cic.term -> Cic.term -> bool + +val meta_convertibility_eq: equality -> equality -> bool + diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml new file mode 100644 index 000000000..405ba15a6 --- /dev/null +++ b/helm/ocaml/paramodulation/saturation.ml @@ -0,0 +1,387 @@ +open Inference;; +open Utils;; + +type result = + | Failure + | Success of Cic.term option * environment +;; + + +type equality_sign = Negative | Positive;; + +let string_of_sign = function + | Negative -> "Negative" + | Positive -> "Positive" +;; + + +let string_of_equality ?env = + match env with + | None -> ( + function + | _, (ty, left, right), _, _ -> + Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty) + (CicPp.ppterm left) (CicPp.ppterm right) + ) + | Some (_, context, _) -> ( + let names = names_of_context context in + function + | _, (ty, left, right), _, _ -> + Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names) + (CicPp.pp left names) (CicPp.pp right names) + ) +;; + + +module OrderedEquality = +struct + type t = Inference.equality + + let compare eq1 eq2 = + match meta_convertibility_eq eq1 eq2 with + | true -> 0 + | false -> Pervasives.compare eq1 eq2 +end + +module EqualitySet = Set.Make(OrderedEquality);; + + + +let select env passive = + match passive with + | hd::tl, pos -> (Negative, hd), (tl, pos) + | [], hd::tl -> (Positive, hd), ([], tl) + | _, _ -> assert false +;; + + +(* +let select env passive = + match passive with + | neg, pos when EqualitySet.is_empty neg -> + let elem = EqualitySet.min_elt pos in + (Positive, elem), (neg, EqualitySet.remove elem pos) + | neg, pos -> + let elem = EqualitySet.min_elt neg in + (Negative, elem), (EqualitySet.remove elem neg, pos) +;; +*) + + +(* TODO: find a better way! *) +let maxmeta = ref 0;; + +let infer env sign current active = + let rec infer_negative current = function + | [] -> [], [] + | (Negative, _)::tl -> infer_negative current tl + | (Positive, equality)::tl -> + let res = superposition_left env current equality in + let neg, pos = infer_negative current tl in + res @ neg, pos + + and infer_positive current = function + | [] -> [], [] + | (Negative, equality)::tl -> + let res = superposition_left env equality current in + let neg, pos = infer_positive current tl in + res @ neg, pos + | (Positive, equality)::tl -> + let maxm, res = superposition_right !maxmeta env current equality in + let maxm, res' = superposition_right maxm env equality current in + maxmeta := maxm; + let neg, pos = infer_positive current tl in + +(* Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *) +(* (string_of_equality ~env current) (string_of_equality ~env equality) *) +(* (String.concat "\n" (List.map (string_of_equality ~env) res)); *) +(* Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *) +(* (string_of_equality ~env equality) (string_of_equality ~env current) *) +(* (String.concat "\n" (List.map (string_of_equality ~env) res')); *) + + neg, res @ res' @ pos + in + match sign with + | Negative -> infer_negative current active + | Positive -> infer_positive current active +;; + + +let contains_empty env (negative, positive) = + let metasenv, context, ugraph = env in + try + let (proof, _, _, _) = + List.find + (fun (proof, (ty, left, right), m, a) -> + fst (CicReduction.are_convertible context left right ugraph)) + negative + in + true, Some proof + with Not_found -> + false, None +;; + + +let add_to_passive (passive_neg, passive_pos) (new_neg, new_pos) = + let find sign eq1 eq2 = + if meta_convertibility_eq eq1 eq2 then ( +(* Printf.printf "Trovato equazione duplicata di segno %s\n%s\n\n" *) +(* (string_of_sign sign) (string_of_equality eq1); *) + true + ) else + false + in + let ok sign equalities equality = + not (List.exists (find sign equality) equalities) + in + let neg = List.filter (ok Negative passive_neg) new_neg in + let pos = List.filter (ok Positive passive_pos) new_pos in +(* let neg, pos = new_neg, new_pos in *) + (neg @ passive_neg, passive_pos @ pos) +;; + + +let is_identity ((_, context, ugraph) as env) = function + | ((_, (ty, left, right), _, _) as equality) -> + let res = + (left = right || + (fst (CicReduction.are_convertible context left right ugraph))) + in +(* if res then ( *) +(* Printf.printf "is_identity: %s" (string_of_equality ~env equality); *) +(* print_newline (); *) +(* ); *) + res +;; + + +let forward_simplify env (sign, current) active = +(* if sign = Negative then *) +(* Some (sign, current) *) +(* else *) + let rec aux env (sign, current) = + function + | [] -> Some (sign, current) + | (Negative, _)::tl -> aux env (sign, current) tl + | (Positive, equality)::tl -> + let newmeta, current = demodulation !maxmeta env current equality in + maxmeta := newmeta; + if is_identity env current then + None + else + aux env (sign, current) tl + in + aux env (sign, current) active +;; + + +let forward_simplify_new env (new_neg, new_pos) active = + let remove_identities equalities = + let ok eq = not (is_identity env eq) in + List.filter ok equalities + in + let rec simpl active target = + match active with + | [] -> target + | (Negative, _)::tl -> simpl tl target + | (Positive, source)::tl -> + let newmeta, target = demodulation !maxmeta env target source in + maxmeta := newmeta; + if is_identity env target then target + else simpl tl target + in + let new_neg = List.map (simpl active) new_neg + and new_pos = List.map (simpl active) new_pos in + new_neg, remove_identities new_pos +;; + + +let backward_simplify env (sign, current) active = + match sign with + | Negative -> active + | Positive -> + let active = + List.map + (fun (s, equality) -> + (* match s with *) + (* | Negative -> s, equality *) + (* | Positive -> *) + let newmeta, equality = + demodulation !maxmeta env equality current in + maxmeta := newmeta; + s, equality) + active + in + let active = + List.filter (fun (s, eq) -> not (is_identity env eq)) active + in + let find eq1 where = + List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where + in + List.fold_right + (fun (s, eq) res -> if find eq res then res else (s, eq)::res) + active [] +;; + + +(* +let add_to_passive (passive_neg, passive_pos) (new_neg, new_pos) = + let add_all = List.fold_left (fun res eq -> EqualitySet.add eq res) in + add_all passive_neg new_neg, add_all passive_pos new_pos +;; +*) + + +let rec given_clause env passive active = + match passive with +(* | s1, s2 when (EqualitySet.is_empty s1) && (EqualitySet.is_empty s2) -> *) +(* Failure *) + | [], [] -> Failure + | passive -> +(* Printf.printf "before select\n"; *) + let (sign, current), passive = select env passive in +(* Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *) +(* (string_of_sign sign) (string_of_equality ~env current); *) + match forward_simplify env (sign, current) active with + | None when sign = Negative -> + Printf.printf "OK!!! %s %s" (string_of_sign sign) + (string_of_equality ~env current); + print_newline (); + let proof, _, _, _ = current in + Success (Some proof, env) + | None -> + Printf.printf "avanti... %s %s" (string_of_sign sign) + (string_of_equality ~env current); + print_newline (); + given_clause env passive active + | Some (sign, current) -> +(* Printf.printf "sign: %s\ncurrent: %s\n" *) +(* (string_of_sign sign) (string_of_equality ~env current); *) +(* print_newline (); *) + + let new' = infer env sign current active in + + let active = + backward_simplify env (sign, current) active +(* match new' with *) +(* | [], [] -> backward_simplify env (sign, current) active *) +(* | _ -> active *) + in + + let new' = forward_simplify_new env new' active in + + print_endline "\n================================================"; + let _ = + Printf.printf "active:\n%s\n" + (String.concat "\n" + ((List.map + (fun (s, e) -> (string_of_sign s) ^ " " ^ + (string_of_equality ~env e)) active))); + print_newline (); + in +(* let _ = *) +(* match new' with *) +(* | neg, pos -> *) +(* Printf.printf "new':\n%s\n" *) +(* (String.concat "\n" *) +(* ((List.map *) +(* (fun e -> "Negative " ^ *) +(* (string_of_equality ~env e)) neg) @ *) +(* (List.map *) +(* (fun e -> "Positive " ^ *) +(* (string_of_equality ~env e)) pos))); *) +(* print_newline (); *) +(* in *) + match contains_empty env new' with + | false, _ -> + let active = + match sign with + | Negative -> (sign, current)::active + | Positive -> active @ [(sign, current)] + in + let passive = add_to_passive passive new' in + given_clause env passive active + | true, proof -> + Success (proof, env) +;; + + +let get_from_user () = + let dbd = Mysql.quick_connect + ~host:"localhost" ~user:"helm" ~database:"mowgli" () in + let rec get () = + match read_line () with + | "" -> [] + | t -> t::(get ()) + in + let term_string = String.concat "\n" (get ()) in + let env, metasenv, term, ugraph = + List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0 + in + term, metasenv, ugraph +;; + + +let main () = + let module C = Cic in + let module T = CicTypeChecker in + let module PET = ProofEngineTypes in + let module PP = CicPp in + let term, metasenv, ugraph = get_from_user () in + let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in + let proof, goals = + PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in + let goal = List.nth goals 0 in + let _, metasenv, meta_proof, _ = proof in + let _, context, goal = CicUtil.lookup_meta goal metasenv in + let equalities, maxm = find_equalities context proof in + maxmeta := maxm; (* TODO ugly!! *) + let env = (metasenv, context, ugraph) in + try + let term_equality = equality_of_term meta_proof goal in + let meta_proof, (eq_ty, left, right), _, _ = term_equality in + let active = [] in +(* let passive = *) +(* (EqualitySet.singleton term_equality, *) +(* List.fold_left *) +(* (fun res eq -> EqualitySet.add eq res) EqualitySet.empty equalities) *) +(* in *) + let passive = [term_equality], equalities in + Printf.printf "\ncurrent goal: %s ={%s} %s\n" + (PP.ppterm left) (PP.ppterm eq_ty) (PP.ppterm right); + Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); + Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv); + Printf.printf "\nequalities:\n"; + List.iter + (function (_, (ty, t1, t2), _, _) -> + let w1 = weight_of_term t1 in + let w2 = weight_of_term t2 in + let res = nonrec_kbo t1 t2 in + Printf.printf "{%s}: %s<%s> %s %s<%s>\n" (PP.ppterm ty) + (PP.ppterm t1) (string_of_weight w1) + (string_of_comparison res) + (PP.ppterm t2) (string_of_weight w2)) + equalities; + print_endline "--------------------------------------------------"; + let start = Sys.time () in + print_endline "GO!"; + let res = given_clause env passive active in + let finish = Sys.time () in + match res with + | Failure -> + Printf.printf "NO proof found! :-(\n\n" + | Success (Some proof, env) -> + Printf.printf "OK, found a proof!:\n%s\n%.9f\n" (PP.ppterm proof) + (finish -. start); + | Success (None, env) -> + Printf.printf "Success, but no proof?!?\n\n" + with exc -> + print_endline ("EXCEPTION: " ^ (Printexc.to_string exc)); +;; + + +let _ = + let configuration_file = "../../gTopLevel/gTopLevel.conf.xml" in + Helm_registry.load_from configuration_file +in +main () diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml new file mode 100644 index 000000000..01293a958 --- /dev/null +++ b/helm/ocaml/paramodulation/utils.ml @@ -0,0 +1,289 @@ +let print_metasenv metasenv = + String.concat "\n--------------------------\n" + (List.map (fun (i, context, term) -> + (string_of_int i) ^ " [\n" ^ (CicPp.ppcontext context) ^ + "\n] " ^ (CicPp.ppterm term)) + metasenv) +;; + + +let print_subst subst = + String.concat "\n" + (List.map + (fun (i, (c, t, ty)) -> + Printf.sprintf "?%d -> %s : %s" i + (CicPp.ppterm t) (CicPp.ppterm ty)) + subst) +;; + +(* (weight of constants, [(meta, weight_of_meta)]) *) +type weight = int * (int * int) list;; + +let string_of_weight (cw, mw) = + let s = + String.concat ", " + (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw) + in + Printf.sprintf "[%d; %s]" cw s + + +let weight_of_term term = + (* ALB: what to consider as a variable? I think "variables" in our case are + Metas and maybe Rels... *) + let module C = Cic in + let vars_dict = Hashtbl.create 5 in + let rec aux = function + | C.Meta (metano, _) -> + (try + let oldw = Hashtbl.find vars_dict metano in + Hashtbl.replace vars_dict metano (oldw+1) + with Not_found -> + Hashtbl.add vars_dict metano 1); + 0 + + | C.Var (_, ens) + | C.Const (_, ens) + | C.MutInd (_, _, ens) + | C.MutConstruct (_, _, _, ens) -> + List.fold_left (fun w (u, t) -> (aux t) + w) 1 ens + + | C.Cast (t1, t2) + | C.Lambda (_, t1, t2) + | C.Prod (_, t1, t2) + | C.LetIn (_, t1, t2) -> + let w1 = aux t1 in + let w2 = aux t2 in + w1 + w2 + 1 + + | C.Appl l -> List.fold_left (+) 0 (List.map aux l) + + | C.MutCase (_, _, outt, t, pl) -> + let w1 = aux outt in + let w2 = aux t in + let w3 = List.fold_left (+) 0 (List.map aux pl) in + w1 + w2 + w3 + 1 + + | C.Fix (_, fl) -> + List.fold_left (fun w (n, i, t1, t2) -> (aux t1) + (aux t2) + w) 1 fl + + | C.CoFix (_, fl) -> + List.fold_left (fun w (n, t1, t2) -> (aux t1) + (aux t2) + w) 1 fl + + | _ -> 1 + in + let w = aux term in + let l = + Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict [] in + let compare w1 w2 = + match w1, w2 with + | (m1, _), (m2, _) -> m2 - m1 + in + (w, List.sort compare l) (* from the biggest meta to the smallest (0) *) +;; + + +(* returns a "normalized" version of the polynomial weight wl (with type + * weight list), i.e. a list sorted ascending by meta number, + * from 0 to maxmeta. wl must be sorted descending by meta number. Example: + * normalize_weight 5 (3, [(3, 2); (1, 1)]) -> + * (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *) +let normalize_weight maxmeta (cw, wl) = +(* Printf.printf "normalize_weight: %d, %s\n" maxmeta *) +(* (string_of_weight (cw, wl)); *) + let rec aux = function + | 0 -> [] + | m -> (m, 0)::(aux (m-1)) + in + let tmpl = aux maxmeta in + let wl = + List.sort + (fun (m, _) (n, _) -> Pervasives.compare m n) + (List.fold_left + (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl) + in + (cw, wl) +;; + + +let normalize_weights (cw1, wl1) (cw2, wl2) = + let rec aux wl1 wl2 = + match wl1, wl2 with + | [], [] -> [], [] + | (m, w)::tl1, (n, w')::tl2 when m = n -> + let res1, res2 = aux tl1 tl2 in + (m, w)::res1, (n, w')::res2 + | (m, w)::tl1, ((n, w')::_ as wl2) when m < n -> + let res1, res2 = aux tl1 wl2 in + (m, w)::res1, (m, 0)::res2 + | ((m, w)::_ as wl1), (n, w')::tl2 when m > n -> + let res1, res2 = aux wl1 tl2 in + (n, 0)::res1, (n, w')::res2 + | [], (n, w)::tl2 -> + let res1, res2 = aux [] tl2 in + (n, 0)::res1, (n, w)::res2 + | (m, w)::tl1, [] -> + let res1, res2 = aux tl1 [] in + (m, w)::res1, (m, 0)::res2 + in + let cmp (m, _) (n, _) = compare m n in + let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in + (cw1, wl1), (cw2, wl2) +;; + + +type comparison = Lt | Le | Eq | Ge | Gt | Incomparable;; + +let string_of_comparison = function + | Lt -> "<" + | Le -> "<=" + | Gt -> ">" + | Ge -> ">=" + | Eq -> "=" + | Incomparable -> "I" + + +let compare_weights ?(normalize=false) + ((h1, w1) as weight1) ((h2, w2) as weight2)= + let (h1, w1), (h2, w2) = + if normalize then +(* let maxmeta = *) +(* let maxmeta l = *) +(* try *) +(* match List.hd l with *) +(* | (m, _) -> m *) +(* with Failure _ -> 0 *) +(* in *) +(* max (maxmeta w1) (maxmeta w2) *) +(* in *) +(* (normalize_weight maxmeta (h1, w1)), (normalize_weight maxmeta (h2, w2)) *) + normalize_weights weight1 weight2 + else + (h1, w1), (h2, w2) + in + let res, diffs = + try + List.fold_left2 + (fun ((lt, eq, gt), diffs) w1 w2 -> + match w1, w2 with + | (meta1, w1), (meta2, w2) when meta1 = meta2 -> + let diffs = (w1 - w2) + diffs in + let r = compare w1 w2 in + if r < 0 then (lt+1, eq, gt), diffs + else if r = 0 then (lt, eq+1, gt), diffs + else (lt, eq, gt+1), diffs + | (meta1, w1), (meta2, w2) -> + Printf.printf "HMMM!!!! %s, %s\n" + (string_of_weight weight1) (string_of_weight weight2); + assert false) + ((0, 0, 0), 0) w1 w2 + with Invalid_argument _ -> + Printf.printf "Invalid_argument: %s{%s}, %s{%s}, normalize = %s\n" + (string_of_weight (h1, w1)) (string_of_weight weight1) + (string_of_weight (h2, w2)) (string_of_weight weight2) + (string_of_bool normalize); + assert false + in + let hdiff = h1 - h2 in + match res with + | (0, _, 0) -> + if hdiff < 0 then Lt + else if hdiff > 0 then Gt + else Eq (* Incomparable *) + | (m, _, 0) -> + if hdiff <= 0 then + if m > 0 || hdiff < 0 then Lt + else if diffs >= (- hdiff) then Le else Incomparable + else + if diffs >= (- hdiff) then Le else Incomparable + | (0, _, m) -> + if hdiff >= 0 then + if m > 0 || hdiff > 0 then Gt + else if (- diffs) >= hdiff then Ge else Incomparable + else + if (- diffs) >= hdiff then Ge else Incomparable + | (m, _, n) when m > 0 && n > 0 -> + Incomparable +;; + + +let rec aux_ordering t1 t2 = + let module C = Cic in + let compare_uris u1 u2 = + let res = + compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2) in + if res < 0 then Lt + else if res = 0 then Eq + else Gt + in + match t1, t2 with + | C.Meta _, _ + | _, C.Meta _ -> Incomparable + + | t1, t2 when t1 = t2 -> Eq + + | C.Rel n, C.Rel m -> if n > m then Lt else Gt (* ALB: changed < to > *) + | C.Rel _, _ -> Lt + | _, C.Rel _ -> Gt + + | C.Const (u1, _), C.Const (u2, _) -> compare_uris u1 u2 + | C.Const _, _ -> Lt + | _, C.Const _ -> Gt + + | C.MutInd (u1, _, _), C.MutInd (u2, _, _) -> compare_uris u1 u2 + | C.MutInd _, _ -> Lt + | _, C.MutInd _ -> Gt + + | C.MutConstruct (u1, _, _, _), C.MutConstruct (u2, _, _, _) -> + compare_uris u1 u2 + | C.MutConstruct _, _ -> Lt + | _, C.MutConstruct _ -> Gt + + | C.Appl l1, C.Appl l2 -> + let rec cmp t1 t2 = + match t1, t2 with + | [], [] -> Eq + | _, [] -> Gt + | [], _ -> Lt + | hd1::tl1, hd2::tl2 -> + let o = aux_ordering hd1 hd2 in + if o = Eq then cmp tl1 tl2 + else o + in + cmp l1 l2 + + | t1, t2 -> + Printf.printf "These two terms are not comparable:\n%s\n%s\n\n" + (CicPp.ppterm t1) (CicPp.ppterm t2); + Incomparable +;; + + +(* w1, w2 are the weights, they should already be normalized... *) +let nonrec_kbo_w (t1, w1) (t2, w2) = + match compare_weights w1 w2 with + | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable + | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable + | Eq -> aux_ordering t1 t2 + | res -> res +;; + + +let nonrec_kbo t1 t2 = + let w1 = weight_of_term t1 in + let w2 = weight_of_term t2 in + match compare_weights ~normalize:true w1 w2 with + | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable + | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable + | Eq -> aux_ordering t1 t2 + | res -> res +;; + + +let names_of_context context = + List.map + (function + | None -> None + | Some (n, e) -> Some n) + context +;; + diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli new file mode 100644 index 000000000..471e6e307 --- /dev/null +++ b/helm/ocaml/paramodulation/utils.mli @@ -0,0 +1,26 @@ +(* (weight of constants, [(meta, weight_of_meta)]) *) +type weight = int * (int * int) list;; + +type comparison = Lt | Le | Eq | Ge | Gt | Incomparable;; + +val print_metasenv: Cic.metasenv -> string + +val print_subst: Cic.substitution -> string + +val string_of_weight: weight -> string + +val weight_of_term: Cic.term -> weight + +val normalize_weight: int -> weight -> weight + +val string_of_comparison: comparison -> string + +val compare_weights: ?normalize:bool -> weight -> weight -> comparison + +val nonrec_kbo: Cic.term -> Cic.term -> comparison + +val nonrec_kbo_w: (Cic.term * weight) -> (Cic.term * weight) -> comparison + +val names_of_context: Cic.context -> (Cic.name option) list + +