From: Alberto Griggio Date: Fri, 22 Jul 2005 17:53:47 +0000 (+0000) Subject: added optional "paramodulation" parameter to auto to turn on paramodulation X-Git-Tag: V_0_7_2~97 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ee69e02cdf70e8fed61c3bf1c8f165b4798ad9fb;p=helm.git added optional "paramodulation" parameter to auto to turn on paramodulation --- diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index d0223a80b..d4f9c3fac 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -31,7 +31,7 @@ open MatitaMisc (* ALB to link paramodulation... *) -let _ = Saturation.init () +let _ = Paramodulation.Saturation.init () (** {2 Initialization} *) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 767182bc1..fe9ea94d6 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -59,8 +59,9 @@ let tactic_of_ast = function | GrafiteAst.Absurd (_, term) -> Tactics.absurd term | GrafiteAst.Apply (_, term) -> Tactics.apply term | GrafiteAst.Assumption _ -> Tactics.assumption - | GrafiteAst.Auto (_,depth,width) -> - AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) () + | GrafiteAst.Auto (_,depth,width,paramodulation) -> (* ALB *) + AutoTactic.auto_tac ?depth ?width ?paramodulation + ~dbd:(MatitaDb.instance ()) () | GrafiteAst.Change (_, pattern, with_what) -> Tactics.change ~pattern with_what | GrafiteAst.Clear (_,id) -> Tactics.clear id @@ -178,7 +179,7 @@ let disambiguate_tactic status = function let status, cic = disambiguate_term status term in status, GrafiteAst.Absurd (loc, cic) | GrafiteAst.Assumption loc -> status, GrafiteAst.Assumption loc - | GrafiteAst.Auto (loc,depth,width) -> status, GrafiteAst.Auto (loc,depth,width) + | GrafiteAst.Auto (loc,depth,width,paramodulation) -> status, GrafiteAst.Auto (loc,depth,width,paramodulation) (* ALB *) | GrafiteAst.Change (loc, pattern, with_what) -> let status, with_what = disambiguate_term status with_what in let status, pattern = disambiguate_pattern status pattern in diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 108b36bfb..d21241a8d 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -524,7 +524,7 @@ class gui () = (tac_w_term (A.Transitivity (loc, hole))); connect_button tbar#assumptionButton (tac (A.Assumption loc)); connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole))); - connect_button tbar#autoButton (tac (A.Auto (loc,None,None))); + connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None))); (* ALB *) MatitaGtkMisc.toggle_widget_visibility ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget) ~check:self#main#tacticsBarMenuItem; diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml index b27e115f4..40526e74d 100644 --- a/helm/matita/matitac.ml +++ b/helm/matita/matitac.ml @@ -25,7 +25,7 @@ (* ALB to link paramodulation... *) -let _ = Saturation.init () +let _ = Paramodulation.Saturation.init () let _ = MatitacLib.main `COMPILER diff --git a/helm/matita/tests/paramodulation.ma b/helm/matita/tests/paramodulation.ma index af8d59be6..b56c0da27 100644 --- a/helm/matita/tests/paramodulation.ma +++ b/helm/matita/tests/paramodulation.ma @@ -22,10 +22,10 @@ alias symbol "times" (instance 0) = "natural times". theorem para1: \forall n,m,n1,m1:nat. n=m \to n1 = m1 \to (n + n1) = (m + m1). -intros. auto. +intros. auto paramodulation. qed. theorem para2: \forall n:nat. n + n = 2 * n. -intros. auto. -qed. \ No newline at end of file +intros. auto paramodulation. +qed.