From 2733f83db41c374254fe9357ac6025ceeacb7edf Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Thu, 26 Oct 2023 11:56:05 -0500 Subject: [PATCH 1/3] Fix const inlining for type declarations --- src/lustre/lustreAstInlineConstants.ml | 2 +- tests/regression/success/test_const_decls.lus | 8 ++++++-- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/lustre/lustreAstInlineConstants.ml b/src/lustre/lustreAstInlineConstants.ml index 9140e7522..e83d34fc2 100644 --- a/src/lustre/lustreAstInlineConstants.ml +++ b/src/lustre/lustreAstInlineConstants.ml @@ -489,7 +489,7 @@ let substitute: TC.tc_context -> LA.declaration -> (TC.tc_context * LA.declarati function | TypeDecl (span, AliasType (pos, i, t)) -> let t' = inline_constants_of_lustre_type ctx t in - ctx, LA.TypeDecl (span, AliasType (pos, i, t')) + TC.add_ty_syn ctx i t', LA.TypeDecl (span, AliasType (pos, i, t')) | ConstDecl (span, FreeConst (pos, id, ty)) -> let ty' = inline_constants_of_lustre_type ctx ty in ctx, ConstDecl (span, FreeConst (pos, id, ty')) diff --git a/tests/regression/success/test_const_decls.lus b/tests/regression/success/test_const_decls.lus index f8bb366a5..e3322b3d0 100644 --- a/tests/regression/success/test_const_decls.lus +++ b/tests/regression/success/test_const_decls.lus @@ -87,7 +87,11 @@ const j = complex1 { re = -(3.0)/2.0; im = 3.0/2.0 }; const c100:int = 1 + 1; const c101:real = 1.0 + 1.0; -node main () returns (x:int;) +type s1 = subrange [-1,1] of int; + +node imported R(x: s1) returns (y:s1); + +node main (x: s1) returns (y: s1) let - x = 0; + y = R(pre x); tel From ce89fa6d6afccf901fb8e4bf38da8576244096d7 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Thu, 26 Oct 2023 13:40:53 -0500 Subject: [PATCH 2/3] Synchronize type and const stores in typing context --- src/lustre/lustreAstInlineConstants.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/lustre/lustreAstInlineConstants.ml b/src/lustre/lustreAstInlineConstants.ml index e83d34fc2..5b2aa99ee 100644 --- a/src/lustre/lustreAstInlineConstants.ml +++ b/src/lustre/lustreAstInlineConstants.ml @@ -501,11 +501,13 @@ let substitute: TC.tc_context -> LA.declaration -> (TC.tc_context * LA.declarati , ConstDecl (span, UntypedConst (pos', i, e'))) | Some ty -> let ty' = inline_constants_of_lustre_type ctx ty in - (TC.add_const ctx i e' ty', ConstDecl (span, UntypedConst (pos', i, e')))) + let ctx' = TC.add_ty (TC.add_const ctx i e' ty') i ty' in + (ctx', ConstDecl (span, UntypedConst (pos', i, e')))) | ConstDecl (span, TypedConst (pos', i, e, ty)) -> let ty' = inline_constants_of_lustre_type ctx ty in - let e' = simplify_expr ctx e in - (TC.add_const ctx i e' ty', ConstDecl (span, TypedConst (pos', i, e', ty'))) + let e' = simplify_expr ctx e in + let ctx' = TC.add_ty (TC.add_const ctx i e' ty') i ty' in + (ctx', ConstDecl (span, TypedConst (pos', i, e', ty'))) | (LA.NodeDecl (span, (i, imported, params, ips, ops, ldecls, items, contract))) -> let ips' = inline_constants_of_const_clocked_type_decl ctx ips in let ops' = inline_constants_of_clocked_type_decl ctx ops in From c2d6105736ae7ffe7626f6993363d26b2ed50b2e Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Wed, 1 Nov 2023 21:44:30 -0500 Subject: [PATCH 3/3] No inlining for enum types --- src/lustre/lustreAstInlineConstants.ml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/lustre/lustreAstInlineConstants.ml b/src/lustre/lustreAstInlineConstants.ml index 5b2aa99ee..4c4dff98e 100644 --- a/src/lustre/lustreAstInlineConstants.ml +++ b/src/lustre/lustreAstInlineConstants.ml @@ -488,8 +488,16 @@ let rec inline_constants_of_contract: TC.tc_context -> LA.contract -> LA.contrac let substitute: TC.tc_context -> LA.declaration -> (TC.tc_context * LA.declaration) = fun ctx -> function | TypeDecl (span, AliasType (pos, i, t)) -> - let t' = inline_constants_of_lustre_type ctx t in - TC.add_ty_syn ctx i t', LA.TypeDecl (span, AliasType (pos, i, t')) + let ctx', t' = + match t with + | LA.EnumType _ -> + (* Special handling is applied to enum types (see type_check_infer_globals) *) + ctx, t + | _ -> + let t' = inline_constants_of_lustre_type ctx t in + TC.add_ty_syn ctx i t', t' + in + ctx', LA.TypeDecl (span, AliasType (pos, i, t')) | ConstDecl (span, FreeConst (pos, id, ty)) -> let ty' = inline_constants_of_lustre_type ctx ty in ctx, ConstDecl (span, FreeConst (pos, id, ty'))