Leonardo de Moura
parent
e4410cfbf8
commit
6f075e6ece
5 changed files with 328 additions and 3 deletions
|
|
@ -19,3 +19,4 @@ import Init.NotationExtra
|
|||
import Init.SimpLemmas
|
||||
import Init.Hints
|
||||
import Init.Conv
|
||||
import Init.Enum
|
||||
|
|
|
|||
35
src/Init/Enum.lean
Normal file
35
src/Init/Enum.lean
Normal file
|
|
@ -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)
|
||||
|
|
@ -102,7 +102,7 @@ inductive SymbolKind where
|
|||
| property
|
||||
| field
|
||||
| constructor
|
||||
| enum
|
||||
| «enum»
|
||||
| interface
|
||||
| function
|
||||
| «variable»
|
||||
|
|
|
|||
289
tests/lean/run/654.lean
Normal file
289
tests/lean/run/654.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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 ]*)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue