From 44d337f8d772c6895d310a1b1d62770c3355fe03 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 30 Jun 2005 14:46:31 +0000 Subject: [PATCH] Signature and concrete syntax of fold fixed. --- .../cic_disambiguation/cicTextualParser2.ml | 4 ++-- helm/ocaml/cic_transformations/tacticAst.ml | 2 +- helm/ocaml/cic_transformations/tacticAstPp.ml | 5 +++-- helm/ocaml/tactics/fourierR.ml | 16 ++++++---------- helm/ocaml/tactics/reductionTactics.ml | 2 +- helm/ocaml/tactics/reductionTactics.mli | 2 +- helm/ocaml/tactics/tactics.mli | 1 + 7 files changed, 15 insertions(+), 17 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 728ff94a0..e59e13987 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -398,8 +398,8 @@ EXTEND | IDENT "exists" -> TacticAst.Exists loc | IDENT "fail" -> TacticAst.Fail loc - | IDENT "fold"; kind = reduction_kind; p = pattern_spec -> - TacticAst.Fold (loc, kind, p) + | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec -> + TacticAst.Fold (loc, kind, t, p) | IDENT "fourier" -> TacticAst.Fourier loc | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 -> diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 3f6e74346..c4f2a29ac 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -50,7 +50,7 @@ type ('term, 'ident) tactic = | Exact of loc * 'term | Exists of loc | Fail of loc - | Fold of loc * reduction_kind * ('term, 'ident) pattern + | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern | Fourier of loc | FwdSimpl of loc * string * 'ident list | Generalize of loc * ('term, 'ident) pattern * 'ident option diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 67b5733d2..86c7185ec 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -82,8 +82,9 @@ let rec pp_tactic = function | ElimType (_, term) -> "elim type " ^ pp_term_ast term | Exact (_, term) -> "exact " ^ pp_term_ast term | Exists _ -> "exists" - | Fold (_, kind, pattern) -> - sprintf "fold %s %s" (pp_reduction_kind kind) (pp_pattern pattern) + | Fold (_, kind, term, pattern) -> + sprintf "fold %s %s %s" (pp_reduction_kind kind) + (pp_term_ast term) (pp_pattern pattern) | FwdSimpl (_, hyp, idents) -> sprintf "fwd %s%s" hyp (match idents with [] -> "" | idents -> " " ^ pp_idents idents) diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index 2fbba97ad..3079b327b 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -693,16 +693,12 @@ let tac_zero_infeq_false gl (n,d) = (Tacticals.then_ ~start: (ReductionTactics.fold_tac ~reduction:CicReduction.whd - ~pattern: - (ProofEngineTypes.conclusion_pattern - (Some - (Cic.Appl - [_Rle ; _R0 ; - Cic.Appl - [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]] - ] - ))) - ) + ~pattern:(ProofEngineTypes.conclusion_pattern None) + ~term: + (Cic.Appl + [_Rle ; _R0 ; + Cic.Appl + [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]])) ~continuation: (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index ae99ecb33..18db1a302 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -83,7 +83,7 @@ let whd_tac ~pattern = let normalize_tac ~pattern = mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern );; -let fold_tac ~reduction ~pattern = +let fold_tac ~reduction ~term ~pattern = (* let fold_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) ~term (proof,goal) = diff --git a/helm/ocaml/tactics/reductionTactics.mli b/helm/ocaml/tactics/reductionTactics.mli index 20e45827d..00d3e5890 100644 --- a/helm/ocaml/tactics/reductionTactics.mli +++ b/helm/ocaml/tactics/reductionTactics.mli @@ -30,5 +30,5 @@ val whd_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val normalize_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val fold_tac: - reduction:(Cic.context -> Cic.term -> Cic.term) -> + reduction:(Cic.context -> Cic.term -> Cic.term) -> term:Cic.term -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 187dc2be3..c155d67d3 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -33,6 +33,7 @@ val exists : ProofEngineTypes.tactic val fail : ProofEngineTypes.tactic val fold : reduction:(Cic.context -> Cic.term -> Cic.term) -> + term:Cic.term -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val fourier : ProofEngineTypes.tactic val fwd_simpl : -- 2.39.2