feat(widget): pretty printing restricted quantifiers

src/tactic/interactive_expr.lean

@@ -55,6 +55,8 @@ meta def sf.repr : sf → format
 meta instance : has_to_format sf := ⟨sf.repr⟩
 meta instance : has_to_string sf := ⟨λ s, s.repr.to_string⟩
 meta instance : has_repr sf := ⟨λ s, s.repr.to_string⟩
+meta instance : has_coe string sf := ⟨sf.of_string⟩
+meta instance : has_append sf := ⟨sf.compose⟩
 
 /-- Constructs an `sf` from an `eformat` by forgetting grouping, nesting, etc. -/
 meta def sf.of_eformat : eformat → sf
@@ -65,6 +67,80 @@ meta def sf.of_eformat : eformat → sf
 | (of_format f) := sf.of_string $ format.to_string f
 | (compose x y) := sf.compose (sf.of_eformat x) (sf.of_eformat y)
 
+/-- `subtract x y` is some `z` when `∃ z, x = y ++ z` [fixme] this probably already exists. -/
+def subtract {α} [decidable_eq α]: (list α) → (list α) → option (list α)
+| a [] := some a -- [] ++ a = a
+| [] _ := none   -- (h::t) ++ _ ≠ []
+-- if t₂ ++ z = t₁ then (h₁ :: t₁) ++ z = (h₁ :: t₂)
+| (h₁ :: t₁) (h₂ :: t₂) := if h₁ = h₂ then subtract t₁ t₂ else none
+
+/-- Get the subexpression and sf object at the given address, if any.
+The address must point to a `sf.tag_expr` boundary. -/
+meta def sf.follow : expr.address → sf → option (expr × sf)
+| [] s := none
+| l (sf.tag_expr ea e  m) := do
+  a ← subtract l ea,
+  if a = [] then pure (e,m) else
+  sf.follow a m
+| l (sf.block _ a) := sf.follow l a
+| l (sf.highlight _ a) := sf.follow l a
+| l (sf.of_string _) := none
+| l (sf.compose a b) := sf.follow l a <|> sf.follow l b
+
+/-- Run `f` on each of the immediate child substrings of the given string. -/
+meta def sf.traverse {m} [applicative m] (f : sf → m sf) : sf → m sf
+| (sf.tag_expr ea e m) := pure (sf.tag_expr ea e) <*> f m
+| (sf.block x a) := pure (sf.block x) <*> f a
+| (sf.highlight x a) := pure (sf.highlight x) <*> f a
+| (sf.compose a b) := pure (sf.compose) <*> f a <*> f b
+| (sf.of_string s) := pure $ sf.of_string s
+
+/-- Run `f` on each child. If it fails then stop traversing and keep it the same.-/
+meta def sf.replace {m} [monad m] [alternative m] (f : sf → m sf) : sf → m sf
+| x := (f x >>= sf.traverse sf.replace) <|> pure x
+
+/-- The test for whether the proposition is a valid target for restricted quantifier collapsing.
+Eg (@has_mem.mem _ _ _ _) -/
+meta def sf.collapse_restricted_quantifiers_pred : expr → tactic bool
+| `(@gt _ _ %%(expr.var 0) _) := pure tt
+| `(@has_lt.lt _ _ %%(expr.var 0) _) := pure tt
+| `(@has_le.le _ _ %%(expr.var 0) _) := pure tt
+| `(@ge _ _ %%(expr.var 0) _) := pure tt
+| `(@has_mem.mem _ _ _ %%(expr.var 0) _) := pure tt
+-- [fixme] add to this list! So many predicates. Maybe just include all of them.
+| _ := pure ff
+
+open expr.coord
+
+/-- If the given sf has the form `∀ (x : α), P x → Q`
+and `P x` obeys `collapse_restricted_quantifiers_pred`
+then replace it with `∀ (P x), Q`, mapping the addresses properly
+so interactive rendering still works. -/
+meta def sf.collapse_restricted_quantifiers_core : sf → tactic sf
+| s@(sf.tag_expr addr e@(expr.pi x xbi xy (expr.pi p pbi py b)) a) := (do
+  should_collapse ← sf.collapse_restricted_quantifiers_pred py,
+  if ¬ should_collapse then pure s else do
+  a1 ← pure $ [pi_body, pi_var_type],
+  a2 ← pure $ [pi_body, pi_body],
+  (e1, s1) ← sf.follow a1 a,
+  (e2, s2) ← sf.follow a2 a,
+  pure (sf.tag_expr addr e $ "∀ (" ++ (sf.tag_expr (addr ++ a1) e1 s1) ++ "), " ++ (sf.tag_expr (addr ++ a2) e2 s2))
+  ) <|> pure s
+| s@(sf.tag_expr addr e a) := (do
+  `(Exists %%pred) ← pure e,
+  expr.lam _ _ α pred ← pure pred,
+  `(Exists %%pred) ← pure pred,
+  expr.lam _ _ py pred ← pure pred,
+  should_collapse ← sf.collapse_restricted_quantifiers_pred py,
+  if ¬ should_collapse then pure s else do
+  a1 ← pure $ [app_arg, lam_var_type], -- [hack] There is a bug in the addresing code. Second binder has the address of the first binder!
+  a2 ← pure $ [app_arg, lam_body, app_arg, lam_body],
+  (e1, s1) ← sf.follow a1 a,
+  (e2, s2) ← sf.follow a2 a,
+  pure (sf.tag_expr addr e $ "∃ (" ++ (sf.tag_expr (addr ++ a1) e1 s1) ++ "), " ++ (sf.tag_expr (addr ++ a2) e2 s2))
+  ) <|> pure s
+| x := pure x
+
 /-- Flattens an `sf`, i.e. merges adjacent `of_string` constructors. -/
 meta def sf.flatten : sf → sf
 | (sf.tag_expr ea e m) := (sf.tag_expr ea e $ sf.flatten m)
@@ -240,6 +316,7 @@ $ tc.mk_simple
     let m := m.elim_part_apps,
     let m := m.flatten,
     let m := m.tag_expr [] e, -- [hack] in pp.cpp I forgot to add an expr-boundary for the root expression.
+    m ← sf.replace sf.collapse_restricted_quantifiers_core m,
     v ← view tooltip_comp (prod.snd <$> ca) (prod.snd <$> sa) ⟨e, []⟩ m,
     pure $
     [ h "span" [