package at.ac.tuwien.dbai.alternation.gui.example;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import at.ac.tuwien.dbai.alternation.examples.Horn;
import at.ac.tuwien.dbai.alternation.gui.DefaultFormat;
import at.ac.tuwien.dbai.alternation.gui.MainFrame;
import at.ac.tuwien.dbai.alternation.runtime.ComputationTree;

public class HornTest {

    /*
     * some methods to create a Horn formula
     */
    private static void addRule(Map<Character, Set<Set<Character>>> rules,
            char head, Set<Character> body) {
        if (rules.containsKey(head)) {
            rules.get(head).add(body);
        } else {
            rules.put(head, new HashSet<Set<Character>>());
            rules.get(head).add(body);
        }
    }
    private static void addBinaryRule(
            Map<Character, Set<Set<Character>>> rules, char head, char body1,
            char body2) {
        Set<Character> body = new HashSet<Character>();
        body.add(body1);
        body.add(body2);
        addRule(rules, head, body);
    }
    private static void addLiteral(Map<Character, Set<Set<Character>>> rules,
            char head) {
        if (!rules.containsKey(head)) {
            rules.put(head, new HashSet<Set<Character>>());
        }
    }

    /**
     * The format-class for the GUI
     *
     */
    private static class HornFormatMath extends DefaultFormat<Horn.Inputtape,
    Horn.Worktape> {

        public String getLongInformation(Horn.Worktape tape, String state) {
            if(state.equals("head")){
                return "Proof the literal: "+tape.head;
            } else {
                if (state.equals("body")){
                    return "Proof the rule body:\n "+tape.body;
                } else {
                    throw new RuntimeException("Not a valid Horn state.");
                }

            }
        }

        public String getShortInformation(Horn.Worktape tape, String state) {
            if(state.equals("head")){
                return ""+tape.head;
            } else {
                if (state.equals("body")){
                    return tape.body.toString();
                } else {
                    throw new RuntimeException("Not a valid Horn state.");
                }

            }
        }
    }

    /**
     * Executes the HORN ALter-Java program on an instance and visualizes the
     resulting computation tree in the Alter-Java GUI.
     *
     *
     * @param args
     */
    public static void main(String[] args) {
        // creating an instance
        Set<Character> facts = new HashSet<Character>();
        Map<Character, Set<Set<Character>>> rules = new HashMap<Character, Set<
                                                    Set<Character>>>();
        char goal;
        facts.add('a');
        facts.add('b');
        goal = 'g';
        addBinaryRule(rules, 'c', 'a', 'b');
        addBinaryRule(rules, 'e', 'a', 'c');
        addBinaryRule(rules, 'f', 'b', 'e');
        addBinaryRule(rules, 'g', 'b', 'f');
        addBinaryRule(rules, 'g', 'b', 'f');
        addBinaryRule(rules, 'g', 'd', 'a');
        addBinaryRule(rules, 'g', 'd', 'b');
        addBinaryRule(rules, 'g', 'd', 'c');
        addBinaryRule(rules, 'g', 'd', 'e');
        addBinaryRule(rules, 'g', 'd', 'f');
        addBinaryRule(rules, 'c', 'd', 'a');
        addBinaryRule(rules, 'e', 'd', 'a');
        addBinaryRule(rules, 'f', 'd', 'b');
        addBinaryRule(rules, 'f', 'd', 'e');
        addLiteral(rules, 'd');
        addLiteral(rules, 'h');

        // execute the Alter-Java program
        Horn atm = new Horn();
        atm.compute(goal, rules, facts);
        // get the computation tree
        ComputationTree<Horn.Worktape> cT = atm.getComputationTree();

        // start the GUI
        new MainFrame<Horn.Inputtape, Horn.Worktape>(cT, new HornFormatMath());
    }


}