CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-07 10:35:56 +03:00
Code Issues Projects Releases Wiki Activity

Remove the with-exceptions backend

Browse Source 
*Disclaimer*: This is intended for discussion

My impression is that the with-exceptions backend is to be superseded by the
without-exception backend, which is more general and more efficient. Therefore,
seeing the added complexity of maintaining the two in parallel, I see no good
reason to keep the with-exceptions version now that the equivalence of their
semantics have been proved.

It will also be nice to reduce divergences between the different backends ; and
this should make further simplifications possible (e.g. some thunkings may no
longer be needed)

Of course I am ready to hear arguments in favor of keeping it, be it in the mid-
or long-term.

This patch removes the `--avoid-exceptions` flag, making it the only option, and
the corresponding `with_exceptions` variant of the dcalc->lcalc translation. It
doesn't do further simplifications.
This commit is contained in:
Louis Gesbert 2024-06-24 12:16:19 +02:00
parent d073103578
commit 583e80993a
27 changed files with 175 additions and 433 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile
View File

@ -217,7 +217,7 @@ tests: test
TEST_FLAGS_LIST = ""\
-O \
--lcalc \
--lcalc,--avoid-exceptions,-O
--lcalc,--closure-conversion,-O
# Does not include running dune (to avoid duplication when run among bigger rules)
testsuite-base: .FORCE

12
build_system/clerk_driver.ml
View File

@ -75,8 +75,8 @@ module Cli = struct
tests. Comma-separated list. A subset may also be applied to the \
compilation of modules, as needed.\n\
WARNING: flag shortcuts are not allowed here (i.e. don't use \
non-ambiguous prefixes such as $(b,--avoid-ex) for \
$(b,--avoid-exceptions))\n\
non-ambiguous prefixes such as $(b,--closure) for \
$(b,--closure-conversion))\n\
NOTE: if this is set, all inline tests that are $(i,not) \
$(b,catala test-scope) are skipped to avoid redundant testing.")
@ -481,17 +481,13 @@ let base_bindings catala_exe catala_flags build_dir include_dirs test_flags =
let catala_flags_ocaml =
List.filter
(function
| "--avoid-exceptions" | "-O" | "--optimize" | "--closure-conversion" ->
true
| _ -> false)
| "-O" | "--optimize" | "--closure-conversion" -> true | _ -> false)
test_flags
in
let catala_flags_python =
List.filter
(function
| "--avoid-exceptions" | "-O" | "--optimize" | "--closure-conversion" ->
true
| _ -> false)
| "-O" | "--optimize" | "--closure-conversion" -> true | _ -> false)
test_flags
in
let ocaml_flags = Lazy.force Poll.ocaml_include_flags in

11
compiler/catala_utils/cli.ml
View File

@ -334,13 +334,6 @@ module Flags = struct
~env:(Cmd.Env.info "CATALA_OPTIMIZE")
~doc:"Run compiler optimizations."
let avoid_exceptions =
value
& flag
& info ["avoid-exceptions"]
~env:(Cmd.Env.info "CATALA_AVOID_EXCEPTIONS")
~doc:"Compiles the default calculus without exceptions."
let keep_special_ops =
value
& flag
@ -381,9 +374,7 @@ module Flags = struct
value
& flag
& info ["closure-conversion"]
~doc:
"Performs closure conversion on the lambda calculus. Implies \
$(b,--avoid-exceptions)."
~doc:"Performs closure conversion on the lambda calculus."
let disable_counterexamples =
value

1
compiler/catala_utils/cli.mli
View File

@ -55,7 +55,6 @@ module Flags : sig
val ex_variable : string Term.t
val output : raw_file option Term.t
val optimize : bool Term.t
val avoid_exceptions : bool Term.t
val closure_conversion : bool Term.t
val keep_special_ops : bool Term.t
val monomorphize_types : bool Term.t

12
compiler/catala_utils/hash.ml
View File

