Correct cli typecheck behavior

This commit is contained in:
Denis Merigoux 2023-01-05 18:56:19 +01:00
parent 124491410d
commit 9d619a26ba
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3

View File

@ -202,8 +202,21 @@ let driver source_file (options : Cli.options) : int =
end
else prgm
in
(* Cli.debug_print (Format.asprintf "Typechecking results :@\n%a"
(Print.typ prgm.decl_ctx) typ); *)
match backend with
| `Typecheck ->
Cli.debug_print "Typechecking again...";
let _ =
try Shared_ast.Typing.program prgm
with Errors.StructuredError (msg, details) ->
let msg =
"Typing error occured during re-typing on the 'default \
calculus'. This is a bug in the Catala compiler.\n"
^ msg
in
raise (Errors.StructuredError (msg, details))
in
(* That's it! *)
Cli.result_print "Typechecking successful!"
| `Dcalc ->
@ -229,7 +242,7 @@ let driver source_file (options : Cli.options) : int =
Shared_ast.Expr.unbox (Shared_ast.Program.to_expr prgm scope_uid)
in
Format.fprintf fmt "%a\n"
(Shared_ast.Expr.format prgm.decl_ctx)
(Shared_ast.Expr.format ~debug:options.debug prgm.decl_ctx)
prgrm_dcalc_expr
| (`Interpret | `OCaml | `Python | `Scalc | `Lcalc | `Proof | `Plugin _)
as backend -> (
@ -244,8 +257,6 @@ let driver source_file (options : Cli.options) : int =
in
raise (Errors.StructuredError (msg, details))
in
(* Cli.debug_print (Format.asprintf "Typechecking results :@\n%a"
(Print.typ prgm.decl_ctx) typ); *)
match backend with
| `Proof ->
let vcs =