open Structs;;
open Pieuvre;;
open Tactic;;
    
(* Lorsqu'une tactique ne peut se lancer. Contient la tactique ainsi qu'un message contenant l'erreur.*)
exception TacticException of tactic*string;;
(* Lorsqu'une tactique est mal écrite*)
exception TacticParseException;;
(* Exception renvoyée lorsque la fonction de trou est appelée sur une liste trop grande. *)
(* Ne devrait jamais être lancée *)
exception TrouException;;

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

let reduce_option = ref false in
let alpha_option = ref false in
let typecheck_option = ref false in

Arg.parse
    [("-reduce", Arg.Set reduce_option, "Show the step-by-step reduction of a lambda-term");
     ("-alpha", Arg.Set alpha_option, "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

if !reduce_option then (
    let lexbuf = Lexing.from_channel (match file with
      | None -> stdin
      | Some file -> file
    )
    in
    let lambda_term =
        try
            Parser.main_lambda Lexer.token lexbuf
        with e -> (
            Printf.printf "Can't read lambda term\n";
            raise e
       )
    in
    reduce lambda_term;
    exit 0
);

if !alpha_option then (
    let lexbuf = Lexing.from_channel (match file with
      | None -> stdin
      | Some file -> file
    )
    in
    let lam1, lam2 =
        try
            Parser.main_two_lambda Lexer.token lexbuf
        with e -> (
            Printf.printf "Can't read lambda terms\n";
            raise e
       )
    in
    if alpha lam1 lam2 then (
        Printf.printf "%s and %s are α-equivalent\n" (string_of_lam lam1) (string_of_lam lam2)
    ) else (
        Printf.printf "%s and %s are not α-equivalent\n" (string_of_lam lam1) (string_of_lam lam2)
    );
    exit 0
);

(*if !typecheck_option then (
    let lexbuf = Lexing.from_channel (match file with
      | None -> stdin
      | Some file -> file
    )
    in
    let lambda_term =
        try
            Parser.main_lambda Lexer.token lexbuf
        with e -> (
            Printf.printf "Can't read lambda term\n";
            raise e
       )
    in
    Printf.printf "The type of %s is " (string_of_lam lambda_term);
    if typecheck [] lambda_term then (
        Printf.printf "correct\n"
    ) else (
        Printf.printf "incorrect\n"
    );
    exit 0
);*)

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

    let find_hyp (var: var_lambda) : ty option =
        let rec explore = function
          | [] -> None
          | (var_hyp, hyp) :: hyps when var_hyp = var -> Some hyp
          | _ :: hyps -> explore hyps
        in
        explore hyps
    in


    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);
        List.iter (fun (ty, _) ->
            Printf.printf "%s\n" (string_of_ty ty)
        ) !subgoals;

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

    let rec read_tactic () =
        try
            let lexbuf = Lexing.from_string (readline ()) in
            Parser.main_tactic Lexer.token lexbuf
        with e -> raise TacticParseException
    in
    
    let applyTactic tactic =
        begin
        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)
                        | _ -> raise TrouException
                    )
                | _ -> raise (TacticException(tactic,"Cannot intro when the goal is no implication."))
            )
        | Assumption -> (
                let rec explore = function
                | (var, hyp) :: _ when hyp = ty -> (
                        fill_holes := fun holes -> f ((LVar var) :: holes)
                    )
                | [] -> raise (TacticException(tactic,"Cannot find a tactic that equals the goal."))
                | _ :: hyps -> explore hyps
                in
                explore hyps
            )
        | Apply var -> (
                match find_hyp var with
                | Some (TImpl (t1, t2)) when t2 = ty -> (
                        subgoals := (t1, hyps) :: !subgoals;
                        fill_holes := function
                        | hole :: holes -> f ((LApp (LVar var, hole)) :: holes)
                        | [] -> raise TrouException
                    )
                | None -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it does not exist."))
                | _ -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it is no implication."))
            )
        | Elim var -> (
                match find_hyp var with
                | Some TFalse -> fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes)
                | Some TAnd(tl,tr) -> (
                        subgoals := (TImpl(tl,TImpl(tr,ty)),hyps)::!subgoals;
                        fill_holes := fun holes -> match holes with
                        | h::r -> f ((LApp(LApp(h,LFst(LVar(var))),LSnd(LVar(var))))::r)
                        | _ -> raise TrouException
                    )
                | Some TOr(tl,tr) -> (
                        subgoals := (TImpl(tl,ty),hyps)::(TImpl(tr,ty),hyps)::!subgoals;
                        fill_holes := fun holes -> match holes with
                        | hl::hr::r -> f (LCase(LVar(var),hl,hr)::r)
                        | _ -> raise TrouException
                    )
                | None -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it does not exist."))
                | _ -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it is neither an implication, nor a /\\ or a \\/"))
            )
        (* Pour montrer A, on montre B -> A et B *)
        | Cut tint -> (
                subgoals := (TImpl (tint, ty), hyps) :: (tint, hyps) :: !subgoals;
                fill_holes := function
                | pf :: px :: s -> f ((LApp (pf, px)) :: s)
                | _ -> raise TrouException
            )

        | Split -> (
                match ty with
                | TAnd(t1,t2) -> (
                        subgoals := (t1, hyps) :: (t2, hyps) :: !subgoals;
                        fill_holes := fun holes -> match holes with
                        | h1 :: h2 :: hs -> f (LCouple(h1,h2) :: hs)
                        | _ -> raise TrouException
                    )
                | _ -> raise (TacticException(tactic,"Cannot split as the goal is no /\\ clause"))
            )
        | Left -> (
                match ty with
                | TOr(tl,tr) -> (
                        subgoals := (tl, hyps) :: !subgoals;
                        fill_holes := fun holes -> match holes with
                        | hl :: hs -> f (LIg(hl,tr) :: hs)
                        | _ -> raise TrouException
                    )
                | _ -> raise (TacticException(tactic,"Cannot prove left as the goal is no \\/ clause"))
            )
        | Right -> (
                match ty with
                | TOr(tl,tr) -> (
                        subgoals := (tr, hyps) :: !subgoals;
                        fill_holes := fun holes -> match holes with
                        | hr :: hs -> f (LId(hr,tl) :: hs)
                        | _ -> raise TrouException
                    )
                | _ -> raise (TacticException(tactic,"Cannot prove right as the goal is no \\/ clause"))
            )
        end
    in
    
    let rec applyUntilWorking () =
        try
            (
                let readTactic = read_tactic () in
                    applyTactic readTactic
            )
        with
            | TacticException(t,s) -> 
                Printf.printf "\027[31mCannot apply the tactic: %s\027[0m\n" s;
                if(is_interactive) then applyUntilWorking () else raise (TacticException(t,s))
            | TacticParseException -> 
                Printf.printf "\027[31mCannot parse the tactic, please refer to pieuvre documentation.\027[0m\n";
                if(is_interactive) then applyUntilWorking () else raise TacticParseException
            | e -> 
                Printf.printf "\027[31mPieuvre Failed Unexpectedly !\027[0m\n";
                raise e
    in
    applyUntilWorking ()
done;

let finalLam = !fill_holes [] in
    if (typecheck [] finalLam ty) then (
        Printf.printf "Final proof :\n";
        reduce 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"
    )
;;