From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 15 Jun 2006 09:38:42 +0000 (+0000)
Subject: Apply-Silvie tactic added!
X-Git-Tag: make_still_working~7179
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=52a418c32f7d60439f4aaba580d4ed3ba8439602;p=helm.git

Apply-Silvie tactic added!
---

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index c00eb8404..ffd35c703 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/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/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 9038b3b60..9e1dffdcd 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/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/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index ff173bc37..e4f70117a 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/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/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 3d1899835..0e96aaf2d 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/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/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 5bf73503b..cbaed19b0 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/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";