Merge pull request Contract-LIB#4 from Contract-LIB/mu/repairParamPar…

…sing

repair the type parameters (par X) in datatypes and abstractions.

src/main/java/org/contractlib/parser/ContractLibANTLRParser.java

@@ -63,15 +63,13 @@ public Void visitCmd_declareAbstractions(ContractLIBParser.Cmd_declareAbstractio
             arities.add(new Pair<>(name, arity));
         }
 
-        List<String> params = new ArrayList<>();
-        for (var p : ctx.sort_dec()) {
-            params.add(convertSymbol(p.symbol()));
-            //System.out.println("Found datatype declaration: " + p.getText());
-        }
-        Types<TYPE> context = factory.types(params);
-
         List<ABS> abstractions = new ArrayList<>();
         for (var d : ctx.datatype_dec()) {
+            List<String> params = new ArrayList<>();
+            for(var par : d.symbol()) {
+                params.add(convertSymbol(par));
+            }
+            Types<TYPE> context = factory.types(params);
             ABS abstr = convertAbstraction(d, params, context, arities);
             abstractions.add(abstr);
             //System.out.println("Found declaration of abstraction " + abstr);
@@ -107,19 +105,22 @@ private Pair<String, List<Pair<String, TYPE>>> convertConstructor(ContractLIBPar
         return new Pair<>(ctrName, selectors);
     }
 
-    private TYPE convertSort(ContractLIBParser.SortContext sort, Types<TYPE> params) {
+    private TYPE convertSort(ContractLIBParser.SortContext sort, Types<TYPE> types) {
         String identifier = sort.identifier().getText();
 
         // TODO: repair parametric sorts
-        /*List<TYPE> args = new ArrayList<>();
+        List<TYPE> args = new ArrayList<>();
         if (sort.sort() != null) {
             // parametric sort
             for (var arg : sort.sort()) {
-                args.add(convertSort(arg, params));
+                args.add(convertSort(arg, types));
             }
         }
-        return new TYPE.Sort(identifier, args);*/
-        return params.identifier(identifier);
+        if(args.isEmpty()) {
+            return types.identifier(identifier);
+        } else {
+            return types.sort(identifier, args);
+        }
     }
 
 
@@ -286,14 +287,13 @@ public Void visitCmd_declareDatatypes(ContractLIBParser.Cmd_declareDatatypesCont
             arities.add(new Pair<>(name, arity));
         }
 
-        List<String> params = new ArrayList<>();
-        for (var p : ctx.sort_dec()) {
-            params.add(convertSymbol(p.symbol()));
-        }
-        Types<TYPE> context = factory.types(params);
-
         List<DT> datatypes = new ArrayList<>();
         for (var d : ctx.datatype_dec()) {
+            List<String> params = new ArrayList<>();
+            for(var par : d.symbol()) {
+                params.add(convertSymbol(par));
+            }
+            Types<TYPE> context = factory.types(params);
             DT dt = convertDatatype(d, params, context, arities);
             datatypes.add(dt);
         }

src/test/java/org/contractlib/AntlrParserTests.java

@@ -18,6 +18,7 @@
 import java.io.Reader;
 import java.nio.file.Path;
 import java.nio.file.Paths;
+import java.util.List;
 
 class AntlrParserTests {
 
@@ -106,6 +107,52 @@ void regression() throws IOException {
         canParseAll(new File("src/test/contractlib/regression"));
     }
 
+    // was a bug
+    @Test
+    void testParamsDatatypes() {
+        String input = "(declare-datatypes ((List 1)) ((par (T) ((nil) (cons (car T) (cdr (List T)))))))";
+        String expected = "[DeclareDatatypes[arities=[Pair[first=List, second=1]], " +
+                "datatypes=[Datatype[params=[T], constrs=[Pair[first=nil, second=[]], " +
+                "Pair[first=cons, second=[Pair[first=car, second=[Param[name=T]]], Pair[first=cdr, second=[Sort[name=List, arguments=[Param[name=T]]]]]]]]]]]]";
+        Assertions.assertEquals(expected, parse(input).toString());
+
+        input = "(declare-datatypes ((List 0)) ( ((nil) (cons (car Int) (cdr List))))))";
+        expected = "[DeclareDatatypes[arities=[Pair[first=List, second=0]], " +
+                "datatypes=[Datatype[params=[], constrs=[Pair[first=nil, second=[]], " +
+                "Pair[first=cons, second=[Pair[first=car, second=[Sort[name=Int, arguments=[]]]], Pair[first=cdr, second=[Sort[name=List, arguments=[]]]]]]]]]]]";
+        Assertions.assertEquals(expected, parse(input).toString());
+    }
+
+    // was a bug
+    @Test
+    void testParamsAbstractions() {
+        String input = "(declare-abstractions ((List 1)) ((par (T) ((nil) (cons (car T) (cdr (List T)))))))";
+        String expected = "[DeclareAbstractions[arities=[Pair[first=List, second=1]], " +
+                "abstractions=[Abstraction[params=[T], constrs=[Pair[first=nil, second=[]], " +
+                "Pair[first=cons, second=[Pair[first=car, second=[Param[name=T]]], Pair[first=cdr, second=[Sort[name=List, arguments=[Param[name=T]]]]]]]]]]]]";
+        Assertions.assertEquals(expected, parse(input).toString());
+
+        input = "(declare-abstractions ((List 0)) ( ((nil) (cons (car Int) (cdr List))))))";
+        expected = "[DeclareAbstractions[arities=[Pair[first=List, second=0]], " +
+                "abstractions=[Abstraction[params=[], constrs=[Pair[first=nil, second=[]], " +
+                "Pair[first=cons, second=[Pair[first=car, second=[Sort[name=Int, arguments=[]]]], Pair[first=cdr, second=[Sort[name=List, arguments=[]]]]]]]]]]]";
+        Assertions.assertEquals(expected, parse(input).toString());
+    }
+
+    private List<Command> parse(String string) {
+        // ANTLR parser
+        CharStream charStream = CharStreams.fromString(string);
+        ContractLIBLexer lexer = new ContractLIBLexer(charStream);
+        CommonTokenStream tokens = new CommonTokenStream(lexer);
+        ContractLIBParser parser = new ContractLIBParser(tokens);
+
+        ContractLIBParser.ScriptContext ctx = parser.script();
+        Factory factory = new Factory();
+        ContractLibANTLRParser<Term, Type, Abstraction, Datatype, FunDecl, Command> converter = new ContractLibANTLRParser<>(factory);
+        converter.visit(ctx);
+        return converter.getCommands();
+    }
+
     void canParseAll(File path) throws IOException {
         File[] files = path.listFiles();
 
@@ -116,6 +163,7 @@ void canParseAll(File path) throws IOException {
         }
     }
 
+
     void canParse(File file) throws IOException {
         System.out.println("Parsing:  " + file.getPath());