CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-08 07:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Just typechecking for compiler

Browse Source
This commit is contained in:
Denis Merigoux 2022-01-31 15:28:19 +01:00
parent effc2b24e4
commit edeba14692
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
4 changed files with 11 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
build_system/clerk.ml
View File

@ -97,6 +97,7 @@ let catala_backend_to_string (backend : Cli.backend_option) : string =
| Cli.Proof -> "Proof"
| Cli.Html -> "Html"
| Cli.Python -> "Python"
| Cli.Typecheck -> "Typecheck"
type expected_output_descr = {
base_filename : string;
@ -124,6 +125,7 @@ let filename_to_expected_output_descr (output_dir : string) (filename : string)
| ".html" -> Some Cli.Html
| ".py" -> Some Cli.Python
| ".proof" -> Some Cli.Proof
| ".typecheck" -> Some Cli.Typecheck
| _ -> None
in
match backend with
@ -187,7 +189,7 @@ let test_file (tested_file : string) (catala_exe : string) (catala_opts : string
| _ -> [])
@
match expected_output.backend with
| Cli.Interpret | Cli.Proof ->
| Cli.Interpret | Cli.Proof | Cli.Typecheck ->
if reset_test_outputs then
[
">";

5
compiler/driver.ml
View File

@ -71,6 +71,7 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
else if backend = "scopelang" then Cli.Scopelang
else if backend = "python" then Cli.Python
else if backend = "proof" then Cli.Proof
else if backend = "typecheck" then Cli.Typecheck
else
Errors.raise_error
(Printf.sprintf "The selected backend (%s) is not supported by Catala" backend)
@ -216,6 +217,10 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
(* Cli.debug_print (Format.asprintf "Typechecking results :@\n%a" (Dcalc.Print.format_typ
prgm.decl_ctx) typ); *)
match backend with
| Cli.Typecheck ->
(* That's it! *)
Cli.result_print "Typechecking successful!";
0
| Cli.Proof ->
let vcs = Verification.Conditions.generate_verification_conditions prgm in
Verification.Solver.solve_vc prgm prgm.decl_ctx vcs;

2
compiler/utils/cli.ml
View File

@ -78,6 +78,7 @@ type backend_option =
| Makefile
| Html
| Interpret
| Typecheck
| OCaml
| Python
| Dcalc
@ -143,6 +144,7 @@ let info =
( "$(b,Intepret)",
"Runs the interpreter on the Catala program, executing the scope specified by the \
$(b,-s) option assuming no additional external inputs." );
`I ("$(b,Typecheck)", "Parses and typechecks a Catala program, without interpreting it.");
`I
( "$(b,Proof)",
"Generates and proves verification conditions about the well-behaved execution of the \

1
compiler/utils/cli.mli
View File

@ -57,6 +57,7 @@ type backend_option =
| Makefile
| Html
| Interpret
| Typecheck
| OCaml
| Python
| Dcalc