02c8c2f9e1
This PR implements first-class support for nondependent let expressions in the elaborator; recall that a let expression `let x : t := v; b` is called *nondependent* if `fun x : t => b` typechecks, and the notation for a nondependent let expression is `have x := v; b`. Previously we encoded `have` using the `letFun` function, but now we make use of the `nondep` flag in the `Expr.letE` constructor for the encoding. This has been given full support throughout the metaprogramming interface and the elaborator. Key changes to the metaprogramming interface: - Local context `ldecl`s with `nondep := true` are generally treated as `cdecl`s. This is because in the body of a `have` expression the variable is opaque. Functions like `LocalDecl.isLet` by default return `false` for nondependent `ldecl`s. In the rare case where it is needed, they take an additional optional `allowNondep : Bool` flag (defaults to `false`) if the variable is being processed in a context where the value is relevant. - Functions such as `mkLetFVars` by default generalize nondependent let variables and create lambda expressions for them. The `generalizeNondepLet` flag (default true) can be set to false if `have` expressions should be produced instead. **Breaking change:** Uses of `letLambdaTelescope`/`mkLetFVars` need to use `generalizeNondepLet := false`. See the next item. - There are now some mapping functions to make telescoping operations more convenient. See `mapLetTelescope` and `mapLambdaLetTelescope`. There is also `mapLetDecl` as a counterpart to `withLetDecl` for creating `let`/`have` expressions. - Important note about the `generalizeNondepLet` flag: it should only be used for variables in a local context that the metaprogram "owns". Since nondependent let variables are treated as constants in most cases, the `value` field might refer to variables that do not exist, if for example those variables were cleared or reverted. Using `mapLetDecl` is always fine. - The simplifier will cache its let dependence calculations in the nondep field of let expressions. - The `intro` tactic still produces *dependent* local variables. Given that the simplifier will transform lets into haves, it would be surprising if that would prevent `intro` from creating a local variable whose value cannot be used. Note that nondependence of lets is not checked by the kernel. To external checker authors: If the elaborator gets the nondep flag wrong, we consider this to be an elaborator error. Feel free to typecheck `letE n t v b true` as if it were `app (lam n t b default) v` and please report issues. This PR follows up from #8751, which made sure the nondep flag was preserved in the C++ interface.
106 lines
4 KiB
Text
106 lines
4 KiB
Text
import Lean
|
|
/-!
|
|
# Tests of `Expr.letE (nondep := true) ..`
|
|
|
|
This file exercises the Lean/C++ interface to make sure that the `nondep` field
|
|
is successfully part of the data model.
|
|
|
|
It also tests the metaprogramming API.
|
|
-/
|
|
|
|
open Lean
|
|
|
|
/-!
|
|
Equality checking. Both `Expr.eqv` and `Expr.equal` are implemented in C++.
|
|
-/
|
|
/-- info: true -/
|
|
#guard_msgs in #eval Expr.eqv (mkLet `n default default default) (mkLet `n default default default)
|
|
/-- info: false -/
|
|
#guard_msgs in #eval Expr.eqv (mkLet `n default default default) (mkHave `n default default default)
|
|
/-- info: false -/
|
|
#guard_msgs in #eval Expr.eqv (mkHave `n default default default) (mkLet `n default default default)
|
|
/-- info: true -/
|
|
#guard_msgs in #eval Expr.eqv (mkHave `n default default default) (mkHave `n default default default)
|
|
/-- info: true -/
|
|
#guard_msgs in #eval Expr.equal (mkLet `n default default default) (mkLet `n default default default)
|
|
/-- info: false -/
|
|
#guard_msgs in #eval Expr.equal (mkLet `n default default default) (mkHave `n default default default)
|
|
/-- info: false -/
|
|
#guard_msgs in #eval Expr.equal (mkHave `n default default default) (mkLet `n default default default)
|
|
/-- info: true -/
|
|
#guard_msgs in #eval Expr.equal (mkHave `n default default default) (mkHave `n default default default)
|
|
|
|
/-!
|
|
Inequality checking. This too is implemented in C++.
|
|
-/
|
|
/-- info: false -/
|
|
#guard_msgs in #eval Expr.lt (mkLet `n default default default) (mkLet `n default default default)
|
|
/-- info: true -/
|
|
#guard_msgs in #eval Expr.lt (mkLet `n default default default) (mkHave `n default default default)
|
|
/-- info: false -/
|
|
#guard_msgs in #eval Expr.lt (mkHave `n default default default) (mkLet `n default default default)
|
|
/-- info: false -/
|
|
#guard_msgs in #eval Expr.lt (mkHave `n default default default) (mkHave `n default default default)
|
|
|
|
/-!
|
|
Testing toString, which is implemented in C++.
|
|
-/
|
|
/-- info: "let n : _inhabitedExprDummy := _inhabitedExprDummy; _inhabitedExprDummy" -/
|
|
#guard_msgs in #eval toString (mkLet `n default default default)
|
|
/-- info: "have n : _inhabitedExprDummy := _inhabitedExprDummy; _inhabitedExprDummy" -/
|
|
#guard_msgs in #eval toString (mkHave `n default default default)
|
|
|
|
/-!
|
|
Testing the Lean pretty printer.
|
|
-/
|
|
elab "eval_expr% " t:term : term => do
|
|
let e ← Elab.Term.elabTermEnsuringType t (mkConst ``Expr)
|
|
unsafe Meta.evalExpr Expr (mkConst ``Expr) e
|
|
/--
|
|
info: let n := Nat.zero;
|
|
n : Nat
|
|
-/
|
|
#guard_msgs in #check eval_expr% (mkLet `n (mkConst ``Nat) (mkConst ``Nat.zero) (.bvar 0))
|
|
/--
|
|
info: have n := Nat.zero;
|
|
n : Nat
|
|
-/
|
|
#guard_msgs in #check eval_expr% (mkHave `n (mkConst ``Nat) (mkConst ``Nat.zero) (.bvar 0))
|
|
|
|
/-!
|
|
Testing `Expr.replace`, which is implemented in C++.
|
|
The `nondep` flag was previously cleared.
|
|
-/
|
|
/-- info: Lean.Expr.letE `n (Lean.Expr.bvar 1) (Lean.Expr.bvar 1) (Lean.Expr.bvar 1) true -/
|
|
#guard_msgs in #eval Expr.replace (fun e => if let .bvar i := e then some (.bvar (i + 1)) else none) (mkHave `n (.bvar 0) (.bvar 0) (.bvar 0))
|
|
|
|
/-!
|
|
Testing `instantiateMvars`, which is implemented in C++.
|
|
The `nondep` flag was previously cleared.
|
|
-/
|
|
/--
|
|
info: Lean.Expr.letE `n (Lean.Expr.const `Nat []) (Lean.Expr.const `Nat.zero []) (Lean.Expr.const `Unit []) true
|
|
-/
|
|
#guard_msgs in #eval show MetaM Expr from do
|
|
let m ← Meta.mkFreshExprMVar none
|
|
m.mvarId!.assign (mkConst ``Unit)
|
|
Lean.instantiateMVars (Lean.mkLet `n (mkConst ``Nat) (mkConst ``Nat.zero) m true)
|
|
|
|
namespace TestLambdaLetTelescope
|
|
/-!
|
|
Check that `lambdaLetTelescope` consumes `haves`. Also checks that `preserveNondepLet := false` turns `have`s into `let`s.
|
|
-/
|
|
def c : Nat → Nat → Bool := fun x => have y := 1; fun z => x == y + z
|
|
/--
|
|
info: #[false, true, false]
|
|
#[false, false, false]
|
|
-/
|
|
#guard_msgs in
|
|
open Lean Meta in
|
|
run_meta do
|
|
let decl ← getConstInfo ``c
|
|
lambdaLetTelescope decl.value! fun xs _ => do
|
|
IO.println <| ← xs.mapM fun x => return (← x.fvarId!.getDecl).isNondep
|
|
lambdaLetTelescope decl.value! (preserveNondepLet := false) fun xs _ => do
|
|
IO.println <| ← xs.mapM fun x => return (← x.fvarId!.getDecl).isNondep
|
|
end TestLambdaLetTelescope
|