|
|
/- Copied from `https://github.com/leanprover-community/mathlib4/tree/thorimur/refine_struct-via-StructInst` -/
|
|
|
|
|
|
/-
|
|
|
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
Authors: Leonardo de Moura
|
|
|
-/
|
|
|
import Lean.Util.FindExpr
|
|
|
import Lean.Parser.Term
|
|
|
import Lean.Meta.Structure
|
|
|
import Lean.Elab.App
|
|
|
import Lean.Elab.Binders
|
|
|
|
|
|
set_option autoImplicit true
|
|
|
|
|
|
/-!
|
|
|
# Structure Instances With (Variadic) Holes
|
|
|
This file defines a term elaborator for structure instance syntax that includes "variadic holes",
|
|
|
i.e. holes of "variable length", which are represented via via the syntax `?..`, `?..!`, etc.,
|
|
|
e.g. `{ x := 0, ?.. }`.
|
|
|
This serves to port the functionality of mathlib3's `refine_struct { .. }`, but via `refine`
|
|
|
(e.g. `refine { ?.. }`).
|
|
|
Lean currently already supports one form of variadic hole in structure instances, namely `..`,
|
|
|
which fills all unspecified fields with natural metavariables and which is frequently used in
|
|
|
pattern matching.
|
|
|
Variadic holes that begin with a question mark are meant to parallel named holes (e.g. `?x`).
|
|
|
Therefore, syntax like `{ x := 0, ?.. }` will fill all remaining fields with metavariables named
|
|
|
by the field in question (e.g. `y := ?y`). Identifiers can optionally be provided to prefix the
|
|
|
name; see below.
|
|
|
Tests are performed in `Tests/StructInstWithHoles.lean`.
|
|
|
At the end of this file, we implement `haveFieldProj` in analogy to `have_field` with some
|
|
|
modifications. (This might be moved or eliminated.)
|
|
|
## Current specifics
|
|
|
The following is subject to change.
|
|
|
Several variants are supported to enable the choice between synthetic holes (`?`) and natural
|
|
|
ones, and to enable the choice between filling all unspecified fields with holes (`!`) and
|
|
|
synthesizing defaults where possible.
|
|
|
Currently only three combinations are allowed, since I can't see a use for unnamed/natural goals
|
|
|
with synthesized defaults. More descriptive syntax might be used for indicating whether to
|
|
|
synthesize defaults or not (e.g. `?.. noDefaults`)
|
|
|
synthesize defaults
|
|
|
┌──true──┬─false──┐
|
|
|
named goals │ `?..` │ `?..!` │
|
|
|
├────────┼────────┤
|
|
|
unnamed goals │ × │ `..` │
|
|
|
└────────┴────────┘
|
|
|
Identifiers can be provided after the variadic hole syntax in the `?` case, e.g. `?..foo` and
|
|
|
`?..!foo`. These will be prefixed to the goal name. For example, a field `y`'s goal will be named
|
|
|
`foo.y` instead of `y`.
|
|
|
# Overview of existing code
|
|
|
This document began as `StructInst.lean`, then was modified as needed. The modifications are done
|
|
|
in such a way as to (hopefully) make it easy for them to be absorbed into `StructInst.lean`, if
|
|
|
that's where it ends up. The following details how the original `StructInst.lean` works (which is
|
|
|
largely preserved).
|
|
|
## Short version
|
|
|
The way this works is that we start with syntax, parse it into a bare-bones `Struct`, use
|
|
|
`expandStruct` to expand that struct into another struct that has intermediate indicators
|
|
|
(`FieldVal`s) holding raw syntax or accounting for its absence. We then `elabStruct` that struct
|
|
|
into an `ElabStructResult` which has the potential result expression (an application of the
|
|
|
structure's single constructor to its values, which may be metavariables if they weren't found in
|
|
|
the syntax) plus info on the original struct. We then synthesize defaults using `propagate` to
|
|
|
assign any metavariables standing in for default values, and then return the expression.
|
|
|
## Long version
|
|
|
We start with turning the syntax into a struct. First we extract the sources (everything before
|
|
|
the `with` and any variadic holes (`..` or similar)), then we feed this to `elabStructInstAux`
|
|
|
along with the raw syntax and expected type. Inside `elabStructInstAux` we make the syntax into a
|
|
|
Struct (`mkStructView`), then `expandStruct`.
|
|
|
There's a "pre-expression scaffolding/framework/spine" set up early on in the process in the form
|
|
|
of FieldVal's, which hold raw information: `.term stx` where `stx` is syntax, if a term was
|
|
|
provided; a `.missing` value if it was missing; or a `.nested s` value where `s` is a `Struct` if
|
|
|
a subobject relation obtains. The `FieldVal`s for a field might be modified as elaboration
|
|
|
proceeds: for example, some might become `.nested`, or some defaults might turn into terms. This
|
|
|
all happens during `expandStruct`.
|
|
|
The `Struct` holds everything, and is updated throughout the process.
|
|
|
One of its fields is `field`, which holds a list of `Field Struct`'s. (The appearance of `Struct`
|
|
|
within `Field Struct` is to allow the `Struct`s to nest other `Struct`s when we have subobjects.)
|
|
|
The fields of each element of the `field` field (got that?) are
|
|
|
* `ref : Syntax`, which holds the `Syntax` found for that field
|
|
|
* `lhs : FieldLHS`, which describes the name of the field in question
|
|
|
* `val : FieldVal`, which holds the pre-expression `FieldVal`—either `.term stx` where `stx` is
|
|
|
the syntax of the field's value, `.default` (now `.missing`) if no syntax was found, or `.nested
|
|
|
s` if the field represents a subobject `s` of the structure (e.g. `toFoo`, produced by `extends`)
|
|
|
* `expr? : Option Expr`, which holds the elaborated expression when it becomes available (or a
|
|
|
metavariable, if the syntax is missing), and which begins at this stage as `none`.
|
|
|
`elacStructInstAux` then calls `elabStruct` on the skeletal `Struct` (which has appropriate
|
|
|
`FieldVal`s, but `none` for each field's `expr?`), which turns the `Struct` into an
|
|
|
`ElabStructResult`.
|
|
|
`elabStruct` elaborates everything but defaults, constructing the structure instance as an
|
|
|
expression given by the application of the structure's constructor to the values it finds by
|
|
|
elaborating the `stx` in any `.term stx` `FieldVal` while ensuring the appropriate type. (It's
|
|
|
not quite true that no defaults are taken care of here: `autoparam`s are turned into `.term`s.)
|
|
|
If the `FieldVal` is `.nested s`, it calls `elabStruct` on `s`; if it finds a `.default` (now
|
|
|
renamed to `.missing`) `FieldVal`, it uses a fresh metavariable in place of an elaborated
|
|
|
expression. As it does this, it stores any elaborated expressions in the `expr?` field of its
|
|
|
fields and builds this constructor application expression, which is, in the resulting
|
|
|
`ElabStructResult` structure, confusingly also named "val". Occasionally the `FieldVals` for each
|
|
|
field are updated as well. Also returned in `ElabStructResult` is the updated Struct with all its
|
|
|
new fields, and `instMVars`, an array of metavariables for dealing with typeclass instance
|
|
|
synthesis.
|
|
|
During `elabStruct`, defaults were inserted as metavariables into the constructed expression and
|
|
|
into `expr?`, but they were also annotated with ``structInstDefault` to indicate that they
|
|
|
represented a missing default value, and needed to be synthesized during the default loop.
|
|
|
Indeed, the function `isMissingDefault?` checks that this metavariable is unassigned when
|
|
|
deciding whether to return true or false. We finish our elaboration of the structure instance
|
|
|
with the `propagate` loop, which iteratively synthesizes the defaults, as sometimes the default
|
|
|
values of fields reference other fields which may also have a default value (etc.).
|
|
|
# Modifications
|
|
|
Changes from `StructInst.lean` are no longer marked with `!!` in a comment (or with `!!/`, `!!\`
|
|
|
surrounding a new or altered block). These are however visible in past commits.
|
|
|
Existing comments are left unchanged, and new comments begin with "~~".
|
|
|
## Syntax
|
|
|
We use the parser from `Term.lean`, but change `optional ".."` to our parseer for variadic holes,
|
|
|
`variadicHole`
|
|
|
## Logic
|
|
|
The original implementation of `..`, which creates a natural metavariable for each goal (and does
|
|
|
not synthesize defaults) affects things early on, at the stage of `FieldVal`s. Instead of using a
|
|
|
`.default` `FieldVal`, it makes a hole via syntax by providing a `.term (mkHole ref)` `FieldVal`
|
|
|
for each missing field value.
|
|
|
We preserve this behavior only for the `isSynthetic := false, useDefaults := false` case.
|
|
|
Otherwise, we use the `.default` `FieldVal`—now renamed to `.missing` to reflect its changed
|
|
|
function—and intervene mostly within the `ImplicitFields` namespace (previously the
|
|
|
`DefaultFields` namespace), where defaults are synthesized. If the variadic hole syntax says not
|
|
|
to, we don't propagate the default-synthesizing loop and therefore don't synthesize any defaults.
|
|
|
Typically, when the default loop ends with some fields still annotated as missing, an error is
|
|
|
thrown (`fields missing: ...`). However, if there's a variadic hole, we simply return from the
|
|
|
loop without error; next (whether the loop has run or not) we assign those remaining annotated
|
|
|
fields to *new* metavariables, which, in the `isSynthetic := true` case, are well-named and hold
|
|
|
all of the metadata we want them to. These are ripe to be used in a `refine` statement.
|
|
|
The only exception to this flow is how we handle `autoparam`s: autoparams are handled in
|
|
|
`elabStruct`, so that's where we intervene as well.
|
|
|
## Style
|
|
|
New code is often written in a "lookahead" fashion, to make it as easy as possible to move this
|
|
|
to core, in case it would better belong there. Therefore some cases that don't occur in this
|
|
|
elaboration are nonetheless accounted for—for example, the case where variadic hole syntax is
|
|
|
absent (where the value of struct.source.implicit is none), and the case where `isSynthetic :=
|
|
|
false, useDefaults := false`, which is already accounted for by existing `..` syntax. We use a
|
|
|
different token (`...`) only to show that this works.
|
|
|
This modification of `StructInst.lean` also attempts to be "minimally invasive" by intervening in
|
|
|
as few places as possible and leaving the existing flow of computation intact.
|
|
|
## Locations of changes
|
|
|
The changes to existing definitions are localized to the following:
|
|
|
### Necessary parsing and syntax processing changes
|
|
|
* The `structInst` term parser was modified to allow variadic hole syntax.
|
|
|
* `expandStructInstFieldAbbrev`
|
|
|
* update `$[..%$ell]?` syntax match to accommodate variadic holes
|
|
|
* type of `implicit` in `Source` structure: `Option Syntax` ⇒ `Option VariadicHoleConfig`
|
|
|
* originally this held the syntax `..` if present; now it holds information derived from the
|
|
|
variadic hole syntax (if present) as opposed to the raw syntax
|
|
|
* `getStructSource`
|
|
|
* inserted `getVariadicHoleConfig?` in front of the raw `implicitSource` syntax to process it
|
|
|
into a `VariadicHoleConfig`
|
|
|
* `formatStruct`
|
|
|
* instead of using a literal `".."` whenever `implicit.isSome`, use the syntax we encountered
|
|
|
(stored as one of the fields of `VariadicHoleConfig`)
|
|
|
### Logic
|
|
|
**Simple renamings**
|
|
|
* The `.default` `FieldVal`, which was used to indicate that fields would be synthesized by the
|
|
|
default loop, is renamed to `.missing` for clarity. Likewise `Struct.allDefault` is renamed to
|
|
|
`Struct.allMissing` (since it simply checks these `FieldVal`s), and `formatField` formats
|
|
|
`.missing` fields via `"<missing>"` instead of via `"<default>"`.
|
|
|
* We rename the `DefaultFields` namespace to `ImplicitFields`, since this is now where we
|
|
|
intervene to handle holes as well.
|
|
|
**Setup changes**
|
|
|
* `addMissingFields`, which is responsible for attaching `.missing` to unspecified fields,
|
|
|
previously attached a `.term (mkHole stx)` to any missing field whenever `..` was present. Here,
|
|
|
we only do so in the `isSynthetic := false, useDefaults := false` case, attaching `.missing` in
|
|
|
all other cases (both when we exepct them to be synthesized as defaults and not).
|
|
|
* `elabStruct` – this function uses `FieldVal`s to 1) generate `expr?`s for each field when
|
|
|
possible and 2) apply the structure's constructor to the arguments it finds to build the instance
|
|
|
expression. It stops short of synthesizing defaults, inserting a metavariable in both places when
|
|
|
it encounters a `.missing` field. However, autoparams for `.missing` values are handled here. We
|
|
|
therefore modify that section of the code so that
|
|
|
* if the variadic hole says to use holes instead of defaults, we don't try the autoparam
|
|
|
* if it says to use defaults, we try the autoparam in such a way that if it fails we use a hole
|
|
|
instead
|
|
|
* we also need to introduce a new optional `Bool` argument to the internal `cont` function
|
|
|
that, when modified from its default, takes a different branch. Otherwise `cont` is
|
|
|
untouched, and the original behavior is used when this argument is not specified.
|
|
|
* if there's no variadic hole, use the original behavior
|
|
|
**Default loop changes**
|
|
|
* `propagateLoop` – this is a pass of the loop used for synthesizing defaults, and is responsible
|
|
|
for throwing an error when too few fields are specified. If there is a variadic hole, it does not
|
|
|
throw that error and simply returns.
|
|
|
* `propagate` – this sets things up for the loop and executes it.
|
|
|
* We check the variadic hole config and don't run `propagateLoop` if it says not to. (We start
|
|
|
with a `do` to accommodate this.)
|
|
|
* At the end, if there is a variadic hole, we run `assignRemainingDefaultsToFieldHoles` (a new
|
|
|
function which does what you expect)
|
|
|
## New Code
|
|
|
The new functionality is in the `ImplicitFields` section to attach metadata to the goals
|
|
|
produced. Currently, we attach the metadata as a `KVMap` to the type of the goal, but this may
|
|
|
change. We use this metadata to resolve name conflicts, appending an appropriate index if any
|
|
|
existing metavariable is from a structure that shares a field name. This is meant to improve
|
|
|
clarity: for example, if `Foo` and `Bar` both have fields `x` and `y`,
|
|
|
`refine ({ y := 0, ?.. : Foo}, { x := 1, ?.. : Bar})` will produce goals `x` and `y_1` to show
|
|
|
that these are not from the same structure. (This may change if we decide to prefix each goal
|
|
|
name with the name of the structure.)
|
|
|
# Questions
|
|
|
* Should `trySynthStructInstance?` be run even when `useDefaults` is `false`?
|
|
|
* what about `bi == .instImplicit`? Should default synthesis be avoided in that case too?
|
|
|
* Dhould metadata be on the type, or somewhere else?
|
|
|
* Is the best way to get a unique id for a syntax instance via getPos? Do we need to do so anyway?
|
|
|
* Should utility-like functions be refactored into other files?
|
|
|
* Can the docstrings of the original structure instance and `refine` be modified from "within
|
|
|
mathlib" somehow?
|
|
|
* Do I need to add to "authors" at the top or worry about the copyright?
|
|
|
* Check for unreachable code after design decisions have been made.
|
|
|
-/
|
|
|
namespace Lean.Elab.Term.StructInstWithHoles
|
|
|
|
|
|
open Meta
|
|
|
open TSyntax.Compat
|
|
|
|
|
|
/--
|
|
|
A synthetic variadic hole. When used in structure instance syntax, it fills the unspecified
|
|
|
fields with metavariables named by the field. It synthesizes defaults when possible.
|
|
|
It can be followed by an identifier to specify a prefix for the names of the holes.
|
|
|
-/
|
|
|
def vH?dd := leading_parser "?.." >> Parser.optional Parser.ident
|
|
|
/--
|
|
|
A synthetic variadic hole that does not synthesize any defaults. When used in structure instance
|
|
|
syntax, it fills the unspecified fields with metavariables named by the field. It synthesizes
|
|
|
defaults when possible. It can be followed by an identifier to specify a prefix for the names of
|
|
|
the holes.
|
|
|
-/
|
|
|
def vH?dd! := leading_parser "?..!" >> Parser.optional Parser.ident
|
|
|
/-~~! Removed for now.
|
|
|
/-- A natural variadic hole that does not synthesize defaults. -/
|
|
|
def vHdd! := leading_parser "..!"
|
|
|
/-- A natural variadic hole that synthesizes defaults when possible. -/
|
|
|
def vHdd := leading_parser "..."
|
|
|
-/
|
|
|
/-- A variadic hole that fills multiple spots with holes. -/
|
|
|
def variadicHole := leading_parser (vH?dd <|> vH?dd! /-~~! <|> vHdd! <|> vHdd-/)
|
|
|
|
|
|
open Lean.Parser Lean.Parser.Term in
|
|
|
/--
|
|
|
Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
|
|
|
inherited. If `e` is itself a variable called `x`, it can be elided:
|
|
|
`fun x => { x , y := 1 }`.
|
|
|
A *structure update* of an existing value can be given via `with`:
|
|
|
`{ point with x := 1 }`.
|
|
|
The structure type can be specified if not inferable:
|
|
|
`{ x := 1, y := 2 : Point }`.
|
|
|
`..` can be used in pattern-matching to fill all unspecified fields with `_`:
|
|
|
`match s with | { x := 1, .. } => ...`
|
|
|
`?..` fills all unspecified fields with automatically-named goals:
|
|
|
if a `Foo` has fields `x`, `y`, `z`, `{ x := 1, ?.. } : Foo` creates `?y`, `?z`.
|
|
|
-/
|
|
|
@[term_parser] def structInstWithHoles := leading_parser "{" >> ppHardSpace >> Lean.Parser.optional
|
|
|
(atomic (sepBy1 termParser ", " >> " with "))
|
|
|
>> sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true)
|
|
|
>> variadicHole -- Only apply this elaboration to syntax that has one of these holes
|
|
|
>> Lean.Parser.optional (" : " >> termParser) >> " }"
|
|
|
|
|
|
/--
|
|
|
Syntactically move any type specification outside of the structure instance syntax:
|
|
|
`{ x := 0 : Foo }` becomes `{ x := 0 } : Foo`.
|
|
|
-/
|
|
|
@[macro structInstWithHoles] def expandStructInstWithHolesExpectedType : Macro := fun stx =>
|
|
|
let expectedArg := stx[4]
|
|
|
if expectedArg.isNone then
|
|
|
Macro.throwUnsupported
|
|
|
else
|
|
|
let expected := expectedArg[1]
|
|
|
let stxNew := stx.setArg 4 mkNullNode
|
|
|
`(($stxNew : $expected))
|
|
|
|
|
|
/-- Expand field abbreviations. Example: `{ x, y := 0 }` expands to `{ x := x, y := 0 }` -/
|
|
|
@[macro structInstWithHoles] def expandStructInstWithHolesFieldAbbrev : Macro
|
|
|
| `({ $[$srcs,* with]? $fields,* $ell:variadicHole $[: $ty]? }) =>
|
|
|
if fields.getElems.raw.any (·.getKind == ``Lean.Parser.Term.structInstFieldAbbrev) then do
|
|
|
let fieldsNew ← fields.getElems.mapM fun
|
|
|
| `(Parser.Term.structInstFieldAbbrev| $id:ident) =>
|
|
|
`(Parser.Term.structInstField| $id:ident := $id:ident)
|
|
|
| field => return field
|
|
|
`({ $[$srcs,* with]? $fieldsNew,* $ell $[: $ty]? })
|
|
|
else
|
|
|
Macro.throwUnsupported
|
|
|
| _ => Macro.throwUnsupported
|
|
|
|
|
|
/--
|
|
|
If `stx` is of the form `{ s₁, ..., sₙ with ... }` and `sᵢ` is not a local variable, expand into
|
|
|
`let src := sᵢ; { ..., src, ... with ... }`.
|
|
|
Note that this one is not a `Macro` because we need to access the local context.
|
|
|
-/
|
|
|
private def expandNonAtomicExplicitSources (stx : Syntax) : TermElabM (Option Syntax) := do
|
|
|
let sourcesOpt := stx[1]
|
|
|
if sourcesOpt.isNone then
|
|
|
return none
|
|
|
else
|
|
|
let sources := sourcesOpt[0]
|
|
|
if sources.isMissing then
|
|
|
throwAbortTerm
|
|
|
let sources := sources.getSepArgs
|
|
|
if (← sources.allM fun source => return (← isLocalIdent? source).isSome) then
|
|
|
return none
|
|
|
if sources.any (·.isMissing) then
|
|
|
throwAbortTerm
|
|
|
return some (← go sources.toList #[])
|
|
|
where
|
|
|
go (sources : List Syntax) (sourcesNew : Array Syntax) : TermElabM Syntax := do
|
|
|
match sources with
|
|
|
| [] =>
|
|
|
let sources := Syntax.mkSep sourcesNew (mkAtomFrom stx ", ")
|
|
|
return stx.setArg 1 (stx[1].setArg 0 sources)
|
|
|
| source :: sources =>
|
|
|
if (← isLocalIdent? source).isSome then
|
|
|
go sources (sourcesNew.push source)
|
|
|
else
|
|
|
withFreshMacroScope do
|
|
|
let sourceNew ← `(src)
|
|
|
let r ← go sources (sourcesNew.push sourceNew)
|
|
|
`(let src := $source; $r)
|
|
|
|
|
|
/-- Information for any explicit sources encountered (i.e. some `sᵢ` in `s₁, ..., sₙ with`) -/
|
|
|
structure ExplicitSourceInfo where
|
|
|
/-- The syntax of some `sᵢ` in `s₁, ..., sₙ with` -/
|
|
|
stx : Syntax
|
|
|
/-- The name of some structure `sᵢ` in `s₁, ..., sₙ with` -/
|
|
|
structName : Name
|
|
|
deriving Inhabited
|
|
|
|
|
|
/--
|
|
|
Information deduced from variadic hole syntax, as well as the raw
|
|
|
syntax itself and any identifiers that were found.
|
|
|
-/
|
|
|
structure VariadicHoleConfig where
|
|
|
/-- The raw variadic hole syntax encountered (`?..`, `..`, etc.)-/
|
|
|
stx : TSyntax ``variadicHole
|
|
|
/-- An optional name `x` found in `?..x` or `?..!x`, to be used as a prefix. -/
|
|
|
name : Option Name := none
|
|
|
/-- Whether the holes should be synthetic and automatically named. -/
|
|
|
isSynthetic : Bool
|
|
|
/-- Whether defaults should attempt to be synthesized before filling fields with holes. -/
|
|
|
useDefaults : Bool
|
|
|
deriving Inhabited, Repr
|
|
|
|
|
|
/--
|
|
|
Information on other sources of field values via structure update syntax or variadic holes.
|
|
|
Collects of explicit source info (preceding `with` in structure updates) and implicit source
|
|
|
info (for specification of holes, e.g. `..` or `?..`).
|
|
|
-/
|
|
|
structure Source where
|
|
|
/-- info for all `sᵢ` in `s₁, ..., sₙ with` -/
|
|
|
explicit : Array ExplicitSourceInfo
|
|
|
/-- info for any variadic hole syntax encountered (`?..`, `..`, etc.) -/
|
|
|
implicit : Option VariadicHoleConfig
|
|
|
deriving Inhabited
|
|
|
|
|
|
/-- Check if neither an explicit nor an implicit source has been specified. -/
|
|
|
def Source.isNone : Source → Bool
|
|
|
| { explicit := #[], implicit := none } => true
|
|
|
| _ => false
|
|
|
|
|
|
/-- Process variadic hole syntax into a VariadicHoleConfig. -/
|
|
|
def getVariadicHoleConfig? : TSyntax ``variadicHole → Option VariadicHoleConfig
|
|
|
| stx => match stx with
|
|
|
| `(variadicHole|?..$[$x:ident]?) => some
|
|
|
{stx, isSynthetic := true, useDefaults := true, name := x.map Syntax.getId}
|
|
|
| `(variadicHole|?..!$[$x:ident]?) => some
|
|
|
{stx, isSynthetic := true, useDefaults := false, name := x.map Syntax.getId}
|
|
|
| _ => none
|
|
|
|
|
|
/--
|
|
|
Put an array of source syntax into a form which matches
|
|
|
`optional (atomic (sepBy1 termParser ", " >> " with ")`, e.g. `s₁, s₂, s₃ with`.
|
|
|
Should only be called when `sources` is a nonempty `Array`.
|
|
|
-/
|
|
|
private def mkSourcesWithSyntax (sources : Array Syntax) : Syntax :=
|
|
|
let ref := sources[0]!
|
|
|
let stx := Syntax.mkSep sources (mkAtomFrom ref ", ")
|
|
|
mkNullNode #[stx, mkAtomFrom ref "with "]
|
|
|
|
|
|
/--
|
|
|
Extract and process both explicit (`s₁, ..., sₙ with`) and implicit (`..`, `?..`, etc.) source
|
|
|
syntax from structure syntax.
|
|
|
-/
|
|
|
private def getStructSource (structStx : Syntax) : TermElabM Source :=
|
|
|
withRef structStx do
|
|
|
let explicitSource := structStx[1]
|
|
|
let implicitSource := structStx[3]
|
|
|
let explicit ← if explicitSource.isNone then
|
|
|
pure #[]
|
|
|
else
|
|
|
explicitSource[0].getSepArgs.mapM fun stx => do
|
|
|
let some src ← isLocalIdent? stx | unreachable!
|
|
|
addTermInfo' stx src
|
|
|
let srcType ← whnf (← inferType src)
|
|
|
tryPostponeIfMVar srcType
|
|
|
let structName ← getStructureName srcType
|
|
|
return { stx, structName }
|
|
|
let implicit :=
|
|
|
if implicitSource[0].isNone
|
|
|
then none
|
|
|
else getVariadicHoleConfig? implicitSource
|
|
|
return { explicit, implicit }
|
|
|
|
|
|
/--
|
|
|
We say a `{ ... }` notation is a `modifyOp` if it contains only one
|
|
|
```
|
|
|
def structInstArrayRef := leading_parser "[" >> termParser >>"]"
|
|
|
```
|
|
|
-/
|
|
|
private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
|
|
|
let s? ← stx[2].getSepArgs.foldlM (init := none) fun s? arg => do
|
|
|
/- arg is of the form `structInstFieldAbbrev <|> structInstField` -/
|
|
|
if arg.getKind == ``Lean.Parser.Term.structInstField then
|
|
|
/- Remark: the syntax for `structInstField` is
|
|
|
```
|
|
|
def structInstLVal := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many
|
|
|
(group ("." >> (ident <|> numLit)) <|> structInstArrayRef)
|
|
|
def structInstField := leading_parser structInstLVal >> " := " >> termParser
|
|
|
```
|
|
|
-/
|
|
|
let lval := arg[0]
|
|
|
let k := lval[0].getKind
|
|
|
if k == ``Lean.Parser.Term.structInstArrayRef then
|
|
|
match s? with
|
|
|
| none => return some arg
|
|
|
| some s =>
|
|
|
if s.getKind == ``Lean.Parser.Term.structInstArrayRef then
|
|
|
throwErrorAt arg "invalid \{...} notation, at most one `[..]` at a given level"
|
|
|
else
|
|
|
throwErrorAt arg "invalid \{...} notation, can't mix field and `[..]` at a given level"
|
|
|
else
|
|
|
match s? with
|
|
|
| none => return some arg
|
|
|
| some s =>
|
|
|
if s.getKind == ``Lean.Parser.Term.structInstArrayRef then
|
|
|
throwErrorAt arg "invalid \{...} notation, can't mix field and `[..]` at a given level"
|
|
|
else
|
|
|
return s?
|
|
|
else
|
|
|
return s?
|
|
|
match s? with
|
|
|
| none => return none
|
|
|
| some s => if s[0][0].getKind == ``Lean.Parser.Term.structInstArrayRef then return s? else
|
|
|
return none
|
|
|
|
|
|
/-- Elaborate `modifyOp`s given a single explicit source. -/
|
|
|
private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSourceInfo)
|
|
|
(expectedType? : Option Expr) : TermElabM Expr := do
|
|
|
if sources.size > 1 then
|
|
|
throwError "invalid \{...} notation, multiple sources and array update is not supported."
|
|
|
let cont (val : Syntax) : TermElabM Expr := do
|
|
|
let lval := modifyOp[0][0]
|
|
|
let idx := lval[1]
|
|
|
let self := sources[0]!.stx
|
|
|
let stxNew ← `($(self).modifyOp (idx := $idx) (fun s => $val))
|
|
|
trace[Elab.struct.modifyOp] "{stx}\n===>\n{stxNew}"
|
|
|
withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
|
|
|
let rest := modifyOp[0][1]
|
|
|
if rest.isNone then
|
|
|
cont modifyOp[2]
|
|
|
else
|
|
|
let s ← `(s)
|
|
|
let valFirst := rest[0]
|
|
|
let valFirst := if valFirst.getKind == ``Lean.Parser.Term.structInstArrayRef then valFirst
|
|
|
else valFirst[1]
|
|
|
let restArgs := rest.getArgs
|
|
|
let valRest := mkNullNode restArgs[1:restArgs.size]
|
|
|
let valField := modifyOp.setArg 0 <| mkNode ``Parser.Term.structInstLVal #[valFirst, valRest]
|
|
|
let valSource := mkSourcesWithSyntax #[s]
|
|
|
let val := stx.setArg 1 valSource
|
|
|
let val := val.setArg 2 <| mkNullNode #[valField]
|
|
|
trace[Elab.struct.modifyOp] "{stx}\nval: {val}"
|
|
|
cont val
|
|
|
|
|
|
/--
|
|
|
Get structure name.
|
|
|
This method tries to postpone execution if the expected type is not available.
|
|
|
If the expected type is available and it is a structure, then we use it.
|
|
|
Otherwise, we use the type of the first source.
|
|
|
-/
|
|
|
private def getStructName (expectedType? : Option Expr) (sourceView : Source) : TermElabM Name := do
|
|
|
tryPostponeIfNoneOrMVar expectedType?
|
|
|
let useSource : Unit → TermElabM Name := fun _ => do
|
|
|
unless sourceView.explicit.isEmpty do
|
|
|
return sourceView.explicit[0]!.structName
|
|
|
match expectedType? with
|
|
|
| some expectedType => throwUnexpectedExpectedType expectedType
|
|
|
| none => throwUnknownExpectedType
|
|
|
match expectedType? with
|
|
|
| none => useSource ()
|
|
|
| some expectedType =>
|
|
|
let expectedType ← whnf expectedType
|
|
|
match expectedType.getAppFn with
|
|
|
| Expr.const constName _ =>
|
|
|
unless isStructure (← getEnv) constName do
|
|
|
throwError "invalid \{...} notation, structure type expected{indentExpr expectedType}"
|
|
|
return constName
|
|
|
| _ => useSource ()
|
|
|
where
|
|
|
throwUnknownExpectedType :=
|
|
|
throwError "invalid \{...} notation, expected type is not known"
|
|
|
throwUnexpectedExpectedType type (kind := "expected") := do
|
|
|
let type ← instantiateMVars type
|
|
|
if type.getAppFn.isMVar then
|
|
|
throwUnknownExpectedType
|
|
|
else
|
|
|
throwError "invalid \{...} notation, {kind} type is not of the form (C ...){indentExpr type}"
|
|
|
|
|
|
/-- Information on the left hand side of a binding encountered in structure syntax. -/
|
|
|
inductive FieldLHS where
|
|
|
/-- A representation of the name of a field as encountered in binding syntax (e.g. `x` in
|
|
|
`x := ...`). -/
|
|
|
| fieldName (ref : Syntax) (name : Name)
|
|
|
/-- A representation of the index of a field as encountered in binding syntax (e.g. `3` in
|
|
|
`3 := ...`). -/
|
|
|
| fieldIndex (ref : Syntax) (idx : Nat)
|
|
|
/-- A representation of a modifyOp as encountered in binding syntax. -/
|
|
|
| modifyOp (ref : Syntax) (index : Syntax)
|
|
|
deriving Inhabited
|
|
|
|
|
|
instance : ToFormat FieldLHS := ⟨fun lhs =>
|
|
|
match lhs with
|
|
|
| .fieldName _ n => format n
|
|
|
| .fieldIndex _ i => format i
|
|
|
| .modifyOp _ i => "[" ++ i.prettyPrint ++ "]"⟩
|
|
|
|
|
|
/--
|
|
|
A limited, pre-expression description of the values of fields. Only terms given by raw syntax,
|
|
|
nested values (for subobjects), and missing values are can be specified.
|
|
|
The polymorphism via its `Type` argument is only used for nested `FieldVal`s, which need to
|
|
|
know what type their argument should be. In practice, we only ever take this argument to be
|
|
|
`Struct`.
|
|
|
-/
|
|
|
inductive FieldVal (σ : Type) where
|
|
|
/-- Term syntax encountered on the RHS of a binding, e.g. `1+1` in `x := 1+1`. -/
|
|
|
| term (stx : Syntax) : FieldVal σ
|
|
|
/-- A nested `FieldVal`, which in practice is used to hold subobjects as `Struct`s. -/
|
|
|
| nested (s : σ) : FieldVal σ
|
|
|
/-- An indication that this field was missing, i.e. not specified explicitly in the syntax. -/
|
|
|
| missing : FieldVal σ
|
|
|
deriving Inhabited
|
|
|
|
|
|
/--
|
|
|
A representation of a field in a structure. This contains the original syntax of the field
|
|
|
(`ref`), a representation of the LHS of the `:=` binding (`lhs`), the pre-expression `FieldVal`
|
|
|
(`val`), and the actual expression that we take to be the value of the field (`expr?`).
|
|
|
`expr?` begins as `none`, and is modified over the course of this code as we figure out whether
|
|
|
we need to elaborate some syntax encountered (e.g. if `.term stx` is in `val`) or if the field
|
|
|
value is `.missing` (in which case we make a metavariable).
|
|
|
-/
|
|
|
structure Field (σ : Type) where
|
|
|
/-- The syntax of the binding used to specify this field. -/
|
|
|
ref : Syntax
|
|
|
/-- Information on the LHS of the binding used to specify this field. -/
|
|
|
lhs : List FieldLHS
|
|
|
/-- The basic content of the field value, prior to elaboration. -/
|
|
|
val : FieldVal σ
|
|
|
/-- The elaborated value of the field in question as it becomes available, which starts
|
|
|
out as `none` and is updated during `elabStruct` with either elaborated terms or
|
|
|
metavariables which may get assigned to synthesized defaults. -/
|
|
|
expr? : Option Expr := none
|
|
|
deriving Inhabited
|
|
|
|
|
|
/-- Check if the LHS of the binding specifying a field is a single `FieldLHS`. -/
|
|
|
def Field.isSimple {σ} : Field σ → Bool
|
|
|
| { lhs := [_], .. } => true
|
|
|
| _ => false
|
|
|
|
|
|
/--
|
|
|
The organized content of the structure instance.
|
|
|
The field `params` is used for `.missing` value propagation. It is initially empty, and
|
|
|
then set at `elabStruct`. -/
|
|
|
inductive Struct where
|
|
|
| mk (ref : Syntax) (structName : Name) (params : Array (Name × Expr))
|
|
|
(fields : List (Field Struct)) (source : Source)
|
|
|
deriving Inhabited
|
|
|
|
|
|
/-- Abbreviation for `List (Field Struct)`: A list of representations of the structure's fields. -/
|
|
|
abbrev Fields := List (Field Struct)
|
|
|
|
|
|
/-- The original syntax of the structure instance. -/
|
|
|
def Struct.ref : Struct → Syntax
|
|
|
| ⟨ref, _, _, _, _⟩ => ref
|
|
|
|
|
|
/-- The name of the structure. -/
|
|
|
def Struct.structName : Struct → Name
|
|
|
| ⟨_, structName, _, _, _⟩ => structName
|
|
|
|
|
|
/-- Parameters used during the initial processing of `.missing` fields. Initially `none`, and set
|
|
|
at `elabStruct`. -/
|
|
|
def Struct.params : Struct → Array (Name × Expr)
|
|
|
| ⟨_, _, params, _, _⟩ => params
|
|
|
|
|
|
/-- The list of `fields` in the structure instance as `Field Struct`s. Updated over the course of
|
|
|
the elaboration to include computed values. -/
|
|
|
def Struct.fields : Struct → Fields
|
|
|
| ⟨_, _, _, fields, _⟩ => fields
|
|
|
|
|
|
/-- Information on other sources of values for the structure. Namely, any structures preceding
|
|
|
`with` in structure update syntax and any variadic holes (`..`, `?..`) following the field
|
|
|
bindings. -/
|
|
|
def Struct.source : Struct → Source
|
|
|
| ⟨_, _, _, _, s⟩ => s
|
|
|
|
|
|
/-- `true` iff all fields of the given structure are marked as `.missing`. -/
|
|
|
partial def Struct.allMissing (s : Struct) : Bool :=
|
|
|
s.fields.all fun { val := val, .. } => match val with
|
|
|
| .term _ => false
|
|
|
| .missing => true
|
|
|
| .nested s => allMissing s
|
|
|
|
|
|
/-- Pretty-prints a field (`Field Struct`). Uses the field LHS's and its `val : FieldVal Struct`. -/
|
|
|
def formatField (formatStruct : Struct → Format) (field : Field Struct) : Format :=
|
|
|
Format.joinSep field.lhs " . " ++ " := " ++
|
|
|
match field.val with
|
|
|
| .term v => v.prettyPrint
|
|
|
| .nested s => formatStruct s
|
|
|
| .missing => "<missing>"
|
|
|
|
|
|
/-- Pretty-prints a `Struct`. -/
|
|
|
partial def formatStruct : Struct → Format
|
|
|
| ⟨_, _, _, fields, source⟩ =>
|
|
|
let fieldsFmt := Format.joinSep (fields.map (formatField formatStruct)) ", "
|
|
|
let implicitFmt := match source.implicit with
|
|
|
| some v => format v.stx
|
|
|
| none => ""
|
|
|
if source.explicit.isEmpty then
|
|
|
"{" ++ fieldsFmt ++ implicitFmt ++ "}"
|
|
|
else
|
|
|
"{" ++ format (source.explicit.map (·.stx)) ++ " with " ++ fieldsFmt ++ implicitFmt ++ "}"
|
|
|
|
|
|
instance : ToFormat Struct := ⟨formatStruct⟩
|
|
|
instance : ToString Struct := ⟨toString ∘ format⟩
|
|
|
|
|
|
instance : ToFormat (Field Struct) := ⟨formatField formatStruct⟩
|
|
|
instance : ToString (Field Struct) := ⟨toString ∘ format⟩
|
|
|
|
|
|
/--
|
|
|
Turns a `FieldLHS` into syntax. The first argument specifies whether this is the first in a list of
|
|
|
`FieldLHS`'s or not.
|
|
|
Recall that `structInstField` elements have the form
|
|
|
```
|
|
|
def structInstField := leading_parser structInstLVal >> " := " >> termParser
|
|
|
def structInstLVal := leading_parser (ident <|> numLit <|> structInstArrayRef)
|
|
|
>> many (("." >> (ident <|> numLit)) <|> structInstArrayRef)
|
|
|
def structInstArrayRef := leading_parser "[" >> termParser >>"]"
|
|
|
```
|
|
|
Remark: this code relies on the fact that `expandStruct` only transforms `fieldLHS.fieldName`
|
|
|
-/
|
|
|
def FieldLHS.toSyntax (first : Bool) : FieldLHS → Syntax
|
|
|
| .modifyOp stx _ => stx
|
|
|
| .fieldName stx name => if first then mkIdentFrom stx name
|
|
|
else mkGroupNode #[mkAtomFrom stx ".", mkIdentFrom stx name]
|
|
|
| .fieldIndex stx _ => if first then stx else mkGroupNode #[mkAtomFrom stx ".", stx]
|
|
|
|
|
|
/-- Extracts the `stx` from a `.term stx : FieldVal Struct`. Panics when called on any other
|
|
|
constructor of `FieldVal Struct`. -/
|
|
|
def FieldVal.toSyntax : FieldVal Struct → Syntax
|
|
|
| .term stx => stx
|
|
|
| _ => unreachable!
|
|
|
|
|
|
/-- Turns a field (as a `Field Struct`) into syntax if has a `val` of the form `.term stx`; panics
|
|
|
otherwise. Panics if the `lhs` is an empty list. -/
|
|
|
def Field.toSyntax : Field Struct → Syntax
|
|
|
| field =>
|
|
|
let stx := field.ref
|
|
|
let stx := stx.setArg 2 field.val.toSyntax
|
|
|
match field.lhs with
|
|
|
| first::rest => stx.setArg 0 <| mkNullNode
|
|
|
#[first.toSyntax true, mkNullNode <| rest.toArray.map (FieldLHS.toSyntax false) ]
|
|
|
| _ => unreachable!
|
|
|
|
|
|
/-- Processes syntax into a `FieldLHS`. -/
|
|
|
private def toFieldLHS (stx : Syntax) : MacroM FieldLHS :=
|
|
|
if stx.getKind == ``Lean.Parser.Term.structInstArrayRef then
|
|
|
return FieldLHS.modifyOp stx stx[1]
|
|
|
else
|
|
|
-- Note that the representation of the first field is different.
|
|
|
let stx := if stx.getKind == groupKind then stx[1] else stx
|
|
|
if stx.isIdent then
|
|
|
return FieldLHS.fieldName stx stx.getId.eraseMacroScopes
|
|
|
else match stx.isFieldIdx? with
|
|
|
| some idx => return FieldLHS.fieldIndex stx idx
|
|
|
| none => Macro.throwError "unexpected structure syntax"
|
|
|
|
|
|
/-- Processes structure instance syntax into a `Struct` given the `structName` and its `source`s. -/
|
|
|
private def mkStructView (stx : Syntax) (structName : Name) (source : Source) : MacroM Struct := do
|
|
|
/- Recall that `stx` is of the form
|
|
|
```
|
|
|
leading_parser "{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
|
|
|
>> sepByIndent (structInstFieldAbbrev <|> structInstField) ...
|
|
|
>> variadicHole
|
|
|
>> optional (" : " >> termParser)
|
|
|
>> " }"
|
|
|
```
|
|
|
This method assumes that `structInstFieldAbbrev` had already been expanded.
|
|
|
-/
|
|
|
let fields ← stx[2].getSepArgs.toList.mapM fun fieldStx => do
|
|
|
let val := fieldStx[2]
|
|
|
let first ← toFieldLHS fieldStx[0][0]
|
|
|
let rest ← fieldStx[0][1].getArgs.toList.mapM toFieldLHS
|
|
|
return { ref := fieldStx, lhs := first :: rest, val := FieldVal.term val : Field Struct }
|
|
|
return ⟨stx, structName, #[], fields, source⟩
|
|
|
|
|
|
/-- (Monadic) Modifies a `Struct`'s fields with a monadic function. -/
|
|
|
def Struct.modifyFieldsM {m : Type → Type} [Monad m] (s : Struct) (f : Fields → m Fields) :
|
|
|
m Struct :=
|
|
|
match s with
|
|
|
| ⟨ref, structName, params, fields, source⟩ =>
|
|
|
return ⟨ref, structName, params, (← f fields), source⟩
|
|
|
|
|
|
/-- Modify a `Struct`'s `Fields` with a function. -/
|
|
|
def Struct.modifyFields (s : Struct) (f : Fields → Fields) : Struct :=
|
|
|
Id.run <| s.modifyFieldsM f
|
|
|
|
|
|
/-- Overwrite a `Struct`'s fields. -/
|
|
|
def Struct.setFields (s : Struct) (fields : Fields) : Struct :=
|
|
|
s.modifyFields fun _ => fields
|
|
|
|
|
|
/-- Overwrite a `Struct`'s params. -/
|
|
|
def Struct.setParams (s : Struct) (ps : Array (Name × Expr)) : Struct :=
|
|
|
match s with
|
|
|
| ⟨ref, structName, _, fields, source⟩ => ⟨ref, structName, ps, fields, source⟩
|
|
|
|
|
|
/-- Breaks down non-anonymous names in the lhs of fields into lists of their components. -/
|
|
|
private def expandCompositeFields (s : Struct) : Struct :=
|
|
|
s.modifyFields fun fields => fields.map fun field => match field with
|
|
|
| { lhs := .fieldName _ (.str Name.anonymous ..) :: _, .. } => field
|
|
|
| { lhs := .fieldName ref n@(.str ..) :: rest, .. } =>
|
|
|
let newEntries := n.components.map <| FieldLHS.fieldName ref
|
|
|
{ field with lhs := newEntries ++ rest }
|
|
|
| _ => field
|
|
|
|
|
|
/-- Replaces field lhs's that are specified by index with the name of the field (as registered in
|
|
|
the structure). -/
|
|
|
private def expandNumLitFields (s : Struct) : TermElabM Struct :=
|
|
|
s.modifyFieldsM fun fields => do
|
|
|
let env ← getEnv
|
|
|
let fieldNames := getStructureFields env s.structName
|
|
|
fields.mapM fun field => match field with
|
|
|
| { lhs := .fieldIndex ref idx :: rest, .. } =>
|
|
|
if idx == 0 then throwErrorAt ref "invalid field index, index must be greater than 0"
|
|
|
else if idx > fieldNames.size
|
|
|
then throwErrorAt ref "invalid field index, structure has only #{fieldNames.size} fields"
|
|
|
else return { field with lhs := .fieldName ref fieldNames[idx - 1]! :: rest }
|
|
|
| _ => return field
|
|
|
|
|
|
/-- For example, consider the following structures:
|
|
|
```
|
|
|
structure A where
|
|
|
x : Nat
|
|
|
structure B extends A where
|
|
|
y : Nat
|
|
|
structure C extends B where
|
|
|
z : Bool
|
|
|
```
|
|
|
This method expands parent structure fields using the path to the parent structure.
|
|
|
For example,
|
|
|
```
|
|
|
{ x := 0, y := 0, z := true : C }
|
|
|
```
|
|
|
is expanded into
|
|
|
```
|
|
|
{ toB.toA.x := 0, toB.y := 0, z := true : C }
|
|
|
```
|
|
|
-/
|
|
|
private def expandParentFields (s : Struct) : TermElabM Struct := do
|
|
|
let env ← getEnv
|
|
|
s.modifyFieldsM fun fields => fields.mapM fun field => do match field with
|
|
|
| { lhs := .fieldName ref fieldName :: _, .. } =>
|
|
|
addCompletionInfo <| CompletionInfo.fieldId ref fieldName (← getLCtx) s.structName
|
|
|
match findField? env s.structName fieldName with
|
|
|
| none => throwErrorAt ref "'{fieldName}' is not a field of structure '{s.structName}'"
|
|
|
| some baseStructName =>
|
|
|
if baseStructName == s.structName then pure field
|
|
|
else match getPathToBaseStructure? env baseStructName s.structName with
|
|
|
| some path =>
|
|
|
let path := path.map fun funName => match funName with
|
|
|
| .str _ s => .fieldName ref (Name.mkSimple s)
|
|
|
| _ => unreachable!
|
|
|
return { field with lhs := path ++ field.lhs }
|
|
|
| _ => throwErrorAt ref "failed to access field '{fieldName}' in parent structure"
|
|
|
| _ => return field
|
|
|
|
|
|
/-- Abbreviation for `HashMap Name Fields`: A hash map from field names to lists of representations
|
|
|
of fields. -/
|
|
|
private abbrev FieldMap := HashMap Name Fields
|
|
|
|
|
|
/-- Creates a hash map from field names to lists of representations of fields. The length of the
|
|
|
list can be greater than one if the field is not simple. Panics if the lhs of a field is empty.
|
|
|
-/
|
|
|
private def mkFieldMap (fields : Fields) : TermElabM FieldMap :=
|
|
|
fields.foldlM (init := {}) fun fieldMap field =>
|
|
|
match field.lhs with
|
|
|
| .fieldName _ fieldName :: _ =>
|
|
|
match fieldMap.find? fieldName with
|
|
|
| some (prevField::restFields) =>
|
|
|
if field.isSimple || prevField.isSimple then
|
|
|
throwErrorAt field.ref "field '{fieldName}' has already been specified"
|
|
|
else
|
|
|
return fieldMap.insert fieldName (field::prevField::restFields)
|
|
|
| _ => return fieldMap.insert fieldName [field]
|
|
|
| _ => unreachable!
|
|
|
|
|
|
/-- Unwraps a `Field Struct` from a list of length one, and otherwise returns `none`. -/
|
|
|
private def isSimpleField? : Fields → Option (Field Struct)
|
|
|
| [field] => if field.isSimple then some field else none
|
|
|
| _ => none
|
|
|
|
|
|
/-- Finds the index of the field name in its third argument in the list of field names in its
|
|
|
second. The first argument, the name of the structure, is used only for descriptive error
|
|
|
messages. -/
|
|
|
private def getFieldIdx (structName : Name) (fieldNames : Array Name) (fieldName : Name) :
|
|
|
TermElabM Nat := do
|
|
|
match fieldNames.findIdx? fun n => n == fieldName with
|
|
|
| some idx => return idx
|
|
|
| none => throwError "field '{fieldName}' is not a valid field of '{structName}'"
|
|
|
|
|
|
/-- Constructs the syntax for a field projection. Only does so if the given field name is in fact a
|
|
|
field of the given structure name; returns `none` otherwise. -/
|
|
|
def mkProjStx? (s : Syntax) (structName : Name) (fieldName : Name) : TermElabM (Option Syntax) := do
|
|
|
if (findField? (← getEnv) structName fieldName).isNone then
|
|
|
return none
|
|
|
return some <| mkNode ``Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName]
|
|
|
|
|
|
/-- Gets a field from a list of fields by name. If not found, returns `none`. -/
|
|
|
def findField? (fields : Fields) (fieldName : Name) : Option (Field Struct) :=
|
|
|
fields.find? fun field =>
|
|
|
match field.lhs with
|
|
|
| [.fieldName _ n] => n == fieldName
|
|
|
| _ => false
|
|
|
|
|
|
mutual
|
|
|
|
|
|
/-- Group fields that belong to a subobject as a `Struct` under that subobject field via a
|
|
|
`.nested s` `FieldVal`. For example, a `Struct` representing
|
|
|
`{ toFoo.x := 1, toFoo.y := 2, z := 3 }` will become one representing
|
|
|
`{ toFoo := { x := 1, y := 2 }, z := 3 }`.
|
|
|
-/
|
|
|
private partial def groupFields (s : Struct) : TermElabM Struct := do
|
|
|
let env ← getEnv
|
|
|
withRef s.ref do
|
|
|
s.modifyFieldsM fun fields => do
|
|
|
let fieldMap ← mkFieldMap fields
|
|
|
fieldMap.toList.mapM fun ⟨fieldName, fields⟩ => do
|
|
|
match isSimpleField? fields with
|
|
|
| some field => pure field
|
|
|
| none =>
|
|
|
let substructFields := fields.map fun field => { field with lhs := field.lhs.tail! }
|
|
|
let field := fields.head!
|
|
|
match Lean.isSubobjectField? env s.structName fieldName with
|
|
|
| some substructName =>
|
|
|
let substruct := Struct.mk s.ref substructName #[] substructFields s.source
|
|
|
let substruct ← expandStruct substruct
|
|
|
pure { field with lhs := [field.lhs.head!], val := FieldVal.nested substruct }
|
|
|
| none =>
|
|
|
let updateSource (structStx : Syntax) : TermElabM Syntax := do
|
|
|
let sourcesNew ← s.source.explicit.filterMapM
|
|
|
fun source => mkProjStx? source.stx source.structName fieldName
|
|
|
let explicitSourceStx := if sourcesNew.isEmpty then mkNullNode
|
|
|
else mkSourcesWithSyntax sourcesNew
|
|
|
let implicitSourceStx := s.source.implicit.map (·.stx) |>.getD mkNullNode
|
|
|
return (structStx.setArg 1 explicitSourceStx).setArg 3 implicitSourceStx
|
|
|
let valStx := s.ref -- construct substructure syntax using s.ref as template
|
|
|
let valStx := valStx.setArg 4 mkNullNode -- erase optional expected type
|
|
|
let args := substructFields.toArray.map (·.toSyntax)
|
|
|
let valStx := valStx.setArg 2 (mkNullNode <| mkSepArray args (mkAtom ","))
|
|
|
let valStx ← updateSource valStx
|
|
|
return { field with lhs := [field.lhs.head!], val := FieldVal.term valStx }
|
|
|
|
|
|
/--
|
|
|
Add `val : FieldVal`s to fields as specified by the sources.
|
|
|
If a value is found in the explicit sources (prior to `with`), add it as a `.term` or a
|
|
|
`.nested` `FieldVal`, as appropriate. If not, check for `..`, and make a hole via syntax as a
|
|
|
`.term`. Otherwise, mark the field as as `.missing`.
|
|
|
-/
|
|
|
private partial def addMissingFields (s : Struct) : TermElabM Struct := do
|
|
|
let env ← getEnv
|
|
|
let fieldNames := getStructureFields env s.structName
|
|
|
let ref := s.ref.mkSynthetic
|
|
|
withRef ref do
|
|
|
let fields ← fieldNames.foldlM (init := []) fun fields fieldName => do
|
|
|
match findField? s.fields fieldName with
|
|
|
| some field => return field::fields
|
|
|
| none =>
|
|
|
let addField (val : FieldVal Struct) : TermElabM Fields := do
|
|
|
return { ref, lhs := [FieldLHS.fieldName ref fieldName], val := val } :: fields
|
|
|
match Lean.isSubobjectField? env s.structName fieldName with
|
|
|
| some substructName =>
|
|
|
-- If one of the sources has the subobject field, use it
|
|
|
if let some val ← s.source.explicit.findSomeM?
|
|
|
fun source => mkProjStx? source.stx source.structName fieldName
|
|
|
then
|
|
|
addField (FieldVal.term val)
|
|
|
else
|
|
|
let substruct := Struct.mk ref substructName #[] [] s.source
|
|
|
let substruct ← expandStruct substruct
|
|
|
addField (FieldVal.nested substruct)
|
|
|
| none =>
|
|
|
if let some val ← s.source.explicit.findSomeM?
|
|
|
fun source => mkProjStx? source.stx source.structName fieldName
|
|
|
then
|
|
|
addField (FieldVal.term val)
|
|
|
else
|
|
|
-- Use hole syntax as a term in the natural, no-defaults (`..`) case;
|
|
|
-- otherwise mark it as a missing field.
|
|
|
match s.source.implicit with
|
|
|
| some { isSynthetic := false, useDefaults := false, .. } =>
|
|
|
addField (FieldVal.term (mkHole ref))
|
|
|
| _ => addField FieldVal.missing
|
|
|
return s.setFields fields.reverse
|
|
|
|
|
|
/-- Put the `Struct` into canonical form by expanding different ways of specifying fields
|
|
|
(composite, by index, subobject); group fields by subobject; and incorporate values (or
|
|
|
holes) sources. -/
|
|
|
private partial def expandStruct (s : Struct) : TermElabM Struct := do
|
|
|
let s := expandCompositeFields s
|
|
|
let s ← expandNumLitFields s
|
|
|
let s ← expandParentFields s
|
|
|
let s ← groupFields s
|
|
|
addMissingFields s
|
|
|
|
|
|
end
|
|
|
|
|
|
/-- Information about the constructor. -/
|
|
|
structure CtorHeaderResult where
|
|
|
/-- The constructor function itself as an `Expr`. -/
|
|
|
ctorFn : Expr
|
|
|
/-- The type of the constructor as an `Expr`. -/
|
|
|
ctorFnType : Expr
|
|
|
/-- Metavariables for instances. -/
|
|
|
instMVars : Array MVarId
|
|
|
/-- Named parameters encountered in bindings of the type and the expressions used for them. -/
|
|
|
params : Array (Name × Expr)
|
|
|
|
|
|
/-- Helper function that processes the constructor and its type until its first parameter reaches 0.
|
|
|
-/
|
|
|
private def mkCtorHeaderAux :
|
|
|
Nat → Expr → Expr → Array MVarId → Array (Name × Expr) → TermElabM CtorHeaderResult
|
|
|
| 0, type, ctorFn, instMVars, params =>
|
|
|
return { ctorFn , ctorFnType := type, instMVars, params }
|
|
|
| n+1, type, ctorFn, instMVars, params => do
|
|
|
match (← whnfForall type) with
|
|
|
| .forallE paramName d b c =>
|
|
|
match c with
|
|
|
| .instImplicit =>
|
|
|
let a ← mkFreshExprMVar d .synthetic
|
|
|
mkCtorHeaderAux n (b.instantiate1 a) (mkApp ctorFn a) (instMVars.push a.mvarId!)
|
|
|
(params.push (paramName, a))
|
|
|
| _ =>
|
|
|
let a ← mkFreshExprMVar d
|
|
|
mkCtorHeaderAux n (b.instantiate1 a) (mkApp ctorFn a) instMVars (params.push (paramName, a))
|
|
|
| _ => throwError "unexpected constructor type"
|
|
|
|
|
|
/-- Burrows into the body of a `.forallE` expression `n` times if possible, and returns the result.
|
|
|
If an expression not of the form `.forallE` is encountered along the way, return `none`. -/
|
|
|
private partial def getForallBody : Nat → Expr → Option Expr
|
|
|
| i+1, .forallE _ _ b _ => getForallBody i b
|
|
|
| _+1, _ => none
|
|
|
| 0, type => type
|
|
|
|
|
|
/-- When the expected type is known, attempt to get the type of the constructor by stripping `n`
|
|
|
`.forallE`'s off of the expression and then assigning metavariables by `isDefEq`'ing with
|
|
|
the expected type. -/
|
|
|
private def propagateExpectedType (type : Expr) (numFields : Nat) (expectedType? : Option Expr) :
|
|
|
TermElabM Unit := do
|
|
|
match expectedType? with
|
|
|
| none => return ()
|
|
|
| some expectedType =>
|
|
|
match getForallBody numFields type with
|
|
|
| none => pure ()
|
|
|
| some typeBody =>
|
|
|
unless typeBody.hasLooseBVars do
|
|
|
discard <| isDefEq expectedType typeBody
|
|
|
|
|
|
/-- Process information about a given `ConstructorVal`. -/
|
|
|
private def mkCtorHeader (ctorVal : ConstructorVal) (expectedType? : Option Expr) :
|
|
|
TermElabM CtorHeaderResult := do
|
|
|
let us ← mkFreshLevelMVars ctorVal.levelParams.length
|
|
|
let val := Lean.mkConst ctorVal.name us
|
|
|
let type ← instantiateTypeLevelParams (ConstantInfo.ctorInfo ctorVal) us
|
|
|
let r ← mkCtorHeaderAux ctorVal.numParams type val #[] #[]
|
|
|
propagateExpectedType r.ctorFnType ctorVal.numFields expectedType?
|
|
|
synthesizeAppInstMVars r.instMVars r.ctorFn
|
|
|
return r
|
|
|
|
|
|
/-- Annotate an expression to indicate that it must be synthesized as a default value.
|
|
|
In practice, the expression is a metavariable. -/
|
|
|
def markDefaultMissing (e : Expr) : Expr :=
|
|
|
mkAnnotation `structInstDefault e
|
|
|
|
|
|
/-- Check if an expression has been annotated in a way that indicates it should be synthesized
|
|
|
during the default loop. -/
|
|
|
def defaultMissing? (e : Expr) : Option Expr :=
|
|
|
annotation? `structInstDefault e
|
|
|
|
|
|
/-- Provide a descriptive error message if the structure instance elaboration fails. -/
|
|
|
def throwFailedToElabField {α} (fieldName : Name) (structName : Name) (msgData : MessageData) :
|
|
|
TermElabM α :=
|
|
|
throwError "failed to elaborate field '{fieldName}' of '{structName}, {msgData}"
|
|
|
|
|
|
/-- Attempt to synthesize an -/
|
|
|
def trySynthStructInstance? (s : Struct) (expectedType : Expr) : TermElabM (Option Expr) := do
|
|
|
if !s.allMissing then
|
|
|
return none
|
|
|
else
|
|
|
try synthInstance? expectedType catch _ => return none
|
|
|
|
|
|
-- By Mario Carneiro
|
|
|
/-- Use an expression in syntax. Example: ``(foo $(← toSyntax e))`.
|
|
|
This works by creating syntax for a metavariable, then elaborating that syntax and assigning
|
|
|
the metavariable to the expression in question.
|
|
|
-/
|
|
|
def toSyntax (e : Expr) (type? : Option Expr := none) : TermElabM Syntax := withFreshMacroScope do
|
|
|
let stx ← `(?a)
|
|
|
let mvar ← elabTerm stx type?
|
|
|
mvar.mvarId!.assign e
|
|
|
pure stx
|
|
|
|
|
|
/--
|
|
|
The result of running `elabStruct` on a `Struct`, containing:
|
|
|
* `struct : Struct`, now with updated `expr?` values in its fields, representing the values for
|
|
|
those fields.
|
|
|
* `val : Expr`, the constructor applied to the field values (`expr?`s). This is the actual
|
|
|
expression that the structure instance elaborates to. (Note that this is distinct from the
|
|
|
`val` of each field, which is a `FieldVal`.)
|
|
|
* `instMVars : Array MVarId`, used forkeeping track of instances.
|
|
|
-/
|
|
|
structure ElabStructResult where
|
|
|
/-- The structure's constructor applied to the field values (`expr?`s). This is the actual
|
|
|
expression that the structure instance elaborates to. -/
|
|
|
val : Expr
|
|
|
/-- The `struct` that was fed to `elabStruct`, but now with updated `expr?` values for all of its
|
|
|
fields containing their values as expressions. -/
|
|
|
struct : Struct
|
|
|
/-- Used for keeping track of instances. -/
|
|
|
instMVars : Array MVarId
|
|
|
|
|
|
/--
|
|
|
Elaborates a `Struct` into an `ElabStructResult`.
|
|
|
This computes expressions for all fields of a structure (in `expr?`) on the basis of `FieldVal`s
|
|
|
while simultaneously building the elaboration of the structure instance itself, in the form of
|
|
|
its constructor applied to the expressions for each of its fields in turn.
|
|
|
`.term stx` `FieldVals` are elaborated while ensuring the type (as given by the constructor's
|
|
|
type), `.nested s` `FieldVals` are recursed into. `.missing` `FieldVals` are replaced with
|
|
|
metavariables and annotated to indicate that they will get assigned during the default synthesis
|
|
|
loop. Note that in this case the same metavariable is used both in the `expr?` field and the
|
|
|
final constructed expression (`val`), so that assigning it gives access to the value in both
|
|
|
places. The one exception is if an `autoParam` is encountered in the type, in which case the
|
|
|
tactic is elaborated.
|
|
|
-/
|
|
|
private partial def elabStruct (s : Struct) (expectedType? : Option Expr) :
|
|
|
TermElabM ElabStructResult := withRef s.ref do
|
|
|
let env ← getEnv
|
|
|
let vhc? := s.source.implicit
|
|
|
let ctorVal := getStructureCtor env s.structName
|
|
|
if isPrivateNameFromImportedModule env ctorVal.name then
|
|
|
throwError "invalid \{...} notation, constructor for `{s.structName}` is marked as private"
|
|
|
-- We store the parameters at the resulting `Struct`.
|
|
|
-- We use this information during default value propagation.
|
|
|
let { ctorFn, ctorFnType, params, .. } ← mkCtorHeader ctorVal expectedType?
|
|
|
let (e, _, fields, instMVars) ← s.fields.foldlM
|
|
|
(init := (ctorFn, ctorFnType, [], #[]))
|
|
|
fun (e, type, fields, instMVars) field => do
|
|
|
match field.lhs with
|
|
|
| [.fieldName ref fieldName] =>
|
|
|
let type ← whnfForall type
|
|
|
trace[Elab.struct] "elabStruct {field}, {type}"
|
|
|
match type with
|
|
|
| .forallE _ d b bi =>
|
|
|
let cont (val : Expr) (field : Field Struct) (instMVars := instMVars)
|
|
|
(updateField := true) : TermElabM (Expr × Expr × Fields × Array MVarId) := do
|
|
|
pushInfoTree <| InfoTree.node (children := {}) <| Info.ofFieldInfo {
|
|
|
projName := s.structName.append fieldName,
|
|
|
fieldName,
|
|
|
lctx := (← getLCtx),
|
|
|
val,
|
|
|
stx := ref }
|
|
|
let e := mkApp e val
|
|
|
let type := b.instantiate1 val
|
|
|
let field := if updateField then { field with expr? := some val } else field
|
|
|
return (e, type, field::fields, instMVars)
|
|
|
match field.val with
|
|
|
| .term stx =>
|
|
|
cont (← elabTermEnsuringType stx d.consumeTypeAnnotations) field
|
|
|
| .nested s =>
|
|
|
let inst? := if vhc?.all (·.useDefaults) then
|
|
|
(← trySynthStructInstance? s d) else none
|
|
|
match inst? with
|
|
|
| some val =>
|
|
|
cont val { field with val := FieldVal.term (mkHole field.ref) }
|
|
|
| none =>
|
|
|
let { val, struct := sNew, instMVars := instMVarsNew } ← elabStruct s (some d)
|
|
|
let val ← ensureHasType d val
|
|
|
cont val { field with val := FieldVal.nested sNew } (instMVars ++ instMVarsNew)
|
|
|
| .missing =>
|
|
|
match d.getAutoParamTactic? with
|
|
|
| some (.const tacticDecl ..) =>
|
|
|
let d := (d.getArg! 0).consumeTypeAnnotations
|
|
|
if vhc?.all (·.useDefaults) then
|
|
|
match evalSyntaxConstant env (← getOptions) tacticDecl with
|
|
|
| .error err => throwError err
|
|
|
| .ok tacticSyntax =>
|
|
|
if vhc?.isSome then
|
|
|
let val := (← mkFreshExprMVar (some d) .synthetic)
|
|
|
let stx ← `(by first | $tacticSyntax | exact $(← toSyntax val))
|
|
|
cont (← elabTermEnsuringType stx d)
|
|
|
{field with expr? := some (markDefaultMissing val)}
|
|
|
(updateField := false)
|
|
|
else
|
|
|
let stx ← `(by $tacticSyntax)
|
|
|
cont (← elabTermEnsuringType stx d) field
|
|
|
else
|
|
|
let val ← withRef field.ref <| mkFreshExprMVar (some d)
|
|
|
cont (markDefaultMissing val) field
|
|
|
| _ =>
|
|
|
if bi == .instImplicit then
|
|
|
let val ← withRef field.ref <| mkFreshExprMVar d .synthetic
|
|
|
trace[Elab.struct] ".instImplicit ({val})"
|
|
|
cont val field (instMVars.push val.mvarId!)
|
|
|
else
|
|
|
let val ← withRef field.ref <| mkFreshExprMVar (some d)
|
|
|
cont (markDefaultMissing val) field
|
|
|
| _ => withRef field.ref (throwFailedToElabField
|
|
|
fieldName s.structName m!"unexpected constructor type{indentExpr type}")
|
|
|
| _ => throwErrorAt field.ref "unexpected unexpanded structure field"
|
|
|
return { val := e, struct := s.setFields fields.reverse |>.setParams params, instMVars }
|
|
|
|
|
|
namespace ImplicitFields
|
|
|
|
|
|
/-- Updated as we search for default values. We must search for default values overriden in derived
|
|
|
structures. -/
|
|
|
structure Context where
|
|
|
/-- `Struct`s in the context which might supply default values. -/
|
|
|
structs : Array Struct := #[]
|
|
|
/-- The names of structures in the context which might supply default values. -/
|
|
|
allStructNames : Array Name := #[]
|
|
|
/--
|
|
|
Consider the following example:
|
|
|
```
|
|
|
structure A where
|
|
|
x : Nat := 1
|
|
|
structure B extends A where
|
|
|
y : Nat := x + 1
|
|
|
x := y + 1
|
|
|
structure C extends B where
|
|
|
z : Nat := 2*y
|
|
|
x := z + 3
|
|
|
```
|
|
|
And we are trying to elaborate a structure instance for `C`.
|
|
|
There are default values for `x` at `A`, `B`, and `C`.
|
|
|
We say the default value at `C` has distance 0, the one at `B` distance 1, and the one at `A`
|
|
|
distance 2.
|
|
|
The field `maxDistance` specifies the maximum distance considered in a round of Default field
|
|
|
computation.
|
|
|
Remark: since `C` does not set a default value of `y`, the default value at `B` is at distance 0.
|
|
|
The fixpoint for setting default values works in the following way.
|
|
|
- Keep computing default values using `maxDistance == 0`.
|
|
|
- We increase `maxDistance` whenever we failed to compute a new default value in a round.
|
|
|
- If `maxDistance > 0`, then we interrupt a round as soon as we compute some default value.
|
|
|
We use depth-first search.
|
|
|
- We sign an error if no progress is made when `maxDistance` == structure hierarchy depth (2 in
|
|
|
the example above).
|
|
|
-/
|
|
|
maxDistance : Nat := 0
|
|
|
|
|
|
/-- Stores an indicator of whether progress has been made during a round in the default loop. -/
|
|
|
structure State where
|
|
|
/-- Indicates whether progress has been made during a round in the default loop. -/
|
|
|
progress : Bool := false
|
|
|
|
|
|
/-- Collects the names of all nested structures in a `Struct` (at any depth), including the name of
|
|
|
the structure itself. -/
|
|
|
partial def collectStructNames (struct : Struct) (names : Array Name) : Array Name :=
|
|
|
let names := names.push struct.structName
|
|
|
struct.fields.foldl (init := names) fun names field =>
|
|
|
match field.val with
|
|
|
| .nested struct => collectStructNames struct names
|
|
|
| _ => names
|
|
|
|
|
|
/-- Gets the maximum depth at which any structure is nested within the given structure, i.e. the
|
|
|
height of its subobject poset. -/
|
|
|
partial def getHierarchyDepth (struct : Struct) : Nat :=
|
|
|
struct.fields.foldl (init := 0) fun max field =>
|
|
|
match field.val with
|
|
|
| .nested struct => Nat.max max (getHierarchyDepth struct + 1)
|
|
|
| _ => max
|
|
|
|
|
|
/-- (Monadic) Checks if the value of a field (`expr?`) is an unassigned metavariable that is
|
|
|
annotated to indicate that it should be synthesized during the default loop. -/
|
|
|
def isDefaultMissing? [Monad m] [MonadMCtx m] (field : Field Struct) : m Bool := do
|
|
|
if let some expr := field.expr? then
|
|
|
if let some (.mvar mvarId) := defaultMissing? expr then
|
|
|
unless (← mvarId.isAssigned) do
|
|
|
return true
|
|
|
return false
|
|
|
|
|
|
/-- (Monadic) Gets the first encountered field in a `Struct` whose value (`expr?`) is an unassigned
|
|
|
metavariable that is annotated to indicate that it should be synthesized during the default
|
|
|
loop. -/
|
|
|
partial def findDefaultMissing? [Monad m] [MonadMCtx m] (struct : Struct) :
|
|
|
m (Option (Field Struct)) :=
|
|
|
struct.fields.findSomeM? fun field => do
|
|
|
match field.val with
|
|
|
| .nested struct => findDefaultMissing? struct
|
|
|
| _ => return if (← isDefaultMissing? field) then field else none
|
|
|
|
|
|
/-- (Monadic) Gets an array containing all fields in the `Struct` whose value (`expr?`) is an
|
|
|
unassigned metavariable that is annotated to indicate that it should be synthesized during the
|
|
|
default loop. -/
|
|
|
partial def allDefaultMissing [Monad m] [MonadMCtx m] (struct : Struct) :
|
|
|
m (Array (Field Struct)) :=
|
|
|
go struct *> get |>.run' #[]
|
|
|
where
|
|
|
/-- Loop through all fields in the `Struct`, recursing if a `.nested` one is found, and storing
|
|
|
the field in a mutable array if it `isDefaultMissing?` -/
|
|
|
go (struct : Struct) : StateT (Array (Field Struct)) m Unit :=
|
|
|
for field in struct.fields do
|
|
|
if let .nested struct := field.val then
|
|
|
go struct
|
|
|
else if (← isDefaultMissing? field) then
|
|
|
modify (·.push field)
|
|
|
|
|
|
/-- Gets the name of a field, assuming that its `lhs` is of the form `[.fieldName _ fieldName]`.
|
|
|
Panics otherwise. -/
|
|
|
def getFieldName (field : Field Struct) : Name :=
|
|
|
match field.lhs with
|
|
|
| [.fieldName _ fieldName] => fieldName
|
|
|
| _ => unreachable!
|
|
|
|
|
|
/-- Abbreviation for `ReaderT Context (StateRefT State TermElabM)`: A monad transformation of
|
|
|
`TermElabM` that lets us access the `Context` (relevant for checking if default values are
|
|
|
overridden) and keeping track of whether progress has been made during a round of the default
|
|
|
loop (`State`). -/
|
|
|
abbrev M := ReaderT Context (StateRefT State TermElabM)
|
|
|
|
|
|
/-- Checks if the round has completed by checking that progress has been made and that the
|
|
|
`maxDistance > 0`. -/
|
|
|
def isRoundDone : M Bool := do
|
|
|
return (← get).progress && (← read).maxDistance > 0
|
|
|
|
|
|
/-- Gets the value (`expr?`) of a field in a `Struct` given the name of the field. -/
|
|
|
def getFieldValue? (struct : Struct) (fieldName : Name) : Option Expr :=
|
|
|
struct.fields.findSome? fun field =>
|
|
|
if getFieldName field == fieldName then
|
|
|
field.expr?
|
|
|
else
|
|
|
none
|
|
|
|
|
|
section NamedGoalsWithMetadata
|
|
|
/-- A convenient representation of the metadata attached to named goals produced by `?..` syntax. -/
|
|
|
structure FieldHoleMData where
|
|
|
/-- The index of the named goal used for name conflict resolution when dealing with multiple
|
|
|
occcurrences of `?..`. Each conflicting use of `?..` should generate field holes with
|
|
|
different indices. An index of `0` indicates that no name conflicts were found with any
|
|
|
existing goals. -/
|
|
|
index : Nat
|
|
|
/-- The syntax of the structure instance that contained the `?..` syntax. -/
|
|
|
structRef : Syntax
|
|
|
/-- The name of the structure that contained the `?..` syntax. -/
|
|
|
structName : Name
|
|
|
/-- The name of the field this goal represents. -/
|
|
|
fieldName : Name
|
|
|
/-- The name to be prefixed to the name of this goal. `Name.anonymous` indicates that no name is
|
|
|
to be prefixed. -/
|
|
|
prefixName : Name
|
|
|
|
|
|
/-- Creates the metadata for a field's named goal given the field, the `Struct`, and the
|
|
|
conflict-resolution index. -/
|
|
|
def mkFieldHoleMData (index : Nat) (field : Field Struct) (struct : Struct) : FieldHoleMData :=
|
|
|
{
|
|
|
index,
|
|
|
structRef := struct.ref
|
|
|
structName := struct.structName
|
|
|
fieldName := getFieldName field
|
|
|
prefixName := match struct.source.implicit with
|
|
|
| some {name := some prefixName, ..} => prefixName
|
|
|
| _ => Name.anonymous
|
|
|
}
|
|
|
|
|
|
open KVMap in
|
|
|
/-- Gets the field hole metadata from a metavariable if present. -/
|
|
|
def getFieldHoleMDataFromMVar? (decl : MetavarDecl) : Option FieldHoleMData :=
|
|
|
match decl.type with
|
|
|
| .mdata md _ =>
|
|
|
if getBool md `fieldHole then
|
|
|
some
|
|
|
{
|
|
|
index := getNat md `index
|
|
|
structRef := getSyntax md `structRef
|
|
|
structName := getName md `structName
|
|
|
fieldName := getName md `fieldName
|
|
|
prefixName := getName md `prefixName
|
|
|
}
|
|
|
else none
|
|
|
| _ => none
|
|
|
|
|
|
/-- Checks if a metavariable decl is a named field hole created by `?..` syntax. -/
|
|
|
def isFieldHole (decl : MetavarDecl) : Bool :=
|
|
|
match decl.type with
|
|
|
| .mdata md _ => KVMap.getBool md `fieldHole
|
|
|
| _ => false
|
|
|
|
|
|
section KVMap
|
|
|
/-- Merges two `KVMap`s, overwriting the values of any shared keys with those in the second `KVMap`
|
|
|
-/
|
|
|
def mergeKVMap : KVMap → KVMap → KVMap :=
|
|
|
fun m₀ m₁ => Id.run do
|
|
|
let mut m := m₀
|
|
|
for (name, data) in m₁ do
|
|
|
m := KVMap.insert m name data
|
|
|
return m
|
|
|
|
|
|
/-- Turns a list of key-value pairs (e.g. ``[(`a, ofBool true), (`b, ofNat 2), ...]``) into a
|
|
|
`KVMap`. -/
|
|
|
def toKVMap : List (Name × DataValue) → KVMap
|
|
|
| l => l.foldl (fun m (n, d) => KVMap.insert m n d) {}
|
|
|
|
|
|
end KVMap
|
|
|
|
|
|
open DataValue in
|
|
|
/-- Turns a representation of field hole metadata into actual metadata (a `KVMap`). -/
|
|
|
def mkFieldHoleMDataKVMap (f : FieldHoleMData) : KVMap :=
|
|
|
toKVMap [
|
|
|
(`fieldHole , ofBool true ),
|
|
|
(`index , ofNat f.index ),
|
|
|
(`structRef , ofSyntax f.structRef ),
|
|
|
(`structName , ofName f.structName),
|
|
|
(`fieldName , ofName f.fieldName ),
|
|
|
(`prefixName , ofName f.prefixName)
|
|
|
]
|
|
|
|
|
|
/--
|
|
|
Create a metavariable with `metadata` attached to its `type`.
|
|
|
If there's any existing metadata on `type`, `metadata` is preferentially merged into it.
|
|
|
-/
|
|
|
def mkFreshExprMVarWithMData (type : Expr) (metadata : KVMap) (kind : MetavarKind := default)
|
|
|
(userName := Name.anonymous) : MetaM Expr :=
|
|
|
let annotatedType :=
|
|
|
match type with
|
|
|
| .mdata m e =>
|
|
|
let merge := mergeKVMap m metadata
|
|
|
Expr.mdata merge e
|
|
|
| _ =>
|
|
|
Expr.mdata metadata type
|
|
|
mkFreshExprMVar annotatedType (kind := kind) (userName := userName)
|
|
|
|
|
|
/-- Make a fresh expression metavariable for a field, named accordingly, and with metadata
|
|
|
attached. -/
|
|
|
def mkFreshFieldNamedMVar (type : Expr) (index : Nat) (prefixName : Option Name)
|
|
|
(field : Field Struct) (struct : Struct) : MetaM Expr :=
|
|
|
let fieldHoleMData := mkFieldHoleMDataKVMap <| mkFieldHoleMData index field struct
|
|
|
let name :=
|
|
|
match prefixName with
|
|
|
| some x => x ++ (getFieldName field)
|
|
|
| none => getFieldName field
|
|
|
let name := if index == 0 then name else name.appendIndexAfter index
|
|
|
mkFreshExprMVarWithMData type fieldHoleMData (kind := .syntheticOpaque) (userName := name)
|
|
|
|
|
|
/-- Given the names of two structures, check if they have any field names in common. -/
|
|
|
def fieldsOverlap (env : Environment) (structName₀ : Name) (structName₁ : Name) : Bool :=
|
|
|
let fields₀ := getStructureFieldsFlattened env structName₀ false
|
|
|
let fields₁ := getStructureFieldsFlattened env structName₁ false
|
|
|
fields₀.any (fun field => fields₁.contains field)
|
|
|
|
|
|
-- Monadic to enable tracing.
|
|
|
/-- If the provided metavariable decl is a named field hole created by `?..` syntax, check if it
|
|
|
conflicts with the current structure and prefix name. If so, return its index. Otherwise,
|
|
|
return `none`. -/
|
|
|
def getConflictingIndex? (env : Environment) (s : Struct) (prefixName : Name) (decl : MetavarDecl)
|
|
|
: TermElabM (Option Nat) := do
|
|
|
let fieldHoleMData? := getFieldHoleMDataFromMVar? decl
|
|
|
match fieldHoleMData? with
|
|
|
| some fieldHoleMData =>
|
|
|
let cond2 := prefixName == fieldHoleMData.prefixName
|
|
|
let cond3 := fieldsOverlap env s.structName (fieldHoleMData.structName)
|
|
|
trace[Elab.struct]
|
|
|
"goal name conflict for {fieldHoleMData.structName}: {cond2} && {cond3}"
|
|
|
if cond2 && cond3
|
|
|
then return some fieldHoleMData.index
|
|
|
else return none
|
|
|
| none => return none
|
|
|
|
|
|
/-- Get the next non-conflicting index among all metavariable conflicts.
|
|
|
A metavariable conflicts iff all of the following are true:
|
|
|
* it is a named field hole created by `?..` syntax
|
|
|
* it is not from the same occurrence of `?..`
|
|
|
* it has the same prefix name (possibly `Name.anonymous` if it does not have a prefix)
|
|
|
* it belongs to a structure that has field names in common with the current structure
|
|
|
Note that this gets the index one greater than the maximum conflicting index, not the next
|
|
|
"available" index. We take a "wide berth" approach to avoid situations where it might appear
|
|
|
like two goals are from the same occurrence of `?..` despite this not being the case. -/
|
|
|
def nextIndexGivenCollisions (env : Environment) (mctx : MetavarContext) (s : Struct)
|
|
|
: TermElabM Nat := do
|
|
|
let prefixName := match s.source.implicit with
|
|
|
| some { name := some prefixName, .. } => prefixName
|
|
|
| _ => Name.anonymous
|
|
|
let conflictingIndex : (Option Nat) ← mctx.decls.foldl
|
|
|
(fun i? _ decl => do
|
|
|
let i'? ← getConflictingIndex? env s prefixName decl
|
|
|
return (Option.merge max (← i?) i'?)) (pure none)
|
|
|
match conflictingIndex with
|
|
|
| some i => return i+1
|
|
|
| none => return 0
|
|
|
|
|
|
/-- Assign all fields which did not get synthesized during the default loop (but which were marked
|
|
|
as such) to appropriately-named field holes with metadata in the case of `?..` syntax (and to
|
|
|
natural holes when the `?` is absent). -/
|
|
|
def assignRemainingDefaultsToFieldHoles (struct : Struct) : TermElabM Unit :=
|
|
|
withRef struct.ref do
|
|
|
match struct.source.implicit with
|
|
|
| some vhc =>
|
|
|
let index ← nextIndexGivenCollisions (← getEnv) (← getMCtx) struct
|
|
|
for field in (← allDefaultMissing struct) do
|
|
|
match field.expr? with
|
|
|
| some expr =>
|
|
|
match defaultMissing? expr with
|
|
|
| some (.mvar mvarId) =>
|
|
|
let type := (← getMVarDecl mvarId).type
|
|
|
if vhc.isSynthetic then
|
|
|
mvarId.assign (← withRef field.ref <|
|
|
|
mkFreshFieldNamedMVar type index vhc.name field struct)
|
|
|
else
|
|
|
let newHole ← withRef field.ref <| mkFreshExprMVar type (kind := .natural)
|
|
|
mvarId.assign newHole
|
|
|
registerMVarErrorHoleInfo newHole.mvarId! struct.ref
|
|
|
| _ => unreachable!
|
|
|
| none => unreachable!
|
|
|
| none => return ()
|
|
|
|
|
|
end NamedGoalsWithMetadata
|
|
|
/-- A helper function that applies lambdas whose parameters are field names to the corresponding
|
|
|
field values until it finds a non-lambda, using propagated parameters instead of field names if
|
|
|
necessary along the way. Returns `none` if it finds a lambda that's not of this form. -/
|
|
|
partial def mkDefaultValueAux? (struct : Struct) : Expr → TermElabM (Option Expr)
|
|
|
| .lam n d b c => withRef struct.ref do
|
|
|
if c.isExplicit then
|
|
|
let fieldName := n
|
|
|
match getFieldValue? struct fieldName with
|
|
|
| none => return none
|
|
|
| some val =>
|
|
|
let valType ← inferType val
|
|
|
if (← isDefEq valType d) then
|
|
|
mkDefaultValueAux? struct (b.instantiate1 val)
|
|
|
else
|
|
|
return none
|
|
|
else
|
|
|
if let some (_, param) := struct.params.find? fun (paramName, _) => paramName == n then
|
|
|
-- Recall that we did not use to have support for parameter propagation here.
|
|
|
if (← isDefEq (← inferType param) d) then
|
|
|
mkDefaultValueAux? struct (b.instantiate1 param)
|
|
|
else
|
|
|
return none
|
|
|
else
|
|
|
let arg ← mkFreshExprMVar d
|
|
|
mkDefaultValueAux? struct (b.instantiate1 arg)
|
|
|
| e =>
|
|
|
if e.isAppOfArity ``id 2 then
|
|
|
return some e.appArg!
|
|
|
else
|
|
|
return some e
|
|
|
|
|
|
/-- If possible, make a default value by applying lambdas in the given constant to the appropriate
|
|
|
field values or propagated parameter values. -/
|
|
|
def mkDefaultValue? (struct : Struct) (cinfo : ConstantInfo) : TermElabM (Option Expr) :=
|
|
|
withRef struct.ref do
|
|
|
let us ← mkFreshLevelMVarsFor cinfo
|
|
|
mkDefaultValueAux? struct (← instantiateValueLevelParams cinfo us)
|
|
|
|
|
|
/-- Reduce default value. It performs beta reduction and projections of the given structures. -/
|
|
|
partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
|
|
|
match e with
|
|
|
| .lam .. => lambdaLetTelescope e fun xs b => do mkLambdaFVars xs (← reduce structNames b)
|
|
|
| .forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← reduce structNames b)
|
|
|
| .letE .. => lambdaLetTelescope e fun xs b => do mkLetFVars xs (← reduce structNames b)
|
|
|
| .proj _ i b =>
|
|
|
match (← Meta.project? b i) with
|
|
|
| some r => reduce structNames r
|
|
|
| none => return e.updateProj! (← reduce structNames b)
|
|
|
| .app f .. =>
|
|
|
match (← reduceProjOf? e structNames.contains) with
|
|
|
| some r => reduce structNames r
|
|
|
| none =>
|
|
|
let f := f.getAppFn
|
|
|
let f' ← reduce structNames f
|
|
|
if f'.isLambda then
|
|
|
let revArgs := e.getAppRevArgs
|
|
|
reduce structNames (f'.betaRev revArgs)
|
|
|
else
|
|
|
let args ← e.getAppArgs.mapM (reduce structNames)
|
|
|
return mkAppN f' args
|
|
|
| .mdata _ b =>
|
|
|
let b ← reduce structNames b
|
|
|
if (defaultMissing? e).isSome && !b.isMVar then
|
|
|
return b
|
|
|
else
|
|
|
return e.updateMData! b
|
|
|
| .mvar mvarId =>
|
|
|
match (← getExprMVarAssignment? mvarId) with
|
|
|
| some val => if val.isMVar then pure val else reduce structNames val
|
|
|
| none => return e
|
|
|
| e => return e
|
|
|
|
|
|
/--
|
|
|
Attempt to synthesize the default value for a field, looping through nested structures if
|
|
|
necessary. If a default value is found, assign it to the metavariable that we created for the
|
|
|
field's value back in `elabStruct`, and return `true`. Otherwise return `false`.
|
|
|
-/
|
|
|
partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Array Name)
|
|
|
(maxDistance : Nat) (fieldName : Name) (mvarId : MVarId) : TermElabM Bool :=
|
|
|
let rec loop (i : Nat) (dist : Nat) := do
|
|
|
if dist > maxDistance then
|
|
|
return false
|
|
|
else if h : i < structs.size then
|
|
|
let struct := structs.get ⟨i, h⟩
|
|
|
match getDefaultFnForField? (← getEnv) struct.structName fieldName with
|
|
|
| some defFn =>
|
|
|
let cinfo ← getConstInfo defFn
|
|
|
let mctx ← getMCtx
|
|
|
match (← mkDefaultValue? struct cinfo) with
|
|
|
| none => setMCtx mctx; loop (i+1) (dist+1)
|
|
|
| some val =>
|
|
|
let val ← reduce allStructNames val
|
|
|
match val.find? fun e => (defaultMissing? e).isSome with
|
|
|
| some _ => setMCtx mctx; loop (i+1) (dist+1)
|
|
|
| none =>
|
|
|
let mvarDecl ← getMVarDecl mvarId
|
|
|
let val ← ensureHasType mvarDecl.type val
|
|
|
mvarId.assign val
|
|
|
return true
|
|
|
| _ => loop (i+1) dist
|
|
|
else
|
|
|
return false
|
|
|
loop 0 0
|
|
|
|
|
|
/-- The main loop of `tryToSynthesizeDefault`, which keeps track of which struct out of an array of
|
|
|
all nested structs is being considered, as well as the distance to make sure it doesn't exceed
|
|
|
the `maxDistance` (see the documentation for `Context.maxDistance`). -/
|
|
|
add_decl_doc tryToSynthesizeDefault.loop
|
|
|
|
|
|
/--
|
|
|
A step within the default synthesis loop. We proceed only if the round is not done. We loop
|
|
|
through all fields in the structure, attempting to synthesize a default via
|
|
|
`tryToSynthesizeDefault` when possible. If we succeed, we set `progress := true` in the `State`.
|
|
|
Note: by now, all `expr?`s should be `some expr` from `elabStruct`, even if that `expr` is a
|
|
|
metavariable; as such, we panic if one of them is `none`.
|
|
|
-/
|
|
|
partial def step (struct : Struct) : M Unit :=
|
|
|
unless (← isRoundDone) do
|
|
|
withReader (fun ctx => { ctx with structs := ctx.structs.push struct }) do
|
|
|
for field in struct.fields do
|
|
|
match field.val with
|
|
|
| .nested struct => step struct
|
|
|
| _ => match field.expr? with
|
|
|
| none => unreachable!
|
|
|
| some expr =>
|
|
|
match defaultMissing? expr with
|
|
|
| some (.mvar mvarId) =>
|
|
|
unless (← mvarId.isAssigned) do
|
|
|
let ctx ← read
|
|
|
if (← withRef field.ref (tryToSynthesizeDefault
|
|
|
ctx.structs ctx.allStructNames ctx.maxDistance (getFieldName field) mvarId))
|
|
|
then
|
|
|
modify fun _ => { progress := true }
|
|
|
| _ => pure ()
|
|
|
|
|
|
/--
|
|
|
The workhorse of the default synthesis loop.
|
|
|
If there are no fields left that need to be synthesized during the default loop, we return from
|
|
|
the loop.
|
|
|
Otherwise, when we find a field that ought to be synthesized during the default loop, we take a
|
|
|
`step`. If we've made `progress`, we call `propagateLoop` again and reset the depth to `0`. If we
|
|
|
haven't, we call `propagateLoop` again with a higher depth.
|
|
|
If the depth ever exceeds the hierarchy depth, we know that we've searched all nested structures,
|
|
|
but no default values were to be found. In this case, we either throw an error with the missing
|
|
|
fields, or, if a variadic hole is present (e.g. `?..`), simply return from the loop (at which
|
|
|
point the remaining holes will be assigned by `assignRemainingDefaultsToFieldHoles` ).
|
|
|
-/
|
|
|
partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : Struct) : M Unit := do
|
|
|
match (← findDefaultMissing? struct) with
|
|
|
| none => return () -- Done
|
|
|
| some field =>
|
|
|
trace[Elab.struct] "propagate [{d}] [field := {field}]: {struct}"
|
|
|
if d > hierarchyDepth then
|
|
|
let missingFields := (← allDefaultMissing struct).map getFieldName
|
|
|
if struct.source.implicit.isSome then
|
|
|
return ()
|
|
|
else
|
|
|
let missingFieldsWithoutDefault :=
|
|
|
let env := (← getEnv)
|
|
|
let structs := (← read).allStructNames
|
|
|
missingFields.filter fun fieldName => structs.all fun struct =>
|
|
|
(getDefaultFnForField? env struct fieldName).isNone
|
|
|
let fieldsToReport :=
|
|
|
if missingFieldsWithoutDefault.isEmpty then missingFields else missingFieldsWithoutDefault
|
|
|
throwErrorAt field.ref
|
|
|
"fields missing: {fieldsToReport.toList.map (s!"'{·}'") |> ", ".intercalate}"
|
|
|
else withReader (fun ctx => { ctx with maxDistance := d }) do
|
|
|
modify fun _ => { progress := false }
|
|
|
step struct
|
|
|
if (← get).progress then
|
|
|
propagateLoop hierarchyDepth 0 struct
|
|
|
else
|
|
|
propagateLoop hierarchyDepth (d+1) struct
|
|
|
|
|
|
/--
|
|
|
The default synthesis loop.
|
|
|
We call our workhorse function `propagateLoop` with appropriate initial values, which implements
|
|
|
the loop itself (unless there is a variadic hole that specifies defaults are not to be used).
|
|
|
Then, if there is a variadic hole, we assign the remaining metavariables that couldn't be
|
|
|
synthesized into default values to (named) field holes.
|
|
|
-/
|
|
|
def propagate (struct : Struct) : TermElabM Unit := do
|
|
|
let hierarchyDepth := getHierarchyDepth struct
|
|
|
let structNames := collectStructNames struct #[]
|
|
|
let vhc? := struct.source.implicit
|
|
|
if vhc?.all (·.useDefaults) then
|
|
|
propagateLoop hierarchyDepth 0 struct { allStructNames := structNames } |>.run' {}
|
|
|
if vhc?.isSome then
|
|
|
assignRemainingDefaultsToFieldHoles struct
|
|
|
|
|
|
end ImplicitFields
|
|
|
|
|
|
/--
|
|
|
The main content of the elaboration, during which we normalize the `Struct`'s form, call
|
|
|
`elabStruct` to compute field values and construct the elaborated expression, run the default
|
|
|
synthesis loop (and provide named field holes if warranted), and synthesize instances. -/
|
|
|
private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (source : Source)
|
|
|
: TermElabM Expr := do
|
|
|
let structName ← getStructName expectedType? source
|
|
|
let struct ← liftMacroM <| mkStructView stx structName source
|
|
|
let struct ← expandStruct struct
|
|
|
trace[Elab.struct] "{struct}"
|
|
|
/- We try to synthesize pending problems with `withSynthesize` combinator before trying to use
|
|
|
default values.
|
|
|
This is important in examples such as
|
|
|
```
|
|
|
structure MyStruct where
|
|
|
{α : Type u}
|
|
|
{β : Type v}
|
|
|
a : α
|
|
|
b : β
|
|
|
#check { a := 10, b := true : MyStruct }
|
|
|
```
|
|
|
were the `α` will remain "unknown" until the default instance for `OfNat` is used to ensure
|
|
|
that `10` is a `Nat`.
|
|
|
TODO: investigate whether this design decision may have unintended side effects or produce
|
|
|
confusing behavior.
|
|
|
-/
|
|
|
let { val := r, struct, instMVars } ← withSynthesize (mayPostpone := true) <|
|
|
|
elabStruct struct expectedType?
|
|
|
trace[Elab.struct] "before propagate {r}"
|
|
|
ImplicitFields.propagate struct
|
|
|
synthesizeAppInstMVars instMVars r
|
|
|
return r
|
|
|
|
|
|
/-- The term elaborator for structure instance syntax that includes variadic holes (`?..`). -/
|
|
|
@[term_elab structInstWithHoles] def elabStructInstWithHoles : TermElab := fun stx expectedType? =>
|
|
|
do
|
|
|
match (← expandNonAtomicExplicitSources stx) with
|
|
|
| some stxNew => withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
|
|
|
| none =>
|
|
|
let sourceView ← getStructSource stx
|
|
|
if let some modifyOp ← isModifyOp? stx then
|
|
|
if sourceView.explicit.isEmpty then
|
|
|
throwError
|
|
|
"invalid \{...} notation, explicit source is required when using '[<index>] := <value>'"
|
|
|
elabModifyOp stx modifyOp sourceView.explicit expectedType?
|
|
|
else
|
|
|
elabStructInstAux stx expectedType? sourceView
|
|
|
|
|
|
section haveFieldProj
|
|
|
|
|
|
/-- `as foo` names the field projection `foo`. -/
|
|
|
declare_syntax_cat asname
|
|
|
/-- `as foo` names the field projection `foo`. -/
|
|
|
syntax "as" ident : asname
|
|
|
|
|
|
-- couldn't write elab "haveFieldProj" f:(ident)? x:("as" n:ident)? : tactic
|
|
|
/--
|
|
|
Once a goal has been created for a structure's field via `?..` syntax, `haveFieldProj` can be
|
|
|
used equivalently to `have <field name>.proj := <projection function>`.
|
|
|
`haveFieldProj f as a` gets the field projection for the field `f` and names it `a`;
|
|
|
`f` and `as a` can both be individually omitted.
|
|
|
-/
|
|
|
elab "haveFieldProj" f:(ident)? x:(asname)? : tactic => do
|
|
|
let fieldHoleMData? := ImplicitFields.getFieldHoleMDataFromMVar? (← Tactic.getMainDecl)
|
|
|
match fieldHoleMData? with
|
|
|
| some fieldHoleMData =>
|
|
|
let fieldName := match f with | some f' => f'.getId | none => fieldHoleMData.fieldName
|
|
|
let structName := fieldHoleMData.structName -- so the error fits on one line
|
|
|
let some projname :=
|
|
|
(getProjFnForField? (← getEnv) fieldHoleMData.structName fieldName) | throwError
|
|
|
"couldn't find projection function for field {fieldName} of structure {structName}"
|
|
|
let name := match x with
|
|
|
| some stx => match stx with
|
|
|
| `(asname|as $n:ident) => n
|
|
|
| _ => mkIdent (fieldName ++ `proj)
|
|
|
| none => mkIdent (fieldName ++ `proj)
|
|
|
Tactic.evalTactic (←`(tactic|have $name := $(mkIdent projname)))
|
|
|
| none => throwError "no field metadata found on the main goal"
|
|
|
|
|
|
end haveFieldProj
|