CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-19 00:15:39 +03:00
Code Issues Projects Releases Wiki Activity

Adding tuples: fixes following review

Browse Source
This commit is contained in:
Louis Gesbert 2024-01-08 12:09:12 +01:00
parent d3e7c565a9
commit 12f208b3fc
9 changed files with 62 additions and 44 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
compiler/dcalc/invariants.ml
View File

@ -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

41
compiler/desugared/from_surface.ml
View File

@ -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))

12
compiler/shared_ast/typing.mli
View File

@ -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 ->

12
tests/test_arithmetic/bad/division_by_zero.catala_en
View File

@ -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

4
tests/test_array/bad/fold_error.catala_en
View File

@ -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:

8
tests/test_func/bad/bad_func.catala_en
View File

@ -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#
```

4
tests/test_money/bad/no_mingle.catala_en
View File

@ -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:

14
tests/test_tuples/good/tuples.catala_en
View File

@ -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]
```

8
tests/test_typing/bad/err3.catala_en
View File

@ -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: