diff --git a/plugins/qcheck-stm/test/all_warnings.mli b/plugins/qcheck-stm/test/all_warnings.mli index b0bfab54..ae8b6563 100644 --- a/plugins/qcheck-stm/test/all_warnings.mli +++ b/plugins/qcheck-stm/test/all_warnings.mli @@ -1,13 +1,13 @@ (*@ predicate p (x : 'a) = true *) type 'a t = { v : 'a array } -(*@ mutable model contents : 'a list *) +(*@ mutable model contents : 'a sequence *) type s val make : int -> 'a -> 'a t (*@ t = make i a - ensures t.contents = List.init i (fun _ -> a) *) + ensures t.contents = Sequence.init i (fun _ -> a) *) val constant : unit (*@ constant @@ -47,7 +47,7 @@ val ghost_returned_value : 'a t -> bool val unsupported_quantification : 'a t -> bool (*@ b = unsupported_quantification t - ensures b = forall a. List.mem a t.contents -> p a *) + ensures b = forall a. Sequence.mem a t.contents -> p a *) val record_not_model_field : 'a t -> bool (*@ b = record_not_model_field t diff --git a/plugins/qcheck-stm/test/all_warnings_errors.expected b/plugins/qcheck-stm/test/all_warnings_errors.expected index d2d91a05..d8b6dbc8 100644 --- a/plugins/qcheck-stm/test/all_warnings_errors.expected +++ b/plugins/qcheck-stm/test/all_warnings_errors.expected @@ -59,14 +59,14 @@ File "all_warnings.mli", line 36, characters 0-66: 36 | val type_not_supported : 'a t -> s 37 | (*@ s = type_not_supported t *) Warning: Incomplete computation of the returned value in the specification of type_not_supported. Failure message won't be able to display the expected returned value. -File "all_warnings.mli", line 48, characters 0-140: +File "all_warnings.mli", line 48, characters 0-144: 48 | val unsupported_quantification : 'a t -> bool 49 | (*@ b = unsupported_quantification t -50 | ensures b = forall a. List.mem a t.contents -> p a *) +50 | ensures b = forall a. Sequence.mem a t.contents -> p a *) Warning: Incomplete computation of the returned value in the specification of unsupported_quantification. Failure message won't be able to display the expected returned value. -File "all_warnings.mli", line 50, characters 16-54: -50 | ensures b = forall a. List.mem a t.contents -> p a *) - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +File "all_warnings.mli", line 50, characters 16-58: +50 | ensures b = forall a. Sequence.mem a t.contents -> p a *) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping clause: unsupported quantification. File "all_warnings.mli", line 52, characters 0-111: 52 | val record_not_model_field : 'a t -> bool diff --git a/plugins/qcheck-stm/test/conjunctive_clauses.mli b/plugins/qcheck-stm/test/conjunctive_clauses.mli index 9ca67df3..86e8f8ca 100644 --- a/plugins/qcheck-stm/test/conjunctive_clauses.mli +++ b/plugins/qcheck-stm/test/conjunctive_clauses.mli @@ -1,16 +1,13 @@ type 'a t -(*@ mutable model contents : 'a list *) +(*@ mutable model contents : 'a sequence *) val make : int -> 'a -> 'a t (*@ t = make i a checks i >= 0 - ensures true /\ true && t.contents = List.init i (fun _ -> a) *) - -(*@ function set_contents (c : 'a list) (i : integer) (a : 'a) : 'a list = - List.mapi (fun j x -> if i = j then a else x) c *) + ensures true /\ true && t.contents = Sequence.init i (fun _ -> a) *) val set : 'a t -> int -> 'a -> unit (*@ set t i a - checks 0 <= i < List.length t.contents + checks 0 <= i < Sequence.length t.contents modifies t - ensures true /\ true && t.contents = set_contents (old t.contents) i a *) + ensures true /\ true && t.contents = Sequence.set (old t.contents) i a *) diff --git a/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml b/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml index 51f8ffcb..3bae1ce3 100644 --- a/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml @@ -3,31 +3,6 @@ [@@@ocaml.warning "-26-27-69-32-38"] open Conjunctive_clauses module Ortac_runtime = Ortac_runtime_qcheck_stm -let set_contents c i a_1 = - try - Ortac_runtime.Gospelstdlib.List.mapi - (fun j -> fun x -> if i = j then a_1 else x) c - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 10; - pos_bol = 580; - pos_cnum = 590 - }; - Ortac_runtime.stop = - { - pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 10; - pos_bol = 580; - pos_cnum = 637 - } - })) module SUT = (Ortac_runtime.SUT.Make)(struct type sut = char t @@ -36,15 +11,15 @@ module SUT = module ModelElt = struct type nonrec elt = { - contents: char list } + contents: char Ortac_runtime.Gospelstdlib.sequence } let init = - let i_1 = 42 - and a_2 = 'a' in + let i = 42 + and a_1 = 'a' in { contents = (try - Ortac_runtime.Gospelstdlib.List.init - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) (fun _ -> a_2) + Ortac_runtime.Gospelstdlib.Sequence.init + (Ortac_runtime.Gospelstdlib.integer_of_int i) (fun _ -> a_1) with | e -> raise @@ -55,15 +30,15 @@ module ModelElt = { pos_fname = "conjunctive_clauses.mli"; pos_lnum = 7; - pos_bol = 295; - pos_cnum = 336 + pos_bol = 303; + pos_cnum = 344 }; Ortac_runtime.stop = { pos_fname = "conjunctive_clauses.mli"; pos_lnum = 7; - pos_bol = 295; - pos_cnum = 360 + pos_bol = 303; + pos_cnum = 372 } }))) } @@ -87,30 +62,30 @@ module Spec = | Set of int * char let show_cmd cmd__001_ = match cmd__001_ with - | Make (i_1, a_2) -> + | Make (i, a_1) -> Format.asprintf "protect (fun () -> %s %a %a)" "make" - (Util.Pp.pp_int true) i_1 (Util.Pp.pp_char true) a_2 - | Set (i_2, a_3) -> + (Util.Pp.pp_int true) i (Util.Pp.pp_char true) a_1 + | Set (i_1, a_2) -> Format.asprintf "protect (fun () -> %s %a %a)" "set" - (Util.Pp.pp_int true) i_2 (Util.Pp.pp_char true) a_3 + (Util.Pp.pp_int true) i_1 (Util.Pp.pp_char true) a_2 let cleanup _ = () let arb_cmd _ = let open QCheck in make ~print:show_cmd (let open Gen in oneof - [((pure (fun i_1 -> fun a_2 -> Make (i_1, a_2))) <*> + [((pure (fun i -> fun a_1 -> Make (i, a_1))) <*> small_signed_int) <*> char; - ((pure (fun i_2 -> fun a_3 -> Set (i_2, a_3))) <*> int) <*> + ((pure (fun i_1 -> fun a_2 -> Set (i_1, a_2))) <*> int) <*> char]) let next_state cmd__002_ state__003_ = match cmd__002_ with - | Make (i_1, a_2) -> + | Make (i, a_1) -> if (try Ortac_runtime.Gospelstdlib.(>=) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.integer_of_int i) (Ortac_runtime.Gospelstdlib.integer_of_int 0) with | e -> @@ -122,15 +97,15 @@ module Spec = { pos_fname = "conjunctive_clauses.mli"; pos_lnum = 6; - pos_bol = 277; - pos_cnum = 288 + pos_bol = 285; + pos_cnum = 296 }; Ortac_runtime.stop = { pos_fname = "conjunctive_clauses.mli"; pos_lnum = 6; - pos_bol = 277; - pos_cnum = 294 + pos_bol = 285; + pos_cnum = 302 } }))) then @@ -139,9 +114,9 @@ module Spec = { contents = (try - Ortac_runtime.Gospelstdlib.List.init - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) - (fun _ -> a_2) + Ortac_runtime.Gospelstdlib.Sequence.init + (Ortac_runtime.Gospelstdlib.integer_of_int i) + (fun _ -> a_1) with | e -> raise @@ -152,32 +127,33 @@ module Spec = { pos_fname = "conjunctive_clauses.mli"; pos_lnum = 7; - pos_bol = 295; - pos_cnum = 336 + pos_bol = 303; + pos_cnum = 344 }; Ortac_runtime.stop = { pos_fname = "conjunctive_clauses.mli"; pos_lnum = 7; - pos_bol = 295; - pos_cnum = 360 + pos_bol = 303; + pos_cnum = 372 } }))) } in Model.push (Model.drop_n state__003_ 0) t_1__005_ else state__003_ - | Set (i_2, a_3) -> + | Set (i_1, a_2) -> let t_2__006_ = Model.get state__003_ 0 in if (try let __t1__008_ = Ortac_runtime.Gospelstdlib.(<=) (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int i_2) in + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in let __t2__009_ = Ortac_runtime.Gospelstdlib.(<) - (Ortac_runtime.Gospelstdlib.integer_of_int i_2) - (Ortac_runtime.Gospelstdlib.List.length t_2__006_.contents) in + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.Sequence.length + t_2__006_.contents) in __t1__008_ && __t2__009_ with | e -> @@ -188,16 +164,16 @@ module Spec = Ortac_runtime.start = { pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 14; - pos_bol = 825; - pos_cnum = 836 + pos_lnum = 11; + pos_bol = 571; + pos_cnum = 582 }; Ortac_runtime.stop = { pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 14; - pos_bol = 825; - pos_cnum = 867 + pos_lnum = 11; + pos_bol = 571; + pos_cnum = 617 } }))) then @@ -206,8 +182,9 @@ module Spec = { contents = (try - set_contents t_2__006_.contents - (Ortac_runtime.Gospelstdlib.integer_of_int i_2) a_3 + Ortac_runtime.Gospelstdlib.Sequence.set + t_2__006_.contents + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) a_2 with | e -> raise @@ -217,39 +194,39 @@ module Spec = Ortac_runtime.start = { pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 16; - pos_bol = 883; - pos_cnum = 924 + pos_lnum = 13; + pos_bol = 633; + pos_cnum = 674 }; Ortac_runtime.stop = { pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 16; - pos_bol = 883; - pos_cnum = 936 + pos_lnum = 13; + pos_bol = 633; + pos_cnum = 707 } }))) } in Model.push (Model.drop_n state__003_ 1) t_2__007_ else state__003_ let precond cmd__017_ state__018_ = - match cmd__017_ with | Make (i_1, a_2) -> true | Set (i_2, a_3) -> true + match cmd__017_ with | Make (i, a_1) -> true | Set (i_1, a_2) -> true let postcond _ _ _ = true let run cmd__019_ sut__020_ = match cmd__019_ with - | Make (i_1, a_2) -> + | Make (i, a_1) -> Res ((result sut exn), - (let res__021_ = protect (fun () -> make i_1 a_2) () in + (let res__021_ = protect (fun () -> make i a_1) () in ((match res__021_ with | Ok res -> SUT.push sut__020_ res | Error _ -> ()); res__021_))) - | Set (i_2, a_3) -> + | Set (i_1, a_2) -> Res ((result unit exn), (let t_2__022_ = SUT.pop sut__020_ in - let res__023_ = protect (fun () -> set t_2__022_ i_2 a_3) () in + let res__023_ = protect (fun () -> set t_2__022_ i_1 a_2) () in (SUT.push sut__020_ t_2__022_; res__023_))) end module STMTests = (Ortac_runtime.Make)(Spec) @@ -258,7 +235,7 @@ let ortac_show_cmd cmd__025_ state__026_ last__028_ res__027_ = let open Spec in let open STM in match (cmd__025_, res__027_) with - | (Make (i_1, a_2), Res ((Result (SUT, Exn), _), t_1)) -> + | (Make (i, a_1), Res ((Result (SUT, Exn), _), t_1)) -> let lhs = if last__028_ then "r" @@ -268,24 +245,24 @@ let ortac_show_cmd cmd__025_ state__026_ last__028_ res__027_ = | Error _ -> "_") and shift = match t_1 with | Ok _ -> 1 | Error _ -> 0 in Format.asprintf "let %s = protect (fun () -> %s %a %a)" lhs "make" - (Util.Pp.pp_int true) i_1 (Util.Pp.pp_char true) a_2 - | (Set (i_2, a_3), Res ((Result (Unit, Exn), _), _)) -> + (Util.Pp.pp_int true) i (Util.Pp.pp_char true) a_1 + | (Set (i_1, a_2), Res ((Result (Unit, Exn), _), _)) -> let lhs = if last__028_ then "r" else "_" and shift = 0 in Format.asprintf "let %s = protect (fun () -> %s %s %a %a)" lhs "set" (SUT.get_name state__026_ (0 + shift)) - (Util.Pp.pp_int true) i_2 (Util.Pp.pp_char true) a_3 + (Util.Pp.pp_int true) i_1 (Util.Pp.pp_char true) a_2 | _ -> assert false let ortac_postcond cmd__010_ state__011_ res__012_ = let open Spec in let open STM in let new_state__013_ = lazy (next_state cmd__010_ state__011_) in match (cmd__010_, res__012_) with - | (Make (i_1, a_2), Res ((Result (SUT, Exn), _), t_1)) -> + | (Make (i, a_1), Res ((Result (SUT, Exn), _), t_1)) -> (match if try Ortac_runtime.Gospelstdlib.(>=) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.integer_of_int i) (Ortac_runtime.Gospelstdlib.integer_of_int 0) with | e -> @@ -297,15 +274,15 @@ let ortac_postcond cmd__010_ state__011_ res__012_ = { pos_fname = "conjunctive_clauses.mli"; pos_lnum = 6; - pos_bol = 277; - pos_cnum = 288 + pos_bol = 285; + pos_cnum = 296 }; Ortac_runtime.stop = { pos_fname = "conjunctive_clauses.mli"; pos_lnum = 6; - pos_bol = 277; - pos_cnum = 294 + pos_bol = 285; + pos_cnum = 302 } })) then None @@ -320,15 +297,15 @@ let ortac_postcond cmd__010_ state__011_ res__012_ = { pos_fname = "conjunctive_clauses.mli"; pos_lnum = 6; - pos_bol = 277; - pos_cnum = 288 + pos_bol = 285; + pos_cnum = 296 }; Ortac_runtime.stop = { pos_fname = "conjunctive_clauses.mli"; pos_lnum = 6; - pos_bol = 277; - pos_cnum = 294 + pos_bol = 285; + pos_cnum = 302 } })]) with @@ -340,7 +317,7 @@ let ortac_postcond cmd__010_ state__011_ res__012_ = if (try Ortac_runtime.Gospelstdlib.(>=) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.integer_of_int i) (Ortac_runtime.Gospelstdlib.integer_of_int 0) with | e -> @@ -352,15 +329,15 @@ let ortac_postcond cmd__010_ state__011_ res__012_ = { pos_fname = "conjunctive_clauses.mli"; pos_lnum = 6; - pos_bol = 277; - pos_cnum = 288 + pos_bol = 285; + pos_cnum = 296 }; Ortac_runtime.stop = { pos_fname = "conjunctive_clauses.mli"; pos_lnum = 6; - pos_bol = 277; - pos_cnum = 294 + pos_bol = 285; + pos_cnum = 302 } }))) then None @@ -376,29 +353,29 @@ let ortac_postcond cmd__010_ state__011_ res__012_ = { pos_fname = "conjunctive_clauses.mli"; pos_lnum = 6; - pos_bol = 277; - pos_cnum = 288 + pos_bol = 285; + pos_cnum = 296 }; Ortac_runtime.stop = { pos_fname = "conjunctive_clauses.mli"; pos_lnum = 6; - pos_bol = 277; - pos_cnum = 294 + pos_bol = 285; + pos_cnum = 302 } })]))) - | (Set (i_2, a_3), Res ((Result (Unit, Exn), _), res)) -> + | (Set (i_1, a_2), Res ((Result (Unit, Exn), _), res)) -> (match if let tmp__014_ = Model.get state__011_ 0 in try let __t1__015_ = Ortac_runtime.Gospelstdlib.(<=) (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int i_2) in + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in let __t2__016_ = Ortac_runtime.Gospelstdlib.(<) - (Ortac_runtime.Gospelstdlib.integer_of_int i_2) - (Ortac_runtime.Gospelstdlib.List.length + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.Sequence.length tmp__014_.contents) in __t1__015_ && __t2__016_ with @@ -410,16 +387,16 @@ let ortac_postcond cmd__010_ state__011_ res__012_ = Ortac_runtime.start = { pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 14; - pos_bol = 825; - pos_cnum = 836 + pos_lnum = 11; + pos_bol = 571; + pos_cnum = 582 }; Ortac_runtime.stop = { pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 14; - pos_bol = 825; - pos_cnum = 867 + pos_lnum = 11; + pos_bol = 571; + pos_cnum = 617 } })) then None @@ -428,21 +405,21 @@ let ortac_postcond cmd__010_ state__011_ res__012_ = (Ortac_runtime.report "Conjunctive_clauses" "make 42 'a'" (Ortac_runtime.Exception "Invalid_argument") "set" - [("0 <= i < List.length t.contents", + [("0 <= i < Sequence.length t.contents", { Ortac_runtime.start = { pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 14; - pos_bol = 825; - pos_cnum = 836 + pos_lnum = 11; + pos_bol = 571; + pos_cnum = 582 }; Ortac_runtime.stop = { pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 14; - pos_bol = 825; - pos_cnum = 867 + pos_lnum = 11; + pos_bol = 571; + pos_cnum = 617 } })]) with @@ -457,11 +434,11 @@ let ortac_postcond cmd__010_ state__011_ res__012_ = let __t1__015_ = Ortac_runtime.Gospelstdlib.(<=) (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int i_2) in + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in let __t2__016_ = Ortac_runtime.Gospelstdlib.(<) - (Ortac_runtime.Gospelstdlib.integer_of_int i_2) - (Ortac_runtime.Gospelstdlib.List.length + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.Sequence.length tmp__014_.contents) in __t1__015_ && __t2__016_ with @@ -473,16 +450,16 @@ let ortac_postcond cmd__010_ state__011_ res__012_ = Ortac_runtime.start = { pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 14; - pos_bol = 825; - pos_cnum = 836 + pos_lnum = 11; + pos_bol = 571; + pos_cnum = 582 }; Ortac_runtime.stop = { pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 14; - pos_bol = 825; - pos_cnum = 867 + pos_lnum = 11; + pos_bol = 571; + pos_cnum = 617 } }))) then None @@ -491,21 +468,21 @@ let ortac_postcond cmd__010_ state__011_ res__012_ = (Ortac_runtime.report "Conjunctive_clauses" "make 42 'a'" (Ortac_runtime.Exception "Invalid_argument") "set" - [("0 <= i < List.length t.contents", + [("0 <= i < Sequence.length t.contents", { Ortac_runtime.start = { pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 14; - pos_bol = 825; - pos_cnum = 836 + pos_lnum = 11; + pos_bol = 571; + pos_cnum = 582 }; Ortac_runtime.stop = { pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 14; - pos_bol = 825; - pos_cnum = 867 + pos_lnum = 11; + pos_bol = 571; + pos_cnum = 617 } })]))) | _ -> None diff --git a/plugins/qcheck-stm/test/hashtbl.mli b/plugins/qcheck-stm/test/hashtbl.mli index 8b10a514..d0d376f7 100644 --- a/plugins/qcheck-stm/test/hashtbl.mli +++ b/plugins/qcheck-stm/test/hashtbl.mli @@ -1,20 +1,20 @@ type (!'a, !'b) t -(*@ mutable model contents : ('a * 'b) list *) +(*@ mutable model contents : ('a * 'b) sequence *) val create : ?random:(* thwart tools/sync_stdlib_docs *) bool -> int -> ('a, 'b) t (*@ h = create ?random size - ensures h.contents = [] *) + ensures h.contents = Sequence.empty *) val clear : ('a, 'b) t -> unit (*@ clear h modifies h - ensures h.contents = [] *) + ensures h.contents = Sequence.empty *) val reset : ('a, 'b) t -> unit (*@ reset h modifies h - ensures h.contents = [] *) + ensures h.contents = Sequence.empty *) val copy : ('a, 'b) t -> ('a, 'b) t (*@ h2 = copy h1 @@ -23,19 +23,19 @@ val copy : ('a, 'b) t -> ('a, 'b) t val add : ('a, 'b) t -> 'a -> 'b -> unit (*@ add h a b modifies h - ensures h.contents = (a, b) :: old h.contents *) + ensures h.contents = Sequence.cons (a, b) (old h.contents) *) val find : ('a, 'b) t -> 'a -> 'b (*@ b = find h a - raises Not_found -> forall x. not (List.mem (a, x) h.contents) - raises Not_found -> not (List.mem a (List.map fst h.contents)) - ensures List.mem (a, b) h.contents *) + raises Not_found -> forall x. not (Sequence.mem h.contents (a, x)) + raises Not_found -> not (Sequence.mem (Sequence.map fst h.contents) a) + ensures Sequence.mem h.contents (a, b) *) val find_opt : ('a, 'b) t -> 'a -> 'b option (*@ o = find_opt h a ensures match o with - | None -> not (List.mem a (List.map fst h.contents)) - | Some b -> List.mem (a, b) h.contents *) + | None -> not (Sequence.mem (Sequence.map fst h.contents) a) + | Some b -> Sequence.mem h.contents (a, b) *) val find_all : ('a, 'b) t -> 'a -> 'b list (*@ bs = find_all h a @@ -43,12 +43,14 @@ val find_all : ('a, 'b) t -> 'a -> 'b list val mem : ('a, 'b) t -> 'a -> bool (*@ b = mem h a - ensures b = List.mem a (List.map fst h.contents) *) + ensures b = Sequence.mem (Sequence.map fst h.contents) a *) -(*@ function rec remove_first (x: 'a) (xs : ('a * 'b) list) : ('a * 'b) list = - match xs with - | (a, b) :: xs -> if a = x then xs else (a, b) :: (remove_first x xs) - | [] -> [] *) +(*@ function rec remove_first (x: 'a) (xs : ('a * 'b) sequence) : ('a * 'b) sequence = + if Sequence.empty = xs + then xs + else if fst (Sequence.hd xs) = x + then Sequence.tl xs + else Sequence.cons (Sequence.hd xs) (remove_first x (Sequence.tl xs)) *) val remove : ('a, 'b) t -> 'a -> unit (*@ remove h a @@ -58,7 +60,7 @@ val remove : ('a, 'b) t -> 'a -> unit val replace : ('a, 'b) t -> 'a -> 'b -> unit (*@ replace h a b modifies h - ensures h.contents = (a, b) :: remove_first a (old h.contents) *) + ensures h.contents = Sequence.cons (a, b) (remove_first a (old h.contents)) *) val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit val filter_map_inplace : ('a -> 'b -> 'b option) -> ('a, 'b) t -> unit @@ -73,7 +75,7 @@ val filter_map_inplace : ('a -> 'b -> 'b option) -> ('a, 'b) t -> unit val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c val length : ('a, 'b) t -> int (*@ i = length h - ensures i = List.length h.contents *) + ensures i = Sequence.length h.contents *) val randomize : unit -> unit val is_randomized : unit -> bool diff --git a/plugins/qcheck-stm/test/hashtbl_errors.expected b/plugins/qcheck-stm/test/hashtbl_errors.expected index 0a31f27c..7b9e508d 100644 --- a/plugins/qcheck-stm/test/hashtbl_errors.expected +++ b/plugins/qcheck-stm/test/hashtbl_errors.expected @@ -1,105 +1,105 @@ -File "hashtbl.mli", line 63, characters 12-28: -63 | val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit +File "hashtbl.mli", line 65, characters 12-28: +65 | val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit ^^^^^^^^^^^^^^^^ Warning: Skipping iter: functions are not supported yet as arguments. -File "hashtbl.mli", line 64, characters 26-47: -64 | val filter_map_inplace : ('a -> 'b -> 'b option) -> ('a, 'b) t -> unit +File "hashtbl.mli", line 66, characters 26-47: +66 | val filter_map_inplace : ('a -> 'b -> 'b option) -> ('a, 'b) t -> unit ^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping filter_map_inplace: functions are not supported yet as arguments. -File "hashtbl.mli", line 73, characters 12-32: -73 | val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c +File "hashtbl.mli", line 75, characters 12-32: +75 | val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c ^^^^^^^^^^^^^^^^^^^^ Warning: Skipping fold: functions are not supported yet as arguments. -File "hashtbl.mli", line 78, characters 0-28: -78 | val randomize : unit -> unit +File "hashtbl.mli", line 80, characters 0-28: +80 | val randomize : unit -> unit ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping randomize: functions without specifications cannot be tested. -File "hashtbl.mli", line 79, characters 0-32: -79 | val is_randomized : unit -> bool +File "hashtbl.mli", line 81, characters 0-32: +81 | val is_randomized : unit -> bool ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping is_randomized: functions without specifications cannot be tested. -File "hashtbl.mli", line 81, characters 0-92: -81 | val rebuild : -82 | ?random:(* thwart tools/sync_stdlib_docs *) bool -> ('a, 'b) t -> ('a, 'b) t +File "hashtbl.mli", line 83, characters 0-92: +83 | val rebuild : +84 | ?random:(* thwart tools/sync_stdlib_docs *) bool -> ('a, 'b) t -> ('a, 'b) t Warning: Skipping rebuild: functions without specifications cannot be tested. -File "hashtbl.mli", line 96, characters 0-36: -96 | val stats : ('a, 'b) t -> statistics +File "hashtbl.mli", line 98, characters 0-36: +98 | val stats : ('a, 'b) t -> statistics ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping stats: functions without specifications cannot be tested. -File "hashtbl.mli", line 97, characters 0-42: -97 | val to_seq : ('a, 'b) t -> ('a * 'b) Seq.t +File "hashtbl.mli", line 99, characters 0-42: +99 | val to_seq : ('a, 'b) t -> ('a * 'b) Seq.t ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping to_seq: functions without specifications cannot be tested. -File "hashtbl.mli", line 98, characters 0-39: -98 | val to_seq_keys : ('a, _) t -> 'a Seq.t - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +File "hashtbl.mli", line 100, characters 0-39: +100 | val to_seq_keys : ('a, _) t -> 'a Seq.t + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping to_seq_keys: functions without specifications cannot be tested. -File "hashtbl.mli", line 99, characters 0-41: -99 | val to_seq_values : (_, 'b) t -> 'b Seq.t - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +File "hashtbl.mli", line 101, characters 0-41: +101 | val to_seq_values : (_, 'b) t -> 'b Seq.t + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping to_seq_values: functions without specifications cannot be tested. -File "hashtbl.mli", line 100, characters 0-51: -100 | val add_seq : ('a, 'b) t -> ('a * 'b) Seq.t -> unit +File "hashtbl.mli", line 102, characters 0-51: +102 | val add_seq : ('a, 'b) t -> ('a * 'b) Seq.t -> unit ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping add_seq: functions without specifications cannot be tested. -File "hashtbl.mli", line 101, characters 0-55: -101 | val replace_seq : ('a, 'b) t -> ('a * 'b) Seq.t -> unit +File "hashtbl.mli", line 103, characters 0-55: +103 | val replace_seq : ('a, 'b) t -> ('a * 'b) Seq.t -> unit ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping replace_seq: functions without specifications cannot be tested. -File "hashtbl.mli", line 102, characters 0-42: -102 | val of_seq : ('a * 'b) Seq.t -> ('a, 'b) t +File "hashtbl.mli", line 104, characters 0-42: +104 | val of_seq : ('a * 'b) Seq.t -> ('a, 'b) t ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping of_seq: functions without specifications cannot be tested. -File "hashtbl.mli", line 103, characters 0-20: -103 | val hash : 'a -> int +File "hashtbl.mli", line 105, characters 0-20: +105 | val hash : 'a -> int ^^^^^^^^^^^^^^^^^^^^ Warning: Skipping hash: functions without specifications cannot be tested. -File "hashtbl.mli", line 104, characters 0-34: -104 | val seeded_hash : int -> 'a -> int +File "hashtbl.mli", line 106, characters 0-34: +106 | val seeded_hash : int -> 'a -> int ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping seeded_hash: functions without specifications cannot be tested. -File "hashtbl.mli", line 105, characters 0-40: -105 | val hash_param : int -> int -> 'a -> int +File "hashtbl.mli", line 107, characters 0-40: +107 | val hash_param : int -> int -> 'a -> int ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping hash_param: functions without specifications cannot be tested. -File "hashtbl.mli", line 106, characters 0-54: -106 | val seeded_hash_param : int -> int -> int -> 'a -> int +File "hashtbl.mli", line 108, characters 0-54: +108 | val seeded_hash_param : int -> int -> int -> 'a -> int ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping seeded_hash_param: functions without specifications cannot be tested. -File "hashtbl.mli", line 28, characters 0-226: +File "hashtbl.mli", line 28, characters 0-242: 28 | val find : ('a, 'b) t -> 'a -> 'b 29 | (*@ b = find h a -30 | raises Not_found -> forall x. not (List.mem (a, x) h.contents) -31 | raises Not_found -> not (List.mem a (List.map fst h.contents)) -32 | ensures List.mem (a, b) h.contents *) +30 | raises Not_found -> forall x. not (Sequence.mem h.contents (a, x)) +31 | raises Not_found -> not (Sequence.mem (Sequence.map fst h.contents) a) +32 | ensures Sequence.mem h.contents (a, b) *) Warning: Incomplete computation of the returned value in the specification of find. Failure message won't be able to display the expected returned value. -File "hashtbl.mli", line 30, characters 24-66: -30 | raises Not_found -> forall x. not (List.mem (a, x) h.contents) - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +File "hashtbl.mli", line 30, characters 24-70: +30 | raises Not_found -> forall x. not (Sequence.mem h.contents (a, x)) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Skipping clause: unsupported quantification. -File "hashtbl.mli", line 34, characters 0-197: +File "hashtbl.mli", line 34, characters 0-209: 34 | val find_opt : ('a, 'b) t -> 'a -> 'b option 35 | (*@ o = find_opt h a 36 | ensures match o with -37 | | None -> not (List.mem a (List.map fst h.contents)) -38 | | Some b -> List.mem (a, b) h.contents *) +37 | | None -> not (Sequence.mem (Sequence.map fst h.contents) a) +38 | | Some b -> Sequence.mem h.contents (a, b) *) Warning: Incomplete computation of the returned value in the specification of find_opt. Failure message won't be able to display the expected returned value. File "hashtbl.mli", line 40, characters 0-162: 40 | val find_all : ('a, 'b) t -> 'a -> 'b list 41 | (*@ bs = find_all h a 42 | ensures bs = Sequence.filter_map (fun (x, y) -> if x = a then Some y else None) h.contents *) Warning: Incomplete computation of the returned value in the specification of find_all. Failure message won't be able to display the expected returned value. -File "hashtbl.mli", line 44, characters 0-106: +File "hashtbl.mli", line 44, characters 0-114: 44 | val mem : ('a, 'b) t -> 'a -> bool 45 | (*@ b = mem h a -46 | ensures b = List.mem a (List.map fst h.contents) *) +46 | ensures b = Sequence.mem (Sequence.map fst h.contents) a *) Warning: Incomplete computation of the returned value in the specification of mem. Failure message won't be able to display the expected returned value. diff --git a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml index 6071bbb6..fa9dcd21 100644 --- a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml @@ -3,12 +3,20 @@ [@@@ocaml.warning "-26-27-69-32-38"] open Hashtbl module Ortac_runtime = Ortac_runtime_qcheck_stm -let rec remove_first x xs_1 = +let rec remove_first x xs = try - match xs_1 with - | (a_1, b_1)::xs -> - if a_1 = x then xs else (a_1, b_1) :: (remove_first x xs) - | [] -> [] + if Ortac_runtime.Gospelstdlib.Sequence.empty = xs + then xs + else + if + (Ortac_runtime.Gospelstdlib.fst + (Ortac_runtime.Gospelstdlib.Sequence.hd xs)) + = x + then Ortac_runtime.Gospelstdlib.Sequence.tl xs + else + Ortac_runtime.Gospelstdlib.Sequence.cons + (Ortac_runtime.Gospelstdlib.Sequence.hd xs) + (remove_first x (Ortac_runtime.Gospelstdlib.Sequence.tl xs)) with | e -> raise @@ -19,15 +27,15 @@ let rec remove_first x xs_1 = { pos_fname = "hashtbl.mli"; pos_lnum = 49; - pos_bol = 2390; - pos_cnum = 2396 + pos_bol = 2556; + pos_cnum = 2562 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; - pos_lnum = 51; - pos_bol = 2486; - pos_cnum = 2502 + pos_lnum = 53; + pos_bol = 2669; + pos_cnum = 2749 } })) module SUT = @@ -37,14 +45,15 @@ module SUT = end) module ModelElt = struct - type nonrec elt = { - contents: (char * int) list } + type nonrec elt = + { + contents: (char * int) Ortac_runtime.Gospelstdlib.sequence } let init = let random = false and size = 16 in { contents = - (try [] + (try Ortac_runtime.Gospelstdlib.Sequence.empty with | e -> raise @@ -55,15 +64,15 @@ module ModelElt = { pos_fname = "hashtbl.mli"; pos_lnum = 7; - pos_bol = 318; - pos_cnum = 343 + pos_bol = 326; + pos_cnum = 351 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 7; - pos_bol = 318; - pos_cnum = 345 + pos_bol = 326; + pos_cnum = 365 } }))) } @@ -103,23 +112,23 @@ module Spec = | Clear -> Format.asprintf "%s " "clear" | Reset -> Format.asprintf "%s " "reset" | Copy -> Format.asprintf "%s " "copy" - | Add (a_2, b_2) -> - Format.asprintf "%s %a %a" "add" (Util.Pp.pp_char true) a_2 - (Util.Pp.pp_int true) b_2 - | Find a_3 -> + | Add (a_1, b_1) -> + Format.asprintf "%s %a %a" "add" (Util.Pp.pp_char true) a_1 + (Util.Pp.pp_int true) b_1 + | Find a_2 -> Format.asprintf "protect (fun () -> %s %a)" "find" - (Util.Pp.pp_char true) a_3 - | Find_opt a_4 -> - Format.asprintf "%s %a" "find_opt" (Util.Pp.pp_char true) a_4 - | Find_all a_5 -> - Format.asprintf "%s %a" "find_all" (Util.Pp.pp_char true) a_5 - | Mem a_6 -> - Format.asprintf "%s %a" "mem" (Util.Pp.pp_char true) a_6 - | Remove a_7 -> - Format.asprintf "%s %a" "remove" (Util.Pp.pp_char true) a_7 - | Replace (a_8, b_3) -> + (Util.Pp.pp_char true) a_2 + | Find_opt a_3 -> + Format.asprintf "%s %a" "find_opt" (Util.Pp.pp_char true) a_3 + | Find_all a_4 -> + Format.asprintf "%s %a" "find_all" (Util.Pp.pp_char true) a_4 + | Mem a_5 -> + Format.asprintf "%s %a" "mem" (Util.Pp.pp_char true) a_5 + | Remove a_6 -> + Format.asprintf "%s %a" "remove" (Util.Pp.pp_char true) a_6 + | Replace (a_7, b_2) -> Format.asprintf "%s %a %a" "replace" (Util.Pp.pp_char true) - a_8 (Util.Pp.pp_int true) b_3 + a_7 (Util.Pp.pp_int true) b_2 | Length -> Format.asprintf "%s " "length" let cleanup _ = () let arb_cmd _ = @@ -133,14 +142,14 @@ module Spec = pure Clear; pure Reset; pure Copy; - ((pure (fun a_2 -> fun b_2 -> Add (a_2, b_2))) <*> char) <*> + ((pure (fun a_1 -> fun b_1 -> Add (a_1, b_1))) <*> char) <*> int; - (pure (fun a_3 -> Find a_3)) <*> char; - (pure (fun a_4 -> Find_opt a_4)) <*> char; - (pure (fun a_5 -> Find_all a_5)) <*> char; - (pure (fun a_6 -> Mem a_6)) <*> char; - (pure (fun a_7 -> Remove a_7)) <*> char; - ((pure (fun a_8 -> fun b_3 -> Replace (a_8, b_3))) <*> char) + (pure (fun a_2 -> Find a_2)) <*> char; + (pure (fun a_3 -> Find_opt a_3)) <*> char; + (pure (fun a_4 -> Find_all a_4)) <*> char; + (pure (fun a_5 -> Mem a_5)) <*> char; + (pure (fun a_6 -> Remove a_6)) <*> char; + ((pure (fun a_7 -> fun b_2 -> Replace (a_7, b_2))) <*> char) <*> int; pure Length]) let next_state cmd__002_ state__003_ = @@ -150,7 +159,7 @@ module Spec = let open ModelElt in { contents = - (try [] + (try Ortac_runtime.Gospelstdlib.Sequence.empty with | e -> raise @@ -161,15 +170,15 @@ module Spec = { pos_fname = "hashtbl.mli"; pos_lnum = 7; - pos_bol = 318; - pos_cnum = 343 + pos_bol = 326; + pos_cnum = 351 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 7; - pos_bol = 318; - pos_cnum = 345 + pos_bol = 326; + pos_cnum = 365 } }))) } in @@ -180,7 +189,7 @@ module Spec = let open ModelElt in { contents = - (try [] + (try Ortac_runtime.Gospelstdlib.Sequence.empty with | e -> raise @@ -191,15 +200,15 @@ module Spec = { pos_fname = "hashtbl.mli"; pos_lnum = 12; - pos_bol = 486; - pos_cnum = 511 + pos_bol = 518; + pos_cnum = 543 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 12; - pos_bol = 486; - pos_cnum = 513 + pos_bol = 518; + pos_cnum = 557 } }))) } in @@ -210,7 +219,7 @@ module Spec = let open ModelElt in { contents = - (try [] + (try Ortac_runtime.Gospelstdlib.Sequence.empty with | e -> raise @@ -221,15 +230,15 @@ module Spec = { pos_fname = "hashtbl.mli"; pos_lnum = 17; - pos_bol = 655; - pos_cnum = 680 + pos_bol = 711; + pos_cnum = 736 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 17; - pos_bol = 655; - pos_cnum = 682 + pos_bol = 711; + pos_cnum = 750 } }))) } in @@ -251,28 +260,30 @@ module Spec = { pos_fname = "hashtbl.mli"; pos_lnum = 21; - pos_bol = 819; - pos_cnum = 845 + pos_bol = 899; + pos_cnum = 925 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 21; - pos_bol = 819; - pos_cnum = 856 + pos_bol = 899; + pos_cnum = 936 } }))) } and h1__012_ = h1__010_ in Model.push (Model.push (Model.drop_n state__003_ 1) h1__012_) h2__013_ - | Add (a_2, b_2) -> + | Add (a_1, b_1) -> let h_3__014_ = Model.get state__003_ 0 in let h_3__015_ = let open ModelElt in { contents = - (try (a_2, b_2) :: h_3__014_.contents + (try + Ortac_runtime.Gospelstdlib.Sequence.cons (a_1, b_1) + h_3__014_.contents with | e -> raise @@ -283,42 +294,42 @@ module Spec = { pos_fname = "hashtbl.mli"; pos_lnum = 26; - pos_bol = 1020; - pos_cnum = 1045 + pos_bol = 1100; + pos_cnum = 1125 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 26; - pos_bol = 1020; - pos_cnum = 1069 + pos_bol = 1100; + pos_cnum = 1162 } }))) } in Model.push (Model.drop_n state__003_ 1) h_3__015_ - | Find a_3 -> + | Find a_2 -> let h_4__016_ = Model.get state__003_ 0 in let h_4__017_ = h_4__016_ in Model.push (Model.drop_n state__003_ 1) h_4__017_ - | Find_opt a_4 -> + | Find_opt a_3 -> let h_5__018_ = Model.get state__003_ 0 in let h_5__019_ = h_5__018_ in Model.push (Model.drop_n state__003_ 1) h_5__019_ - | Find_all a_5 -> + | Find_all a_4 -> let h_6__020_ = Model.get state__003_ 0 in let h_6__021_ = h_6__020_ in Model.push (Model.drop_n state__003_ 1) h_6__021_ - | Mem a_6 -> + | Mem a_5 -> let h_7__022_ = Model.get state__003_ 0 in let h_7__023_ = h_7__022_ in Model.push (Model.drop_n state__003_ 1) h_7__023_ - | Remove a_7 -> + | Remove a_6 -> let h_8__024_ = Model.get state__003_ 0 in let h_8__025_ = let open ModelElt in { contents = - (try remove_first a_7 h_8__024_.contents + (try remove_first a_6 h_8__024_.contents with | e -> raise @@ -328,27 +339,29 @@ module Spec = Ortac_runtime.start = { pos_fname = "hashtbl.mli"; - pos_lnum = 56; - pos_bol = 2643; - pos_cnum = 2668 + pos_lnum = 58; + pos_bol = 2954; + pos_cnum = 2979 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; - pos_lnum = 56; - pos_bol = 2643; - pos_cnum = 2680 + pos_lnum = 58; + pos_bol = 2954; + pos_cnum = 2991 } }))) } in Model.push (Model.drop_n state__003_ 1) h_8__025_ - | Replace (a_8, b_3) -> + | Replace (a_7, b_2) -> let h_9__026_ = Model.get state__003_ 0 in let h_9__027_ = let open ModelElt in { contents = - (try (a_8, b_3) :: (remove_first a_8 h_9__026_.contents) + (try + Ortac_runtime.Gospelstdlib.Sequence.cons (a_7, b_2) + (remove_first a_7 h_9__026_.contents) with | e -> raise @@ -358,16 +371,16 @@ module Spec = Ortac_runtime.start = { pos_fname = "hashtbl.mli"; - pos_lnum = 61; - pos_bol = 2890; - pos_cnum = 2915 + pos_lnum = 63; + pos_bol = 3201; + pos_cnum = 3226 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; - pos_lnum = 61; - pos_bol = 2890; - pos_cnum = 2956 + pos_lnum = 63; + pos_bol = 3201; + pos_cnum = 3280 } }))) } in @@ -382,13 +395,13 @@ module Spec = | Clear -> true | Reset -> true | Copy -> true - | Add (a_2, b_2) -> true - | Find a_3 -> true - | Find_opt a_4 -> true - | Find_all a_5 -> true - | Mem a_6 -> true - | Remove a_7 -> true - | Replace (a_8, b_3) -> true + | Add (a_1, b_1) -> true + | Find a_2 -> true + | Find_opt a_3 -> true + | Find_all a_4 -> true + | Mem a_5 -> true + | Remove a_6 -> true + | Replace (a_7, b_2) -> true | Length -> true let postcond _ _ _ = true let run cmd__063_ sut__064_ = @@ -418,47 +431,47 @@ module Spec = (SUT.push sut__064_ h1__070_; SUT.push sut__064_ res__071_; res__071_))) - | Add (a_2, b_2) -> + | Add (a_1, b_1) -> Res (unit, (let h_3__072_ = SUT.pop sut__064_ in - let res__073_ = add h_3__072_ a_2 b_2 in + let res__073_ = add h_3__072_ a_1 b_1 in (SUT.push sut__064_ h_3__072_; res__073_))) - | Find a_3 -> + | Find a_2 -> Res ((result int exn), (let h_4__074_ = SUT.pop sut__064_ in - let res__075_ = protect (fun () -> find h_4__074_ a_3) () in + let res__075_ = protect (fun () -> find h_4__074_ a_2) () in (SUT.push sut__064_ h_4__074_; res__075_))) - | Find_opt a_4 -> + | Find_opt a_3 -> Res ((option int), (let h_5__076_ = SUT.pop sut__064_ in - let res__077_ = find_opt h_5__076_ a_4 in + let res__077_ = find_opt h_5__076_ a_3 in (SUT.push sut__064_ h_5__076_; res__077_))) - | Find_all a_5 -> + | Find_all a_4 -> Res ((list int), (let h_6__078_ = SUT.pop sut__064_ in - let res__079_ = find_all h_6__078_ a_5 in + let res__079_ = find_all h_6__078_ a_4 in (SUT.push sut__064_ h_6__078_; res__079_))) - | Mem a_6 -> + | Mem a_5 -> Res (bool, (let h_7__080_ = SUT.pop sut__064_ in - let res__081_ = mem h_7__080_ a_6 in + let res__081_ = mem h_7__080_ a_5 in (SUT.push sut__064_ h_7__080_; res__081_))) - | Remove a_7 -> + | Remove a_6 -> Res (unit, (let h_8__082_ = SUT.pop sut__064_ in - let res__083_ = remove h_8__082_ a_7 in + let res__083_ = remove h_8__082_ a_6 in (SUT.push sut__064_ h_8__082_; res__083_))) - | Replace (a_8, b_3) -> + | Replace (a_7, b_2) -> Res (unit, (let h_9__084_ = SUT.pop sut__064_ in - let res__085_ = replace h_9__084_ a_8 b_3 in + let res__085_ = replace h_9__084_ a_7 b_2 in (SUT.push sut__064_ h_9__084_; res__085_))) | Length -> Res @@ -493,43 +506,43 @@ let ortac_show_cmd cmd__089_ state__090_ last__092_ res__091_ = and shift = 1 in Format.asprintf "let %s = %s %s" lhs "copy" (SUT.get_name state__090_ (0 + shift)) - | (Add (a_2, b_2), Res ((Unit, _), _)) -> + | (Add (a_1, b_1), Res ((Unit, _), _)) -> let lhs = if last__092_ then "r" else "_" and shift = 0 in Format.asprintf "let %s = %s %s %a %a" lhs "add" - (SUT.get_name state__090_ (0 + shift)) (Util.Pp.pp_char true) a_2 - (Util.Pp.pp_int true) b_2 - | (Find a_3, Res ((Result (Int, Exn), _), _)) -> + (SUT.get_name state__090_ (0 + shift)) (Util.Pp.pp_char true) a_1 + (Util.Pp.pp_int true) b_1 + | (Find a_2, Res ((Result (Int, Exn), _), _)) -> let lhs = if last__092_ then "r" else "_" and shift = 0 in Format.asprintf "let %s = protect (fun () -> %s %s %a)" lhs "find" - (SUT.get_name state__090_ (0 + shift)) (Util.Pp.pp_char true) a_3 - | (Find_opt a_4, Res ((Option (Int), _), _)) -> + (SUT.get_name state__090_ (0 + shift)) (Util.Pp.pp_char true) a_2 + | (Find_opt a_3, Res ((Option (Int), _), _)) -> let lhs = if last__092_ then "r" else "_" and shift = 0 in Format.asprintf "let %s = %s %s %a" lhs "find_opt" - (SUT.get_name state__090_ (0 + shift)) (Util.Pp.pp_char true) a_4 - | (Find_all a_5, Res ((List (Int), _), _)) -> + (SUT.get_name state__090_ (0 + shift)) (Util.Pp.pp_char true) a_3 + | (Find_all a_4, Res ((List (Int), _), _)) -> let lhs = if last__092_ then "r" else "_" and shift = 0 in Format.asprintf "let %s = %s %s %a" lhs "find_all" - (SUT.get_name state__090_ (0 + shift)) (Util.Pp.pp_char true) a_5 - | (Mem a_6, Res ((Bool, _), _)) -> + (SUT.get_name state__090_ (0 + shift)) (Util.Pp.pp_char true) a_4 + | (Mem a_5, Res ((Bool, _), _)) -> let lhs = if last__092_ then "r" else "_" and shift = 0 in Format.asprintf "let %s = %s %s %a" lhs "mem" - (SUT.get_name state__090_ (0 + shift)) (Util.Pp.pp_char true) a_6 - | (Remove a_7, Res ((Unit, _), _)) -> + (SUT.get_name state__090_ (0 + shift)) (Util.Pp.pp_char true) a_5 + | (Remove a_6, Res ((Unit, _), _)) -> let lhs = if last__092_ then "r" else "_" and shift = 0 in Format.asprintf "let %s = %s %s %a" lhs "remove" - (SUT.get_name state__090_ (0 + shift)) (Util.Pp.pp_char true) a_7 - | (Replace (a_8, b_3), Res ((Unit, _), _)) -> + (SUT.get_name state__090_ (0 + shift)) (Util.Pp.pp_char true) a_6 + | (Replace (a_7, b_2), Res ((Unit, _), _)) -> let lhs = if last__092_ then "r" else "_" and shift = 0 in Format.asprintf "let %s = %s %s %a %a" lhs "replace" - (SUT.get_name state__090_ (0 + shift)) (Util.Pp.pp_char true) a_8 - (Util.Pp.pp_int true) b_3 + (SUT.get_name state__090_ (0 + shift)) (Util.Pp.pp_char true) a_7 + (Util.Pp.pp_int true) b_2 | (Length, Res ((Int, _), _)) -> let lhs = if last__092_ then "r" else "_" and shift = 0 in @@ -545,17 +558,17 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = | (Clear, Res ((Unit, _), _)) -> None | (Reset, Res ((Unit, _), _)) -> None | (Copy, Res ((SUT, _), h2)) -> None - | (Add (a_2, b_2), Res ((Unit, _), _)) -> None - | (Find a_3, Res ((Result (Int, Exn), _), b_4)) -> - (match b_4 with - | Ok b_4 -> + | (Add (a_1, b_1), Res ((Unit, _), _)) -> None + | (Find a_2, Res ((Result (Int, Exn), _), b_3)) -> + (match b_3 with + | Ok b_3 -> if let h_old__038_ = Model.get state__031_ 0 and h_new__039_ = lazy (Model.get (Lazy.force new_state__033_) 0) in (try - Ortac_runtime.Gospelstdlib.List.mem (a_3, b_4) - (Lazy.force h_new__039_).contents + Ortac_runtime.Gospelstdlib.Sequence.mem + (Lazy.force h_new__039_).contents (a_2, b_3) with | e -> raise @@ -566,15 +579,15 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = { pos_fname = "hashtbl.mli"; pos_lnum = 32; - pos_bol = 1360; - pos_cnum = 1372 + pos_bol = 1478; + pos_cnum = 1490 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 32; - pos_bol = 1360; - pos_cnum = 1398 + pos_bol = 1478; + pos_cnum = 1520 } }))) then None @@ -583,21 +596,21 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = (Ortac_runtime.report "Hashtbl" "create ~random:false 16" (Ortac_runtime.Protected_value (Res (Ortac_runtime.dummy, ()))) "find" - [("List.mem (a, b) h.contents", + [("Sequence.mem h.contents (a, b)", { Ortac_runtime.start = { pos_fname = "hashtbl.mli"; pos_lnum = 32; - pos_bol = 1360; - pos_cnum = 1372 + pos_bol = 1478; + pos_cnum = 1490 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 32; - pos_bol = 1360; - pos_cnum = 1398 + pos_bol = 1478; + pos_cnum = 1520 } })]) | Error (Not_found) -> @@ -607,10 +620,10 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = lazy (Model.get (Lazy.force new_state__033_) 0) in (try not - (Ortac_runtime.Gospelstdlib.List.mem a_3 - (Ortac_runtime.Gospelstdlib.List.map + (Ortac_runtime.Gospelstdlib.Sequence.mem + (Ortac_runtime.Gospelstdlib.Sequence.map Ortac_runtime.Gospelstdlib.fst - (Lazy.force h_new__043_).contents)) + (Lazy.force h_new__043_).contents) a_2) with | e -> raise @@ -621,15 +634,15 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = { pos_fname = "hashtbl.mli"; pos_lnum = 31; - pos_bol = 1293; - pos_cnum = 1317 + pos_bol = 1403; + pos_cnum = 1427 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 31; - pos_bol = 1293; - pos_cnum = 1359 + pos_bol = 1403; + pos_cnum = 1477 } }))) then None @@ -637,25 +650,25 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = Some (Ortac_runtime.report "Hashtbl" "create ~random:false 16" (Ortac_runtime.Exception "Not_found") "find" - [("not (List.mem a (List.map fst h.contents))", + [("not (Sequence.mem (Sequence.map fst h.contents) a)", { Ortac_runtime.start = { pos_fname = "hashtbl.mli"; pos_lnum = 31; - pos_bol = 1293; - pos_cnum = 1317 + pos_bol = 1403; + pos_cnum = 1427 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 31; - pos_bol = 1293; - pos_cnum = 1359 + pos_bol = 1403; + pos_cnum = 1477 } })]) | _ -> None) - | (Find_opt a_4, Res ((Option (Int), _), o)) -> + | (Find_opt a_3, Res ((Option (Int), _), o)) -> if let h_old__045_ = Model.get state__031_ 0 and h_new__046_ = lazy (Model.get (Lazy.force new_state__033_) 0) in @@ -664,16 +677,16 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = | None -> if not - (Ortac_runtime.Gospelstdlib.List.mem a_4 - (Ortac_runtime.Gospelstdlib.List.map + (Ortac_runtime.Gospelstdlib.Sequence.mem + (Ortac_runtime.Gospelstdlib.Sequence.map Ortac_runtime.Gospelstdlib.fst - (Lazy.force h_new__046_).contents)) + (Lazy.force h_new__046_).contents) a_3) then true else false - | Some b_5 -> + | Some b_4 -> if - Ortac_runtime.Gospelstdlib.List.mem (a_4, b_5) - (Lazy.force h_new__046_).contents + Ortac_runtime.Gospelstdlib.Sequence.mem + (Lazy.force h_new__046_).contents (a_3, b_4) then true else false) = true @@ -687,15 +700,15 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = { pos_fname = "hashtbl.mli"; pos_lnum = 36; - pos_bol = 1559; - pos_cnum = 1571 + pos_bol = 1685; + pos_cnum = 1697 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 38; - pos_bol = 1643; - pos_cnum = 1687 + pos_bol = 1777; + pos_cnum = 1825 } }))) then None @@ -704,33 +717,32 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = (Ortac_runtime.report "Hashtbl" "create ~random:false 16" (Ortac_runtime.Value (Res (Ortac_runtime.dummy, ()))) "find_opt" - [("match o with\n | None -> not (List.mem a (List.map fst h.contents))\n | Some b -> List.mem (a, b) h.contents", + [("match o with\n | None -> not (Sequence.mem (Sequence.map fst h.contents) a)\n | Some b -> Sequence.mem h.contents (a, b)", { Ortac_runtime.start = { pos_fname = "hashtbl.mli"; pos_lnum = 36; - pos_bol = 1559; - pos_cnum = 1571 + pos_bol = 1685; + pos_cnum = 1697 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 38; - pos_bol = 1643; - pos_cnum = 1687 + pos_bol = 1777; + pos_cnum = 1825 } })]) - | (Find_all a_5, Res ((List (Int), _), bs)) -> + | (Find_all a_4, Res ((List (Int), _), bs)) -> if let h_old__048_ = Model.get state__031_ 0 and h_new__049_ = lazy (Model.get (Lazy.force new_state__033_) 0) in (try (Ortac_runtime.Gospelstdlib.List.to_seq bs) = (Ortac_runtime.Gospelstdlib.Sequence.filter_map - (fun (x_1, y) -> if x_1 = a_5 then Some y else None) - (Ortac_runtime.Gospelstdlib.List.to_seq - (Lazy.force h_new__049_).contents)) + (fun (x_1, y) -> if x_1 = a_4 then Some y else None) + (Lazy.force h_new__049_).contents) with | e -> raise @@ -741,15 +753,15 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = { pos_fname = "hashtbl.mli"; pos_lnum = 42; - pos_bol = 1853; - pos_cnum = 1865 + pos_bol = 1995; + pos_cnum = 2007 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 42; - pos_bol = 1853; - pos_cnum = 1947 + pos_bol = 1995; + pos_cnum = 2089 } }))) then None @@ -764,27 +776,27 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = { pos_fname = "hashtbl.mli"; pos_lnum = 42; - pos_bol = 1853; - pos_cnum = 1865 + pos_bol = 1995; + pos_cnum = 2007 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 42; - pos_bol = 1853; - pos_cnum = 1947 + pos_bol = 1995; + pos_cnum = 2089 } })]) - | (Mem a_6, Res ((Bool, _), b_6)) -> + | (Mem a_5, Res ((Bool, _), b_5)) -> if let h_old__051_ = Model.get state__031_ 0 and h_new__052_ = lazy (Model.get (Lazy.force new_state__033_) 0) in (try - (b_6 = true) = - (Ortac_runtime.Gospelstdlib.List.mem a_6 - (Ortac_runtime.Gospelstdlib.List.map + (b_5 = true) = + (Ortac_runtime.Gospelstdlib.Sequence.mem + (Ortac_runtime.Gospelstdlib.Sequence.map Ortac_runtime.Gospelstdlib.fst - (Lazy.force h_new__052_).contents)) + (Lazy.force h_new__052_).contents) a_5) with | e -> raise @@ -795,15 +807,15 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = { pos_fname = "hashtbl.mli"; pos_lnum = 46; - pos_bol = 2149; - pos_cnum = 2161 + pos_bol = 2291; + pos_cnum = 2303 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 46; - pos_bol = 2149; - pos_cnum = 2201 + pos_bol = 2291; + pos_cnum = 2351 } }))) then None @@ -811,32 +823,32 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = Some (Ortac_runtime.report "Hashtbl" "create ~random:false 16" (Ortac_runtime.Value (Res (Ortac_runtime.dummy, ()))) "mem" - [("b = List.mem a (List.map fst h.contents)", + [("b = Sequence.mem (Sequence.map fst h.contents) a", { Ortac_runtime.start = { pos_fname = "hashtbl.mli"; pos_lnum = 46; - pos_bol = 2149; - pos_cnum = 2161 + pos_bol = 2291; + pos_cnum = 2303 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; pos_lnum = 46; - pos_bol = 2149; - pos_cnum = 2201 + pos_bol = 2291; + pos_cnum = 2351 } })]) - | (Remove a_7, Res ((Unit, _), _)) -> None - | (Replace (a_8, b_3), Res ((Unit, _), _)) -> None + | (Remove a_6, Res ((Unit, _), _)) -> None + | (Replace (a_7, b_2), Res ((Unit, _), _)) -> None | (Length, Res ((Int, _), i)) -> if let h_old__058_ = Model.get state__031_ 0 and h_new__059_ = lazy (Model.get (Lazy.force new_state__033_) 0) in (try (Ortac_runtime.Gospelstdlib.integer_of_int i) = - (Ortac_runtime.Gospelstdlib.List.length + (Ortac_runtime.Gospelstdlib.Sequence.length (Lazy.force h_new__059_).contents) with | e -> @@ -847,16 +859,16 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = Ortac_runtime.start = { pos_fname = "hashtbl.mli"; - pos_lnum = 76; - pos_bol = 3727; - pos_cnum = 3739 + pos_lnum = 78; + pos_bol = 4064; + pos_cnum = 4076 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; - pos_lnum = 76; - pos_bol = 3727; - pos_cnum = 3765 + pos_lnum = 78; + pos_bol = 4064; + pos_cnum = 4106 } }))) then None @@ -870,7 +882,7 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = and h_new__057_ = lazy (Model.get (Lazy.force new_state__033_) 0) in try - Ortac_runtime.Gospelstdlib.List.length + Ortac_runtime.Gospelstdlib.Sequence.length (Lazy.force h_new__057_).contents with | e -> @@ -881,33 +893,33 @@ let ortac_postcond cmd__030_ state__031_ res__032_ = Ortac_runtime.start = { pos_fname = "hashtbl.mli"; - pos_lnum = 76; - pos_bol = 3727; - pos_cnum = 3743 + pos_lnum = 78; + pos_bol = 4064; + pos_cnum = 4080 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; - pos_lnum = 76; - pos_bol = 3727; - pos_cnum = 3765 + pos_lnum = 78; + pos_bol = 4064; + pos_cnum = 4106 } })))))) "length" - [("i = List.length h.contents", + [("i = Sequence.length h.contents", { Ortac_runtime.start = { pos_fname = "hashtbl.mli"; - pos_lnum = 76; - pos_bol = 3727; - pos_cnum = 3739 + pos_lnum = 78; + pos_bol = 4064; + pos_cnum = 4076 }; Ortac_runtime.stop = { pos_fname = "hashtbl.mli"; - pos_lnum = 76; - pos_bol = 3727; - pos_cnum = 3765 + pos_lnum = 78; + pos_bol = 4064; + pos_cnum = 4106 } })]) | _ -> None diff --git a/plugins/qcheck-stm/test/sut_in_type.mli b/plugins/qcheck-stm/test/sut_in_type.mli index c3480db3..74e3430c 100644 --- a/plugins/qcheck-stm/test/sut_in_type.mli +++ b/plugins/qcheck-stm/test/sut_in_type.mli @@ -1,14 +1,14 @@ type 'a t -(*@ mutable model contents : 'a list *) +(*@ mutable model contents : 'a sequence *) val make : int -> 'a -> 'a t (*@ t = make i a checks i >= 0 - ensures t.contents = List.init i (fun j -> a) *) + ensures t.contents = Sequence.init i (fun j -> a) *) val sut_in_type : 'a t list -> int (*@ r = sut_in_type ts - ensures r = List.length ts *) + ensures r = Sequence.length ts *) val sut_in_tuple : 'a t * int -> bool (*@ r = sut_in_tuple a diff --git a/plugins/qcheck-stm/test/sut_in_type_stm_tests.expected.ml b/plugins/qcheck-stm/test/sut_in_type_stm_tests.expected.ml index 1ab3f931..6497dc9c 100644 --- a/plugins/qcheck-stm/test/sut_in_type_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/sut_in_type_stm_tests.expected.ml @@ -9,14 +9,14 @@ module SUT = module ModelElt = struct type nonrec elt = { - contents: int list } + contents: int Ortac_runtime.Gospelstdlib.sequence } let init = let i = 16 and a_1 = 0 in { contents = (try - Ortac_runtime.Gospelstdlib.List.init + Ortac_runtime.Gospelstdlib.Sequence.init (Ortac_runtime.Gospelstdlib.integer_of_int i) (fun j -> a_1) with | e -> @@ -28,15 +28,15 @@ module ModelElt = { pos_fname = "sut_in_type.mli"; pos_lnum = 7; - pos_bol = 263; - pos_cnum = 288 + pos_bol = 271; + pos_cnum = 296 }; Ortac_runtime.stop = { pos_fname = "sut_in_type.mli"; pos_lnum = 7; - pos_bol = 263; - pos_cnum = 312 + pos_bol = 271; + pos_cnum = 324 } }))) } @@ -95,15 +95,15 @@ module Spec = { pos_fname = "sut_in_type.mli"; pos_lnum = 6; - pos_bol = 245; - pos_cnum = 256 + pos_bol = 253; + pos_cnum = 264 }; Ortac_runtime.stop = { pos_fname = "sut_in_type.mli"; pos_lnum = 6; - pos_bol = 245; - pos_cnum = 262 + pos_bol = 253; + pos_cnum = 270 } }))) then @@ -112,7 +112,7 @@ module Spec = { contents = (try - Ortac_runtime.Gospelstdlib.List.init + Ortac_runtime.Gospelstdlib.Sequence.init (Ortac_runtime.Gospelstdlib.integer_of_int i) (fun j -> a_1) with @@ -125,15 +125,15 @@ module Spec = { pos_fname = "sut_in_type.mli"; pos_lnum = 7; - pos_bol = 263; - pos_cnum = 288 + pos_bol = 271; + pos_cnum = 296 }; Ortac_runtime.stop = { pos_fname = "sut_in_type.mli"; pos_lnum = 7; - pos_bol = 263; - pos_cnum = 312 + pos_bol = 271; + pos_cnum = 324 } }))) } in @@ -192,15 +192,15 @@ let ortac_postcond cmd__006_ state__007_ res__008_ = { pos_fname = "sut_in_type.mli"; pos_lnum = 6; - pos_bol = 245; - pos_cnum = 256 + pos_bol = 253; + pos_cnum = 264 }; Ortac_runtime.stop = { pos_fname = "sut_in_type.mli"; pos_lnum = 6; - pos_bol = 245; - pos_cnum = 262 + pos_bol = 253; + pos_cnum = 270 } })) then None @@ -214,15 +214,15 @@ let ortac_postcond cmd__006_ state__007_ res__008_ = { pos_fname = "sut_in_type.mli"; pos_lnum = 6; - pos_bol = 245; - pos_cnum = 256 + pos_bol = 253; + pos_cnum = 264 }; Ortac_runtime.stop = { pos_fname = "sut_in_type.mli"; pos_lnum = 6; - pos_bol = 245; - pos_cnum = 262 + pos_bol = 253; + pos_cnum = 270 } })]) with @@ -246,15 +246,15 @@ let ortac_postcond cmd__006_ state__007_ res__008_ = { pos_fname = "sut_in_type.mli"; pos_lnum = 6; - pos_bol = 245; - pos_cnum = 256 + pos_bol = 253; + pos_cnum = 264 }; Ortac_runtime.stop = { pos_fname = "sut_in_type.mli"; pos_lnum = 6; - pos_bol = 245; - pos_cnum = 262 + pos_bol = 253; + pos_cnum = 270 } }))) then None @@ -269,15 +269,15 @@ let ortac_postcond cmd__006_ state__007_ res__008_ = { pos_fname = "sut_in_type.mli"; pos_lnum = 6; - pos_bol = 245; - pos_cnum = 256 + pos_bol = 253; + pos_cnum = 264 }; Ortac_runtime.stop = { pos_fname = "sut_in_type.mli"; pos_lnum = 6; - pos_bol = 245; - pos_cnum = 262 + pos_bol = 253; + pos_cnum = 270 } })]))) | _ -> None diff --git a/plugins/qcheck-stm/test/test_without_sut.mli b/plugins/qcheck-stm/test/test_without_sut.mli index b617d172..3191dcb4 100644 --- a/plugins/qcheck-stm/test/test_without_sut.mli +++ b/plugins/qcheck-stm/test/test_without_sut.mli @@ -1,10 +1,10 @@ type 'a t -(*@ mutable model contents : 'a list *) +(*@ mutable model contents : 'a sequence *) val make : int -> 'a -> 'a t (*@ t = make i a checks i >= 0 - ensures t.contents = List.init i (fun j -> a) *) + ensures t.contents = Sequence.init i (fun j -> a) *) val add : int -> int -> int (*@ c = add a b diff --git a/plugins/qcheck-stm/test/test_without_sut_stm_tests.expected.ml b/plugins/qcheck-stm/test/test_without_sut_stm_tests.expected.ml index 4377221c..c8c82d51 100644 --- a/plugins/qcheck-stm/test/test_without_sut_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/test_without_sut_stm_tests.expected.ml @@ -9,14 +9,14 @@ module SUT = module ModelElt = struct type nonrec elt = { - contents: int list } + contents: int Ortac_runtime.Gospelstdlib.sequence } let init = let i = 16 and a_1 = 0 in { contents = (try - Ortac_runtime.Gospelstdlib.List.init + Ortac_runtime.Gospelstdlib.Sequence.init (Ortac_runtime.Gospelstdlib.integer_of_int i) (fun j -> a_1) with | e -> @@ -28,15 +28,15 @@ module ModelElt = { pos_fname = "test_without_sut.mli"; pos_lnum = 7; - pos_bol = 283; - pos_cnum = 308 + pos_bol = 291; + pos_cnum = 316 }; Ortac_runtime.stop = { pos_fname = "test_without_sut.mli"; pos_lnum = 7; - pos_bol = 283; - pos_cnum = 332 + pos_bol = 291; + pos_cnum = 344 } }))) } @@ -100,15 +100,15 @@ module Spec = { pos_fname = "test_without_sut.mli"; pos_lnum = 6; - pos_bol = 265; - pos_cnum = 276 + pos_bol = 273; + pos_cnum = 284 }; Ortac_runtime.stop = { pos_fname = "test_without_sut.mli"; pos_lnum = 6; - pos_bol = 265; - pos_cnum = 282 + pos_bol = 273; + pos_cnum = 290 } }))) then @@ -117,7 +117,7 @@ module Spec = { contents = (try - Ortac_runtime.Gospelstdlib.List.init + Ortac_runtime.Gospelstdlib.Sequence.init (Ortac_runtime.Gospelstdlib.integer_of_int i) (fun j -> a_1) with @@ -130,15 +130,15 @@ module Spec = { pos_fname = "test_without_sut.mli"; pos_lnum = 7; - pos_bol = 283; - pos_cnum = 308 + pos_bol = 291; + pos_cnum = 316 }; Ortac_runtime.stop = { pos_fname = "test_without_sut.mli"; pos_lnum = 7; - pos_bol = 283; - pos_cnum = 332 + pos_bol = 291; + pos_cnum = 344 } }))) } in @@ -204,15 +204,15 @@ let ortac_postcond cmd__006_ state__007_ res__008_ = { pos_fname = "test_without_sut.mli"; pos_lnum = 6; - pos_bol = 265; - pos_cnum = 276 + pos_bol = 273; + pos_cnum = 284 }; Ortac_runtime.stop = { pos_fname = "test_without_sut.mli"; pos_lnum = 6; - pos_bol = 265; - pos_cnum = 282 + pos_bol = 273; + pos_cnum = 290 } })) then None @@ -226,15 +226,15 @@ let ortac_postcond cmd__006_ state__007_ res__008_ = { pos_fname = "test_without_sut.mli"; pos_lnum = 6; - pos_bol = 265; - pos_cnum = 276 + pos_bol = 273; + pos_cnum = 284 }; Ortac_runtime.stop = { pos_fname = "test_without_sut.mli"; pos_lnum = 6; - pos_bol = 265; - pos_cnum = 282 + pos_bol = 273; + pos_cnum = 290 } })]) with @@ -258,15 +258,15 @@ let ortac_postcond cmd__006_ state__007_ res__008_ = { pos_fname = "test_without_sut.mli"; pos_lnum = 6; - pos_bol = 265; - pos_cnum = 276 + pos_bol = 273; + pos_cnum = 284 }; Ortac_runtime.stop = { pos_fname = "test_without_sut.mli"; pos_lnum = 6; - pos_bol = 265; - pos_cnum = 282 + pos_bol = 273; + pos_cnum = 290 } }))) then None @@ -281,15 +281,15 @@ let ortac_postcond cmd__006_ state__007_ res__008_ = { pos_fname = "test_without_sut.mli"; pos_lnum = 6; - pos_bol = 265; - pos_cnum = 276 + pos_bol = 273; + pos_cnum = 284 }; Ortac_runtime.stop = { pos_fname = "test_without_sut.mli"; pos_lnum = 6; - pos_bol = 265; - pos_cnum = 282 + pos_bol = 273; + pos_cnum = 290 } })]))) | (Add (a_2, b), Res ((Int, _), c)) -> @@ -309,15 +309,15 @@ let ortac_postcond cmd__006_ state__007_ res__008_ = { pos_fname = "test_without_sut.mli"; pos_lnum = 11; - pos_bol = 499; - pos_cnum = 511 + pos_bol = 515; + pos_cnum = 527 }; Ortac_runtime.stop = { pos_fname = "test_without_sut.mli"; pos_lnum = 11; - pos_bol = 499; - pos_cnum = 520 + pos_bol = 515; + pos_cnum = 536 } }))) then None @@ -341,15 +341,15 @@ let ortac_postcond cmd__006_ state__007_ res__008_ = { pos_fname = "test_without_sut.mli"; pos_lnum = 11; - pos_bol = 499; - pos_cnum = 517 + pos_bol = 515; + pos_cnum = 533 }; Ortac_runtime.stop = { pos_fname = "test_without_sut.mli"; pos_lnum = 11; - pos_bol = 499; - pos_cnum = 518 + pos_bol = 515; + pos_cnum = 534 } })))))) "add" [("c = a + b", @@ -358,15 +358,15 @@ let ortac_postcond cmd__006_ state__007_ res__008_ = { pos_fname = "test_without_sut.mli"; pos_lnum = 11; - pos_bol = 499; - pos_cnum = 511 + pos_bol = 515; + pos_cnum = 527 }; Ortac_runtime.stop = { pos_fname = "test_without_sut.mli"; pos_lnum = 11; - pos_bol = 499; - pos_cnum = 520 + pos_bol = 515; + pos_cnum = 536 } })]) | _ -> None diff --git a/plugins/qcheck-stm/test/tuples.mli b/plugins/qcheck-stm/test/tuples.mli index 2276e1c7..6cb41e7b 100644 --- a/plugins/qcheck-stm/test/tuples.mli +++ b/plugins/qcheck-stm/test/tuples.mli @@ -1,41 +1,41 @@ type (!'a, !'b) t -(*@ mutable model contents : ('a * 'b) list *) +(*@ mutable model contents : ('a * 'b) sequence *) val create : unit -> ('a, 'b) t (*@ h = create () - ensures h.contents = [] *) + ensures h.contents = Sequence.empty *) val clear : ('a, 'b) t -> unit (*@ clear h modifies h - ensures h.contents = [] *) + ensures h.contents = Sequence.empty *) val add : ('a, 'b) t -> 'a * 'b -> unit (*@ add h tup modifies h - ensures h.contents = match tup with a, b -> (a, b) :: old h.contents *) + ensures h.contents = match tup with a, b -> Sequence.cons (a, b) (old h.contents) *) val add' : ('a, 'b) t -> bool * 'a * 'b -> unit (*@ add' h tup modifies h ensures h.contents = match tup with c, a, b -> - if c then (a, b) :: old h.contents + if c then Sequence.cons (a, b) (old h.contents) else old h.contents *) val add'' : ('a, 'b) t -> bool * ('a * 'b) -> unit (*@ add'' h tup modifies h ensures h.contents = match tup with c, (a, b) -> - if c then (a, b) :: old h.contents + if c then Sequence.cons (a, b) (old h.contents) else old h.contents *) val size_tup : ('a, 'b) t -> int * int (*@ x, y = size_tup t - ensures x = List.length t.contents - ensures y = List.length t.contents *) + ensures x = Sequence.length t.contents + ensures y = Sequence.length t.contents *) val size_tup' : ('a, 'b) t -> int * int * int (*@ x, y, z = size_tup' t - ensures x = List.length t.contents - ensures y = List.length t.contents - ensures z = List.length t.contents *) + ensures x = Sequence.length t.contents + ensures y = Sequence.length t.contents + ensures z = Sequence.length t.contents *) diff --git a/plugins/qcheck-stm/test/tuples_errors.expected b/plugins/qcheck-stm/test/tuples_errors.expected index 332d58fd..ef42e0e0 100644 --- a/plugins/qcheck-stm/test/tuples_errors.expected +++ b/plugins/qcheck-stm/test/tuples_errors.expected @@ -1,13 +1,13 @@ -File "tuples.mli", line 32, characters 0-141: +File "tuples.mli", line 32, characters 0-149: 32 | val size_tup : ('a, 'b) t -> int * int 33 | (*@ x, y = size_tup t -34 | ensures x = List.length t.contents -35 | ensures y = List.length t.contents *) +34 | ensures x = Sequence.length t.contents +35 | ensures y = Sequence.length t.contents *) Warning: Incomplete computation of the returned value in the specification of size_tup. Failure message won't be able to display the expected returned value. -File "tuples.mli", line 37, characters 0-191: +File "tuples.mli", line 37, characters 0-203: 37 | val size_tup' : ('a, 'b) t -> int * int * int 38 | (*@ x, y, z = size_tup' t -39 | ensures x = List.length t.contents -40 | ensures y = List.length t.contents -41 | ensures z = List.length t.contents *) +39 | ensures x = Sequence.length t.contents +40 | ensures y = Sequence.length t.contents +41 | ensures z = Sequence.length t.contents *) Warning: Incomplete computation of the returned value in the specification of size_tup'. Failure message won't be able to display the expected returned value. diff --git a/plugins/qcheck-stm/test/tuples_stm_tests.expected.ml b/plugins/qcheck-stm/test/tuples_stm_tests.expected.ml index 51b5a5f7..1e1ce657 100644 --- a/plugins/qcheck-stm/test/tuples_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/tuples_stm_tests.expected.ml @@ -10,13 +10,14 @@ module SUT = end) module ModelElt = struct - type nonrec elt = { - contents: (char * int) list } + type nonrec elt = + { + contents: (char * int) Ortac_runtime.Gospelstdlib.sequence } let init = let () = () in { contents = - (try [] + (try Ortac_runtime.Gospelstdlib.Sequence.empty with | e -> raise @@ -27,15 +28,15 @@ module ModelElt = { pos_fname = "tuples.mli"; pos_lnum = 6; - pos_bol = 251; - pos_cnum = 276 + pos_bol = 259; + pos_cnum = 284 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 6; - pos_bol = 251; - pos_cnum = 278 + pos_bol = 259; + pos_cnum = 298 } }))) } @@ -118,7 +119,7 @@ module Spec = let open ModelElt in { contents = - (try [] + (try Ortac_runtime.Gospelstdlib.Sequence.empty with | e -> raise @@ -129,15 +130,15 @@ module Spec = { pos_fname = "tuples.mli"; pos_lnum = 6; - pos_bol = 251; - pos_cnum = 276 + pos_bol = 259; + pos_cnum = 284 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 6; - pos_bol = 251; - pos_cnum = 278 + pos_bol = 259; + pos_cnum = 298 } }))) } in @@ -148,7 +149,7 @@ module Spec = let open ModelElt in { contents = - (try [] + (try Ortac_runtime.Gospelstdlib.Sequence.empty with | e -> raise @@ -159,15 +160,15 @@ module Spec = { pos_fname = "tuples.mli"; pos_lnum = 11; - pos_bol = 416; - pos_cnum = 441 + pos_bol = 448; + pos_cnum = 473 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 11; - pos_bol = 416; - pos_cnum = 443 + pos_bol = 448; + pos_cnum = 487 } }))) } in @@ -180,7 +181,9 @@ module Spec = contents = (try match tup with - | (a_1, b_1) -> (a_1, b_1) :: h_2__008_.contents + | (a_1, b_1) -> + Ortac_runtime.Gospelstdlib.Sequence.cons (a_1, b_1) + h_2__008_.contents with | e -> raise @@ -191,15 +194,15 @@ module Spec = { pos_fname = "tuples.mli"; pos_lnum = 16; - pos_bol = 594; - pos_cnum = 619 + pos_bol = 650; + pos_cnum = 675 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 16; - pos_bol = 594; - pos_cnum = 666 + pos_bol = 650; + pos_cnum = 735 } }))) } in @@ -214,7 +217,9 @@ module Spec = match tup_1 with | (c, a_2, b_2) -> if c = true - then (a_2, b_2) :: h_3__010_.contents + then + Ortac_runtime.Gospelstdlib.Sequence.cons + (a_2, b_2) h_3__010_.contents else h_3__010_.contents with | e -> @@ -226,15 +231,15 @@ module Spec = { pos_fname = "tuples.mli"; pos_lnum = 21; - pos_bol = 871; - pos_cnum = 896 + pos_bol = 953; + pos_cnum = 978 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 23; - pos_bol = 965; - pos_cnum = 992 + pos_bol = 1060; + pos_cnum = 1087 } }))) } in @@ -249,7 +254,9 @@ module Spec = match tup_2 with | (c_1, (a_3, b_3)) -> if c_1 = true - then (a_3, b_3) :: h_4__012_.contents + then + Ortac_runtime.Gospelstdlib.Sequence.cons + (a_3, b_3) h_4__012_.contents else h_4__012_.contents with | e -> @@ -261,15 +268,15 @@ module Spec = { pos_fname = "tuples.mli"; pos_lnum = 28; - pos_bol = 1156; - pos_cnum = 1181 + pos_bol = 1251; + pos_cnum = 1276 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 30; - pos_bol = 1252; - pos_cnum = 1279 + pos_bol = 1360; + pos_cnum = 1387 } }))) } in @@ -401,7 +408,7 @@ let ortac_postcond cmd__018_ state__019_ res__020_ = lazy (Model.get (Lazy.force new_state__021_) 0) in try (Ortac_runtime.Gospelstdlib.integer_of_int x) = - (Ortac_runtime.Gospelstdlib.List.length + (Ortac_runtime.Gospelstdlib.Sequence.length (Lazy.force t_new__027_).contents) with | e -> @@ -413,15 +420,15 @@ let ortac_postcond cmd__018_ state__019_ res__020_ = { pos_fname = "tuples.mli"; pos_lnum = 34; - pos_bol = 1422; - pos_cnum = 1434 + pos_bol = 1530; + pos_cnum = 1542 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 34; - pos_bol = 1422; - pos_cnum = 1460 + pos_bol = 1530; + pos_cnum = 1572 } })) then None @@ -430,21 +437,21 @@ let ortac_postcond cmd__018_ state__019_ res__020_ = (Ortac_runtime.report "Tuples" "create ()" (Ortac_runtime.Value (Res (Ortac_runtime.dummy, ()))) "size_tup" - [("x = List.length t.contents", + [("x = Sequence.length t.contents", { Ortac_runtime.start = { pos_fname = "tuples.mli"; pos_lnum = 34; - pos_bol = 1422; - pos_cnum = 1434 + pos_bol = 1530; + pos_cnum = 1542 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 34; - pos_bol = 1422; - pos_cnum = 1460 + pos_bol = 1530; + pos_cnum = 1572 } })])) (if @@ -453,7 +460,7 @@ let ortac_postcond cmd__018_ state__019_ res__020_ = lazy (Model.get (Lazy.force new_state__021_) 0) in try (Ortac_runtime.Gospelstdlib.integer_of_int y) = - (Ortac_runtime.Gospelstdlib.List.length + (Ortac_runtime.Gospelstdlib.Sequence.length (Lazy.force t_new__029_).contents) with | e -> @@ -465,15 +472,15 @@ let ortac_postcond cmd__018_ state__019_ res__020_ = { pos_fname = "tuples.mli"; pos_lnum = 35; - pos_bol = 1461; - pos_cnum = 1473 + pos_bol = 1573; + pos_cnum = 1585 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 35; - pos_bol = 1461; - pos_cnum = 1499 + pos_bol = 1573; + pos_cnum = 1615 } })) then None @@ -482,21 +489,21 @@ let ortac_postcond cmd__018_ state__019_ res__020_ = (Ortac_runtime.report "Tuples" "create ()" (Ortac_runtime.Value (Res (Ortac_runtime.dummy, ()))) "size_tup" - [("y = List.length t.contents", + [("y = Sequence.length t.contents", { Ortac_runtime.start = { pos_fname = "tuples.mli"; pos_lnum = 35; - pos_bol = 1461; - pos_cnum = 1473 + pos_bol = 1573; + pos_cnum = 1585 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 35; - pos_bol = 1461; - pos_cnum = 1499 + pos_bol = 1573; + pos_cnum = 1615 } })])) | (Size_tup', Res ((Tup3 (Int, Int, Int), _), (x_1, y_1, z))) -> @@ -507,7 +514,7 @@ let ortac_postcond cmd__018_ state__019_ res__020_ = lazy (Model.get (Lazy.force new_state__021_) 0) in try (Ortac_runtime.Gospelstdlib.integer_of_int x_1) = - (Ortac_runtime.Gospelstdlib.List.length + (Ortac_runtime.Gospelstdlib.Sequence.length (Lazy.force t_new__032_).contents) with | e -> @@ -519,15 +526,15 @@ let ortac_postcond cmd__018_ state__019_ res__020_ = { pos_fname = "tuples.mli"; pos_lnum = 39; - pos_bol = 1664; - pos_cnum = 1676 + pos_bol = 1784; + pos_cnum = 1796 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 39; - pos_bol = 1664; - pos_cnum = 1702 + pos_bol = 1784; + pos_cnum = 1826 } })) then None @@ -536,21 +543,21 @@ let ortac_postcond cmd__018_ state__019_ res__020_ = (Ortac_runtime.report "Tuples" "create ()" (Ortac_runtime.Value (Res (Ortac_runtime.dummy, ()))) "size_tup'" - [("x = List.length t.contents", + [("x = Sequence.length t.contents", { Ortac_runtime.start = { pos_fname = "tuples.mli"; pos_lnum = 39; - pos_bol = 1664; - pos_cnum = 1676 + pos_bol = 1784; + pos_cnum = 1796 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 39; - pos_bol = 1664; - pos_cnum = 1702 + pos_bol = 1784; + pos_cnum = 1826 } })])) (Ortac_runtime.append @@ -560,7 +567,7 @@ let ortac_postcond cmd__018_ state__019_ res__020_ = lazy (Model.get (Lazy.force new_state__021_) 0) in try (Ortac_runtime.Gospelstdlib.integer_of_int y_1) = - (Ortac_runtime.Gospelstdlib.List.length + (Ortac_runtime.Gospelstdlib.Sequence.length (Lazy.force t_new__034_).contents) with | e -> @@ -572,15 +579,15 @@ let ortac_postcond cmd__018_ state__019_ res__020_ = { pos_fname = "tuples.mli"; pos_lnum = 40; - pos_bol = 1703; - pos_cnum = 1715 + pos_bol = 1827; + pos_cnum = 1839 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 40; - pos_bol = 1703; - pos_cnum = 1741 + pos_bol = 1827; + pos_cnum = 1869 } })) then None @@ -589,21 +596,21 @@ let ortac_postcond cmd__018_ state__019_ res__020_ = (Ortac_runtime.report "Tuples" "create ()" (Ortac_runtime.Value (Res (Ortac_runtime.dummy, ()))) "size_tup'" - [("y = List.length t.contents", + [("y = Sequence.length t.contents", { Ortac_runtime.start = { pos_fname = "tuples.mli"; pos_lnum = 40; - pos_bol = 1703; - pos_cnum = 1715 + pos_bol = 1827; + pos_cnum = 1839 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 40; - pos_bol = 1703; - pos_cnum = 1741 + pos_bol = 1827; + pos_cnum = 1869 } })])) (if @@ -612,7 +619,7 @@ let ortac_postcond cmd__018_ state__019_ res__020_ = lazy (Model.get (Lazy.force new_state__021_) 0) in try (Ortac_runtime.Gospelstdlib.integer_of_int z) = - (Ortac_runtime.Gospelstdlib.List.length + (Ortac_runtime.Gospelstdlib.Sequence.length (Lazy.force t_new__036_).contents) with | e -> @@ -624,15 +631,15 @@ let ortac_postcond cmd__018_ state__019_ res__020_ = { pos_fname = "tuples.mli"; pos_lnum = 41; - pos_bol = 1742; - pos_cnum = 1754 + pos_bol = 1870; + pos_cnum = 1882 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 41; - pos_bol = 1742; - pos_cnum = 1780 + pos_bol = 1870; + pos_cnum = 1912 } })) then None @@ -641,21 +648,21 @@ let ortac_postcond cmd__018_ state__019_ res__020_ = (Ortac_runtime.report "Tuples" "create ()" (Ortac_runtime.Value (Res (Ortac_runtime.dummy, ()))) "size_tup'" - [("z = List.length t.contents", + [("z = Sequence.length t.contents", { Ortac_runtime.start = { pos_fname = "tuples.mli"; pos_lnum = 41; - pos_bol = 1742; - pos_cnum = 1754 + pos_bol = 1870; + pos_cnum = 1882 }; Ortac_runtime.stop = { pos_fname = "tuples.mli"; pos_lnum = 41; - pos_bol = 1742; - pos_cnum = 1780 + pos_bol = 1870; + pos_cnum = 1912 } })]))) | _ -> None