From 1b3f24947f19050f3947397e50a8d5ed3b61b71b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 1 Jun 2006 15:32:34 +0000 Subject: [PATCH] implemented tinycals: - 1,2,3: ... - *: --- .../components/binaries/tptp2grafite/main.ml | 3 +- .../software/components/grafite/grafiteAst.ml | 3 +- .../components/grafite/grafiteAstPp.ml | 3 +- .../grafite_engine/grafiteEngine.ml | 19 ++++++------ .../grafite_parser/grafiteParser.ml | 3 +- .../components/tactics/continuationals.ml | 31 ++++++++++++------- .../components/tactics/continuationals.mli | 4 ++- helm/software/components/tactics/tacticals.ml | 4 ++- .../software/components/tactics/tacticals.mli | 3 +- 9 files changed, 46 insertions(+), 27 deletions(-) diff --git a/helm/software/components/binaries/tptp2grafite/main.ml b/helm/software/components/binaries/tptp2grafite/main.ml index 9b47e4a58..b7efd6820 100644 --- 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 20635bd64..c00eb8404 100644 --- 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 ab27e853e..43e2117cd 100644 --- 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 8b83bcff0..ff173bc37 100644 --- 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 1b06b81c9..d4c89e0e3 100644 --- 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 4c00fd704..7ea357e89 100644 --- 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 d40202d4b..6383b97bf 100644 --- 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 a674fe313..ceb2d2de8 100644 --- 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 88fafc1f8..e8d245cd1 100644 --- 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 -- 2.39.2