From 5243956434c3de7a787fe31857e96cfca1e897e0 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Thu, 29 Aug 2024 10:31:58 -0500 Subject: [PATCH 1/2] Expand types of call arguments and output --- src/lustre/lustreTypeChecker.ml | 1 + .../success/expand_type_call_arg.lus | 23 +++++++++++++++++++ 2 files changed, 24 insertions(+) create mode 100644 tests/regression/success/expand_type_call_arg.lus diff --git a/src/lustre/lustreTypeChecker.ml b/src/lustre/lustreTypeChecker.ml index 6c81b4db5..efc74dc8a 100644 --- a/src/lustre/lustreTypeChecker.ml +++ b/src/lustre/lustreTypeChecker.ml @@ -915,6 +915,7 @@ let rec infer_type_expr: tc_context -> HString.t option -> LA.expr -> (tc_type * | _ -> assert false in let* given_arg_tys, warnings2 = infer_type_node_args ctx arg_exprs in + let given_arg_tys = expand_type_syn ctx given_arg_tys in let* are_equal = eq_lustre_type ctx exp_arg_tys given_arg_tys in if are_equal then (check_constant_args ctx i arg_exprs >> (R.ok (exp_ret_tys, List.flatten warnings1 @ warnings2))) diff --git a/tests/regression/success/expand_type_call_arg.lus b/tests/regression/success/expand_type_call_arg.lus new file mode 100644 index 000000000..1475bc2e4 --- /dev/null +++ b/tests/regression/success/expand_type_call_arg.lus @@ -0,0 +1,23 @@ + +type Nat = subrange [0,*] of int; + +type D = subtype { i:Nat | i < 10 }; + +type R1 = struct { + f1: D; +}; + +type R2 = struct { + r1: R1; +}; + +function F2(r1: R1) returns (ok:bool); +let + ok = r1.f1 < 10; +tel + +function F1(m: R2) returns (ok:bool); +let + ok = F2(m.r1); + check ok; +tel \ No newline at end of file From db97edcc7540801957170a996fcece2d0fa33388 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Thu, 29 Aug 2024 11:00:42 -0500 Subject: [PATCH 2/2] Expand nested types --- src/lustre/typeCheckerContext.ml | 20 +++++++++++--- .../success/expand_nested_types.lus | 26 +++++++++++++++++++ 2 files changed, 43 insertions(+), 3 deletions(-) create mode 100644 tests/regression/success/expand_nested_types.lus diff --git a/src/lustre/typeCheckerContext.ml b/src/lustre/typeCheckerContext.ml index d4b98feec..3d80920e5 100644 --- a/src/lustre/typeCheckerContext.ml +++ b/src/lustre/typeCheckerContext.ml @@ -167,10 +167,24 @@ let rec lookup_ty_syn: tc_context -> LA.ident -> tc_type list -> tc_type option let rec expand_type_syn: tc_context -> tc_type -> tc_type = fun ctx -> function - | UserType (_, ty_args, i) as ty -> - (match lookup_ty_syn ctx i ty_args with + | UserType (_, ty_args, i) as ty -> ( + match IMap.find_opt i (ctx.ty_syns) with | None -> ty - | Some ty' -> ty') + | Some ty -> ( + match ty with + | UserType (_, _, uid) when uid = i -> ty + | _ -> ( + let ty_vars = + match IMap.find_opt i (ctx.ty_ty_vars) with + | Some ps -> ps + | None -> [] + in + let sigma = List.combine ty_vars ty_args in + let ty = LustreAstHelpers.apply_type_subst_in_type sigma ty in + expand_type_syn ctx ty + ) + ) + ) | TupleType (p, tys) -> let tys = List.map (expand_type_syn ctx) tys in TupleType (p, tys) diff --git a/tests/regression/success/expand_nested_types.lus b/tests/regression/success/expand_nested_types.lus new file mode 100644 index 000000000..eb7a4dde0 --- /dev/null +++ b/tests/regression/success/expand_nested_types.lus @@ -0,0 +1,26 @@ +type Nat = subrange [0,*] of int; + +type D = subtype { i: Nat | i < 10 }; + +type R1 = struct { + f1: D; +}; + +type R2 = struct { + r1: R1; +}; + +type R3 = struct { + r2: R2; +}; + +function F2(r2: R2) returns (ok: bool); +let + ok = r2.r1.f1 < 10; +tel + +function F1(r3: R3) returns (ok: bool); +let + ok = F2(r3.r2); + check ok; +tel \ No newline at end of file