source: experiments/frams/logic/data/scripts/data_conversion.inc @ 480

//This file contains data conversion functions such as index-encoding-to-human-readible-format function, prefix-to-infix-format conversion function,
//formula-to-latex converters, etc...  


function binaryToIndex(binaryCombination, baseHypothesesIndexed)
{
        
        if(binaryCombination.find(1) == -1)
                return null;
        
        var hypothesis = Vector.new();
        var first = binaryCombination.find(1);
        hypothesis = getIndexedConjunctionFromLiterals(baseHypothesesIndexed[first]);
        var i;
        
        for(i = first + 1; i < binaryCombination.size; i++)
        {
                if(binaryCombination[i] == 1)
                {
                        hypothesis = (plainListCopyInsert(mergePlainLists(hypothesis, getIndexedConjunctionFromLiterals(baseHypothesesIndexed[i])), 0, [2]));
                }
        }
        
        return hypothesis;
}


function binaryToForm(binaryCombinations, baseHypotheses)
{
        
        if(binaryCombinations.find(1) == -1)
                return null;
        
        var hypothesis = "";
        
        var first = binaryCombinations.find(1);
        hypothesis = baseHypotheses[first];
        var i;
        
        for(i = first + 1; i < binaryCombinations.size; i++)
        {
                if(binaryCombinations[i] == 1)
                {
                        hypothesis = "A" + hypothesis + baseHypotheses[i];
                }
        }
        
        return hypothesis;
}

function convertIndexedSetToLatex(listOfIndexedForms)
{
        
        var i;
        var setLatex = "\\{";
        var litLatex = "";
        var allLatex = "";
        for(i = 0; i < listOfIndexedForms.size; i++)
        {               
                        var infix = Vector.new();
                        infix = indexesPrefixToInfix(listOfIndexedForms[i], infix);
                        var formInfix = createInfixFormFromIndexesInfix(infix);
                        var latex = formToLatex(formInfix);
                        
                        if(i < (listOfIndexedForms.size - 2))
                                setLatex += latex + ", ";
                        else if(i == (listOfIndexedForms.size - 2))
                                        setLatex += latex;
                                 else if(i == (listOfIndexedForms.size - 1))
                                                litLatex = latex;
                                                
        }
                if(setLatex != "\\{")
                        allLatex = setLatex + ", " + litLatex + "\\}";
                else
                        allLatex = setLatex + litLatex + "\\}";
                
                return allLatex;
}

function formToLatex(form)
{
        var i;
        var len = String.len(form);
        
        var newForm = String.replace(form, "A", " \\lor ");
                newForm = String.replace(newForm, "K", " \\land ");
                newForm = String.replace(newForm, "C", " \\to ");
                newForm = String.replace(newForm, "E", " \\equiv ");
                newForm = String.replace(newForm, "N", " \\lnot ");
                                
        return newForm;
}

function createInfixFormFromIndexesInfix(indexesInfix)
{
        var form = "";
        var i;
        var symbolType = 0;
        for(i = 0; i < indexesInfix.size; i++)
        {
                symbolType = typeof(indexesInfix[i]);
                if(symbolType != 0)
                {
                        if(symbolType == 3)
                        {
                                form += indexesInfix[i];
                        }
                        else
                        {
                                form += g_symbolsChart[indexesInfix[i]];
                        }
                }
                else
                        return Simulator.print("There is a problem with symbols in the indexed infix form!");
        }
        
        return form;
}

function indexesPrefixToInfix(listOfIndexes, infix)
{
        var symbol = listOfIndexes[0];
                
        if((symbol == 1) || (symbol == 2) || (symbol == 3))
        {
                        var args = getIndexedMainArgs(listOfIndexes);
                        infix.add("(");
                        infix = indexesPrefixToInfix(args[0],infix);
                        infix.add(symbol);
                        infix = indexesPrefixToInfix(args[1], infix);
                        infix.add(")");
                        return infix;
        }
        else
        {
                if(symbol == 0)
                {
                        infix.add(symbol);
                        var args = getIndexedMainArgs(listOfIndexes);
                        infix = indexesPrefixToInfix(args[0], infix);
                        return infix;
                }
                else
                {
                        infix.add(symbol);
                        return infix;
                }
        }
}

function getIndexedConjunctionFromLiterals(indexedListOfLiterals)
{
        var i,j;
        var result = Vector.new();
        
        
        
        for(j = 0; j < indexedListOfLiterals[0].size; j++)
                result.add(indexedListOfLiterals[0][j]);
        
        for(i = 1; i < indexedListOfLiterals.size; i++)
        {
                result = plainListCopyInsert(result, 0, [1]);
                for(j = 0; j < indexedListOfLiterals[i].size; j++)
                        result.add(indexedListOfLiterals[i][j]);
                
        }
        
        return result;
}

function formulaFromLiterals(literals)
{
        var i,j;
        var form = convertIndexesToForm(literals[0]);
        
        
        for(i = 1; i < literals.size; i++)
                form = "K" + form + convertIndexesToForm(literals[i]);
                
        return form;
}

function convertIndexesToForm(setOfIndexes)
{
        var form = "";
        var i;
        
        for(i = 0; i < setOfIndexes.size; i++)
        {
                form += g_symbolsChart[setOfIndexes[i]];        
        }
        
        return form;
}

function getFormListFromIndexes(literalsListsIndexed)
{
        var i,j;
        var new = Vector.new();
        for(i = 0; i < literalsListsIndexed.size; i++)
        {
                new.add(Vector.new());
                
                for(j = 0; j < literalsListsIndexed[i].size; j++)
                        new[i].add(convertIndexesToForm(literalsListsIndexed[i][j]));
        }
        
        return new;
}

function convertLiteralsToNumbers(setOfLiteralsIndexed)
{
        var i;
        var result = Vector.new();
        
        for(i = 0; i < setOfLiteralsIndexed.size; i++)
        {
                if(setOfLiteralsIndexed[i].size > 0 && setOfLiteralsIndexed[i].size < 3)
                {
                        if(setOfLiteralsIndexed[i][0] == 0)
                                result.add(setOfLiteralsIndexed[i][1]);
                        else
                                result.add(100+setOfLiteralsIndexed[i][0]);
                }
                else
                {
                        Simulator.print("There is a problem with entangled literals!");
                }
        }
        return result;
}

function convertNumbersToLiterals(setOfNumbers)
{
        var i;
        var result = Vector.new();
        
        for(i = 0; i < setOfNumbers.size; i++)
        {
                if(setOfNumbers[i] != 0)
                {
                        if(setOfNumbers[i] < 100)
                        {
                                result.add([0,setOfNumbers[i]]);
                        }
                        else
                        {
                                result.add([setOfNumbers[i]%100]);
                        }
                }
                else
                        Simulator.print("There is a problem with entangled literals!");
        }
        
        return result;
}