Skip to content

Commit

Permalink
Expand nested types
Browse files Browse the repository at this point in the history
  • Loading branch information
daniel-larraz committed Aug 29, 2024
1 parent 5243956 commit db97edc
Show file tree
Hide file tree
Showing 2 changed files with 43 additions and 3 deletions.
20 changes: 17 additions & 3 deletions src/lustre/typeCheckerContext.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
26 changes: 26 additions & 0 deletions tests/regression/success/expand_nested_types.lus
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit db97edc

Please sign in to comment.