From: Andrea Asperti Date: Thu, 15 Jun 2006 09:38:42 +0000 (+0000) Subject: Apply-Silvie tactic added! X-Git-Tag: 0.4.95@7852~1313 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a0ff15484a45e64185e593af9ea95ad51a95879d;p=helm.git Apply-Silvie tactic added! --- diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index c00eb8404..ffd35c703 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -47,6 +47,7 @@ type 'lazy_term reduction = type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Absurd of loc * 'term | Apply of loc * 'term + | ApplyS of loc * 'term | Assumption of loc | Auto of loc * int option * int option * string option * string option (* depth, width, paramodulation, full *) (* ALB *) diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 9038b3b60..9e1dffdcd 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -72,6 +72,7 @@ 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 | Auto (_,_,_,Some kind,_) -> "auto " ^ kind | Auto _ -> "auto" | Assumption _ -> "assumption" diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index ff173bc37..e4f70117a 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -60,6 +60,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.Assumption _ -> Tactics.assumption | GrafiteAst.Auto (_,depth,width,paramodulation,full) -> AutoTactic.auto_tac ?depth ?width ?paramodulation ?full diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 3d1899835..0e96aaf2d 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -124,6 +124,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) -> + let metasenv,cic = disambiguate_term context metasenv term in + metasenv,GrafiteAst.ApplyS (loc, cic) | GrafiteAst.Assumption loc -> metasenv,GrafiteAst.Assumption loc | GrafiteAst.Auto (loc,depth,width,paramodulation,full) -> diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 5bf73503b..cbaed19b0 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -128,6 +128,8 @@ EXTEND GrafiteAst.Absurd (loc, t) | IDENT "apply"; t = tactic_term -> GrafiteAst.Apply (loc, t) + | IDENT "applyS"; t = tactic_term -> + GrafiteAst.ApplyS (loc, t) | IDENT "assumption" -> GrafiteAst.Assumption loc | IDENT "auto";