Add set_set_comp lemma and simp configuration

Leanses/Lens.lean

@@ -312,6 +312,11 @@ open Lean Meta PrettyPrinter Delaborator SubExpr Core in
               = @set _ _ _ _ $appliedLens (@set _ _ _ _ g v (@view _ _ $appliedLens s)) s := by
             simp [view, set, Functor.map, lens', lens, Id.run, Const.get, Composable2.comp, Composable4.comp4
                  , $fieldNameIdent:ident])
+      let set_set_comp_lemma ←
+        `(@[aesop norm (rule_sets := [lens])] theorem $(freshName "_comp_set_set") $names:ident* :
+            ∀ α s (v v': α) (g : Lens' _ α), @set _ _ _ _ (@Composable4.comp4 Lens _ _ _ _ _ α α $appliedLens g) v' (@set _ _ _ _ (@Composable4.comp4 Lens _ _ _ _ _ α α $appliedLens g) v s)
+                      = @set _ _ _ _ (@Composable4.comp4 Lens _ _ _ _ _ α α $appliedLens g) v' s := by
+            simp [view, set, Functor.map, lens', lens, Id.run, Const.get, Composable2.comp, Composable4.comp4, $fieldNameIdent:ident])
       let view_set_comp_lemma ←
         `(@[aesop norm (rule_sets := [lens])] theorem $(freshName "_view_set_comp") $names:ident* :
             ∀ x y v s (f: Lens' _ x) (g: Lens' _ y),
@@ -358,6 +363,9 @@ open Lean Meta PrettyPrinter Delaborator SubExpr Core in
       elabCommand <| ← `(addlensrule $(freshName "_view_constr"):ident)
       elabCommand <| comp_view_lemma
       elabCommand <| ← `(addlensrule $(freshName "_comp_view"):ident)
+      -- trace[debug] "{set_set_comp_lemma}"
+      -- elabCommand <| set_set_comp_lemma
+      -- elabCommand <| ← `(addlensrule $(freshName "_comp_set_set"):ident)
       --elabCommand <| comp_set_lemma
       --elabCommand <| view_set_comp_lemma
       elabCommand <| view_set_comp2_lemma

Leanses/Tactic.lean

@@ -6,8 +6,16 @@ import Leanses.Options
 
 namespace Leanses
 
+/-- Optional configuration option for tactics -/
+syntax lens_config := atomic(" (" &"lens_config") " := " withoutPosition(term) ")"
+
+structure Config where
+  defaultHints : Bool := false
+
+declare_config_elab elabSimpLensConfig Config
+
 open Lean.Parser.Tactic in
-syntax (name := simpLens) "simp_lens" (config)? (discharger)? 
+syntax (name := simpLens) "simp_lens" (lens_config)? (config)? (discharger)? 
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
 
 open Lean.Parser.Tactic in
@@ -30,6 +38,14 @@ def getSimpTheorems : MetaM SimpTheorems := do
     s ← s.addConst name
   return s
 
+open Lean Meta Simp Core in
+def getAllSimpTheorems : MetaM SimpTheorems := do
+  let rlist := lens_ext.getState (← getEnv)
+  let mut s : SimpTheorems ← Lean.Meta.getSimpTheorems
+  for name in rlist do
+    s ← s.addConst name
+  return s
+
 open Lean Meta Simp Core in
 def getUnfoldTheorems : MetaM SimpTheorems := do
   let rlist := lens_ext_unfold.getState (← getEnv)
@@ -43,11 +59,14 @@ open Lean.Elab.Tactic in
 def evalSimpLens : Tactic := fun stx => withMainContext do
   match stx with 
   | Lean.Syntax.node si st _ =>
-    let nstx_arr := Array.mkArray6 stx[0] stx[1] stx[2] Lean.Syntax.missing stx[3] stx[4]
+    let nstx_arr := Array.mkArray6 stx[0] stx[2] stx[3] Lean.Syntax.missing stx[4] stx[5]
     let nstx := Lean.Syntax.node si st nstx_arr
-    let { ctx, simprocs, dischargeWrapper } ← mkSimpContext nstx (simpTheorems := pure (← getSimpTheorems)) (eraseLocal := false)
+    let config ← elabSimpLensConfig stx[1]
+    let { ctx, simprocs, dischargeWrapper } ← mkSimpContext nstx 
+      (simpTheorems := pure (← (if config.defaultHints then getAllSimpTheorems else getSimpTheorems))) 
+      (eraseLocal := false)
     let usedSimps ← dischargeWrapper.with fun discharge? =>
-      simpLocation ctx simprocs discharge? (expandOptLocation stx[4])
+      simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
     if tactic.simp.trace.get (← Lean.getOptions) then
         traceSimpCall stx usedSimps
   | _ => panic! "Wrong simp_lens syntax"