big_eq_dec.v

Require Import Coq.NArith.NArith.
Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Require Import Coq.Logic.Eqdep_dec.

Definition decidable (P: Prop) := {P} + {~P}.
Definition eq_dec T := forall (x y:T), decidable (x=y).

Inductive spec_type: Set :=
| abruption
| additiveExpression
| argumentList
| arguments
| arrayAssignmentPattern
| arrayBindingPattern
| arrayLiteral
| assignmentElement
| assignmentElementList
| assignmentElisionElement
| assignmentExpression
| assignmentOperator
| assignmentPattern
| assignmentProperty
| assignmentPropertyList
| assignmentRestElement
| assignmentRestProperty
| bindingElement
| bindingElementList
| bindingElisionElement
| bindingIdentifier
| bindingList
| bindingPattern
| bindingProperty
| bindingPropertyList
| bindingRestElement
| bindingRestProperty
| bindingStatus
| bitwiseANDExpression
| bitwiseORExpression
| bitwiseXORExpression
| block
| blockStatement
| booleanLiteral
| breakStatement
| breakableStatement
| callExpression
| callMemberExpression
| coalesceExpression
| coalesceExpressionHead
| codeEvaluationState
| completionType
| completionValue
| computationFlow
| computedPropertyName
| conditionalExpression
| constructorKind
| continueStatement
| coverCallExpressionAndAsyncArrowHead
| coverInitializedName
| coverParenthesizedExpressionAndArrowParameterList
| declaration
| destructuringAssignmentTarget
| elementList
| elision
| equalityExpression
| exponentiationExpression
| expression
| expressionStatement
| forBinding
| forDeclaration
| formalParameter
| formalParameterList
| formalParameters
| functionBody
| functionDeclaration
| functionExpression
| functionMode
| functionRestParameter
| functionStatementList
| hoistableDeclaration
| identifier
| identifierReference
| ifStatement
| importCall
| importMeta
| initializer
| integrityLevel
| internalSlot
| intrinsicObject
| iterationStatement
| labelIdentifier
| labelledItem
| labelledStatement
| leftHandSideExpression
| letOrConst
| lexicalBinding
| lexicalDeclaration
| lexicalEnvironment
| lexical_this
| literal
| literalPropertyName
| loc_Object
| loc_scriptOrModule
| logicalANDExpression
| logicalORExpression
| maybeEmpty
| maybeNull
| maybeUndefined
| memberExpression
| metaProperty
| multiplicativeExpression
| multiplicativeOperator
| mutability
| newExpression
| newTarget
| nullLiteral
| numericLiteral
| objectAssignmentPattern
| objectBindingPattern
| objectLiteral
| optionalChain
| optionalExpression
| out
| parenthesizedExpression
| pd_Properties
| primaryExpression
| primitivePreference
| propertyDefinition
| propertyDefinitionList
| propertyName
| reference_bv
| relationalExpression
| returnStatement
| script
| scriptBody
| shiftExpression
| shortCircuitExpression
| singleNameBinding
| spreadElement
| statement
| statementList
| statementListItem
| superCall
| superProperty
| sync
| thisBindingStatus
| throwStatement
| type_DeclarativeEnvironmentRecord
| type_EnvironmentRecord
| type_exoticInternalMethod
| type_internalMethod
| type_maybeEmpty
| type_maybeNull
| type_maybeUndefined
| type_reference
| type_valref
| type_value
| unaryExpression
| uniqueFormalParameters
| updateExpression
| valref
| value
| variableDeclaration
| variableDeclarationList
| variableStatement
| voption
| withStatement.

