<commit_before>/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
prelude
import init.meta.tactic init.meta.attribute init.meta.constructor_tactic
import init.meta.relation_tactics init.meta.occurrences
import init.data.option.instances

open tactic

meta constant simp_lemmas : Type
meta constant simp_lemmas.mk : simp_lemmas
meta constant simp_lemmas.join : simp_lemmas → simp_lemmas → simp_lemmas
meta constant simp_lemmas.erase : simp_lemmas → list name → simp_lemmas
meta constant simp_lemmas.mk_default : tactic simp_lemmas
meta constant simp_lemmas.add : simp_lemmas → expr → tactic simp_lemmas
meta constant simp_lemmas.add_simp : simp_lemmas → name → tactic simp_lemmas
meta constant simp_lemmas.add_congr : simp_lemmas → name → tactic simp_lemmas

meta def simp_lemmas.append (s : simp_lemmas) (hs : list expr) : tactic simp_lemmas :=
hs.mfoldl simp_lemmas.add s

/-- `simp_lemmas.rewrite_core m s prove R e` apply a simplification lemma from 's'

   - 'prove' is used to discharge proof obligations.
   - 'R'     is the equivalence relation being used (e.g., 'eq', 'iff')
   - 'e'     is the expression to be "simplified"

   Result (new_e, pr) is the new expression 'new_e' and a proof (pr : e R new_e) -/
meta constant simp_lemmas.rewrite_core : transparency → simp_lemmas → tactic unit → name → expr → tactic (expr × expr)

meta def simp_lemmas.rewrite : simp_lemmas → tactic unit → name → expr → tactic (expr × expr) :=
simp_lemmas.rewrite_core reducible

/-- `simp_lemmas.drewrite s e` tries to rewrite 'e' using only refl lemmas in 's' -/
meta constant simp_lemmas.drewrite_core : transparency → simp_lemmas → expr → tactic expr

meta def simp_lemmas.drewrite : simp_lemmas → expr → tactic expr :=
simp_lemmas.drewrite_core reducible

meta constant is_valid_simp_lemma_cnst : name → tactic bool
meta constant is_valid_simp_lemma : expr → tactic bool

def default_max_steps := 10000000

meta constant simp_lemmas.pp : simp_lemmas → tactic format

namespace tactic
/-- `get_eqn_lemmas_for deps d` returns the automatically generated equational lemmas for definition d.
   If deps is tt, then lemmas for automatically generated auxiliary declarations used to define d are also included. -/
meta constant get_eqn_lemmas_for : bool → name → tactic (list name)

structure dsimp_config :=
(md                        := reducible)
(max_steps : nat           := default_max_steps)
(canonize_instances : bool := tt)
(single_pass : bool        := ff)
(fail_if_unchaged          := tt)
(eta                       := tt)
(memoize                   := tt)
end tactic

/-- (Definitional) Simplify the given expression using *only* reflexivity equality lemmas from the given set of lemmas.
   The resulting expression is definitionally equal to the input. -/
meta constant simp_lemmas.dsimplify (s : simp_lemmas) (e : expr) (cfg : tactic.dsimp_config := {}) : tactic expr

namespace tactic
/- Remark: the configuration parameters `cfg.md` and `cfg.eta` are ignored by this tactic. -/
meta constant dsimplify_core
  /- The user state type. -/
  {α : Type}
  /- Initial user data -/
  (a : α)
  /- (pre a e) is invoked before visiting the children of subterm 'e',
     if it succeeds the result (new_a, new_e, flag) where
       - 'new_a' is the new value for the user data
       - 'new_e' is a new expression that must be definitionally equal to 'e',
       - 'flag'  if tt 'new_e' children should be visited, and 'post' invoked. -/
  (pre             : α → expr → tactic (α × expr × bool))
  /- (post a e) is invoked after visiting the children of subterm 'e',
     The output is similar to (pre a e), but the 'flag' indicates whether
     the new expression should be revisited or not. -/
  (post            : α → expr → tactic (α × expr × bool))
  (e               : expr)
  (cfg             : dsimp_config := {})
  : tactic (α × expr)

meta def dsimplify
  (pre             : expr → tactic (expr × bool))
  (post            : expr → tactic (expr × bool))
  : expr → tactic expr :=
λ e, do (a, new_e) ← dsimplify_core ()
                       (λ u e, do r ← pre e, return (u, r))
                       (λ u e, do r ← post e, return (u, r)) e,
        return new_e

