From 93d36f107e97697140ea049c753905ba84a00003 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Fri, 1 Dec 2023 14:33:55 -0600 Subject: [PATCH 1/7] When type checking node calls, consider everything in the same context --- src/lustre/lustreAstHelpers.ml | 71 ++++++++++++++++++++++++ src/lustre/lustreAstHelpers.mli | 6 ++ src/lustre/lustreTypeChecker.ml | 68 +++++++++++++++++++---- tests/ounit/lustre/testLustreFrontend.ml | 8 +-- 4 files changed, 138 insertions(+), 15 deletions(-) diff --git a/src/lustre/lustreAstHelpers.ml b/src/lustre/lustreAstHelpers.ml index d66e6d9c1..d461e5bbb 100644 --- a/src/lustre/lustreAstHelpers.ml +++ b/src/lustre/lustreAstHelpers.ml @@ -168,6 +168,77 @@ let rec substitute_naive (var:HString.t) t = function | Call (pos, id, expr_list) -> Call (pos, id, List.map (fun e -> substitute_naive var t e) expr_list) +(* Substitute t for var. ChooseOp and Quantifier are not supported due to introduction of bound variables. *) +let rec substitute_naive_list (var:HString.t list) (t:expr list) = function + | Ident (pos, i) -> ( + match List.assoc_opt i (List.combine var t) with + | Some expr -> expr + | None -> Ident (pos, i) + ) + | ModeRef (_, _) as e -> e + | RecordProject (pos, e, idx) -> RecordProject (pos, substitute_naive_list var t e, idx) + | TupleProject (pos, e, idx) -> TupleProject (pos, substitute_naive_list var t e, idx) + | Const (_, _) as e -> e + | UnaryOp (pos, op, e) -> UnaryOp (pos, op, substitute_naive_list var t e) + | BinaryOp (pos, op, e1, e2) -> + BinaryOp (pos, op, substitute_naive_list var t e1, substitute_naive_list var t e2) + | TernaryOp (pos, op, e1, e2, e3) -> + TernaryOp (pos, op, substitute_naive_list var t e1, substitute_naive_list var t e2, substitute_naive_list var t e3) + | ConvOp (pos, op, e) -> ConvOp (pos, op, substitute_naive_list var t e) + | CompOp (pos, op, e1, e2) -> + CompOp (pos, op, substitute_naive_list var t e1, substitute_naive_list var t e2) + | AnyOp _ -> assert false (* Not supported due to introduction of bound variables *) + | Quantifier _ -> assert false (* Not supported due to introduction of bound variables *) + | RecordExpr (pos, ident, expr_list) -> + RecordExpr (pos, ident, List.map (fun (i, e) -> (i, substitute_naive_list var t e)) expr_list) + | GroupExpr (pos, kind, expr_list) -> + GroupExpr (pos, kind, List.map (fun e -> substitute_naive_list var t e) expr_list) + | StructUpdate (pos, e1, idx, e2) -> + StructUpdate (pos, substitute_naive_list var t e1, idx, substitute_naive_list var t e2) + | ArrayConstr (pos, e1, e2) -> + ArrayConstr (pos, substitute_naive_list var t e1, substitute_naive_list var t e2) + | ArrayIndex (pos, e1, e2) -> + ArrayIndex (pos, substitute_naive_list var t e1, substitute_naive_list var t e2) + | When (pos, e, clock) -> When (pos, substitute_naive_list var t e, clock) + | Condact (pos, e1, e2, id, expr_list1, expr_list2) -> + let e1, e2 = substitute_naive_list var t e1, substitute_naive_list var t e2 in + let expr_list1 = List.map (fun e -> substitute_naive_list var t e) expr_list1 in + let expr_list2 = List.map (fun e -> substitute_naive_list var t e) expr_list2 in + Condact (pos, e1, e2, id, expr_list1, expr_list2) + | Activate (pos, ident, e1, e2, expr_list) -> + let e1, e2 = substitute_naive_list var t e1, substitute_naive_list var t e2 in + let expr_list = List.map (fun e -> substitute_naive_list var t e) expr_list in + Activate (pos, ident, e1, e2, expr_list) + | Merge (pos, ident, expr_list) -> + Merge (pos, ident, List.map (fun (i, e) -> (i, substitute_naive_list var t e)) expr_list) + | RestartEvery (pos, ident, expr_list, e) -> + let expr_list = List.map (fun e -> substitute_naive_list var t e) expr_list in + let e = substitute_naive_list var t e in + RestartEvery (pos, ident, expr_list, e) + | Pre (pos, e) -> Pre (pos, substitute_naive_list var t e) + | Arrow (pos, e1, e2) -> Arrow (pos, substitute_naive_list var t e1, substitute_naive_list var t e2) + | Call (pos, id, expr_list) -> + Call (pos, id, List.map (fun e -> substitute_naive_list var t e) expr_list) + +let rec substitute_naive_list_ty (var:HString.t list) (t:expr list) = function + | ArrayType (pos, (ty, expr)) -> ( + let expr = substitute_naive_list var t expr in + let ty = substitute_naive_list_ty var t ty in + ArrayType (pos, (ty, expr)) + ) + | TupleType(pos, tys) -> + TupleType(pos, List.map (substitute_naive_list_ty var t) tys) + | GroupType(pos, tys) -> + GroupType(pos, List.map (substitute_naive_list_ty var t) tys) + | TArr(pos, ty1, ty2) -> + TArr(pos, substitute_naive_list_ty var t ty1, substitute_naive_list_ty var t ty2) + | RecordType (pos, name, tis) -> + let tis = + List.map (fun (p, id, ty) -> (p, id, substitute_naive_list_ty var t ty)) tis + in + RecordType (pos, name, tis) + | ty -> ty + let rec has_unguarded_pre ung = function | Const _ | Ident _ | ModeRef _ -> false diff --git a/src/lustre/lustreAstHelpers.mli b/src/lustre/lustreAstHelpers.mli index 0f7764d79..627c3d1ac 100644 --- a/src/lustre/lustreAstHelpers.mli +++ b/src/lustre/lustreAstHelpers.mli @@ -58,6 +58,12 @@ val substitute_naive : HString.t -> expr -> expr -> expr (** Substitute second param for first param in third param. AnyOp and Quantifier are not supported due to introduction of bound variables. *) +val substitute_naive_list_ty : index list -> expr list -> lustre_type -> lustre_type +(** Substitute second param list for first param list in third param. + The third param is a (possibly dependent) type. + ChooseOp and Quantifier are not supported due to introduction of bound variables. *) + + val has_unguarded_pre : expr -> bool (** Returns true if the expression has unguareded pre's *) diff --git a/src/lustre/lustreTypeChecker.ml b/src/lustre/lustreTypeChecker.ml index 5d5660a3c..f0730550b 100644 --- a/src/lustre/lustreTypeChecker.ml +++ b/src/lustre/lustreTypeChecker.ml @@ -370,6 +370,41 @@ let check_constant_args ctx i arg_exprs = else R.ok () ) +let rec type_extract_array_lens ctx ty = match ty with + | LA.ArrayType (_, (ty, expr)) -> expr :: type_extract_array_lens ctx ty + | TupleType (_, tys) -> List.map (type_extract_array_lens ctx) tys |> List.flatten + | GroupType (_, tys) -> List.map (type_extract_array_lens ctx) tys |> List.flatten + | TArr (_, ty1, ty2) -> + type_extract_array_lens ctx ty1 @ type_extract_array_lens ctx ty2 + | RecordType (_, _, tis) -> + let tys = List.map (fun (_, _, ty) -> ty) tis in + List.map (type_extract_array_lens ctx) tys |> List.flatten + | UserType (_, id) -> + (match (lookup_ty_syn ctx id) with + | Some ty -> type_extract_array_lens ctx ty; + | None -> []) + | _ -> [] + +let update_ty_with_ctx node_ty call_params ctx arg_exprs = + let call_param_array_lens = type_extract_array_lens ctx node_ty in + let find_matching_len_params array_param_lens = + List.map (fun len -> (Lib.list_index (fun (id2, _) -> len = id2) call_params)) array_param_lens + in + let call_param_len_idents = List.map (LH.vars_without_node_call_ids) call_param_array_lens + |> List.map LA.SI.elements + (* Filter out constants *) + |> List.map (List.filter (fun id -> not (member_val ctx id))) + |> List.flatten + in + (* Find indices of array length parameters. E.g. in Call(m :: const int, A :: int^m), the index + of array length param "m" is 0. *) + let array_len_indices = find_matching_len_params call_param_len_idents in + (* Retrieve concrete arguments passed as array lengths *) + let array_len_exprs = (List.map (List.nth arg_exprs)) array_len_indices in + (* Do substitution to express exp_arg_tys and exp_ret_tys in terms of the current context *) + LH.substitute_naive_list_ty call_param_len_idents array_len_exprs node_ty + + let rec infer_type_expr: tc_context -> LA.expr -> (tc_type, [> error]) result = fun ctx -> function (* Identifiers *) @@ -588,17 +623,24 @@ let rec infer_type_expr: tc_context -> LA.expr -> (tc_type, [> error]) result if List.length arg_tys = 1 then R.ok (List.hd arg_tys) else R.ok (LA.GroupType (pos, arg_tys)) in - match (lookup_node_ty ctx i) with - | Some (TArr (_, exp_arg_tys, exp_ret_tys)) -> ( + match (lookup_node_param_attr ctx i), (lookup_node_ty ctx i) with + | Some call_params, Some node_ty -> ( + (* Express exp_arg_tys and exp_ret_tys in terms of the current context *) + let node_ty = update_ty_with_ctx node_ty call_params ctx arg_exprs in + let exp_arg_tys, exp_ret_tys = match node_ty with + | TArr (_, exp_arg_tys, exp_ret_tys) -> exp_arg_tys, exp_ret_tys + | _ -> assert false + in let* given_arg_tys = infer_type_node_args ctx arg_exprs 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)) + let* ctx = (check_constant_args ctx i arg_exprs >> (R.ok exp_ret_tys)) in + R.ok ctx else (type_error pos (IlltypedCall (exp_arg_tys, given_arg_tys))) ) - | Some ty -> type_error pos (ExpectedFunctionType ty) - | None -> type_error pos (UnboundNodeName i) + | _, Some ty -> type_error pos (ExpectedFunctionType ty) + | _, None -> type_error pos (UnboundNodeName i) ) (** Infer the type of a [LA.expr] with the types of free variables given in [tc_context] *) @@ -767,14 +809,18 @@ and check_type_expr: tc_context -> LA.expr -> tc_type -> (unit, [> error]) resul (* Node calls *) | Call (pos, i, args) -> - R.seq (List.map (infer_type_expr ctx) args) >>= fun arg_tys -> + let* arg_tys = R.seq (List.map (infer_type_expr ctx) args) in let arg_ty = if List.length arg_tys = 1 then List.hd arg_tys else GroupType (pos, arg_tys) in - (match (lookup_node_ty ctx i) with - | None -> type_error pos (UnboundNodeName i) - | Some ty -> - R.guard_with (eq_lustre_type ctx ty (LA.TArr (pos, arg_ty, exp_ty))) - (type_error pos (MismatchedNodeType (i, (TArr (pos, arg_ty, exp_ty)), ty)))) + (match (lookup_node_ty ctx i), (lookup_node_param_attr ctx i) with + | None, _ + | _, None -> type_error pos (UnboundNodeName i) + | Some ty, Some call_params -> + (* Express ty in terms of the current context *) + let ty = update_ty_with_ctx ty call_params ctx args in + let* b = (eq_lustre_type ctx ty (LA.TArr (pos, arg_ty, exp_ty))) in + if b then R.ok () + else (type_error pos (MismatchedNodeType (i, (TArr (pos, arg_ty, exp_ty)), ty)))) (** Type checks an expression and returns [ok] * if the expected type is the given type [tc_type] * returns an [Error of string] otherwise *) diff --git a/tests/ounit/lustre/testLustreFrontend.ml b/tests/ounit/lustre/testLustreFrontend.ml index df389bd0b..536f2a9bc 100644 --- a/tests/ounit/lustre/testLustreFrontend.ml +++ b/tests/ounit/lustre/testLustreFrontend.ml @@ -180,6 +180,10 @@ let _ = run_test_tt_main ("frontend LustreSyntaxChecks error tests" >::: [ (* Lustre Ast Array Dependencies Checks *) (* *************************************************************************** *) let _ = run_test_tt_main ("frontend lustreArrayDependencies error tests" >::: [ + mk_test "test illtyped call" (fun () -> + match load_file "./lustreTypeChecker/SteamBoiler2.lus" with + | Error (`LustreArrayDependencies (_, Cycle _)) -> true + | _ -> false); mk_test "test invalid inductive array def 1" (fun () -> match load_file "./lustreArrayDependencies/inductive_array1.lus" with | Error (`LustreArrayDependencies (_, Cycle _)) -> true @@ -479,10 +483,6 @@ let _ = run_test_tt_main ("frontend LustreTypeChecker error tests" >::: [ match load_file "./lustreTypeChecker/mode_reqs_by_idents_shadowing.lus" with | Error (`LustreTypeCheckerError (_, Redeclaration _)) -> true | _ -> false); - mk_test "test illtyped call" (fun () -> - match load_file "./lustreTypeChecker/SteamBoiler2.lus" with - | Error (`LustreTypeCheckerError (_, IlltypedCall _)) -> true - | _ -> false); mk_test "test expected type 1" (fun () -> match load_file "./lustreTypeChecker/test_array_group.lus" with | Error (`LustreTypeCheckerError (_, ExpectedType _)) -> true From f1e09e3c92e7ad8ac5c5358830e15a205cd5bd88 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Fri, 1 Dec 2023 14:38:25 -0600 Subject: [PATCH 2/7] Minor code cleanup --- src/lustre/lustreTypeChecker.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/lustre/lustreTypeChecker.ml b/src/lustre/lustreTypeChecker.ml index f0730550b..0bf858800 100644 --- a/src/lustre/lustreTypeChecker.ml +++ b/src/lustre/lustreTypeChecker.ml @@ -634,8 +634,7 @@ let rec infer_type_expr: tc_context -> LA.expr -> (tc_type, [> error]) result let* given_arg_tys = infer_type_node_args ctx arg_exprs in let* are_equal = eq_lustre_type ctx exp_arg_tys given_arg_tys in if are_equal then - let* ctx = (check_constant_args ctx i arg_exprs >> (R.ok exp_ret_tys)) in - R.ok ctx + (check_constant_args ctx i arg_exprs >> (R.ok exp_ret_tys)) else (type_error pos (IlltypedCall (exp_arg_tys, given_arg_tys))) ) From 21c974b77d7794a7e19b166e3ba82e3542b7b257 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Fri, 1 Dec 2023 14:39:15 -0600 Subject: [PATCH 3/7] Remove unnecessary whitespace --- src/lustre/lustreTypeChecker.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lustre/lustreTypeChecker.ml b/src/lustre/lustreTypeChecker.ml index 0bf858800..699e80cf9 100644 --- a/src/lustre/lustreTypeChecker.ml +++ b/src/lustre/lustreTypeChecker.ml @@ -634,7 +634,7 @@ let rec infer_type_expr: tc_context -> LA.expr -> (tc_type, [> error]) result let* given_arg_tys = infer_type_node_args ctx arg_exprs 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)) + (check_constant_args ctx i arg_exprs >> (R.ok exp_ret_tys)) else (type_error pos (IlltypedCall (exp_arg_tys, given_arg_tys))) ) From d119a8d01f0b10cba3917f84df35dd5a8e42da82 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Mon, 4 Dec 2023 15:13:51 -0600 Subject: [PATCH 4/7] Compute substitution map once in lustreAstHelper --- src/lustre/lustreAstHelpers.ml | 66 ++++++++++++++++----------------- src/lustre/lustreAstHelpers.mli | 8 ++-- src/lustre/lustreTypeChecker.ml | 2 +- 3 files changed, 38 insertions(+), 38 deletions(-) diff --git a/src/lustre/lustreAstHelpers.ml b/src/lustre/lustreAstHelpers.ml index d461e5bbb..fc4759533 100644 --- a/src/lustre/lustreAstHelpers.ml +++ b/src/lustre/lustreAstHelpers.ml @@ -169,72 +169,72 @@ let rec substitute_naive (var:HString.t) t = function Call (pos, id, List.map (fun e -> substitute_naive var t e) expr_list) (* Substitute t for var. ChooseOp and Quantifier are not supported due to introduction of bound variables. *) -let rec substitute_naive_list (var:HString.t list) (t:expr list) = function +let rec apply_subst_in_expr sigma = function | Ident (pos, i) -> ( - match List.assoc_opt i (List.combine var t) with + match List.assoc_opt i sigma with | Some expr -> expr | None -> Ident (pos, i) ) | ModeRef (_, _) as e -> e - | RecordProject (pos, e, idx) -> RecordProject (pos, substitute_naive_list var t e, idx) - | TupleProject (pos, e, idx) -> TupleProject (pos, substitute_naive_list var t e, idx) + | RecordProject (pos, e, idx) -> RecordProject (pos, apply_subst_in_expr sigma e, idx) + | TupleProject (pos, e, idx) -> TupleProject (pos, apply_subst_in_expr sigma e, idx) | Const (_, _) as e -> e - | UnaryOp (pos, op, e) -> UnaryOp (pos, op, substitute_naive_list var t e) + | UnaryOp (pos, op, e) -> UnaryOp (pos, op, apply_subst_in_expr sigma e) | BinaryOp (pos, op, e1, e2) -> - BinaryOp (pos, op, substitute_naive_list var t e1, substitute_naive_list var t e2) + BinaryOp (pos, op, apply_subst_in_expr sigma e1, apply_subst_in_expr sigma e2) | TernaryOp (pos, op, e1, e2, e3) -> - TernaryOp (pos, op, substitute_naive_list var t e1, substitute_naive_list var t e2, substitute_naive_list var t e3) - | ConvOp (pos, op, e) -> ConvOp (pos, op, substitute_naive_list var t e) + TernaryOp (pos, op, apply_subst_in_expr sigma e1, apply_subst_in_expr sigma e2, apply_subst_in_expr sigma e3) + | ConvOp (pos, op, e) -> ConvOp (pos, op, apply_subst_in_expr sigma e) | CompOp (pos, op, e1, e2) -> - CompOp (pos, op, substitute_naive_list var t e1, substitute_naive_list var t e2) + CompOp (pos, op, apply_subst_in_expr sigma e1, apply_subst_in_expr sigma e2) | AnyOp _ -> assert false (* Not supported due to introduction of bound variables *) | Quantifier _ -> assert false (* Not supported due to introduction of bound variables *) | RecordExpr (pos, ident, expr_list) -> - RecordExpr (pos, ident, List.map (fun (i, e) -> (i, substitute_naive_list var t e)) expr_list) + RecordExpr (pos, ident, List.map (fun (i, e) -> (i, apply_subst_in_expr sigma e)) expr_list) | GroupExpr (pos, kind, expr_list) -> - GroupExpr (pos, kind, List.map (fun e -> substitute_naive_list var t e) expr_list) + GroupExpr (pos, kind, List.map (fun e -> apply_subst_in_expr sigma e) expr_list) | StructUpdate (pos, e1, idx, e2) -> - StructUpdate (pos, substitute_naive_list var t e1, idx, substitute_naive_list var t e2) + StructUpdate (pos, apply_subst_in_expr sigma e1, idx, apply_subst_in_expr sigma e2) | ArrayConstr (pos, e1, e2) -> - ArrayConstr (pos, substitute_naive_list var t e1, substitute_naive_list var t e2) + ArrayConstr (pos, apply_subst_in_expr sigma e1, apply_subst_in_expr sigma e2) | ArrayIndex (pos, e1, e2) -> - ArrayIndex (pos, substitute_naive_list var t e1, substitute_naive_list var t e2) - | When (pos, e, clock) -> When (pos, substitute_naive_list var t e, clock) + ArrayIndex (pos, apply_subst_in_expr sigma e1, apply_subst_in_expr sigma e2) + | When (pos, e, clock) -> When (pos, apply_subst_in_expr sigma e, clock) | Condact (pos, e1, e2, id, expr_list1, expr_list2) -> - let e1, e2 = substitute_naive_list var t e1, substitute_naive_list var t e2 in - let expr_list1 = List.map (fun e -> substitute_naive_list var t e) expr_list1 in - let expr_list2 = List.map (fun e -> substitute_naive_list var t e) expr_list2 in + let e1, e2 = apply_subst_in_expr sigma e1, apply_subst_in_expr sigma e2 in + let expr_list1 = List.map (fun e -> apply_subst_in_expr sigma e) expr_list1 in + let expr_list2 = List.map (fun e -> apply_subst_in_expr sigma e) expr_list2 in Condact (pos, e1, e2, id, expr_list1, expr_list2) | Activate (pos, ident, e1, e2, expr_list) -> - let e1, e2 = substitute_naive_list var t e1, substitute_naive_list var t e2 in - let expr_list = List.map (fun e -> substitute_naive_list var t e) expr_list in + let e1, e2 = apply_subst_in_expr sigma e1, apply_subst_in_expr sigma e2 in + let expr_list = List.map (fun e -> apply_subst_in_expr sigma e) expr_list in Activate (pos, ident, e1, e2, expr_list) | Merge (pos, ident, expr_list) -> - Merge (pos, ident, List.map (fun (i, e) -> (i, substitute_naive_list var t e)) expr_list) + Merge (pos, ident, List.map (fun (i, e) -> (i, apply_subst_in_expr sigma e)) expr_list) | RestartEvery (pos, ident, expr_list, e) -> - let expr_list = List.map (fun e -> substitute_naive_list var t e) expr_list in - let e = substitute_naive_list var t e in + let expr_list = List.map (fun e -> apply_subst_in_expr sigma e) expr_list in + let e = apply_subst_in_expr sigma e in RestartEvery (pos, ident, expr_list, e) - | Pre (pos, e) -> Pre (pos, substitute_naive_list var t e) - | Arrow (pos, e1, e2) -> Arrow (pos, substitute_naive_list var t e1, substitute_naive_list var t e2) + | Pre (pos, e) -> Pre (pos, apply_subst_in_expr sigma e) + | Arrow (pos, e1, e2) -> Arrow (pos, apply_subst_in_expr sigma e1, apply_subst_in_expr sigma e2) | Call (pos, id, expr_list) -> - Call (pos, id, List.map (fun e -> substitute_naive_list var t e) expr_list) + Call (pos, id, List.map (fun e -> apply_subst_in_expr sigma e) expr_list) -let rec substitute_naive_list_ty (var:HString.t list) (t:expr list) = function +let rec apply_subst_in_type sigma = function | ArrayType (pos, (ty, expr)) -> ( - let expr = substitute_naive_list var t expr in - let ty = substitute_naive_list_ty var t ty in + let expr = apply_subst_in_expr sigma expr in + let ty = apply_subst_in_type sigma ty in ArrayType (pos, (ty, expr)) ) | TupleType(pos, tys) -> - TupleType(pos, List.map (substitute_naive_list_ty var t) tys) + TupleType(pos, List.map (apply_subst_in_type sigma) tys) | GroupType(pos, tys) -> - GroupType(pos, List.map (substitute_naive_list_ty var t) tys) + GroupType(pos, List.map (apply_subst_in_type sigma) tys) | TArr(pos, ty1, ty2) -> - TArr(pos, substitute_naive_list_ty var t ty1, substitute_naive_list_ty var t ty2) + TArr(pos, apply_subst_in_type sigma ty1, apply_subst_in_type sigma ty2) | RecordType (pos, name, tis) -> let tis = - List.map (fun (p, id, ty) -> (p, id, substitute_naive_list_ty var t ty)) tis + List.map (fun (p, id, ty) -> (p, id, apply_subst_in_type sigma ty)) tis in RecordType (pos, name, tis) | ty -> ty diff --git a/src/lustre/lustreAstHelpers.mli b/src/lustre/lustreAstHelpers.mli index 627c3d1ac..6d4f55050 100644 --- a/src/lustre/lustreAstHelpers.mli +++ b/src/lustre/lustreAstHelpers.mli @@ -58,10 +58,10 @@ val substitute_naive : HString.t -> expr -> expr -> expr (** Substitute second param for first param in third param. AnyOp and Quantifier are not supported due to introduction of bound variables. *) -val substitute_naive_list_ty : index list -> expr list -> lustre_type -> lustre_type -(** Substitute second param list for first param list in third param. - The third param is a (possibly dependent) type. - ChooseOp and Quantifier are not supported due to introduction of bound variables. *) +val apply_subst_in_type : (HString.t * expr) list -> lustre_type -> lustre_type +(** [apply_subst_in_type s t] applies the substitution defined by association list [s] + to the expressions of (possibly dependent) type [t] + AnyOp and Quantifier are not supported due to introduction of bound variables. *) val has_unguarded_pre : expr -> bool diff --git a/src/lustre/lustreTypeChecker.ml b/src/lustre/lustreTypeChecker.ml index 699e80cf9..00bfe20c3 100644 --- a/src/lustre/lustreTypeChecker.ml +++ b/src/lustre/lustreTypeChecker.ml @@ -402,7 +402,7 @@ let update_ty_with_ctx node_ty call_params ctx arg_exprs = (* Retrieve concrete arguments passed as array lengths *) let array_len_exprs = (List.map (List.nth arg_exprs)) array_len_indices in (* Do substitution to express exp_arg_tys and exp_ret_tys in terms of the current context *) - LH.substitute_naive_list_ty call_param_len_idents array_len_exprs node_ty + LH.apply_subst_in_type (List.combine call_param_len_idents array_len_exprs) node_ty let rec infer_type_expr: tc_context -> LA.expr -> (tc_type, [> error]) result From 76c478a0c0a5c07489cd4dd6320eb7134781599d Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Mon, 4 Dec 2023 16:19:03 -0600 Subject: [PATCH 5/7] Optimization in update_ty_with_ctx --- src/lustre/lustreTypeChecker.ml | 37 +++++++++++++++++++-------------- 1 file changed, 21 insertions(+), 16 deletions(-) diff --git a/src/lustre/lustreTypeChecker.ml b/src/lustre/lustreTypeChecker.ml index 00bfe20c3..5faa92fbc 100644 --- a/src/lustre/lustreTypeChecker.ml +++ b/src/lustre/lustreTypeChecker.ml @@ -385,25 +385,30 @@ let rec type_extract_array_lens ctx ty = match ty with | None -> []) | _ -> [] -let update_ty_with_ctx node_ty call_params ctx arg_exprs = - let call_param_array_lens = type_extract_array_lens ctx node_ty in - let find_matching_len_params array_param_lens = - List.map (fun len -> (Lib.list_index (fun (id2, _) -> len = id2) call_params)) array_param_lens - in - let call_param_len_idents = List.map (LH.vars_without_node_call_ids) call_param_array_lens - |> List.map LA.SI.elements +let update_ty_with_ctx node_ty call_params ctx arg_exprs = + let call_param_len_idents = + type_extract_array_lens ctx node_ty + |> List.map (LH.vars_without_node_call_ids) + (* Remove duplicates *) + |> List.fold_left (fun acc vars -> LA.SI.union vars acc) LA.SI.empty + |> LA.SI.elements (* Filter out constants *) - |> List.map (List.filter (fun id -> not (member_val ctx id))) - |> List.flatten + |> List.filter (fun id -> not (member_val ctx id)) in - (* Find indices of array length parameters. E.g. in Call(m :: const int, A :: int^m), the index + match call_param_len_idents with + | [] -> node_ty + | _ -> ( + let find_matching_len_params array_param_lens = + List.map (fun len -> (Lib.list_index (fun (id2, _) -> len = id2) call_params)) array_param_lens + in + (* Find indices of array length parameters. E.g. in Call(m :: const int, A :: int^m), the index of array length param "m" is 0. *) - let array_len_indices = find_matching_len_params call_param_len_idents in - (* Retrieve concrete arguments passed as array lengths *) - let array_len_exprs = (List.map (List.nth arg_exprs)) array_len_indices in - (* Do substitution to express exp_arg_tys and exp_ret_tys in terms of the current context *) - LH.apply_subst_in_type (List.combine call_param_len_idents array_len_exprs) node_ty - + let array_len_indices = find_matching_len_params call_param_len_idents in + (* Retrieve concrete arguments passed as array lengths *) + let array_len_exprs = List.map (List.nth arg_exprs) array_len_indices in + (* Do substitution to express exp_arg_tys and exp_ret_tys in terms of the current context *) + LH.apply_subst_in_type (List.combine call_param_len_idents array_len_exprs) node_ty + ) let rec infer_type_expr: tc_context -> LA.expr -> (tc_type, [> error]) result = fun ctx -> function From e8228807b4d6d1bf3857f9a7950630a680ae1ff7 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Mon, 4 Dec 2023 16:25:11 -0600 Subject: [PATCH 6/7] Add lookup_node_param_ids function --- src/lustre/lustreTypeChecker.ml | 6 +++--- src/lustre/typeCheckerContext.ml | 6 ++++++ src/lustre/typeCheckerContext.mli | 2 ++ 3 files changed, 11 insertions(+), 3 deletions(-) diff --git a/src/lustre/lustreTypeChecker.ml b/src/lustre/lustreTypeChecker.ml index 5faa92fbc..d06a40408 100644 --- a/src/lustre/lustreTypeChecker.ml +++ b/src/lustre/lustreTypeChecker.ml @@ -399,7 +399,7 @@ let update_ty_with_ctx node_ty call_params ctx arg_exprs = | [] -> node_ty | _ -> ( let find_matching_len_params array_param_lens = - List.map (fun len -> (Lib.list_index (fun (id2, _) -> len = id2) call_params)) array_param_lens + List.map (fun len -> (Lib.list_index (fun id2 -> len = id2) call_params)) array_param_lens in (* Find indices of array length parameters. E.g. in Call(m :: const int, A :: int^m), the index of array length param "m" is 0. *) @@ -628,7 +628,7 @@ let rec infer_type_expr: tc_context -> LA.expr -> (tc_type, [> error]) result if List.length arg_tys = 1 then R.ok (List.hd arg_tys) else R.ok (LA.GroupType (pos, arg_tys)) in - match (lookup_node_param_attr ctx i), (lookup_node_ty ctx i) with + match (lookup_node_param_ids ctx i), (lookup_node_ty ctx i) with | Some call_params, Some node_ty -> ( (* Express exp_arg_tys and exp_ret_tys in terms of the current context *) let node_ty = update_ty_with_ctx node_ty call_params ctx arg_exprs in @@ -816,7 +816,7 @@ and check_type_expr: tc_context -> LA.expr -> tc_type -> (unit, [> error]) resul let* arg_tys = R.seq (List.map (infer_type_expr ctx) args) in let arg_ty = if List.length arg_tys = 1 then List.hd arg_tys else GroupType (pos, arg_tys) in - (match (lookup_node_ty ctx i), (lookup_node_param_attr ctx i) with + (match (lookup_node_ty ctx i), (lookup_node_param_ids ctx i) with | None, _ | _, None -> type_error pos (UnboundNodeName i) | Some ty, Some call_params -> diff --git a/src/lustre/typeCheckerContext.ml b/src/lustre/typeCheckerContext.ml index b6123361f..2240d8629 100644 --- a/src/lustre/typeCheckerContext.ml +++ b/src/lustre/typeCheckerContext.ml @@ -178,6 +178,12 @@ let lookup_node_ty: tc_context -> LA.ident -> tc_type option let lookup_node_param_attr: tc_context -> LA.ident -> (HString.t * bool) list option = fun ctx i -> IMap.find_opt i (ctx.node_param_attr) +let lookup_node_param_ids: tc_context -> LA.ident -> HString.t list option + = fun ctx i -> + match IMap.find_opt i (ctx.node_param_attr) with + | Some l -> Some (List.map fst l) + | None -> None + let lookup_const: tc_context -> LA.ident -> (LA.expr * tc_type option) option = fun ctx i -> IMap.find_opt i (ctx.vl_ctx) (** Lookup a constant identifier *) diff --git a/src/lustre/typeCheckerContext.mli b/src/lustre/typeCheckerContext.mli index 05fd96590..ed1654c69 100644 --- a/src/lustre/typeCheckerContext.mli +++ b/src/lustre/typeCheckerContext.mli @@ -105,6 +105,8 @@ val lookup_node_ty: tc_context -> LA.ident -> tc_type option val lookup_node_param_attr: tc_context -> LA.ident -> (HString.t * bool) list option +val lookup_node_param_ids: tc_context -> LA.ident -> HString.t list option + val lookup_const: tc_context -> LA.ident -> (LA.expr * tc_type option) option (** Lookup a constant identifier *) From 33fd5343feafb095f627b0a390c2dcba57d2a0ae Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Tue, 5 Dec 2023 17:57:33 -0600 Subject: [PATCH 7/7] Fix bug filtering out constants in array length constraints --- src/lustre/lustreTypeChecker.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lustre/lustreTypeChecker.ml b/src/lustre/lustreTypeChecker.ml index d06a40408..3b9e1e08e 100644 --- a/src/lustre/lustreTypeChecker.ml +++ b/src/lustre/lustreTypeChecker.ml @@ -392,8 +392,8 @@ let update_ty_with_ctx node_ty call_params ctx arg_exprs = (* Remove duplicates *) |> List.fold_left (fun acc vars -> LA.SI.union vars acc) LA.SI.empty |> LA.SI.elements - (* Filter out constants *) - |> List.filter (fun id -> not (member_val ctx id)) + (* Filter out constants. If "id" is a constant, it must be a local constant *) + |> List.filter (fun id -> not (member_val ctx id) || (List.mem id call_params) ) in match call_param_len_idents with | [] -> node_ty