get rid of FTypeCheckerWrapper

This commit is contained in:
Gabriel Scherer 2022-02-07 16:33:31 +01:00
parent 23b53d1e0b
commit 73450444d6
6 changed files with 25 additions and 23 deletions

View File

@ -437,3 +437,9 @@ and binding_pattern datatype_env scrutinee_ty pat =
let typeof datatype_env t =
typeof datatype_env empty t
let typeof_result datatype_env u =
match typeof datatype_env u with
| v -> Ok v
| exception TypeError e ->
Error e

View File

@ -21,6 +21,11 @@ and arity_requirement = Index of int | Total of int
exception TypeError of type_error
(* [typeof env t] type-checks the closed term [t] in datatype environment [env]
and constructs its type. *)
and constructs its type.
@raise [TypeError] if a type error occurs during type-checking. *)
val typeof: debruijn_datatype_env -> debruijn_term -> debruijn_type
(* Similar to {!typeof}, but returns a [result] type instead of raising an exception. *)
val typeof_result:
debruijn_datatype_env -> debruijn_term -> (debruijn_type, type_error) result

View File

@ -1,6 +0,0 @@
let typeof env u =
try
FTypeChecker.typeof env u
with (FTypeChecker.TypeError e) as exn ->
Utils.emit_endline (FPrinter.print_type_error e);
raise exn

View File

@ -1,12 +0,0 @@
open F
(* A type-checker for System F. *)
(* This wrapper combines the System F type-checker with its type error
printer. If a type error occurs, a type error message is printed to
the standard output -- and the FTypeChecker.TypeError exception is
raised. *)
(* [typeof env t] type-checks the closed term [t] in datatype
environment [env] and returns its type. *)
val typeof: debruijn_datatype_env -> debruijn_term -> debruijn_type

View File

@ -59,8 +59,14 @@ let () =
(* Type-check. This is sanity check; we do not expect a type error. *)
printf "Type-checking...\n%!";
let repetitions = 1 in
let time, _ty = Measure.time ~repetitions
(fun () -> FTypeCheckerWrapper.typeof env v) in
let time, () =
Measure.time ~repetitions @@ fun () ->
match FTypeChecker.typeof_result env v with
| Error e ->
Utils.emit_endline (FPrinter.print_type_error e);
failwith "Sanity check failed."
| Ok _v -> ()
in
Printf.printf "Type-checking: %.3f seconds.\n%!" time;
(* Start the benchmark. Measure how long it takes to perform type inference

View File

@ -11,5 +11,8 @@ let test (env : F.nominal_datatype_env) (t : F.nominal_term) =
let t : F.debruijn_term =
F.Term.translate t in
print_string "Type-checking the System F term...\n";
let _ty : F.debruijn_type = FTypeCheckerWrapper.typeof env t in
()
match FTypeChecker.typeof_result env t with
| Error e ->
Utils.emit_endline (FPrinter.print_type_error e);
failwith "Type-checking error."
| Ok _v -> ()