Add a --no-typing option

it is useful e.g. to be able to print intermediate ASTs when they don't type, to
debug the typing errors. This is better than commenting the typing line each
time.

Note that the option is not available on all targets (esp. not for ocaml and
python outputs ; it's allowed on the interpreters for debugging purposes but I'm
not sure if that's a good idea)
This commit is contained in:
Louis Gesbert 2023-11-02 14:36:55 +01:00
parent 9425753eca
commit b98bad8c33
6 changed files with 100 additions and 41 deletions

View File

@ -346,6 +346,10 @@ module Flags = struct
& flag
& info ["check_invariants"] ~doc:"Check structural invariants on the AST."
let no_typing =
value & flag & info ["no-typing"] ~doc:
"Don't check the consistency of types"
let wrap_weaved_output =
value
& flag

View File

@ -113,6 +113,7 @@ module Flags : sig
(** Parsers for all flags and options that commands can use *)
val check_invariants : bool Term.t
val no_typing : bool Term.t
val wrap_weaved_output : bool Term.t
val print_only_law : bool Term.t
val ex_scope : string Term.t

View File

@ -141,20 +141,32 @@ module Passes = struct
in
prg, ctx, exceptions_graphs
let dcalc options ~includes ~optimize ~check_invariants :
typed Dcalc.Ast.program
* Desugared.Name_resolution.context
* Scopelang.Dependency.TVertex.t list =
let dcalc:
type ty.
Cli.options -> includes:Cli.raw_file list -> optimize:bool -> check_invariants:bool ->
typed: ty mark ->
ty Dcalc.Ast.program
* Desugared.Name_resolution.context
* Scopelang.Dependency.TVertex.t list =
fun options ~includes ~optimize ~check_invariants ~typed ->
let prg, ctx, _ = scopelang options ~includes in
debug_pass_name "dcalc";
let type_ordering =
Scopelang.Dependency.check_type_cycles prg.program_ctx.ctx_structs
prg.program_ctx.ctx_enums
in
Message.emit_debug "Typechecking...";
let prg = Scopelang.Ast.type_program prg in
let (prg: ty Scopelang.Ast.program) =
match typed with
| Typed _ ->
Message.emit_debug "Typechecking...";
Scopelang.Ast.type_program prg
| Untyped _ -> prg
| Custom _ -> invalid_arg "Driver.Passes.dcalc"
in
Message.emit_debug "Translating to default calculus...";
let prg = Dcalc.From_scopelang.translate_program prg in
let prg =
Dcalc.From_scopelang.translate_program prg
in
let prg =
if optimize then begin
Message.emit_debug "Optimizing default calculus...";
@ -162,47 +174,64 @@ module Passes = struct
end
else prg
in
Message.emit_debug "Typechecking again...";
let prg =
try Typing.program ~leave_unresolved:false prg
with Message.CompilerError error_content ->
let bt = Printexc.get_raw_backtrace () in
Printexc.raise_with_backtrace
(Message.CompilerError
(Message.Content.to_internal_error error_content))
bt
let (prg: ty Dcalc.Ast.program) =
match typed with
| Typed _ ->
Message.emit_debug "Typechecking again...";
(try Typing.program ~leave_unresolved:false prg
with Message.CompilerError error_content ->
let bt = Printexc.get_raw_backtrace () in
Printexc.raise_with_backtrace
(Message.CompilerError
(Message.Content.to_internal_error error_content))
bt)
| Untyped _ -> prg
| Custom _ -> assert false
in
if check_invariants then (
Message.emit_debug "Checking invariants...";
let result = Dcalc.Invariants.check_all_invariants prg in
if not result then
raise (Message.raise_internal_error "Some Dcalc invariants are invalid"));
match typed with
| Typed _ ->
let result = Dcalc.Invariants.check_all_invariants prg in
if not result then
raise (Message.raise_internal_error "Some Dcalc invariants are invalid")
| _ ->
Message.raise_error "--check_invariants cannot be used with --no-typing");
prg, ctx, type_ordering
let lcalc
let lcalc (type ty)
options
~includes
~optimize
~check_invariants
~(typed: ty mark)
~avoid_exceptions
~closure_conversion :
untyped Lcalc.Ast.program
* Desugared.Name_resolution.context
* Scopelang.Dependency.TVertex.t list =
let prg, ctx, type_ordering =
dcalc options ~includes ~optimize ~check_invariants
dcalc options ~includes ~optimize ~check_invariants ~typed
in
debug_pass_name "lcalc";
let avoid_exceptions = avoid_exceptions || closure_conversion in
let optimize = optimize || closure_conversion in
(* --closure_conversion implies --avoid_exceptions and --optimize *)
let prg =
if avoid_exceptions then (
if options.trace then
Message.raise_error
"Option --avoid_exceptions is not compatible with option --trace";
Lcalc.Compile_without_exceptions.translate_program prg)
else Program.untype (Lcalc.Compile_with_exceptions.translate_program prg)
match avoid_exceptions, options.trace, typed with
| true, true, _ ->
Message.raise_error
"Option --avoid_exceptions is not compatible with option --trace"
| true, _, Untyped _ ->
Message.raise_error
"Option --avoid_exceptions is not compatible with option --no-typing"
| true, _, Typed _ ->
Lcalc.Compile_without_exceptions.translate_program prg
| false, _, Typed _ ->
Program.untype (Lcalc.Compile_with_exceptions.translate_program prg)
| false, _, Untyped _ ->
Lcalc.Compile_with_exceptions.translate_program prg
| _, _, Custom _ -> invalid_arg "Driver.Passes.lcalc"
in
let prg =
if optimize then begin
@ -240,7 +269,7 @@ module Passes = struct
* Desugared.Name_resolution.context
* Scopelang.Dependency.TVertex.t list =
let prg, ctx, type_ordering =
lcalc options ~includes ~optimize ~check_invariants ~avoid_exceptions
lcalc options ~includes ~optimize ~check_invariants ~typed:Expr.typed ~avoid_exceptions
~closure_conversion
in
debug_pass_name "scalc";
@ -507,9 +536,10 @@ module Commands = struct
~doc:"Parses and typechecks a Catala program, without interpreting it.")
Term.(const typecheck $ Cli.Flags.Global.options $ Cli.Flags.include_dirs)
let dcalc options includes output optimize ex_scope_opt check_invariants =
let dcalc typed options includes output optimize ex_scope_opt check_invariants
=
let prg, ctx, _ =
Passes.dcalc options ~includes ~optimize ~check_invariants
Passes.dcalc options ~includes ~optimize ~check_invariants ~typed
in
let _output_file, with_output = get_output_format options output in
with_output
@ -537,6 +567,9 @@ module Commands = struct
prg_dcalc_expr
let dcalc_cmd =
let f no_typing =
if no_typing then dcalc Expr.untyped else dcalc Expr.typed
in
Cmd.v
(Cmd.info "dcalc"
~doc:
@ -544,7 +577,8 @@ module Commands = struct
representation of the Catala program. Use the $(b,-s) option to \
restrict the output to a particular scope.")
Term.(
const dcalc
const f
$ Cli.Flags.no_typing
$ Cli.Flags.Global.options
$ Cli.Flags.include_dirs
$ Cli.Flags.output
@ -560,7 +594,7 @@ module Commands = struct
check_invariants
disable_counterexamples =
let prg, ctx, _ =
Passes.dcalc options ~includes ~optimize ~check_invariants
Passes.dcalc options ~includes ~optimize ~check_invariants ~typed:Expr.typed
in
Verification.Globals.setup ~optimize ~disable_counterexamples;
let vcs =
@ -608,15 +642,16 @@ module Commands = struct
result)
results
let interpret_dcalc options includes optimize check_invariants ex_scope =
let interpret_dcalc typed options includes optimize check_invariants ex_scope =
let prg, ctx, _ =
Passes.dcalc options ~includes ~optimize ~check_invariants
Passes.dcalc options ~includes ~optimize ~check_invariants ~typed
in
Interpreter.load_runtime_modules prg;
print_interpretation_results options Interpreter.interpret_program_dcalc prg
(get_scope_uid ctx ex_scope)
let interpret_cmd =
let f no_typing = if no_typing then interpret_dcalc Expr.untyped else interpret_dcalc Expr.typed in
Cmd.v
(Cmd.info "interpret"
~doc:
@ -624,7 +659,8 @@ module Commands = struct
specified by the $(b,-s) option assuming no additional external \
inputs.")
Term.(
const interpret_dcalc
const f
$ Cli.Flags.no_typing
$ Cli.Flags.Global.options
$ Cli.Flags.include_dirs
$ Cli.Flags.optimize
@ -632,6 +668,7 @@ module Commands = struct
$ Cli.Flags.ex_scope)
let lcalc
typed
options
includes
output
@ -642,7 +679,7 @@ module Commands = struct
ex_scope_opt =
let prg, ctx, _ =
Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion
~avoid_exceptions ~closure_conversion ~typed
in
let _output_file, with_output = get_output_format options output in
with_output
@ -658,6 +695,9 @@ module Commands = struct
Format.pp_print_newline fmt ()
let lcalc_cmd =
let f no_typing =
if no_typing then lcalc Expr.untyped else lcalc Expr.typed
in
Cmd.v
(Cmd.info "lcalc"
~doc:
@ -665,7 +705,8 @@ module Commands = struct
representation of the Catala program. Use the $(b,-s) option to \
restrict the output to a particular scope.")
Term.(
const lcalc
const f
$ Cli.Flags.no_typing
$ Cli.Flags.Global.options
$ Cli.Flags.include_dirs
$ Cli.Flags.output
@ -676,6 +717,7 @@ module Commands = struct
$ Cli.Flags.ex_scope_opt)
let interpret_lcalc
typed
options
includes
optimize
@ -685,13 +727,16 @@ module Commands = struct
ex_scope =
let prg, ctx, _ =
Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion
~avoid_exceptions ~closure_conversion ~typed
in
Interpreter.load_runtime_modules prg;
print_interpretation_results options Interpreter.interpret_program_lcalc prg
(get_scope_uid ctx ex_scope)
let interpret_lcalc_cmd =
let f no_typing =
if no_typing then interpret_lcalc Expr.untyped else interpret_lcalc Expr.typed
in
Cmd.v
(Cmd.info "interpret_lcalc"
~doc:
@ -699,7 +744,8 @@ module Commands = struct
executing the scope specified by the $(b,-s) option assuming no \
additional external inputs.")
Term.(
const interpret_lcalc
const f
$ Cli.Flags.no_typing
$ Cli.Flags.Global.options
$ Cli.Flags.include_dirs
$ Cli.Flags.optimize
@ -718,7 +764,7 @@ module Commands = struct
closure_conversion =
let prg, _, type_ordering =
Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion
~avoid_exceptions ~closure_conversion ~typed:Expr.typed
in
let output_file, with_output =
get_output_format options ~ext:".ml" output

View File

@ -44,7 +44,8 @@ module Passes : sig
includes:Cli.raw_file list ->
optimize:bool ->
check_invariants:bool ->
Shared_ast.typed Dcalc.Ast.program
typed:'m Shared_ast.mark ->
'm Dcalc.Ast.program
* Desugared.Name_resolution.context
* Scopelang.Dependency.TVertex.t list
@ -53,6 +54,7 @@ module Passes : sig
includes:Cli.raw_file list ->
optimize:bool ->
check_invariants:bool ->
typed:'m Shared_ast.mark ->
avoid_exceptions:bool ->
closure_conversion:bool ->
Shared_ast.untyped Lcalc.Ast.program

View File

@ -248,6 +248,9 @@ let maybe_ty (type m) ?(typ = TAny) (m : m mark) : typ =
| Untyped { pos } | Custom { pos; _ } -> Mark.add pos typ
| Typed { ty; _ } -> ty
let untyped = Untyped { pos = Pos.no_pos }
let typed = Typed { pos = Pos.no_pos; ty = TLit TUnit, Pos.no_pos }
(* - Predefined types (option) - *)
let option_enum = EnumName.fresh [] ("eoption", Pos.no_pos)

View File

@ -193,6 +193,9 @@ val maybe_ty : ?typ:naked_typ -> 'm mark -> typ
(** Returns the corresponding type on a typed expr, or [typ] (defaulting to
[TAny]) at the current position on an untyped one *)
val untyped : untyped mark (** Type witness for untyped marks *)
val typed : typed mark (** Type witness for untyped marks *)
(** {2 Predefined types} *)
val option_enum : EnumName.t