Parsing and type-checking generics

src/main/antlr4/GoParser.g4

@@ -1,39 +1,33 @@
 /*
- [The "BSD licence"]
- Copyright (c) 2017 Sasa Coh, Michał Błotniak
- Copyright (c) 2019 Ivan Kochurkin, [email protected], Positive Technologies
- Copyright (c) 2019 Dmitry Rassadin, [email protected], Positive Technologies
- Copyright (c) 2021 Martin Mirchev, [email protected]
- All rights reserved.
-
- Redistribution and use in source and binary forms, with or without
- modification, are permitted provided that the following conditions
- are met:
- 1. Redistributions of source code must retain the above copyright
-    notice, this list of conditions and the following disclaimer.
- 2. Redistributions in binary form must reproduce the above copyright
-    notice, this list of conditions and the following disclaimer in the
-    documentation and/or other materials provided with the distribution.
- 3. The name of the author may not be used to endorse or promote products
-    derived from this software without specific prior written permission.
-
- THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
- IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
- OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
- IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
- INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
- NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
- DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
- THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
- (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
- THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-*/
+ [The "BSD licence"] Copyright (c) 2017 Sasa Coh, Michał Błotniak Copyright (c) 2019 Ivan Kochurkin,
+ [email protected], Positive Technologies Copyright (c) 2019 Dmitry Rassadin,
+ [email protected],Positive Technologies All rights reserved. Copyright (c) 2021 Martin Mirchev,
+ [email protected]
+
+ Redistribution and use in source and binary forms, with or without modification, are permitted
+ provided that the following conditions are met: 1. Redistributions of source code must retain the
+ above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in
+ binary form must reproduce the above copyright notice, this list of conditions and the following
+ disclaimer in the documentation and/or other materials provided with the distribution. 3. The name
+ of the author may not be used to endorse or promote products derived from this software without
+ specific prior written permission.
+
+ THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING,
+ BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ POSSIBILITY OF SUCH DAMAGE.
+ */
 
 /*
  * A Go grammar for ANTLR 4 derived from the Go Language Specification https://golang.org/ref/spec
  */
 
-// Imported to Gobra from https://github.com/antlr/grammars-v4/tree/fae6a8500e9c6a1ec895fca1495b0384b9144091/golang
+// Imported to Gobra from https://github.com/antlr/grammars-v4/blob/5493f3e2458d443f5a475359bf5e7cda87b25559/golang
+// Extended with Generics
 
 parser grammar GoParser;
 
@@ -68,11 +62,15 @@ expressionList: expression (COMMA expression)*;
 
 typeDecl: TYPE (typeSpec | L_PAREN (typeSpec eos)* R_PAREN);
 
-typeSpec: IDENTIFIER ASSIGN? type_;
+typeSpec: aliasDecl | typeDef;
+
+aliasDecl: IDENTIFIER ASSIGN type_;
+
+typeDef: IDENTIFIER typeParameters? type_;
 
 // Function declarations
 
-functionDecl: FUNC IDENTIFIER (signature block?);
+functionDecl: FUNC IDENTIFIER typeParameters? (signature block?);
 
 methodDecl: FUNC receiver IDENTIFIER ( signature block?);
 
