open Structs;;
open Pieuvre;;

(* 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 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 lexbuf
    with e -> (
        Printf.printf "Can't parse type\n";
        raise e
    )
in

Printf.printf "%s\n" (string_of_ty ty);;