use difx::def_rules::Rule;
use difx::match_rules::{self, Bindings};
use difx::simplify;
use difx::sexpr::{Expr, Parser};
use rustyline::DefaultEditor;
use rustyline::error::ReadlineError;

const MAX_REWRITE_ITERS: usize = 100;

fn parse_expr(input: &str) -> Option<Expr> {
    std::panic::catch_unwind(|| {
        let mut parser = Parser::new(input);
        parser.parse_one()
    })
    .ok()
}

fn rewrite_node(rules: &[Rule], expr: &Expr) -> Option<(usize, Expr)> {
    for (idx, rule) in rules.iter().enumerate() {
        let mut bindings = Bindings::default();
        if match_rules::matches(&rule.lhs, expr, &mut bindings) {
            let rewritten = match_rules::substitute(&rule.rhs, &bindings);
            return Some((idx, rewritten));
        }
    }

    None
}

fn rewrite_top_down_once(rules: &[Rule], expr: &Expr) -> Option<(usize, Expr)> {
    if let Some(hit) = rewrite_node(rules, expr) {
        return Some(hit);
    }

    match expr {
        Expr::Atom(_) => None,
        Expr::Application(items) => {
            for (idx, item) in items.iter().enumerate() {
                if let Some((rule_idx, rewritten_child)) = rewrite_top_down_once(rules, item) {
                    let mut rewritten_items = items.clone();
                    rewritten_items[idx] = rewritten_child;
                    return Some((rule_idx, Expr::Application(rewritten_items)));
                }
            }

            None
        }
        Expr::OrderedList(items) => {
            for (idx, item) in items.iter().enumerate() {
                if let Some((rule_idx, rewritten_child)) = rewrite_top_down_once(rules, item) {
                    let mut rewritten_items = items.clone();
                    rewritten_items[idx] = rewritten_child;
                    return Some((rule_idx, Expr::OrderedList(rewritten_items)));
                }
            }

            None
        }
    }
}

fn main() {
    let input = include_str!("../base.rules");
    let rules = difx::def_rules::parse_def_rules(input.to_string());

    println!("Loaded {} rule(s) from base.rules", rules.len());

    let mut rl = DefaultEditor::new().expect("failed to initialize line editor");

    loop {
        let line = match rl.readline("> ") {
            Ok(line) => line,
            Err(ReadlineError::Interrupted) => {
                println!("^C");
                continue;
            }
            Err(ReadlineError::Eof) => {
                println!();
                break;
            }
            Err(err) => {
                eprintln!("Readline error: {err}");
                break;
            }
        };

        let line = line.trim();
        if line.is_empty() {
            continue;
        }

        if let Err(err) = rl.add_history_entry(line) {
            eprintln!("history error: {err}");
        }

        let Some(mut expr) = parse_expr(line) else {
            println!("Parse error");
            continue;
        };

        let mut applied = 0usize;
        while applied < MAX_REWRITE_ITERS {
            let Some((idx, rewritten_expr)) = rewrite_top_down_once(&rules, &expr) else {
                break;
            };
            let next_expr = simplify::simplify(rewritten_expr);

            let rule = &rules[idx];
            println!("{}.", applied + 1);
            println!("```lisp\n{} => {}\n```", rule.lhs, rule.rhs);
            println!("> {}", next_expr);

            expr = next_expr;
            applied += 1;
        }

        if applied == 0 {
            println!("NO MATCH");
        } else {
            println!("final: {}", expr);
        }

        let stopped = applied == MAX_REWRITE_ITERS;
        if applied == MAX_REWRITE_ITERS {
            let stop_msg = format!("Stopped after {} iterations (safety limit).", MAX_REWRITE_ITERS);
            println!("{}", stop_msg);
        }
    }
}