From 9130db411743f4c253ae54c78afef0ff0b904269 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Mon, 18 Nov 2024 12:22:59 -0600 Subject: [PATCH 1/2] Add support for free constants with refinement types --- src/lustre/lustreAstNormalizer.ml | 24 +++++++++---------- src/lustre/lustreAstNormalizer.mli | 5 ++++ src/lustre/lustreInput.ml | 1 + src/lustre/lustreNodeGen.ml | 17 +++++++++---- src/lustre/lustreTypeChecker.ml | 10 +++++--- .../success/ref_type_local_free_const.lus | 15 ++++++++++++ 6 files changed, 53 insertions(+), 19 deletions(-) create mode 100644 tests/regression/success/ref_type_local_free_const.lus diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml index aa57e6a7d..9a8581679 100644 --- a/src/lustre/lustreAstNormalizer.ml +++ b/src/lustre/lustreAstNormalizer.ml @@ -584,42 +584,42 @@ let mk_fresh_subrange_constraint source info pos node_id constrained_name expr_t in List.fold_left union (empty ()) gids -let rec mk_ref_type_expr: Ctx.tc_context -> A.expr -> source -> A.lustre_type -> (source * A.expr) list - = fun ctx id source ty -> +let rec mk_ref_type_expr: Ctx.tc_context -> A.expr -> A.lustre_type -> A.expr list + = fun ctx id ty -> let ty = Ctx.expand_type_syn ctx ty in match ty with | A.RefinementType (_, (_, id2, _), expr) -> (* For refinement type variable of the form x = { y: int | ... }, write the constraint in terms of x instead of y *) let expr = AH.substitute_naive id2 id expr in - [(source, expr)] + [expr] | TupleType (pos, tys) | GroupType (pos, tys) -> List.mapi (fun i ty -> - mk_ref_type_expr ctx (A.TupleProject(pos, id, i)) source ty + mk_ref_type_expr ctx (A.TupleProject(pos, id, i)) ty ) tys |> List.flatten | RecordType (p, _, tis) -> List.map (fun (_, id2, ty) -> let expr = A.RecordProject(p, id, id2) in - mk_ref_type_expr ctx expr source ty + mk_ref_type_expr ctx expr ty ) tis |> List.flatten | ArrayType (_, (ty, len)) -> let pos = AH.pos_of_expr id in let dummy_index = mk_fresh_dummy_index () in - let exprs_sources = mk_ref_type_expr ctx (A.ArrayIndex(pos, id, Ident(pos, dummy_index))) source ty in - List.map (fun (source, expr) -> + let exprs = mk_ref_type_expr ctx (A.ArrayIndex(pos, id, Ident(pos, dummy_index))) ty in + List.map (fun expr -> let bound1 = A.CompOp(pos, Lte, A.Const(pos, Num (HString.mk_hstring "0")), A.Ident(pos, dummy_index)) in let bound2 = A.CompOp(pos, Lt, A.Ident(pos, dummy_index), len) in let expr = A.BinaryOp(pos, Impl, A.BinaryOp(pos, And, bound1, bound2), expr) in - source, A.Quantifier(pos, Forall, [pos, dummy_index, A.Int pos], expr) - ) exprs_sources + A.Quantifier(pos, Forall, [pos, dummy_index, A.Int pos], expr) + ) exprs | _ -> [] let mk_fresh_refinement_type_constraint source info pos id expr_type = - let ref_type_exprs = mk_ref_type_expr info.context id source expr_type in - let gids = List.map (fun (source, ref_type_expr) -> + let ref_type_exprs = mk_ref_type_expr info.context id expr_type in + let gids = List.map (fun ref_type_expr -> i := !i + 1; let output_expr = AH.rename_contract_vars ref_type_expr in let prefix = HString.mk_hstring (string_of_int !i) in @@ -1758,7 +1758,7 @@ and normalize_expr ?guard info node_id map = let expr = A.Ident(dpos, id) in let range_exprs = List.map fst (mk_enum_range_expr info.context (Some node_id) ty expr) @ - List.map snd (mk_ref_type_expr info.context expr Local ty) + (mk_ref_type_expr info.context expr ty) in range_exprs :: acc ) diff --git a/src/lustre/lustreAstNormalizer.mli b/src/lustre/lustreAstNormalizer.mli index f74857caf..4f40c6957 100644 --- a/src/lustre/lustreAstNormalizer.mli +++ b/src/lustre/lustreAstNormalizer.mli @@ -88,6 +88,11 @@ val mk_range_expr : TypeCheckerContext.tc_context -> LustreAst.expr -> (LustreAst.expr * bool) list +val mk_ref_type_expr : TypeCheckerContext.tc_context -> + LustreAst.expr -> + LustreAst.lustre_type -> + LustreAst.expr list + val mk_enum_range_expr : TypeCheckerContext.tc_context -> HString.t option -> LustreAst.lustre_type -> diff --git a/src/lustre/lustreInput.ml b/src/lustre/lustreInput.ml index c549ef7e6..e911fc225 100644 --- a/src/lustre/lustreInput.ml +++ b/src/lustre/lustreInput.ml @@ -205,6 +205,7 @@ let type_check declarations = let inlined_global_ctx, const_inlined_nodes_and_contracts = LIP.instantiate_polymorphic_nodes inlined_global_ctx const_inlined_nodes_and_contracts in (* Step 17. Flatten refinement types *) + let const_inlined_type_and_consts = LFR.flatten_ref_types inlined_global_ctx const_inlined_type_and_consts in let const_inlined_nodes_and_contracts = LFR.flatten_ref_types inlined_global_ctx const_inlined_nodes_and_contracts in (* Step 18. Normalize AST: guard pres, abstract to locals where appropriate *) diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml index af90d610a..6c4489b63 100644 --- a/src/lustre/lustreNodeGen.ml +++ b/src/lustre/lustreNodeGen.ml @@ -2365,15 +2365,24 @@ and compile_const_decl ?(ghost = false) cstate ctx map scope = function else ( let global_constraints = let ty = Ctx.expand_type_syn ctx ty in - if Ctx.type_contains_subrange ctx ty then ( + let has_subrange = Ctx.type_contains_subrange ctx ty in + let has_ref_type = Ctx.type_contains_ref ctx ty in + if has_subrange || has_ref_type then ( + let ctx = Ctx.add_ty ctx i ty in let range_exprs = - let ctx = Ctx.add_ty ctx i ty in - AN.mk_range_expr ctx None ty (A.Ident (p, i)) |> List.map fst + if has_subrange then + AN.mk_range_expr ctx None ty (A.Ident (p, i)) |> List.map fst + else [] + in + let ref_type_exprs = + if has_ref_type then + AN.mk_ref_type_expr ctx (A.Ident(p, i)) ty + else [] in List.map (fun expr -> let c_expr = compile_ast_expr cstate ctx [] map expr in X.max_binding c_expr |> snd - ) range_exprs @ cstate.global_constraints + ) (range_exprs @ ref_type_exprs) @ cstate.global_constraints ) else cstate.global_constraints in diff --git a/src/lustre/lustreTypeChecker.ml b/src/lustre/lustreTypeChecker.ml index efc74dc8a..c502e7eeb 100644 --- a/src/lustre/lustreTypeChecker.ml +++ b/src/lustre/lustreTypeChecker.ml @@ -193,7 +193,7 @@ let error_message kind = match kind with ^ Lib.string_of_t LA.pp_print_expr e | IntervalMustHaveBound -> "Range should have at least one bound" | ExpectedRecordType ty -> "Expected record type but found " ^ string_of_tc_type ty - | GlobalConstRefType id -> "Global constant '" ^ HString.string_of_hstring id ^ "' has refinement type (not yet supported)" + | GlobalConstRefType id -> "Definition of global constant '" ^ HString.string_of_hstring id ^ "' has refinement type (not yet supported)" | QuantifiedAbstractType id -> "Variable '" ^ HString.string_of_hstring id ^ "' with type that contains an abstract type (or type variable) cannot be quantified" | InvalidPolymorphicCall id -> "Call to node, contract, or user type '" ^ HString.string_of_hstring id ^ "' passes an incorrect number of type parameters" @@ -1928,8 +1928,7 @@ and build_type_and_const_context: tc_context -> LA.t -> (tc_context * [> warning | LA.TypeDecl (_, ty_decl) :: rest -> let* ctx' = tc_ctx_of_ty_decl ctx ty_decl in build_type_and_const_context ctx' rest - | LA.ConstDecl (_, (TypedConst (p, i, _, ty) as const_decl)) :: rest - | LA.ConstDecl (_, ((FreeConst (p, i, ty)) as const_decl)) :: rest -> + | LA.ConstDecl (_, (TypedConst (p, i, _, ty) as const_decl)) :: rest -> let ty = expand_type_syn ctx ty in if type_contains_ref ctx ty then type_error p (GlobalConstRefType i) else ( @@ -1937,6 +1936,11 @@ and build_type_and_const_context: tc_context -> LA.t -> (tc_context * [> warning let* ctx', warnings2 = build_type_and_const_context ctx' rest in R.ok (ctx', warnings1 @ warnings2) ) + | LA.ConstDecl (_, ((FreeConst _) as const_decl)) :: rest -> ( + let* ctx', warnings1 = tc_ctx_const_decl ctx Global None const_decl in + let* ctx', warnings2 = build_type_and_const_context ctx' rest in + R.ok (ctx', warnings1 @ warnings2) + ) | LA.ConstDecl (_, UntypedConst _) :: _ -> assert false | _ :: rest -> build_type_and_const_context ctx rest (** Process top level type declarations and make a type context with diff --git a/tests/regression/success/ref_type_local_free_const.lus b/tests/regression/success/ref_type_local_free_const.lus new file mode 100644 index 000000000..374a790e9 --- /dev/null +++ b/tests/regression/success/ref_type_local_free_const.lus @@ -0,0 +1,15 @@ + +type Nat = subrange [0,*] of int; + +type R0 = struct { x: Nat; y: Nat }; + +type R1 = subtype { r: R0 | r.x < 10 }; + +type R2 = subtype { r: R1 | r.y < 20}; + +const C: R2; + +node N() returns () +let + check "P1" C.x < 10 and C.y < 20; +tel \ No newline at end of file From 7ae9436e3a72ac92482d8a1940115f93d44e7a96 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Mon, 18 Nov 2024 12:24:08 -0600 Subject: [PATCH 2/2] Update ref_type_local_free_const.lus test --- tests/regression/success/ref_type_local_free_const.lus | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tests/regression/success/ref_type_local_free_const.lus b/tests/regression/success/ref_type_local_free_const.lus index 374a790e9..ce3da234e 100644 --- a/tests/regression/success/ref_type_local_free_const.lus +++ b/tests/regression/success/ref_type_local_free_const.lus @@ -7,9 +7,8 @@ type R1 = subtype { r: R0 | r.x < 10 }; type R2 = subtype { r: R1 | r.y < 20}; -const C: R2; - node N() returns () +const C: R2; let check "P1" C.x < 10 and C.y < 20; tel \ No newline at end of file