Merge pull request #1112 from daniel-larraz/history-index-type

Use a refinement type for the type of history index
kind2-mc · Dec 4, 2024 · a2d99db · a2d99db
2 parents 36ce56e + cc7bd1d
commit a2d99db
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 14 deletions.
diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml
@@ -788,30 +788,32 @@ let desugar_history_in_expr ctx ctr_id prefix expr =
             in
             match kind with
             | Exists -> (
-              let c = mk_range pos bv in
+              let rng = mk_range pos bv in
+              let bound_ty = A.RefinementType (pos, (pos, bv, A.Int pos), rng) in
               StringSet.add i vars,
               StringMap.add bv hist_varid map,
-              (pos, bv, A.Int pos) :: idents,
-              c :: constrs
+              (pos, bv, bound_ty) :: idents,
+              constrs
             )
             | Forall -> (
               let idx_varid =
                 HString.mk_hstring
                   (Format.asprintf "_idx_%a" HString.pp_print_hstring bv)
               in
               let c =
-                let e' =
-                  let eq =
-                    let lhs = A.Ident(pos, bv) in
-                    let rhs =
-                      A.ArrayIndex(pos,
-                        Ident(pos, hist_varid), Ident(pos, idx_varid))
-                    in
-                    A.CompOp(pos, A.Eq, lhs, rhs)
+                let rng = mk_range pos idx_varid in
+                let bound_ty =
+                  A.RefinementType (pos, (pos, idx_varid, A.Int pos), rng)
+                in
+                let eq =
+                  let lhs = A.Ident(pos, bv) in
+                  let rhs =
+                    A.ArrayIndex(pos,
+                      Ident(pos, hist_varid), Ident(pos, idx_varid))
                   in
-                  A.BinaryOp (pos, A.And, mk_range pos idx_varid, eq)
+                  A.CompOp(pos, A.Eq, lhs, rhs)
                 in
-                A.Quantifier (pos, A.Exists, [(pos, idx_varid, A.Int pos)], e')
+                A.Quantifier (pos, A.Exists, [(pos, idx_varid, bound_ty)], eq)
               in
               let base_ty = Ctx.lookup_ty ctx i |> get in
               StringSet.add i vars, map,

diff --git a/src/lustre/lustreTypeChecker.ml b/src/lustre/lustreTypeChecker.ml
@@ -841,7 +841,7 @@ let rec infer_type_expr: tc_context -> HString.t option -> LA.expr -> (tc_type *
   | LA.Quantifier (_, _, qs, e) ->
     let* warnings1 =
       R.seq (List.map (fun (_, _, ty) ->
-        check_type_well_formed ctx Local nname true ty) qs)
+        check_type_well_formed ctx Local nname false ty) qs)
     in
     let extn_ctx = List.fold_left union ctx
                     (List.map (fun (_, i, ty) -> singleton_ty i ty) qs) in