From 24fd2e37e128d428d9d7f3a7e85fc7fc383fbb20 Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 30 Jun 2022 19:24:18 -0400 Subject: [PATCH] chore: update Lean version + adapt to `TSyntax` --- Lake/DSL/Config.lean | 2 +- Lake/DSL/DeclUtil.lean | 26 +++++++++++++++++++++++++- Lake/DSL/Package.lean | 26 +++++++++++++------------- Lake/DSL/Script.lean | 12 ++++++------ Lake/DSL/Targets.lean | 12 ++++++------ Lake/Util/Name.lean | 18 +++++++++--------- lean-toolchain | 2 +- 7 files changed, 61 insertions(+), 37 deletions(-) diff --git a/Lake/DSL/Config.lean b/Lake/DSL/Config.lean index 0e1c16e165..811b6efa15 100644 --- a/Lake/DSL/Config.lean +++ b/Lake/DSL/Config.lean @@ -48,7 +48,7 @@ scoped syntax (name := argsConst) "__args__" :term def elabArgsConst : TermElab := fun stx expectedType? => do let exp := if let some args := argsExt.getState (← getEnv) then - quote args + quote (k := `term) args else -- `id` app forces Lean to show macro's doc rather than the constant's Syntax.mkApp (mkCIdentFrom stx ``id) #[mkCIdentFrom stx ``dummyArgs] diff --git a/Lake/DSL/DeclUtil.lean b/Lake/DSL/DeclUtil.lean index 4f6655e879..f0d03e18de 100644 --- a/Lake/DSL/DeclUtil.lean +++ b/Lake/DSL/DeclUtil.lean @@ -8,6 +8,30 @@ import Lean.Parser.Command namespace Lake.DSL open Lean Parser Command +abbrev DocComment := TSyntax ``docComment +abbrev Attributes := TSyntax ``Term.attributes +abbrev AttrInstance := TSyntax ``Term.attrInstance +abbrev WhereDecls := TSyntax ``Term.whereDecls + +abbrev Hole := TSyntax ``Term.hole +abbrev BinderIdent := TSyntax ``Term.binderIdent +abbrev SimpleBinder := TSyntax ``Term.simpleBinder +abbrev FunBinder := TSyntax ``Term.funBinder + +instance : Coe Hole BinderIdent where + coe s := ⟨s.raw⟩ + +instance : Coe Ident BinderIdent where + coe s := ⟨s.raw⟩ + +instance : Coe BinderIdent SimpleBinder where + coe s := ⟨s.raw⟩ + +instance : Coe SimpleBinder FunBinder where + coe s := ⟨s.raw⟩ + +--- + syntax structVal := "{" manyIndent(group(Term.structInstField ", "?)) "}" @@ -23,7 +47,7 @@ syntax declValTyped := syntax declValOptTyped := (Term.typeSpec)? declValSimple -def expandAttrs (attrs? : Option Syntax) : Array Syntax := +def expandAttrs (attrs? : Option Attributes) : Array AttrInstance := if let some attrs := attrs? then match attrs with | `(Term.attributes| @[$attrs,*]) => attrs diff --git a/Lake/DSL/Package.lean b/Lake/DSL/Package.lean index 010d046f34..c9ad45a628 100644 --- a/Lake/DSL/Package.lean +++ b/Lake/DSL/Package.lean @@ -19,34 +19,34 @@ syntax packageDeclSpec := ident (Command.whereStructInst <|> declValTyped <|> packageDeclWithBinders)? def expandPackageBinders -: (dir? : Option Syntax) → (args? : Option Syntax) → MacroM (Bool × Syntax × Syntax) -| none, none => do let hole ← `(_); return (false, hole, hole) -| some dir, none => return (true, dir, ← `(_)) -| none, some args => return (true, ← `(_), args) +: Option SimpleBinder → Option SimpleBinder → MacroM (Bool × SimpleBinder × SimpleBinder) +| none, none => do let hole ← `(Term.hole|_); return (false, hole, hole) +| some dir, none => return (true, dir, ← `(Term.hole|_)) +| none, some args => return (true, ← `(Term.hole|_), args) | some dir, some args => return (true, dir, args) def mkSimplePackageDecl -(doc? : Option Syntax) (attrs : Array Syntax) (id : Syntax) (defn : Syntax) -(dir? : Option Syntax) (args? : Option Syntax) (wds? : Option Syntax) : MacroM Syntax := do +(doc? : Option DocComment) (attrs : Array AttrInstance) (id : Ident) (defn : Term) +(dir? : Option SimpleBinder) (args? : Option SimpleBinder) (wds? : Option WhereDecls) : MacroM Syntax := do let (hasBinders, dir, args) ← expandPackageBinders dir? args? if hasBinders then - `($[$doc?:docComment]? @[$attrs,*] def $id : Packager := + `($[$doc?]? @[$attrs,*] def $id : Packager := (fun $dir $args => $defn) $[$wds?]?) else - `($[$doc?:docComment]? @[$attrs,*] def $id : PackageConfig := $defn $[$wds?]?) + `($[$doc?]? @[$attrs,*] def $id : PackageConfig := $defn $[$wds?]?) /-- The name given to the definition created by the `package` syntax. -/ def packageDeclName := `_package -def mkPackageDecl (doc? : Option Syntax) (attrs : Array Syntax) : Macro +def mkPackageDecl (doc? : Option DocComment) (attrs : Array AttrInstance) : Macro | `(packageDeclSpec| $id:ident) => - `($[$doc?:docComment]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : PackageConfig := + `($[$doc?]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : PackageConfig := {name := $(quote id.getId)}) | `(packageDeclSpec| $id:ident where $ds;* $[$wds?]?) => - `($[$doc?:docComment]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : PackageConfig where + `($[$doc?]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : PackageConfig where name := $(quote id.getId); $ds;* $[$wds?]?) | `(packageDeclSpec| $id:ident : $ty := $defn $[$wds?]?) => - `($[$doc?:docComment]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : $ty := $defn $[$wds?]?) + `($[$doc?]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : $ty := $defn $[$wds?]?) | `(packageDeclSpec| $id:ident $[($dir?)]? $[($args?)]? := $defn $[$wds?]?) => mkSimplePackageDecl doc? attrs (mkIdentFrom id packageDeclName) defn dir? args? wds? | `(packageDeclSpec| $id:ident $[($dir?)]? $[($args?)]? { $[$fs $[,]?]* } $[$wds?]?) => do @@ -54,7 +54,7 @@ def mkPackageDecl (doc? : Option Syntax) (attrs : Array Syntax) : Macro mkSimplePackageDecl doc? attrs (mkIdentFrom id packageDeclName) defn dir? args? wds? | `(packageDeclSpec| $id:ident $[($dir?)]? $[($args?)]? do $seq $[$wds?]?) => do let (_, dir, args) ← expandPackageBinders dir? args? - `($[$doc?:docComment]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : IOPackager := + `($[$doc?]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : IOPackager := (fun $dir $args => do $seq) $[$wds?]?) | stx => Macro.throwErrorAt stx "ill-formed package declaration" diff --git a/Lake/DSL/Script.lean b/Lake/DSL/Script.lean index dabf23c6bc..be4f59f085 100644 --- a/Lake/DSL/Script.lean +++ b/Lake/DSL/Script.lean @@ -18,10 +18,10 @@ scoped syntax (name := scriptDecl) @[macro scriptDecl] def expandScriptDecl : Macro -| `($[$doc?:docComment]? script $id:ident $[($args?)]? do $seq $[$wds?]?) => do - let args := args?.getD (← `(_)) - `($[$doc?:docComment]? @[«script»] def $id : ScriptFn := fun $args => do $seq $[$wds?]?) -| `($[$doc?:docComment]? script $id:ident $[($args?)]? := $defn $[$wds?]?) => do - let args := args?.getD (← `(_)) - `($[$doc?:docComment]? @[«script»] def $id : ScriptFn := fun $args => $defn $[$wds?]?) +| `($[$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?]?) | stx => Macro.throwErrorAt stx "ill-formed script declaration" diff --git a/Lake/DSL/Targets.lean b/Lake/DSL/Targets.lean index 62aa2222f2..8018852d3d 100644 --- a/Lake/DSL/Targets.lean +++ b/Lake/DSL/Targets.lean @@ -20,19 +20,19 @@ syntax targetDeclSpec := ident (Command.whereStructInst <|> declValOptTyped <|> declValStruct)? def mkTargetDecl -(doc? : Option Syntax) (attrs : Array Syntax) (ty : Syntax) +(doc? : Option DocComment) (attrs : Array AttrInstance) (ty : Term) : (spec : Syntax) → MacroM Syntax | `(targetDeclSpec| $id:ident) => - `($[$doc?:docComment]? @[$attrs,*] def $id : $ty := + `($[$doc?]? @[$attrs,*] def $id : $ty := {name := $(quote id.getId)}) | `(targetDeclSpec| $id:ident where $ds;* $[$wds?]?) => - `($[$doc?:docComment]? @[$attrs,*] def $id : $ty where + `($[$doc?]? @[$attrs,*] def $id : $ty where name := $(quote id.getId); $ds;* $[$wds?]?) | `(targetDeclSpec| $id:ident $[: $ty?]? := $defn $[$wds?]?) => - `($[$doc?:docComment]? @[$attrs,*] def $id : $(ty?.getD ty) := $defn $[$wds?]?) + `($[$doc?]? @[$attrs,*] def $id : $(ty?.getD ty) := $defn $[$wds?]?) | `(targetDeclSpec| $id:ident { $[$fs $[,]?]* } $[$wds?]?) => do let defn ← `({ name := $(quote id.getId), $fs,* }) - `($[$doc?:docComment]? @[$attrs,*] def $id : $ty := $defn $[$wds?]?) + `($[$doc?]? @[$attrs,*] def $id : $ty := $defn $[$wds?]?) | stx => Macro.throwErrorAt stx "ill-formed target declaration" /-- @@ -97,6 +97,6 @@ doc?:optional(docComment) attrs?:optional(Term.attributes) let attr ← `(Term.attrInstance| externLib) let ty := ty?.getD <| mkCIdentFrom (← getRef) ``ExternLibConfig let attrs := #[attr] ++ expandAttrs attrs? - `($[$doc?:docComment]? @[$attrs,*] def $id : $ty := + `($[$doc?]? @[$attrs,*] def $id : $ty := {name := $(quote id.getId), target := $defn} $[$wds?]?) | stx => Macro.throwErrorAt stx "ill-formed external library declaration" diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean index cc1acba6b0..6bd9378af7 100644 --- a/Lake/Util/Name.lean +++ b/Lake/Util/Name.lean @@ -258,7 +258,7 @@ instance : EqOfCmp WfName WfName.quickCmp where eq_of_cmp h := WfName.eq_of_quickCmp h open Syntax in -protected def quoteFrom (ref : Syntax) : WfName → Syntax +protected def quoteFrom (ref : Syntax) : WfName → Term | ⟨n, w⟩ => match n with | .anonymous => mkCIdentFrom ref ``anonymous | .str p s _ => mkApp (mkCIdentFrom ref ``mkStr) @@ -280,7 +280,7 @@ instead of their plain counterparts. Well-formed names have additional properties that help ensure certain features of Lake work as intended. -/ scoped macro:max (name := wfNameLit) "&" noWs stx:name : term => - if let some nm := stx.isNameLit? then + if let some nm := stx.raw.isNameLit? then return WfName.quoteFrom stx <| WfName.ofName nm else Macro.throwErrorAt stx "ill-formed name literal" @@ -290,12 +290,12 @@ scoped notation "&`✝" => WfName.anonymous @[scoped appUnexpander WfName.mkStr] def unexpandWfNameMkStr : PrettyPrinter.Unexpander | `($(_) &`✝ $s) => do - let some s := s.isStrLit? | throw () - let qn := quote <| Name.mkStr Name.anonymous s - `(&$(qn[0]):name) + let some s := s.raw.isStrLit? | throw () + let qn := quote (k := `term) <| Name.mkStr Name.anonymous s + `(&$(⟨qn.raw[0]⟩):name) | `($(_) &$n:name $s) => do - let some s := s.isStrLit? | throw () - let some n := n.isNameLit? | throw () - let qn := quote <| Name.mkStr n s - `(&$(qn[0]):name) + let some s := s.raw.isStrLit? | throw () + let some n := n.raw.isNameLit? | throw () + let qn := quote (k := `term) <| Name.mkStr n s + `(&$(⟨qn.raw[0]⟩):name) | _ => throw () diff --git a/lean-toolchain b/lean-toolchain index 7d896509d5..3a15cf8e75 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-06-17 +leanprover/lean4:nightly-2022-06-30