@ -36,22 +36,16 @@ module Flags : sig
type nonrec t = private t
val pass :
(t -> 'a) ->
avoid_exceptions:bool ->
closure_conversion:bool ->
monomorphize_types:bool ->
'a
(t -> 'a) -> closure_conversion:bool -> monomorphize_types:bool -> 'a
val of_t : int -> t
end = struct
type nonrec t = t
let pass k ~avoid_exceptions ~closure_conversion ~monomorphize_types =
let avoid_exceptions = avoid_exceptions || closure_conversion in
let pass k ~closure_conversion ~monomorphize_types =
(* Should not affect the call convention or actual interfaces: include,
optimize, check_invariants, typed *)
!(avoid_exceptions : bool)
% !(closure_conversion : bool)
!(closure_conversion : bool)
% !(monomorphize_types : bool)
% (* The following may not affect the call convention, but we want it set in
an homogeneous way *)

7
compiler/catala_utils/hash.mli
View File

@ -58,12 +58,7 @@ val map :
first argument is expected to be a [Foo.Map.fold] function. The result is
independent of the ordering of the map. *)
val finalise :
t ->
avoid_exceptions:bool ->
closure_conversion:bool ->
monomorphize_types:bool ->
full
val finalise : t -> closure_conversion:bool -> monomorphize_types:bool -> full
(** Turns a raw interface hash into a full hash, ready for printing *)
val to_string : full -> string

88
compiler/driver.ml
View File

@ -227,7 +227,6 @@ module Passes = struct
~optimize
~check_invariants
~(typed : ty mark)
~avoid_exceptions
~closure_conversion
~monomorphize_types :
typed Lcalc.Ast.program * Scopelang.Dependency.TVertex.t list =
@ -235,23 +234,11 @@ module Passes = struct
dcalc options ~includes ~optimize ~check_invariants ~typed
in
debug_pass_name "lcalc";
let avoid_exceptions = avoid_exceptions || closure_conversion in
(* --closure-conversion implies --avoid-exceptions *)
let prg =
if avoid_exceptions && options.trace then
Message.warning
"It is discouraged to use option @{<yellow>--avoid-exceptions@} if \
you@ also@ need@ @{<yellow>--trace@},@ the@ resulting@ trace@ may@ \
be@ unreliable@ at@ the@ moment.";
match avoid_exceptions, typed with
| true, Untyped _ ->
Lcalc.From_dcalc.translate_program_without_exceptions prg
| true, Typed _ ->
Lcalc.From_dcalc.translate_program_without_exceptions prg
| false, Typed _ -> Lcalc.From_dcalc.translate_program_with_exceptions prg
| false, Untyped _ ->
Lcalc.From_dcalc.translate_program_with_exceptions prg
| _, Custom _ -> invalid_arg "Driver.Passes.lcalc"
match typed with
| Untyped _ -> Lcalc.From_dcalc.translate_program prg
| Typed _ -> Lcalc.From_dcalc.translate_program prg
| Custom _ -> invalid_arg "Driver.Passes.lcalc"
in
let prg =
if optimize then begin
@ -295,7 +282,6 @@ module Passes = struct
~includes
~optimize
~check_invariants
~avoid_exceptions
~closure_conversion
~keep_special_ops
~dead_value_assignment
@ -304,7 +290,7 @@ module Passes = struct
Scalc.Ast.program * Scopelang.Dependency.TVertex.t list =
let prg, type_ordering =
lcalc options ~includes ~optimize ~check_invariants ~typed:Expr.typed
~avoid_exceptions ~closure_conversion ~monomorphize_types
~closure_conversion ~monomorphize_types
in
debug_pass_name "scalc";
( Scalc.From_lcalc.translate_program
@ -710,10 +696,7 @@ module Commands = struct
Passes.dcalc options ~includes ~optimize ~check_invariants ~typed
in
Interpreter.load_runtime_modules
~hashf:
Hash.(
finalise ~avoid_exceptions:false ~closure_conversion:false
~monomorphize_types:false)
~hashf:Hash.(finalise ~closure_conversion:false ~monomorphize_types:false)
prg;
print_interpretation_results options Interpreter.interpret_program_dcalc prg
(get_scopeopt_uid prg.decl_ctx ex_scope_opt)
@ -725,13 +708,12 @@ module Commands = struct
output
optimize
check_invariants
avoid_exceptions
closure_conversion
monomorphize_types
ex_scope_opt =
let prg, _ =
Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion ~typed ~monomorphize_types
~closure_conversion ~typed ~monomorphize_types
in
let _output_file, with_output = get_output_format options output in
with_output
@ -764,14 +746,12 @@ module Commands = struct
$ Cli.Flags.output
$ Cli.Flags.optimize
$ Cli.Flags.check_invariants
$ Cli.Flags.avoid_exceptions
$ Cli.Flags.closure_conversion
$ Cli.Flags.monomorphize_types
$ Cli.Flags.ex_scope_opt)
let interpret_lcalc
typed
avoid_exceptions
closure_conversion
monomorphize_types
options
@ -781,32 +761,27 @@ module Commands = struct
ex_scope_opt =
let prg, _ =
Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion ~monomorphize_types ~typed
~closure_conversion ~monomorphize_types ~typed
in
Interpreter.load_runtime_modules
~hashf:
(Hash.finalise ~avoid_exceptions ~closure_conversion ~monomorphize_types)
~hashf:(Hash.finalise ~closure_conversion ~monomorphize_types)
prg;
print_interpretation_results options Interpreter.interpret_program_lcalc prg
(get_scopeopt_uid prg.decl_ctx ex_scope_opt)
let interpret_cmd =
let f lcalc avoid_exceptions closure_conversion monomorphize_types no_typing
=
let f lcalc closure_conversion monomorphize_types no_typing =
if not lcalc then
if avoid_exceptions || closure_conversion || monomorphize_types then
if closure_conversion || monomorphize_types then
Message.error
"The flags @{<bold>--avoid-exceptions@}, \
@{<bold>--closure-conversion@} and @{<bold>--monomorphize-types@} \
only make sense with the @{<bold>--lcalc@} option"
"The flags @{<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
interpret_lcalc Expr.untyped closure_conversion monomorphize_types
else interpret_lcalc Expr.typed closure_conversion monomorphize_types
in
Cmd.v
(Cmd.info "interpret"
@ -817,7 +792,6 @@ module Commands = struct
Term.(
const f
$ Cli.Flags.lcalc
$ Cli.Flags.avoid_exceptions
$ Cli.Flags.closure_conversion
$ Cli.Flags.monomorphize_types
$ Cli.Flags.no_typing
@ -833,13 +807,11 @@ module Commands = struct
output
optimize
check_invariants
avoid_exceptions
closure_conversion
ex_scope_opt =
let prg, type_ordering =
Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~typed:Expr.typed ~closure_conversion
~monomorphize_types:false
~typed:Expr.typed ~closure_conversion ~monomorphize_types:false
in
let output_file, with_output =
get_output_format options ~ext:".ml" output
@ -850,10 +822,7 @@ module Commands = struct
Message.debug "Writing to %s..."
(Option.value ~default:"stdout" output_file);
let exec_scope = Option.map (get_scope_uid prg.decl_ctx) ex_scope_opt in
let hashf =
Hash.finalise ~avoid_exceptions ~closure_conversion
~monomorphize_types:false
in
let hashf = Hash.finalise ~closure_conversion ~monomorphize_types:false in
Lcalc.To_ocaml.format_program fmt prg ?exec_scope ~hashf type_ordering
let ocaml_cmd =
@ -867,7 +836,6 @@ module Commands = struct
$ Cli.Flags.output
$ Cli.Flags.optimize
$ Cli.Flags.check_invariants
$ Cli.Flags.avoid_exceptions
$ Cli.Flags.closure_conversion
$ Cli.Flags.ex_scope_opt)
@ -877,7 +845,6 @@ module Commands = struct
output
optimize
check_invariants
avoid_exceptions
closure_conversion
keep_special_ops
dead_value_assignment
@ -886,8 +853,8 @@ module Commands = struct
ex_scope_opt =
let prg, _ =
Passes.scalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion ~keep_special_ops
~dead_value_assignment ~no_struct_literals ~monomorphize_types
~closure_conversion ~keep_special_ops ~dead_value_assignment
~no_struct_literals ~monomorphize_types
in
let _output_file, with_output = get_output_format options output in
with_output
@ -919,7 +886,6 @@ module Commands = struct
$ Cli.Flags.output
$ Cli.Flags.optimize
$ Cli.Flags.check_invariants
$ Cli.Flags.avoid_exceptions
$ Cli.Flags.closure_conversion
$ Cli.Flags.keep_special_ops
$ Cli.Flags.dead_value_assignment
@ -933,13 +899,11 @@ module Commands = struct
output
optimize
check_invariants
avoid_exceptions
closure_conversion =
let prg, type_ordering =
Passes.scalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion ~keep_special_ops:false
~dead_value_assignment:true ~no_struct_literals:false
~monomorphize_types:false
~closure_conversion ~keep_special_ops:false ~dead_value_assignment:true
~no_struct_literals:false ~monomorphize_types:false
in
let output_file, with_output =
@ -962,15 +926,13 @@ module Commands = struct
$ Cli.Flags.output
$ Cli.Flags.optimize
$ Cli.Flags.check_invariants
$ Cli.Flags.avoid_exceptions
$ Cli.Flags.closure_conversion)
let r options includes output optimize check_invariants closure_conversion =
let prg, type_ordering =
Passes.scalc options ~includes ~optimize ~check_invariants
~avoid_exceptions:false ~closure_conversion ~keep_special_ops:false
~dead_value_assignment:false ~no_struct_literals:false
~monomorphize_types:false
~closure_conversion ~keep_special_ops:false ~dead_value_assignment:false
~no_struct_literals:false ~monomorphize_types:false
in
let output_file, with_output = get_output_format options ~ext:".r" output in
@ -994,7 +956,7 @@ module Commands = struct
let c options includes output optimize check_invariants =
let prg, type_ordering =
Passes.scalc options ~includes ~optimize ~check_invariants
~avoid_exceptions:true ~closure_conversion:true ~keep_special_ops:true
~closure_conversion:true ~keep_special_ops:true
~dead_value_assignment:false ~no_struct_literals:true
~monomorphize_types:true
in

2
compiler/driver.mli
View File

@ -51,7 +51,6 @@ module Passes : sig
optimize:bool ->
check_invariants:bool ->
typed:'m Shared_ast.mark ->
avoid_exceptions:bool ->
closure_conversion:bool ->
monomorphize_types:bool ->
Shared_ast.typed Lcalc.Ast.program * Scopelang.Dependency.TVertex.t list
@ -61,7 +60,6 @@ module Passes : sig
includes:Global.raw_file list ->
optimize:bool ->
check_invariants:bool ->
avoid_exceptions:bool ->
closure_conversion:bool ->
keep_special_ops:bool ->
dead_value_assignment:bool ->

9
compiler/lcalc/closure_conversion.ml
View File

@ -30,11 +30,10 @@ type 'm ctx = {
let new_var ?(pfx = "") name_context =
name_context.counter <- name_context.counter + 1;
Var.make (pfx ^ name_context.prefix ^ string_of_int name_context.counter)
(* TODO: Closures end up as a toplevel names. However for now we assume
toplevel names are unique, this is a temporary workaround to avoid
name wrangling in the backends. We need to have a better system for
name disambiguation when for instance printing to Dcalc/Lcalc/Scalc but
also OCaml, Python, etc. *)
(* TODO: Closures end up as a toplevel names. However for now we assume toplevel
names are unique, this is a temporary workaround to avoid name wrangling in
the backends. We need to have a better system for name disambiguation when
for instance printing to Dcalc/Lcalc/Scalc but also OCaml, Python, etc. *)
let new_context prefix = { prefix; counter = 0 }

95
compiler/lcalc/compile_with_exceptions.ml
View File

@ -1,95 +0,0 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
Denis Merigoux <denis.merigoux@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
License for the specific language governing permissions and limitations under
the License. *)
open Catala_utils
open Shared_ast
module D = Dcalc.Ast
module A = Ast
let rec translate_typ (tau : typ) : typ =
Mark.map
(function
| TDefault t -> Mark.remove (translate_typ t)
| TLit l -> TLit l
| TTuple ts -> TTuple (List.map translate_typ ts)
| TStruct s -> TStruct s
| TEnum en -> TEnum en
| TOption _ ->
Message.error ~internal:true
"The types option should not appear before the dcalc -> lcalc \
translation step."
| TClosureEnv ->
Message.error ~internal:true
"The types closure_env should not appear before the dcalc -> lcalc \
translation step."
| TAny -> TAny
| TArray ts -> TArray (translate_typ ts)
| TArrow (t1, t2) -> TArrow (List.map translate_typ t1, translate_typ t2))
tau
let translate_mark m = Expr.map_ty translate_typ m
let rec translate_default
(exceptions : 'm D.expr list)
(just : 'm D.expr)
(cons : 'm D.expr)
(mark_default : 'm mark) : 'm A.expr boxed =
let pos = Expr.mark_pos mark_default in
let exceptions =
List.map (fun except -> Expr.thunk_term (translate_expr except)) exceptions
in
Expr.eappop
~op:(Op.HandleDefault, Expr.pos cons)
~tys:
[
TArray (TArrow ([TLit TUnit, pos], (TAny, pos)), pos), pos;
TArrow ([TLit TUnit, pos], (TLit TBool, pos)), pos;
TArrow ([TLit TUnit, pos], (TAny, pos)), pos;
]
~args:
[
Expr.earray exceptions
(Expr.map_ty
(fun ty -> TArray (TArrow ([TLit TUnit, pos], ty), pos), pos)
mark_default);
Expr.thunk_term (translate_expr just);
Expr.thunk_term (translate_expr cons);
]
mark_default
and translate_expr (e : 'm D.expr) : 'm A.expr boxed =
match e with
| EEmpty, m -> Expr.eraiseempty (translate_mark m)
| EErrorOnEmpty arg, m ->
let m = translate_mark m in
Expr.ecatchempty (translate_expr arg) (Expr.efatalerror Runtime.NoValue m) m
| EDefault { excepts; just; cons }, m ->
translate_default excepts just cons (translate_mark m)
| EPureDefault e, _ -> translate_expr e
| EAppOp { op; args; tys }, m ->
Expr.eappop ~op:(Operator.translate op)
~args:(List.map translate_expr args)
~tys:(List.map translate_typ tys)
(translate_mark m)
| ( ( ELit _ | EArray _ | EVar _ | EAbs _ | EApp _ | EExternal _
| EIfThenElse _ | ETuple _ | ETupleAccess _ | EInj _ | EAssert _
| EFatalError _ | EStruct _ | EStructAccess _ | EMatch _ ),
_ ) as e ->
Expr.map ~f:translate_expr ~typ:translate_typ e
| _ -> .
let translate_program (prg : 'm D.program) : 'm A.program =
Program.map_exprs prg ~typ:translate_typ ~varf:Var.translate ~f:translate_expr

20
compiler/lcalc/compile_with_exceptions.mli
View File

@ -1,20 +0,0 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
Denis Merigoux <denis.merigoux@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
License for the specific language governing permissions and limitations under
the License. *)
(** Translation from the default calculus to the lambda calculus. This
translation uses exceptions to handle empty default terms. *)
val translate_program : 'm Dcalc.Ast.program -> 'm Ast.program

126
compiler/lcalc/compile_without_exceptions.ml
View File

@ -1,126 +0,0 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
Alain Delaët-Tixeuil <alain.delaet--tixeuil@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
License for the specific language governing permissions and limitations under
the License. *)
open Catala_utils
open Shared_ast
module D = Dcalc.Ast
module A = Ast
(** We make use of the strong invriants on the structure of programs:
Defaultable values can only appear in certin positions. This information is
given by the type structure of expressions. In particular this mean we don't
need to use the monadic bind while computing arithmetic opertions or
function calls. The resulting function is not more difficult than what we
had when translating without exceptions.
The typing translation is to simply trnsform default type into option types. *)
let rec translate_typ (tau : typ) : typ =
Mark.copy tau
begin
match Mark.remove tau with
| TDefault t -> TOption (translate_typ t)
| TLit l -> TLit l
| TTuple ts -> TTuple (List.map translate_typ ts)
| TStruct s -> TStruct s
| TEnum en -> TEnum en
| TOption _ ->
Message.error ~internal:true
"The types option should not appear before the dcalc -> lcalc \
translation step."
| TClosureEnv ->
Message.error ~internal:true
"The types closure_env should not appear before the dcalc -> lcalc \
translation step."
| TAny -> TAny
| TArray ts -> TArray (translate_typ ts)
| TArrow (t1, t2) -> TArrow (List.map translate_typ t1, translate_typ t2)
end
let translate_mark m = Expr.map_ty translate_typ m
let rec translate_default
(exceptions : 'm D.expr list)
(just : 'm D.expr)
(cons : 'm D.expr)
(mark_default : 'm mark) : 'm A.expr boxed =
(* Since the program is well typed, all exceptions have as type [option 't] *)
let pos = Expr.mark_pos mark_default in
let exceptions = List.map translate_expr exceptions in
let exceptions_and_cons_ty = Expr.maybe_ty mark_default in
Expr.eappop
~op:(Op.HandleDefaultOpt, Expr.pos cons)
~tys:
[
TArray exceptions_and_cons_ty, pos;
TArrow ([TLit TUnit, pos], (TLit TBool, pos)), pos;
TArrow ([TLit TUnit, pos], exceptions_and_cons_ty), pos;
]
~args:
[
Expr.earray exceptions
(Expr.map_ty (fun ty -> TArray ty, pos) mark_default);
(* In call-by-value programming languages, as lcalc, arguments are
evalulated before calling the function. Since we don't want to
execute the justification and conclusion while before checking every
exceptions, we need to thunk them. *)
Expr.thunk_term (translate_expr just);
Expr.thunk_term (translate_expr cons);
]
mark_default
and translate_expr (e : 'm D.expr) : 'm A.expr boxed =
match e with
| EEmpty, m ->
let m = translate_mark m in
let pos = Expr.mark_pos m in
Expr.einj
~e:(Expr.elit LUnit (Expr.with_ty m (TLit TUnit, pos)))
~cons:Expr.none_constr ~name:Expr.option_enum m
| EErrorOnEmpty arg, m ->
let m = translate_mark m in
let pos = Expr.mark_pos m in
let cases =
EnumConstructor.Map.of_list
[
( Expr.none_constr,
let x = Var.make "_" in
Expr.make_abs [| x |] (Expr.efatalerror NoValue m) [TAny, pos] pos
);
(* | None x -> raise NoValueProvided *)
Expr.some_constr, Expr.fun_id ~var_name:"arg" m (* | Some x -> x *);
]
in
Expr.ematch ~e:(translate_expr arg) ~name:Expr.option_enum ~cases m
| EDefault { excepts; just; cons }, m ->
translate_default excepts just cons (translate_mark m)
| EPureDefault e, m ->
Expr.einj ~e:(translate_expr e) ~cons:Expr.some_constr
~name:Expr.option_enum (translate_mark m)
| EAppOp { op; tys; args }, m ->
Expr.eappop ~op:(Operator.translate op)
~tys:(List.map translate_typ tys)
~args:(List.map translate_expr args)
(translate_mark m)
| ( ( ELit _ | EArray _ | EVar _ | EApp _ | EAbs _ | EExternal _
| EIfThenElse _ | ETuple _ | ETupleAccess _ | EInj _ | EAssert _
| EFatalError _ | EStruct _ | EStructAccess _ | EMatch _ ),
_ ) as e ->
Expr.map ~f:translate_expr ~typ:translate_typ e
| _ -> .
let translate_program (prg : 'm D.program) : 'm A.program =
Program.map_exprs prg ~typ:translate_typ ~varf:Var.translate ~f:translate_expr

22
compiler/lcalc/compile_without_exceptions.mli
View File

@ -1,22 +0,0 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2020-2022 Inria,
contributor: Alain Delaët-Tixeuil <alain.delaet--tixeuil@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
License for the specific language governing permissions and limitations under
the License. *)
(** Translation from the default calculus to the lambda calculus. This
translation uses an option monad to handle empty defaults terms. This
transformation is one piece to permit to compile toward legacy languages
that does not contains exceptions. *)
val translate_program : 'm Dcalc.Ast.program -> 'm Ast.program

118
compiler/lcalc/from_dcalc.ml
View File

@ -1,6 +1,6 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
Denis Merigoux <denis.merigoux@inria.fr>
Alain Delaët-Tixeuil <alain.delaet--tixeuil@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
@ -14,7 +14,113 @@
License for the specific language governing permissions and limitations under
the License. *)
open Catala_utils
open Shared_ast
module D = Dcalc.Ast
module A = Ast
(** We make use of the strong invriants on the structure of programs:
Defaultable values can only appear in certin positions. This information is
given by the type structure of expressions. In particular this mean we don't
need to use the monadic bind while computing arithmetic opertions or
function calls. The resulting function is not more difficult than what we
had when translating without exceptions.
The typing translation is to simply trnsform default type into option types. *)
let rec translate_typ (tau : typ) : typ =
Mark.copy tau
begin
match Mark.remove tau with
| TDefault t -> TOption (translate_typ t)
| TLit l -> TLit l
| TTuple ts -> TTuple (List.map translate_typ ts)
| TStruct s -> TStruct s
| TEnum en -> TEnum en
| TOption _ ->
Message.error ~internal:true
"The types option should not appear before the dcalc -> lcalc \
translation step."
| TClosureEnv ->
Message.error ~internal:true
"The types closure_env should not appear before the dcalc -> lcalc \
translation step."
| TAny -> TAny
| TArray ts -> TArray (translate_typ ts)
| TArrow (t1, t2) -> TArrow (List.map translate_typ t1, translate_typ t2)
end
let translate_mark m = Expr.map_ty translate_typ m
let rec translate_default
(exceptions : 'm D.expr list)
(just : 'm D.expr)
(cons : 'm D.expr)
(mark_default : 'm mark) : 'm A.expr boxed =
(* Since the program is well typed, all exceptions have as type [option 't] *)
let pos = Expr.mark_pos mark_default in
let exceptions = List.map translate_expr exceptions in
let exceptions_and_cons_ty = Expr.maybe_ty mark_default in
Expr.eappop
~op:(Op.HandleDefaultOpt, Expr.pos cons)
~tys:
[
TArray exceptions_and_cons_ty, pos;
TArrow ([TLit TUnit, pos], (TLit TBool, pos)), pos;
TArrow ([TLit TUnit, pos], exceptions_and_cons_ty), pos;
]
~args:
[
Expr.earray exceptions
(Expr.map_ty (fun ty -> TArray ty, pos) mark_default);
(* In call-by-value programming languages, as lcalc, arguments are
evalulated before calling the function. Since we don't want to
execute the justification and conclusion while before checking every
exceptions, we need to thunk them. *)
Expr.thunk_term (translate_expr just);
Expr.thunk_term (translate_expr cons);
]
mark_default
and translate_expr (e : 'm D.expr) : 'm A.expr boxed =
match e with
| EEmpty, m ->
let m = translate_mark m in
let pos = Expr.mark_pos m in
Expr.einj
~e:(Expr.elit LUnit (Expr.with_ty m (TLit TUnit, pos)))
~cons:Expr.none_constr ~name:Expr.option_enum m
| EErrorOnEmpty arg, m ->
let m = translate_mark m in
let pos = Expr.mark_pos m in
let cases =
EnumConstructor.Map.of_list
[
( Expr.none_constr,
let x = Var.make "_" in
Expr.make_abs [| x |] (Expr.efatalerror NoValue m) [TAny, pos] pos
);
(* | None x -> raise NoValueProvided *)
Expr.some_constr, Expr.fun_id ~var_name:"arg" m (* | Some x -> x *);
]
in
Expr.ematch ~e:(translate_expr arg) ~name:Expr.option_enum ~cases m
| EDefault { excepts; just; cons }, m ->
translate_default excepts just cons (translate_mark m)
| EPureDefault e, m ->
Expr.einj ~e:(translate_expr e) ~cons:Expr.some_constr
~name:Expr.option_enum (translate_mark m)
| EAppOp { op; tys; args }, m ->
Expr.eappop ~op:(Operator.translate op)
~tys:(List.map translate_typ tys)
~args:(List.map translate_expr args)
(translate_mark m)
| ( ( ELit _ | EArray _ | EVar _ | EApp _ | EAbs _ | EExternal _
| EIfThenElse _ | ETuple _ | ETupleAccess _ | EInj _ | EAssert _
| EFatalError _ | EStruct _ | EStructAccess _ | EMatch _ ),
_ ) as e ->
Expr.map ~f:translate_expr ~typ:translate_typ e
| _ -> .
let add_option_type ctx =
{
@ -26,9 +132,7 @@ let add_option_type ctx =
let add_option_type_program prg =
{ prg with decl_ctx = add_option_type prg.decl_ctx }
let translate_program_with_exceptions =
Compile_with_exceptions.translate_program
let translate_program_without_exceptions prg =
let prg = add_option_type_program prg in
Compile_without_exceptions.translate_program prg
let translate_program (prg : 'm D.program) : 'm A.program =
Program.map_exprs
(add_option_type_program prg)
~typ:translate_typ ~varf:Var.translate ~f:translate_expr

14
compiler/lcalc/from_dcalc.mli
View File

@ -1,6 +1,6 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
Denis Merigoux <denis.merigoux@inria.fr>
and social benefits computation rules. Copyright (C) 2020-2022 Inria,
contributor: Alain Delaët-Tixeuil <alain.delaet--tixeuil@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
@ -14,13 +14,9 @@
License for the specific language governing permissions and limitations under
the License. *)
val translate_program_with_exceptions : 'm Dcalc.Ast.program -> 'm Ast.program
(** Translation from the default calculus to the lambda calculus. This
translation uses exceptions to handle empty default terms. *)
val translate_program_without_exceptions :
'm Dcalc.Ast.program -> 'm Ast.program
(** Translation from the default calculus to the lambda calculus. This
translation uses an option monad to handle empty defaults terms. This
transformation is one piece to permit to compile toward legacy languages
that does not contains catchable exceptions. *)
that does not contains exceptions. *)
val translate_program : 'm Dcalc.Ast.program -> 'm Ast.program

5
compiler/plugins/api_web.ml
View File

@ -471,15 +471,13 @@ let run
output
optimize
check_invariants
avoid_exceptions
closure_conversion
monomorphize_types
_options =
let options = Global.enforce_options ~trace:true () in
let prg, type_ordering =
Driver.Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion ~typed:Expr.typed
~monomorphize_types
~closure_conversion ~typed:Expr.typed ~monomorphize_types
in
let jsoo_output_file, with_formatter =
Driver.Commands.get_output_format options ~ext:"_api_web.ml" output
@ -506,7 +504,6 @@ let term =
$ Cli.Flags.output
$ Cli.Flags.optimize
$ Cli.Flags.check_invariants
$ Cli.Flags.avoid_exceptions
$ Cli.Flags.closure_conversion
$ Cli.Flags.monomorphize_types

4
compiler/plugins/explain.ml
View File

@ -1382,9 +1382,7 @@ let run includes optimize ex_scope explain_options global_options =
~check_invariants:false ~typed:Expr.typed
in
Interpreter.load_runtime_modules prg
~hashf:
(Hash.finalise ~avoid_exceptions:false ~closure_conversion:false
~monomorphize_types:false);
~hashf:(Hash.finalise ~closure_conversion:false ~monomorphize_types:false);
let scope = Driver.Commands.get_scope_uid prg.decl_ctx ex_scope in
(* let result_expr, env = interpret_program prg scope in *)
let g, base_vars, env = program_to_graph explain_options prg scope in

5
compiler/plugins/json_schema.ml
View File

@ -210,15 +210,13 @@ let run
output
optimize
check_invariants
avoid_exceptions
closure_conversion
monomorphize_types
ex_scope
options =
let prg, _ =
Driver.Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion ~typed:Expr.typed
~monomorphize_types
~closure_conversion ~typed:Expr.typed ~monomorphize_types
in
let output_file, with_output =
Driver.Commands.get_output_format options ~ext:"_schema.json" output
@ -239,7 +237,6 @@ let term =
$ Cli.Flags.output
$ Cli.Flags.optimize
$ Cli.Flags.check_invariants
$ Cli.Flags.avoid_exceptions
$ Cli.Flags.closure_conversion
$ Cli.Flags.monomorphize_types
$ Cli.Flags.ex_scope

4
compiler/plugins/lazy_interp.ml
View File

@ -272,9 +272,7 @@ let run includes optimize check_invariants ex_scope options =
~typed:Expr.typed
in
Interpreter.load_runtime_modules prg
~hashf:
(Hash.finalise ~avoid_exceptions:false ~closure_conversion:false
~monomorphize_types:false);
~hashf:(Hash.finalise ~closure_conversion:false ~monomorphize_types:false);
let scope = Driver.Commands.get_scope_uid prg.decl_ctx ex_scope in
let result_expr, _env = interpret_program prg scope in
let fmt = Format.std_formatter in

15
compiler/plugins/python.ml
View File

@ -22,20 +22,12 @@
open Catala_utils
let run
includes
output
optimize
check_invariants
avoid_exceptions
closure_conversion
options =
let run includes output optimize check_invariants closure_conversion options =
let open Driver.Commands in
let prg, type_ordering =
Driver.Passes.scalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion ~keep_special_ops:false
~dead_value_assignment:true ~no_struct_literals:false
~monomorphize_types:false
~closure_conversion ~keep_special_ops:false ~dead_value_assignment:true
~no_struct_literals:false ~monomorphize_types:false
in
let output_file, with_output = get_output_format options ~ext:".py" output in
@ -50,7 +42,6 @@ let term =
$ Cli.Flags.output
$ Cli.Flags.optimize
$ Cli.Flags.check_invariants
$ Cli.Flags.avoid_exceptions
$ Cli.Flags.closure_conversion
let () =

12
compiler/scalc/print.ml
View File

@ -233,21 +233,11 @@ let format_item decl_ctx ?debug ppf def =
Format.pp_print_cut ppf ()
let format_program ?debug ppf prg =
let decl_ctx =
(* TODO: this is redundant with From_dcalc.add_option_type (which is already
applied in avoid_exceptions mode) *)
{
prg.ctx.decl_ctx with
ctx_enums =
EnumName.Map.add Expr.option_enum Expr.option_enum_config
prg.ctx.decl_ctx.ctx_enums;
}
in
Format.pp_open_vbox ppf 0;
ModuleName.Map.iter
(fun m var ->
Format.fprintf ppf "%a %a = %a@," Print.keyword "module" format_var_name
var ModuleName.format m)
prg.ctx.modules;
Format.pp_print_list (format_item decl_ctx ?debug) ppf prg.code_items;
Format.pp_print_list (format_item prg.ctx.decl_ctx ?debug) ppf prg.code_items;
Format.pp_close_box ppf ()

4
tests/func/good/closure_conversion.catala_en
View File

@ -24,7 +24,7 @@ $ catala Typecheck --check-invariants
```
```catala-test-inline
$ catala Lcalc --avoid-exceptions -O --closure-conversion
$ catala Lcalc -O --closure-conversion
type Eoption = | ENone of unit | ESome of any
type S_in = { x_in: bool; }
type S = { z: integer; }
@ -65,7 +65,7 @@ scope S2Use:
```
```catala-test-inline
$ catala Lcalc --avoid-exceptions -O --closure-conversion -s S2Use
$ catala Lcalc -O --closure-conversion -s S2Use
let scope S2Use
(S2Use_in: S2Use_in)
: S2Use {

8
tests/func/good/closure_conversion_reduce.catala_en
View File

@ -24,7 +24,7 @@ $ catala Typecheck --check-invariants
```
```catala-test-inline
$ catala Lcalc -s S --avoid-exceptions -O --closure-conversion
$ catala Lcalc -s S -O --closure-conversion
let scope S (S_in: S_in {x_in: list of integer}): S {y: integer} =
let get x : list of integer = S_in.x_in in
let set y : integer =
@ -38,12 +38,12 @@ let scope S (S_in: S_in {x_in: list of integer}): S {y: integer} =
```
The next test of closure conversion should give the same results, it checks that
`--avoid-exceptions` and `-O` are correctly implied by `--closure-conversion`
`-O` is correctly implied by `--closure-conversion`
The detection of closures that should not be converted because they are arguments
to reduce or other special operators relies on pattern matching the special
operator and its EAbs argument. However without exceptions on, because the
--avoid-exceptions pass is not optimized and produces more options than needed,
the closures that are arguments to special operators are let-binded with an
lcalc translation pass is not optimized and produces more options than needed,
the closures that are arguments to special operators are let-bound with an
option. This let-binding is reduced by partial evaluation, which is why the test
with optimizations on passes.

2
tests/func/good/closure_return.catala_en
View File

@ -22,7 +22,7 @@ $ catala Typecheck --check-invariants
```
```catala-test-inline
$ catala Lcalc --avoid-exceptions -O --closure-conversion
$ catala Lcalc -O --closure-conversion
type Eoption = | ENone of unit | ESome of any
type S_in = { x_in: bool; }
type S = { f: ((closure_env, integer) → integer, closure_env); }

4
tests/func/good/closure_through_scope.catala_en
View File

@ -30,7 +30,7 @@ $ catala Typecheck --check-invariants
```
```catala-test-inline
$ catala Lcalc -s T --avoid-exceptions -O --closure-conversion
$ catala Lcalc -s T -O --closure-conversion
let scope T (T_in: T_in): T {y: integer} =
let set s : S {f: ((closure_env, integer) → integer, closure_env)} =
{ S f = (closure_s1, to_closure_env ()); }
@ -45,7 +45,7 @@ let scope T (T_in: T_in): T {y: integer} =
```
```catala-test-inline
$ catala Interpret --lcalc -s T --avoid-exceptions -O --closure-conversion
$ catala Interpret --lcalc -s T -O --closure-conversion
┌─[RESULT]─
│ y = -2
└─

4
tests/func/good/scope_call_func_struct_closure.catala_en
View File

@ -53,7 +53,7 @@ $ catala Typecheck --check-invariants
```
```catala-test-inline
$ catala Lcalc --avoid-exceptions -O --closure-conversion
$ catala Lcalc -O --closure-conversion
type Eoption = | ENone of unit | ESome of any
type Result = {
r: ((closure_env, integer) → integer, closure_env);
@ -165,7 +165,7 @@ let scope Foo
```
```catala-test-inline
$ catala Interpret --lcalc -s Foo --avoid-exceptions -O --closure-conversion
$ catala Interpret --lcalc -s Foo -O --closure-conversion
┌─[RESULT]─
│ z = 11
└─

2
tests/scope/good/scope_call4.catala_en
View File

@ -68,7 +68,7 @@ $ catala interpret -s RentComputation --debug
```
```catala-test-inline
$ catala Interpret --lcalc -s RentComputation --avoid-exceptions --optimize --debug
$ catala Interpret --lcalc -s RentComputation --optimize --debug
[DEBUG] = INIT =
[DEBUG] = SURFACE =
[DEBUG] Parsing "tests/scope/good/scope_call4.catala_en"