This PR puts code in terms of syntax quotations now that there has been a stage0 update. Fixes a lingering bug in StructInst where some intermediate syntax was malformed, but this had no observable effects outside of some debug messages.
This commit is contained in:
Kyle Miller
GitHub
parent
ca96922b4b
commit
7b8504cf06
4 changed files with 46 additions and 78 deletions
|
|
@ -283,9 +283,8 @@ private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) (
|
|||
loop 0 #[]
|
||||
|
||||
private def expandWhereStructInst : Macro := fun whereStx => do
|
||||
let whereTk := whereStx[0]
|
||||
let structInstFields : TSyntaxArray ``Parser.Term.structInstField := .mk whereStx[1][0].getSepArgs
|
||||
let whereDecls? := whereStx[2].getOptional?
|
||||
let `(Parser.Command.whereStructInst| where%$whereTk $[$structInstFields];* $[$whereDecls?:whereDecls]?) := whereStx
|
||||
| Macro.throwUnsupported
|
||||
|
||||
let startOfStructureTkInfo : SourceInfo :=
|
||||
match whereTk.getPos? with
|
||||
|
|
|
|||
|
|
@ -261,16 +261,11 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
|
|||
| `({ $[$srcs?,* with]? $fields,* $[..%$ell?]? $[: $ty?]? }) =>
|
||||
if let some srcs := srcs? then
|
||||
throwErrorAt (mkNullNode srcs) "invalid struct instance pattern, 'with' is not allowed in patterns"
|
||||
-- TODO(kmill) restore this
|
||||
-- let fields ← fields.getElems.mapM fun
|
||||
-- | `(Parser.Term.structInstField| $lval:structInstLVal := $val) => do
|
||||
-- let newVal ← collect val
|
||||
-- `(Parser.Term.structInstField| $lval:structInstLVal := $newVal)
|
||||
-- | _ => throwInvalidPattern -- `structInstFieldAbbrev` should be expanded at this point
|
||||
let fields ← fields.getElems.mapM fun field => do
|
||||
let field := field.raw
|
||||
let val ← collect field[1][2][1]
|
||||
pure <| field.setArg 1 <| field[1].setArg 2 <| field[1][2].setArg 1 val
|
||||
let fields ← fields.getElems.mapM fun
|
||||
| `(Parser.Term.structInstField| $lval:structInstLVal := $val) => do
|
||||
let newVal ← collect val
|
||||
`(Parser.Term.structInstField| $lval:structInstLVal := $newVal)
|
||||
| _ => throwInvalidPattern -- `structInstField` should be expanded at this point
|
||||
`({ $[$srcs?,* with]? $fields,* $[..%$ell?]? $[: $ty?]? })
|
||||
| _ => throwInvalidPattern
|
||||
|
||||
|
|
|
|||
|
|
@ -74,62 +74,44 @@ Structure instance notation makes use of the expected type.
|
|||
`(($stxNew : $expected))
|
||||
|
||||
def mkStructInstField (lval : TSyntax ``Parser.Term.structInstLVal) (binders : TSyntaxArray ``Parser.Term.structInstFieldBinder)
|
||||
(type? : Option Term) (val : Term) : MacroM Term := do
|
||||
(type? : Option Term) (val : Term) : MacroM (TSyntax ``Parser.Term.structInstField) := do
|
||||
let mut val := val
|
||||
if let some type := type? then
|
||||
val ← `(($val : $type))
|
||||
if !binders.isEmpty then
|
||||
-- HACK: this produces invalid syntax, but the fun elaborator supports structInstFieldBinder as well
|
||||
val ← `(fun $binders* => $val)
|
||||
-- `(Parser.Term.structInstField| $lval := $val)
|
||||
return mkNode ``Parser.Term.structInstField
|
||||
#[lval, mkNullNode #[mkNullNode, mkNullNode, mkNode ``Parser.Term.structInstFieldDef #[mkAtom " := ", val]]]
|
||||
`(Parser.Term.structInstField| $lval := $val)
|
||||
|
||||
/--
|
||||
Takes an arbitrary `structInstField` and expands it to be a `structInstFieldDef` without any binders or type ascription.
|
||||
-/
|
||||
private def expandStructInstField (stx : Syntax) : MacroM (Option Syntax) := withRef stx do
|
||||
if stx.isOfKind `Lean.Parser.Term.structInstField && stx.getNumArgs == 3 then
|
||||
-- old syntax
|
||||
let lval : TSyntax ``Parser.Term.structInstLVal := stx[0]
|
||||
let val : Term := stx[2]
|
||||
mkStructInstField lval #[] none val
|
||||
else if stx.isOfKind `Lean.Parser.Term.structInstFieldAbbrev then
|
||||
-- old syntax
|
||||
let id : Ident := stx[0]
|
||||
let lval ← `(Parser.Term.structInstLVal| $id:ident)
|
||||
mkStructInstField lval #[] none id
|
||||
else if stx.isOfKind ``Parser.Term.structInstField then
|
||||
let lval := stx[0]
|
||||
if stx[1].getNumArgs > 0 then
|
||||
let binders := stx[1][0].getArgs
|
||||
let ty? := match stx[1][1] with | `(Parser.Term.optTypeForStructInst| $[: $ty?]?) => ty? | _ => none
|
||||
let decl := stx[1][2]
|
||||
match decl with
|
||||
| `(Parser.Term.structInstFieldDef| := $val) =>
|
||||
if binders.isEmpty && ty?.isNone then
|
||||
return none
|
||||
else
|
||||
mkStructInstField lval binders ty? val
|
||||
| `(Parser.Term.structInstFieldEqns| $alts:matchAlts) =>
|
||||
let val ← expandMatchAltsIntoMatch stx alts (useExplicit := false)
|
||||
mkStructInstField lval binders ty? val
|
||||
| _ => Macro.throwUnsupported
|
||||
else
|
||||
-- Abbreviation
|
||||
match lval with
|
||||
| `(Parser.Term.structInstLVal| $id:ident) =>
|
||||
mkStructInstField lval #[] none id
|
||||
| _ =>
|
||||
Macro.throwErrorAt lval "unsupported structure instance field abbreviation, expecting identifier"
|
||||
else
|
||||
Macro.throwUnsupported
|
||||
match stx with
|
||||
| `(Parser.Term.structInstField| $_:structInstLVal := $_) =>
|
||||
-- Already expanded.
|
||||
return none
|
||||
| `(Parser.Term.structInstField| $lval:structInstLVal $[$binders]* $[: $ty?]? $decl:structInstFieldDecl) =>
|
||||
match decl with
|
||||
| `(Parser.Term.structInstFieldDef| := $val) =>
|
||||
mkStructInstField lval binders ty? val
|
||||
| `(Parser.Term.structInstFieldEqns| $alts:matchAlts) =>
|
||||
let val ← expandMatchAltsIntoMatch stx alts (useExplicit := false)
|
||||
mkStructInstField lval binders ty? val
|
||||
| _ => Macro.throwUnsupported
|
||||
| `(Parser.Term.structInstField| $lval:structInstLVal) =>
|
||||
-- Abbreviation
|
||||
match lval with
|
||||
| `(Parser.Term.structInstLVal| $id:ident) =>
|
||||
mkStructInstField lval #[] none id
|
||||
| _ =>
|
||||
Macro.throwErrorAt lval "unsupported structure instance field abbreviation, expecting identifier"
|
||||
| _ => Macro.throwUnsupported
|
||||
|
||||
/--
|
||||
Expands fields.
|
||||
* Abbrevations. Example: `{ x }` expands to `{ x := x }`.
|
||||
* Equations. Example: `{ f | 0 => 0 | n + 1 => n }` expands to `{ f := fun x => match x with | 0 => 0 | n + 1 => n }`.
|
||||
* `where`. Example: `{ s where x := 1 }` expands to `{ s := { x := 1 }}`.
|
||||
* Binders and types. Example: `{ f n : Nat := n + 1 }` expands to `{ f := fun n => (n + 1 : Nat) }`.
|
||||
-/
|
||||
@[builtin_macro Lean.Parser.Term.structInst] def expandStructInstFields : Macro | stx => do
|
||||
|
|
@ -461,7 +443,7 @@ Converts a `FieldLHS` back into syntax. This assumes the `ref` fields have the c
|
|||
|
||||
Recall that `structInstField` elements have the form
|
||||
```lean
|
||||
def structInstField := leading_parser structInstLVal >> " := " >> termParser
|
||||
def structInstField := leading_parser structInstLVal >> group (null >> null >> group (" := " >> termParser))
|
||||
def structInstLVal := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (("." >> (ident <|> numLit)) <|> structInstArrayRef)
|
||||
def structInstArrayRef := leading_parser "[" >> termParser >>"]"
|
||||
```
|
||||
|
|
@ -487,7 +469,7 @@ private def Field.toSyntax : Field → Syntax
|
|||
let stx := field.ref
|
||||
let stx := stx.setArg 1 <| stx[1].setArg 2 <| stx[1][2].setArg 1 field.val.toSyntax
|
||||
match field.lhs with
|
||||
| first::rest => stx.setArg 0 <| mkNullNode #[first.toSyntax true, mkNullNode <| rest.toArray.map (FieldLHS.toSyntax false) ]
|
||||
| first::rest => stx.setArg 0 <| mkNode ``Parser.Term.structInstLVal #[first.toSyntax true, mkNullNode <| rest.toArray.map (FieldLHS.toSyntax false) ]
|
||||
| _ => unreachable!
|
||||
|
||||
/-- Creates a view of a field left-hand side. -/
|
||||
|
|
@ -509,25 +491,21 @@ and the computed structure name (from `Lean.Elab.Term.StructInst.getStructName`)
|
|||
and structure source view (from `Lean.Elab.Term.StructInst.getStructSources`).
|
||||
-/
|
||||
private def mkStructView (stx : Syntax) (structName : Name) (sources : SourcesView) : MacroM StructInstView := do
|
||||
/- Recall that `stx` is of the form
|
||||
```
|
||||
leading_parser "{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
|
||||
>> structInstFields (sepByIndent structInstField ...)
|
||||
>> optional ".."
|
||||
>> optional (" : " >> termParser)
|
||||
>> " }"
|
||||
```
|
||||
This method assumes that `structInstField` had already been expanded by the macro `expandStructInstFields`
|
||||
and is of the form
|
||||
```
|
||||
def structInstFieldDef := leading_parser
|
||||
structInstLVal >> group (null >> null >> group (" := " >> termParser))
|
||||
```
|
||||
/-
|
||||
Recall that `stx` is of the form
|
||||
```
|
||||
leading_parser "{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
|
||||
>> structInstFields (sepByIndent structInstField ...)
|
||||
>> optional ".."
|
||||
>> optional (" : " >> termParser)
|
||||
>> " }"
|
||||
```
|
||||
This method assumes that `structInstField` had already been expanded by the macro `expandStructInstFields`.
|
||||
-/
|
||||
let fields ← stx[2][0].getSepArgs.toList.mapM fun fieldStx => do
|
||||
let val := fieldStx[1][2][1]
|
||||
let first ← toFieldLHS fieldStx[0][0]
|
||||
let rest ← fieldStx[0][1].getArgs.toList.mapM toFieldLHS
|
||||
let `(Parser.Term.structInstField| $lval:structInstLVal := $val) := fieldStx | Macro.throwUnsupported
|
||||
let first ← toFieldLHS lval.raw[0]
|
||||
let rest ← lval.raw[1].getArgs.toList.mapM toFieldLHS
|
||||
return { ref := fieldStx, lhs := first :: rest, val := FieldVal.term val : Field }
|
||||
return { ref := stx, structName, params := #[], fields, sources }
|
||||
|
||||
|
|
@ -673,7 +651,7 @@ mutual
|
|||
let updateSource (structStx : Syntax) : TermElabM Syntax := do
|
||||
let sourcesNew ← s.sources.explicit.filterMapM fun source => mkProjStx? source.stx source.structName fieldName
|
||||
let explicitSourceStx := if sourcesNew.isEmpty then mkNullNode else mkSourcesWithSyntax sourcesNew
|
||||
let implicitSourceStx := s.sources.implicit.getD mkNullNode
|
||||
let implicitSourceStx := s.sources.implicit.getD (mkNode ``Parser.Term.optEllipsis #[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
|
||||
|
|
|
|||
|
|
@ -238,11 +238,7 @@ def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStruct
|
|||
let fieldPos ← nextExtraPos
|
||||
let fieldId := annotatePos fieldPos fieldId
|
||||
addFieldInfo fieldPos (s.induct ++ fieldName) fieldName fieldId fieldVals[idx]!
|
||||
-- TODO(kmill) restore this
|
||||
-- let field ← `(structInstField|$fieldId:ident := $(stx[1][idx]))
|
||||
let lval ← `(structInstLVal| $fieldId:ident)
|
||||
let field := mkNode ``Parser.Term.structInstField
|
||||
#[lval, mkNullNode #[mkNullNode, mkNullNode, mkNode ``Parser.Term.structInstFieldDef #[mkAtom " := ", stx[1][idx]]]]
|
||||
let field ← `(structInstField|$fieldId:ident := $(stx[1][idx]))
|
||||
fields := fields.push field
|
||||
let tyStx ← withType do
|
||||
if (← getPPOption getPPStructureInstanceType) then delab >>= pure ∘ some else pure none
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue