package model.latex;

import model.Proof;

import java.io.IOException;
import java.nio.file.Files;
import java.nio.file.Path;
import java.util.HashMap;

public class ExportLatex {
    private static final HashMap<Character, String> unicodeToLaTeX;

    static {
        unicodeToLaTeX = new HashMap<Character, String>();
        unicodeToLaTeX.put('∧',"\\land ");
        unicodeToLaTeX.put('∨',"\\lor ");
        unicodeToLaTeX.put('¬',"\\neg ");
        unicodeToLaTeX.put('→',"\\to ");
        unicodeToLaTeX.put('∃',"\\exists ");
        unicodeToLaTeX.put('∀',"\\forall ");
        unicodeToLaTeX.put('⊥',"\\bot ");
    };
    public static void export (Proof proof, Path file) throws IOException {
        String[] lines = proof.getProofString().split("\\r?\\n");
        String output = "";
        int maxDepth = -1;
        int curDepth = 1;
        for (String line : lines) {
            System.out.println(line);
            String[] info = line.split("::");
            int depth = Integer.parseInt(info[0]);
            if (maxDepth < depth) {
                maxDepth = depth;
            }
            while (curDepth < depth) {
                output += "\\begin{subproof}\n";
                ++curDepth;
            }
            while (curDepth > depth) {
                if (output.substring(output.length()-3,output.length()-1).equals("\\\n")) {
                    output = output.substring(0, output.length()-3) + '\n';
                }
                output += "\\end{subproof}\n";
                --curDepth;
            }
            output += replaceAllUnicode(info[1]);
            output += "&";
            output += replaceAllUnicode(info[2]);
            output += "\\\\\n";

        }
        while (curDepth > 1) {
            output += "\\end{subproof}\n";
            --curDepth;
        }
        output = "\\begin{logicproof}{" +maxDepth + "}\n" + output + "\\end{logicproof}";
        Files.write(file, output.getBytes());
    }

    private static String replaceAllUnicode(String s) {
        String ret = "";
        for (int i = 0; i < s.length(); i++) {
            String next = unicodeToLaTeX.getOrDefault(s.charAt(i), null);
            if (next == null)
                ret += s.charAt(i);
            else
                ret += next;
        }
        return ret;
    }
}

@@ -345,16 +345,17 @@
 put('%E2%88%A7',
+ 
 %22%5C%5Cland 
@@ -389,16 +389,17 @@
 put('%E2%88%A8',
+ 
 %22%5C%5Clor %22
@@ -432,16 +432,17 @@
 put('%C2%AC',
+ 
 %22%5C%5Cneg %22
@@ -475,16 +475,17 @@
 put('%E2%86%92',
+ 
 %22%5C%5Cto %22)
@@ -517,16 +517,17 @@
 put('%E2%88%83',
+ 
 %22%5C%5Cexist
@@ -563,16 +563,17 @@
 put('%E2%88%80',
+ 
 %22%5C%5Cforal
@@ -609,16 +609,17 @@
 put('%E2%8A%A5',
+ 
 %22%5C%5Cbot %22
@@ -626,17 +626,17 @@
 );%0A    %7D
-;
+%0A
 %0A    pub
@@ -657,17 +657,16 @@
 d export
- 
 (Proof p
@@ -1330,11 +1330,14 @@
 th()
--
+ - 
 3,
+ 
 outp
@@ -1347,18 +1347,16 @@
 length()
--1
 ).equals
@@ -1360,16 +1360,18 @@
 als(%22%5C%5C%5C
+%5C%5C
 n%22)) %7B%0A 
@@ -1433,17 +1433,19 @@
 length()
--
+ - 
 3) + '%5Cn
@@ -1873,16 +1873,17 @@
 oof%7D%7B%22 +
+ 
 maxDepth
@@ -2292,32 +2292,32 @@
 next;%0A        %7D%0A
-
         return r
@@ -2325,11 +2325,211 @@
 t;%0A    %7D
+%0A%0A    private static String trimEnd(String s) %7B%0A        if (s.substring(s.length() - 3, s.length()).equals(%22%5C%5C%5C%5C%5Cn%22))%0A            return s.substring(0, s.length() - 3) + '%5Cn';%0A        return s;%0A%0A    %7D
 %0A%7D%0A

Trim backslashes if ending environment