CLI: replace interpret_lcalc by interpret --lcalc

This will make it easier when running tests to just toggle the different flags
This commit is contained in:
Louis Gesbert 2024-02-22 17:02:00 +01:00
parent 97ae62384e
commit 4a049080a4
3 changed files with 41 additions and 35 deletions

View File

@ -454,6 +454,14 @@ module Flags = struct
& pos_right 0 file []
& Arg.info [] ~docv:"FILE" ~docs:Manpage.s_arguments
~doc:"Additional input files."
let lcalc =
value
& flag
& info ["lcalc"]
~doc:
"Compile all the way to lcalc before interpreting (the default is to \
interpret at dcalc stage). For debugging purposes."
end
(* Retrieve current version from dune *)

View File

@ -135,7 +135,12 @@ module Flags : sig
val no_struct_literals : bool Term.t
val include_dirs : raw_file list Term.t
val disable_counterexamples : bool Term.t
val extra_files : file list Term.t
(** for the 'latex' command *)
val lcalc : bool Term.t
(** for the 'interpret' command *)
end
(** {2 Command-line application} *)

View File

@ -707,26 +707,6 @@ module Commands = struct
print_interpretation_results options Interpreter.interpret_program_dcalc prg
(get_scope_uid prg.decl_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:
"Runs the interpreter on the Catala program, executing the scope \
specified by the $(b,-s) option assuming no additional external \
inputs.")
Term.(
const f
$ Cli.Flags.no_typing
$ Cli.Flags.Global.options
$ Cli.Flags.include_dirs
$ Cli.Flags.optimize
$ Cli.Flags.check_invariants
$ Cli.Flags.ex_scope)
let lcalc
typed
options
@ -780,13 +760,13 @@ module Commands = struct
let interpret_lcalc
typed
avoid_exceptions
closure_conversion
monomorphize_types
options
includes
optimize
check_invariants
avoid_exceptions
closure_conversion
monomorphize_types
ex_scope =
let prg, _ =
Passes.lcalc options ~includes ~optimize ~check_invariants
@ -796,27 +776,41 @@ module Commands = struct
print_interpretation_results options Interpreter.interpret_program_lcalc prg
(get_scope_uid prg.decl_ctx ex_scope)
let interpret_lcalc_cmd =
let f no_typing =
if no_typing then interpret_lcalc Expr.untyped
else interpret_lcalc Expr.typed
let interpret_cmd =
let f lcalc avoid_exceptions closure_conversion monomorphize_types no_typing
=
if not lcalc then
if avoid_exceptions || closure_conversion || monomorphize_types then
Message.raise_error
"The flags @{<bold>--avoid-exceptions@}, \
@{<bold>--closure-conversion@} and @{<bold>--monomorphize-types@} \
only make sense with the @{<bold>--lcalc@} option"
else if no_typing then interpret_dcalc Expr.untyped
else interpret_dcalc Expr.typed
else if no_typing then
interpret_lcalc Expr.untyped avoid_exceptions closure_conversion
monomorphize_types
else
interpret_lcalc Expr.typed avoid_exceptions closure_conversion
monomorphize_types
in
Cmd.v
(Cmd.info "interpret_lcalc"
(Cmd.info "interpret"
~doc:
"Runs the interpreter on the lcalc pass on the Catala program, \
executing the scope specified by the $(b,-s) option assuming no \
additional external inputs.")
"Runs the interpreter on the Catala program, executing the scope \
specified by the $(b,-s) option assuming no additional external \
inputs.")
Term.(
const f
$ Cli.Flags.lcalc
$ Cli.Flags.avoid_exceptions
$ Cli.Flags.closure_conversion
$ Cli.Flags.monomorphize_types
$ Cli.Flags.no_typing
$ Cli.Flags.Global.options
$ Cli.Flags.include_dirs
$ Cli.Flags.optimize
$ Cli.Flags.check_invariants
$ Cli.Flags.avoid_exceptions
$ Cli.Flags.closure_conversion
$ Cli.Flags.monomorphize_types
$ Cli.Flags.ex_scope)
let ocaml
@ -1017,7 +1011,6 @@ module Commands = struct
let commands =
[
interpret_cmd;
interpret_lcalc_cmd;
typecheck_cmd;
proof_cmd;
ocaml_cmd;