open Structs;;
open Pieuvre;;

let fail () =
    failwith "Unknown error";;

(* Parsage des arguments*)
let filename = ref "" in

let reduce = ref false in
let alpha = ref false in
let typecheck_option = ref false in

Arg.parse
    [("-reduce", Arg.Set reduce, "Show the step-by-step reduction of a lambda-term");
     ("-alpha", Arg.Set alpha, "Check is two lambda-terms separated by '&' are alpha-convertible");
     ("-typecheck", Arg.Set typecheck_option, "Check if a lambda term has a given type")]
    (fun s -> filename := s)
    "The available options are:";

(* Ouverture éventuelle du fichier *)
let file = match !filename with
  | "" -> None
  | fn -> Some (open_in fn)
in
let is_interactive = match file with
  | None -> true
  | _ -> false
in

let readline () = match file with
  | None -> (
        Printf.printf ">>> ";
        flush stdout;
        read_line ()
    )
  | Some f -> input_line f
in

(* Show a message only if the input is read from stdin *)
let show s = match file with
  | None -> Printf.printf "%s" s
  | _ -> ()
in

show "Please type the formula to prove\n";

let ty =
    try
        let lexbuf = Lexing.from_string (readline ()) in
        Parser.main_type Lexer.token_ty lexbuf
    with e -> (
        Printf.printf "Can't parse type\n";
        raise e
    )
in

let subgoals: (ty * (var_lambda * ty) list) list ref = ref [(ty, [])] in

(* On donne en paramètre une liste contenant un lambda-terme par trou (ie subgoal),
 * et elle renvoie le lambda-terme complet (en remplaçant les trous) *)
let fill_holes = ref (fun holes -> List.hd holes) in

while !subgoals <> [] do
    let (ty, hyps) = List.hd !subgoals in
    subgoals := List.tl !subgoals;

    if is_interactive then (
        (* Nettoyage du terminal *)
        let _ = Sys.command("clear -x") in

        (* Affichage des hypothèses *)
        List.iter (fun (var, h) -> Printf.printf "%s: %s\n" var (string_of_ty h)) hyps;

        (* Affichage des sous-buts *)
        Printf.printf "================\n";
        Printf.printf "%s\n" (string_of_ty ty);

        (* Lecture d'une tactique *)
        Printf.printf "What do you want to do?\n"
    );

    let tactic =
        let rec read_tactic () =
            try
                let lexbuf = Lexing.from_string (readline ()) in
                Parser.main_tactic Lexer.token_tactic lexbuf
            with e -> (
                  Printf.printf "Can't parse tactic\n";
                  if is_interactive then
                      read_tactic ()
                  else
                      raise e
            )
        in
        read_tactic ()
    in

    let f = !fill_holes in

    match tactic with
      | Intro var -> (
            match ty with
              | TImpl (ty1, ty2) -> (
                    subgoals := (ty2, (var, ty1) :: hyps) :: !subgoals;
                    fill_holes := fun holes -> match holes with
                      | h :: hs -> f (LFun (var, ty1, h) :: hs)
                      | _ -> fail ()
                )
              | _ -> failwith "Can't intro"
        )
      | Assumption -> (
            let rec explore = function
              | (var, hyp) :: _ when hyp = ty -> (
                    fill_holes := fun holes -> f ((LVar var) :: holes)
                )
              | [] -> failwith "No such hypothesis"
              | _ :: hyps -> explore hyps
            in
            explore hyps
        )
      | Apply var -> (
            let rec explore = function
              | (var_hyp, TImpl (t1, t2)) :: _ when var_hyp = var && t2 = ty -> (
                    subgoals := (t1, hyps) :: !subgoals;
                    fill_holes := function
                      | hole :: holes -> f ((LApp (LVar var_hyp, hole)) :: holes)
                      | [] -> fail ()
                )
              | [] -> failwith ("Hypothesis " ^ var ^ " not found or unusable")
              | _ :: hyps -> explore hyps
            in
            explore hyps;
        )
done;

let finalLam = !fill_holes [] in
    if (typecheck [] finalLam ty) then
        Printf.printf "Final proof :\n%s\n" (string_of_lam finalLam)
    else (
        Printf.printf "Invalid proof constructed !\n";
        Printf.printf "%s can't be typed with %s.\n" (string_of_lam finalLam) (string_of_ty ty);
        Printf.printf "The whole development team of pieuvre is sorry for the damage eventually done by this error.\n"
    )
;;