Main.ml 1.16 KB
Newer Older
1
2
3
4
5
open Printf
open AlphaLib
open F
open FTypeChecker

6
7
8
9
(* -------------------------------------------------------------------------- *)

(* Typechecking a term. *)

POTTIER Francois's avatar
POTTIER Francois committed
10
11
let check (t : raw_term) =
  printf "Raw term:\n%a\n"
12
13
    Print.term t
  ;
POTTIER Francois's avatar
POTTIER Francois committed
14
15
16
17
  let t : nominal_term =
    import_term KitImport.empty t
  in
  printf "Imported (and reexported) term:\n%a\n"
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
    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 () =
37
38
39
40
41
42
  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."
43