From b2ade985a813813ca84e48c2ce37cf791b6ed628 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2020 19:51:33 -0800 Subject: [PATCH] feat: elaborate `macro` command --- src/Init/Lean/Elab/Syntax.lean | 95 ++++++++++++++++++++++++++++---- tests/lean/run/newfrontend1.lean | 18 ++++-- 2 files changed, 96 insertions(+), 17 deletions(-) diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean index 18c77e696a..0b6fac88ed 100644 --- a/src/Init/Lean/Elab/Syntax.lean +++ b/src/Init/Lean/Elab/Syntax.lean @@ -143,12 +143,16 @@ fun stx => do env ← liftIO stx $ Parser.registerParserCategory env attrName catName; setEnv env +def mkFreshKind (catName : Name) : CommandElabM Name := do +env ← getEnv; +let (env, kind) := Parser.mkFreshKind env catName; +setEnv env; +pure kind + + private def elabKind (stx : Syntax) (catName : Name) : CommandElabM Name := do -if stx.isNone then do - env ← getEnv; - let (env, kind) := Parser.mkFreshKind env catName; - setEnv env; - pure kind +if stx.isNone then + mkFreshKind catName else do let kind := stx.getIdAt 1; currNamespace ← getCurrNamespace; @@ -205,6 +209,11 @@ else if k == `Lean.Parser.Command.strLitPrec then else throwUnsupportedSyntax +def strLitPrecToPattern (stx: Syntax) : CommandElabM Syntax := +match (stx.getArg 0).isStrLit? with +| some str => pure $ mkAtomFrom stx str +| none => throwUnsupportedSyntax + /- Convert `notation` command lhs item a pattern element -/ def expandNotationItemIntoPattern (stx : Syntax) : CommandElabM Syntax := let k := stx.getKind; @@ -214,30 +223,92 @@ if k == `Lean.Parser.Command.identPrec then else if k == `Lean.Parser.Command.quotedSymbolPrec then pure $ (stx.getArg 0).getArg 1 else if k == `Lean.Parser.Command.strLitPrec then - match (stx.getArg 0).isStrLit? with - | some str => pure $ mkAtomFrom stx str - | none => throwUnsupportedSyntax + strLitPrecToPattern stx else throwUnsupportedSyntax @[builtinCommandElab «notation»] def elabNotation : CommandElab := adaptExpander $ fun stx => match_syntax stx with | `(notation $items* => $rhs) => do + kind ← mkFreshKind `term; -- build parser syntaxParts ← items.mapM expandNotationItemIntoSyntaxItem; let cat := mkIdentFrom stx `term; - -- build macro + -- build macro rules let vars := items.filter $ fun item => item.getKind == `Lean.Parser.Command.identPrec; let vars := vars.map $ fun var => var.getArg 0; let rhs := antiquote vars rhs; patArgs ← items.mapM expandNotationItemIntoPattern; - scp ← getCurrMacroScope; - -- manually create hygienic kind name - let kind := addMacroScope `myParser scp; let pat := Syntax.node kind patArgs; `(syntax [$(mkIdentFrom stx kind)] $syntaxParts* : $cat macro_rules | `($pat) => `($rhs)) | _ => throwUnsupportedSyntax +/- Convert `macro` head into a `syntax` command item -/ +def expandMacroHeadIntoSyntaxItem (stx : Syntax) : CommandElabM Syntax := +let k := stx.getKind; +if k == `Lean.Parser.Command.identPrec then + let info := stx.getHeadInfo; + let id := (stx.getArg 0).getId; + pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit (toString id) info, stx.getArg 1] +else if k == `Lean.Parser.Command.strLitPrec then + pure $ Syntax.node `Lean.Parser.Syntax.atom stx.getArgs +else + throwUnsupportedSyntax + +/- Convert `macro` argument into a `syntax` command item -/ +def expandMacroArgIntoSyntaxItem (stx : Syntax) : CommandElabM Syntax := +let k := stx.getKind; +if k == `Lean.Parser.Command.macroArgSimple then + pure $ Syntax.node `Lean.Parser.Syntax.cat #[stx.getArg 2, stx.getArg 3] +else if k == `Lean.Parser.Command.strLitPrec then + pure $ Syntax.node `Lean.Parser.Syntax.atom stx.getArgs +else + throwUnsupportedSyntax + +/- Convert `macro` head into a pattern element -/ +def expandMacroHeadIntoPattern (stx : Syntax) : CommandElabM Syntax := +let k := stx.getKind; +if k == `Lean.Parser.Command.identPrec then + let str := toString (stx.getArg 0).getId; + pure $ mkAtomFrom stx str +else if k == `Lean.Parser.Command.strLitPrec then + strLitPrecToPattern stx +else + throwUnsupportedSyntax + +/- Convert `macro` arg into a pattern element -/ +def expandMacroArgIntoPattern (stx : Syntax) : CommandElabM Syntax := +let k := stx.getKind; +if k == `Lean.Parser.Command.macroArgSimple then + let item := stx.getArg 0; + pure $ mkNode `antiquot #[mkAtom "$", mkTermIdFromIdent item, mkNullNode, mkNullNode] +else if k == `Lean.Parser.Command.strLitPrec then + strLitPrecToPattern stx +else + throwUnsupportedSyntax + +@[builtinCommandElab «macro»] def elabMacro : CommandElab := +adaptExpander $ fun stx => do + let head := stx.getArg 1; + let args := (stx.getArg 2).getArgs; + let cat := stx.getArg 4; + let rhsBody := stx.getArg 7; + kind ← mkFreshKind cat.getId; + -- build parser + stxPart ← expandMacroHeadIntoSyntaxItem head; + stxParts ← args.mapM expandMacroArgIntoSyntaxItem; + let stxParts := #[stxPart] ++ stxParts; + -- build macro rules + patHead ← expandMacroHeadIntoPattern head; + patArgs ← args.mapM expandMacroArgIntoPattern; + let pat := Syntax.node kind (#[patHead] ++ patArgs); + trace `Elab.syntax stx $ fun _ => pat; + `(syntax [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => `($rhsBody)) + +@[init] private def regTraceClasses : IO Unit := do +registerTraceClass `Elab.syntax; +pure () + end Command end Elab end Lean diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean index 69d98ebc33..3e24816e09 100644 --- a/tests/lean/run/newfrontend1.lean +++ b/tests/lean/run/newfrontend1.lean @@ -63,9 +63,17 @@ begin assumption end --- set_option trace.Elab true --- set_option syntaxMaxDepth 100 +macro intro3 : tactic => `(intro; intro; intro) +macro check2 x:term : command => `(#check $x #check $x) +macro foo x:term "," y:term : term => `($x + $y + $x) --- macro intro3 : tactic => `(intro; intro) --- macro check2 x: term : command => `(#check $x #check $x) --- macro foo x: term ", " y: term : term => `($x + $y + $x) +set_option pp.all false + +check2 0+1 +check2 foo 0,1 + +theorem simple4 (x y : Nat) : y = y → x = x → x = y → x = y := +begin + intro3; + assumption +end