meta.expr_lens

# A lens for zooming into nested expr applications #

A "lens" for looking into the subterms of an expression, tracking where we've been, so that when we "zoom out" after making a change we know exactly which order of congr_funs and congr_args we need to make things work.

This file defines the expr_lens inductive type, defines basic operations this type, and defines a useful map-like function expr.app_map on exprs which maps over applications.

This file is for non-tactics.

## Tags #

expr, expr_lens, congr, environment, meta, metaprogramming, tactic

### Declarations about expr_lens#

meta inductive expr_lens  :
Type

You're supposed to think of an expr_lens as a big set of nested applications with a single hole which needs to be filled, either in a function spot or argument spot. expr_lens.fill can fill this hole and turn your lens back into a real expr.

inductive expr_lens.dir  :
Type

Inductive type with two constructors F and A, that represent the function-part f and arg-part a of an application f a. They specify the directions in which an expr_lens should zoom into an expr.

This type is used in the development of rewriting tactics such as nth_rewrite and rewrite_search.

@[instance]
@[instance]

String representation of dir.

Equations
@[instance]
Equations
meta def expr_lens.fill  :

Fill the function or argument hole in this lens with the given expr.

meta def expr_lens.zoom  :

Zoom into e : expr given the context of an expr_lens, popping out an expr and a new zoomed expr_lens, if this is possible (e has to be an application).

meta def expr_lens.to_dirs  :

Convert an expr_lens into a list of instructions needed to build it; repeatedly inspecting a function or its argument a finite number of times.

meta def expr_lens.mk_congr_arg_using_dsimp (G W : expr) (u : list name) :

Sometimes mk_congr_arg fails, when the function is 'superficially dependent'. Try to dsimp the function first before building the congr_arg expression.

meta def expr_lens.congr  :

Turn an e : expr_lens and a proof that a = b into a series of congr_arg or congr_fun applications showing that the expressions obtained from e.fill a and e.fill b are equal.

Pretty print a lens.

meta def expr.app_map {α : Type u_1} (F : expr_lensexprtactic (list α)) (e : expr) :

app_map F e maps a function F which understands expr_lenses over the given e : expr in the natural way; that is, make holes in e everywhere where that is possible (generating expr_lenses in the process), and at each stage call the function F passing both the expr_lens generated and the expr which was removed to make the hole.

At each stage F returns a list of some type, and app_map collects these lists together and returns a concatenation of them all.