From 9301e05a7e9015445262ffaa400dde128ae45a1b Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 27 Apr 2021 16:25:32 +0200 Subject: [PATCH] feat: double-quoted quotation semantics and basic precheck hooks --- src/Lean/Elab/Binders.lean | 13 +++++++ src/Lean/Elab/Do.lean | 5 --- src/Lean/Elab/Match.lean | 20 ++++++++++- src/Lean/Elab/Quotation/Precheck.lean | 51 +++++++++++++++++++++++++-- tests/lean/StxQuot.lean | 8 +++++ tests/lean/StxQuot.lean.expected.out | 6 ++++ 6 files changed, 95 insertions(+), 8 deletions(-) diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index e86b44f133..de40ac3e00 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ +import Lean.Elab.Quotation.Precheck import Lean.Elab.Term import Lean.Parser.Term @@ -494,6 +495,18 @@ def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax := | stx@`(fun $m:matchAlts) => expandMatchAltsIntoMatch stx m | _ => Macro.throwUnsupported +open Lean.Elab.Term.Quotation in +@[builtinQuotPrecheck Lean.Parser.Term.fun] def precheckFun : Precheck + | `(fun $binders* => $body) => do + let (binders, body, expandedPattern) ← liftMacroM <| expandFunBinders binders body + let mut ids := #[] + for b in binders do + for v in ← matchBinder b do + Quotation.withNewLocals ids <| precheck v.type + ids := ids.push v.id.getId + Quotation.withNewLocals ids <| precheck body + | _ => throwUnsupportedSyntax + @[builtinTermElab «fun»] partial def elabFun : TermElab := fun stx expectedType? => match stx with | `(fun $binders* => $body) => do diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index bcc51fc6d7..370ec31bd0 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -561,11 +561,6 @@ def concat (terminal : CodeBlock) (kRef : Syntax) (y? : Option Name) (k : CodeBl def getLetIdDeclVar (letIdDecl : Syntax) : Name := letIdDecl[0].getId -def getPatternVarNames (pvars : Array PatternVar) : Array Name := - pvars.filterMap fun - | PatternVar.localVar x => some x - | _ => none - -- support both regular and syntax match def getPatternVarsEx (pattern : Syntax) : TermElabM (Array Name) := getPatternVarNames <$> getPatternVars pattern <|> diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 8a7427acb0..23ebca691f 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -512,7 +512,7 @@ private def collectPatternVars (alt : MatchAltView) : TermElabM (Array PatternVa return (s.vars, alt) /- Return the pattern variables in the given pattern. - Remark: this method is not used here, but in other macros (e.g., at `Do.lean`). -/ + Remark: this method is not used by the main `match` elaborator, but in the precheck hook and other macros (e.g., at `Do.lean`). -/ def getPatternVars (patternStx : Syntax) : TermElabM (Array PatternVar) := do let patternStx ← liftMacroM <| expandMacros patternStx let (_, s) ← (CollectPatternVars.collect patternStx).run {} @@ -525,6 +525,24 @@ def getPatternsVars (patterns : Array Syntax) : TermElabM (Array PatternVar) := let (_, s) ← collect.run {} return s.vars +def getPatternVarNames (pvars : Array PatternVar) : Array Name := + pvars.filterMap fun + | PatternVar.localVar x => some x + | _ => none + +open Lean.Elab.Term.Quotation in +@[builtinQuotPrecheck Lean.Parser.Term.match] def precheckMatch : Precheck + | `(match $[$discrs:term],* with $[| $[$patss],* => $rhss]*) => do + discrs.forM precheck + for (pats, rhs) in patss.zip rhss do + let vars ← + try + getPatternsVars pats + catch + | _ => return -- can happen in case of pattern antiquotations + Quotation.withNewLocals (getPatternVarNames vars) <| precheck rhs + | _ => throwUnsupportedSyntax + /- We convert the collected `PatternVar`s intro `PatternVarDecl` -/ inductive PatternVarDecl where /- For `anonymousVar`, we create both a metavariable and a free variable. The free variable is used as an assignment for the metavariable diff --git a/src/Lean/Elab/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean index 3be63981d4..5f13b96d7d 100644 --- a/src/Lean/Elab/Quotation/Precheck.lean +++ b/src/Lean/Elab/Quotation/Precheck.lean @@ -11,6 +11,7 @@ import Lean.Elab.Quotation.Util namespace Lean.Elab.Term.Quotation open Lean.Elab.Term +open Lean.Parser.Term structure Precheck.Context where quotLCtx : NameSet @@ -18,6 +19,12 @@ structure Precheck.Context where abbrev PrecheckM := ReaderT Precheck.Context TermElabM abbrev Precheck := Syntax → PrecheckM Unit +protected def withNewLocal (l : Name) (x : PrecheckM α) : PrecheckM α := + withReader (fun ctx => { ctx with quotLCtx := ctx.quotLCtx.insert l }) x + +protected def withNewLocals (ls : Array Name) (x : PrecheckM α) : PrecheckM α := + withReader (fun ctx => { ctx with quotLCtx := ls.foldl NameSet.insert ctx.quotLCtx }) x + unsafe def mkPrecheckAttribute : IO (KeyedDeclsAttribute Precheck) := KeyedDeclsAttribute.init { builtinName := `builtinQuotPrecheck, @@ -31,7 +38,9 @@ unsafe def mkPrecheckAttribute : IO (KeyedDeclsAttribute Precheck) := partial def precheck : Precheck := fun stx => do if let p::_ := precheckAttribute.getValues (← getEnv) stx.getKind then - p stx + if ← catchInternalId unsupportedSyntaxExceptionId (do withRef stx <| p stx; true) (fun _ => false) then + return + if stx.isAntiquot then return if !hasIdent stx then return -- we only precheck identifiers, so there is nothing to check here @@ -42,11 +51,49 @@ partial def precheck : Precheck := fun stx => do where hasIdent stx := do for stx in stx.topDown do - if stx.isIdent then + if stx.isIdent then return true return false def runPrecheck (stx : Syntax) : TermElabM Unit := precheck stx |>.run { quotLCtx := {} } +@[builtinQuotPrecheck ident] def precheckIdent : Precheck + | Syntax.ident info rawVal val preresolved => do + if !preresolved.isEmpty then + return + if let _::_ ← resolveGlobalName val then + return + if (← read).quotLCtx.contains val then + return + throwError "unknown identifier '{val}'" + | _ => throwUnsupportedSyntax + +@[builtinQuotPrecheck Lean.Parser.Term.app] def precheckApp : Precheck + | `($f $args*) => do + precheck f + for arg in args do + match arg with + | `(argument| ($n := $e)) => precheck e + | `(argument| $e:term) => precheck e + | `(argument| ..) => pure () + | _ => throwUnsupportedSyntax + | _ => throwUnsupportedSyntax + +@[builtinQuotPrecheck Lean.Parser.Term.paren] def precheckParen : Precheck + | `(()) => pure () + | `(($e : $type)) => do + precheck e + precheck type + | `(($e)) => precheck e + | `(($e, $es,*)) => do + precheck e + es.getElems.forM precheck + | _ => throwUnsupportedSyntax + +@[builtinTermElab precheckedQuot] def elabPrecheckedQuot : TermElab := fun stx expectedType? => do + let singleQuot := stx[1] + runPrecheck singleQuot.getQuotContent + adaptExpander (fun _ => singleQuot) stx expectedType? + end Lean.Elab.Term.Quotation diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean index 9051e32695..4c1da4c570 100644 --- a/tests/lean/StxQuot.lean +++ b/tests/lean/StxQuot.lean @@ -97,3 +97,11 @@ open Parser.Term match Syntax.setHeadInfo (← `(fun x =>%$(Syntax.atom (SourceInfo.synthetic 2 2) "") x)) (SourceInfo.synthetic 1 1) with | `(fun%$i1 $x =>%$i2 $y) => pure #[i1.getPos?, i2.getPos?] | _ => unreachable! + +#eval run ``(x) +#eval run ``(id) +#eval run ``(pure) +#eval run ``(fun x => x) +#eval run ``(fun x => y) +#eval run ``(fun x y => x y) +#eval run ``(fun ⟨x, y⟩ => x) diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index a477b4f399..29d14be5ba 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/tests/lean/StxQuot.lean.expected.out @@ -46,3 +46,9 @@ StxQuot.lean:18:15: error: expected term StxQuot.lean:94:39-94:44: error: unexpected antiquotation splice fun (a : ?m) => sorry : (a : ?m) → ?m a "#[(some 1), (some 2)]" +StxQuot.lean:101:13-101:14: error: unknown identifier 'x' +"`id._@.UnhygienicMain._hyg.1" +"`pure._@.UnhygienicMain._hyg.1" +"(Term.fun \"fun\" (Term.basicFun [`x._@.UnhygienicMain._hyg.1] \"=>\" `x._@.UnhygienicMain._hyg.1))" +"(Term.fun\n \"fun\"\n (Term.basicFun\n [`x._@.UnhygienicMain._hyg.1 `y._@.UnhygienicMain._hyg.1]\n \"=>\"\n (Term.app `x._@.UnhygienicMain._hyg.1 [`y._@.UnhygienicMain._hyg.1])))" +"(Term.fun\n \"fun\"\n (Term.basicFun\n [(Term.anonymousCtor \"⟨\" [`x._@.UnhygienicMain._hyg.1 \",\" `y._@.UnhygienicMain._hyg.1] \"⟩\")]\n \"=>\"\n `x._@.UnhygienicMain._hyg.1))"