Inductive constructor: spec_type -> Set :=
| WithSTMT : constructor withStatement
| VNone : constructor voption
| VSome : constructor voption
| VarSTMT : constructor variableStatement
| VarDeclLST : constructor variableDeclarationList
| VarDeclLST_Decl : constructor variableDeclarationList
| VarDecl_ID : constructor variableDeclaration
| VarDecl_Pattern : constructor variableDeclaration
| BigInt : constructor value
| Boolean : constructor value
| Null : constructor value
| Number : constructor value
| Obj : constructor value
| Str : constructor value
| Symbol : constructor value
| Undefined : constructor value
| Reference : constructor valref
| Value : constructor valref
| UpdE_postDec : constructor updateExpression
| UpdE_postInc : constructor updateExpression
| UpdE_preDec : constructor updateExpression
| UpdE_preInc : constructor updateExpression
| UpdExp : constructor updateExpression
| UniFormPars : constructor uniqueFormalParameters
| UnaE_await : constructor unaryExpression
| UnaE_bang : constructor unaryExpression
| UnaE_delete : constructor unaryExpression
| UnaE_minus : constructor unaryExpression
| UnaE_plus : constructor unaryExpression
| UnaE_tilde : constructor unaryExpression
| UnaE_typeof : constructor unaryExpression
| UnaE_void : constructor unaryExpression
| UnaExp : constructor unaryExpression
| T_BigInt : constructor type_value
| T_Boolean : constructor type_value
| T_Null : constructor type_value
| T_Number : constructor type_value
| T_Obj : constructor type_value
| T_Str : constructor type_value
| T_Symbol : constructor type_value
| T_Undefined : constructor type_value
| T_Reference : constructor type_valref
| T_Value : constructor type_valref
| T_R_EnvironmentRecord : constructor type_reference
| T_R_Value : constructor type_reference
| T_MU_Defined : constructor type_maybeUndefined
| T_MU_Undefined : constructor type_maybeUndefined
| T_MN_NotNull : constructor type_maybeNull
| T_MN_Null : constructor type_maybeNull
| T_Empty : constructor type_maybeEmpty
| T_NotEmpty : constructor type_maybeEmpty
| BuiltInExoticMethod : constructor type_internalMethod
| BuiltInFunctionMethod : constructor type_internalMethod
| FunctionMethod : constructor type_internalMethod
| OrdinaryMethod : constructor type_internalMethod
| ProxyObjectMethod : constructor type_internalMethod
| ArgumentsMethod : constructor type_exoticInternalMethod
| ArrayMethod : constructor type_exoticInternalMethod
| BoundFunctionMethod : constructor type_exoticInternalMethod
| ImmutablePrototypeMethod : constructor type_exoticInternalMethod
| IntegerIndexedMethod : constructor type_exoticInternalMethod
| ModuleNamespaceMethod : constructor type_exoticInternalMethod
| StrMethod : constructor type_exoticInternalMethod
| DeclarativeEnvironment : constructor type_EnvironmentRecord
| GlobalEnvironment : constructor type_EnvironmentRecord
| ObjectEnvironment : constructor type_EnvironmentRecord
| Declarative : constructor type_DeclarativeEnvironmentRecord
| Function : constructor type_DeclarativeEnvironmentRecord
| Module : constructor type_DeclarativeEnvironmentRecord
| ThrSTMT : constructor throwStatement
| TB_Initialized : constructor thisBindingStatus
| TB_Lexical : constructor thisBindingStatus
| TB_Uninitialized : constructor thisBindingStatus
| Async : constructor sync
| Sync : constructor sync
| SP_Expression : constructor superProperty
| SP_IdentifierName : constructor superProperty
| SC_Arguments : constructor superCall
| STMTListIt_Decl : constructor statementListItem
| STMTListIt_STMT : constructor statementListItem
| STMTList : constructor statementList
| STMTList_Item : constructor statementList
| BlockStatement : constructor statement
| BreakableStatement : constructor statement
| ContinueStatement : constructor statement
| DebuggerStatement : constructor statement
| EmptyStatement : constructor statement
| ExpressionStatement : constructor statement
| IfStatement : constructor statement
| LabelledStatement : constructor statement
| ReturnStatement : constructor statement
| ThrowStatement : constructor statement
| TryStatement : constructor statement
| VariableStatement : constructor statement
| WithStatement : constructor statement
| SE_AssignmentExpression : constructor spreadElement
| SNB : constructor singleNameBinding
| SCE_CoaE : constructor shortCircuitExpression
| SCE_LOE : constructor shortCircuitExpression
| ShExp_Additive : constructor shiftExpression
| ShExp_LeftShift : constructor shiftExpression
| ShExp_SignRightShift : constructor shiftExpression
| ShExp_UnsignRightShift : constructor shiftExpression
| ScriptBody : constructor scriptBody
| Script : constructor script
| RetSTMT : constructor returnStatement
| RetSTMT_ID : constructor returnStatement
| RelExp_Shift : constructor relationalExpression
| RelExp_geq : constructor relationalExpression
| RelExp_greater : constructor relationalExpression
| RelExp_in : constructor relationalExpression
| RelExp_instanceof : constructor relationalExpression
| RelExp_leq : constructor relationalExpression
| RelExp_lower : constructor relationalExpression
| R_EnvironmentRecord : constructor reference_bv
| R_Value : constructor reference_bv
| PN_ComputedPropertyName : constructor propertyName
| PN_LiteralPropertyName : constructor propertyName
| PDL_PropertyDefinition : constructor propertyDefinitionList
| PDL_PropertyDefinitionList : constructor propertyDefinitionList
| PD_AssignmentExpression : constructor propertyDefinition
| PD_CoverInitializedName : constructor propertyDefinition
| PD_IdentifierReference : constructor propertyDefinition
| PD_MethodDefinition : constructor propertyDefinition
| PD_PropertyNameAssignmentExpression : constructor propertyDefinition
| PP_Number : constructor primitivePreference
| PP_Str : constructor primitivePreference
| PE_ArrayLiteral : constructor primaryExpression
| PE_AsyncFunctionExpression : constructor primaryExpression
| PE_AsyncGeneratorExpression : constructor primaryExpression
| PE_ClassExpression : constructor primaryExpression
| PE_CoverParenthesizedExpressionAndArrowParameterList : constructor primaryExpression
| PE_FunctionExpression : constructor primaryExpression
| PE_GeneratorExpression : constructor primaryExpression
| PE_IdentifierReference : constructor primaryExpression
| PE_Literal : constructor primaryExpression
| PE_ObjectLiteral : constructor primaryExpression
| PE_RegularExpressionLiteral : constructor primaryExpression
| PE_TemplateLiteral : constructor primaryExpression
| PE_this : constructor primaryExpression
| PD_Confingurable : constructor pd_Properties
| PD_CustomProperty : constructor pd_Properties
| PD_Enumerable : constructor pd_Properties
| PD_Get : constructor pd_Properties
| PD_Set : constructor pd_Properties
| PD_Value : constructor pd_Properties
| PD_Writable : constructor pd_Properties
| PE_Expression : constructor parenthesizedExpression
| Anomaly : constructor out
| Success : constructor out
| OE_CallExpression : constructor optionalExpression
| OE_MemberExpression : constructor optionalExpression
| OE_OptionalExpression : constructor optionalExpression
| OC_Arguments : constructor optionalChain
| OC_Expression : constructor optionalChain
| OC_IdentifierName : constructor optionalChain
| OC_QArguments : constructor optionalChain
| OC_QExpression : constructor optionalChain
| OC_QIdentifierName : constructor optionalChain
| OC_QTemplateLiteral : constructor optionalChain
| OC_TemplateLiteral : constructor optionalChain
| OL_Empty : constructor objectLiteral
| OL_PropertyDefinitionList : constructor objectLiteral
| OL_PropertyDefinitionListComma : constructor objectLiteral
| OBP : constructor objectBindingPattern
| OBP_Empty : constructor objectBindingPattern
| OBP_PropList : constructor objectBindingPattern
| OBP_Rest : constructor objectBindingPattern
| OAP : constructor objectAssignmentPattern
| OAP_AssPropList : constructor objectAssignmentPattern
| OAP_AssRestProp : constructor objectAssignmentPattern
| OAP_Empty : constructor objectAssignmentPattern
| DecimalBigIntegerLiteral : constructor numericLiteral
| DecimalLiteral : constructor numericLiteral
| NonDecimalIntegerLiteral : constructor numericLiteral
| NonDecimalIntegerLiteralBigIntLiteralSuffix : constructor numericLiteral
| NullLiteral : constructor nullLiteral
| New_Target : constructor newTarget
| NE_MemberExpression : constructor newExpression
| NE_NewExpression : constructor newExpression
| Immutable : constructor mutability
| Mutable : constructor mutability
| Div : constructor multiplicativeOperator
| Mod : constructor multiplicativeOperator
| Mul : constructor multiplicativeOperator
| MulE_Exponentiation : constructor multiplicativeExpression
| MulE_Multiplicative : constructor multiplicativeExpression
| MP_ImportMeta : constructor metaProperty
| MP_NewTarget : constructor metaProperty
| ME_Expression : constructor memberExpression
| ME_IdentifierName : constructor memberExpression
| ME_MetaProperty : constructor memberExpression
| ME_NewMemberExpression : constructor memberExpression
| ME_PrimaryExpression : constructor memberExpression
| ME_SuperProperty : constructor memberExpression
| ME_TemplateLiteral : constructor memberExpression
| MU_Defined : constructor maybeUndefined
| MU_Undefined : constructor maybeUndefined
| MN_NotNull : constructor maybeNull
| MN_Null : constructor maybeNull
| Empty : constructor maybeEmpty
| NotEmpty : constructor maybeEmpty
| LOE : constructor logicalORExpression
| LOE_LAE : constructor logicalORExpression
| LAE : constructor logicalANDExpression
| LAE_BOR : constructor logicalANDExpression
| LOC_ModuleRecord : constructor loc_scriptOrModule
| LOC_ScriptRecord : constructor loc_scriptOrModule
| ObjectLocation_Intrinsic : constructor loc_Object
| ObjectLocation_Object : constructor loc_Object
| LPN_IdentifierName : constructor literalPropertyName
| LPN_NumericLiteral : constructor literalPropertyName
| LPN_StrLiteral : constructor literalPropertyName
| Lit_BooleanLiteral : constructor literal
| Lit_NullLiteral : constructor literal
| Lit_NumericLiteral : constructor literal
| Lit_StrLiteral : constructor literal
| Lexical_this : constructor lexical_this
| Non_lexical_this : constructor lexical_this
| LE_Null : constructor lexicalEnvironment
| LexicalEnvironment : constructor lexicalEnvironment
| LexDecl : constructor lexicalDeclaration
| LexBind_ID : constructor lexicalBinding
| LexBind_Pattern : constructor lexicalBinding
| Const : constructor letOrConst
| Let_0 : constructor letOrConst
| LHSE_CallExpression : constructor leftHandSideExpression
| LHSE_NewExpression : constructor leftHandSideExpression
| LHSE_OptionalExpression : constructor leftHandSideExpression
| LabelSTMT : constructor labelledStatement
| LabIt_FunDec : constructor labelledItem
| LabIt_STMT : constructor labelledItem
| LI_await : constructor labelIdentifier
| LI_identifier : constructor labelIdentifier
| LI_yield : constructor labelIdentifier
| DoWhile : constructor iterationStatement
| ForAwaitForBind : constructor iterationStatement
| ForAwaitForDecl : constructor iterationStatement
| ForAwaitLHS : constructor iterationStatement
| ForExpr : constructor iterationStatement
| ForForBindof : constructor iterationStatement
| ForForDeclin : constructor iterationStatement
| ForForDeclof : constructor iterationStatement
| ForLHSin : constructor iterationStatement
| ForLHSof : constructor iterationStatement
| ForLexDecl : constructor iterationStatement
| ForVarBindin : constructor iterationStatement
| ForVarDecl : constructor iterationStatement
| While : constructor iterationStatement
| IntrinsicArray : constructor intrinsicObject
| IntrinsicArrayBuffer : constructor intrinsicObject
| IntrinsicArrayBufferPrototype : constructor intrinsicObject
| IntrinsicArrayIteratorPrototype : constructor intrinsicObject
| IntrinsicArrayProto_entries : constructor intrinsicObject
| IntrinsicArrayProto_forEach : constructor intrinsicObject
| IntrinsicArrayProto_keys : constructor intrinsicObject
| IntrinsicArrayProto_values : constructor intrinsicObject
| IntrinsicArrayPrototype : constructor intrinsicObject
| IntrinsicAsyncFromSyncIteratorPrototype : constructor intrinsicObject
| IntrinsicAsyncFunction : constructor intrinsicObject
| IntrinsicAsyncFunctionPrototype : constructor intrinsicObject
| IntrinsicAsyncGenerator : constructor intrinsicObject
| IntrinsicAsyncGeneratorFunction : constructor intrinsicObject
| IntrinsicAsyncGeneratorPrototype : constructor intrinsicObject
| IntrinsicAsyncIteratorPrototype : constructor intrinsicObject
| IntrinsicAtomics : constructor intrinsicObject
| IntrinsicBoolean : constructor intrinsicObject
| IntrinsicBooleanPrototype : constructor intrinsicObject
| IntrinsicDataView : constructor intrinsicObject
| IntrinsicDataViewPrototype : constructor intrinsicObject
| IntrinsicDate : constructor intrinsicObject
| IntrinsicDatePrototype : constructor intrinsicObject
| IntrinsicDecodeURI : constructor intrinsicObject
| IntrinsicDecodeURIComponent : constructor intrinsicObject
| IntrinsicEncodeURI : constructor intrinsicObject
| IntrinsicEncodeURIComponent : constructor intrinsicObject
| IntrinsicError : constructor intrinsicObject
| IntrinsicErrorPrototype : constructor intrinsicObject
| IntrinsicEval : constructor intrinsicObject
| IntrinsicEvalError : constructor intrinsicObject
| IntrinsicEvalErrorPrototype : constructor intrinsicObject
| IntrinsicFloat32Array : constructor intrinsicObject
| IntrinsicFloat32ArrayPrototype : constructor intrinsicObject
| IntrinsicFloat64Array : constructor intrinsicObject
| IntrinsicFloat64ArrayPrototype : constructor intrinsicObject
| IntrinsicFunction : constructor intrinsicObject
| IntrinsicFunctionPrototype : constructor intrinsicObject
| IntrinsicGenerator : constructor intrinsicObject
| IntrinsicGeneratorFunction : constructor intrinsicObject
| IntrinsicGeneratorPrototype : constructor intrinsicObject
| IntrinsicInt16Array : constructor intrinsicObject
| IntrinsicInt16ArrayPrototype : constructor intrinsicObject
| IntrinsicInt32Array : constructor intrinsicObject
| IntrinsicInt32ArrayPrototype : constructor intrinsicObject
| IntrinsicInt8Array : constructor intrinsicObject
| IntrinsicInt8ArrayPrototype : constructor intrinsicObject
| IntrinsicIsFinite : constructor intrinsicObject
| IntrinsicIsNan : constructor intrinsicObject
| IntrinsicIteratorType : constructor intrinsicObject
| IntrinsicJSON : constructor intrinsicObject
| IntrinsicJSONParse : constructor intrinsicObject
| IntrinsicJSONStrify : constructor intrinsicObject
| IntrinsicMap : constructor intrinsicObject
| IntrinsicMapIteratorPrototype : constructor intrinsicObject
| IntrinsicMapPrototype : constructor intrinsicObject
| IntrinsicMath : constructor intrinsicObject
| IntrinsicNumber : constructor intrinsicObject
| IntrinsicNumberPrototype : constructor intrinsicObject
| IntrinsicObjProto_toStr : constructor intrinsicObject
| IntrinsicObjProto_valueOf : constructor intrinsicObject
| IntrinsicObject : constructor intrinsicObject
| IntrinsicObjectPrototype : constructor intrinsicObject
| IntrinsicParseFloat : constructor intrinsicObject
| IntrinsicParseInt : constructor intrinsicObject
| IntrinsicPromise : constructor intrinsicObject
| IntrinsicPromiseProto_then : constructor intrinsicObject
| IntrinsicPromisePrototype : constructor intrinsicObject
| IntrinsicPromise_all : constructor intrinsicObject
| IntrinsicPromise_reject : constructor intrinsicObject
| IntrinsicPromise_resolve : constructor intrinsicObject
| IntrinsicProxy : constructor intrinsicObject
| IntrinsicRangeError : constructor intrinsicObject
| IntrinsicRangeErrorPrototype : constructor intrinsicObject
| IntrinsicReferenceError : constructor intrinsicObject
| IntrinsicReferenceErrorPrototype : constructor intrinsicObject
| IntrinsicReflect : constructor intrinsicObject
| IntrinsicRegExp : constructor intrinsicObject
| IntrinsicRegExpPrototype : constructor intrinsicObject
| IntrinsicSet : constructor intrinsicObject
| IntrinsicSetIteratorPrototype : constructor intrinsicObject
| IntrinsicSetPrototype : constructor intrinsicObject
| IntrinsicSharedArrayBuffer : constructor intrinsicObject
| IntrinsicSharedArrayBufferPrototype : constructor intrinsicObject
| IntrinsicStr : constructor intrinsicObject
| IntrinsicStrIteratorPrototype : constructor intrinsicObject
| IntrinsicStrPrototype : constructor intrinsicObject
| IntrinsicSymbol : constructor intrinsicObject
| IntrinsicSymbolPrototype : constructor intrinsicObject
| IntrinsicSyntaxError : constructor intrinsicObject
| IntrinsicSyntaxErrorPrototype : constructor intrinsicObject
| IntrinsicThrowTypeError : constructor intrinsicObject
| IntrinsicTypeError : constructor intrinsicObject
| IntrinsicTypeErrorPrototype : constructor intrinsicObject
| IntrinsicTypedArray : constructor intrinsicObject
| IntrinsicTypedArrayPrototype : constructor intrinsicObject
| IntrinsicURIError : constructor intrinsicObject
| IntrinsicURIErrorPrototype : constructor intrinsicObject
| IntrinsicUint16Array : constructor intrinsicObject
| IntrinsicUint16ArrayPrototype : constructor intrinsicObject
| IntrinsicUint32Array : constructor intrinsicObject
| IntrinsicUint32ArrayPrototype : constructor intrinsicObject
| IntrinsicUint8Array : constructor intrinsicObject
| IntrinsicUint8ArrayPrototype : constructor intrinsicObject
| IntrinsicUint8ClampedArray : constructor intrinsicObject
| IntrinsicUint8ClampedArrayPrototype : constructor intrinsicObject
| IntrinsicWeakMap : constructor intrinsicObject
| IntrinsicWeakMapPrototype : constructor intrinsicObject
| IntrinsicWeakSet : constructor intrinsicObject
| IntrinsicWeakSetPrototype : constructor intrinsicObject
| ConstructorKind : constructor internalSlot
| ECMAScriptCode : constructor internalSlot
| Environment : constructor internalSlot
| Extensible : constructor internalSlot
| FormalParameters : constructor internalSlot
| HomeObject : constructor internalSlot
| IsClassConstructor : constructor internalSlot
| Prototype : constructor internalSlot
| Realm : constructor internalSlot
| ScriptOrModule : constructor internalSlot
| SourceText : constructor internalSlot
| Strict : constructor internalSlot
| ThisMode : constructor internalSlot
| Frozen : constructor integrityLevel
| Sealed : constructor integrityLevel
| Init : constructor initializer
| Import_Meta : constructor importMeta
| IC_AssignmentExpression : constructor importCall
| If : constructor ifStatement
| IfElse : constructor ifStatement
| IR_await : constructor identifierReference
| IR_identifier : constructor identifierReference
| IR_yield : constructor identifierReference
| IdentifierName : constructor identifier
| AsyncFunctionDeclaration : constructor hoistableDeclaration
| AsyncGeneratorDeclaration : constructor hoistableDeclaration
| FunctionDeclaration : constructor hoistableDeclaration
| GeneratorDeclaration : constructor hoistableDeclaration
| FuncSTMTList : constructor functionStatementList
| FunRestPar : constructor functionRestParameter
| F_Global : constructor functionMode
| F_Lexical : constructor functionMode
| F_Strict : constructor functionMode
| FuncExpr : constructor functionExpression
| FuncDecl : constructor functionDeclaration
| FuncDecl_Bound : constructor functionDeclaration
| FuncBody : constructor functionBody
| FormPars : constructor formalParameters
| FormPars_CommaList : constructor formalParameters
| FormPars_Empty : constructor formalParameters
| FormPars_List : constructor formalParameters
| FormPars_RestParam : constructor formalParameters
| FormParList : constructor formalParameterList
| FormParList_Par : constructor formalParameterList
| FormPar : constructor formalParameter
| ForDecl : constructor forDeclaration
| ForBind_Id : constructor forBinding
| ForBind_Patt : constructor forBinding
| ExprSTMT : constructor expressionStatement
| Expr_AssExpr : constructor expression
| Expression : constructor expression
| EE_Exponentiation : constructor exponentiationExpression
| EE_UnaryExpression : constructor exponentiationExpression
| EqExp_Relational : constructor equalityExpression
| EqExp_eq : constructor equalityExpression
| EqExp_neq : constructor equalityExpression
| EqExp_strictEq : constructor equalityExpression
| EqExp_strictNeq : constructor equalityExpression
| E_Comma : constructor elision
| E_Elision : constructor elision
| EL_ElementListAssignmentExpression : constructor elementList
| EL_ElementListSpreadElement : constructor elementList
| EL_ElisionAssignmentExpression : constructor elementList
| EL_ElisionSpreadElement : constructor elementList
| DAT : constructor destructuringAssignmentTarget
| ClassDeclaration : constructor declaration
| HoistableDeclaration : constructor declaration
| LexicalDeclaration : constructor declaration
| CPEAAPL_BindingIdentifier : constructor coverParenthesizedExpressionAndArrowParameterList
| CPEAAPL_Expression : constructor coverParenthesizedExpressionAndArrowParameterList
| CPEAAPL_ExpressionBindingIdentifier : constructor coverParenthesizedExpressionAndArrowParameterList
| CPEAAPL_ExpressionBindingPattern : constructor coverParenthesizedExpressionAndArrowParameterList
| CPEAAPL_ExpressionComma : constructor coverParenthesizedExpressionAndArrowParameterList
| CPEAAPL_bindingPattern : constructor coverParenthesizedExpressionAndArrowParameterList
| CPEAAPL_empty : constructor coverParenthesizedExpressionAndArrowParameterList
| CIN : constructor coverInitializedName
| CCEAAAH : constructor coverCallExpressionAndAsyncArrowHead
| ContSTMT : constructor continueStatement
| ContSTMT_ID : constructor continueStatement
| CK_Base : constructor constructorKind
| CK_Derived : constructor constructorKind
| CondE : constructor conditionalExpression
| CondE_ShortCircuit : constructor conditionalExpression
| CPN : constructor computedPropertyName
| ContinueComputation : constructor computationFlow
| ReturnAbruption : constructor computationFlow
| ReturnComputation : constructor computationFlow
| Abruption : constructor completionValue
| Ok : constructor completionValue
| Break : constructor completionType
| Continue : constructor completionType
| Normal : constructor completionType
| Return : constructor completionType
| Throw : constructor completionType
| Perform : constructor codeEvaluationState
| Resume : constructor codeEvaluationState
| Suspend : constructor codeEvaluationState
| CoaEH_BOR : constructor coalesceExpressionHead
| CoaEH_CoaE : constructor coalesceExpressionHead
| CoaE : constructor coalesceExpression
| CME : constructor callMemberExpression
| CE_Arguments : constructor callExpression
| CE_CoverCallExpressionAndAsyncArrowHead : constructor callExpression
| CE_Expression : constructor callExpression
| CE_IdentifierName : constructor callExpression
| CE_ImportCall : constructor callExpression
| CE_SuperCall : constructor callExpression
| CE_TemplateLiteral : constructor callExpression
| IterationStatement : constructor breakableStatement
| SwitchStatement : constructor breakableStatement
| BreakSTMT : constructor breakStatement
| BreakSTMT_ID : constructor breakStatement
| False : constructor booleanLiteral
| True : constructor booleanLiteral
| BlockSTMT : constructor blockStatement
| Block : constructor block
| BXE : constructor bitwiseXORExpression
| BXE_BAE : constructor bitwiseXORExpression
| BOE : constructor bitwiseORExpression
| BOE_BXE : constructor bitwiseORExpression
| BAE : constructor bitwiseANDExpression
| BAE_Equality : constructor bitwiseANDExpression
| Initialized : constructor bindingStatus
| Uninitialized : constructor bindingStatus
| BRP : constructor bindingRestProperty
| BRE_BID : constructor bindingRestElement
| BRE_Patt : constructor bindingRestElement
| BPL : constructor bindingPropertyList
| BPL_Prop : constructor bindingPropertyList
| BindP : constructor bindingProperty
| BindP_SingleName : constructor bindingProperty
| BindPatt_Arr : constructor bindingPattern
| BindPatt_Obj : constructor bindingPattern
| BindLST : constructor bindingList
| LexBind : constructor bindingList
| BI_await : constructor bindingIdentifier
| BI_identifier : constructor bindingIdentifier
| BI_yield : constructor bindingIdentifier
| BEE : constructor bindingElisionElement
| BEL : constructor bindingElementList
| BEL_ElisionElem : constructor bindingElementList
| BindE : constructor bindingElement
| BindE_SingleName : constructor bindingElement
| ARProp : constructor assignmentRestProperty
| ARE : constructor assignmentRestElement
| APL : constructor assignmentPropertyList
| APL_AssProp : constructor assignmentPropertyList
| AP_IDRef : constructor assignmentProperty
| AP_PropName : constructor assignmentProperty
| ArrAssPattern : constructor assignmentPattern
| ObjAssPattern : constructor assignmentPattern
| BANDAss : constructor assignmentOperator
| BORAss : constructor assignmentOperator
| BXORAss : constructor assignmentOperator
| DivAss : constructor assignmentOperator
| ExpAss : constructor assignmentOperator
| MinusAss : constructor assignmentOperator
| ModAss : constructor assignmentOperator
| MulAss : constructor assignmentOperator
| PlusAss : constructor assignmentOperator
| SLAss : constructor assignmentOperator
| SSRAss : constructor assignmentOperator
| USRAss : constructor assignmentOperator
| AssE_ArrowFunction : constructor assignmentExpression
| AssE_Assignment : constructor assignmentExpression
| AssE_AssignmentOp : constructor assignmentExpression
| AssE_AsyncArrowFunction : constructor assignmentExpression
| AssE_CondE : constructor assignmentExpression
| AssE_YieldExpression : constructor assignmentExpression
| AEE : constructor assignmentElisionElement
| AEL : constructor assignmentElementList
| AEL_AssEliEl : constructor assignmentElementList
| AssElem : constructor assignmentElement
| AL_ElementList : constructor arrayLiteral
| AL_ElementListElision : constructor arrayLiteral
| AL_Elision : constructor arrayLiteral
| ABP : constructor arrayBindingPattern
| ABP_ElemLST : constructor arrayBindingPattern
| ABP_Elision : constructor arrayBindingPattern
| AAP : constructor arrayAssignmentPattern
| AAP_AssElemList : constructor arrayAssignmentPattern
| AAP_Elision : constructor arrayAssignmentPattern
| Args_ArgumentList : constructor arguments
| Args_ArgumentListComma : constructor arguments
| Args_Empty : constructor arguments
| AL_AssignmentExpression : constructor argumentList
| AL_CommaAssignmentExpression : constructor argumentList
| AL_CommaDotsAssignmentExpression : constructor argumentList
| AL_DotsAssignmentExpression : constructor argumentList
| AddE_Multiplicative : constructor additiveExpression
| AddE_Sub : constructor additiveExpression
| AddE_Sum : constructor additiveExpression
| AnomalyAbruption : constructor abruption
| NotImplemented : constructor abruption
| ObjectAbruption : constructor abruption.

