#include "type.h"
#include "typesubstitution.h"
#include "substitution.h"
#include "term.h"
#include "textconverter.h"
#include "atrsreader.h"
#include "environment.h"
#include "typer.h"
#include "matchrule.h"
#include <iostream>

int main() {
  TextConverter converter;
  Alphabet Sigma;
  Sigma.add("map", converter.TYPE("($a -> $a) -> list($a) -> list($a)"));
  Sigma.add("nil", converter.TYPE("list($a)"));
  Sigma.add("cons", converter.TYPE("$a -> list($a) -> list($a)"));
  Sigma.add("0", converter.TYPE("nat"));
  Sigma.add("s", converter.TYPE("nat -> nat"));
  Sigma.add("plus", converter.TYPE("nat -> nat -> nat"));
  Sigma.add("minus", converter.TYPE("nat -> nat -> nat"));
  Sigma.add("if", converter.TYPE("bool -> $a -> $a -> $a"));
  Sigma.add("true", converter.TYPE("bool"));
  Sigma.add("false", converter.TYPE("bool"));

  vector<MatchRule*> rules;
  
  PTerm left, right;
  converter.RULE("map F nil", "nil", Sigma, left, right);
  cout << "Found left, right." << endl;
  if (left != NULL && right != NULL) rules.push_back(new MatchRule(left, right));
  cout << "Made rule." << endl;
  PTerm l, r;
  cout << "About to convert." << endl;
  converter.RULE("map F (cons H T)", "cons (F H) (map F T)", Sigma, l, r);
  cout << "Found left, right again." << endl;
  if (l != NULL && r != NULL) rules.push_back(new MatchRule(l, r));
  else cout << converter.query_warning() << endl;
  cout << "Made final rule." << endl;
  for (int i = 0; i < rules.size(); i++) cout << rules[i]->to_string() << endl;

  return 0;

/*
  ATRSreader reader;
  
  if (!reader.read("benchmarks/001.trs"))
    cout << reader.query_warning() << endl;
  else
    cout << "Succes!" << endl;
  return 0;
*/
}

