diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 4111752a18..6a80c79a28 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -441,11 +441,11 @@ private def hasUnusedArguments : Expr → Bool When we look for such an instance it is enough to look for an instance `c : C` and then return `fun _ => c`. Tomas' approach makes sure that instance of a type like `a : A → C` never gets tabled/cached. More on that later. - At the core is the this methos. it takes an expression E and does two things: + At the core is this method. it takes an expression E and does two things: The modification to TC resolution works this way: We are looking for an instance of `E`, if it is tabled just get it as normal, but if not first remove all unused arguments producing `E'`. Now we look up the table again but - for `E'`. If it exists, use the transforme to create E. If it does not exists, create a new goal `E'`. + for `E'`. If it exists, use the transformer to create E. If it does not exists, create a new goal `E'`. -/ private def removeUnusedArguments? (mctx : MetavarContext) (mvar : Expr) : MetaM (Option (Expr × Expr)) := withMCtx mctx do diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean index ea4bb99162..c831c224c1 100644 --- a/src/Lean/Parser.lean +++ b/src/Lean/Parser.lean @@ -40,6 +40,8 @@ builtin_initialize register_parser_alias many1Indent register_parser_alias optional { autoGroupArgs := false } register_parser_alias withPosition { stackSz? := none } + register_parser_alias withoutPosition { stackSz? := none } + register_parser_alias withoutForbidden { stackSz? := none } register_parser_alias (kind := interpolatedStrKind) interpolatedStr register_parser_alias orelse register_parser_alias andthen { stackSz? := none } diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 85efd2bf6a..bb61fbcc34 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -11,7 +11,7 @@ namespace Parser /-- Syntax quotation for terms. -/ @[builtin_term_parser] def Term.quot := leading_parser - "`(" >> incQuotDepth termParser >> ")" + "`(" >> withoutPosition (incQuotDepth termParser) >> ")" @[builtin_term_parser] def Term.precheckedQuot := leading_parser "`" >> Term.quot @@ -26,7 +26,7 @@ Multiple commands will be put in a `` `null `` node, but a single command will not (so that you can directly match against a quotation in a command kind's elaborator). -/ @[builtin_term_parser low] def quot := leading_parser - "`(" >> incQuotDepth (many1Unbox commandParser) >> ")" + "`(" >> withoutPosition (incQuotDepth (many1Unbox commandParser)) >> ")" /- A mutual block may be broken in different cliques, @@ -60,7 +60,7 @@ def moduleDoc := leading_parser ppDedent <| "/-!" >> commentBody >> ppLine def namedPrio := leading_parser - atomic ("(" >> nonReservedSymbol "priority") >> " := " >> priorityParser >> ")" + atomic ("(" >> nonReservedSymbol "priority") >> " := " >> withoutPosition priorityParser >> ")" def optNamedPrio := optional (ppSpace >> namedPrio) def «private» := leading_parser "private " @@ -157,12 +157,12 @@ def classInductive := leading_parser optional (symbol " :=" <|> " where") >> many ctor >> optDeriving def structExplicitBinder := leading_parser atomic (declModifiers true >> "(") >> - many1 ident >> ppIndent optDeclSig >> - optional (Term.binderTactic <|> Term.binderDefault) >> ")" + withoutPosition (many1 ident >> ppIndent optDeclSig >> + optional (Term.binderTactic <|> Term.binderDefault)) >> ")" def structImplicitBinder := leading_parser - atomic (declModifiers true >> "{") >> many1 ident >> declSig >> "}" + atomic (declModifiers true >> "{") >> withoutPosition (many1 ident >> declSig) >> "}" def structInstBinder := leading_parser - atomic (declModifiers true >> "[") >> many1 ident >> declSig >> "]" + atomic (declModifiers true >> "[") >> withoutPosition (many1 ident >> declSig) >> "]" def structSimpleBinder := leading_parser atomic (declModifiers true >> ident) >> optDeclSig >> optional (Term.binderTactic <|> Term.binderDefault) @@ -228,7 +228,7 @@ def eraseAttr := leading_parser "-" >> rawIdent @[builtin_command_parser] def «attribute» := leading_parser "attribute " >> "[" >> - sepBy1 (eraseAttr <|> Term.attrInstance) ", " >> + withoutPosition (sepBy1 (eraseAttr <|> Term.attrInstance) ", ") >> "] " >> many1 ident @[builtin_command_parser] def «export» := leading_parser "export " >> ident >> " (" >> many1 ident >> ")" diff --git a/src/Lean/Parser/Level.lean b/src/Lean/Parser/Level.lean index 0e6f4d7d1c..3f05122c46 100644 --- a/src/Lean/Parser/Level.lean +++ b/src/Lean/Parser/Level.lean @@ -17,7 +17,7 @@ builtin_initialize namespace Level @[builtin_level_parser] def paren := leading_parser - "(" >> levelParser >> ")" + "(" >> withoutPosition levelParser >> ")" @[builtin_level_parser] def max := leading_parser nonReservedSymbol "max" true >> many1 (ppSpace >> levelParser maxPrec) @[builtin_level_parser] def imax := leading_parser diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index b173f706c0..4529fcff5f 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -30,19 +30,19 @@ namespace Syntax @[builtin_prec_parser] def numPrec := checkPrec maxPrec >> numLit @[builtin_syntax_parser] def paren := leading_parser - "(" >> many1 syntaxParser >> ")" + "(" >> withoutPosition (many1 syntaxParser) >> ")" @[builtin_syntax_parser] def cat := leading_parser ident >> optPrecedence @[builtin_syntax_parser] def unary := leading_parser - ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ")" + ident >> checkNoWsBefore >> "(" >> withoutPosition (many1 syntaxParser) >> ")" @[builtin_syntax_parser] def binary := leading_parser - ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ", " >> many1 syntaxParser >> ")" + ident >> checkNoWsBefore >> "(" >> withoutPosition (many1 syntaxParser >> ", " >> many1 syntaxParser) >> ")" @[builtin_syntax_parser] def sepBy := leading_parser - "sepBy(" >> many1 syntaxParser >> ", " >> strLit >> - optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep") >> ")" + "sepBy(" >> withoutPosition (many1 syntaxParser >> ", " >> strLit >> + optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep")) >> ")" @[builtin_syntax_parser] def sepBy1 := leading_parser - "sepBy1(" >> many1 syntaxParser >> ", " >> strLit >> - optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep") >> ")" + "sepBy1(" >> withoutPosition (many1 syntaxParser >> ", " >> strLit >> + optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep")) >> ")" @[builtin_syntax_parser] def atom := leading_parser strLit @[builtin_syntax_parser] def nonReserved := leading_parser diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 0a12609fc4..c326c994a6 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -159,7 +159,7 @@ def sufficesDecl := leading_parser withPosition ("suffices " >> sufficesDecl) >> optSemicolon termParser @[builtin_term_parser] def «show» := leading_parser:leadPrec "show " >> termParser >> ppSpace >> showRhs def structInstArrayRef := leading_parser - "[" >> termParser >>"]" + "[" >> withoutPosition termParser >>"]" def structInstLVal := leading_parser (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef) @@ -180,10 +180,10 @@ The structure type can be specified if not inferable: `{ x := 1, y := 2 : Point }`. -/ @[builtin_term_parser] def structInst := leading_parser - "{" >> ppHardSpace >> optional (atomic (sepBy1 termParser ", " >> " with ")) + "{" >> withoutPosition (ppHardSpace >> optional (atomic (sepBy1 termParser ", " >> " with ")) >> sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true) >> optEllipsis - >> optional (" : " >> termParser) >> " }" + >> optional (" : " >> termParser)) >> " }" def typeSpec := leading_parser " : " >> termParser def optType : Parser := optional typeSpec /-- @@ -197,7 +197,7 @@ def optType : Parser := optional typeSpec In contrast to regular patterns, `e` may be an arbitrary term of the appropriate type. -/ @[builtin_term_parser] def inaccessible := leading_parser - ".(" >> termParser >> ")" + ".(" >> withoutPosition termParser >> ")" def binderIdent : Parser := ident <|> hole def binderType (requireType := false) : Parser := if requireType then node nullKind (" : " >> termParser) else optional (" : " >> termParser) @@ -206,13 +206,13 @@ def binderTactic := leading_parser def binderDefault := leading_parser " := " >> termParser def explicitBinder (requireType := false) := ppGroup $ leading_parser - "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")" + "(" >> withoutPosition (many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault)) >> ")" /-- Implicit binder. In regular applications without `@`, it is automatically inserted and solved by unification whenever all explicit parameters before it are specified. -/ def implicitBinder (requireType := false) := ppGroup $ leading_parser - "{" >> many1 binderIdent >> binderType requireType >> "}" + "{" >> withoutPosition (many1 binderIdent >> binderType requireType) >> "}" def strictImplicitLeftBracket := atomic (group (symbol "{" >> "{")) <|> "⦃" def strictImplicitRightBracket := atomic (group (symbol "}" >> "}")) <|> "⦄" /-- @@ -228,7 +228,7 @@ Instance-implicit binder. In regular applications without `@`, it is automatical and solved by typeclass inference of the specified class. -/ def instBinder := ppGroup <| leading_parser - "[" >> optIdent >> termParser >> "]" + "[" >> withoutPosition (optIdent >> termParser) >> "]" def bracketedBinder (requireType := false) := withAntiquot (mkAntiquot "bracketedBinder" decl_name% (isPseudoKind := true)) <| explicitBinder requireType <|> strictImplicitBinder requireType <|> @@ -286,7 +286,7 @@ def generalizingParam := leading_parser def motive := leading_parser atomic ("(" >> nonReservedSymbol "motive" >> " := ") >> - termParser >> ")" >> ppSpace + withoutPosition termParser >> ")" >> ppSpace /-- Pattern matching. `match e, ... with | p, ... => f | ...` matches each given @@ -461,7 +461,7 @@ def attrKind := leading_parser optional («scoped» <|> «local») def attrInstance := ppGroup $ leading_parser attrKind >> attrParser def attributes := leading_parser - "@[" >> sepBy1 attrInstance ", " >> "]" + "@[" >> withoutPosition (sepBy1 attrInstance ", ") >> "]" def letRecDecl := leading_parser optional Command.docComment >> optional «attributes» >> letDecl def letRecDecls := leading_parser @@ -544,7 +544,7 @@ We use them to implement `macro_rules` and `elab_rules` "no_error_if_unused%" >> termParser def namedArgument := leading_parser (withAnonymousAntiquot := false) - atomic ("(" >> ident >> " := ") >> termParser >> ")" + atomic ("(" >> ident >> " := ") >> withoutPosition termParser >> ")" def ellipsis := leading_parser (withAnonymousAntiquot := false) ".." def argument := checkWsBefore "expected space" >> @@ -646,7 +646,7 @@ def macroLastArg := macroDollarArg <|> macroArg "StateRefT" >> macroArg >> macroLastArg @[builtin_term_parser] def dynamicQuot := leading_parser - "`(" >> ident >> "|" >> incQuotDepth (parserOfStack 1) >> ")" + "`(" >> ident >> "|" >> withoutPosition (incQuotDepth (parserOfStack 1)) >> ")" @[builtin_term_parser] def dotIdent := leading_parser "." >> checkNoWsBefore >> rawIdent @@ -654,9 +654,9 @@ def macroLastArg := macroDollarArg <|> macroArg end Term @[builtin_term_parser default+1] def Tactic.quot : Parser := leading_parser - "`(tactic|" >> incQuotDepth tacticParser >> ")" + "`(tactic|" >> withoutPosition (incQuotDepth tacticParser) >> ")" @[builtin_term_parser] def Tactic.quotSeq : Parser := leading_parser - "`(tactic|" >> incQuotDepth Tactic.seq1 >> ")" + "`(tactic|" >> withoutPosition (incQuotDepth Tactic.seq1) >> ")" open Term in builtin_initialize