package jolie.typeChecker;

import java.io.IOException;
import java.io.Writer;
import java.util.HashSet;

/**
 * Created by Timur on 19.07.2016.
 */
public class TypeCheckerWriter {

    private Writer writer;
    private StringBuilder sb;

    private HashSet<String> declaredConsts = new HashSet<>();

    public TypeCheckerWriter(Writer writer) throws IOException {
        this.writer = writer;
        sb = new StringBuilder();
        sb.append(
                "(declare-sort Type)\n" +
                "(declare-sort Term)\n" +
                "\n" +
                "(declare-fun hasType (Term Type) Bool)\n" +
                "(declare-fun sameType (Term Term) Bool)\n" +
                "(declare-fun typeOf (Term) Type)\n" +
                "\n"
        );

        String[] types = {"bool", "int", "long", "double", "string", "raw", "void", "undefined"};

        sb.append(";; Define types\n");
        for (int i = 0; i < types.length; i++) {
            sb.append("(declare-fun " + types[i] + " () Type)\n");
        }
        sb.append("(declare-fun any () Type)\n"); // TODO clarify equality with other types
        sb.append("\n");

        sb.append(";; Ensure non-equality of types\n");
        for (int i = 0; i < types.length; i++) {
            for (int j = i + 1; j < types.length; j++) {
                sb.append("(assert (not (= " + types[i] + " " + types[j] + ")))\n");
            }
            sb.append("\n");
        }

        sb.append(";; Describe type functions behavior\n"); // TODO maybe biconitional assertions needed?
        for (int i = 0; i < types.length; i++) {
            sb.append("(assert (forall ((t Term)) (=> (hasType t " + types[i] + ") (= (typeOf t) " + types[i] + "))))\n");
        }

        sb.append("\n");
        sb.append("(assert (forall ((t1 Term) (t2 Term)) (=> (sameType t1 t2) (= (typeOf t1) (typeOf t2)))))\n");
        sb.append("\n");

        sb.append(";; Program constraints\n");
    }

    protected void flush() throws IOException {
        writer.write(sb.toString());
        writer.write("\n(check-sat)\n");
        writer.flush();
    }

    public void write(String s) {
        sb.append(s);
    }

    public void writeLine() {
        sb.append("\n");
    }

    public void writeLine(String s) {
        sb.append(s);
        sb.append("\n");
    }

    public boolean declareTermOnce(String name) {
        if (!declaredConsts.contains(name)) {
            writeLine("(declare-const " + name + " Term)");
            declaredConsts.add(name);
            return true;
        }
        return false;
    }
}

@@ -21,16 +21,47 @@
 ecker;%0A%0A
+import jolie.lang.NativeType;%0A%0A
 import j
@@ -134,51 +134,8 @@
 t;%0A%0A
-/**%0A * Created by Timur on 19.07.2016.%0A */%0A
 publ
@@ -763,83 +763,493 @@
     
-String%5B%5D types = %7B%22bool%22, %22int%22, %22long%22, %22double%22, %22string%22, %22raw%22, %22void%22,
+NativeType%5B%5D nativeTypes = NativeType.values();%0A        int nativeTypesLength = nativeTypes.length;%0A%0A        String%5B%5D types = new String%5BnativeTypesLength%5D;%0A%0A        for (int i = 0; i %3C nativeTypesLength; i++) %7B%0A            NativeType type = nativeTypes%5Bi%5D;%0A%0A            // we don't need 'any' type here, but we do need 'undefined', so just replace it%0A            if (!type.equals(NativeType.ANY)) %7B%0A                types%5Bi%5D = type.id();%0A            %7D else %7B%0A                types%5Bi%5D =
  %22un
@@ -1260,10 +1260,33 @@
 ned%22
-%7D
 ;
+%0A            %7D%0A        %7D
 %0A%0A  
@@ -1340,40 +1340,27 @@
 or (
-int i = 0; i %3C types.length; i++
+String type : types
 ) %7B%0A
@@ -1396,30 +1396,38 @@
 re-fun %22
- + types%5Bi%5D + 
+).append(type).append(
 %22 () Typ
@@ -1772,39 +1772,63 @@
 (= %22
- + types%5Bi%5D + %22 %22 + types%5Bj%5D + 
+).append(types%5Bi%5D).append(%22 %22).append(types%5Bj%5D).append(
 %22)))
@@ -2010,40 +2010,27 @@
 or (
-int i = 0; i %3C types.length; i++
+String type : types
 ) %7B%0A
@@ -2081,17 +2081,16 @@
 erm)) (=
-%3E
  (hasTyp
@@ -2098,54 +2098,70 @@
  t %22
- + types%5Bi%5D + %22) (= (typeOf t) %22 + types%5Bi%5D + 
+).append(type).append(%22) (= (typeOf t) %22).append(type).append(
 %22)))
@@ -2262,17 +2262,16 @@
 erm)) (=
-%3E
  (sameTy

use joline naive types for checker types definition