Fixes.

semantics/c/language/common/conversion.k

@@ -358,8 +358,6 @@ module C-CONVERSION
                     | implPointerToInt()
      rule lintCastingAwayQuals() => .K
           requires notBool hasLint
-     rule implPointerToInt() => .K
-          requires notBool hasLint
 
      syntax UType ::= castTypes(UType, UType) [function]
      rule castTypes(ut(_, T'::SimpleUType), ut(Mods::Set, _)) => ut(Mods, T')

semantics/c/language/translation/typing/expr.k

@@ -42,8 +42,6 @@ module C-TYPING-EXPR
      context typeof((HOLE:KItem => typeof(HOLE)) % _) [result(Type)]
      context typeof((HOLE:KItem => typeof(HOLE)) + _) [result(Type)]
      context typeof((HOLE:KItem => typeof(HOLE)) - _) [result(Type)]
-     context typeof((HOLE:KItem => typeof(HOLE)) == _) [result(Type)]
-     context typeof((HOLE:KItem => typeof(HOLE)) != _) [result(Type)]
      context typeof((HOLE:KItem => typeof(HOLE)) & _) [result(Type)]
      context typeof((HOLE:KItem => typeof(HOLE)) ^ _) [result(Type)]
      context typeof((HOLE:KItem => typeof(HOLE)) | _) [result(Type)]
@@ -70,13 +68,9 @@ module C-TYPING-EXPR
      context typeof(_ % (HOLE:KItem => typeof(HOLE))) [result(Type)]
      context typeof(_ + (HOLE:KItem => typeof(HOLE))) [result(Type)]
      context typeof(_ - (HOLE:KItem => typeof(HOLE))) [result(Type)]
-     context typeof(_ == (HOLE:KItem => typeof(HOLE))) [result(Type)]
-     context typeof(_ != (HOLE:KItem => typeof(HOLE))) [result(Type)]
      context typeof(_ & (HOLE:KItem => typeof(HOLE))) [result(Type)]
      context typeof(_ ^ (HOLE:KItem => typeof(HOLE))) [result(Type)]
      context typeof(_ | (HOLE:KItem => typeof(HOLE))) [result(Type)]
-     context typeof(_ && (HOLE:KItem => typeof(HOLE))) [result(Type)]
-     context typeof(_ || (HOLE:KItem => typeof(HOLE))) [result(Type)]
 
      // primary expressions
      rule <k> typeof(X:CId => T:Type) ...</k>

semantics/c/library/stdio.k

@@ -1659,7 +1659,7 @@ module LIBC-STDIO
 
      syntax List ::= tail(List) [function]
      rule tail(ListItem(_) L::List) => L
-     rule tail(_) => .List [owise]
+     rule tail(.List) => .List
 
      syntax String ::= fst(ParseStrResult) [function, klabel(fstParseStr)]
      rule fst(parseStrResult(S::String, _)) => S

semantics/cpp/language/common/class.k

@@ -10,10 +10,6 @@ module CPP-CLASS-BASIC-SORTS
 
      syntax LocalQualifier
 
-     syntax LocalClass
-
-     syntax InnerClass
-
      syntax ClassSpecifier
 
 endmodule // CPP-CLASS-BASIC-SORTS
@@ -39,15 +35,20 @@ module CPP-CLASS-BASIC-SYNTAX
 
      syntax Class ::= ClassQualifier "::" ClassSpecifier [klabel(classId)]
 
-     syntax LocalClass ::= LocalQualifier "::" ClassSpecifier [klabel(classId)]
+     // TODO(chathhorn): the stuff below causes parsing ambiguities with the Class production above. Need to resolve in
+     // a better way.
+     syntax InnerClass ::= Class // TODO(chathhorn): added as an interim fix.
+     syntax LocalInnerClass ::= Class // TODO(chathhorn): added as an interim fix.
+
+     // syntax LocalClass ::= LocalQualifier "::" ClassSpecifier [klabel(classId)]
 
-     syntax Class ::= LocalClass
-     syntax Class ::= InnerClass
+     // syntax Class ::= LocalClass
+     // syntax Class ::= InnerClass
 
-     syntax InnerClass ::= Class "::" ClassSpecifier [klabel(classId)]
+     // syntax InnerClass ::= Class "::" ClassSpecifier [klabel(classId)]
 
-     syntax LocalInnerClass ::= LocalClass
-                             | LocalInnerClass "::" ClassSpecifier [klabel(classId)]
+     // syntax LocalInnerClass ::= LocalClass
+     //                         | LocalInnerClass "::" ClassSpecifier [klabel(classId)]
 
      syntax ClassSpecifier ::= Class(Tag, CId, TemplateArgs) [klabel(classSpecifier)]
 

semantics/cpp/language/common/dynamic.k

@@ -8,8 +8,6 @@ module CPP-NAMESPACE-SORTS
 
      syntax NamespaceSpecifier
 
-     syntax UnnamedNamespace
-
 endmodule // CPP-NAMESPACE-SORTS
 
 module CPP-NAMESPACE-SYNTAX
@@ -20,7 +18,6 @@ module CPP-NAMESPACE-SYNTAX
 
      syntax Namespace ::= Namespace "::" NamespaceSpecifier
                         | NoNamespace() // signifies a declaration at block scope
-                        | UnnamedNamespace
 
      syntax NamespaceSpecifier ::= Namespace(CId)
 
@@ -586,7 +583,7 @@ module CPP-DYNAMIC-OTHER-SYNTAX
 
      syntax DefaultArguments ::= DefaultArgumentsResult
 
-     syntax DefaultArgumentsResult ::= defArgs(vals: StrictListResult, types: StrictListResult, cats: StrictListResult)
+     syntax DefaultArgumentsResult ::= defArgsResult(vals: StrictListResult, types: StrictListResult, cats: StrictListResult)
 
 endmodule // CPP-DYNAMIC-OTHER-SYNTAX
 

semantics/cpp/language/common/syntax.k

@@ -193,19 +193,19 @@ module CPP-SYNTAX
      syntax Expr ::= ConvertType(CPPType, Expr)
                    | ExprLoc
 
-     syntax ExprLoc ::= ExprLoc(CabsLoc, Expr)
+     syntax ExprLoc ::= ExprLoc(CabsLoc, Expr) [symbol]
 
-     syntax Init ::= ExprLoc(CabsLoc, Init)
+     syntax Init ::= InitLoc(CabsLoc, Init)
 
-     syntax BraceInit ::= ExprLoc(CabsLoc, BraceInit)
+     syntax BraceInit ::= BraceInitLoc(CabsLoc, BraceInit)
 
      syntax Block ::= BlockStmt(List)
                     | BlockStmt(Int, List)
 
      syntax Decl
 
-     syntax Stmt ::= LabelStmt(CId, List)
-                   | GotoStmt(CId)
+     syntax Stmt ::= LabelStmt(CId, List) [symbol]
+                   | GotoStmt(CId) [symbol]
                    | ExpressionStmt(Expr) [strict(c)]
                    | PRValExpressionStmt(Expr) [strict(c)]
                    | BreakStmt()

semantics/cpp/language/common/typing.k

@@ -78,35 +78,35 @@ module CPP-TYPING-SYNTAX
                             | CPPSimpleDependentType
                             | CPPSimpleAutoType
 
-     syntax CPPSimpleSignedType ::= bitfieldType(CPPSimpleSignedType, Int) [klabel(bitfieldTypeCpp)]
+     // syntax CPPSimpleSignedType ::= bitfieldType(CPPSimpleSignedType, Int) [klabel(bitfieldTypeCpp)]
 
-     syntax CPPSimpleUnsignedType ::= bitfieldType(CPPSimpleUnsignedType, Int) [klabel(bitfieldTypeCpp)]
+     // syntax CPPSimpleUnsignedType ::= bitfieldType(CPPSimpleUnsignedType, Int) [klabel(bitfieldTypeCpp)]
 
-     syntax CPPSimpleSignedCharType ::= bitfieldType(CPPSimpleSignedCharType, Int) [klabel(bitfieldTypeCpp)]
+     // syntax CPPSimpleSignedCharType ::= bitfieldType(CPPSimpleSignedCharType, Int) [klabel(bitfieldTypeCpp)]
 
-     syntax CPPSimpleUnsignedCharType ::= bitfieldType(CPPSimpleUnsignedCharType, Int) [klabel(bitfieldTypeCpp)]
+     // syntax CPPSimpleUnsignedCharType ::= bitfieldType(CPPSimpleUnsignedCharType, Int) [klabel(bitfieldTypeCpp)]
 
-     syntax CPPSimpleBoolType ::= bitfieldType(CPPSimpleBoolType, Int) [klabel(bitfieldTypeCpp)]
+     // syntax CPPSimpleBoolType ::= bitfieldType(CPPSimpleBoolType, Int) [klabel(bitfieldTypeCpp)]
 
-     syntax CPPSimpleWideCharType ::= bitfieldType(CPPSimpleWideCharType, Int) [klabel(bitfieldTypeCpp)]
+     // syntax CPPSimpleWideCharType ::= bitfieldType(CPPSimpleWideCharType, Int) [klabel(bitfieldTypeCpp)]
 
-     syntax CPPSimpleScopedEnumType ::= bitfieldType(CPPSimpleScopedEnumType, Int) [klabel(bitfieldTypeCpp)]
+     // syntax CPPSimpleScopedEnumType ::= bitfieldType(CPPSimpleScopedEnumType, Int) [klabel(bitfieldTypeCpp)]
 
-     syntax CPPSimpleUnscopedEnumType ::= bitfieldType(CPPSimpleUnscopedEnumType, Int) [klabel(bitfieldTypeCpp)]
+     // syntax CPPSimpleUnscopedEnumType ::= bitfieldType(CPPSimpleUnscopedEnumType, Int) [klabel(bitfieldTypeCpp)]
 
      syntax CPPSimpleBitfieldType ::= bitfieldType(CPPSimpleType, Int) [klabel(bitfieldTypeCpp)]
 
-     syntax CPPSimpleSignedType ::= CPPSimpleBottomType
-     syntax CPPSimpleUnsignedType ::= CPPSimpleBottomType
-     syntax CPPSimpleSignedCharType ::= CPPSimpleBottomType
-     syntax CPPSimpleUnsignedCharType ::= CPPSimpleBottomType
-     syntax CPPSimpleBoolType ::= CPPSimpleBottomType
-     syntax CPPSimpleWideCharType ::= CPPSimpleBottomType
-     syntax CPPSimpleScopedEnumType ::= CPPSimpleBottomType
-     syntax CPPSimpleUnscopedEnumType ::= CPPSimpleBottomType
-     syntax CPPSimpleBitfieldType ::= CPPSimpleBottomType
-
-     syntax CPPSimpleBottomType ::= bitfieldType(CPPSimpleBottomType, Int) [klabel(bitfieldTypeCpp)]
+     // syntax CPPSimpleSignedType ::= CPPSimpleBottomType
+     // syntax CPPSimpleUnsignedType ::= CPPSimpleBottomType
+     // syntax CPPSimpleSignedCharType ::= CPPSimpleBottomType
+     // syntax CPPSimpleUnsignedCharType ::= CPPSimpleBottomType
+     // syntax CPPSimpleBoolType ::= CPPSimpleBottomType
+     // syntax CPPSimpleWideCharType ::= CPPSimpleBottomType
+     // syntax CPPSimpleScopedEnumType ::= CPPSimpleBottomType
+     // syntax CPPSimpleUnscopedEnumType ::= CPPSimpleBottomType
+     // syntax CPPSimpleBitfieldType ::= CPPSimpleBottomType
+
+     // syntax CPPSimpleBottomType ::= bitfieldType(CPPSimpleBottomType, Int) [klabel(bitfieldTypeCpp)]
 
      syntax CPPSimpleSignedType ::= CPPSimpleSignedCharType | "short" | "int" | "long" | "long-long" | "oversized"
 

semantics/cpp/language/translation/decl/declarator.k

@@ -8,7 +8,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR-SYNTAX
      imports CPP-SORTS
      imports CPP-TYPING-SORTS
 
-     syntax Decl ::= DeclaratorAndSpecifiers(Declarator, Set)
+     syntax Decl ::= DeclaratorAndSpecifiers(Decl, Set)
                     | declareObject(NNSVal, NNSVal, CId, CId, CPPType, Init, DeclarationType, Linkage, Duration, Set)
                     | defineObject(NNSVal, CId, CId, CPPType, Init, DeclarationType, Set)
                     | initializeObject(NNSVal, CId, CPPType, init: KItem, DeclarationType) [strict(c; 4)]
@@ -53,18 +53,18 @@ module CPP-TRANSLATION-DECL-DECLARATOR
      imports CPP-TRANSLATION-CONSTANT-SYNTAX
      imports CPP-TRANSLATION-DECL-CLASS-DESTRUCTOR
 
-     rule FunctionDecl(N::NNSVal, X::CId, Mangled::CId, T::CPPType, Params::List)
+     rule FunctionDecl(N::NNS, X::CId, Mangled::CId, T::AType, Params::List)
           => NormalizedDecl(N, X, Mangled, T, NoInit(), Function(Params)) [anywhere]
 
-     rule VarDecl(N::NNSVal, X::CId, Mangled::CId, T::CPPType, Init::Init, IsDirect:Bool)
+     rule VarDecl(N::NNS, X::CId, Mangled::CId, T::AType, Init::Init, IsDirect:Bool)
           => NormalizedDecl(N, X, Mangled, T, Init, Var(#if IsDirect #then DirectInit() #else CopyInit() #fi)) [anywhere]
 
-     rule FunctionDefinition(N::NNSVal, X::CId, Mangled::CId, T::CPPType, Params::List, Body::Stmt)
+     rule FunctionDefinition(N::NNS, X::CId, Mangled::CId, T::AType, Params::List, Body::Stmt)
           => NormalizedDecl(N, X, Mangled, T, Body, Function(Params)) [anywhere]
 
      rule DeclStmt(L::List) => listToK(L)
 
-     rule Specifier(S::Specifier, D:Declarator) => DeclaratorAndSpecifiers(D, SetItem(S))
+     rule Specifier(S::Specifier, D::Decl) => DeclaratorAndSpecifiers(D, SetItem(S))
           requires S =/=K Auto() [anywhere]
 
      // Auto is a type specifier in C++ so it is handled elsewhere by AutoType
@@ -151,8 +151,6 @@ module CPP-TRANSLATION-DECL-DECLARATOR
      rule getClassLinkage(_:LocalQualifier :: _) => NoLinkage
 
      // @ref n4296 3.5:4
-     rule getNamespaceLinkage(N:UnnamedNamespace) => InternalLinkage
-
      rule getNamespaceLinkage(GlobalNamespace()) => ExternalLinkage
 
      rule getNamespaceLinkage(Parent::Namespace :: _) => getNamespaceLinkage(Parent) [owise]
@@ -418,7 +416,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
 
      syntax CPPType ::= completeDeclaration(CPPType, Init) [function]
 
-     rule completeDeclaration(T::CPPType, (ExprLoc(_, I::Init) => I))
+     rule completeDeclaration(T::CPPType, (InitLoc(_, I::Init) => I))
 
      // @ref n4296 8.5.4:3.2 (char x[] = {"foo"})
      rule completeDeclaration(t(Q::Quals, Mods::Set, incompleteArrayType(t(Q'::Quals, Mods'::Set, T:CPPSimpleCharType))), BraceInit(ListItem(StringLiteral(Narrow::CharKind, S::String)))) => t(Q, Mods, arrayType(t(Q', Mods', T), lengthString(S) +Int 1))
@@ -790,9 +788,12 @@ module CPP-TRANSLATION-DECL-DECLARATOR
      rule stripInitHolds(V::Val) => V
           requires isEvalVal(V)
 
-     context defArgs(_, (HOLE:StrictList => types(HOLE)), _)
+     context defArgs(_, (HOLE::StrictList => types(HOLE)), _)
+
+     context defArgs(_, _, (HOLE::StrictList => cats(HOLE)))
 
-     context defArgs(_, _, (HOLE:StrictList => cats(HOLE)))
+     rule defArgs(A:StrictListResult, B:StrictListResult, C:StrictListResult)
+          => defArgsResult(A, B, C)
 
      syntax DefaultArguments ::= computeDefaultArgs(CPPType, DeclarationType)
 
@@ -841,7 +842,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
      rule #makeFunctionDeclarationType(_, .List) => .List
 
      rule emptyDefaultArguments(t(... st: functionType(...)) #as T::CPPType)
-       => #emptyDefaultArguments(#if hasImplicitParameter(T) #then size(getRealParams(T)) -Int 1 #else size(getRealParams(T)) #fi, defArgs(krlist(.List), krlist(.List), krlist(.List)))
+       => #emptyDefaultArguments(#if hasImplicitParameter(T) #then size(getRealParams(T)) -Int 1 #else size(getRealParams(T)) #fi, defArgsResult(krlist(.List), krlist(.List), krlist(.List)))
 
      rule emptyDefaultArguments(_) => NoDefArgs() [owise]
 
@@ -850,7 +851,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
      rule #emptyDefaultArguments(0, DA::DefaultArgumentsResult) => DA
 
      rule #emptyDefaultArguments(N::Int => N -Int 1,
-            defArgs(krlist(_::List (.List => ListItem(NoArg()))),
+            defArgsResult(krlist(_::List (.List => ListItem(NoArg()))),
                     krlist(_::List (.List => ListItem(NoInitType()))),
                     krlist(_::List (.List => ListItem(NoInitCat()))))) [owise]
 endmodule

semantics/cpp/language/translation/decl/initializer.k

@@ -102,7 +102,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER
 
      syntax KItem ::= #figureInitHeatBase(destT: CPPType, type: InitType, init: Init, srcT: K, srcCat: K, ConstructorType, Duration)
 
-     rule <k> #figureInit(... init: ExprLoc(L::CabsLoc, I::Init) => I) ...</k>
+     rule <k> #figureInit(... init: InitLoc(L::CabsLoc, I::Init) => I) ...</k>
           <curr-tr-program-loc> _ => L </curr-tr-program-loc>
 
      // @ref n4296 8.5:6.1
@@ -416,7 +416,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER
 
      rule #evalBraceOrEqualInitializer(_, _, NoInit()) => BraceInit(.List)
 
-     rule #evalBraceOrEqualInitializer(_, _, ExprLoc(L::CabsLoc, I::Init) => I)
+     rule #evalBraceOrEqualInitializer(_, _, InitLoc(L::CabsLoc, I::Init) => I)
 
      rule #evalBraceOrEqualInitializer(C::Class, Base::Expr, BraceInit(L::List))
        => BraceInit(#evalBraceOrEqualInitializers(C, Base, L))

semantics/cpp/language/translation/env.k

@@ -99,11 +99,11 @@ module CPP-TRANSLATION-ENV
          <cenv> CE::Map => CE[X <- stripType(T) |-> (T, envEntry(Base, IsUsing, NoDefArgs()))] </cenv>
          requires notBool isCPPFunctionType(T)
 
-     rule getDefaultArgsVals(defArgs(... vals: krlist(Args::List))) => Args
+     rule getDefaultArgsVals(defArgsResult(... vals: krlist(Args::List))) => Args
 
-     rule getDefaultArgsTypes(defArgs(... types: krlist(Types::List))) => Types
+     rule getDefaultArgsTypes(defArgsResult(... types: krlist(Types::List))) => Types
 
-     rule getDefaultArgsCats(defArgs(... cats: krlist(Cats::List))) => Cats
+     rule getDefaultArgsCats(defArgsResult(... cats: krlist(Cats::List))) => Cats
 
      syntax Map ::= updateFnEnv(Map, CId, CPPType, SymBase, Bool) [function]
 
@@ -123,38 +123,38 @@ module CPP-TRANSLATION-ENV
      syntax DefaultArgumentsResult ::= #updateDefaultArgs(newArgs: DefaultArgumentsResult, oldArgs: DefaultArgumentsResult) [function]
 
      rule #updateDefaultArgs(NewArgs::DefaultArgumentsResult, OldArgs::DefaultArgumentsResult)
-          => #updateDefaultArgs(NewArgs, OldArgs, defArgs(krlist(.List), krlist(.List), krlist(.List)))
+          => #updateDefaultArgs(NewArgs, OldArgs, defArgsResult(krlist(.List), krlist(.List), krlist(.List)))
 
      syntax DefaultArgumentsResult ::= #updateDefaultArgs(newArgs: DefaultArgumentsResult, oldArgs: DefaultArgumentsResult, resultArgs: DefaultArgumentsResult) [function, klabel(updateDefaultArgsHelper)]
 
     // The next rule compensates for the clang policy to aggregate existing default args from previous declarations
     // Hence, we'll trust clang to check that the user does not redefine an old def. arg.
      rule #updateDefaultArgs(
-            defArgs(krlist((ListItem(_) => .List) _),
+            defArgsResult(krlist((ListItem(_) => .List) _),
                     krlist((ListItem(_) => .List) _),
                     krlist((ListItem(_) => .List) _)),
-            defArgs(krlist((ListItem(I:KItem) => .List) _),
+            defArgsResult(krlist((ListItem(I:KItem) => .List) _),
                     krlist((ListItem(T::CPPDType) => .List) _),
                     krlist((ListItem(C::ValueCategory) => .List) _)),
-            defArgs(krlist(_::List (.List => ListItem(I:KItem))),
+            defArgsResult(krlist(_::List (.List => ListItem(I:KItem))),
                     krlist(_::List (.List => ListItem(T::CPPDType))),
                     krlist(_::List (.List => ListItem(C::ValueCategory)))))
           requires I =/=K NoArg()
 
      rule #updateDefaultArgs(
-            defArgs(krlist((ListItem(I:KItem) => .List) _),
+            defArgsResult(krlist((ListItem(I:KItem) => .List) _),
                     krlist((ListItem(T::CPPDType) => .List) _),
                     krlist((ListItem(C::ValueCategory) => .List) _)),
-            defArgs(krlist((ListItem(NoArg()) => .List) _),
+            defArgsResult(krlist((ListItem(NoArg()) => .List) _),
                     krlist((ListItem(_) => .List) _),
                     krlist((ListItem(_) => .List) _)),
-            defArgs(krlist(_::List (.List => ListItem(I:KItem))),
+            defArgsResult(krlist(_::List (.List => ListItem(I:KItem))),
                     krlist(_::List (.List => ListItem(T::CPPDType))),
                     krlist(_::List (.List => ListItem(C::ValueCategory)))))
 
      rule #updateDefaultArgs(
-            defArgs(krlist(.List), krlist(.List), krlist(.List)),
-            defArgs(krlist(.List), krlist(.List), krlist(.List)),
+            defArgsResult(krlist(.List), krlist(.List), krlist(.List)),
+            defArgsResult(krlist(.List), krlist(.List), krlist(.List)),
             DA::DefaultArgumentsResult) => DA
 
      rule <k> clearScope() => .K ...</k>

semantics/cpp/language/translation/overloading.k

@@ -606,7 +606,7 @@ module CPP-TRANSLATION-OVERLOADING
           requires isCPPPointerType(T) andBool isCPPFunctionType(innerType(T))
 
      // only one viable candidate
-     rule bestViable(T::CPPType, envEntry(... base: Base::SymBase, defaultArgs: defArgs(... vals: DArgs::StrictListResult)))
+     rule bestViable(T::CPPType, envEntry(... base: Base::SymBase, defaultArgs: defArgsResult(... vals: DArgs::StrictListResult)))
           ~> #resolveOverload2(cSet(... id: X::QualId), list(Args::List), _, _, E::Expr, _)
           => #if isMethodPure(T) andBool isVirtualCall(hasTrace(E), T) #then .K #else Odr.newUse(Base) #fi
           ~> updateExternalUses(Base)

semantics/cpp/language/translation/syntax.k

@@ -50,9 +50,9 @@ module CPP-ABSTRACT-SYNTAX
                       | ConstructorMember(CId, Init) [symbol]
                       | ConstructorDelegating(Init) [symbol]
 
-     syntax Declarator ::= FunctionDefinition(NNS, CId, CId, AType, List, AStmt) [strict(4), symbol]
-                         | FunctionDecl(NNS, CId, CId, AType, List) [strict(4), symbol]
-                         | VarDecl(NNS, CId, CId, AType, Init, isDirect: Bool) [strict(4), symbol]
+     syntax Declarator ::= FunctionDefinition(NNS, CId, CId, AType, List, Stmt) [symbol]
+                         | FunctionDecl(NNS, CId, CId, AType, List) [symbol]
+                         | VarDecl(NNS, CId, CId, AType, Init, isDirect: Bool) [symbol]
                          | FieldDecl(NNS, CId, AType, Init) [strict(3), symbol]
                          | BitFieldDecl(NNS, CId, AType, Expr) [strict(3), symbol]
 
@@ -93,8 +93,7 @@ module CPP-ABSTRACT-SYNTAX
                    | UsingDecl(Bool, NNS, CId) [symbol]
                    | UsingDirective(CId, NNS) [symbol]
 
-     syntax Decl ::= DeclLoc(CabsLoc, Decl) [symbol]
-                   | NoDecl() [symbol]
+     syntax Decl ::= NoDecl() [symbol]
 
      syntax BaseSpecifier ::= BaseClass(Bool, Bool, AccessSpecifier, AType) [symbol]
 

semantics/cpp/language/translation/typing/expr.k

@@ -61,7 +61,7 @@ module CPP-TRANSLATION-TYPING-EXPR
 
      rule ofSTypeList(K:KItem types:: L::STypeList) => ListItem(K) ofSTypeList(L) [owise]
 
-     rule (ExprLoc(_, BraceInit(L::List)) => BraceInit(L)) types:: _
+     rule (BraceInitLoc(_, BraceInit(L::List)) => BraceInit(L)) types:: _
 
      rule (.K => types(list(L))) ~> BraceInit(L::List) types:: _