implemented tinycals:

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

diff --git a/helm/software/components/binaries/tptp2grafite/main.ml b/helm/software/components/binaries/tptp2grafite/main.ml
index 9b47e4a58782862f5a447cc4217ab1982832257c..b7efd6820bcf464d8a0fa88750b6621336ec7ecd 100644 (file)
--- a/helm/software/components/binaries/tptp2grafite/main.ml
+++ b/helm/software/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/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 20635bd648accbf1e53f4d8717eebe0e2d61c9c8..c00eb8404d2f8ca0a459bb28fbca4e0a328f02ac 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/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/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index ab27e853e300843a9605b8a05a1d8bb1795f69cb..43e2117cdb13470cb435776cd22c1420f6c68819 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/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/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 8b83bcff0fcf3569af351757165b11b88cd3dfbc..ff173bc37aa1d717ed3b7e32f69d26043b5a9b42 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/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/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 1b06b81c97fd64b26b4429956c25e9c573c7bdd5..d4c89e0e33f6b93b06f14f73981c0bc238012748 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/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/helm/software/components/tactics/continuationals.ml b/helm/software/components/tactics/continuationals.ml
index 4c00fd704f19709dc67b9abb4a098dde46831ddd..7ea357e89679694087ce106e890559b4e028d686 100644 (file)
--- a/helm/software/components/tactics/continuationals.ml
+++ b/helm/software/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/helm/software/components/tactics/continuationals.mli b/helm/software/components/tactics/continuationals.mli
index d40202d4b37e2a92f1ba878a0581fdbf50501bcb..6383b97bfc7a4c7dc69ba069be8e4e82bbca5e03 100644 (file)
--- a/helm/software/components/tactics/continuationals.mli
+++ b/helm/software/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/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index a674fe31344a1f840971afececcc9b5a0f19fa61..ceb2d2de88cb28fc8a7554ee87c1167e5c846af8 100644 (file)
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/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/helm/software/components/tactics/tacticals.mli b/helm/software/components/tactics/tacticals.mli
index 88fafc1f8bf5e91be97802e7fcfea51bc44c5d75..e8d245cd1bf1635a37c199f62c0caa8aa2437a1d 100644 (file)
--- a/helm/software/components/tactics/tacticals.mli
+++ b/helm/software/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