From 0d254219f4870d603ab3ecf5b0013a9a81e14314 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 6 Jul 2005 12:01:48 +0000 Subject: [PATCH] * Bug fixed: "tac." was parsed as Seq [tac] * Pretty printing of Seq and other tacticals was utterly wrong. --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 8 ++++---- helm/ocaml/cic_transformations/tacticAstPp.ml | 11 +++++------ 2 files changed, 9 insertions(+), 10 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 9ce70062f..fd79cdab1 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -477,8 +477,8 @@ EXTEND ]; tactical: [ "sequence" LEFTA - [ tacticals = LIST1 NEXT SEP SYMBOL ";" -> - TacticAst.Seq (loc, tacticals) + [ tactical = NEXT -> tactical + | tacticals = LIST1 NEXT SEP SYMBOL ";" -> TacticAst.Seq (loc, tacticals) ] | "then" NONA [ tac = tactical; @@ -486,9 +486,9 @@ EXTEND (TacticAst.Then (loc, tac, tacs)) ] | "loops" RIGHTA - [ [ IDENT "do" ]; count = int; tac = tactical -> + [ IDENT "do"; count = int; tac = tactical -> TacticAst.Do (loc, count, tac) - | [ IDENT "repeat" ]; tac = tactical -> + | IDENT "repeat"; tac = tactical -> TacticAst.Repeat (loc, tac) ] | "simple" NONA diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 327595365..2c31f3bfc 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -30,7 +30,6 @@ open TacticAst let tactical_terminator = "." let tactic_terminator = tactical_terminator let command_terminator = tactical_terminator -let tactical_separator = ";" let pp_term_ast term = CicAstPp.pp_term term let pp_term_cic term = CicPp.ppterm term @@ -245,14 +244,14 @@ let rec pp_tactical = function | Tactic (_, tac) -> pp_tactic tac | Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac) | Repeat (_, tac) -> "repeat " ^ pp_tactical tac - | Seq (_, tacs) -> pp_tacticals tacs + | Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs | Then (_, tac, tacs) -> - sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs) - | Tries (_, tacs) -> sprintf "tries [%s]" (pp_tacticals tacs) + sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals ~sep:" | " tacs) + | Tries (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs) | Try (_, tac) -> "try " ^ pp_tactical tac -and pp_tacticals tacs = - String.concat (tactical_separator ^ " ") (List.map pp_tactical tacs) +and pp_tacticals ~sep tacs = + String.concat sep (List.map pp_tactical tacs) let pp_tactical tac = pp_tactical tac ^ tactical_terminator let pp_tactic tac = pp_tactic tac ^ tactic_terminator -- 2.39.2