From 76917216be769918258c90e486bb7c06d81b70b4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 9 Oct 2006 17:48:45 +0000 Subject: [PATCH] applyS now receives the same parameters that auto receives. The parameters are not used yet. --- components/grafite/grafiteAst.ml | 2 +- components/grafite/grafiteAstPp.ml | 5 +++- components/grafite_engine/grafiteEngine.ml | 4 +-- .../grafite_parser/grafiteDisambiguate.ml | 4 +-- components/grafite_parser/grafiteParser.ml | 6 ++-- components/tactics/auto.ml | 2 +- components/tactics/auto.mli | 5 ++-- components/tactics/tactics.mli | 3 +- matita/help/C/matita.xml | 1 + matita/help/C/sec_tactics.xml | 14 +++++---- matita/help/C/sec_terms.xml | 30 +++++++++++++++++++ 11 files changed, 58 insertions(+), 18 deletions(-) diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index e4b2cf24d..8816f2efa 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -46,7 +46,7 @@ type 'lazy_term reduction = type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Absurd of loc * 'term | Apply of loc * 'term - | ApplyS of loc * 'term + | ApplyS of loc * 'term * (string * string) list | Assumption of loc | Auto of loc * (string * string) list | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 5644d33d3..13a4690dd 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -75,7 +75,10 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = function | Absurd (_, term) -> "absurd" ^ term_pp term | Apply (_, term) -> "apply " ^ term_pp term - | ApplyS (_, term) -> "applyS " ^ term_pp term + | ApplyS (_, term, params) -> + "applyS " ^ term_pp term ^ + String.concat " " + (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | Auto (_,params) -> "auto " ^ String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 2d0d691f1..4539029af 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -61,8 +61,8 @@ let tactic_of_ast ast = match ast with | GrafiteAst.Absurd (_, term) -> Tactics.absurd term | GrafiteAst.Apply (_, term) -> Tactics.apply term - | GrafiteAst.ApplyS (_, term) -> - Tactics.applyS ~term ~dbd:(LibraryDb.instance ()) + | GrafiteAst.ApplyS (_, term, params) -> + Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ()) | GrafiteAst.Assumption _ -> Tactics.assumption | GrafiteAst.Auto (_,params) -> AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ()) diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 134a16895..9528d45e1 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -123,9 +123,9 @@ let disambiguate_tactic | GrafiteAst.Apply (loc, term) -> let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Apply (loc, cic) - | GrafiteAst.ApplyS (loc, term) -> + | GrafiteAst.ApplyS (loc, term, params) -> let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.ApplyS (loc, cic) + metasenv,GrafiteAst.ApplyS (loc, cic, params) | GrafiteAst.Assumption loc -> metasenv,GrafiteAst.Assumption loc | GrafiteAst.Auto (loc,params) -> diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 6e108ce04..af185a63e 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -133,8 +133,10 @@ EXTEND GrafiteAst.Absurd (loc, t) | IDENT "apply"; t = tactic_term -> GrafiteAst.Apply (loc, t) - | IDENT "applyS"; t = tactic_term -> - GrafiteAst.ApplyS (loc, t) + | IDENT "applyS"; t = tactic_term ; params = + LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int -> + string_of_int v | v = IDENT -> v ] -> i,v ] -> + GrafiteAst.ApplyS (loc, t, params) | IDENT "assumption" -> GrafiteAst.Assumption loc | IDENT "auto"; params = diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index 1e99c9b64..117978d8c 100644 --- a/components/tactics/auto.ml +++ b/components/tactics/auto.ml @@ -533,7 +533,7 @@ let auto dbd cache context metasenv gl flags = | Fail s,tables,cache,maxm -> None,cache ;; -let applyS_tac ~dbd ~term = +let applyS_tac ~dbd ~term ~params = ProofEngineTypes.mk_tactic (fun status -> try diff --git a/components/tactics/auto.mli b/components/tactics/auto.mli index 5883f0bf2..c9f3b9b09 100644 --- a/components/tactics/auto.mli +++ b/components/tactics/auto.mli @@ -42,5 +42,6 @@ val auto_all_solutions: AutoTypes.flags -> (Cic.substitution * Cic.metasenv) list * AutoCache.cache -val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic - +val applyS_tac: + dbd:HMysql.dbd -> term: Cic.term -> params:(string * string) list -> + ProofEngineTypes.tactic diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index c49303555..7a7d92fdc 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,7 +1,8 @@ (* GENERATED FILE, DO NOT EDIT. STAMP:Thu Sep 28 10:29:58 CEST 2006 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic -val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic +val applyS : + dbd:HMysql.dbd -> term:Cic.term -> params:(string * string) list -> ProofEngineTypes.tactic val assumption : ProofEngineTypes.tactic val auto : params:(string * string) list -> dbd:HMysql.dbd -> ProofEngineTypes.tactic diff --git a/matita/help/C/matita.xml b/matita/help/C/matita.xml index c3ea1da84..bb281ac67 100644 --- a/matita/help/C/matita.xml +++ b/matita/help/C/matita.xml @@ -48,6 +48,7 @@ LCF-tactical"> qstring"> interpretation"> + auto_params"> ]> diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml index 468a27695..ff8d099c0 100644 --- a/matita/help/C/sec_tactics.xml +++ b/matita/help/C/sec_tactics.xml @@ -89,13 +89,13 @@ applyS applyS - applyS t + applyS t auto_params Synopsis: - applyS &sterm; + applyS &sterm; &autoparams; @@ -123,6 +123,8 @@ Then it closes the current sequent by applying t to n implicit arguments (that become new sequents). + The auto_params parameters are passed + directly to auto paramodulation. @@ -176,13 +178,13 @@ auto auto - auto depth=d width=w paramodulation full + auto params Synopsis: - auto [depth=&nat;] [width=&nat;] [paramodulation] [full] + auto &autoparams; @@ -190,10 +192,10 @@ None, but the tactic may fail finding a proof if every proof is in the search space that is pruned away. Pruning is - controlled by d and w. + controlled by the optional params. Moreover, only lemmas whose type signature is a subset of the signature of the current sequent are considered. The signature of - a sequent is ...TODO + a sequent is ...&TODO; diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml index add3ba750..f5ac2b3ec 100644 --- a/matita/help/C/sec_terms.xml +++ b/matita/help/C/sec_terms.xml @@ -687,6 +687,36 @@ + + + auto-params + &TODO; + + reduction-kind + + + + &autoparams; + ::= + depth=&nat; + &TODO; + + + + | + width=&nat; + &TODO; + + + + | + &TODO; + &TODO; + + + +
+ -- 2.39.2