From 6f075e6ecefa5eea2ad82ac9f54b7267e3400ca7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Sep 2021 16:57:03 -0700 Subject: [PATCH] feat: add `enum` command for declaring enumeration types closes #654 --- src/Init.lean | 1 + src/Init/Enum.lean | 35 +++ src/Lean/Data/Lsp/LanguageFeatures.lean | 2 +- tests/lean/run/654.lean | 289 ++++++++++++++++++++++++ tests/lean/run/manyAritySyntax.lean | 4 +- 5 files changed, 328 insertions(+), 3 deletions(-) create mode 100644 src/Init/Enum.lean create mode 100644 tests/lean/run/654.lean diff --git a/src/Init.lean b/src/Init.lean index 54741d4ed8..b636f37730 100644 --- a/src/Init.lean +++ b/src/Init.lean @@ -19,3 +19,4 @@ import Init.NotationExtra import Init.SimpLemmas import Init.Hints import Init.Conv +import Init.Enum diff --git a/src/Init/Enum.lean b/src/Init/Enum.lean new file mode 100644 index 0000000000..3561280e8d --- /dev/null +++ b/src/Init/Enum.lean @@ -0,0 +1,35 @@ +/- +Copyright (c) 2021 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.NotationExtra +import Init.Data.Range +import Init.Data.Stream + +/-- + Macro for declaring big enumeration types. It is more efficient than using `inductive`. + + It also generates the instances `BEq`, `DecidableEq`, `Inhabited`, and `Repr` for the new type +-/ +macro "enum " n:ident " where " cs:(group("| " ident))+ : command => open Lean in do + let cs := cs.getArgs + let numCtors := cs.size + let structDecl ← `(structure $n:ident where (val : Fin $(quote numCtors))) + let derivingCmd ← `(deriving instance BEq, DecidableEq, Inhabited for $n:ident) + let currNamespace ← Macro.getCurrNamespace + let mkCtorName (ctorDeclStx : Syntax) : Name := + n.getId ++ ctorDeclStx[1].getId + let mut ctorDefs := #[] + for c in cs, i in [:numCtors] do + let ctorName := mkCtorName c + let ctorDef ← `(@[matchPattern] abbrev $(mkIdentFrom c ctorName):ident : $n:ident := ⟨$(quote i)⟩) + ctorDefs := ctorDefs.push ctorDef + -- generate `Repr` instance + let ctorFmts ← cs.mapM fun c => + `(Std.format $(quote <| toString (currNamespace ++ mkCtorName c))) + let reprInst ← `( + def enumFmts : Array Std.Format := [ $(ctorFmts),*].toArray + instance : Repr $n := ⟨fun e _ => enumFmts[e.val.val]⟩) + return mkNullNode (#[structDecl, derivingCmd, reprInst] ++ ctorDefs) diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean index d5c02a452d..b95851d1f1 100644 --- a/src/Lean/Data/Lsp/LanguageFeatures.lean +++ b/src/Lean/Data/Lsp/LanguageFeatures.lean @@ -102,7 +102,7 @@ inductive SymbolKind where | property | field | constructor - | enum + | «enum» | interface | function | «variable» diff --git a/tests/lean/run/654.lean b/tests/lean/run/654.lean new file mode 100644 index 0000000000..53bf14659d --- /dev/null +++ b/tests/lean/run/654.lean @@ -0,0 +1,289 @@ +enum Foo where + | a | b | c + +def f : Foo → Nat + | Foo.a => 10 + | Foo.b => 20 + | Foo.c => 35 + +#eval Foo.b + +enum CXCursorKind where + | CXCursor_UnexposedDecl + | CXCursor_StructDecl + | CXCursor_UnionDecl + | CXCursor_ClassDecl + | CXCursor_EnumDecl + | CXCursor_FieldDecl + | CXCursor_EnumConstantDecl + | CXCursor_FunctionDecl + | CXCursor_VarDecl + | CXCursor_ParmDecl + | CXCursor_ObjCInterfaceDecl + | CXCursor_ObjCCategoryDecl + | CXCursor_ObjCProtocolDecl + | CXCursor_ObjCPropertyDecl + | CXCursor_ObjCIvarDecl + | CXCursor_ObjCInstanceMethodDecl + | CXCursor_ObjCClassMethodDecl + | CXCursor_ObjCImplementationDecl + | CXCursor_ObjCCategoryImplDecl + | CXCursor_TypedefDecl + | CXCursor_CXXMethod + | CXCursor_Namespace + | CXCursor_LinkageSpec + | CXCursor_Constructor + | CXCursor_Destructor + | CXCursor_ConversionFunction + | CXCursor_TemplateTypeParameter + | CXCursor_NonTypeTemplateParameter + | CXCursor_TemplateTemplateParameter + | CXCursor_FunctionTemplate + | CXCursor_ClassTemplate + | CXCursor_ClassTemplatePartialSpecialization + | CXCursor_NamespaceAlias + | CXCursor_UsingDirective + | CXCursor_UsingDeclaration + | CXCursor_TypeAliasDecl + | CXCursor_ObjCSynthesizeDecl + | CXCursor_ObjCDynamicDecl + | CXCursor_CXXAccessSpecifier + | CXCursor_FirstDecl + | CXCursor_LastDecl + | CXCursor_FirstRef + | CXCursor_ObjCSuperClassRef + | CXCursor_ObjCProtocolRef + | CXCursor_ObjCClassRef + | CXCursor_TypeRef + | CXCursor_CXXBaseSpecifier + | CXCursor_TemplateRef + | CXCursor_NamespaceRef + | CXCursor_MemberRef + | CXCursor_LabelRef + | CXCursor_OverloadedDeclRef + | CXCursor_VariableRef + | CXCursor_LastRef + | CXCursor_FirstInvalid + | CXCursor_InvalidFile + | CXCursor_NoDeclFound + | CXCursor_NotImplemented + | CXCursor_InvalidCode + | CXCursor_LastInvalid + | CXCursor_FirstExpr + | CXCursor_UnexposedExpr + | CXCursor_DeclRefExpr + | CXCursor_MemberRefExpr + | CXCursor_CallExpr + | CXCursor_ObjCMessageExpr + | CXCursor_BlockExpr + | CXCursor_IntegerLiteral + | CXCursor_FloatingLiteral + | CXCursor_ImaginaryLiteral + | CXCursor_StringLiteral + | CXCursor_CharacterLiteral + | CXCursor_ParenExpr + | CXCursor_UnaryOperator + | CXCursor_ArraySubscriptExpr + | CXCursor_BinaryOperator + | CXCursor_CompoundAssignOperator + | CXCursor_ConditionalOperator + | CXCursor_CStyleCastExpr + | CXCursor_CompoundLiteralExpr + | CXCursor_InitListExpr + | CXCursor_AddrLabelExpr + | CXCursor_StmtExpr + | CXCursor_GenericSelectionExpr + | CXCursor_GNUNullExpr + | CXCursor_CXXStaticCastExpr + | CXCursor_CXXDynamicCastExpr + | CXCursor_CXXReinterpretCastExpr + | CXCursor_CXXConstCastExpr + | CXCursor_CXXFunctionalCastExpr + | CXCursor_CXXTypeidExpr + | CXCursor_CXXBoolLiteralExpr + | CXCursor_CXXNullPtrLiteralExpr + | CXCursor_CXXThisExpr + | CXCursor_CXXThrowExpr + | CXCursor_CXXNewExpr + | CXCursor_CXXDeleteExpr + | CXCursor_UnaryExpr + | CXCursor_ObjCStringLiteral + | CXCursor_ObjCEncodeExpr + | CXCursor_ObjCSelectorExpr + | CXCursor_ObjCProtocolExpr + | CXCursor_ObjCBridgedCastExpr + | CXCursor_PackExpansionExpr + | CXCursor_SizeOfPackExpr + | CXCursor_LambdaExpr + | CXCursor_ObjCBoolLiteralExpr + | CXCursor_ObjCSelfExpr + | CXCursor_OMPArraySectionExpr + | CXCursor_ObjCAvailabilityCheckExpr + | CXCursor_FixedPointLiteral + | CXCursor_OMPArrayShapingExpr + | CXCursor_OMPIteratorExpr + | CXCursor_CXXAddrspaceCastExpr + | CXCursor_LastExpr + | CXCursor_FirstStmt + | CXCursor_UnexposedStmt + | CXCursor_LabelStmt + | CXCursor_CompoundStmt + | CXCursor_CaseStmt + | CXCursor_DefaultStmt + | CXCursor_IfStmt + | CXCursor_SwitchStmt + | CXCursor_WhileStmt + | CXCursor_DoStmt + | CXCursor_ForStmt + | CXCursor_GotoStmt + | CXCursor_IndirectGotoStmt + | CXCursor_ContinueStmt + | CXCursor_BreakStmt + | CXCursor_ReturnStmt + | CXCursor_GCCAsmStmt + | CXCursor_AsmStmt + | CXCursor_ObjCAtTryStmt + | CXCursor_ObjCAtCatchStmt + | CXCursor_ObjCAtFinallyStmt + | CXCursor_ObjCAtThrowStmt + | CXCursor_ObjCAtSynchronizedStmt + | CXCursor_ObjCAutoreleasePoolStmt + | CXCursor_ObjCForCollectionStmt + | CXCursor_CXXCatchStmt + | CXCursor_CXXTryStmt + | CXCursor_CXXForRangeStmt + | CXCursor_SEHTryStmt + | CXCursor_SEHExceptStmt + | CXCursor_SEHFinallyStmt + | CXCursor_MSAsmStmt + | CXCursor_NullStmt + | CXCursor_DeclStmt + | CXCursor_OMPParallelDirective + | CXCursor_OMPSimdDirective + | CXCursor_OMPForDirective + | CXCursor_OMPSectionsDirective + | CXCursor_OMPSectionDirective + | CXCursor_OMPSingleDirective + | CXCursor_OMPParallelForDirective + | CXCursor_OMPParallelSectionsDirective + | CXCursor_OMPTaskDirective + | CXCursor_OMPMasterDirective + | CXCursor_OMPCriticalDirective + | CXCursor_OMPTaskyieldDirective + | CXCursor_OMPBarrierDirective + | CXCursor_OMPTaskwaitDirective + | CXCursor_OMPFlushDirective + | CXCursor_SEHLeaveStmt + | CXCursor_OMPOrderedDirective + | CXCursor_OMPAtomicDirective + | CXCursor_OMPForSimdDirective + | CXCursor_OMPParallelForSimdDirective + | CXCursor_OMPTargetDirective + | CXCursor_OMPTeamsDirective + | CXCursor_OMPTaskgroupDirective + | CXCursor_OMPCancellationPointDirective + | CXCursor_OMPCancelDirective + | CXCursor_OMPTargetDataDirective + | CXCursor_OMPTaskLoopDirective + | CXCursor_OMPTaskLoopSimdDirective + | CXCursor_OMPDistributeDirective + | CXCursor_OMPTargetEnterDataDirective + | CXCursor_OMPTargetExitDataDirective + | CXCursor_OMPTargetParallelDirective + | CXCursor_OMPTargetParallelForDirective + | CXCursor_OMPTargetUpdateDirective + | CXCursor_OMPDistributeParallelForDirective + | CXCursor_OMPDistributeParallelForSimdDirective + | CXCursor_OMPDistributeSimdDirective + | CXCursor_OMPTargetParallelForSimdDirective + | CXCursor_OMPTargetSimdDirective + | CXCursor_OMPTeamsDistributeDirective + | CXCursor_OMPTeamsDistributeSimdDirective + | CXCursor_OMPTeamsDistributeParallelForSimdDirective + | CXCursor_OMPTeamsDistributeParallelForDirective + | CXCursor_OMPTargetTeamsDirective + | CXCursor_OMPTargetTeamsDistributeDirective + | CXCursor_OMPTargetTeamsDistributeParallelForDirective + | CXCursor_OMPTargetTeamsDistributeParallelForSimdDirective + | CXCursor_OMPTargetTeamsDistributeSimdDirective + | CXCursor_BuiltinBitCastExpr + | CXCursor_OMPMasterTaskLoopDirective + | CXCursor_OMPParallelMasterTaskLoopDirective + | CXCursor_OMPMasterTaskLoopSimdDirective + | CXCursor_OMPParallelMasterTaskLoopSimdDirective + | CXCursor_OMPParallelMasterDirective + | CXCursor_OMPDepobjDirective + | CXCursor_OMPScanDirective + | CXCursor_OMPTileDirective + | CXCursor_OMPCanonicalLoop + | CXCursor_OMPInteropDirective + | CXCursor_OMPDispatchDirective + | CXCursor_OMPMaskedDirective + | CXCursor_OMPUnrollDirective + | CXCursor_LastStmt + | CXCursor_TranslationUnit + | CXCursor_FirstAttr + | CXCursor_UnexposedAttr + | CXCursor_IBActionAttr + | CXCursor_IBOutletAttr + | CXCursor_IBOutletCollectionAttr + | CXCursor_CXXFinalAttr + | CXCursor_CXXOverrideAttr + | CXCursor_AnnotateAttr + | CXCursor_AsmLabelAttr + | CXCursor_PackedAttr + | CXCursor_PureAttr + | CXCursor_ConstAttr + | CXCursor_NoDuplicateAttr + | CXCursor_CUDAConstantAttr + | CXCursor_CUDADeviceAttr + | CXCursor_CUDAGlobalAttr + | CXCursor_CUDAHostAttr + | CXCursor_CUDASharedAttr + | CXCursor_VisibilityAttr + | CXCursor_DLLExport + | CXCursor_DLLImport + | CXCursor_NSReturnsRetained + | CXCursor_NSReturnsNotRetained + | CXCursor_NSReturnsAutoreleased + | CXCursor_NSConsumesSelf + | CXCursor_NSConsumed + | CXCursor_ObjCException + | CXCursor_ObjCNSObject + | CXCursor_ObjCIndependentClass + | CXCursor_ObjCPreciseLifetime + | CXCursor_ObjCReturnsInnerPointer + | CXCursor_ObjCRequiresSuper + | CXCursor_ObjCRootClass + | CXCursor_ObjCSubclassingRestricted + | CXCursor_ObjCExplicitProtocolImpl + | CXCursor_ObjCDesignatedInitializer + | CXCursor_ObjCRuntimeVisible + | CXCursor_ObjCBoxable + | CXCursor_FlagEnum + | CXCursor_ConvergentAttr + | CXCursor_WarnUnusedAttr + | CXCursor_WarnUnusedResultAttr + | CXCursor_AlignedAttr + | CXCursor_LastAttr + | CXCursor_PreprocessingDirective + | CXCursor_MacroDefinition + | CXCursor_MacroExpansion + | CXCursor_MacroInstantiation + | CXCursor_InclusionDirective + | CXCursor_FirstPreprocessing + | CXCursor_LastPreprocessing + | CXCursor_ModuleImportDecl + | CXCursor_TypeAliasTemplateDecl + | CXCursor_StaticAssert + | CXCursor_FriendDecl + | CXCursor_FirstExtraDecl + | CXCursor_LastExtraDecl + | CXCursor_OverloadCandidate + +open CXCursorKind + +example (h : CXCursor_CUDAGlobalAttr = CXCursor_CUDAHostAttr) : False := by + contradiction + +#eval CXCursor_CUDAConstantAttr diff --git a/tests/lean/run/manyAritySyntax.lean b/tests/lean/run/manyAritySyntax.lean index d5aa87be43..e7897a54fb 100644 --- a/tests/lean/run/manyAritySyntax.lean +++ b/tests/lean/run/manyAritySyntax.lean @@ -1,3 +1,3 @@ -syntax "enum" ident " where " ("|" ident)* : command +syntax "enum'" ident " where " ("|" ident)* : command macro_rules - | `(enum $id where $[| $ids ]*) =>`(inductive $id where $[| $ids:ident ]*) + | `(enum' $id where $[| $ids ]*) =>`(inductive $id where $[| $ids:ident ]*)