From 9680f6df42892b7b586fb2932617fa99703036bf Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 15 Nov 2004 09:04:40 +0000 Subject: [PATCH] changed reduction tactics ast --- .../cic_disambiguation/cicTextualParser2.ml | 21 +++++++++++++++---- helm/ocaml/cic_transformations/tacticAst.ml | 12 +++++++++-- .../cic_transformations/tacticAst2Box.ml | 6 +++--- helm/ocaml/cic_transformations/tacticAstPp.ml | 13 ++++++++++-- 4 files changed, 41 insertions(+), 11 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 775f13f7d..fddf27e99 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -240,9 +240,9 @@ EXTEND [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] ]; reduction_kind: [ - [ "reduce" -> `Reduce - | "simpl" -> `Simpl - | "whd" -> `Whd ] + [ [ IDENT "reduce" | IDENT "Reduce" ] -> `Reduce + | [ IDENT "simplify" | IDENT "Simplify" ] -> `Simpl + | [ IDENT "whd" | IDENT "Whd" ] -> `Whd ] ]; tactic: [ [ [ IDENT "absurd" | IDENT "Absurd" ]; t = tactic_term -> @@ -296,7 +296,20 @@ EXTEND | [ "let" | "Let" ]; t = tactic_term; "in"; where = IDENT -> return_tactic loc (TacticAst.LetIn (t, where)) - (* TODO Reduce *) + | kind = reduction_kind; + pat = OPT [ + "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] -> + pat + ]; + terms = LIST0 term SEP SYMBOL "," -> + let tac = + (match (pat, terms) with + | None, [] -> TacticAst.Reduce (kind, None) + | None, terms -> TacticAst.Reduce (kind, Some (terms, `Goal)) + | Some pat, [] -> TacticAst.Reduce (kind, Some ([], pat)) + | Some pat, terms -> TacticAst.Reduce (kind, Some (terms, pat))) + in + return_tactic loc tac | [ IDENT "reflexivity" | IDENT "Reflexivity" ] -> return_tactic loc TacticAst.Reflexivity | [ IDENT "replace" | IDENT "Replace" ]; diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 7be8293da..112d87b70 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -25,7 +25,10 @@ type direction = [ `Left | `Right ] type reduction_kind = [ `Reduce | `Simpl | `Whd ] -type 'term pattern = Pattern of 'term +(* type 'term pattern = Pattern of 'term *) + + (* everywhere includes goal and hypotheses *) +type 'term pattern = [ `Goal | `Everywhere ] (* when an 'ident option is None, the default is to apply the tactic to the current goal *) @@ -56,7 +59,12 @@ type ('term, 'ident) tactic = | Left | LetIn of 'term * 'ident (* | Named_intros of 'ident list (* joined with Intros above *) *) - | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *) +(* | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *) *) + | Reduce of reduction_kind * ('term list * 'term pattern) option + (* kind, (what, where) + * if second argument is None, reduction is applied to the current goal, + * otherwise to each occurrence of terms given in list occuring in term + * pattern *) | Reflexivity | Replace of 'term * 'term (* what, with what *) | Replace_pattern of 'term pattern * 'term diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index 5afb38ca8..80e3effce 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -78,7 +78,7 @@ let rec count_tactic current_size tac = | Left -> current_size + 4 | LetIn (term, ident) -> countterm (current_size + 5 + String.length ident) term - | Reduce (_, _, _) -> assert false (* TODO *) + | Reduce (_, _) -> assert false (* TODO *) | Reflexivity -> current_size + 11 | Replace (t1, t2) -> let size1 = countterm (current_size + 14) t1 in (* replace, with *) @@ -105,7 +105,7 @@ let rec small_tactic2box tac = let string_of_kind = function | `Reduce -> "reduce" - | `Simpl -> "simpl" + | `Simpl -> "simplify" | `Whd -> "whd" let dummy_tbl = Hashtbl.create 0 @@ -214,7 +214,7 @@ and big_tactic2box = function Box.smallskip; Box.Text([],"=")]); Box.indent (ast2astBox term)]) - | Reduce (_, _, _) -> assert false (* TODO *) + | Reduce (_, _) -> assert false (* TODO *) | Reflexivity -> Box.Text([],"reflexivity") | Replace (t1, t2) -> Box.V([], diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 76f1bbd56..d0e87b094 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -33,7 +33,7 @@ let pp_idents idents = "[" ^ String.concat "; " idents ^ "]" let pp_reduction_kind = function | `Reduce -> "reduce" - | `Simpl -> "simpl" + | `Simpl -> "simplify" | `Whd -> "whd" let rec pp_tactic = function @@ -68,7 +68,16 @@ let rec pp_tactic = function (match idents with [] -> "" | idents -> " " ^ pp_idents idents) | Left -> "left" | LetIn (term, ident) -> sprintf "let %s in %s" (pp_term term) ident - | Reduce (_, _, _) -> assert false (* TODO *) + | Reduce (kind, None) + | Reduce (kind, Some ([], `Goal)) -> pp_reduction_kind kind + | Reduce (kind, Some ([], `Everywhere)) -> + sprintf "%s in hyp" (pp_reduction_kind kind) + | Reduce (kind, Some (terms, `Goal)) -> + sprintf "%s %s" (pp_reduction_kind kind) + (String.concat ", " (List.map pp_term terms)) + | Reduce (kind, Some (terms, `Everywhere)) -> + sprintf "%s in hyp %s" (pp_reduction_kind kind) + (String.concat ", " (List.map pp_term terms)) | Reflexivity -> "reflexivity" | Replace (t1, t2) -> sprintf "replace %s with %s" (pp_term t1) (pp_term t2) | Replace_pattern (_, _) -> assert false (* TODO *) -- 2.39.2