package edu.osu.cse.groenkeb.logic.test;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
import java.util.Scanner;
import java.util.stream.Stream;

import com.google.common.collect.ImmutableSet;

import edu.osu.cse.groenkeb.logic.Absurdity;
import edu.osu.cse.groenkeb.logic.Sentence;
import edu.osu.cse.groenkeb.logic.Term;
import edu.osu.cse.groenkeb.logic.model.Domain;
import edu.osu.cse.groenkeb.logic.model.FirstOrderModel;
import edu.osu.cse.groenkeb.logic.parse.SentenceParser;
import edu.osu.cse.groenkeb.logic.parse.SentenceParserOpts;
import edu.osu.cse.groenkeb.logic.proof.NaiveProofStrategy;
import edu.osu.cse.groenkeb.logic.proof.ProofContext;
import edu.osu.cse.groenkeb.logic.proof.ProofResult;
import edu.osu.cse.groenkeb.logic.proof.ProofSolver;
import edu.osu.cse.groenkeb.logic.proof.Success;
import edu.osu.cse.groenkeb.logic.proof.types.Premise;
import edu.osu.cse.groenkeb.logic.proof.types.ProudPremise;
import edu.osu.cse.groenkeb.logic.test.CommandProcessor.Command;
import edu.osu.cse.groenkeb.utils.Convert;
import scala.collection.JavaConversions;

public class ModelVerificationCommandProcessor implements CommandProcessor<ModelVerificationContext>
{
  private static final String QUERY = "?";
  private static final String SET = "$";
  
  private final Scanner input;
  private final SentenceParser parser;
  private final SentenceParserOpts opts;
  
  public ModelVerificationCommandProcessor(final Scanner input, final SentenceParser parser, final SentenceParserOpts opts)
  {
    this.input = input;
    this.parser = parser;
    this.opts = opts;
  }
  
  @Override
  public Command<ModelVerificationContext> tryParseNextCommand() throws InvalidCommandException
  {
    final String next = input.nextLine();
    if (next == null || next.isEmpty()) return null;
    
    final String cmdStr = next.substring(1, next.length()).trim();
    try
    {
      if (next.startsWith(QUERY))
      {
        return parseQuery(cmdStr);
      }
      else if (next.startsWith(SET))
      {
        return parseSet(cmdStr);
      }
    }
    catch (Exception e)
    {
      e.printStackTrace ();
      throw new InvalidCommandException("unable to parse input: " + e.getMessage());
    }
    
    throw new InvalidCommandException("unrecognized command string: " + next);
  }
  
  public QueryCommand parseQuery(final String input)
  {
    final Sentence querySentence = this.parser.parse(input, opts);
    return new QueryCommand(querySentence);
  }
  
  public SetCommand parseSet(final String input)
  {
    Domain auxDomain = new Domain(Convert.emptyScalaSeq ());
    final List<Sentence> sentences = new ArrayList<Sentence>();
    for (final String pt : input.split(";"))
    {
      final String str = pt.trim();
      if (str.startsWith("{") && str.endsWith("}"))
      {
        final List<String> termStrs = Arrays.asList(str.substring(1, str.length() - 1).split(","));
        final Stream<Term> terms = termStrs.stream().map((String s) -> new Term(s));
        auxDomain = auxDomain.merge(new Domain(Convert.toScalaSeq(terms::iterator)));
      }
      else
      {
        sentences.add(this.parser.parse(pt, this.opts));
      }
    }
    
    final FirstOrderModel model = FirstOrderModel.from(Convert.toScalaSeq(sentences));
    return new SetCommand(model.withDomain(auxDomain));
  }
  
  private class QueryCommand implements Command<ModelVerificationContext>
  {
    private final Sentence sentence;
    private final ProofSolver solver = new ProofSolver(new NaiveProofStrategy());
    
    QueryCommand(final Sentence sentence)
    {
      this.sentence = sentence;
    }
    
    @Override
    public ModelVerificationContext execute(ModelVerificationContext current)
    {
      final ProofContext verifyProofContext = new ProofContext(this.sentence, current.getModel().rules(), Convert.<Premise>emptyScalaSet());
      final ImmutableSet<Premise> falsifyPremiseSet = ImmutableSet.of (new ProudPremise(this.sentence));
      final ProofContext falsifyProofContext = new ProofContext(new Absurdity(), current.getModel().rules(), Convert.toScalaSet (falsifyPremiseSet));
      final scala.collection.immutable.Stream <ProofResult> verifyResults = solver.prove(verifyProofContext);
      final java.util.Iterator<ProofResult> results = JavaConversions.asJavaIterator (verifyResults.iterator ());
      while (results.hasNext())
      {
        ProofResult result = results.next();
        if (result instanceof Success)
        {
          System.out.println(result);
        }
      }
      return current;
    }
  }
  
  private class SetCommand implements Command<ModelVerificationContext>
  {
    private final FirstOrderModel model;
    
    SetCommand(FirstOrderModel model)
    {
      this.model = model;
    }
    
    public ModelVerificationContext execute(ModelVerificationContext current)
    {
      return new ModelVerificationContext(model);
    }
  }
}

@@ -612,235 +612,9 @@
 oof.
-NaiveProofStrategy;%0Aimport edu.osu.cse.groenkeb.logic.proof.ProofContext;%0Aimport edu.osu.cse.groenkeb.logic.proof.ProofResult;%0Aimport edu.osu.cse.groenkeb.logic.proof.ProofSolver;%0Aimport edu.osu.cse.groenkeb.logic.proof.Success
+*
 ;%0Aim
@@ -730,73 +730,8 @@
 se;%0A
-import edu.osu.cse.groenkeb.logic.test.CommandProcessor.Command;%0A
 impo
@@ -3959,22 +3959,16 @@
 ;%0A      
-final 
 java.uti
@@ -4209,34 +4209,522 @@
     
-System.out.println(result)
+ProofUtils.prettyPrint (((Success) result).proof ());%0A          return current;%0A        %7D%0A      %7D%0A      %0A      final scala.collection.immutable.Stream%3CProofResult%3E falsifyResults = solver.prove(falsifyProofContext);%0A      results = JavaConversions.asJavaIterator (falsifyResults.iterator());%0A      while (results.hasNext())%0A      %7B%0A        ProofResult result = results.next();%0A        if (result instanceof Success)%0A        %7B%0A          ProofUtils.prettyPrint (((Success) result).proof ());%0A          return current
 ;%0A  
@@ -4735,24 +4735,31 @@
   %7D%0A      %7D%0A
+      %0A
       return

Update verify program command processor.