@@ -207,7 +205,7 @@ rangeClause: (
 
 goStmt: GO expression;
 
-type_: typeName | typeLit | L_PAREN type_ R_PAREN;
+type_: typeName index? | typeLit | L_PAREN type_ R_PAREN;
 
 typeName: qualifiedIdent | IDENTIFIER;
 
@@ -230,7 +228,13 @@ elementType: type_;
 pointerType: STAR type_;
 
 interfaceType:
-	INTERFACE L_CURLY ((methodSpec | typeName) eos)* R_CURLY;
+	INTERFACE L_CURLY (interfaceElem eos)* R_CURLY;
+
+interfaceElem: methodSpec | typeElem;
+
+typeElem: typeTerm (OR typeTerm)*;
+
+typeTerm: type_;
 
 sliceType: L_BRACKET R_BRACKET elementType;
 
@@ -256,6 +260,14 @@ parameters:
 
 parameterDecl: identifierList? ELLIPSIS? type_;
 
+typeParameters: L_BRACKET typeParamList COMMA? R_BRACKET;
+
+typeParamList: typeParamDecl (COMMA typeParamDecl)*;
+
+typeParamDecl: identifierList typeConstraint;
+
+typeConstraint: typeElem;
+
 expression:
 	primaryExpr
 	| unary_op = (
@@ -301,7 +313,9 @@ primaryExpr:
 	);
 
 
-conversion: nonNamedType L_PAREN expression COMMA? R_PAREN;
+
+
+conversion: type_ L_PAREN expression COMMA? R_PAREN;
 
 nonNamedType: typeLit | L_PAREN nonNamedType R_PAREN;
 
@@ -335,7 +349,7 @@ literalType:
 	| L_BRACKET ELLIPSIS R_BRACKET elementType
 	| sliceType
 	| mapType
-	| typeName;
+	| typeName index?;
 
 literalValue: L_CURLY (elementList COMMA?)? R_CURLY;
 
@@ -356,11 +370,11 @@ fieldDecl: (
 
 string_: RAW_STRING_LIT | INTERPRETED_STRING_LIT;
 
-embeddedField: STAR? typeName;
+embeddedField: STAR? typeName index?;
 
 functionLit: FUNC signature block; // function
 
-index: L_BRACKET expression R_BRACKET;
+index: L_BRACKET expression (COMMA expression)* COMMA? R_BRACKET;
 
 slice_:
 	L_BRACKET (

src/main/antlr4/GobraParser.g4

@@ -226,7 +226,7 @@ new_: NEW L_PAREN type_ R_PAREN;
 
 specMember: specification (functionDecl[$specification.trusted, $specification.pure] | methodDecl[$specification.trusted, $specification.pure]);
 
-functionDecl[boolean trusted, boolean pure]:  FUNC IDENTIFIER (signature blockWithBodyParameterInfo?);
+functionDecl[boolean trusted, boolean pure]:  FUNC IDENTIFIER typeParameters? (signature blockWithBodyParameterInfo?);
 
 methodDecl[boolean trusted, boolean pure]: FUNC receiver IDENTIFIER (signature blockWithBodyParameterInfo?);
 
@@ -393,7 +393,9 @@ predConstructArgs: L_PRED expressionList? COMMA? R_PRED;
 
 // Added predicate spec and method specifications
 interfaceType:
-  INTERFACE L_CURLY ((methodSpec | typeName| predicateSpec) eos)* R_CURLY;
+  INTERFACE L_CURLY (interfaceElem eos)* R_CURLY;
+
+interfaceElem: methodSpec | typeElem | predicateSpec;
 
 predicateSpec: PRED IDENTIFIER parameters;
 
@@ -402,7 +404,7 @@ methodSpec:
   | GHOST? specification IDENTIFIER parameters;
 
 // Added ghostTypeLiterals
-type_: typeName | typeLit | ghostTypeLit | L_PAREN type_ R_PAREN;
+type_: typeName index? | typeLit | ghostTypeLit | L_PAREN type_ R_PAREN;
 
 // Added pred types
 typeLit:
@@ -428,7 +430,7 @@ literalType:
   | sliceType
   | mapType
   | ghostTypeLit
-  | typeName;
+  | typeName index?;
 
 implicitArray: L_BRACKET ELLIPSIS R_BRACKET elementType;
 

src/main/java/viper/gobra/frontend/GobraLexer.java

@@ -1,4 +1,4 @@
-// Generated from src/main/antlr4/GobraLexer.g4 by ANTLR 4.12.0
+// Generated from S:/GitHub/gobra/src/main/antlr4\GobraLexer.g4 by ANTLR 4.12.0
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.Lexer;
 import org.antlr.v4.runtime.CharStream;