Merge pull request kind2-mc#1022 from daniel-larraz/const-inlining-fix

Fix constant inlining for type declarations

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
-    ctx, 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'))
@@ -501,11 +509,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

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