Ltac head x :=
  lazymatch x with
  | ?f _ => head f
  | _ => x
  end.
Ltac find_evar_tail x :=
  lazymatch x with
  | Datatypes.cons _ ?x => find_evar_tail x
  | ?ev => let __ := match goal with _ => is_evar ev end in
           ev
  end.
Ltac curry_ind_family P :=
  lazymatch eval cbv beta in P with
  | ?T -> Logic.True => T
  | forall a : ?A, @?B a
    => let a' := fresh in
       lazymatch constr:({ a' : A & ltac:(let v := curry_ind_family (B a') in exact v) }) with
       | { a : ?A & { b : @?B a & @?C a b } }
         => constr:({ ab : Specif.sigT B & C (Specif.projT1 ab) (Specif.projT2 ab) })
       | ?v => v
       end
  end.
Ltac build_all_ind_gen P :=
  let F := curry_ind_family P in
  let make := lazymatch F with
              | sigT ?P => fun h => constr:(Specif.existT P _ h)
              | _ => fun h => h
              end in
  let res := open_constr:(_ : Datatypes.list F) in
  let fill_next v :=
      let next := find_evar_tail res in
      let __ := open_constr:(eq_refl : next = v) in
      constr:(I) in
  let __ := open_constr:(
              ltac:(intros;
                    let val' := fresh "val'" in
                    lazymatch goal with
                    | [ val : _ |- _ ] => pose val as val'; destruct val
                    end;
                    let val := (eval cbv [val'] in val') in
                    let h := head val in
                    let hv := make h in
                    let __ := fill_next open_constr:(Datatypes.cons hv _) in
                    constructor)
              : P) in
  let __ := fill_next uconstr:(Datatypes.nil) in
  (eval cbv in (List.rev res)).

Ltac build_ind_to_N ty :=
  let v :=
      open_constr:(
        ltac:(
          let H := fresh in
          let rec inst_next n :=
              try (instantiate (1 := n) in (value of H);
                   let n := (eval cbv in (N.succ n)) in
                   inst_next n) in
          epose (ltac:(intros;
                       let val := lazymatch goal with val : _ |- _ => val end in
                       destruct val)
                 : ty) as H;
          inst_next N0;
          exact H)) in
  (eval cbv beta zeta in v).

Lemma eq_dec_iff {T1 T2} {f : T2 -> T1} (H : forall x y, f x = f y -> x = y)
  : eq_dec T1 -> eq_dec T2.
Proof.
  intros dec1 x y; specialize (H x y); specialize (dec1 (f x) (f y)).
  destruct dec1;
    [ left; apply H; assumption
    | right; clear H; abstract (intro; subst; tauto) ].
Defined.

(* This should really be in Coq's stdlib *)
Lemma seq_nth_error n start len
  : List.nth_error (List.seq start len) n
    = if n <? len
      then Datatypes.Some (n + start)
      else Datatypes.None.
Proof.
  revert len start; induction n as [|n IHn], len as [|len]; intro start;
    cbn [List.nth_error List.seq]; try reflexivity.
  rewrite IHn, <- plus_n_Sm, !plus_Sn_m.
  reflexivity.
Qed.

(* This should really be in Coq's stdlib *)
Lemma map_nth_error_full A B (f : A -> B) ls n
  : List.nth_error (List.map f ls) n = option_map f (List.nth_error ls n).
Proof.
  revert ls; induction n as [|n IHn], ls as [|l ls];
    cbn [List.nth_error List.map]; try reflexivity.
  rewrite IHn; reflexivity.
Qed.

(** definitions specific to [constructor] *)

Time Definition all_constructor : Datatypes.list { x : _ & constructor x }
  := ltac:(let v := build_all_ind_gen (forall x, constructor x -> Logic.True) in exact v).
(* Finished transaction in 3.515 secs (3.515u,0.s) (successful) *)

Time Definition constructor_to_N : forall {x}, constructor x -> N
  := ltac:(let v := build_ind_to_N (forall x, constructor x -> N) in exact v).
(* Finished transaction in 0.284 secs (0.284u,0.s) (successful) *)

Lemma constructor_of_to_N {x} (c : constructor x)
  : List.nth_error all_constructor (N.to_nat (constructor_to_N c))
    = Datatypes.Some (Specif.existT _ _ c).
Proof. Time destruct c; reflexivity. Qed.
(* Finished transaction in 0.308 secs (0.308u,0.s) (successful) *)

Lemma map_constructor_to_N_seq
  : List.map (fun v => constructor_to_N (projT2 v)) all_constructor
    = List.map N.of_nat (List.seq 0 (List.length all_constructor)).
Proof. vm_cast_no_check (eq_refl (List.map N.of_nat (List.seq 0 (List.length all_constructor)))). Qed.

Lemma constructor_to_of_N {n} {v}
  : List.nth_error all_constructor n = Some v
    -> constructor_to_N (projT2 v) = N.of_nat n.
Proof.
  destruct v; cbn [projT1 projT2].
  intro H; eapply map_nth_error with (f:=fun v => constructor_to_N (projT2 v)) in H.
  setoid_rewrite map_constructor_to_N_seq in H.
  rewrite map_nth_error_full, seq_nth_error, <- plus_n_O in H.
  cbv [option_map] in H.
  now edestruct Nat.ltb; inversion H.
Qed.

Lemma eq_constructor_sig_inj (x y : {v:spec_type & constructor v})
  : constructor_to_N (projT2 x) = constructor_to_N (projT2 y) -> x = y.
Proof.
  intro H.
  pose proof (constructor_of_to_N (projT2 x)) as Hx.
  pose proof (constructor_of_to_N (projT2 y)) as Hy.
  generalize dependent (constructor_to_N (projT2 y)); intro n1.
  generalize dependent (constructor_to_N (projT2 x)); intro n2.
  intros; subst n2.
  generalize dependent (List.nth_error all_constructor (N.to_nat n1)); intros ??; subst.
  destruct x as [x1 x2], y as [y1 y2]; cbn [projT1 projT2].
  intro H; inversion H; reflexivity.
Qed.

Definition constructor_eq_dec_aux: eq_dec {v:spec_type & constructor v}.
Proof.
  eapply eq_dec_iff; [ apply eq_constructor_sig_inj | exact N.eq_dec ].
Defined.

(** definitions specific to [spec_type] *)
Time Definition all_spec_type : Datatypes.list spec_type
  := ltac:(let v := build_all_ind_gen (spec_type -> Logic.True) in exact v).
(* Finished transaction in 0.256 secs (0.256u,0.s) (successful) *)

Time Definition spec_type_to_N : spec_type -> N
  := ltac:(let v := build_ind_to_N (spec_type -> N) in exact v).
(* Finished transaction in 0.031 secs (0.031u,0.s) (successful) *)

Lemma spec_type_of_to_N (c : spec_type)
  : List.nth_error all_spec_type (N.to_nat (spec_type_to_N c)) = Datatypes.Some c.
Proof. Time destruct c; reflexivity. Qed.
(* Finished transaction in 0.035 secs (0.035u,0.s) (successful) *)

Lemma map_spec_type_to_N_seq
  : List.map spec_type_to_N all_spec_type
    = List.map N.of_nat (List.seq 0 (List.length all_spec_type)).
Proof. vm_cast_no_check (eq_refl (List.map N.of_nat (List.seq 0 (List.length all_spec_type)))). Qed.

Lemma spec_type_to_of_N {n v}
  : List.nth_error all_spec_type n = Some v
    -> spec_type_to_N v = N.of_nat n.
Proof.
  intro H; eapply map_nth_error with (f:=spec_type_to_N) in H.
  setoid_rewrite map_spec_type_to_N_seq in H.
  rewrite map_nth_error_full, seq_nth_error, <- plus_n_O in H.
  cbv [option_map] in H.
  now edestruct Nat.ltb; inversion H.
Qed.

Lemma eq_spec_type_sig_inj (x y : spec_type)
  : spec_type_to_N x = spec_type_to_N y -> x = y.
Proof.
  intro H.
  pose proof (spec_type_of_to_N x) as Hx.
  pose proof (spec_type_of_to_N y) as Hy.
  generalize dependent (spec_type_to_N y); intro n1.
  generalize dependent (spec_type_to_N x); intro n2.
  intros; subst n2.
  generalize dependent (List.nth_error all_spec_type (N.to_nat n1)); intros ??; subst.
  intro H; inversion H; reflexivity.
Qed.

(** We need decidable equality on [spec_type] to be able to prove [existT constructor s x = existT constructor s y] implies [x = y] *)
Definition spec_type_eq_dec: eq_dec spec_type.
Proof.
  eapply eq_dec_iff; [ apply eq_spec_type_sig_inj | exact N.eq_dec ].
Defined.

Definition constructor_eq_dec v : eq_dec (constructor v).
Proof.
  intros x y.
  destruct (constructor_eq_dec_aux (existT _ _ x) (existT _ _ y)) as [e|ne].
  - left; inversion_sigma; subst.
    erewrite (@UIP_dec _ spec_type_eq_dec _ _ _ eq_refl).
    reflexivity.
  - right; contradict ne; subst; reflexivity.
Defined.