diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean index 07d664c455..7c007a3513 100644 --- a/library/init/lean/parser/command.lean +++ b/library/init/lean/parser/command.lean @@ -29,11 +29,11 @@ def docComment := parser! "/--" >> commentBody def attrArg : Parser := ident <|> strLit <|> numLit def attrInstance := parser! ident >> many attrArg def attributes := parser! "@[" >> sepBy1 attrInstance ", " >> "]" -def «private» := parser! "private" -def «protected» := parser! "protected" +def «private» := parser! "private " +def «protected» := parser! "protected " def visibility := «private» <|> «protected» -def «noncomputable» := parser! "noncomputable" -def «unsafe» := parser! "unsafe" +def «noncomputable» := parser! " noncomputable " +def «unsafe» := parser! " unsafe " def declModifiers := parser! optional docComment >> optional «attributes» >> optional visibility >> optional «noncomputable» >> optional «unsafe» def declId := parser! ident >> optional (".{" >> sepBy1 ident ", " >> "}") def declSig := parser! many Term.bracktedBinder >> Term.typeSpec @@ -48,9 +48,23 @@ def «constant» := parser! "constant " >> declId >> declSig >> optional d def «instance» := parser! "instance " >> optional declId >> declSig >> declVal def «axiom» := parser! "axiom " >> declId >> declSig def «example» := parser! "example " >> declSig >> declVal +def relaxedInferMod := parser! "{" >> "}" +def strictInferMod := parser! "(" >> ")" +def inferMod := relaxedInferMod <|> strictInferMod +def introRule := parser! " | " >> ident >> optional inferMod >> optDeclSig +def «inductive» := parser! "inductive " >> declId >> optDeclSig >> many introRule +def structExplicitBinder := parser! "(" >> many ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")" +def structImplicitBinder := parser! "{" >> many ident >> optional inferMod >> optDeclSig >> "}" +def structInstBinder := parser! "[" >> many ident >> optional inferMod >> optDeclSig >> "]" +def structFields := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder) +def structCtor := parser! 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.bracktedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields -@[builtinCommandParser] def declaration := -declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example») +@[builtinCommandParser] def declaration := parser! +declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> «structure») end Command diff --git a/tests/playground/cmdparsertest1.lean b/tests/playground/cmdparsertest1.lean index a34bbd9307..877edbcb85 100644 --- a/tests/playground/cmdparsertest1.lean +++ b/tests/playground/cmdparsertest1.lean @@ -22,5 +22,9 @@ test [ "protected def length.{u} {α : Type u} : List α → Nat | [] := 0 | (a::as) := 1 + length as", -"/-- doc string test -/ private theorem bla (x : Nat) : x = x := Eq.refl x" +"/-- doc string test -/ private theorem bla (x : Nat) : x = x := Eq.refl x", +"class Alternative (f : Type u → Type v) extends Applicative f : Type (max (u+1) v) := +(failure : ∀ {α : Type u}, f α) +(orelse : ∀ {α : Type u}, f α → f α → f α) +" ]