From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 1 Jun 2006 15:32:34 +0000 (+0000)
Subject: implemented tinycals:
X-Git-Tag: 0.4.95@7852~1363
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cbf47ddef11207628a9838973a192566e1e60ba7;p=helm.git

implemented tinycals:
- 1,2,3: ...
- *:
---

diff --git a/components/binaries/tptp2grafite/main.ml b/components/binaries/tptp2grafite/main.ml
index 9b47e4a58..b7efd6820 100644
--- a/components/binaries/tptp2grafite/main.ml
+++ b/components/binaries/tptp2grafite/main.ml
@@ -196,7 +196,8 @@ let convert_ast statements context = function
                 (fun _ -> 
                   [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
                     GA.Exists floc),Some (GA.Branch floc)));
-                   GA.Executable(floc,GA.Tactical(floc, GA.Pos (floc,2),None))])
+                   GA.Executable(floc,GA.Tactical(floc,
+                    GA.Pos (floc,[2]),None))])
                 fv)) 
            else [])@
             [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index 20635bd64..c00eb8404 100644
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -140,7 +140,8 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactical =
   | Semicolon of loc
   | Branch of loc
   | Shift of loc
-  | Pos of loc * int
+  | Pos of loc * int list
+  | Wildcard of loc
   | Merge of loc
   | Focus of loc * int list
   | Unfocus of loc
diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index ab27e853e..43e2117cd 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -232,7 +232,8 @@ let rec pp_tactical ~term_pp ~lazy_term_pp =
   | Semicolon _ -> ";"
   | Branch _ -> "["
   | Shift _ -> "|"
-  | Pos (_, i) -> sprintf "%d:" i
+  | Pos (_, i) -> sprintf "%s:" (String.concat "," (List.map string_of_int i))
+  | Wildcard _ -> "*:"
   | Merge _ -> "]"
   | Focus (_, goals) ->
       sprintf "focus %s" (String.concat " " (List.map string_of_int goals))
diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 8b83bcff0..ff173bc37 100644
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -480,15 +480,16 @@ let eval_tactical ~disambiguate_tactic status tac =
         MatitaTacticals.solve_tactics
          ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
 
-    | GrafiteAst.Skip loc -> MatitaTacticals.skip
-    | GrafiteAst.Dot loc -> MatitaTacticals.dot
-    | GrafiteAst.Semicolon loc -> MatitaTacticals.semicolon
-    | GrafiteAst.Branch loc -> MatitaTacticals.branch
-    | GrafiteAst.Shift loc -> MatitaTacticals.shift
-    | GrafiteAst.Pos (loc, i) -> MatitaTacticals.pos i
-    | GrafiteAst.Merge loc -> MatitaTacticals.merge
-    | GrafiteAst.Focus (loc, goals) -> MatitaTacticals.focus goals
-    | GrafiteAst.Unfocus loc -> MatitaTacticals.unfocus
+    | GrafiteAst.Skip _loc -> MatitaTacticals.skip
+    | GrafiteAst.Dot _loc -> MatitaTacticals.dot
+    | GrafiteAst.Semicolon _loc -> MatitaTacticals.semicolon
+    | GrafiteAst.Branch _loc -> MatitaTacticals.branch
+    | GrafiteAst.Shift _loc -> MatitaTacticals.shift
+    | GrafiteAst.Pos (_loc, i) -> MatitaTacticals.pos i
+    | GrafiteAst.Merge _loc -> MatitaTacticals.merge
+    | GrafiteAst.Focus (_loc, goals) -> MatitaTacticals.focus goals
+    | GrafiteAst.Unfocus _loc -> MatitaTacticals.unfocus
+    | GrafiteAst.Wildcard _loc -> MatitaTacticals.wildcard
   in
   let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in
   let status =  (* is proof completed? *)
diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 1b06b81c9..d4c89e0e3 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -266,7 +266,8 @@ EXTEND
     [
       [ SYMBOL "[" -> GrafiteAst.Branch loc
       | SYMBOL "|" -> GrafiteAst.Shift loc
-      | i = int; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
+      | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
+      | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
       | SYMBOL "]" -> GrafiteAst.Merge loc
       | SYMBOL ";" -> GrafiteAst.Semicolon loc
       | SYMBOL "." -> GrafiteAst.Dot loc
diff --git a/components/tactics/continuationals.ml b/components/tactics/continuationals.ml
index 4c00fd704..7ea357e89 100644
--- a/components/tactics/continuationals.ml
+++ b/components/tactics/continuationals.ml
@@ -205,7 +205,8 @@ sig
 
     | Branch
     | Shift
-    | Pos of int
+    | Pos of int list
+    | Wildcard
     | Merge
 
     | Focus of goal list
@@ -233,7 +234,8 @@ struct
     | Semicolon
     | Branch
     | Shift
-    | Pos of int
+    | Pos of int list
+    | Wildcard
     | Merge
     | Focus of goal list
     | Unfocus
@@ -245,7 +247,8 @@ struct
     | Semicolon -> "Semicolon"
     | Branch -> "Branch"
     | Shift -> "Shift"
-    | Pos i -> "Pos " ^ string_of_int i
+    | Pos i -> "Pos " ^ (String.concat "," (List.map string_of_int i))
+    | Wildcard -> "Wildcard"
     | Merge -> "Merge"
     | Focus gs ->
         sprintf "Focus [%s]" (String.concat "; " (List.map string_of_int gs))
@@ -327,18 +330,24 @@ struct
                 (([ loc ], t @+ filter_open g, [],`BranchTag)
                 :: (loc_tl, t', k', tag) :: s))
       | Shift, _ -> fail (lazy "can't shift goals here")
-      | Pos i, ([ loc ], [], [],`BranchTag) :: (g', t', k', tag) :: s
+      | Pos i_s, ([ loc ], [], [],`BranchTag) :: (g', t', k', tag) :: s
         when is_fresh loc ->
-          let loc_i, g' = extract_pos i g' in
+          let l_js = List.filter (fun (i, _) -> List.mem i i_s) g' in
           new_stack
-            (([ loc_i ], [], [],`BranchTag)
-             :: ([ loc ] @+ g', t', k', tag) :: s)
-      | Pos i, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
-          let loc_i, g' = extract_pos i g' in
+            ((l_js, [], [],`BranchTag)
+             :: ([ loc ] @+ g' @- l_js, t', k', tag) :: s)
+      | Pos i_s, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
+          let l_js = List.filter (fun (i, _) -> List.mem i i_s) g' in
           new_stack
-            (([ loc_i ], [], [],`BranchTag)
-             :: (g', t' @+ filter_open g, k', tag) :: s)
+            ((l_js, [], [],`BranchTag)
+             :: (g' @- l_js, t' @+ filter_open g, k', tag) :: s)
       | Pos _, _ -> fail (lazy "can't use relative positioning here")
+      | Wildcard, (g, t, k, `BranchTag) :: (g', t', k', tag) :: s
+        when g = [] || is_fresh (List.hd g) ->
+          new_stack
+            ((g', [], [], `BranchTag)
+             :: ([], t' @+ filter_open g @+ k, k', tag) :: s)
+      | Wildcard, _ -> fail (lazy "can't use wildcard here")
       | Merge, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
           new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
       | Merge, _ -> fail (lazy "can't merge goals here")
diff --git a/components/tactics/continuationals.mli b/components/tactics/continuationals.mli
index d40202d4b..6383b97bf 100644
--- a/components/tactics/continuationals.mli
+++ b/components/tactics/continuationals.mli
@@ -109,8 +109,10 @@ sig
 
     | Branch
     | Shift
-    | Pos of int
+    | Pos of int list
+    | Wildcard
     | Merge
+
     | Focus of goal list
     | Unfocus
 
diff --git a/components/tactics/tacticals.ml b/components/tactics/tacticals.ml
index a674fe313..ceb2d2de8 100644
--- a/components/tactics/tacticals.ml
+++ b/components/tactics/tacticals.ml
@@ -104,7 +104,8 @@ sig
   val semicolon: tactic
   val branch: tactic
   val shift: tactic
-  val pos: int -> tactic
+  val pos: int list -> tactic
+  val wildcard: tactic
   val merge: tactic
   val focus: int list -> tactic
   val unfocus: tactic
@@ -295,6 +296,7 @@ struct
   let branch = cont_proxy C.Branch
   let shift = cont_proxy C.Shift
   let pos i = cont_proxy (C.Pos i)
+  let wildcard =  cont_proxy C.Wildcard
   let merge = cont_proxy C.Merge
   let focus goals = cont_proxy (C.Focus goals)
   let unfocus = cont_proxy C.Unfocus
diff --git a/components/tactics/tacticals.mli b/components/tactics/tacticals.mli
index 88fafc1f8..e8d245cd1 100644
--- a/components/tactics/tacticals.mli
+++ b/components/tactics/tacticals.mli
@@ -72,7 +72,8 @@ sig
   val semicolon: tactic
   val branch: tactic
   val shift: tactic
-  val pos: int -> tactic
+  val pos: int list -> tactic
+  val wildcard: tactic
   val merge: tactic
   val focus: int list -> tactic
   val unfocus: tactic