diff --git a/compiler/dcalc/from_scopelang.ml b/compiler/dcalc/from_scopelang.ml index f084eca6..4da2cb2d 100644 --- a/compiler/dcalc/from_scopelang.ml +++ b/compiler/dcalc/from_scopelang.ml @@ -117,7 +117,11 @@ let merge_defaults (Expr.with_ty m_callee (Mark.add (Expr.mark_pos m_callee) (TLit TBool))) in - let d = Expr.make_default [caller] ltrue (Expr.rebox body) in + + let cons = Expr.make_puredefault (Expr.rebox body) in + let d = + Expr.edefault ~excepts:[caller] ~just:ltrue ~cons (Mark.get cons) + in Expr.make_abs vars (Expr.make_erroronempty d) tys (Expr.mark_pos m_callee) | _ -> assert false (* should not happen because there should always be a lambda at the @@ -136,7 +140,9 @@ let merge_defaults Expr.elit (LBool true) (Expr.with_ty m (Mark.add (Expr.mark_pos m) (TLit TBool))) in - Expr.make_erroronempty (Expr.make_default [caller] ltrue callee) + let cons = Expr.make_puredefault callee in + Expr.make_erroronempty + (Expr.edefault ~excepts:[caller] ~just:ltrue ~cons (Mark.get cons)) in body @@ -567,8 +573,9 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) : | EDefault { excepts; just; cons } -> let excepts = collapse_similar_outcomes excepts in Expr.edefault - (List.map (translate_expr ctx) excepts) - (translate_expr ctx just) (translate_expr ctx cons) m + ~excepts:(List.map (translate_expr ctx) excepts) + ~just:(translate_expr ctx just) ~cons:(translate_expr ctx cons) m + | EPureDefault e -> Expr.epuredefault (translate_expr ctx e) m | ELocation (ScopelangScopeVar { name = a }) -> let v, _, _ = ScopeVar.Map.find (Mark.remove a) ctx.scope_vars in Expr.evar v m diff --git a/compiler/lcalc/compile_with_exceptions.ml b/compiler/lcalc/compile_with_exceptions.ml index df05747c..e13aacd3 100644 --- a/compiler/lcalc/compile_with_exceptions.ml +++ b/compiler/lcalc/compile_with_exceptions.ml @@ -56,6 +56,7 @@ and translate_expr (e : 'm D.expr) : 'm A.expr boxed = m | EDefault { excepts; just; cons } -> translate_default excepts just cons (Mark.get e) + | EPureDefault e -> translate_expr e | EOp { op; tys } -> Expr.eop (Operator.translate op) tys m | ( ELit _ | EApp _ | EArray _ | EVar _ | EExternal _ | EAbs _ | EIfThenElse _ | ETuple _ | ETupleAccess _ | EInj _ | EAssert _ | EStruct _ diff --git a/compiler/lcalc/compile_without_exceptions.ml b/compiler/lcalc/compile_without_exceptions.ml index 6c5220fa..74061a52 100644 --- a/compiler/lcalc/compile_without_exceptions.ml +++ b/compiler/lcalc/compile_without_exceptions.ml @@ -155,6 +155,7 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr (Expr.eop Op.HandleDefaultOpt [TAny, pos; TAny, pos; TAny, pos] m') [Expr.earray excepts' m; Expr.thunk_term just' m; Expr.thunk_term cons' m] pos + | EPureDefault e -> trans ctx e | ELit l -> Ast.OptionMonad.return ~mark (Expr.elit l m) | EEmptyError -> Ast.OptionMonad.empty ~mark | EErrorOnEmpty arg -> diff --git a/compiler/scopelang/from_desugared.ml b/compiler/scopelang/from_desugared.ml index 30684063..7032a5e7 100644 --- a/compiler/scopelang/from_desugared.ml +++ b/compiler/scopelang/from_desugared.ml @@ -142,11 +142,14 @@ let rec translate_expr (ctx : ctx) (e : D.expr) : untyped Ast.expr boxed = let arg = Var.make "arg" in let pos = Expr.mark_pos m in Expr.make_abs [| arg |] - (Expr.edefault [] (Expr.elit (LBool true) m) - (Expr.make_app e' [Expr.evar arg m] pos) + (Expr.edefault ~excepts:[] ~just:(Expr.elit (LBool true) m) + ~cons: + (Expr.epuredefault + (Expr.make_app e' [Expr.evar arg m] pos) + m) m) targs pos - | Some _ -> Expr.edefault [] (Expr.elit (LBool true) m) e' m + | Some _ -> Expr.epuredefault e' m | None -> e' in ScopeVar.Map.add v' e' args') @@ -166,8 +169,8 @@ let rec translate_expr (ctx : ctx) (e : D.expr) : untyped Ast.expr boxed = Expr.eapp (Expr.eop op (List.rev tys) m1) (List.rev args) m) | EOp _ -> assert false (* Only allowed within [EApp] *) | ( EStruct _ | ETuple _ | ETupleAccess _ | EInj _ | EMatch _ | ELit _ - | EApp _ | EDefault _ | EIfThenElse _ | EArray _ | EEmptyError - | EErrorOnEmpty _ ) as e -> + | EApp _ | EDefault _ | EPureDefault _ | EIfThenElse _ | EArray _ + | EEmptyError | EErrorOnEmpty _ ) as e -> Expr.map ~f:(translate_expr ctx) (e, m) (** {1 Rule tree construction} *) @@ -416,18 +419,19 @@ let rec rule_tree_to_expr list in let default_containing_base_cases = - Expr.make_default - (List.map2 - (fun base_just base_cons -> - Expr.make_default [] - (* Here we insert the logging command that records when a decision - is taken for the value of a variable. *) - (tag_with_log_entry base_just PosRecordIfTrueBool []) - base_cons) - (translate_and_unbox_list base_just_list) - (translate_and_unbox_list base_cons_list)) - (Expr.elit (LBool false) emark) - (Expr.eerroronempty (Expr.eemptyerror emark) emark) + Expr.edefault + ~excepts: + (List.map2 + (fun base_just base_cons -> + Expr.make_default [] + (* Here we insert the logging command that records when a + decision is taken for the value of a variable. *) + (tag_with_log_entry base_just PosRecordIfTrueBool []) + base_cons) + (translate_and_unbox_list base_just_list) + (translate_and_unbox_list base_cons_list)) + ~just:(Expr.elit (LBool false) emark) + ~cons:(Expr.eemptyerror emark) emark in let exceptions = List.map @@ -438,9 +442,12 @@ let rec rule_tree_to_expr let default = if exceptions = [] then default_containing_base_cases else - Expr.make_default exceptions - (Expr.elit (LBool true) emark) - (Expr.eerroronempty default_containing_base_cases emark) + Expr.edefault ~excepts:exceptions + ~just:(Expr.elit (LBool true) emark) + ~cons: + (* if toplevel then Expr.eerroronempty default_containing_base_cases emark + * else *) + default_containing_base_cases emark in let default = if toplevel && not (subscope && is_reentrant_var) then diff --git a/compiler/shared_ast/definitions.ml b/compiler/shared_ast/definitions.ml index 03c7ed08..7e2d906f 100644 --- a/compiler/shared_ast/definitions.ml +++ b/compiler/shared_ast/definitions.ml @@ -550,6 +550,9 @@ and ('a, 'b, 'm) base_gexpr = cons : ('a, 'm) gexpr; } -> ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr + | EPureDefault : + ('a, 'm) gexpr + -> ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr | EEmptyError : ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr | EErrorOnEmpty : ('a, 'm) gexpr diff --git a/compiler/shared_ast/expr.ml b/compiler/shared_ast/expr.ml index 72f8ea24..2f5063b6 100644 --- a/compiler/shared_ast/expr.ml +++ b/compiler/shared_ast/expr.ml @@ -126,10 +126,12 @@ let eapp f args = Box.app1n f args @@ fun f args -> EApp { f; args } let eassert e1 = Box.app1 e1 @@ fun e1 -> EAssert e1 let eop op tys = Box.app0 @@ EOp { op; tys } -let edefault excepts just cons = +let edefault ~excepts ~just ~cons = Box.app2n just cons excepts @@ fun just cons excepts -> EDefault { excepts; just; cons } +let epuredefault e = Box.app1 e @@ fun e1 -> EPureDefault e1 + let eifthenelse cond etrue efalse = Box.app3 cond etrue efalse @@ fun cond etrue efalse -> EIfThenElse { cond; etrue; efalse } @@ -288,7 +290,8 @@ let map | EInj { name; cons; e } -> einj ~name ~cons ~e:(f e) m | EAssert e1 -> eassert (f e1) m | EDefault { excepts; just; cons } -> - edefault (List.map f excepts) (f just) (f cons) m + edefault ~excepts:(List.map f excepts) ~just:(f just) ~cons:(f cons) m + | EPureDefault e1 -> epuredefault (f e1) m | EEmptyError -> eemptyerror m | EErrorOnEmpty e1 -> eerroronempty (f e1) m | ECatch { body; exn; handler } -> ecatch (f body) exn (f handler) m @@ -333,6 +336,7 @@ let shallow_fold | EInj { e; _ } -> acc |> f e | EAssert e -> acc |> f e | EDefault { excepts; just; cons } -> acc |> lfold excepts |> f just |> f cons + | EPureDefault e -> acc |> f e | EErrorOnEmpty e -> acc |> f e | ECatch { body; handler; _ } -> acc |> f body |> f handler | EStruct { fields; _ } -> acc |> StructField.Map.fold (fun _ -> f) fields @@ -399,7 +403,10 @@ let map_gather let acc1, excepts = lfoldmap excepts in let acc2, just = f just in let acc3, cons = f cons in - join (join acc1 acc2) acc3, edefault excepts just cons m + join (join acc1 acc2) acc3, edefault ~excepts ~just ~cons m + | EPureDefault e -> + let acc, e = f e in + acc, epuredefault e m | EEmptyError -> acc, eemptyerror m | EErrorOnEmpty e -> let acc, e = f e in @@ -597,6 +604,7 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool = | ( EDefault { excepts = exc1; just = def1; cons = cons1 }, EDefault { excepts = exc2; just = def2; cons = cons2 } ) -> equal def1 def2 && equal cons1 cons2 && equal_list exc1 exc2 + | EPureDefault e1, EPureDefault e2 -> equal e1 e2 | ( EIfThenElse { cond = if1; etrue = then1; efalse = else1 }, EIfThenElse { cond = if2; etrue = then2; efalse = else2 } ) -> equal if1 if2 && equal then1 then2 && equal else1 else2 @@ -632,10 +640,10 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool = ECustom { obj = obj2; targs = targs2; tret = tret2 } ) -> Type.equal_list targs1 targs2 && Type.equal tret1 tret2 && obj1 == obj2 | ( ( EVar _ | EExternal _ | ETuple _ | ETupleAccess _ | EArray _ | ELit _ - | EAbs _ | EApp _ | EAssert _ | EOp _ | EDefault _ | EIfThenElse _ - | EEmptyError | EErrorOnEmpty _ | ERaise _ | ECatch _ | ELocation _ - | EStruct _ | EDStructAccess _ | EStructAccess _ | EInj _ | EMatch _ - | EScopeCall _ | ECustom _ ), + | EAbs _ | EApp _ | EAssert _ | EOp _ | EDefault _ | EPureDefault _ + | EIfThenElse _ | EEmptyError | EErrorOnEmpty _ | ERaise _ | ECatch _ + | ELocation _ | EStruct _ | EDStructAccess _ | EStructAccess _ | EInj _ + | EMatch _ | EScopeCall _ | ECustom _ ), _ ) -> false @@ -714,6 +722,8 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int = compare just1 just2 @@< fun () -> compare cons1 cons2 @@< fun () -> List.compare compare exs1 exs2 + | EPureDefault e1, EPureDefault e2 -> + compare e1 e2 | EEmptyError, EEmptyError -> 0 | EErrorOnEmpty e1, EErrorOnEmpty e2 -> compare e1 e2 @@ -746,6 +756,7 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int = | EInj _, _ -> -1 | _, EInj _ -> 1 | EAssert _, _ -> -1 | _, EAssert _ -> 1 | EDefault _, _ -> -1 | _, EDefault _ -> 1 + | EPureDefault _, _ -> -1 | _, EPureDefault _ -> 1 | EEmptyError , _ -> -1 | _, EEmptyError -> 1 | EErrorOnEmpty _, _ -> -1 | _, EErrorOnEmpty _ -> 1 | ERaise _, _ -> -1 | _, ERaise _ -> 1 @@ -766,6 +777,7 @@ let rec skip_wrappers : type a. (a, 'm) gexpr -> (a, 'm) gexpr = function | EErrorOnEmpty e, _ -> skip_wrappers e | EDefault { excepts = []; just = ELit (LBool true), _; cons = e }, _ -> skip_wrappers e + | EPureDefault e, _ -> skip_wrappers e | e -> e let remove_logging_calls e = @@ -871,6 +883,7 @@ let rec size : type a. (a, 't) gexpr -> int = | EInj { e; _ } -> size e + 1 | EAssert e -> size e + 1 | EErrorOnEmpty e -> size e + 1 + | EPureDefault e -> size e + 1 | EApp { f; args } -> List.fold_left (fun acc arg -> acc + size arg) (1 + size f) args | EAbs { binder; _ } -> @@ -959,14 +972,15 @@ let make_let_in x tau e1 e2 mpos = let make_multiple_let_in xs taus e1s e2 mpos = make_app (make_abs xs e2 taus mpos) e1s (pos e2) -let make_default exc just cons = +let make_puredefault e = let mark = - map_mark - (fun pos -> pos) - (fun cty -> TDefault cty, Mark.get cty) - (Mark.get cons) + map_mark (fun pos -> pos) (fun ty -> TDefault ty, Mark.get ty) (Mark.get e) in - edefault exc just cons mark + epuredefault e mark + +let make_default excepts just cons = + let cons = make_puredefault cons in + edefault ~excepts ~just ~cons (Mark.get cons) let make_tuple el m0 = match el with diff --git a/compiler/shared_ast/expr.mli b/compiler/shared_ast/expr.mli index 90f62583..0ae09317 100644 --- a/compiler/shared_ast/expr.mli +++ b/compiler/shared_ast/expr.mli @@ -80,8 +80,13 @@ val eassert : val eop : 'a operator -> typ list -> 'm mark -> ('a any, 'm) boxed_gexpr val edefault : - ('a, 'm) boxed_gexpr list -> - ('a, 'm) boxed_gexpr -> + excepts:('a, 'm) boxed_gexpr list -> + just:('a, 'm) boxed_gexpr -> + cons:('a, 'm) boxed_gexpr -> + 'm mark -> + ((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr + +val epuredefault : ('a, 'm) boxed_gexpr -> 'm mark -> ((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr @@ -317,6 +322,9 @@ val make_app : Pos.t -> ('a any, 'm) boxed_gexpr +val make_puredefault : + ('a, 'm) boxed_gexpr -> ((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr + val make_erroronempty : ('a, 'm) boxed_gexpr -> ((< defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr @@ -348,6 +356,8 @@ val make_default : ('a, 'm) boxed_gexpr -> (* 'm mark -> *) ((< polymorphic : yes ; defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr +(** The [cons] argument is implicitely made into a [EPureDefault] by this + function *) val make_tuple : ('a any, 'm) boxed_gexpr list -> 'm mark -> ('a, 'm) boxed_gexpr diff --git a/compiler/shared_ast/interpreter.ml b/compiler/shared_ast/interpreter.ml index bafe199a..6dc101df 100644 --- a/compiler/shared_ast/interpreter.ml +++ b/compiler/shared_ast/interpreter.ml @@ -713,7 +713,8 @@ let rec evaluate_expr : | EEmptyError, _ -> Message.raise_spanned_error (Expr.pos e') "This variable evaluated to an empty term (no rule that defined it \ - applied in this situation)" + applied in this situation): %a" + Expr.format e | e -> e) | EDefault { excepts; just; cons } -> ( let excepts = List.map (evaluate_expr ctx lang) excepts in @@ -722,7 +723,6 @@ let rec evaluate_expr : | 0 -> ( let just = evaluate_expr ctx lang just in match Mark.remove just with - | EEmptyError -> Mark.add m EEmptyError | ELit (LBool true) -> evaluate_expr ctx lang cons | ELit (LBool false) -> Mark.copy e EEmptyError | _ -> @@ -738,6 +738,7 @@ let rec evaluate_expr : (List.filter (fun sub -> not (is_empty_error sub)) excepts)) "There is a conflict between multiple valid consequences for assigning \ the same variable.") + | EPureDefault e -> evaluate_expr ctx lang e | ERaise exn -> raise (CatalaException exn) | ECatch { body; exn; handler } -> ( try evaluate_expr ctx lang body @@ -790,6 +791,7 @@ let addcustom e = | (ECustom _, _) as e -> Expr.map ~f e | EOp { op; tys }, m -> Expr.eop (Operator.translate op) tys m | (EDefault _, _) as e -> Expr.map ~f e + | (EPureDefault _, _) as e -> Expr.map ~f e | (EEmptyError, _) as e -> Expr.map ~f e | (EErrorOnEmpty _, _) as e -> Expr.map ~f e | (ECatch _, _) as e -> Expr.map ~f e @@ -811,6 +813,7 @@ let delcustom e = | ECustom _, _ -> invalid_arg "Custom term remaining in evaluated term" | EOp { op; tys }, m -> Expr.eop (Operator.translate op) tys m | (EDefault _, _) as e -> Expr.map ~f e + | (EPureDefault _, _) as e -> Expr.map ~f e | (EEmptyError, _) as e -> Expr.map ~f e | (EErrorOnEmpty _, _) as e -> Expr.map ~f e | (ECatch _, _) as e -> Expr.map ~f e diff --git a/compiler/shared_ast/print.ml b/compiler/shared_ast/print.ml index a67efb47..8361e854 100644 --- a/compiler/shared_ast/print.ml +++ b/compiler/shared_ast/print.ml @@ -428,6 +428,7 @@ module Precedence = struct | EDStructAccess _ | EStructAccess _ -> Dot | EAssert _ -> App | EDefault _ -> Contained + | EPureDefault _ -> Contained | EEmptyError -> Contained | EErrorOnEmpty _ -> App | ERaise _ -> App @@ -645,6 +646,12 @@ module ExprGen (C : EXPR_PARAM) = struct cons (default_punct (List.hd colors)) "⟩" + | EPureDefault e -> + Format.fprintf fmt "%a%a%a" + (default_punct (List.hd colors)) + "⟨" expr e + (default_punct (List.hd colors)) + "⟩" | EEmptyError -> lit_style fmt "∅" | EErrorOnEmpty e' -> Format.fprintf fmt "@[%a@ %a@]" op_style "error_empty" @@ -1075,8 +1082,9 @@ module UserFacing = struct | EAbs _ -> Format.pp_print_string ppf "" | EExternal _ -> Format.pp_print_string ppf "" | EApp _ | EOp _ | EVar _ | EIfThenElse _ | EMatch _ | ETupleAccess _ - | EStructAccess _ | EAssert _ | EDefault _ | EErrorOnEmpty _ | ERaise _ - | ECatch _ | ELocation _ | EScopeCall _ | EDStructAccess _ | ECustom _ -> + | EStructAccess _ | EAssert _ | EDefault _ | EPureDefault _ + | EErrorOnEmpty _ | ERaise _ | ECatch _ | ELocation _ | EScopeCall _ + | EDStructAccess _ | ECustom _ -> fallback ppf e (* This function is already in module [Expr], but [Expr] depends on this diff --git a/compiler/shared_ast/typing.ml b/compiler/shared_ast/typing.ml index 9ce3e69b..fe460856 100644 --- a/compiler/shared_ast/typing.ml +++ b/compiler/shared_ast/typing.ml @@ -906,11 +906,7 @@ and typecheck_expr_top_down : in Expr.eop op tys mark | A.EDefault { excepts; just; cons } -> - let inner_ty = unionfind (TAny (Any.fresh ())) in - unify ctx e (unionfind (TDefault inner_ty)) tau; - let cons' = - typecheck_expr_top_down ~leave_unresolved ctx env inner_ty cons - in + let cons' = typecheck_expr_top_down ~leave_unresolved ctx env tau cons in let just' = typecheck_expr_top_down ~leave_unresolved ctx env (unionfind ~pos:just (TLit TBool)) @@ -919,7 +915,14 @@ and typecheck_expr_top_down : let excepts' = List.map (typecheck_expr_top_down ~leave_unresolved ctx env tau) excepts in - Expr.edefault excepts' just' cons' context_mark + Expr.edefault ~excepts:excepts' ~just:just' ~cons:cons' context_mark + | A.EPureDefault e1 -> + let inner_ty = unionfind ~pos:e1 (TAny (Any.fresh ())) in + let mark = + mark_with_tau_and_unify (unionfind ~pos:e1 (TDefault inner_ty)) + in + let e1' = typecheck_expr_top_down ~leave_unresolved ctx env inner_ty e1 in + Expr.epuredefault e1' mark | A.EIfThenElse { cond; etrue = et; efalse = ef } -> let et' = typecheck_expr_top_down ~leave_unresolved ctx env tau et in let ef' = typecheck_expr_top_down ~leave_unresolved ctx env tau ef in diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index f5ea87f2..2db4e0bc 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -764,6 +764,7 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr = | EAssert e -> translate_expr ctx e | EOp _ -> failwith "[Z3 encoding] EOp unsupported" | EDefault _ -> failwith "[Z3 encoding] EDefault unsupported" + | EPureDefault _ -> failwith "[Z3 encoding] EPureDefault unsupported" | EIfThenElse { cond = e_if; etrue = e_then; efalse = e_else } -> (* We rely on Z3's native encoding for ite to encode this node. There might be some interesting optimization in the future about when to split this diff --git a/tests/test_array/good/aggregation_3.catala_en b/tests/test_array/good/aggregation_3.catala_en index 7bfedbbc..cee922d0 100644 --- a/tests/test_array/good/aggregation_3.catala_en +++ b/tests/test_array/good/aggregation_3.catala_en @@ -34,7 +34,7 @@ scope S: ```catala-test-inline $ catala scopelang -s S let scope S (x: integer|internal|output) = - let x : integer = error_empty ⟨ ⟨true ⊢ 0⟩ | false ⊢ error_empty ∅ ⟩; + let x : integer = error_empty ⟨ ⟨true ⊢ ⟨0⟩⟩ | false ⊢ ∅ ⟩; assert (map (λ (i: integer) → i + 2) [ 1; 2; 3 ]) = [ 3; 4; 5 ]; assert (filter (λ (i: integer) → i >= 2) [ 1; 2; 3 ]) = [ 2; 3 ]; assert (map (λ (i: integer) → i + 2) diff --git a/tests/test_bool/good/test_bool.catala_en b/tests/test_bool/good/test_bool.catala_en index 95946d8e..adac4fbb 100644 --- a/tests/test_bool/good/test_bool.catala_en +++ b/tests/test_bool/good/test_bool.catala_en @@ -19,16 +19,14 @@ let TestBool : TestBool_in → TestBool = let bar : unit → ⟨integer⟩ = TestBool_in.bar_in in let bar1 : integer = error_empty - ⟨ bar () - | true ⊢ error_empty ⟨ ⟨true ⊢ 1⟩ | false ⊢ error_empty ∅ ⟩ ⟩ + ⟨ bar () | true ⊢ ⟨error_empty ⟨ ⟨true ⊢ ⟨1⟩⟩ | false ⊢ ∅ ⟩⟩ ⟩ in let foo1 : bool = error_empty ⟨ foo () | true - ⊢ error_empty - ⟨ ⟨bar1 >= 0 ⊢ true⟩, ⟨bar1 < 0 ⊢ false⟩ - | false ⊢ error_empty ∅ ⟩ ⟩ + ⊢ ⟨error_empty + ⟨ ⟨bar1 >= 0 ⊢ ⟨true⟩⟩, ⟨bar1 < 0 ⊢ ⟨false⟩⟩ | false ⊢ ∅ ⟩⟩ ⟩ in { TestBool foo = foo1; bar = bar1; } in @@ -52,10 +50,9 @@ struct TestBool = { let scope TestBool (foo: ⟨bool⟩|context|output) (bar: ⟨integer⟩|context| output) = let bar : integer = reentrant or by default - error_empty ⟨ ⟨true ⊢ 1⟩ | false ⊢ error_empty ∅ ⟩; + error_empty ⟨ ⟨true ⊢ ⟨1⟩⟩ | false ⊢ ∅ ⟩; let foo : bool = reentrant or by default - error_empty - ⟨ ⟨bar >= 0 ⊢ true⟩, ⟨bar < 0 ⊢ false⟩ | false ⊢ error_empty ∅ ⟩ + error_empty ⟨ ⟨bar >= 0 ⊢ ⟨true⟩⟩, ⟨bar < 0 ⊢ ⟨false⟩⟩ | false ⊢ ∅ ⟩ ``` ```catala-test-inline $ catala Interpret_Lcalc -s TestBool --avoid_exceptions --optimize diff --git a/tests/test_default/bad/empty.catala_en b/tests/test_default/bad/empty.catala_en index f25e7747..1ac3bc8a 100644 --- a/tests/test_default/bad/empty.catala_en +++ b/tests/test_default/bad/empty.catala_en @@ -19,7 +19,8 @@ $ catala Interpret -s A │ ‾ └─ Article [ERROR] -This variable evaluated to an empty term (no rule that defined it applied in this situation) +This variable evaluated to an empty term (no rule that defined it applied in this situation): +error_empty ⟨ ⟨false ⊢ ⟨error_empty ∅⟩⟩ | false ⊢ ∅ ⟩ ┌─⯈ tests/test_default/bad/empty.catala_en:6.10-6.11: └─┐ diff --git a/tests/test_default/bad/empty_with_rules.catala_en b/tests/test_default/bad/empty_with_rules.catala_en index f8271e06..bf16c9ed 100644 --- a/tests/test_default/bad/empty_with_rules.catala_en +++ b/tests/test_default/bad/empty_with_rules.catala_en @@ -15,7 +15,9 @@ scope A: ```catala-test-inline $ catala Interpret -s A [ERROR] -This variable evaluated to an empty term (no rule that defined it applied in this situation) +This variable evaluated to an empty term (no rule that defined it applied in this situation): +error_empty + ⟨ ⟨ ⟨ ⟨1 = 4 ⊢ ⟨1⟩⟩ | 1 = 3 ⊢ ⟨1⟩ ⟩ | 1 = 2 ⊢ ⟨1⟩ ⟩ | false ⊢ ∅ ⟩ ┌─⯈ tests/test_default/bad/empty_with_rules.catala_en:5.10-5.11: └─┐ diff --git a/tests/test_exception/good/double_definition.catala_en b/tests/test_exception/good/double_definition.catala_en index 364cfe02..e9203bc5 100644 --- a/tests/test_exception/good/double_definition.catala_en +++ b/tests/test_exception/good/double_definition.catala_en @@ -26,8 +26,7 @@ $ catala Scopelang -s Foo │ ‾‾‾‾‾‾‾‾‾‾‾‾ └─ Foo let scope Foo (x: integer|internal|output) = - let x : integer = - error_empty ⟨ ⟨true ⊢ 1⟩, ⟨true ⊢ 1⟩ | false ⊢ error_empty ∅ ⟩ + let x : integer = error_empty ⟨ ⟨true ⊢ ⟨1⟩⟩, ⟨true ⊢ ⟨1⟩⟩ | false ⊢ ∅ ⟩ ``` In Scopelang we have what looks like conflicting exceptions. But after @@ -53,7 +52,7 @@ $ catala Dcalc -s Foo └─ Foo let scope Foo (Foo_in: Foo_in): Foo {x: integer} = let set x : integer = - error_empty ⟨ ⟨ ⟨true ⊢ 1⟩ | true ⊢ 1 ⟩ | false ⊢ error_empty ∅ ⟩ + error_empty ⟨ ⟨ ⟨true ⊢ ⟨1⟩⟩ | true ⊢ ⟨1⟩ ⟩ | false ⊢ ∅ ⟩ in return { Foo x = x; } ``` diff --git a/tests/test_exception/good/groups_of_exceptions.catala_en b/tests/test_exception/good/groups_of_exceptions.catala_en index 34a7e9f5..6144ba7f 100644 --- a/tests/test_exception/good/groups_of_exceptions.catala_en +++ b/tests/test_exception/good/groups_of_exceptions.catala_en @@ -29,23 +29,45 @@ scope Foo: exception intermediate definition x under condition y = 5 consequence equals 5 + +declaration scope Test: + f scope Foo + output x content integer + +scope Test: + definition f.y equals 2 + definition x equals f.x ``` + +```catala-test-inline +$ catala interpret -s Test +[RESULT] Computation successful! Results: +[RESULT] x = 2 +``` + + ```catala-test-inline $ catala Scopelang struct Foo = { x: integer } +struct Test = { + x: integer +} + let scope Foo (y: integer|input) (x: integer|internal|output) = let x : integer = error_empty - ⟨ ⟨ ⟨ ⟨y = 4 ⊢ 4⟩, ⟨y = 5 ⊢ 5⟩ | false ⊢ error_empty ∅ ⟩ - | true - ⊢ error_empty - ⟨ ⟨y = 2 ⊢ 2⟩, ⟨y = 3 ⊢ 3⟩ | false ⊢ error_empty ∅ ⟩ ⟩ - | true - ⊢ error_empty ⟨ ⟨y = 0 ⊢ 0⟩, ⟨y = 1 ⊢ 1⟩ | false ⊢ error_empty ∅ ⟩ ⟩ + ⟨ ⟨ ⟨ ⟨y = 4 ⊢ ⟨4⟩⟩, ⟨y = 5 ⊢ ⟨5⟩⟩ | false ⊢ ∅ ⟩ + | true ⊢ ⟨ ⟨y = 2 ⊢ ⟨2⟩⟩, ⟨y = 3 ⊢ ⟨3⟩⟩ | false ⊢ ∅ ⟩ ⟩ + | true ⊢ ⟨ ⟨y = 0 ⊢ ⟨0⟩⟩, ⟨y = 1 ⊢ ⟨1⟩⟩ | false ⊢ ∅ ⟩ ⟩ + +let scope Test (x: integer|internal|output) = + let f.y : integer = error_empty ⟨ ⟨true ⊢ ⟨2⟩⟩ | false ⊢ ∅ ⟩; + call Foo[f]; + let x : integer = error_empty ⟨ ⟨true ⊢ ⟨f.x⟩⟩ | false ⊢ ∅ ⟩ ``` ```catala-test-inline diff --git a/tests/test_func/good/closure_conversion_reduce.catala_en b/tests/test_func/good/closure_conversion_reduce.catala_en index 9542bfe7..81ffb26a 100644 --- a/tests/test_func/good/closure_conversion_reduce.catala_en +++ b/tests/test_func/good/closure_conversion_reduce.catala_en @@ -94,7 +94,7 @@ let scope S ESome -1 y_2) ] (λ (_: unit) → ESome false) - (λ (_: unit) → ESome raise NoValueProvided)) + (λ (_: unit) → ENone ())) with | ENone _ → raise NoValueProvided | ESome y → y diff --git a/tests/test_io/good/all_io.catala_en b/tests/test_io/good/all_io.catala_en index 7a087aff..c6265e1f 100644 --- a/tests/test_io/good/all_io.catala_en +++ b/tests/test_io/good/all_io.catala_en @@ -33,22 +33,16 @@ let scope A let get d : integer = A_in.d_in in let get e : unit → ⟨integer⟩ = A_in.e_in in let get f : unit → ⟨integer⟩ = A_in.f_in in - let set a : integer = - error_empty ⟨ ⟨true ⊢ 0⟩ | false ⊢ error_empty ∅ ⟩ - in - let set b : integer = - error_empty ⟨ ⟨true ⊢ a + 1⟩ | false ⊢ error_empty ∅ ⟩ - in + let set a : integer = error_empty ⟨ ⟨true ⊢ ⟨0⟩⟩ | false ⊢ ∅ ⟩ in + let set b : integer = error_empty ⟨ ⟨true ⊢ ⟨a + 1⟩⟩ | false ⊢ ∅ ⟩ in let set e : integer = error_empty ⟨ e () - | true - ⊢ error_empty ⟨ ⟨true ⊢ b + c + d + 1⟩ | false ⊢ error_empty ∅ ⟩ ⟩ + | true ⊢ ⟨error_empty ⟨ ⟨true ⊢ ⟨b + c + d + 1⟩⟩ | false ⊢ ∅ ⟩⟩ ⟩ in let set f : integer = error_empty - ⟨ f () - | true ⊢ error_empty ⟨ ⟨true ⊢ e + 1⟩ | false ⊢ error_empty ∅ ⟩ ⟩ + ⟨ f () | true ⊢ ⟨error_empty ⟨ ⟨true ⊢ ⟨e + 1⟩⟩ | false ⊢ ∅ ⟩⟩ ⟩ in return { A b = b; d = d; f = f; } ``` diff --git a/tests/test_io/good/condition_only_input.catala_en b/tests/test_io/good/condition_only_input.catala_en index 64774332..087ee740 100644 --- a/tests/test_io/good/condition_only_input.catala_en +++ b/tests/test_io/good/condition_only_input.catala_en @@ -17,9 +17,7 @@ scope B: ```catala-test-inline $ catala Dcalc -s B let scope B (B_in: B_in): B = - let sub_set a.x : bool = - error_empty ⟨ ⟨true ⊢ false⟩ | false ⊢ error_empty ∅ ⟩ - in + let sub_set a.x : bool = error_empty ⟨ ⟨true ⊢ ⟨false⟩⟩ | false ⊢ ∅ ⟩ in let call result : A {y: integer} = A { A_in x_in = a.x; } in let sub_get a.y : integer = result.y in let assert _ : unit = assert ((a.y = 1)) in diff --git a/tests/test_io/good/subscope.catala_en b/tests/test_io/good/subscope.catala_en index 77fbb957..9432378f 100644 --- a/tests/test_io/good/subscope.catala_en +++ b/tests/test_io/good/subscope.catala_en @@ -24,9 +24,7 @@ scope B: $ catala Dcalc -s B let scope B (B_in: B_in): B = let sub_set a.a : unit → ⟨integer⟩ = λ (_: unit) → ∅ in - let sub_set a.b : integer = - error_empty ⟨ ⟨true ⊢ 2⟩ | false ⊢ error_empty ∅ ⟩ - in + let sub_set a.b : integer = error_empty ⟨ ⟨true ⊢ ⟨2⟩⟩ | false ⊢ ∅ ⟩ in let call result : A {c: integer} = A { A_in a_in = a.a; b_in = a.b; } in let sub_get a.c : integer = result.c in let assert _ : unit = assert ((a.c = 1)) in diff --git a/tests/test_modules/good/output/mod_def.ml b/tests/test_modules/good/output/mod_def.ml index c9668378..4a2d5a4e 100644 --- a/tests/test_modules/good/output/mod_def.ml +++ b/tests/test_modules/good/output/mod_def.ml @@ -38,12 +38,7 @@ let s (s_in: S_in.t) : S.t = end_line=0; end_column=1; law_headings=[]} ([||]) (fun (_: unit) -> true) (fun (_: unit) -> money_of_cents_string "100000"))|]) - (fun (_: unit) -> false) - (fun (_: unit) -> try (raise EmptyError) with - EmptyError -> (raise (NoValueProvided - {filename = "tests/test_modules/good/mod_def.catala_en"; - start_line=16; start_column=10; end_line=16; end_column=12; - law_headings=["Test modules + inclusions 1"]})))) + (fun (_: unit) -> false) (fun (_: unit) -> raise EmptyError)) with EmptyError -> (raise (NoValueProvided {filename = "tests/test_modules/good/mod_def.catala_en"; start_line=16; @@ -59,12 +54,7 @@ let s (s_in: S_in.t) : S.t = {filename = ""; start_line=0; start_column=1; end_line=0; end_column=1; law_headings=[]} ([||]) (fun (_: unit) -> true) (fun (_: unit) -> Enum1.Maybe ()))|]) - (fun (_: unit) -> false) - (fun (_: unit) -> try (raise EmptyError) with - EmptyError -> (raise (NoValueProvided - {filename = "tests/test_modules/good/mod_def.catala_en"; - start_line=17; start_column=10; end_line=17; end_column=12; - law_headings=["Test modules + inclusions 1"]})))) + (fun (_: unit) -> false) (fun (_: unit) -> raise EmptyError)) with EmptyError -> (raise (NoValueProvided {filename = "tests/test_modules/good/mod_def.catala_en"; start_line=17; diff --git a/tests/test_name_resolution/good/let_in2.catala_en b/tests/test_name_resolution/good/let_in2.catala_en index 277753e3..e26a3e82 100644 --- a/tests/test_name_resolution/good/let_in2.catala_en +++ b/tests/test_name_resolution/good/let_in2.catala_en @@ -65,11 +65,7 @@ let s (s_in: S_in.t) : S.t = in (let a_ : bool = (o_or a_ true) in a_))))|]) (fun (_: unit) -> false) - (fun (_: unit) -> try (raise EmptyError) with - EmptyError -> (raise (NoValueProvided - {filename = "tests/test_name_resolution/good/let_in2.catala_en"; - start_line=5; start_column=18; - end_line=5; end_column=19; law_headings=["Article"]})))) + (fun (_: unit) -> raise EmptyError)) with EmptyError -> (raise (NoValueProvided {filename = "tests/test_name_resolution/good/let_in2.catala_en"; diff --git a/tests/test_name_resolution/good/toplevel_defs.catala_en b/tests/test_name_resolution/good/toplevel_defs.catala_en index 3b02d0a7..15c81e23 100644 --- a/tests/test_name_resolution/good/toplevel_defs.catala_en +++ b/tests/test_name_resolution/good/toplevel_defs.catala_en @@ -114,10 +114,7 @@ let S2_6 (S2_in_11: S2_in) = try: decl temp_a_22 : any; let temp_a_22 (__23 : unit) = - try: - raise EmptyError - with EmptyError: - raise NoValueProvided; + raise EmptyError; decl temp_a_20 : any; let temp_a_20 (__21 : unit) = return false; @@ -143,10 +140,7 @@ let S3_7 (S3_in_24: S3_in) = try: decl temp_a_35 : any; let temp_a_35 (__36 : unit) = - try: - raise EmptyError - with EmptyError: - raise NoValueProvided; + raise EmptyError; decl temp_a_33 : any; let temp_a_33 (__34 : unit) = return false; @@ -172,10 +166,7 @@ let S4_8 (S4_in_37: S4_in) = try: decl temp_a_48 : any; let temp_a_48 (__49 : unit) = - try: - raise EmptyError - with EmptyError: - raise NoValueProvided; + raise EmptyError; decl temp_a_46 : any; let temp_a_46 (__47 : unit) = return false; @@ -201,10 +192,7 @@ let S_9 (S_in_50: S_in) = try: decl temp_a_73 : any; let temp_a_73 (__74 : unit) = - try: - raise EmptyError - with EmptyError: - raise NoValueProvided; + raise EmptyError; decl temp_a_71 : any; let temp_a_71 (__72 : unit) = return false; @@ -227,10 +215,7 @@ let S_9 (S_in_50: S_in) = try: decl temp_b_62 : any; let temp_b_62 (__63 : unit) = - try: - raise EmptyError - with EmptyError: - raise NoValueProvided; + raise EmptyError; decl temp_b_60 : any; let temp_b_60 (__61 : unit) = return false; @@ -435,15 +420,7 @@ glob2 = ( def s2(s2_in:S2In): try: def temp_a(_:Unit): - try: - raise EmptyError - except EmptyError: - raise NoValueProvided(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en", - start_line=37, - start_column=10, - end_line=37, - end_column=11, - law_headings=["Test toplevel function defs"])) + raise EmptyError def temp_a_1(_:Unit): return False def temp_a_2(_:Unit): @@ -471,15 +448,7 @@ def s2(s2_in:S2In): def s3(s3_in:S3In): try: def temp_a_6(_:Unit): - try: - raise EmptyError - except EmptyError: - raise NoValueProvided(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en", - start_line=57, - start_column=10, - end_line=57, - end_column=11, - law_headings=["Test function def with two args"])) + raise EmptyError def temp_a_7(_:Unit): return False def temp_a_8(_:Unit): @@ -508,15 +477,7 @@ def s3(s3_in:S3In): def s4(s4_in:S4In): try: def temp_a_12(_:Unit): - try: - raise EmptyError - except EmptyError: - raise NoValueProvided(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en", - start_line=80, - start_column=10, - end_line=80, - end_column=11, - law_headings=["Test inline defs in toplevel defs"])) + raise EmptyError def temp_a_13(_:Unit): return False def temp_a_14(_:Unit): @@ -543,15 +504,7 @@ def s4(s4_in:S4In): def s(s_in:SIn): try: def temp_a_18(_:Unit): - try: - raise EmptyError - except EmptyError: - raise NoValueProvided(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en", - start_line=7, - start_column=10, - end_line=7, - end_column=11, - law_headings=["Test basic toplevel values defs"])) + raise EmptyError def temp_a_19(_:Unit): return False def temp_a_20(_:Unit): @@ -575,15 +528,7 @@ def s(s_in:SIn): a_3 = temp_a_23 try: def temp_b(_:Unit): - try: - raise EmptyError - except EmptyError: - raise NoValueProvided(SourcePosition(filename="tests/test_name_resolution/good/toplevel_defs.catala_en", - start_line=8, - start_column=10, - end_line=8, - end_column=11, - law_headings=["Test basic toplevel values defs"])) + raise EmptyError def temp_b_1(_:Unit): return False def temp_b_2(_:Unit): diff --git a/tests/test_scope/good/scope_call3.catala_en b/tests/test_scope/good/scope_call3.catala_en index bc4c8f6b..b2c8b69e 100644 --- a/tests/test_scope/good/scope_call3.catala_en +++ b/tests/test_scope/good/scope_call3.catala_en @@ -32,7 +32,7 @@ $ catala Interpret -t -s HousingComputation --debug [DEBUG] Translating to default calculus... [DEBUG] Typechecking again... [DEBUG] Starting interpretation... -[LOG] ≔ HousingComputation.f: λ (x_90: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ (let result_91 : RentComputation = (#{→ RentComputation.direct} (λ (RentComputation_in_92: RentComputation_in) → let g_93 : integer → integer = #{≔ RentComputation.g} (λ (x1_94: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ x1_94 +! 1⟩ | false ⊢ error_empty ∅ ⟩) in let f_95 : integer → integer = #{≔ RentComputation.f} (λ (x1_96: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ #{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} g_93) #{≔ RentComputation.g.input0} (x1_96 +! 1)⟩ | false ⊢ error_empty ∅ ⟩) in { RentComputation f = f_95; })) #{≔ RentComputation.direct.input} {RentComputation_in} in let result1_97 : RentComputation = { RentComputation f = λ (param0_98: integer) → #{← RentComputation.f} #{≔ RentComputation.f.output} (#{→ RentComputation.f} result_91.f) #{≔ RentComputation.f.input0} param0_98; } in #{← RentComputation.direct} #{≔ RentComputation.direct.output} if #{☛ RentComputation.direct.output} true then result1_97 else result1_97).f x_90⟩ | false ⊢ error_empty ∅ ⟩ +[LOG] ≔ HousingComputation.f: λ (x_90: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨(let result_91 : RentComputation = (#{→ RentComputation.direct} (λ (RentComputation_in_92: RentComputation_in) → let g_93 : integer → integer = #{≔ RentComputation.g} (λ (x1_94: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x1_94 +! 1⟩⟩ | false ⊢ ∅ ⟩) in let f_95 : integer → integer = #{≔ RentComputation.f} (λ (x1_96: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨#{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} g_93) #{≔ RentComputation.g.input0} (x1_96 +! 1)⟩⟩ | false ⊢ ∅ ⟩) in { RentComputation f = f_95; })) #{≔ RentComputation.direct.input} {RentComputation_in} in let result1_97 : RentComputation = { RentComputation f = λ (param0_98: integer) → #{← RentComputation.f} #{≔ RentComputation.f.output} (#{→ RentComputation.f} result_91.f) #{≔ RentComputation.f.input0} param0_98; } in #{← RentComputation.direct} #{≔ RentComputation.direct.output} if #{☛ RentComputation.direct.output} true then result1_97 else result1_97).f x_90⟩⟩ | false ⊢ ∅ ⟩ [LOG] ☛ Definition applied: ┌─⯈ tests/test_scope/good/scope_call3.catala_en:8.14-8.20: └─┐ @@ -47,14 +47,14 @@ $ catala Interpret -t -s HousingComputation --debug │ ‾ [LOG] → RentComputation.direct [LOG] ≔ RentComputation.direct.input: {RentComputation_in} -[LOG] ≔ RentComputation.g: λ (x_99: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ x_99 +! 1⟩ | false ⊢ error_empty ∅ ⟩ -[LOG] ≔ RentComputation.f: λ (x_100: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ #{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} (λ (x1_101: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ x1_101 +! 1⟩ | false ⊢ error_empty ∅ ⟩)) #{≔ RentComputation.g.input0} (x_100 +! 1)⟩ | false ⊢ error_empty ∅ ⟩ +[LOG] ≔ RentComputation.g: λ (x_99: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x_99 +! 1⟩⟩ | false ⊢ ∅ ⟩ +[LOG] ≔ RentComputation.f: λ (x_100: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨#{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} (λ (x1_101: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x1_101 +! 1⟩⟩ | false ⊢ ∅ ⟩)) #{≔ RentComputation.g.input0} (x_100 +! 1)⟩⟩ | false ⊢ ∅ ⟩ [LOG] ☛ Definition applied: ┌─⯈ tests/test_scope/good/scope_call3.catala_en:7.29-7.54: └─┐ 7 │ definition f of x equals (output of RentComputation).f of x │ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾ -[LOG] ≔ RentComputation.direct.output: { RentComputation f = λ (param0_102: integer) → #{← RentComputation.f} #{≔ RentComputation.f.output} (#{→ RentComputation.f} { RentComputation f = λ (x_103: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ #{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} (λ (x1_104: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ x1_104 +! 1⟩ | false ⊢ error_empty ∅ ⟩)) #{≔ RentComputation.g.input0} (x_103 +! 1)⟩ | false ⊢ error_empty ∅ ⟩; }.f) #{≔ RentComputation.f.input0} param0_102; } +[LOG] ≔ RentComputation.direct.output: { RentComputation f = λ (param0_102: integer) → #{← RentComputation.f} #{≔ RentComputation.f.output} (#{→ RentComputation.f} { RentComputation f = λ (x_103: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨#{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} (λ (x1_104: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x1_104 +! 1⟩⟩ | false ⊢ ∅ ⟩)) #{≔ RentComputation.g.input0} (x_103 +! 1)⟩⟩ | false ⊢ ∅ ⟩; }.f) #{≔ RentComputation.f.input0} param0_102; } [LOG] ← RentComputation.direct [LOG] → RentComputation.f [LOG] ≔ RentComputation.f.input0: 1 @@ -83,25 +83,25 @@ $ catala Interpret -t -s HousingComputation --debug f = λ (x: integer) → error_empty ⟨ ⟨true - ⊢ (let result : RentComputation = - (λ (RentComputation_in: RentComputation_in) → - let g : integer → integer = - λ (x1: integer) → - error_empty ⟨ ⟨true ⊢ x1 + 1⟩ | false ⊢ error_empty ∅ ⟩ - in - let f : integer → integer = - λ (x1: integer) → - error_empty ⟨ ⟨true ⊢ g (x1 + 1)⟩ | false ⊢ error_empty ∅ ⟩ - in - { RentComputation f = f; }) - {RentComputation_in} - in - let result1 : RentComputation = - { RentComputation f = λ (param0: integer) → result.f param0; } - in - if true then result1 else result1). - f - x⟩ - | false ⊢ error_empty ∅ ⟩ + ⊢ ⟨(let result : RentComputation = + (λ (RentComputation_in: RentComputation_in) → + let g : integer → integer = + λ (x1: integer) → + error_empty ⟨ ⟨true ⊢ ⟨x1 + 1⟩⟩ | false ⊢ ∅ ⟩ + in + let f : integer → integer = + λ (x1: integer) → + error_empty ⟨ ⟨true ⊢ ⟨g (x1 + 1)⟩⟩ | false ⊢ ∅ ⟩ + in + { RentComputation f = f; }) + {RentComputation_in} + in + let result1 : RentComputation = + { RentComputation f = λ (param0: integer) → result.f param0; } + in + if true then result1 else result1). + f + x⟩⟩ + | false ⊢ ∅ ⟩ [RESULT] result = 3 ``` diff --git a/tests/test_scope/good/scope_call4.catala_en b/tests/test_scope/good/scope_call4.catala_en index 39d137a0..d714d486 100644 --- a/tests/test_scope/good/scope_call4.catala_en +++ b/tests/test_scope/good/scope_call4.catala_en @@ -44,16 +44,16 @@ $ catala Interpret -s RentComputation --debug f1 = λ (x: integer) → error_empty ⟨ ⟨true - ⊢ let x1 : integer = x + 1 in - error_empty ⟨ ⟨true ⊢ x1 + 1⟩ | false ⊢ error_empty ∅ ⟩⟩ - | false ⊢ error_empty ∅ ⟩ + ⊢ ⟨let x1 : integer = x + 1 in + error_empty ⟨ ⟨true ⊢ ⟨x1 + 1⟩⟩ | false ⊢ ∅ ⟩⟩⟩ + | false ⊢ ∅ ⟩ [RESULT] f2 = λ (x: integer) → error_empty ⟨ ⟨true - ⊢ let x1 : integer = x + 1 in - error_empty ⟨ ⟨true ⊢ x1 + 1⟩ | false ⊢ error_empty ∅ ⟩⟩ - | false ⊢ error_empty ∅ ⟩ + ⊢ ⟨let x1 : integer = x + 1 in + error_empty ⟨ ⟨true ⊢ ⟨x1 + 1⟩⟩ | false ⊢ ∅ ⟩⟩⟩ + | false ⊢ ∅ ⟩ ``` ```catala-test-inline diff --git a/tests/test_scope/good/simple.catala_en b/tests/test_scope/good/simple.catala_en index 49affb6a..998e7aae 100644 --- a/tests/test_scope/good/simple.catala_en +++ b/tests/test_scope/good/simple.catala_en @@ -17,8 +17,7 @@ let scope Foo (Foo_in: Foo_in): Foo {bar: integer} = [ λ (_: unit) → handle_default [ ] (λ (_1: unit) → true) (λ (_1: unit) → 0) ] (λ (_: unit) → false) - (λ (_: unit) → - try raise EmptyError with EmptyError -> raise NoValueProvided) + (λ (_: unit) → raise EmptyError) with EmptyError -> raise NoValueProvided in return { Foo bar = bar; } diff --git a/tests/test_variable_state/good/subscope.catala_en b/tests/test_variable_state/good/subscope.catala_en index c9b16de5..232892c9 100644 --- a/tests/test_variable_state/good/subscope.catala_en +++ b/tests/test_variable_state/good/subscope.catala_en @@ -35,11 +35,11 @@ $ catala Scopelang -s A let scope A (foo_bar: ⟨integer⟩|context) (foo_baz: integer|internal) (foo_fizz: integer|internal|output) = let foo_bar : integer = reentrant or by default - error_empty ⟨ ⟨true ⊢ 1⟩ | false ⊢ error_empty ∅ ⟩; + error_empty ⟨ ⟨true ⊢ ⟨1⟩⟩ | false ⊢ ∅ ⟩; let foo_baz : integer = - error_empty ⟨ ⟨true ⊢ foo_bar + 1⟩ | false ⊢ error_empty ∅ ⟩; + error_empty ⟨ ⟨true ⊢ ⟨foo_bar + 1⟩⟩ | false ⊢ ∅ ⟩; let foo_fizz : integer = - error_empty ⟨ ⟨true ⊢ foo_baz + 1⟩ | false ⊢ error_empty ∅ ⟩ + error_empty ⟨ ⟨true ⊢ ⟨foo_baz + 1⟩⟩ | false ⊢ ∅ ⟩ ``` ```catala-test-inline