diff --git a/compiler/dcalc/invariants.ml b/compiler/dcalc/invariants.ml index b9f0a04b..80e40438 100644 --- a/compiler/dcalc/invariants.ml +++ b/compiler/dcalc/invariants.ml @@ -93,8 +93,7 @@ let invariant_app_inversion () : string * invariant_expr = fun _ctx e -> match Mark.remove e with | EApp { f = EAbs { binder; _ }, _; args; _ } -> - if Bindlib.mbinder_arity binder = 1 && List.length args = 1 then Pass - else Fail + if Bindlib.mbinder_arity binder = List.length args then Pass else Fail | EApp { f = EVar _, _; _ } -> Pass | EApp { f = EStructAccess _, _; _ } -> Pass | EApp { f = EExternal _, _; _ } -> Pass diff --git a/compiler/desugared/from_surface.ml b/compiler/desugared/from_surface.ml index a56f753c..01d618bd 100644 --- a/compiler/desugared/from_surface.ml +++ b/compiler/desugared/from_surface.ml @@ -35,11 +35,15 @@ module Runtime = Runtime_ocaml.Runtime Shared_ast.Operator} for detail. *) let translate_binop : - S.binop -> Pos.t -> Ast.expr boxed -> Ast.expr boxed -> Ast.expr boxed = - fun op pos lhs rhs -> + S.binop Mark.pos -> + Pos.t -> + Ast.expr boxed -> + Ast.expr boxed -> + Ast.expr boxed = + fun (op, op_pos) pos lhs rhs -> let op_expr op tys = Expr.eappop ~op - ~tys:(List.map (Mark.add pos) tys) + ~tys:(List.map (Mark.add op_pos) tys) ~args:[lhs; rhs] (Untyped { pos }) in @@ -73,7 +77,7 @@ let translate_binop : | S.KDec -> [TLit TRat; TLit TRat] | S.KMoney -> [TLit TMoney; TLit TRat] | S.KDate -> - Message.raise_spanned_error pos + Message.raise_spanned_error op_pos "This operator doesn't exist, dates can't be multiplied" | S.KDuration -> [TLit TDuration; TLit TInt]) | S.Div k -> @@ -84,7 +88,7 @@ let translate_binop : | S.KDec -> [TLit TRat; TLit TRat] | S.KMoney -> [TLit TMoney; TLit TMoney] | S.KDate -> - Message.raise_spanned_error pos + Message.raise_spanned_error op_pos "This operator doesn't exist, dates can't be divided" | S.KDuration -> [TLit TDuration; TLit TDuration]) | S.Lt k | S.Lte k | S.Gt k | S.Gte k -> @@ -106,11 +110,11 @@ let translate_binop : op_expr Eq [TAny; TAny] (* This is a truly polymorphic operator, not an overload *) | S.Neq -> assert false (* desugared already *) - | S.Concat -> op_expr Concat [TArray (TAny, pos); TArray (TAny, pos)] + | S.Concat -> op_expr Concat [TArray (TAny, op_pos); TArray (TAny, op_pos)] -let translate_unop (op : S.unop) pos arg : Ast.expr boxed = +let translate_unop ((op, op_pos) : S.unop Mark.pos) pos arg : Ast.expr boxed = let op_expr op ty = - Expr.eappop ~op ~tys:[Mark.add pos ty] ~args:[arg] (Untyped { pos }) + Expr.eappop ~op ~tys:[Mark.add op_pos ty] ~args:[arg] (Untyped { pos }) in match op with | S.Not -> op_expr Not (TLit TBool) @@ -122,7 +126,7 @@ let translate_unop (op : S.unop) pos arg : Ast.expr boxed = | S.KDec -> TLit TRat | S.KMoney -> TLit TMoney | S.KDate -> - Message.raise_spanned_error pos + Message.raise_spanned_error op_pos "This operator doesn't exist, dates can't be negative" | S.KDuration -> TLit TDuration) @@ -257,17 +261,15 @@ let rec translate_expr | Binop ((((S.And | S.Or | S.Xor), _) as op), e1, e2) -> check_formula op e1; check_formula op e2; - translate_binop (Mark.remove op) (Mark.get op) (rec_helper e1) - (rec_helper e2) + translate_binop op pos (rec_helper e1) (rec_helper e2) | IfThenElse (e_if, e_then, e_else) -> Expr.eifthenelse (rec_helper e_if) (rec_helper e_then) (rec_helper e_else) emark | Binop ((S.Neq, posn), e1, e2) -> (* Neq is just sugar *) rec_helper (Unop ((S.Not, posn), (Binop ((S.Eq, posn), e1, e2), posn)), pos) - | Binop ((op, pos), e1, e2) -> - translate_binop op pos (rec_helper e1) (rec_helper e2) - | Unop ((op, pos), e) -> translate_unop op pos (rec_helper e) + | Binop (op, e1, e2) -> translate_binop op pos (rec_helper e1) (rec_helper e2) + | Unop (op, e) -> translate_unop op pos (rec_helper e) | Literal l -> let lit = match l with @@ -693,7 +695,8 @@ let rec translate_expr let acc = Expr.make_var acc_var (Untyped { pos = Mark.get param0 }) in Expr.eabs (Expr.bind [| acc_var; param |] - (translate_binop op pos acc (rec_helper ~local_vars predicate))) + (translate_binop (op, pos) pos acc + (rec_helper ~local_vars predicate))) [TAny, pos; TAny, pos] emark in @@ -711,7 +714,7 @@ let rec translate_expr let x1 = Expr.make_var v1 emark in let x2 = Expr.make_var v2 emark in Expr.make_abs [| v1; v2 |] - (Expr.eifthenelse (translate_binop op pos x1 x2) x1 x2 emark) + (Expr.eifthenelse (translate_binop (op, pos) pos x1 x2) x1 x2 emark) [TAny, pos; TAny, pos] pos in @@ -741,7 +744,7 @@ let rec translate_expr let x1 = Expr.make_var v1 emark in let x2 = Expr.make_var v2 emark in Expr.make_abs [| v1; v2 |] - (translate_binop (S.Add KPoly) pos x1 x2) + (translate_binop (S.Add KPoly, pos) pos x1 x2) [TAny, pos; TAny, pos] pos in @@ -1289,7 +1292,6 @@ let process_topdef let translate_typ t = Name_resolution.process_type ctxt t in let translate_tbase (tbase, m) = translate_typ (Base tbase, m) in let typ = translate_typ def.S.topdef_type in - Message.emit_debug "TTYP: %a@." Print.typ_debug typ; let expr_opt = match def.S.topdef_expr, def.S.topdef_args with | None, _ -> None @@ -1314,9 +1316,6 @@ let process_topdef please name the individual arguments" | _ -> () in - Message.emit_debug "TTYPSS: %a@." - (Format.pp_print_list Print.typ_debug) - (List.map translate_tbase tys); let e = Expr.make_abs (Array.of_list (List.map Mark.remove args)) diff --git a/compiler/shared_ast/typing.mli b/compiler/shared_ast/typing.mli index 7fa6d885..a68e2392 100644 --- a/compiler/shared_ast/typing.mli +++ b/compiler/shared_ast/typing.mli @@ -61,12 +61,20 @@ val expr : filling the gaps ([TAny]) if any. Use [Expr.untype] first if this is not what you want. - Note that typing also transparently performs + Note that typing also transparently performs the following changes to the + AST nodes, outside of typing annotations: - disambiguation of constructors: [EDStructAccess] nodes are translated into [EStructAccess] with the suitable structure and field idents (this only concerns [desugared] expressions). - resolution of operator types, which are stored (monomorphised) back in the - AST nodes *) + [EAppOp] nodes + - resolution of function application input types on the [EApp] nodes, when + that was originally empty ([[]]): this documents the arity of the function + application, taking de-tuplification into account. + - [TAny] appearing within nodes are refined to more precise types, e.g. on + `EAbs` nodes (but be careful with this, it may only work for specific + structures of generated code ; [~leave_unresolved:false] checks that it + didn't cause problems) *) val check_expr : leave_unresolved:bool -> diff --git a/tests/test_arithmetic/bad/division_by_zero.catala_en b/tests/test_arithmetic/bad/division_by_zero.catala_en index 828f8467..c0c7352b 100644 --- a/tests/test_arithmetic/bad/division_by_zero.catala_en +++ b/tests/test_arithmetic/bad/division_by_zero.catala_en @@ -37,10 +37,10 @@ $ catala Interpret -s Dec division by zero at runtime The division operator: -┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:20.26-20.27: +┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:20.23-20.30: └──┐ 20 │ definition i equals 1. / 0. - │ ‾ + │ ‾‾‾‾‾‾‾ └┬ `Division_by_zero` exception management └─ with decimals @@ -60,10 +60,10 @@ $ catala Interpret -s Int division by zero at runtime The division operator: -┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:10.25-10.26: +┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:10.23-10.28: └──┐ 10 │ definition i equals 1 / 0 - │ ‾ + │ ‾‾‾‾‾ └┬ `Division_by_zero` exception management └─ with integers @@ -83,10 +83,10 @@ $ catala Interpret -s Money division by zero at runtime The division operator: -┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:30.29-30.30: +┌─⯈ tests/test_arithmetic/bad/division_by_zero.catala_en:30.23-30.35: └──┐ 30 │ definition i equals $10.0 / $0.0 - │ ‾ + │ ‾‾‾‾‾‾‾‾‾‾‾‾ └┬ `Division_by_zero` exception management └─ with money diff --git a/tests/test_array/bad/fold_error.catala_en b/tests/test_array/bad/fold_error.catala_en index c4169ada..b7309aa5 100644 --- a/tests/test_array/bad/fold_error.catala_en +++ b/tests/test_array/bad/fold_error.catala_en @@ -16,10 +16,10 @@ $ catala Interpret -s A I don't know how to apply operator >= on types integer and money -┌─⯈ tests/test_array/bad/fold_error.catala_en:10.50-10.52: +┌─⯈ tests/test_array/bad/fold_error.catala_en:10.48-10.55: └──┐ 10 │ definition list_high_count equals number of (m >= $7) for m among list - │ ‾‾ + │ ‾‾‾‾‾‾‾ └─ Article Type integer coming from expression: diff --git a/tests/test_func/bad/bad_func.catala_en b/tests/test_func/bad/bad_func.catala_en index 1e109048..8df80939 100644 --- a/tests/test_func/bad/bad_func.catala_en +++ b/tests/test_func/bad/bad_func.catala_en @@ -33,17 +33,17 @@ $ catala Interpret -s S There is a conflict between multiple valid consequences for assigning the same variable. This consequence has a valid justification: -┌─⯈ tests/test_func/bad/bad_func.catala_en:14.67-14.68: +┌─⯈ tests/test_func/bad/bad_func.catala_en:14.65-14.70: └──┐ 14 │ definition f of x under condition (x >= x) consequence equals x + x - │ ‾ + │ ‾‾‾‾‾ └─ Article This consequence has a valid justification: -┌─⯈ tests/test_func/bad/bad_func.catala_en:15.64-15.65: +┌─⯈ tests/test_func/bad/bad_func.catala_en:15.62-15.67: └──┐ 15 │ definition f of x under condition not b consequence equals x * x - │ ‾ + │ ‾‾‾‾‾ └─ Article #return code 123# ``` diff --git a/tests/test_money/bad/no_mingle.catala_en b/tests/test_money/bad/no_mingle.catala_en index f3b5760e..0fa32b57 100644 --- a/tests/test_money/bad/no_mingle.catala_en +++ b/tests/test_money/bad/no_mingle.catala_en @@ -18,10 +18,10 @@ $ catala Interpret -s A I don't know how to apply operator * on types money and money -┌─⯈ tests/test_money/bad/no_mingle.catala_en:12.26-12.27: +┌─⯈ tests/test_money/bad/no_mingle.catala_en:12.24-12.29: └──┐ 12 │ definition z equals (x * y) - │ ‾ + │ ‾‾‾‾‾ └─ Article Type money coming from expression: diff --git a/tests/test_tuples/good/tuples.catala_en b/tests/test_tuples/good/tuples.catala_en index 49294541..b0d064d4 100644 --- a/tests/test_tuples/good/tuples.catala_en +++ b/tests/test_tuples/good/tuples.catala_en @@ -32,7 +32,13 @@ scope Test: ``` ```catala-test-inline -$ catala typecheck +$ catala typecheck --check-invariants +[RESULT] Invariant typing_defaults checked. result: [59/59] +[RESULT] Invariant match_inversion checked. result: [1/1] +[RESULT] Invariant app_inversion checked. result: [6/6] +[RESULT] Invariant no_return_a_function checked. result: [8/8] +[RESULT] Invariant no_partial_evaluation checked. result: [6/6] +[RESULT] Invariant default_no_arrow checked. result: [2/2] [RESULT] Typechecking successful! ``` @@ -41,3 +47,9 @@ $ catala interpret -s Test [RESULT] Computation successful! Results: [RESULT] o = [2001-01-03; 6.0] ``` + +```catala-test-inline +$ catala interpret_lcalc -s Test +[RESULT] Computation successful! Results: +[RESULT] o = [2001-01-03; 6.0] +``` diff --git a/tests/test_typing/bad/err3.catala_en b/tests/test_typing/bad/err3.catala_en index 76aecd5e..b7424a6c 100644 --- a/tests/test_typing/bad/err3.catala_en +++ b/tests/test_typing/bad/err3.catala_en @@ -24,10 +24,10 @@ Error during typechecking, incompatible types: └─⯈ decimal This expression has type integer: -┌─⯈ tests/test_typing/bad/err3.catala_en:10.42-10.43: +┌─⯈ tests/test_typing/bad/err3.catala_en:10.23-10.45: └──┐ 10 │ definition a equals number of (z ++ z) * 2 - │ ‾ + │ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾ Expected type decimal coming from expression: ┌─⯈ tests/test_typing/bad/common.catala_en:15.20-15.27: @@ -53,10 +53,10 @@ Error during typechecking, incompatible types: └─⯈ decimal This expression has type integer: -┌─⯈ tests/test_typing/bad/err3.catala_en:10.42-10.43: +┌─⯈ tests/test_typing/bad/err3.catala_en:10.23-10.45: └──┐ 10 │ definition a equals number of (z ++ z) * 2 - │ ‾ + │ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾ Expected type decimal coming from expression: ┌─⯈ tests/test_typing/bad/common.catala_en:15.20-15.27: