From 583e80993a4e837d9679d26f8a3de2a1d48cd74b Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Mon, 24 Jun 2024 12:16:19 +0200 Subject: [PATCH] Remove the with-exceptions backend *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. --- Makefile | 2 +- build_system/clerk_driver.ml | 12 +- compiler/catala_utils/cli.ml | 11 +- compiler/catala_utils/cli.mli | 1 - compiler/catala_utils/hash.ml | 12 +- compiler/catala_utils/hash.mli | 7 +- compiler/driver.ml | 88 ++++-------- compiler/driver.mli | 2 - compiler/lcalc/closure_conversion.ml | 9 +- compiler/lcalc/compile_with_exceptions.ml | 95 ------------- compiler/lcalc/compile_with_exceptions.mli | 20 --- compiler/lcalc/compile_without_exceptions.ml | 126 ------------------ compiler/lcalc/compile_without_exceptions.mli | 22 --- compiler/lcalc/from_dcalc.ml | 118 +++++++++++++++- compiler/lcalc/from_dcalc.mli | 14 +- compiler/plugins/api_web.ml | 5 +- compiler/plugins/explain.ml | 4 +- compiler/plugins/json_schema.ml | 5 +- compiler/plugins/lazy_interp.ml | 4 +- compiler/plugins/python.ml | 15 +-- compiler/scalc/print.ml | 12 +- tests/func/good/closure_conversion.catala_en | 4 +- .../good/closure_conversion_reduce.catala_en | 8 +- tests/func/good/closure_return.catala_en | 2 +- .../func/good/closure_through_scope.catala_en | 4 +- .../scope_call_func_struct_closure.catala_en | 4 +- tests/scope/good/scope_call4.catala_en | 2 +- 27 files changed, 175 insertions(+), 433 deletions(-) delete mode 100644 compiler/lcalc/compile_with_exceptions.ml delete mode 100644 compiler/lcalc/compile_with_exceptions.mli delete mode 100644 compiler/lcalc/compile_without_exceptions.ml delete mode 100644 compiler/lcalc/compile_without_exceptions.mli diff --git a/Makefile b/Makefile index 7e777d80..fd641d71 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/build_system/clerk_driver.ml b/build_system/clerk_driver.ml index 5b8a0122..c62d5c43 100644 --- a/build_system/clerk_driver.ml +++ b/build_system/clerk_driver.ml @@ -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 diff --git a/compiler/catala_utils/cli.ml b/compiler/catala_utils/cli.ml index 3eddd739..961131c7 100644 --- a/compiler/catala_utils/cli.ml +++ b/compiler/catala_utils/cli.ml @@ -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 diff --git a/compiler/catala_utils/cli.mli b/compiler/catala_utils/cli.mli index fe1b723d..d9928c29 100644 --- a/compiler/catala_utils/cli.mli +++ b/compiler/catala_utils/cli.mli @@ -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 diff --git a/compiler/catala_utils/hash.ml b/compiler/catala_utils/hash.ml index d92e790f..59fd8f35 100644 --- a/compiler/catala_utils/hash.ml +++ b/compiler/catala_utils/hash.ml @@ -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 *) diff --git a/compiler/catala_utils/hash.mli b/compiler/catala_utils/hash.mli index b70ba2f1..4d18aba6 100644 --- a/compiler/catala_utils/hash.mli +++ b/compiler/catala_utils/hash.mli @@ -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 diff --git a/compiler/driver.ml b/compiler/driver.ml index a87bbbe0..f4efd0a9 100644 --- a/compiler/driver.ml +++ b/compiler/driver.ml @@ -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 @{--avoid-exceptions@} if \ - you@ also@ need@ @{--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 @{--avoid-exceptions@}, \ - @{--closure-conversion@} and @{--monomorphize-types@} \ - only make sense with the @{--lcalc@} option" + "The flags @{--closure-conversion@} and \ + @{--monomorphize-types@} only make sense with the \ + @{--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 diff --git a/compiler/driver.mli b/compiler/driver.mli index f6109ba6..3184a8e7 100644 --- a/compiler/driver.mli +++ b/compiler/driver.mli @@ -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 -> diff --git a/compiler/lcalc/closure_conversion.ml b/compiler/lcalc/closure_conversion.ml index 2849de40..1a3bb032 100644 --- a/compiler/lcalc/closure_conversion.ml +++ b/compiler/lcalc/closure_conversion.ml @@ -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 } diff --git a/compiler/lcalc/compile_with_exceptions.ml b/compiler/lcalc/compile_with_exceptions.ml deleted file mode 100644 index d3450c13..00000000 --- a/compiler/lcalc/compile_with_exceptions.ml +++ /dev/null @@ -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 - - 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 diff --git a/compiler/lcalc/compile_with_exceptions.mli b/compiler/lcalc/compile_with_exceptions.mli deleted file mode 100644 index da0f4d78..00000000 --- a/compiler/lcalc/compile_with_exceptions.mli +++ /dev/null @@ -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 - - 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 diff --git a/compiler/lcalc/compile_without_exceptions.ml b/compiler/lcalc/compile_without_exceptions.ml deleted file mode 100644 index 3f23af4a..00000000 --- a/compiler/lcalc/compile_without_exceptions.ml +++ /dev/null @@ -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 - - 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 diff --git a/compiler/lcalc/compile_without_exceptions.mli b/compiler/lcalc/compile_without_exceptions.mli deleted file mode 100644 index 6bb2b18d..00000000 --- a/compiler/lcalc/compile_without_exceptions.mli +++ /dev/null @@ -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 - - 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 diff --git a/compiler/lcalc/from_dcalc.ml b/compiler/lcalc/from_dcalc.ml index 98e49b4b..7f8ef858 100644 --- a/compiler/lcalc/from_dcalc.ml +++ b/compiler/lcalc/from_dcalc.ml @@ -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 + Alain Delaët-Tixeuil 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 diff --git a/compiler/lcalc/from_dcalc.mli b/compiler/lcalc/from_dcalc.mli index fb4ba11b..6bb2b18d 100644 --- a/compiler/lcalc/from_dcalc.mli +++ b/compiler/lcalc/from_dcalc.mli @@ -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 + and social benefits computation rules. Copyright (C) 2020-2022 Inria, + contributor: Alain Delaët-Tixeuil 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 diff --git a/compiler/plugins/api_web.ml b/compiler/plugins/api_web.ml index 73d1a22a..b7fb1e74 100644 --- a/compiler/plugins/api_web.ml +++ b/compiler/plugins/api_web.ml @@ -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 diff --git a/compiler/plugins/explain.ml b/compiler/plugins/explain.ml index 929f15f9..29610223 100644 --- a/compiler/plugins/explain.ml +++ b/compiler/plugins/explain.ml @@ -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 diff --git a/compiler/plugins/json_schema.ml b/compiler/plugins/json_schema.ml index 70779512..d187e59e 100644 --- a/compiler/plugins/json_schema.ml +++ b/compiler/plugins/json_schema.ml @@ -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 diff --git a/compiler/plugins/lazy_interp.ml b/compiler/plugins/lazy_interp.ml index 7a2d4d02..52d549c9 100644 --- a/compiler/plugins/lazy_interp.ml +++ b/compiler/plugins/lazy_interp.ml @@ -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 diff --git a/compiler/plugins/python.ml b/compiler/plugins/python.ml index 3ec2c558..1c167290 100644 --- a/compiler/plugins/python.ml +++ b/compiler/plugins/python.ml @@ -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 () = diff --git a/compiler/scalc/print.ml b/compiler/scalc/print.ml index 32d681aa..5863678f 100644 --- a/compiler/scalc/print.ml +++ b/compiler/scalc/print.ml @@ -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 () diff --git a/tests/func/good/closure_conversion.catala_en b/tests/func/good/closure_conversion.catala_en index e869a0de..11211c23 100644 --- a/tests/func/good/closure_conversion.catala_en +++ b/tests/func/good/closure_conversion.catala_en @@ -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 { diff --git a/tests/func/good/closure_conversion_reduce.catala_en b/tests/func/good/closure_conversion_reduce.catala_en index a799b424..de8aa45a 100644 --- a/tests/func/good/closure_conversion_reduce.catala_en +++ b/tests/func/good/closure_conversion_reduce.catala_en @@ -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. diff --git a/tests/func/good/closure_return.catala_en b/tests/func/good/closure_return.catala_en index e3cfd85e..310a6ab0 100644 --- a/tests/func/good/closure_return.catala_en +++ b/tests/func/good/closure_return.catala_en @@ -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); } diff --git a/tests/func/good/closure_through_scope.catala_en b/tests/func/good/closure_through_scope.catala_en index c0a2036a..ccd4680a 100644 --- a/tests/func/good/closure_through_scope.catala_en +++ b/tests/func/good/closure_through_scope.catala_en @@ -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 └─ diff --git a/tests/func/good/scope_call_func_struct_closure.catala_en b/tests/func/good/scope_call_func_struct_closure.catala_en index def85b5f..6d3a5000 100644 --- a/tests/func/good/scope_call_func_struct_closure.catala_en +++ b/tests/func/good/scope_call_func_struct_closure.catala_en @@ -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 └─ diff --git a/tests/scope/good/scope_call4.catala_en b/tests/scope/good/scope_call4.catala_en index e9fb67f0..96af8776 100644 --- a/tests/scope/good/scope_call4.catala_en +++ b/tests/scope/good/scope_call4.catala_en @@ -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"