content: package org.alloytools.alloy.cli;
  
  import java.io.IOException;
  import java.io.InputStream;
  import java.io.OutputStream;
  import java.io.PrintWriter;
  import java.util.List;
  import java.util.stream.Collectors;
  
  import aQute.lib.env.Env;
  import aQute.lib.getopt.Arguments;
  import aQute.lib.getopt.CommandLine;
  import aQute.lib.getopt.Description;
  import aQute.lib.getopt.Options;
  import aQute.libg.qtokens.QuotedTokenizer;
  import edu.mit.csail.sdg.alloy4.TableView;
  import edu.mit.csail.sdg.ast.Command;
  import edu.mit.csail.sdg.ast.Expr;
  import edu.mit.csail.sdg.ast.ExprVar;
  import edu.mit.csail.sdg.parser.CompModule;
  import edu.mit.csail.sdg.translator.A4Solution;
  import edu.mit.csail.sdg.translator.TranslateAlloyToKodkod;
  import jline.console.ConsoleReader;
  import jline.console.completer.StringsCompleter;
  
  /**
   * An evaluator based on a current {@link A4Solution}
   */
  public class Evaluator extends Env {
  	final CompModule	world;
  
  	A4Solution			current;
  	int					state		= 0;
  	String				returnValue	= null;
  
  	final InputStream	in;
  	final OutputStream	out;
  	final PrintWriter	pw;
  
  	public Evaluator(CompModule world, A4Solution solution, InputStream in, OutputStream out) {
  		this.world = world;
  		this.current = solution;
  		this.in = in;
  		this.out = out;
  		this.pw = new PrintWriter(out);
  	}
  
  	String loop() throws Exception {
  
  		try (ConsoleReader reader = new ConsoleReader(in, out);
  				PrintWriter out = new PrintWriter(reader.getOutput())) {
  			reader.setPrompt("> ");
  			CommandLine cl = new CommandLine(this);
  			doCompletions(reader, cl);
  
  			for (String line; (line = reader.readLine()) != null;) {
  				try {
  					out.flush();
  
  					line = line.trim();
  					if (line.isEmpty() || line.startsWith("--") || line.startsWith("//"))
  						continue;
  
  					QuotedTokenizer qt = new QuotedTokenizer(line, " ", false, false);
  					List<String> parts = qt.getTokenSet();
  					String cmd = parts.remove(0);
  
  					if (cmd.startsWith("/")) {
  						String help = cl.execute(this, cmd.substring(1), parts);
  						if (help != null) {
  							out.println(help);
  						}
  
  						if (returnValue != null)
  							return returnValue;
  
  					} else
  						try {
  							world.clearGlobals();
  							for (ExprVar a : current.getAllAtoms()) {
  								world.addGlobal(a.label, a);
  							}
  							for (ExprVar a : current.getAllSkolems()) {
  								world.addGlobal(a.label, a);
  							}
  
  							Expr e = world.parseOneExpressionFromString(line);
  							println(e);
  						} catch (Exception e) {
  							if (e.getClass() != Exception.class)
  								exception(e, "%s %s", e.getMessage(), line);
  						}
  				} catch (Exception e) {
  					exception(e, "unknown error, last line %s", line);
  				}
  				report(out);
  				getErrors().clear();
  				getWarnings().clear();
  			}
  		}
  		return null;
  	}
  
  	@Description("Show basic information about the current solution")
  	interface InfoOptions extends Options {
  		@Description("Show the skolem values")
  		boolean skolems();
  	}
  
  	@Arguments(arg = {})
  	@Description("Show basic information about the current solution")
  	public void _info(InfoOptions options) {
  		pw.println(state + "/" + (current.getTraceLength() - 1));
  		if (options.skolems()) {
  			for (ExprVar a : current.getAllSkolems()) {
  				pw.printf("%-40s %s", a.label, toString(a));
  			}
  		}
  		pw.flush();
  	}
  
  	@Arguments(arg = {})
  	@Description("Set the next state if possible")
  	interface NextOptions extends InfoOptions {
  
  	}
  
  	@Description("Set the state to the next state if possible")
  	public void _next(NextOptions options) {
  		if (state + 1 < current.getTraceLength()) {
  			state++;
  		}
  		_info(options);
  	}
  
  	@Arguments(arg = "new-state")
  	@Description("Adjust the state to a new state. Requires one argument")
  	interface StateOptions extends InfoOptions {
  
  	}
  
  	@Description("Adjust the state to a new state. Requires one argument")
  	public void _state(StateOptions options) {
  		String arg = options._arguments().remove(0);
  		if (!arg.matches("[\\d]+")) {
  			error("not a valid state %s", arg);
  			return;
  		}
  
  		int st = Integer.parseInt(arg);
  		if (st >= current.getTraceLength()) {
  			error("state must be less than %s but is %s", current.getTraceLength(), st);
  			return;
  		}
  		this.state = st;
  		_info(options);
  	}
  
  	@Arguments(arg = {})
  	@Description("Set the previous state if possible")
  	interface PrevOptions extends InfoOptions {
  
  	}
  
  	@Description("Set the previous state if possible")
  	public void _prev(PrevOptions options) {
  		if (state > 0) {
  			state--;
  		}
  		_info(options);
  	}
  
  	@Arguments(arg = {})
  	@Description("exit the shell completely, no continuation even if there is a next solution")
  	interface ExitOptions extends Options {
  
  	}
  
  	@Description("exit the shell completely, no continuation even if there is a next solution")
  	public void _exit(ExitOptions opts) {
  		returnValue = "/exit";
  	}
  
  	@Arguments(arg = { "[command]" })
  	@Description("Commands")
  	interface RunOptions extends InfoOptions {
  
  	}
  
  	@Description("Execute a command or list the commands when no argument given")
  	public void _run(RunOptions opts) throws IOException {
  		List<String> args = opts._arguments();
  		if (args.isEmpty()) {
  			pw.println(getCommands());
  			pw.flush();
  			return;
  		}
  		String name = args.get(0);
  		Command cmd = world.getAllCommands().stream().filter(g -> g.label.equals(name)).findAny().orElse(null);
  		if (cmd == null) {
  			error("no such command %s, existing commands are %s", name, getCommands());
  			return;
  		}
  		doCommand(cmd);
  		_info(opts);
  	}
  
  	private String getCommands() {
  		return world.getAllCommands().stream().map(Object::toString).collect(Collectors.joining("\n"));
  	}
  
  	@Arguments(arg = {})
  	@Description("continue the next solution, if there is one")
  	interface ContinueOptions extends Options {
  
  	}
  
  	@Description("continue the next solution, if there is one")
  	public void _continue(ContinueOptions opts) {
  		returnValue = "/continue";
  	}
  
  	private void doCompletions(ConsoleReader reader, CommandLine cl) {
  		List<String> completions = cl.getCommands(this).keySet().stream().map(s -> "/" + s)
  				.collect(Collectors.toList());
  		completions.add("/exit");
  		completions.add("/continue");
  
  		world.getAllFunc().forEach(f -> completions.add(f.label));
  		world.getAllReachableSigs().forEach(s -> {
  			String label = s.label;
  			int n = label.lastIndexOf('/');
  			if (n >= 0) {
  				label = label.substring(n + 1);
  			}
  			completions.add(label);
  			s.getFields().forEach(field -> {
  				completions.add(field.label);
  			});
  		});
  
  		reader.addCompleter(new StringsCompleter(completions));
  	}
  
  	private void doCommand(Command c) throws IOException {
  		if (c == null) {
  			c = world.getAllCommands().get(0);
  		}
  		SimpleReporter rep = new SimpleReporter(this);
  		current = TranslateAlloyToKodkod.execute_commandFromBook(rep, world.getAllReachableSigs(), c,
  				current.opt);
  		state = 0;
  	}
  
  	private String toString(Expr e) {
  		Object o = current.eval(e, state);
  		if (o != null) {
  			String s = o.toString();
  			if (TableView.isTable(s)) {
  				return TableView.toTable(s, false).toString();
  			}
  			return s;
  		}
  		return "";
  	}
  
  	private void println(Expr e) {
  		pw.println(toString(e));
  		pw.flush();
  	}
  
  }
  