Mysaa/pieuvre
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Remove typecheck

Browse Source
This commit is contained in:
Adrien Vannson 2022-05-16 23:25:40 +02:00
parent b5cad5149c
commit 7439ae817a
No known key found for this signature in database
GPG Key ID: FE2E66FD978C1A55
1 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
main.ml
View File

@ -77,7 +77,7 @@ if !alpha_option then (
exit 0 exit 0
); );
if !typecheck_option then ( (*if !typecheck_option then (
let lexbuf = Lexing.from_channel (match file with let lexbuf = Lexing.from_channel (match file with
| None -> stdin | None -> stdin
| Some file -> file | Some file -> file
@ -92,13 +92,13 @@ if !typecheck_option then (
) )
in in
Printf.printf "The type of %s is " (string_of_lam lambda_term); Printf.printf "The type of %s is " (string_of_lam lambda_term);
if typecheck lambda_term then ( if typecheck [] lambda_term then (
Printf.printf "correct\n" Printf.printf "correct\n"
) else ( ) else (
Printf.printf "incorrect\n" Printf.printf "incorrect\n"
); );
exit 0 exit 0
); );*)
(* Show a message only if the input is read from stdin *) (* Show a message only if the input is read from stdin *)
let show s = match file with let show s = match file with
@ -137,7 +137,7 @@ while !subgoals <> [] do
explore hyps explore hyps
in in
if is_interactive then ( if is_interactive then (
(* Nettoyage du terminal *) (* Nettoyage du terminal *)
let _ = Sys.command("clear -x") in let _ = Sys.command("clear -x") in
@ -231,7 +231,7 @@ while !subgoals <> [] do
| pf :: px :: s -> f ((LApp (pf, px)) :: s) | pf :: px :: s -> f ((LApp (pf, px)) :: s)
| _ -> fail () | _ -> fail ()
) )
| Split ovar -> ( | Split ovar -> (
match ty with match ty with
| TAnd(t1,t2) -> ( | TAnd(t1,t2) -> (