/- Remark: we use transparency.instances by default to make sure that we
   can unfold projections of type classes. Example:

          (@has_add.add nat nat.has_add a b)
-/

/-- If `e` is a projection application, try to unfold it, otherwise fail. -/
meta constant unfold_projection (e : expr) (md := transparency.instances) : tactic expr

meta constant dunfold_expr (e : expr) (md := transparency.instances) : tactic expr

structure dunfold_config extends dsimp_config :=
(md := transparency.instances)

meta constant dunfold_core (cs : list name) (e : expr) (cfg : dunfold_config := {}) : tactic expr

meta def dunfold (cs : list name) (cfg : dunfold_config := {}) : tactic unit :=
do t ← target, dunfold_core cs t cfg >>= unsafe_change

meta def revert_and_transform (transform : expr → tactic expr) (h : expr) : tactic unit :=
do num_reverted : ℕ ← revert h,
   t ← target,
   match t with
   | expr.pi n bi d b  :=
        do h_simp ← transform d,
           unsafe_change $ expr.pi n bi h_simp b
   | expr.elet n g e f :=
        do h_simp ← transform g,
           unsafe_change $ expr.elet n h_simp e f
   | _ := fail "reverting hypothesis created neither a pi nor an elet expr (unreachable?)"
   end,
   intron num_reverted

meta def dunfold_at (cs : list name) (h : expr) (cfg : dunfold_config := {}) : tactic unit :=
revert_and_transform (λ e, dunfold_core cs e cfg) h

structure delta_config :=
(max_steps       := default_max_steps)
(visit_instances := tt)

private meta def is_delta_target (e : expr) (cs : list name) : bool :=
cs.any (λ c,
  if e.is_app_of c then tt   /- Exact match -/
  else let f := e.get_app_fn in
       /- f is an auxiliary constant generated when compiling c -/
       f.is_constant && f.const_name.is_internal && (f.const_name.get_prefix = c))

/-- Delta reduce the given constant names -/
meta def delta_expr (cs : list name) (e : expr) (cfg : delta_config) : tactic expr :=
let unfold (u : unit) (e : expr) : tactic (unit × expr × bool) := do
  guard (is_delta_target e cs),
  (expr.const f_name f_lvls) ← return e.get_app_fn,
  env   ← get_env,
  decl  ← env.get f_name,
  new_f ← decl.instantiate_value_univ_params f_lvls,
  new_e ← head_beta (expr.mk_app new_f e.get_app_args),
  return (u, new_e, tt)
in do (c, new_e) ← dsimplify_core () (λ c e, failed) unfold e {max_steps := cfg.max_steps, canonize_instances := cfg.visit_instances},
      return new_e

meta def delta (cs : list name) : tactic unit :=
do t ← target, delta_expr cs t {} >>= unsafe_change

meta def delta_at (cs : list name) : expr → tactic unit :=
revert_and_transform (λ e, delta_expr cs e {})

meta def unfold_projections_core (e : expr) (md := transparency.instances) (max_steps : nat := default_max_steps) : tactic expr :=
let unfold (changed : bool) (e : expr) : tactic (bool × expr × bool) := do
  new_e ← unfold_projection e md,
  return (tt, new_e, tt)
in do (tt, new_e) ← dsimplify_core ff (λ c e, failed) unfold e {max_steps := max_steps, md := md} | fail "no projections to unfold",
      return new_e

meta def unfold_projections (md := transparency.instances) (max_steps : nat := default_max_steps) : tactic unit :=
do t ← target, unfold_projections_core t md max_steps >>= unsafe_change

meta def unfold_projections_at (h : expr) (md := transparency.instances) (max_steps : nat := default_max_steps) : tactic unit :=
revert_and_transform (λ e, unfold_projections_core e md max_steps) h

structure simp_config :=
(max_steps : nat           := default_max_steps)
(contextual : bool         := ff)
(lift_eq : bool            := tt)
(canonize_instances : bool := tt)
(canonize_proofs : bool    := ff)
(use_axioms : bool         := tt)
(zeta : bool               := tt)
(beta : bool               := tt)
(eta  : bool               := tt)
(proj : bool               := tt) -- reduce projections
(single_pass : bool        := ff)
(fail_if_unchaged          := tt)<commit_msg>refactor(library/init/meta/simp_tactic): `default_max_steps` should not be in the top level<commit_after>/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
prelude
import init.meta.tactic init.meta.attribute init.meta.constructor_tactic
import init.meta.relation_tactics init.meta.occurrences
import init.data.option.instances

