From: Alberto Griggio Date: Fri, 22 Jul 2005 17:29:00 +0000 (+0000) Subject: added optional "paramodulation" parameter to auto to turn on paramodulation X-Git-Tag: V_0_7_2~98 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d43002dfc61afac676ea14bc6a1418e5ec0e3e9c;p=helm.git added optional "paramodulation" parameter to auto to turn on paramodulation --- diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml index f15417fc8..11fef69a1 100644 --- a/helm/ocaml/cic_notation/grafiteAst.ml +++ b/helm/ocaml/cic_notation/grafiteAst.ml @@ -38,7 +38,7 @@ type ('term, 'ident) tactic = | Absurd of loc * 'term | Apply of loc * 'term | Assumption of loc - | Auto of loc * int option * int option (* depth, width *) + | Auto of loc * int option * int option * string option (* depth, width, paramodulation ALB *) | Change of loc * ('term,'ident) pattern * 'term | Clear of loc * 'ident | ClearBody of loc * 'ident diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml index cceeaf10d..056e595e7 100644 --- a/helm/ocaml/cic_notation/grafiteParser.ml +++ b/helm/ocaml/cic_notation/grafiteParser.ml @@ -107,8 +107,9 @@ EXTEND GrafiteAst.Assumption loc | IDENT "auto"; depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; - width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ] -> - GrafiteAst.Auto (loc,depth,width) + width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ]; + paramodulation = OPT [ IDENT "paramodulation" ] -> (* ALB *) + GrafiteAst.Auto (loc,depth,width,paramodulation) | IDENT "clear"; id = IDENT -> GrafiteAst.Clear (loc,id) | IDENT "clearbody"; id = IDENT -> diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 48fbc4aa2..3f4d4226f 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -38,7 +38,7 @@ type ('term, 'ident) tactic = | Absurd of loc * 'term | Apply of loc * 'term | Assumption of loc - | Auto of loc * int option * int option (* depth, width *) + | Auto of loc * int option * int option * string option (* depth, width, paramodulation ALB *) | Change of loc * ('term,'ident) pattern * 'term | Clear of loc * 'ident | ClearBody of loc * 'ident diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index 72609b118..85c5c54be 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -308,7 +308,7 @@ let term_is_equality = ref (fun term -> debug_print "term_is_equality E` DUMMY!!!!"; false);; -let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) () = +let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd:Mysql.dbd) () = let auto_tac dbd (proof, goal) = let normal_auto () = let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in @@ -331,16 +331,19 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) () = | _ -> assert false in let paramodulation_ok = - let _, metasenv, _, _ = proof in - let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in - !term_is_equality meta_goal + match paramodulation with + | None -> false + | Some _ -> + let _, metasenv, _, _ = proof in + let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in + !term_is_equality meta_goal in if paramodulation_ok then ( debug_print "USO PARAMODULATION..."; - try +(* try *) !paramodulation_tactic dbd (proof, goal) - with e -> - normal_auto () +(* with ProofEngineTypes.Fail _ -> *) +(* normal_auto () *) ) else normal_auto () in diff --git a/helm/ocaml/tactics/autoTactic.mli b/helm/ocaml/tactics/autoTactic.mli index c91e92e3f..d9061c1ef 100644 --- a/helm/ocaml/tactics/autoTactic.mli +++ b/helm/ocaml/tactics/autoTactic.mli @@ -25,8 +25,9 @@ *) val auto_tac: - ?depth:int -> ?width:int -> dbd:Mysql.dbd -> unit -> - ProofEngineTypes.tactic + ?depth:int -> ?width:int -> ?paramodulation:string -> + dbd:Mysql.dbd -> unit -> + ProofEngineTypes.tactic val paramodulation_tactic: (Mysql.dbd -> ProofEngineTypes.status ->