max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update Lean version + adapt to TSyntax

Browse source
This commit is contained in:
tydeu 2022-06-30 19:24:18 -04:00
parent 74f3e963ff
commit 24fd2e37e1
7 changed files with 61 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/DSL/Config.lean
View file

@ -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]

26
Lake/DSL/DeclUtil.lean
View file

@ -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

26
Lake/DSL/Package.lean
View file

@ -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"

12
Lake/DSL/Script.lean
View file

@ -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"

12
Lake/DSL/Targets.lean
View file

@ -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"

18
Lake/Util/Name.lean
View file

@ -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 ()

2
lean-toolchain
View file

@ -1 +1 @@
leanprover/lean4:nightly-2022-06-17
leanprover/lean4:nightly-2022-06-30