open tactic

def simp.default_max_steps := 10000000

meta constant simp_lemmas : Type
meta constant simp_lemmas.mk : simp_lemmas
meta constant simp_lemmas.join : simp_lemmas → simp_lemmas → simp_lemmas
meta constant simp_lemmas.erase : simp_lemmas → list name → simp_lemmas
meta constant simp_lemmas.mk_default : tactic simp_lemmas
meta constant simp_lemmas.add : simp_lemmas → expr → tactic simp_lemmas
meta constant simp_lemmas.add_simp : simp_lemmas → name → tactic simp_lemmas
meta constant simp_lemmas.add_congr : simp_lemmas → name → tactic simp_lemmas

meta def simp_lemmas.append (s : simp_lemmas) (hs : list expr) : tactic simp_lemmas :=
hs.mfoldl simp_lemmas.add s

/-- `simp_lemmas.rewrite_core m s prove R e` apply a simplification lemma from 's'

   - 'prove' is used to discharge proof obligations.
   - 'R'     is the equivalence relation being used (e.g., 'eq', 'iff')
   - 'e'     is the expression to be "simplified"

   Result (new_e, pr) is the new expression 'new_e' and a proof (pr : e R new_e) -/
meta constant simp_lemmas.rewrite_core : transparency → simp_lemmas → tactic unit → name → expr → tactic (expr × expr)

meta def simp_lemmas.rewrite : simp_lemmas → tactic unit → name → expr → tactic (expr × expr) :=
simp_lemmas.rewrite_core reducible

/-- `simp_lemmas.drewrite s e` tries to rewrite 'e' using only refl lemmas in 's' -/
meta constant simp_lemmas.drewrite_core : transparency → simp_lemmas → expr → tactic expr

meta def simp_lemmas.drewrite : simp_lemmas → expr → tactic expr :=
simp_lemmas.drewrite_core reducible

meta constant is_valid_simp_lemma_cnst : name → tactic bool
meta constant is_valid_simp_lemma : expr → tactic bool

meta constant simp_lemmas.pp : simp_lemmas → tactic format

namespace tactic
/-- `get_eqn_lemmas_for deps d` returns the automatically generated equational lemmas for definition d.
   If deps is tt, then lemmas for automatically generated auxiliary declarations used to define d are also included. -/
meta constant get_eqn_lemmas_for : bool → name → tactic (list name)

structure dsimp_config :=
(md                        := reducible)
(max_steps : nat           := simp.default_max_steps)
(canonize_instances : bool := tt)
(single_pass : bool        := ff)
(fail_if_unchaged          := tt)
(eta                       := tt)
(memoize                   := tt)
end tactic

/-- (Definitional) Simplify the given expression using *only* reflexivity equality lemmas from the given set of lemmas.
   The resulting expression is definitionally equal to the input. -/
meta constant simp_lemmas.dsimplify (s : simp_lemmas) (e : expr) (cfg : tactic.dsimp_config := {}) : tactic expr

namespace tactic
/- Remark: the configuration parameters `cfg.md` and `cfg.eta` are ignored by this tactic. -/
meta constant dsimplify_core
  /- The user state type. -/
  {α : Type}
  /- Initial user data -/
  (a : α)
  /- (pre a e) is invoked before visiting the children of subterm 'e',
     if it succeeds the result (new_a, new_e, flag) where
       - 'new_a' is the new value for the user data
       - 'new_e' is a new expression that must be definitionally equal to 'e',
       - 'flag'  if tt 'new_e' children should be visited, and 'post' invoked. -/
  (pre             : α → expr → tactic (α × expr × bool))
  /- (post a e) is invoked after visiting the children of subterm 'e',
     The output is similar to (pre a e), but the 'flag' indicates whether
     the new expression should be revisited or not. -/
  (post            : α → expr → tactic (α × expr × bool))
  (e               : expr)
  (cfg             : dsimp_config := {})
  : tactic (α × expr)

meta def dsimplify
  (pre             : expr → tactic (expr × bool))
  (post            : expr → tactic (expr × bool))
  : expr → tactic expr :=
λ e, do (a, new_e) ← dsimplify_core ()
                       (λ u e, do r ← pre e, return (u, r))
                       (λ u e, do r ← post e, return (u, r)) e,
        return new_e

/- Remark: we use transparency.instances by default to make sure that we
   can unfold projections of type classes. Example:

          (@has_add.add nat nat.has_add a b)
