Merge pull request kind2-mc#1020 from daniel-larraz/develop

Inline constants in type of free constant
daniel-larraz · Oct 6, 2023 · 0e29b1a · 0e29b1a
2 parents 7037672 + 74649e5
commit 0e29b1a
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/src/lustre/lustreAstInlineConstants.ml b/src/lustre/lustreAstInlineConstants.ml
@@ -490,7 +490,9 @@ let substitute: TC.tc_context -> LA.declaration -> (TC.tc_context * LA.declarati
   | TypeDecl (span, AliasType (pos, i, t)) ->
     let t' = inline_constants_of_lustre_type ctx t in
     ctx, LA.TypeDecl (span, AliasType (pos, i, t'))
-  | ConstDecl (_, FreeConst _) as c -> (ctx, c)
+  | ConstDecl (span, FreeConst (pos, id, ty)) ->
+    let ty' = inline_constants_of_lustre_type ctx ty in
+    ctx, ConstDecl (span, FreeConst (pos, id, ty'))
   | ConstDecl (span, UntypedConst (pos', i, e)) ->
     let e' = simplify_expr ctx e in
     (match (TC.lookup_ty ctx i) with

diff --git a/tests/regression/success/test_const_decls.lus b/tests/regression/success/test_const_decls.lus
@@ -63,6 +63,8 @@ type m = int^5*h;
 -- Free constants, must have a type (declared later)
 const a1, a2, a3: a;
 
+const a4: subrange [-1,2] of int;
+
 -- Define constants without a type, will be inferred
 const b01 = 1;
       pi = 3.14;