Fix typing upon detuplification

This commit is contained in:
Louis Gesbert 2023-12-19 14:44:01 +01:00
parent a2efc94fd2
commit 5384394a72
3 changed files with 32 additions and 8 deletions

View File

@ -786,10 +786,22 @@ and typecheck_expr_top_down :
List.map2 (typecheck_expr_top_down ~leave_unresolved ctx env) t_args args List.map2 (typecheck_expr_top_down ~leave_unresolved ctx env) t_args args
in in
let t_args = let t_args =
match t_args with match t_args, tys with
| [t] -> ( | [t], [] -> (
(* Handles typing before detuplification: if [tys] was not yet set, we
are allowed to destruct a tuple into multiple arguments (see
[Scopelang.from_desugared] for the corresponding code
transformation) *)
match UnionFind.get t with TTuple tys, _ -> tys | _ -> t_args) match UnionFind.get t with TTuple tys, _ -> tys | _ -> t_args)
| _ -> t_args | _ ->
if List.length t_args <> List.length args' then
Message.raise_spanned_error (Expr.pos e)
(match e1 with
| EAbs _, _ -> "This binds %d variables, but %d were provided."
| _ -> "This function application has %d arguments, but expects %d.")
(List.length t_args) (List.length args');
t_args
in in
let t_func = unionfind ~pos:e1 (TArrow (t_args, tau)) in let t_func = unionfind ~pos:e1 (TArrow (t_args, tau)) in
let e1' = typecheck_expr_top_down ~leave_unresolved ctx env t_func e1 in let e1' = typecheck_expr_top_down ~leave_unresolved ctx env t_func e1 in

View File

@ -55,7 +55,7 @@ $ catala Typecheck --check-invariants
```catala-test-inline ```catala-test-inline
$ catala Lcalc --avoid-exceptions -O --closure-conversion $ catala Lcalc --avoid-exceptions -O --closure-conversion
type Eoption = | ENone of unit | ESome of any
type Result = { type Result = {
r: ((closure_env, integer) → integer * closure_env); r: ((closure_env, integer) → integer * closure_env);
@ -76,7 +76,7 @@ type SubFoo2 = {
y: ((closure_env, integer) → integer * closure_env); y: ((closure_env, integer) → integer * closure_env);
} }
type Foo_in = { b_in: ((any, unit) → eoption bool * any); } type Foo_in = { b_in: ((closure_env, unit) → eoption bool * closure_env); }
type Foo = { z: integer; } type Foo = { z: integer; }
@ -125,10 +125,13 @@ let topval closure_r : (closure_env, integer) → integer =
in in
code_and_env.0 code_and_env.1 param0 code_and_env.0 code_and_env.1 param0
let scope Foo let scope Foo
(Foo_in: Foo_in {b_in: ((any, unit) → eoption bool * any)}) (Foo_in:
Foo_in {b_in: ((closure_env, unit) → eoption bool * closure_env)})
: Foo {z: integer} : Foo {z: integer}
= =
let get b : ((any, unit) → eoption bool * any) = Foo_in.b_in in let get b : ((closure_env, unit) → eoption bool * closure_env) =
Foo_in.b_in
in
let set b : bool = let set b : bool =
match match
(handle_default_opt (handle_default_opt

View File

@ -31,4 +31,13 @@ scope Test:
f2 of str, Two content (12, str)) f2 of str, Two content (12, str))
``` ```
Test in progress ```catala-test-inline
$ catala typecheck
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala interpret -s Test
[RESULT] Computation successful! Results:
[RESULT] o = [2001-01-03; 6.0]
```