-/

/-- If `e` is a projection application, try to unfold it, otherwise fail. -/
meta constant unfold_projection (e : expr) (md := transparency.instances) : tactic expr

meta constant dunfold_expr (e : expr) (md := transparency.instances) : tactic expr

structure dunfold_config extends dsimp_config :=
(md := transparency.instances)

meta constant dunfold_core (cs : list name) (e : expr) (cfg : dunfold_config := {}) : tactic expr

meta def dunfold (cs : list name) (cfg : dunfold_config := {}) : tactic unit :=
do t ← target, dunfold_core cs t cfg >>= unsafe_change

meta def revert_and_transform (transform : expr → tactic expr) (h : expr) : tactic unit :=
do num_reverted : ℕ ← revert h,
   t ← target,
   match t with
   | expr.pi n bi d b  :=
        do h_simp ← transform d,
           unsafe_change $ expr.pi n bi h_simp b
   | expr.elet n g e f :=
        do h_simp ← transform g,
           unsafe_change $ expr.elet n h_simp e f
   | _ := fail "reverting hypothesis created neither a pi nor an elet expr (unreachable?)"
   end,
   intron num_reverted

meta def dunfold_at (cs : list name) (h : expr) (cfg : dunfold_config := {}) : tactic unit :=
revert_and_transform (λ e, dunfold_core cs e cfg) h

structure delta_config :=
(max_steps       := simp.default_max_steps)
(visit_instances := tt)

private meta def is_delta_target (e : expr) (cs : list name) : bool :=
cs.any (λ c,
  if e.is_app_of c then tt   /- Exact match -/
  else let f := e.get_app_fn in
       /- f is an auxiliary constant generated when compiling c -/
       f.is_constant && f.const_name.is_internal && (f.const_name.get_prefix = c))

/-- Delta reduce the given constant names -/
meta def delta_expr (cs : list name) (e : expr) (cfg : delta_config) : tactic expr :=
let unfold (u : unit) (e : expr) : tactic (unit × expr × bool) := do
  guard (is_delta_target e cs),
  (expr.const f_name f_lvls) ← return e.get_app_fn,
  env   ← get_env,
  decl  ← env.get f_name,
  new_f ← decl.instantiate_value_univ_params f_lvls,
  new_e ← head_beta (expr.mk_app new_f e.get_app_args),
  return (u, new_e, tt)
in do (c, new_e) ← dsimplify_core () (λ c e, failed) unfold e {max_steps := cfg.max_steps, canonize_instances := cfg.visit_instances},
      return new_e

meta def delta (cs : list name) : tactic unit :=
do t ← target, delta_expr cs t {} >>= unsafe_change

meta def delta_at (cs : list name) : expr → tactic unit :=
revert_and_transform (λ e, delta_expr cs e {})

meta def unfold_projections_core (e : expr) (md := transparency.instances) (max_steps : nat := simp.default_max_steps) : tactic expr :=
let unfold (changed : bool) (e : expr) : tactic (bool × expr × bool) := do
  new_e ← unfold_projection e md,
  return (tt, new_e, tt)
in do (tt, new_e) ← dsimplify_core ff (λ c e, failed) unfold e {max_steps := max_steps, md := md} | fail "no projections to unfold",
      return new_e

meta def unfold_projections (md := transparency.instances) (max_steps : nat := simp.default_max_steps) : tactic unit :=
do t ← target, unfold_projections_core t md max_steps >>= unsafe_change

meta def unfold_projections_at (h : expr) (md := transparency.instances) (max_steps : nat := simp.default_max_steps) : tactic unit :=
revert_and_transform (λ e, unfold_projections_core e md max_steps) h

structure simp_config :=
(max_steps : nat           := simp.default_max_steps)
(contextual : bool         := ff)
(lift_eq : bool            := tt)
(canonize_instances : bool := tt)
(canonize_proofs : bool    := ff)
(use_axioms : bool         := tt)
(zeta : bool               := tt)
(beta : bool               := tt)
(eta  : bool               := tt)
(proj : bool               := tt) -- reduce projections
(single_pass : bool        := ff)
(fail_if_unchaged          := tt)
{'fraction_non_alphanumeric': 0.10094196292920085, 'fraction_numerical': 0.001701610452749924, 'mean_word_length': 3.14822283841694, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 17, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 2, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7640102', 'n_tokens_mistral': 5644, 'n_tokens_neox': 5362, 'n_words': 2045}