Merge pull request #1095 from daniel-larraz/expand-types

Expand nested types and types of call arguments

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

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)

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

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