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 = 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, "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, hyp) = 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 *)
        Printf.printf "There are %d hypothesis\n" (List.length hyp);

        (* 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

    match tactic with
      | Intro var -> (
            match ty with
              | TImpl (ty1, ty2) -> (
                    subgoals := (ty2, (var, ty1) :: hyp) :: !subgoals;
                    let f = !fill_holes in
                    fill_holes := fun holes -> match holes with
                      | h :: hs -> f (LFun (var, ty1, h) :: hs)
                      | _ -> fail ()
                )
              | _ -> failwith "Can't intro"
        )
done;

Printf.printf "Final proof :\n%s" (string_of_lam (!fill_holes []));;