chore: adapt to simpleBinder removal

Author: Kha

Diff for: Lake/DSL/Script.lean

@@ -11,17 +11,17 @@ namespace Lake.DSL
 open Lean Parser Command
 
 syntax scriptDeclSpec :=
-  ident (ppSpace "(" Term.simpleBinder ")")? (declValSimple <|> declValDo)
+  ident (ppSpace "(" ident+ ")")? (declValSimple <|> declValDo)
 
 scoped syntax (name := scriptDecl)
 (docComment)? "script " scriptDeclSpec : command
 
 @[macro scriptDecl]
 def expandScriptDecl : Macro
-| `($[$doc?]? script $id:ident $[($args?)]? do $seq $[$wds?]?) => do
-  let args := args?.getD (← `(Term.hole|_))
-  `($[$doc?]? @[«script»] def $id : ScriptFn := fun $args => do $seq $[$wds?]?)
-| `($[$doc?]? script $id:ident $[($args?)]? := $defn $[$wds?]?) => do
-  let args := args?.getD (← `(Term.hole|_))
-  `($[$doc?]? @[«script»] def $id : ScriptFn := fun $args => $defn $[$wds?]?)
+| `($[$doc?]? script $id:ident $[($args?*)]? do $seq $[$wds?]?) => do
+  let args := args?.getD (α := Array FunBinder) #[← `(Term.hole|_)]
+  `($[$doc?]? @[«script»] def $id : ScriptFn := fun $args* => do $seq $[$wds?]?)
+| `($[$doc?]? script $id:ident $[($args?*)]? := $defn $[$wds?]?) => do
+  let args := args?.getD (α := Array FunBinder) #[← `(Term.hole|_)]
+  `($[$doc?]? @[«script»] def $id : ScriptFn := fun $args* => $defn $[$wds?]?)
 | stx => Macro.throwErrorAt stx "ill-formed script declaration"

Diff for: Lake/Util/Binder.lean

@@ -39,24 +39,18 @@ instance : Coe Hole BinderIdent where
 instance : Coe Ident BinderIdent where
   coe s := ⟨s.raw⟩
 
-abbrev SimpleBinder := TSyntax ``Term.simpleBinder
 abbrev BracketedBinder := TSyntax ``Term.bracketedBinder
 abbrev FunBinder := TSyntax ``Term.funBinder
 
-instance : Coe BinderIdent SimpleBinder where
-  coe s := ⟨s.raw⟩
-
-instance : Coe SimpleBinder FunBinder where
+instance : Coe BinderIdent FunBinder where
   coe s := ⟨s.raw⟩
 
 @[runParserAttributeHooks]
-def declBinder := Term.simpleBinderWithoutType <|> Term.bracketedBinder
-abbrev DeclBinder := TSyntax ``declBinder
-
-abbrev Binder := TSyntax [``Term.simpleBinder, ``Term.bracketedBinder]
+def binder := Term.binderIdent <|> Term.bracketedBinder
 
-instance : Coe DeclBinder Binder where
-  coe s := ⟨s.raw⟩
+abbrev Binder := TSyntax ``binder
+instance : Coe Binder (TSyntax [identKind, ``Term.hole, ``Term.bracketedBinder]) where
+  coe stx := ⟨stx.raw⟩
 
 abbrev BinderModifier := TSyntax [``Term.binderTactic, ``Term.binderDefault]
 
@@ -102,15 +96,9 @@ def expandBinderModifier (optBinderModifier : Syntax) : Option BinderModifier :=
 
 def matchBinder (stx : Syntax) : MacroM (Array BinderSyntaxView) := do
   let k := stx.getKind
-  if k == ``Lean.Parser.Term.simpleBinder then
-    -- binderIdent+ >> optType
-    let ids ← getBinderIds stx[0]
-    let optType := stx[1]
-    ids.mapM fun id => return {
-      id := (← expandBinderIdent id),
-      type := expandOptType id optType,
-      info := .default
-    }
+  if stx.isIdent || k == ``Term.hole then
+    -- binderIdent
+    return #[{ id := (← expandBinderIdent stx), type := mkHoleFrom stx, info := .default }]
   else if k == ``Lean.Parser.Term.explicitBinder then
     -- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)`
     let ids ← getBinderIds stx[1]
@@ -153,16 +141,16 @@ def matchBinder (stx : Syntax) : MacroM (Array BinderSyntaxView) := do
 def BinderSyntaxView.mkBinder : BinderSyntaxView → MacroM Binder
 | {id, type, info, modifier?} => do
   match info with
-  | .default        => `(declBinder| ($id : $type $[$modifier?]?))
-  | .implicit       => `(declBinder| {$id : $type})
-  | .strictImplicit => `(declBinder| ⦃$id : $type⦄)
-  | .instImplicit   => `(declBinder| [$id : $type])
+  | .default        => `(binder| ($id : $type $[$modifier?]?))
+  | .implicit       => `(binder| {$id : $type})
+  | .strictImplicit => `(binder| ⦃$id : $type⦄)
+  | .instImplicit   => `(binder| [$id : $type])
   | _               => unreachable!
 
 def BinderSyntaxView.mkArgument : BinderSyntaxView → MacroM NamedArgument
 | {id, ..} => `(Term.namedArgument| ($id := $id))
 
-def expandBinders (dbs : Array DeclBinder) : MacroM (Array Binder × Array Term) := do
+def expandBinders (dbs : Array Binder) : MacroM (Array Binder × Array Term) := do
   let mut bs := #[]
   let mut args : Array Term := #[]
   for db in dbs do

Diff for: Lake/Util/Opaque.lean

@@ -17,8 +17,8 @@ namespace Lake
 open Lean Parser Command
 
 macro (name := declareOpaqueType)
-doc?:optional(docComment)  "declare_opaque_type " id:ident dbs:declBinder* : command => do
-  let (bs, args) ← expandBinders dbs
+doc?:optional(docComment)  "declare_opaque_type " id:ident bs:binder* : command => do
+  let (bs, args) ← expandBinders bs
   let nonemptyTypeId := id.getId.modifyBase (· ++ `nonemptyType)
   let nonemptyType := mkIdentFrom id nonemptyTypeId
   let nonemptyTypeApp := Syntax.mkApp nonemptyType args