From 5585f9823f8682cb4bd70d501fb95a78b7e14ba7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Nov 2020 13:05:18 -0800 Subject: [PATCH] chore: cleaner `structure/class` syntax @Kha I implemented the syntax for structure/class that we discussed this morning. It is much cleaner. See new tests at `struct2.lean`. I updated the documentation to use it. --- doc/functions.md | 6 ++-- doc/lean3changes.md | 6 ++-- doc/stringinterp.md | 6 ++-- doc/tour.md | 2 +- src/Lean/Elab/Structure.lean | 15 ++++++---- src/Lean/Parser/Command.lean | 11 +++++--- tests/lean/run/struct2.lean | 53 ++++++++++++++++++++++++++++++++++-- 7 files changed, 77 insertions(+), 22 deletions(-) diff --git a/doc/functions.md b/doc/functions.md index 43d27f7c15..a613b2658c 100644 --- a/doc/functions.md +++ b/doc/functions.md @@ -26,9 +26,9 @@ the function body is `x + 1`, and the return value is of type `Nat`. The following example defines the factorial recursive function using pattern matching. ```lean def fact x := - match x with - | 0 => 1 - | n+1 => (n+1) * fact n + match x with + | 0 => 1 + | n+1 => (n+1) * fact n #eval fact 100 ``` diff --git a/doc/lean3changes.md b/doc/lean3changes.md index 522bb37f34..3ad28c51ff 100644 --- a/doc/lean3changes.md +++ b/doc/lean3changes.md @@ -24,8 +24,8 @@ In Lean 4, one can easily create new notation that abbreviates commonly used idi def Prod.str : Nat × Nat → String := fun (a, b) => "(" ++ toString a ++ ", " ++ toString b ++ ")" -structure Point := - (x y z : Nat) +structure Point where + x y z : Nat def Point.addX : Point → Point → Nat := fun { x := a, .. } { x := b, .. } => a+b @@ -173,7 +173,7 @@ example (x y : α) : g x y = fun (c : α) => x + y + c := rfl In Lean 4, we can use `..` to provide missing explicit arguments as `_`. This feature combined with named arguments is useful for writing patterns. Here is an example: ```lean -inductive Term +inductive Term where | var (name : String) | num (val : Nat) | add (fn : Term) (arg : Term) diff --git a/doc/stringinterp.md b/doc/stringinterp.md index 2fb79a04e9..b40e87ea64 100644 --- a/doc/stringinterp.md +++ b/doc/stringinterp.md @@ -41,9 +41,9 @@ def vals := [1, 2, 3] You can define a `ToString` instance for your own datatypes. ```lean -structure Person := - (name : String) - (age : Nat) +structure Person where + name : String + age : Nat instance : ToString Person where toString : Person -> String diff --git a/doc/tour.md b/doc/tour.md index 5f185f2a05..bed333a73a 100644 --- a/doc/tour.md +++ b/doc/tour.md @@ -84,7 +84,7 @@ theorem twiceAdd2 (a : Nat) : twice (fun x => x + 2) a = a + 4 := -- An enumerated type is a special case of inductive type in Lean -- The following command creates a new type `Weekday` -inductive Weekday := +inductive Weekday where | sunday : Weekday | monday : Weekday | tuesday : Weekday diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index a8ea809859..da2f69985c 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -135,15 +135,20 @@ def checkValidFieldModifier (modifiers : Modifiers) : CommandElabM Unit := do /- ``` -def structExplicitBinder := parser! try (declModifiers >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")" -def structImplicitBinder := parser! try (declModifiers >> "{") >> many1 ident >> optional inferMod >> declSig >> "}" -def structInstBinder := parser! try (declModifiers >> "[") >> many1 ident >> optional inferMod >> declSig >> "]" +def structExplicitBinder := parser! atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")" +def structImplicitBinder := parser! atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}" +def structInstBinder := parser! atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]" +def structSimpleBinder := parser! atomic (declModifiers true >> many1 ident) >> optional inferMod >> optDeclSig >> optional Term.binderDefault def structFields := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder) ``` -/ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : CommandElabM (Array StructFieldView) := let fieldBinders := if structStx[5].isNone then #[] else structStx[5][2][0].getArgs fieldBinders.foldlM (init := #[]) fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do + let mut fieldBinder := fieldBinder + if fieldBinder.getKind == `Lean.Parser.Command.structSimpleBinder then + fieldBinder := Syntax.node `Lean.Parser.Command.structExplicitBinder + #[ fieldBinder[0], mkAtomFrom fieldBinder "(", fieldBinder[1], fieldBinder[2], fieldBinder[3], fieldBinder[4], mkAtomFrom fieldBinder ")" ] let k := fieldBinder.getKind let binfo ← if k == `Lean.Parser.Command.structExplicitBinder then pure BinderInfo.default @@ -178,12 +183,12 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str throwError! "invalid field name '{name}', identifiers starting with '_' are reserved to the system" let declName := structDeclName ++ name let declName ← applyVisibility fieldModifiers.visibility declName - pure $ views.push { + return views.push { ref := ident, modifiers := fieldModifiers, binderInfo := binfo, inferMod := inferMod, - declName := declName, + declName := declName, name := name, binders := binders, type? := type?, diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 4226a17a60..9a29d49b4e 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -47,17 +47,20 @@ def «axiom» := parser! "axiom " >> declId >> declSig def «example» := parser! "example " >> declSig >> declVal def inferMod := parser! atomic ("{" >> "}") def ctor := parser! "\n| " >> declModifiers true >> ident >> optional inferMod >> optDeclSig -def «inductive» := parser! "inductive " >> declId >> optDeclSig >> optional ":=" >> many ctor -def classInductive := parser! atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ":=" >> many ctor +def «inductive» := parser! "inductive " >> declId >> optDeclSig >> optional (":=" <|> "where") >> many ctor +def classInductive := parser! atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional (":=" <|> "where") >> many ctor def structExplicitBinder := parser! atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")" def structImplicitBinder := parser! atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}" def structInstBinder := parser! atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]" -def structFields := parser! many (ppLine >> (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)) +def structSimpleBinder := parser! atomic (declModifiers true >> many1 ident) >> optional inferMod >> optDeclSig >> optional Term.binderDefault +def structFields := parser! manyIndent (ppLine >> checkColGe >>(structExplicitBinder <|> structImplicitBinder <|> structInstBinder <|> structSimpleBinder)) def structCtor := parser! atomic (declModifiers true >> ident >> optional inferMod >> " :: ") def structureTk := parser! "structure " def classTk := parser! "class " def «extends» := parser! " extends " >> sepBy1 termParser ", " -def «structure» := parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> optional (" := " >> optional structCtor >> structFields) +def «structure» := parser! + (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType + >> optional ((" := " <|> " where ") >> optional structCtor >> structFields) @[builtinCommandParser] def declaration := parser! declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure») diff --git a/tests/lean/run/struct2.lean b/tests/lean/run/struct2.lean index 8d4b1b0817..758f88e9e2 100644 --- a/tests/lean/run/struct2.lean +++ b/tests/lean/run/struct2.lean @@ -1,6 +1,4 @@ - - -universe u +universes u v w structure A (α : Type u) := (f : (β : Type u) → α → β → α) @@ -14,3 +12,52 @@ structure B (α : Type u) extends A α := #check B.f._default #check { x := 10 : B Nat} + +namespace New + +structure A (α : Type u) where + f : (β : Type u) → α → β → α + +structure B (α : Type u) extends A α where + x : Nat + f := fun β a b => a + +#check B.f._default + +#check { x := 10 : B Nat } + +structure Data where + index? : Option Nat := none + lowlink? : Option Nat := none + onStack : Bool := false + +structure State (α : Type) where + stack : List α := [] + nextIndex : Nat := 0 + data : Array Data := #[] + sccs : List (List α) := [] + +inductive Format where + | nil : Format + | line : Format + | text : String → Format + | nest (indent : Int) : Format → Format + | append : Format → Format → Format + | group : Format → Format + +class MonadControl (m : Type u → Type v) (n : Type u → Type w) where + stM : Type u → Type u + liftWith {α} : (({β : Type u} → n β → m (stM β)) → m α) → n α + restoreM {α} : m (stM α) → n α + +instance : MonadControl m (ReaderT ρ m) where + stM := id + liftWith f := fun ctx => f fun x => x ctx + restoreM x := fun ctx => x + +instance [Monad m] : MonadControl m (StateT σ m) where + stM α := α × σ + liftWith f := do let s ← get; liftM (f (fun x => x.run s)) + restoreM x := do let (a, s) ← liftM x; set s; pure a + +end New