From 7aba10f5fc9f9b0467a09d2c917b84ede441e522 Mon Sep 17 00:00:00 2001 From: Adrien Vannson Date: Mon, 16 May 2022 23:19:18 +0200 Subject: [PATCH] Typecheck --- main.ml | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/main.ml b/main.ml index a15359d..63f1b87 100644 --- a/main.ml +++ b/main.ml @@ -77,6 +77,29 @@ if !alpha_option then ( 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