open Printf
open AlphaLib
open F
open FTypeChecker

(* -------------------------------------------------------------------------- *)

(* Typechecking a term. *)

let check (t : raw_term) =
  printf "Raw term:\n%a\n"
    Print.term t
  ;
  let t : nominal_term =
    import_term KitImport.empty t
  in
  printf "Imported (and reexported) term:\n%a\n"
    Print.term (export_term KitExport.empty t)
  ;
  match typeof t with
  | ty ->
      printf "Inferred type:\n%a\n"
        Print.typ (export_typ KitExport.empty ty)
  | exception NotAnArrow ty ->
      printf "Type error: this is not a function type:\n%a\n"
        Print.typ ty
  | exception NotAProduct ty ->
      printf "Type error: this is not a product type:\n%a\n"
        Print.typ ty
  | exception NotAForall ty ->
      printf "Type error: this is not a universal type:\n%a\n"
        Print.typ ty

(* -------------------------------------------------------------------------- *)

let () =
  let argc = Array.length Sys.argv in
  if argc > 1 then
    let f = open_in @@ Array.get Sys.argv 1 in
    check @@ Parser.top_level Lexer.prog (Lexing.from_channel f);
    close_in f
  else print_endline "You must give a file."