Merge pull request kind2-mc#1109 from daniel-larraz/fix-subrange-free…

…-const

Fix handling of subrange constraints for free constants

src/lustre/lustreAstNormalizer.ml

@@ -1194,19 +1194,19 @@ and normalize_node info map
   let gids7 = locals
     |> List.filter (function
       | A.NodeVarDecl (_, (_, id, _, _)) 
-      | A.NodeConstDecl (_, FreeConst (_, id, _)) 
       | A.NodeConstDecl (_, TypedConst (_, id, _, _)) -> 
         let ty = get_type_of_id info node_id id in
         Ctx.type_contains_subrange ctx ty || Ctx.type_contains_ref ctx ty
+      | A.NodeConstDecl (_, FreeConst _)
       | A.NodeConstDecl (_, UntypedConst _) -> false)
     |> List.fold_left (fun acc l -> match l with
       | A.NodeVarDecl (p, (_, id, _, _)) 
-      | A.NodeConstDecl (p, FreeConst (_, id, _)) 
       | A.NodeConstDecl (p, TypedConst (_, id, _, _)) ->  
         let ty = get_type_of_id info node_id id in
         let ty = AIC.inline_constants_of_lustre_type info.context ty in
         let gids = union acc (mk_fresh_subrange_constraint Local info p (Some node_id) id ty)
         in union gids (mk_fresh_refinement_type_constraint Local info p (A.Ident (p, id)) ty)
+      | A.NodeConstDecl (_, FreeConst _)
       | A.NodeConstDecl (_, UntypedConst _)-> assert false)
       (empty ())
   in

src/lustre/lustreNodeGen.ml

@@ -2367,6 +2367,7 @@ and compile_const_decl ?(ghost = false) cstate ctx map scope = function
         let ty = Ctx.expand_type_syn ctx ty in
         if Ctx.type_contains_subrange ctx ty then (
           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
           in
           List.map (fun expr ->

tests/regression/success/subrange_local_free_const.lus

@@ -0,0 +1,7 @@
+type Nat = subrange [0,*] of int;
+
+node M() returns ();
+const C: Nat;
+let
+  check "P1" 0 <= C;
+tel