open Parser_entry
open Affichage
open Typing
open Proof
open Types

type entry =
  Simple of Lam.lam
  | Reduce of Lam.lam
  | AlphaEquiv of Lam.lam * Lam.lam


let parse_lam t =
  match Parser.main Lexer.token t with
  | Lam l -> l
  | Cmd _ -> failwith "entry must be a lam"

let parse_cmd t =
  match Parser.main Lexer.token t with
  | Cmd c -> c
  | Lam _ -> failwith "entry must be a cmd"

let beta_reduce e =
  let rec aux = function
    Some e ->
      print_expr e;
      print_newline ();
      aux (Lam.betastep e);
    | None -> ()
  in print_expr e;
  print_newline ();
  let e = Lam.alpha_convert ~readable:true e in
  print_expr e;
  print_newline ();
  aux (Lam.betastep e)

let alpha_get_lam where_from =
  let input_str = In_channel.input_all where_from in
  match Str.split (Str.regexp "&") input_str with
    [s1; s2] -> AlphaEquiv (
          parse_lam (Lexing.from_string (s1^"\n")),
          parse_lam (Lexing.from_string s2)
        )
    | _ -> failwith "Alpha-equivalence: nombre de delimiteurs incorrect"

let rec interactive ((g, gs) : proof) : proof =
  begin
    let fresh_proof (ty : ty) =
      (Some (Ref (ref Hole), ty, []), [])
    in

    let _ = match g with
    None -> print_string "No more goals.\n"
    | Some g' -> print_goal g'
    in

    match parse_cmd (Lexing.from_string ((read_line ())^"\n")) with
    Goal ty -> fresh_proof ty |> interactive
    | Tact t ->
      begin match t with
        Exact_term e ->
          tact_exact_term (g, gs) e |> interactive
        | Exact_proof s ->
            tact_exact_proof (g, gs) s |> interactive
        | Assumption ->
          tact_assumption (g, gs) |> interactive
        | Intro ->
          tact_intro (g, gs) |> interactive
        | Cut ty ->
          tact_cut (g, gs) ty |> interactive
        | Apply id ->
          tact_apply (g, gs) id |> interactive
      end
  end

let interpret e =
  begin
    print_expr e;
    print_newline();
    print_ty (typeinfer [] e);
    print_newline();
    let _ = interactive (None, []) in ()
  end

let nom_fichier = ref ""
let reduce = ref false
let alpha = ref false
let equiv_fichier = ref ""

let parse_channel_lam c =
  let lexbuf = Lexing.from_channel c in
  parse_lam lexbuf

let recupere_entree () =
  let optlist = [
   ("-alpha",
   Arg.Set alpha,
   "Vérifie l'alpha équivalence de deux termes séparés par &");
   ("-reduce",
   Arg.Set reduce,
   "Affiche les réductions successives du lambda-terme")
  ] in

  let usage = "Bienvenue à bord." in  (* message d'accueil, option -help *)

  Arg.parse (* ci-dessous les 3 arguments de Arg.parse : *)
    optlist (* la liste des options definie plus haut *)

    (fun s -> nom_fichier := s) (* la fonction a declencher lorsqu'on recupere un string qui n'est pas une option : ici c'est le nom du fichier, et on stocke cette information dans la reference nom_fichier *)
    usage; (* le message d'accueil *)

  try
    let where_from = match !nom_fichier with
      | "" -> stdin
      | s -> open_in s in
    if !alpha
    then alpha_get_lam where_from
    else if !reduce
    then Reduce (parse_channel_lam where_from)
    else Simple (parse_channel_lam where_from)
  with e -> (Printf.printf "problème de saisie\n"; raise e)

(* la fonction principale *)
let run () =
  try
    match recupere_entree () with
     Simple l -> let _ = interpret l in ()
    | Reduce l -> let _ = beta_reduce l in ()
    | AlphaEquiv (l1, l2) -> begin
        if ((Lam.(=~)) l1 l2) then
          print_string "true\n"
        else
          print_string "false\n"
      end;
    flush stdout
  with e -> raise e

let _ = run ()