From 2eafb705852de9b54a7d37d76796bb3de2c0ea6b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2020 15:52:08 -0800 Subject: [PATCH] chore: add auxiliary functions and simplify `Quotation` --- src/Init/Lean/Elab/BuiltinNotation.lean | 10 +++++----- src/Init/Lean/Elab/Quotation.lean | 24 +++++++++++------------- src/Init/Lean/Elab/Syntax.lean | 2 +- src/Init/Lean/Elab/Term.lean | 19 ++----------------- src/Init/Lean/Parser/Term.lean | 21 +++++++++++++++++++++ src/Init/Lean/Syntax.lean | 2 +- 6 files changed, 41 insertions(+), 37 deletions(-) diff --git a/src/Init/Lean/Elab/BuiltinNotation.lean b/src/Init/Lean/Elab/BuiltinNotation.lean index 8741c8c7a6..8fcede142c 100644 --- a/src/Init/Lean/Elab/BuiltinNotation.lean +++ b/src/Init/Lean/Elab/BuiltinNotation.lean @@ -50,7 +50,7 @@ match expectedType? with if val.ctors.length != 1 then throwError ref ("invalid constructor ⟨...⟩, '" ++ constName ++ "' must have only one constructor") else - let ctor := mkTermId ref val.ctors.head!; + let ctor := mkTermIdFrom ref val.ctors.head!; let args := (stx.getArg 1).getArgs.getEvenElems; do withMacroExpansion ref $ elabTerm (mkAppStx ctor args) expectedType? | _ => throwError ref ("invalid constructor ⟨...⟩, '" ++ constName ++ "' is not an inductive type") @@ -58,13 +58,13 @@ match expectedType? with @[builtinTermElab «show»] def elabShow : TermElab := adaptExpander $ fun stx => match_syntax stx with -| `(show $type from $val) => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $thisId) $val) +| `(show $type from $val) => let thisId := mkTermIdFrom stx `this; `((fun ($thisId : $type) => $thisId) $val) | _ => throwUnsupportedSyntax @[builtinTermElab «have»] def elabHave : TermElab := adaptExpander $ fun stx => match_syntax stx with -| `(have $type from $val; $body) => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $body) $val) -| `(have $type := $val; $body) => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $body) $val) +| `(have $type from $val; $body) => let thisId := mkTermIdFrom stx `this; `((fun ($thisId : $type) => $body) $val) +| `(have $type := $val; $body) => let thisId := mkTermIdFrom stx `this; `((fun ($thisId : $type) => $body) $val) | `(have $x : $type from $val; $body) => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val) | `(have $x : $type := $val; $body) => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val) | _ => throwUnsupportedSyntax @@ -114,7 +114,7 @@ fun stx expectedType? => do elabTerm (mkAppStx f #[a, b]) expectedType? def elabInfixOp (op : Name) : TermElab := -fun stx expectedType? => elabInfix (mkTermId (stx.getArg 1) op) stx expectedType? +fun stx expectedType? => elabInfix (mkTermIdFrom (stx.getArg 1) op) stx expectedType? @[builtinTermElab prod] def elabProd : TermElab := elabInfixOp `Prod @[builtinTermElab fcomp] def ElabFComp : TermElab := elabInfixOp `Function.comp diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean index 6d8c3db846..268f17133b 100644 --- a/src/Init/Lean/Elab/Quotation.lean +++ b/src/Init/Lean/Elab/Quotation.lean @@ -33,32 +33,30 @@ export HasQuote (quote) instance Syntax.HasQuote : HasQuote Syntax := ⟨id⟩ instance String.HasQuote : HasQuote String := ⟨fun s => Syntax.node `Lean.Parser.Term.str #[mkStxStrLit s]⟩ instance Nat.HasQuote : HasQuote Nat := ⟨fun n => Syntax.node `Lean.Parser.Term.num #[mkStxNumLit $ toString n]⟩ +instance Substring.HasQuote : HasQuote Substring := ⟨fun s => mkCAppStx `_root_.String.toSubstring #[quote s.toString]⟩ private def quoteName : Name → Syntax -| Name.anonymous => Unhygienic.run `(_root_.Lean.Name.anonymous) -| Name.str n s _ => Unhygienic.run `(_root_.Lean.mkNameStr $(quoteName n) $(quote s)) -| Name.num n i _ => Unhygienic.run `(_root_.Lean.mkNameNum $(quoteName n) $(quote i)) +| Name.anonymous => mkTermId `_root_.Lean.Name.anonymous +| Name.str n s _ => mkCAppStx `_root_.Lean.mkNameStr #[quoteName n, quote s] +| Name.num n i _ => mkCAppStx `_root_.Lean.mkNameNum #[quoteName n, quote i] instance Name.hasQuote : HasQuote Name := ⟨quoteName⟩ -private def appN (fn : Syntax) (args : Array Syntax) : Syntax := -args.foldl (fun fn arg => Unhygienic.run `($fn $arg)) fn - instance Prod.hasQuote {α β : Type} [HasQuote α] [HasQuote β] : HasQuote (α × β) := -⟨fun ⟨a, b⟩ => Unhygienic.run `(_root_.Prod.mk $(quote a) $(quote b))⟩ +⟨fun ⟨a, b⟩ => mkCAppStx `_root_.Prod.mk #[quote a, quote b]⟩ private def quoteList {α : Type} [HasQuote α] : List α → Syntax -| [] => Unhygienic.run `(_root_.List.nil) -| (x::xs) => Unhygienic.run `(_root_.List.cons $(quote x) $(quoteList xs)) +| [] => mkTermId `_root_.List.nil +| (x::xs) => mkCAppStx `_root_.List.cons #[quote x, quoteList xs] instance List.hasQuote {α : Type} [HasQuote α] : HasQuote (List α) := ⟨quoteList⟩ instance Array.hasQuote {α : Type} [HasQuote α] : HasQuote (Array α) := -⟨fun xs => let stx := quote xs.toList; Unhygienic.run `(_root_.List.toArray $stx)⟩ +⟨fun xs => mkCAppStx `_root_.List.toArray #[quote xs.toList]⟩ private def quoteOption {α : Type} [HasQuote α] : Option α → Syntax -| none => Unhygienic.run `(_root_.Option.none) -| (some x) => Unhygienic.run `(_root_.Option.some $(quote x)) +| none => mkTermId `_root_.Option.none +| (some x) => mkCAppStx `_root_.Option.some #[quote x] instance Option.hasQuote {α : Type} [HasQuote α] : HasQuote (Option α) := ⟨quoteOption⟩ @@ -108,7 +106,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax let preresolved := resolveGlobalName env currNamespace openDecls val ++ preresolved; let val := quote val; -- `scp` is bound in stxQuot.expand - `(Syntax.ident none (String.toSubstring $(quote (toString rawVal))) (addMacroScope $val scp) $(quote preresolved)) + `(Syntax.ident none $(quote rawVal) (addMacroScope $val scp) $(quote preresolved)) -- if antiquotation, insert contents as-is, else recurse | stx@(Syntax.node k args) => if isAntiquot stx then diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean index ffe030d70f..d773625acc 100644 --- a/src/Init/Lean/Elab/Syntax.lean +++ b/src/Init/Lean/Elab/Syntax.lean @@ -210,7 +210,7 @@ def expandNotationItemIntoPattern (stx : Syntax) : CommandElabM Syntax := let k := stx.getKind; if k == `Lean.Parser.Command.identPrec then let item := stx.getArg 0; - pure $ mkNode `antiquot #[mkAtom "$", Term.mkTermIdFromIdent item, mkNullNode, mkNullNode] + pure $ mkNode `antiquot #[mkAtom "$", mkTermIdFromIdent item, mkNullNode, mkNullNode] else if k == `Lean.Parser.Command.quotedSymbolPrec then pure $ (stx.getArg 0).getArg 1 else if k == `Lean.Parser.Command.strLitPrec then diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index 96cf21dacf..84ba1ad973 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/src/Init/Lean/Elab/Term.lean @@ -355,21 +355,6 @@ let instIdx := s.instImplicitIdx; modify $ fun s => { instImplicitIdx := s.instImplicitIdx + 1, .. s}; pure $ (`_inst).appendIndexAfter instIdx -def mkHole (ref : Syntax) := mkNode `Lean.Parser.Term.hole #[mkAtomFrom ref "_"] - -/-- Convert a `Syntax.ident` into a `Lean.Parser.Term.id` node -/ -def mkTermIdFromIdent (ident : Syntax) : Syntax := -match ident with -| Syntax.ident _ _ _ _ => mkNode `Lean.Parser.Term.id #[ident, mkNullNode] -| _ => unreachable! - -/-- - Create a simple `Lean.Parser.Term.id` syntax using position - information from `ref` and name `n`. By simple, we mean that - `optional (explicitUniv <|> namedPattern)` is none. -/ -def mkTermId (ref : Syntax) (n : Name) : Syntax := -mkTermIdFromIdent (mkIdentFrom ref n) - /-- Return true if the given syntax is a `Lean.Parser.Term.cdot` or is a `Lean.Parser.Term.app` containing a `cdot`. @@ -710,8 +695,8 @@ fun stx expectedType? => do let openBkt := stx.getArg 0; let args := stx.getArg 1; let closeBkt := stx.getArg 2; - let consId := mkTermId openBkt `List.cons; - let nilId := mkTermId closeBkt `List.nil; + let consId := mkTermIdFrom openBkt `List.cons; + let nilId := mkTermIdFrom closeBkt `List.nil; let newStx := args.foldSepRevArgs (fun arg r => mkAppStx consId #[arg, r]) nilId; elabTerm newStx expectedType? diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean index 4cd9e4e4f5..9b878747d7 100644 --- a/src/Init/Lean/Parser/Term.lean +++ b/src/Init/Lean/Parser/Term.lean @@ -185,6 +185,27 @@ open Parser def mkAppStx (fn : Syntax) (args : Array Syntax) : Syntax := args.foldl (fun fn arg => Syntax.node `Lean.Parser.Term.app #[fn, arg]) fn +def mkHole (ref : Syntax) := mkNode `Lean.Parser.Term.hole #[mkAtomFrom ref "_"] + +/-- Convert a `Syntax.ident` into a `Lean.Parser.Term.id` node -/ +def mkTermIdFromIdent (ident : Syntax) : Syntax := +match ident with +| Syntax.ident _ _ _ _ => mkNode `Lean.Parser.Term.id #[ident, mkNullNode] +| _ => unreachable! + +/-- + Create a simple `Lean.Parser.Term.id` syntax using position + information from `ref` and name `n`. By simple, we mean that + `optional (explicitUniv <|> namedPattern)` is none. -/ +def mkTermIdFrom (ref : Syntax) (n : Name) : Syntax := +mkTermIdFromIdent (mkIdentFrom ref n) + +def mkTermId (n : Name) : Syntax := +mkTermIdFromIdent (Syntax.ident none n.toString.toSubstring n []) + +def mkCAppStx (fn : Name) (args : Array Syntax) : Syntax := +mkAppStx (mkTermId fn) args + def Syntax.isTermId? (stx : Syntax) : Option (Syntax × Syntax) := stx.ifNode (fun node => diff --git a/src/Init/Lean/Syntax.lean b/src/Init/Lean/Syntax.lean index 6f0d54d41d..f97062bdee 100644 --- a/src/Init/Lean/Syntax.lean +++ b/src/Init/Lean/Syntax.lean @@ -305,7 +305,7 @@ end SyntaxNode /- Helper functions for creating Syntax objects using C++ -/ @[export lean_mk_syntax_atom] -def mkSimpleAtomCore (val : String) : Syntax := +def mkSimpleAtom (val : String) : Syntax := Syntax.atom none val @[export lean_mk_syntax_ident]