diff --git a/src/lustre/lustreAbstractInterpretation.ml b/src/lustre/lustreAbstractInterpretation.ml index cadc1bc6f..91cec3ffa 100644 --- a/src/lustre/lustreAbstractInterpretation.ml +++ b/src/lustre/lustreAbstractInterpretation.ml @@ -151,26 +151,30 @@ let rec restrict_type_by ty restrict = match ty, restrict with | (Some Const (_, Num l1)), (Some Const (_, Num l2)) -> let l1 = Numeral.of_string (HString.string_of_hstring l1) in let l2 = Numeral.of_string (HString.string_of_hstring l2) in - let lnum = Numeral.min l1 l2 in + let lnum = Numeral.max l1 l2 in let l = HString.mk_hstring (Numeral.string_of_numeral lnum) in Some (LA.Const (dpos, Num l)), not (Numeral.equal l1 lnum) - | Some _, None -> None, true - | _ -> None, false + | (Some _ as l), None -> l, false + | None, (Some _ as l) -> l, true + | _ -> None, false in let upper, is_restricted2 = match u1, u2 with | (Some Const (_, Num u1)), (Some Const (_, Num u2)) -> let u1 = Numeral.of_string (HString.string_of_hstring u1) in let u2 = Numeral.of_string (HString.string_of_hstring u2) in - let unum = Numeral.max u1 u2 in + let unum = Numeral.min u1 u2 in let u = HString.mk_hstring (Numeral.string_of_numeral unum) in Some (LA.Const (dpos, Num u)), not (Numeral.equal u1 unum) - | Some _, None -> None, true - | _ -> None, false + | (Some _ as u), None -> u, false + | None, (Some _ as u) -> u, true + | _ -> None, false in (*IntRange (dpos, lower, upper)*) let is_restricted = is_restricted1 || is_restricted2 in - IntRange (dpos, lower, upper), is_restricted + if (lower = None && upper = None) + then Int dpos, is_restricted + else IntRange (dpos, lower, upper), is_restricted | IntRange _ as t, Int _ -> t, false | Int _, (IntRange _ as t) -> t, true | t, _ -> t, false @@ -381,28 +385,45 @@ and interpret_expr_by_type node_id ctx ty_ctx ty proj expr : LA.lustre_type = | Some l2, Some r2 -> let l, r = Numeral.max l1 l2, Numeral.min r1 r2 in subrange_from_bounds l r + | Some l2, None -> + let l = Numeral.max l1 l2 in + subrange_from_bounds l r1 + | None, Some r2 -> + let r = Numeral.min r1 r2 in + subrange_from_bounds l1 r | _ -> t) | IntRange (_, (Some Const (_, Num l1)), None) as t -> let l1 = Numeral.of_string (HString.string_of_hstring l1) in - let l2, _ = interpret_int_expr node_id ctx ty_ctx proj expr in - (match l2 with - | Some l2 -> - let l = Numeral.max l1 l2 in + let l2, r2 = interpret_int_expr node_id ctx ty_ctx proj expr in + (match l2, r2 with + | Some l2, Some r2 -> + let l = Numeral.max l1 l2 in + subrange_from_bounds l r2 + | Some l2, None -> + let l = Numeral.max l1 l2 in subrange_from_lower l + | None, Some r2 -> + subrange_from_bounds l1 r2 | _ -> t) | IntRange (_, None, (Some Const (_, Num r1))) as t -> let r1 = Numeral.of_string (HString.string_of_hstring r1) in - let _, r2 = interpret_int_expr node_id ctx ty_ctx proj expr in - (match r2 with - | Some r2 -> + let l2, r2 = interpret_int_expr node_id ctx ty_ctx proj expr in + (match l2, r2 with + | Some l2, Some r2 -> let r = Numeral.min r1 r2 in + subrange_from_bounds l2 r + | Some l2, None -> + subrange_from_bounds l2 r1 + | None, Some r2 -> + let r = Numeral.min r1 r2 in subrange_from_upper r | _ -> t) - | IntRange (_, None, None) as t -> t | Int _ | IntRange _ -> let l, r = interpret_int_expr node_id ctx ty_ctx proj expr in (match l, r with | Some l, Some r -> subrange_from_bounds l r + | Some l, None -> subrange_from_lower l + | None, Some r -> subrange_from_upper r | _ -> LA.Int dpos) | t -> t