From b1527286e32c8651d65619af61e3f638b3b89f8d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 12 Jan 2006 12:38:36 +0000 Subject: [PATCH] Moved paramodulation inside tactics. Added a new (reduction) tactic demodulate. --- helm/ocaml/grafite/grafiteAst.ml | 3 +- helm/ocaml/grafite/grafiteAstPp.ml | 1 + helm/ocaml/grafite_engine/grafiteEngine.ml | 13 +- .../grafite_parser/grafiteDisambiguate.ml | 1 + helm/ocaml/grafite_parser/grafiteParser.ml | 3 +- helm/ocaml/paramodulation/Makefile | 38 --- helm/ocaml/tactics/.depend | 19 ++ helm/ocaml/tactics/Makefile | 12 +- helm/ocaml/tactics/autoTactic.ml | 7 +- helm/ocaml/tactics/autoTactic.mli | 7 - .../{ => tactics}/paramodulation/.depend | 6 +- helm/ocaml/tactics/paramodulation/Makefile | 14 ++ .../ocaml/{ => tactics}/paramodulation/README | 2 + .../paramodulation/equality_indexing.ml | 0 .../paramodulation/equality_indexing.mli | 0 .../{ => tactics}/paramodulation/indexing.ml | 71 ++++-- .../{ => tactics}/paramodulation/inference.ml | 7 +- .../paramodulation/inference.mli | 0 .../paramodulation/saturate_main.ml | 47 ++-- .../paramodulation/saturation.ml | 31 ++- .../tactics/paramodulation/saturation.mli | 49 ++++ .../paramodulation/test_indexing.ml | 0 .../{ => tactics}/paramodulation/utils.ml | 230 ++++++++++++------ .../{ => tactics}/paramodulation/utils.mli | 2 + helm/ocaml/tactics/tactics.ml | 1 + helm/ocaml/tactics/tactics.mli | 3 + 26 files changed, 373 insertions(+), 194 deletions(-) delete mode 100644 helm/ocaml/paramodulation/Makefile rename helm/ocaml/{ => tactics}/paramodulation/.depend (65%) create mode 100644 helm/ocaml/tactics/paramodulation/Makefile rename helm/ocaml/{ => tactics}/paramodulation/README (96%) rename helm/ocaml/{ => tactics}/paramodulation/equality_indexing.ml (100%) rename helm/ocaml/{ => tactics}/paramodulation/equality_indexing.mli (100%) rename helm/ocaml/{ => tactics}/paramodulation/indexing.ml (94%) rename helm/ocaml/{ => tactics}/paramodulation/inference.ml (99%) rename helm/ocaml/{ => tactics}/paramodulation/inference.mli (100%) rename helm/ocaml/{ => tactics}/paramodulation/saturate_main.ml (84%) rename helm/ocaml/{ => tactics}/paramodulation/saturation.ml (99%) create mode 100644 helm/ocaml/tactics/paramodulation/saturation.mli rename helm/ocaml/{ => tactics}/paramodulation/test_indexing.ml (100%) rename helm/ocaml/{ => tactics}/paramodulation/utils.ml (84%) rename helm/ocaml/{ => tactics}/paramodulation/utils.mli (98%) diff --git a/helm/ocaml/grafite/grafiteAst.ml b/helm/ocaml/grafite/grafiteAst.ml index c9567155d..6c51fc80a 100644 --- a/helm/ocaml/grafite/grafiteAst.ml +++ b/helm/ocaml/grafite/grafiteAst.ml @@ -37,7 +37,8 @@ type ('term, 'ident) type_spec = | Type of UriManager.uri * int type 'lazy_term reduction = - [ `Normalize + [ `Demodulate + | `Normalize | `Reduce | `Simpl | `Unfold of 'lazy_term option diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml index 6abfa4dd6..8bd5c96f1 100644 --- a/helm/ocaml/grafite/grafiteAstPp.ml +++ b/helm/ocaml/grafite/grafiteAstPp.ml @@ -36,6 +36,7 @@ let command_terminator = tactical_terminator let pp_idents idents = "[" ^ String.concat "; " idents ^ "]" let pp_reduction_kind ~term_pp = function + | `Demodulate -> "demodulate" | `Normalize -> "normalize" | `Reduce -> "reduce" | `Simpl -> "simplify" diff --git a/helm/ocaml/grafite_engine/grafiteEngine.ml b/helm/ocaml/grafite_engine/grafiteEngine.ml index c0a453c93..60b2b6a9d 100644 --- a/helm/ocaml/grafite_engine/grafiteEngine.ml +++ b/helm/ocaml/grafite_engine/grafiteEngine.ml @@ -95,6 +95,8 @@ let tactic_of_ast ast = | GrafiteAst.Fold (_, reduction_kind, term, pattern) -> let reduction = match reduction_kind with + | `Demodulate -> + GrafiteTypes.command_error "demodulation can't be folded" | `Normalize -> PET.const_lazy_reduction (CicReduction.normalize ~delta:false ~subst:[]) @@ -136,11 +138,12 @@ let tactic_of_ast ast = Tactics.letin term ~mk_fresh_name_callback:(namer_of [name]) | GrafiteAst.Reduce (_, reduction_kind, pattern) -> (match reduction_kind with - | `Normalize -> Tactics.normalize ~pattern - | `Reduce -> Tactics.reduce ~pattern - | `Simpl -> Tactics.simpl ~pattern - | `Unfold what -> Tactics.unfold ~pattern what - | `Whd -> Tactics.whd ~pattern) + | `Demodulate -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~pattern + | `Normalize -> Tactics.normalize ~pattern + | `Reduce -> Tactics.reduce ~pattern + | `Simpl -> Tactics.simpl ~pattern + | `Unfold what -> Tactics.unfold ~pattern what + | `Whd -> Tactics.whd ~pattern) | GrafiteAst.Reflexivity _ -> Tactics.reflexivity | GrafiteAst.Replace (_, pattern, with_what) -> Tactics.replace ~pattern ~with_what diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml index 3d6f893ee..f5ea66f2f 100644 --- a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml +++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml @@ -81,6 +81,7 @@ let disambiguate_reduction_kind lexicon_status_ref = function | `Unfold (Some t) -> let t = disambiguate_lazy_term lexicon_status_ref t in `Unfold (Some t) + | `Demodulate | `Normalize | `Reduce | `Simpl diff --git a/helm/ocaml/grafite_parser/grafiteParser.ml b/helm/ocaml/grafite_parser/grafiteParser.ml index 90d1898ea..e480efd34 100644 --- a/helm/ocaml/grafite_parser/grafiteParser.ml +++ b/helm/ocaml/grafite_parser/grafiteParser.ml @@ -66,7 +66,8 @@ EXTEND [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] ]; reduction_kind: [ - [ IDENT "normalize" -> `Normalize + [ IDENT "demodulate" -> `Demodulate + | IDENT "normalize" -> `Normalize | IDENT "reduce" -> `Reduce | IDENT "simplify" -> `Simpl | IDENT "unfold"; t = OPT term -> `Unfold t diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile deleted file mode 100644 index 35b650ea7..000000000 --- a/helm/ocaml/paramodulation/Makefile +++ /dev/null @@ -1,38 +0,0 @@ -PACKAGE = paramodulation - -INTERFACE_FILES = \ - utils.mli \ - inference.mli\ - equality_indexing.mli - -IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) \ - indexing.ml \ - saturation.ml - -include ../Makefile.common - -paramodulation.cmo: $(IMPLEMENTATION_FILES:%.ml=%.cmo) - $(OCAMLC) -pack -o $@ $(IMPLEMENTATION_FILES:%.ml=%.cmo) - -paramodulation.cmx: OCAMLOPTIONS=-package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -paramodulation.cmx: $(IMPLEMENTATION_FILES:%.ml=%.cmx) - $(OCAMLOPT) -pack -o $@ $(IMPLEMENTATION_FILES:%.ml=%.cmx) - -OCAMLOPTIONS+=-for-pack Paramodulation - -$(ARCHIVE): paramodulation.cmo $(LIBRARIES) - $(OCAMLC) $(OCAMLARCHIVEOPTIONS) -a -o $@ \ - paramodulation.cmo - -$(ARCHIVE_OPT): paramodulation.cmx $(LIBRARIES_OPT) - $(OCAMLOPT) $(OCAMLARCHIVEOPTIONS) -a -o $@ \ - paramodulation.cmx - -PARAMOD_OBJS = $(IMPLEMENTATION_FILES:%.ml=%.cmo) -PARAMOD_OBJS_OPT = $(IMPLEMENTATION_FILES:%.ml=%.cmx) - -LOCALLINKOPTS = -package helm-cic_disambiguation,helm-content_pres,helm-grafite,helm-grafite_parser -saturate: saturate_main.ml $(PARAMOD_OBJS) $(LIBRARIES) - $(OCAMLC) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $(PARAMOD_OBJS) $< -saturate.opt: saturate_main.ml $(PARAMOD_OBJS_OPT) $(LIBRARIES) - $(OCAMLOPT) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $(PARAMOD_OBJS_OPT) $< diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 95131ecf4..dd623b9ae 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -5,6 +5,9 @@ reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi metadataQuery.cmi: proofEngineTypes.cmi +paramodulation/inference.cmi: proofEngineTypes.cmi +paramodulation/indexing.cmi: proofEngineTypes.cmi +paramodulation/saturation.cmi: proofEngineTypes.cmi variousTactics.cmi: proofEngineTypes.cmi autoTactic.cmi: proofEngineTypes.cmi introductionTactics.cmi: proofEngineTypes.cmi @@ -48,6 +51,22 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ hashtbl_equiv.cmi metadataQuery.cmi metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ hashtbl_equiv.cmx metadataQuery.cmi +paramodulation/utils.cmo: paramodulation/utils.cmi +paramodulation/utils.cmx: paramodulation/utils.cmi +paramodulation/inference.cmo: proofEngineReduction.cmi proofEngineHelpers.cmi \ + metadataQuery.cmi paramodulation/inference.cmi +paramodulation/inference.cmx: proofEngineReduction.cmx proofEngineHelpers.cmx \ + metadataQuery.cmx paramodulation/inference.cmi +paramodulation/equality_indexing.cmo: paramodulation/equality_indexing.cmi +paramodulation/equality_indexing.cmx: paramodulation/equality_indexing.cmi +paramodulation/indexing.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ + paramodulation/indexing.cmi +paramodulation/indexing.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ + paramodulation/indexing.cmi +paramodulation/saturation.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \ + primitiveTactics.cmi paramodulation/saturation.cmi +paramodulation/saturation.cmx: proofEngineTypes.cmx proofEngineReduction.cmx \ + primitiveTactics.cmx paramodulation/saturation.cmi variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ variousTactics.cmi diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 1595fb337..57937414c 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -6,18 +6,26 @@ INTERFACE_FILES = \ continuationals.mli \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \ + paramodulation/utils.mli \ + paramodulation/inference.mli\ + paramodulation/equality_indexing.mli\ + paramodulation/indexing.mli \ + paramodulation/saturation.mli \ variousTactics.mli autoTactic.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ equalityTactics.mli discriminationTactics.mli inversion.mli ring.mli \ fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \ statefulProofEngine.mli tactics.mli + IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) + all: -tactics.mli: tactics.ml *Tactics.mli *Tactic.mli fourierR.mli ring.mli +tactics.mli: tactics.ml *Tactics.mli *Tactic.mli fourierR.mli ring.mli paramodulation/indexing.mli echo "(* GENERATED FILE, DO NOT EDIT *)" > $@ - $(OCAMLC) -i $< >> $@ + $(OCAMLC) -I paramodulation -i $< >> $@ include ../Makefile.common +OCAMLOPTIONS+= -I paramodulation diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index dc5b8324c..42df90768 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -295,13 +295,14 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) ;; *) +(* let paramodulation_tactic = ref (fun dbd ?full ?depth ?width status -> raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));; let term_is_equality = ref (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);; - +*) let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ?full ~(dbd:HMysql.dbd) () = @@ -333,12 +334,12 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation | Some _ -> let _, metasenv, _, _ = proof in let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in - full || (!term_is_equality meta_goal) + full || (Inference.term_is_equality meta_goal) in if paramodulation_ok then ( debug_print (lazy "USO PARAMODULATION..."); (* try *) - !paramodulation_tactic dbd ~depth ~width ~full (proof, goal) + Saturation.saturate dbd ~depth ~width ~full (proof, goal) (* with ProofEngineTypes.Fail _ -> *) (* normal_auto () *) ) else diff --git a/helm/ocaml/tactics/autoTactic.mli b/helm/ocaml/tactics/autoTactic.mli index 696c97007..fe72629f0 100644 --- a/helm/ocaml/tactics/autoTactic.mli +++ b/helm/ocaml/tactics/autoTactic.mli @@ -29,10 +29,3 @@ val auto_tac: dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic -val paramodulation_tactic: - (HMysql.dbd -> ?full:bool -> ?depth:int -> ?width:int -> - ProofEngineTypes.status -> - ProofEngineTypes.proof * ProofEngineTypes.goal list) ref - -val term_is_equality: - (Cic.term -> bool) ref diff --git a/helm/ocaml/paramodulation/.depend b/helm/ocaml/tactics/paramodulation/.depend similarity index 65% rename from helm/ocaml/paramodulation/.depend rename to helm/ocaml/tactics/paramodulation/.depend index 7c6673bad..b5dd3a819 100644 --- a/helm/ocaml/paramodulation/.depend +++ b/helm/ocaml/tactics/paramodulation/.depend @@ -6,7 +6,7 @@ inference.cmo: utils.cmi inference.cmi inference.cmx: utils.cmx inference.cmi equality_indexing.cmo: utils.cmi inference.cmi equality_indexing.cmi equality_indexing.cmx: utils.cmx inference.cmx equality_indexing.cmi -indexing.cmo: utils.cmi inference.cmi equality_indexing.cmi -indexing.cmx: utils.cmx inference.cmx equality_indexing.cmx -saturation.cmo: utils.cmi inference.cmi indexing.cmo +indexing.cmo: utils.cmi inference.cmi equality_indexing.cmi indexing.cmi +indexing.cmx: utils.cmx inference.cmx equality_indexing.cmx indexing.cmi +saturation.cmo: utils.cmi inference.cmi indexing.cmi saturation.cmx: utils.cmx inference.cmx indexing.cmx diff --git a/helm/ocaml/tactics/paramodulation/Makefile b/helm/ocaml/tactics/paramodulation/Makefile new file mode 100644 index 000000000..af04e29c4 --- /dev/null +++ b/helm/ocaml/tactics/paramodulation/Makefile @@ -0,0 +1,14 @@ +PACKAGE = dummy + +LOCALLINKOPTS = -package helm-cic_disambiguation,helm-content_pres,helm-grafite,helm-grafite_parser,helm-tactics + +saturate: saturate_main.ml $(LIBRARIES) + $(OCAMLC) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $< +saturate.opt: saturate_main.ml $(PARAMOD_OBJS_OPT) $(LIBRARIES) + $(OCAMLOPT) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $(PARAMOD_OBJS_OPT) < + +clean: + rm saturate saturate.cmo saturate.cmx + +include ../../Makefile.common + diff --git a/helm/ocaml/paramodulation/README b/helm/ocaml/tactics/paramodulation/README similarity index 96% rename from helm/ocaml/paramodulation/README rename to helm/ocaml/tactics/paramodulation/README index 98deef5ad..bf484ae16 100644 --- a/helm/ocaml/paramodulation/README +++ b/helm/ocaml/tactics/paramodulation/README @@ -28,6 +28,8 @@ dove -l 10 e` il timeout in secondi. Il programma legge da standard input il teorema, per esempio \forall n:nat.n + n = 2 * n +\forall n:R.n + n = 2 * n +\forall n:R.n+n=n+n l'input termina con una riga vuota (quindi basta un doppio invio alla fine) diff --git a/helm/ocaml/paramodulation/equality_indexing.ml b/helm/ocaml/tactics/paramodulation/equality_indexing.ml similarity index 100% rename from helm/ocaml/paramodulation/equality_indexing.ml rename to helm/ocaml/tactics/paramodulation/equality_indexing.ml diff --git a/helm/ocaml/paramodulation/equality_indexing.mli b/helm/ocaml/tactics/paramodulation/equality_indexing.mli similarity index 100% rename from helm/ocaml/paramodulation/equality_indexing.mli rename to helm/ocaml/tactics/paramodulation/equality_indexing.mli diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/tactics/paramodulation/indexing.ml similarity index 94% rename from helm/ocaml/paramodulation/indexing.ml rename to helm/ocaml/tactics/paramodulation/indexing.ml index 2d9076ad5..b60435e04 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/tactics/paramodulation/indexing.ml @@ -145,7 +145,8 @@ let rec find_matches metasenv context ugraph lift_amount term termty = try let r = Inference.matching (metasenv @ metas) context - term (S.lift lift_amount c) ugraph in + term (S.lift lift_amount c) ugraph + in let t2 = Unix.gettimeofday () in match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); r @@ -174,7 +175,9 @@ let rec find_matches metasenv context ugraph lift_amount term termty = match res with | Some (_, s, _, _, _) -> let c' = apply_subst s c in - let other' = U.guarded_simpl context (apply_subst s other) in + (* + let other' = U.guarded_simpl context (apply_subst s other) in *) + let other' = apply_subst s other in let order = cmp c' other' in let names = U.names_of_context context in if order = U.Gt then @@ -458,7 +461,7 @@ let rec demodulation_equality newmeta env table sign target = in let what, other = if pos = Utils.Left then what, other else other, what in let newterm, newproof = - let bo = U.guarded_simpl context (apply_subst subst (S.subst other t)) in + let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in incr demod_counter; let bo' = @@ -517,7 +520,7 @@ let rec demodulation_equality newmeta env table sign target = in let left, right = if is_left then newterm, right else left, newterm in let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in - let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas + let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') and newargs = args in let ordering = !Utils.compare_terms left right in @@ -555,24 +558,13 @@ let rec demodulation_equality newmeta env table sign target = newmeta, target in (* newmeta, newtarget *) - (* tentiamo di ridurre usando CicReduction.normalize *) + (* tentiamo di normalizzare *) let w, p, (ty, left, right, o), m, a = newtarget in - let left' = ProofEngineReduction.simpl context left in - let right' = ProofEngineReduction.simpl context right in - let newleft = - if !Utils.compare_terms left' left = Utils.Lt then left' else left in - let newright = - if !Utils.compare_terms right' right = Utils.Lt then right' else right in -(* if newleft != left || newright != right then ( *) -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "left: %s, left': %s\nright: %s, right': %s\n" *) -(* (CicPp.ppterm left) (CicPp.ppterm left') (CicPp.ppterm right) *) -(* (CicPp.ppterm right'))) *) -(* ); *) - let w' = Utils.compute_equality_weight ty newleft newright in - let o' = !Utils.compare_terms newleft newright in - newmeta, (w', p, (ty, newleft, newright, o'), m, a) + let left = U.guarded_simpl context left in + let right = U.guarded_simpl context right in + let w' = Utils.compute_equality_weight ty left right in + let o' = !Utils.compare_terms left right in + newmeta, (w', p, (ty, left, right, o'), m, a) ;; @@ -838,7 +830,8 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in let what, other = if pos = Utils.Left then what, other else other, what in let newgoal, newproof = - let bo' = apply_subst s (S.subst other bo) in + (* qua *) + let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in let t' = let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in incr sup_r_counter; @@ -905,7 +898,8 @@ let rec demodulation_goal newmeta env table goal = with CicUtil.Meta_not_found _ -> ty in let newterm, newproof = - let bo = apply_subst subst (S.subst other t) in + (* qua *) + let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in let bo' = apply_subst subst t in let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in incr demod_counter; @@ -991,7 +985,8 @@ let rec demodulation_theorem newmeta env table theorem = let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in let what, other = if pos = Utils.Left then what, other else other, what in let newterm, newty = - let bo = apply_subst subst (S.subst other t) in + (* qua *) + let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in let bo' = apply_subst subst t in let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in incr demod_counter; @@ -1019,3 +1014,31 @@ let rec demodulation_theorem newmeta env table theorem = | None -> newmeta, theorem ;; + +let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = + let module I = Inference in + let curi,metasenv,pbo,pty = proof in + let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in + let eq_indexes, equalities, maxm = I.find_equalities context proof in + let lib_eq_uris, library_equalities, maxm = + I.find_library_equalities dbd context (proof, goal) (maxm+2) in + let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in + let library_equalities = List.map snd library_equalities in + let goalterm = Cic.Meta (metano,irl) in + let initgoal = Inference.BasicProof goalterm, [], goalterm in + let equalities = equalities @ library_equalities in + let table = + List.fold_left + (fun tbl eq -> index tbl eq) + empty equalities + in + let _,(newproof, newty, newmetasenv) = demodulation_goal + maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal + in + let proofterm = Inference.build_proof_term newproof in + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:proofterm) + initialstatus + +let demodulate_tac ~dbd ~pattern = + ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern) diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/tactics/paramodulation/inference.ml similarity index 99% rename from helm/ocaml/paramodulation/inference.ml rename to helm/ocaml/tactics/paramodulation/inference.ml index 04cdb0aeb..6c2a9b9dc 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/tactics/paramodulation/inference.ml @@ -507,7 +507,12 @@ let matching_simple metasenv context t1 t2 ugraph = let matching metasenv context t1 t2 ugraph = try let subst, metasenv, ugraph = - unification metasenv context t1 t2 ugraph +try + unification metasenv context t1 t2 ugraph +with CicUtil.Meta_not_found _ as exn -> + Printf.eprintf "t1 = %s\nt2 = %s\nmetasenv = %s\n%!" + (CicPp.ppterm t1) (CicPp.ppterm t2) (CicMetaSubst.ppmetasenv [] metasenv); + raise exn in let t' = CicMetaSubst.apply_subst subst t1 in if not (meta_convertibility t1 t') then diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/tactics/paramodulation/inference.mli similarity index 100% rename from helm/ocaml/paramodulation/inference.mli rename to helm/ocaml/tactics/paramodulation/inference.mli diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/tactics/paramodulation/saturate_main.ml similarity index 84% rename from helm/ocaml/paramodulation/saturate_main.ml rename to helm/ocaml/tactics/paramodulation/saturate_main.ml index bec597645..efcfca4ed 100644 --- a/helm/ocaml/paramodulation/saturate_main.ml +++ b/helm/ocaml/tactics/paramodulation/saturate_main.ml @@ -69,9 +69,9 @@ struct with Exit -> raise (Ambiguous_term (lazy term)) end -let configuration_file = ref "../../matita/matita.conf.xml";; +let configuration_file = ref "../../../matita/matita.conf.xml";; -let core_notation_script = "../../matita/core_notation.moo";; +let core_notation_script = "../../../matita/core_notation.moo";; let get_from_user ~(dbd:HMysql.dbd) = let rec get () = @@ -92,7 +92,7 @@ let retrieve_only = ref false;; let demod_equalities = ref false;; -let _ = +let main () = let module S = Saturation in let set_ratio v = S.weight_age_ratio := v; S.weight_age_counter := v and set_sel v = S.symbols_ratio := v; S.symbols_counter := v; @@ -140,22 +140,27 @@ let _ = "-retrieve", Arg.Unit set_retrieve, "retrieve only"; "-demod-equalities", Arg.Unit set_demod_equalities, "demod equalities"; - ] (fun a -> ()) "Usage:" -in -Helm_registry.load_from !configuration_file; -ignore (CicNotation2.load_notation [] core_notation_script); -ignore (CicNotation2.load_notation [] "../../matita/coq.ma"); -let dbd = HMysql.quick_connect - ~host:(Helm_registry.get "db.host") - ~user:(Helm_registry.get "db.user") - ~database:(Helm_registry.get "db.database") - () -in -let term, metasenv, ugraph = get_from_user ~dbd in -if !retrieve_only then - Saturation.retrieve_and_print dbd term metasenv ugraph -else if !demod_equalities then - Saturation.main_demod_equalities dbd term metasenv ugraph -else - Saturation.main dbd !full term metasenv ugraph + ] (fun a -> ()) "Usage:"; + Helm_registry.load_from !configuration_file; + ignore (CicNotation2.load_notation [] core_notation_script); + ignore (CicNotation2.load_notation [] "../../../matita/library/legacy/coq.ma"); + let dbd = HMysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") + () + in + let term, metasenv, ugraph = get_from_user ~dbd in + if !retrieve_only then + Saturation.retrieve_and_print dbd term metasenv ugraph + else if !demod_equalities then + Saturation.main_demod_equalities dbd term metasenv ugraph + else + Saturation.main dbd !full term metasenv ugraph ;; + +let _ = + (*try*) + main () + (*with exn -> prerr_endline (Printexc.to_string exn)*) + diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/tactics/paramodulation/saturation.ml similarity index 99% rename from helm/ocaml/paramodulation/saturation.ml rename to helm/ocaml/tactics/paramodulation/saturation.ml index eb4a35d6c..d73428c8a 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/tactics/paramodulation/saturation.ml @@ -56,7 +56,8 @@ let symbols_ratio = ref (* 0 *) 3;; let symbols_counter = ref 0;; (* non-recursive Knuth-Bendix term ordering by default *) -Utils.compare_terms := Utils.nonrec_kbo;; +Utils.compare_terms := Utils.rpo;; +(* Utils.compare_terms := Utils.nonrec_kbo;; *) (* Utils.compare_terms := Utils.ao;; *) (* statistics... *) @@ -1829,7 +1830,7 @@ let main dbd full term metasenv ugraph = "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty)) (fst theorems))))) in - try + (*try*) let goal = Inference.BasicProof new_meta_goal, [], goal in let equalities = let equalities = equalities @ library_equalities in @@ -1911,7 +1912,7 @@ let main dbd full term metasenv ugraph = (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities in let _ = - try + (*try*) let ty, ug = CicTypeChecker.type_of_aux' newmetasenv context proof ugraph in @@ -1922,10 +1923,10 @@ let main dbd full term metasenv ugraph = (string_of_bool (fst (CicReduction.are_convertible context type_of_goal ty ug))); - with e -> + (*with e -> Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e); Printf.printf "MAXMETA USED: %d\n" !maxmeta; - print_endline (string_of_float (finish -. start)); + print_endline (string_of_float (finish -. start));*) in () @@ -1949,9 +1950,11 @@ let main dbd full term metasenv ugraph = !Indexing.build_newtarget_time; Printf.printf "derived %d clauses, kept %d clauses.\n" !derived_clauses !kept_clauses; +(* with exc -> print_endline ("EXCEPTION: " ^ (Printexc.to_string exc)); raise exc +*) ;; @@ -2157,12 +2160,12 @@ let saturate let init () = ();; -(* UGLY SIDE EFFECT... *) +(* UGLY SIDE EFFECT... if connect_to_auto then ( AutoTactic.paramodulation_tactic := saturate; AutoTactic.term_is_equality := Inference.term_is_equality; );; - +*) let retrieve_and_print dbd term metasenv ugraph = let module C = Cic in @@ -2287,7 +2290,7 @@ let main_demod_equalities dbd term metasenv ugraph = in let env = (metasenv, context, ugraph) in let t1 = Unix.gettimeofday () in - try + (*try*) let goal = Inference.BasicProof new_meta_goal, [], goal in let equalities = let equalities = equalities @ library_equalities in @@ -2353,8 +2356,10 @@ let main_demod_equalities dbd term metasenv ugraph = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities in - let addfun s e = + let addfun s e = EqualitySet.add e s + (* if not (EqualitySet.mem e initial) then EqualitySet.add e s else s + *) in let passive = @@ -2367,13 +2372,15 @@ let main_demod_equalities dbd term metasenv ugraph = EqualitySet.elements (List.fold_left addfun EqualitySet.empty l) in Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n" -(* (String.concat "\n" (List.map (string_of_equality ~env) active)) *) - (String.concat "\n" - (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) + (String.concat "\n" (List.map (string_of_equality ~env) active)) + (* (String.concat "\n" + (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *) (* (String.concat "\n" (List.map (string_of_equality ~env) passive)); *) (String.concat "\n" (List.map (fun e -> CicPp.ppterm (term_of_equality e)) passive)); print_newline (); +(* with e -> debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e))) +*) ;; diff --git a/helm/ocaml/tactics/paramodulation/saturation.mli b/helm/ocaml/tactics/paramodulation/saturation.mli new file mode 100644 index 000000000..259ab5e6c --- /dev/null +++ b/helm/ocaml/tactics/paramodulation/saturation.mli @@ -0,0 +1,49 @@ +(* Copyright (C) 2006, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id$ *) + +val saturate : + HMysql.dbd -> + ?full:bool -> + ?depth:int -> + ?width:int -> + ProofEngineTypes.proof * ProofEngineTypes.goal -> + (UriManager.uri option * Cic.conjecture list * Cic.term * Cic.term) * + 'a list + +val weight_age_ratio : int ref +val weight_age_counter: int ref +val symbols_ratio: int ref +val symbols_counter: int ref +val use_fullred: bool ref +val time_limit: float ref +val maxwidth: int ref +val maxdepth: int ref +val retrieve_and_print: HMysql.dbd -> Cic.term -> Cic.conjecture list -> 'a -> unit +val main_demod_equalities: HMysql.dbd -> + Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit +val main: HMysql.dbd -> + bool -> Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit diff --git a/helm/ocaml/paramodulation/test_indexing.ml b/helm/ocaml/tactics/paramodulation/test_indexing.ml similarity index 100% rename from helm/ocaml/paramodulation/test_indexing.ml rename to helm/ocaml/tactics/paramodulation/test_indexing.ml diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/tactics/paramodulation/utils.ml similarity index 84% rename from helm/ocaml/paramodulation/utils.ml rename to helm/ocaml/tactics/paramodulation/utils.ml index 5eb591c0b..3cafedd54 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/tactics/paramodulation/utils.ml @@ -38,15 +38,155 @@ let print_metasenv metasenv = ;; + + let print_subst ?(prefix="\n") subst = - String.concat prefix - (List.map + String.concat prefix + (List.map (fun (i, (c, t, ty)) -> Printf.sprintf "?%d -> %s : %s" i (CicPp.ppterm t) (CicPp.ppterm ty)) subst) ;; +type comparison = Lt | Le | Eq | Ge | Gt | Incomparable;; + +let string_of_comparison = function + | Lt -> "<" + | Le -> "<=" + | Gt -> ">" + | Ge -> ">=" + | Eq -> "=" + | Incomparable -> "I" + +module OrderedTerm = +struct + type t = Cic.term + + let compare = Pervasives.compare +end + +module TermSet = Set.Make(OrderedTerm);; +module TermMap = Map.Make(OrderedTerm);; + +let symbols_of_term term = + let module C = Cic in + let rec aux map = function + | C.Meta _ -> map + | C.Appl l -> + List.fold_left (fun res t -> (aux res t)) map l + | t -> + let map = + try + let c = TermMap.find t map in + TermMap.add t (c+1) map + with Not_found -> + TermMap.add t 1 map + in + map + in + aux TermMap.empty term +;; + + +let metas_of_term term = + let module C = Cic in + let rec aux = function + | C.Meta _ as t -> TermSet.singleton t + | C.Appl l -> + List.fold_left (fun res t -> TermSet.union res (aux t)) TermSet.empty l + | t -> TermSet.empty (* TODO: maybe add other cases? *) + in + aux term +;; + + +(************************* rpo ********************************) +let number = [ + UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)",3; + UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)",6; + UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)",9; + HelmLibraryObjects.Peano.pred_URI, 12; + HelmLibraryObjects.Peano.plus_URI, 15; + HelmLibraryObjects.Peano.minus_URI, 18; + HelmLibraryObjects.Peano.mult_URI, 21 + ] +;; + +let atomic t = + match t with + Cic.Const _ + | Cic.MutInd _ + | Cic.MutConstruct _ -> true + | _ -> false + +let sig_order t1 t2 = + try + let u1 = CicUtil.uri_of_term t1 in + let u2 = CicUtil.uri_of_term t2 in + let n1 = List.assoc u1 number in + let n2 = List.assoc u2 number in + if n1 < n2 then Lt + else if n1 > n2 then Gt + else + begin + prerr_endline ("t1 = "^(CicPp.ppterm t1)); + prerr_endline ("t2 = "^(CicPp.ppterm t2)); flush; + assert false + end + with + Invalid_argument _ + | Not_found -> Incomparable + +let rec rpo t1 t2 = + let module C = Cic in + match t1,t2 with + C.Meta (_, _), C.Meta (_,_) -> Incomparable + | C.Meta (_,_) as t1,t2 when TermSet.mem t1 (metas_of_term t2) + -> Lt + | t1, (C.Meta (_,_) as t2) when TermSet.mem t2 (metas_of_term t1) + -> Gt + | C.Appl (h1::arg1),C.Appl (h2::arg2) when h1=h2 -> + (match lex arg1 arg2 with + | Lt when (check Gt t2 arg1) -> Lt + | Gt when (check Gt t1 arg2) -> Gt + | _ -> Incomparable ) + | C.Appl (h1::arg1),C.Appl (h2::arg2) -> + (match sig_order h1 h2 with + | Lt when (check Gt t2 arg1) -> Lt + | Gt when (check Gt t1 arg2) -> Gt + | _ -> Incomparable ) + | C.Appl (h1::arg1), t2 when atomic t2 -> + (match sig_order h1 t2 with + | Lt when (check Gt t2 arg1) -> Lt + | Gt -> Gt + | _ -> Incomparable ) + | t1 , C.Appl (h2::arg2) when atomic t1 -> + (match sig_order t1 h2 with + | Lt -> Lt + | Gt when (check Gt t1 arg2) -> Gt + | _ -> Incomparable ) + | C.Appl [] , _ -> assert false + | _ , C.Appl [] -> assert false + | _,_ -> Incomparable + +and lex l1 l2 = + match l1,l2 with + [],[] -> Incomparable + | [],_ -> assert false + | _, [] -> assert false + | a1::l1, a2::l2 when a1 = a2 -> lex l1 l2 + | a1::_, a2::_ -> rpo a1 a2 + +and check o t l = + List.fold_left + (fun b a -> b && (rpo t a = o)) + true l +;; + + +(*********************** fine rpo *****************************) + (* (weight of constants, [(meta, weight_of_meta)]) *) type weight = int * (int * int) list;; @@ -182,17 +322,6 @@ let normalize_weights (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) = @@ -228,33 +357,22 @@ let compare_weights ?(normalize=false) (string_of_bool normalize))); assert false in - let hdiff = h1 - h2 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 diffs < (- hdiff) then Lt - else if diffs = (- hdiff) then Le else Incomparable -(* - 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 *) + if hdiff <= 0 then Lt + else if (- diffs) >= hdiff then Le else Incomparable | (0, _, m) -> - if (- hdiff) < diffs then Gt - else if (- hdiff) = diffs then Ge else Incomparable -(* - 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 *) + if hdiff >= 0 then Gt + else if diffs >= (- hdiff) then Ge else Incomparable | (m, _, n) when m > 0 && n > 0 -> Incomparable - | _ -> assert false + | _ -> assert false + ;; @@ -452,48 +570,6 @@ let names_of_context context = ;; -module OrderedTerm = -struct - type t = Cic.term - - let compare = Pervasives.compare -end - -module TermSet = Set.Make(OrderedTerm);; -module TermMap = Map.Make(OrderedTerm);; - -let symbols_of_term term = - let module C = Cic in - let rec aux map = function - | C.Meta _ -> map - | C.Appl l -> - List.fold_left (fun res t -> (aux res t)) map l - | t -> - let map = - try - let c = TermMap.find t map in - TermMap.add t (c+1) map - with Not_found -> - TermMap.add t 1 map - in - map - in - aux TermMap.empty term -;; - - -let metas_of_term term = - let module C = Cic in - let rec aux = function - | C.Meta _ as t -> TermSet.singleton t - | C.Appl l -> - List.fold_left (fun res t -> TermSet.union res (aux t)) TermSet.empty l - | t -> TermSet.empty (* TODO: maybe add other cases? *) - in - aux term -;; - - let rec lpo t1 t2 = let module C = Cic in match t1, t2 with @@ -559,16 +635,18 @@ let rec lpo t1 t2 = (* settable by the user... *) -let compare_terms = ref nonrec_kbo;; +(* let compare_terms = ref nonrec_kbo;; *) (* let compare_terms = ref ao;; *) +let compare_terms = ref rpo;; -let guarded_simpl context t = +let guarded_simpl context t = t +(* let t' = ProofEngineReduction.simpl context t in let simpl_order = !compare_terms t t' in if simpl_order = Gt then (* prerr_endline ("reduce: "^(CicPp.ppterm t)^(CicPp.ppterm t')); *) t' - else t + else t *) ;; type equality_sign = Negative | Positive;; diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/tactics/paramodulation/utils.mli similarity index 98% rename from helm/ocaml/paramodulation/utils.mli rename to helm/ocaml/tactics/paramodulation/utils.mli index d52483ddb..2b09e59ae 100644 --- a/helm/ocaml/paramodulation/utils.mli +++ b/helm/ocaml/tactics/paramodulation/utils.mli @@ -44,6 +44,8 @@ val compare_weights: ?normalize:bool -> weight -> weight -> comparison val nonrec_kbo: Cic.term -> Cic.term -> comparison +val rpo: 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 diff --git a/helm/ocaml/tactics/tactics.ml b/helm/ocaml/tactics/tactics.ml index 170d6887f..d70df41f5 100644 --- a/helm/ocaml/tactics/tactics.ml +++ b/helm/ocaml/tactics/tactics.ml @@ -38,6 +38,7 @@ let contradiction = NegationTactics.contradiction_tac let cut = PrimitiveTactics.cut_tac let decide_equality = DiscriminationTactics.decide_equality_tac let decompose = EliminationTactics.decompose_tac +let demodulate = Indexing.demodulate_tac let discriminate = DiscriminationTactics.discriminate_tac let elim_intros = PrimitiveTactics.elim_intros_tac let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 25e479b47..c8c225cdd 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -23,6 +23,9 @@ val decompose : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ?user_types:(UriManager.uri * int) list -> dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic +val demodulate : + dbd:HMysql.dbd -> + pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val discriminate : term:Cic.term -> ProofEngineTypes.tactic val elim_intros : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> -- 2.39.2