diff --git a/CHANGES.md b/CHANGES.md index c0a2e269..80e82fd0 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,7 @@ # Unreleased +- Improve test-failure message + [\#202](https://github.com/ocaml-gospel/ortac/pull/202) - Add a comment warning that the file is generated [\#198](https://github.com/ocaml-gospel/ortac/pull/198) - Add support for type invariants diff --git a/dune-project b/dune-project index 6b2091d4..341a46cc 100644 --- a/dune-project +++ b/dune-project @@ -179,6 +179,24 @@ ortac-core (ortac-qcheck-stm :with-test))) +(package + (name ortac-runtime-qcheck-stm) + (synopsis "Runtime support library for Ortac/QCheck-STM-generated code") + (description + "\> The ortac-runtime-qcheck-stm library provides support for the code + "\> generated by the Ortac/QCheck-STM plugin (provided by the + "\> ortac-qcheck-stm package). + "\> + "\> Ortac (OCaml Runtime Assertion Checking) is a tool to turn + "\> executable Gospel specifications into code to test they hold. + ) + (authors "Nicolas Osborne ") + (maintainers "Nicolas Osborne ") + (depends + (ocaml (>= 4.11.0)) + qcheck-stm + ortac-runtime)) + (package (name ortac-examples) (synopsis diff --git a/examples/dune.lwt_dllist.inc b/examples/dune.lwt_dllist.inc index 1388a7cf..881c3650 100644 --- a/examples/dune.lwt_dllist.inc +++ b/examples/dune.lwt_dllist.inc @@ -56,7 +56,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime) + ortac-runtime-qcheck-stm) (package ortac-examples) (action (run diff --git a/examples/dune.varray.inc b/examples/dune.varray.inc index e9ccbd83..163756c9 100644 --- a/examples/dune.varray.inc +++ b/examples/dune.varray.inc @@ -56,7 +56,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime) + ortac-runtime-qcheck-stm) (package ortac-examples) (action (run diff --git a/examples/dune.varray_circular.inc b/examples/dune.varray_circular.inc index e84c9e0b..7b73c2f4 100644 --- a/examples/dune.varray_circular.inc +++ b/examples/dune.varray_circular.inc @@ -56,7 +56,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime) + ortac-runtime-qcheck-stm) (package ortac-examples) (action (run diff --git a/examples/lwt_dllist_tests.ml b/examples/lwt_dllist_tests.ml index c0a1eff5..89e70aeb 100644 --- a/examples/lwt_dllist_tests.ml +++ b/examples/lwt_dllist_tests.ml @@ -1,10 +1,11 @@ (* This file is generated by ortac qcheck-stm, edit how you run the tool instead *) +[@@@ocaml.warning "-26-27"] open Lwt_dllist_spec +module Ortac_runtime = Ortac_runtime_qcheck_stm module Spec = struct open STM - [@@@ocaml.warning "-26-27"] include Lwt_dllist_incl type sut = int t type cmd = @@ -284,254 +285,7 @@ module Spec = | Take_r -> true | Take_opt_l -> true | Take_opt_r -> true - let postcond cmd__005_ state__006_ res__007_ = - let new_state__008_ = lazy (next_state cmd__005_ state__006_) in - match (cmd__005_, res__007_) with - | (Is_empty, Res ((Bool, _), b)) -> - (try - (b = true) = - ((Lazy.force new_state__008_).contents = - Ortac_runtime.Gospelstdlib.Sequence.empty) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 51; - pos_bol = 2194; - pos_cnum = 2208 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 51; - pos_bol = 2194; - pos_cnum = 2241 - } - }))) - | (Length, Res ((Int, _), l_1)) -> - (try - (Ortac_runtime.Gospelstdlib.integer_of_int l_1) = - (Ortac_runtime.Gospelstdlib.Sequence.length - (Lazy.force new_state__008_).contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 58; - pos_bol = 2649; - pos_cnum = 2663 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 58; - pos_bol = 2649; - pos_cnum = 2693 - } - }))) - | (Add_l a_1, Res ((Node (Int), _), n)) -> true - | (Add_r a_2, Res ((Node (Int), _), n_1)) -> true - | (Take_l, Res ((Result (Int, Exn), _), a_3)) -> - (match a_3 with - | Ok a_3 -> - (try - if - state__006_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty - then false - else - a_3 = - (Ortac_runtime.Gospelstdlib.Sequence.hd - state__006_.contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 85; - pos_bol = 4320; - pos_cnum = 4334 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 87; - pos_bol = 4394; - pos_cnum = 4445 - } - }))) - | Error (Empty) -> - (try - let __t1__009_ = - state__006_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty in - let __t2__010_ = - Ortac_runtime.Gospelstdlib.Sequence.empty = - (Lazy.force new_state__008_).contents in - __t1__009_ && __t2__010_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 88; - pos_bol = 4446; - pos_cnum = 4468 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 88; - pos_bol = 4446; - pos_cnum = 4512 - } - }))) - | _ -> false) - | (Take_r, Res ((Result (Int, Exn), _), a_4)) -> - (match a_4 with - | Ok a_4 -> - (try - if - state__006_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty - then false - else - a_4 = - (Ortac_runtime.Gospelstdlib.__mix_Bub - state__006_.contents - (Ortac_runtime.Gospelstdlib.(-) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__006_.contents) - (Ortac_runtime.Gospelstdlib.integer_of_int 1))) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 99; - pos_bol = 5153; - pos_cnum = 5167 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 101; - pos_bol = 5227; - pos_cnum = 5304 - } - }))) - | Error (Empty) -> - (try - let __t1__011_ = - state__006_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty in - let __t2__012_ = - Ortac_runtime.Gospelstdlib.Sequence.empty = - (Lazy.force new_state__008_).contents in - __t1__011_ && __t2__012_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 102; - pos_bol = 5305; - pos_cnum = 5327 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 102; - pos_bol = 5305; - pos_cnum = 5371 - } - }))) - | _ -> false) - | (Take_opt_l, Res ((Option (Int), _), o)) -> - (try - state__006_.contents = - (match o with - | None -> Ortac_runtime.Gospelstdlib.Sequence.empty - | Some a_5 -> - Ortac_runtime.Gospelstdlib.Sequence.cons a_5 - (Lazy.force new_state__008_).contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 112; - pos_bol = 6030; - pos_cnum = 6044 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 114; - pos_bol = 6131; - pos_cnum = 6201 - } - }))) - | (Take_opt_r, Res ((Option (Int), _), o_1)) -> - (try - state__006_.contents = - (match o_1 with - | None -> Ortac_runtime.Gospelstdlib.Sequence.empty - | Some a_6 -> - Ortac_runtime.Gospelstdlib.Sequence.snoc - (Lazy.force new_state__008_).contents a_6) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 124; - pos_bol = 6869; - pos_cnum = 6883 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 126; - pos_bol = 6970; - pos_cnum = 7040 - } - }))) - | _ -> true + let postcond _ _ _ = true let run cmd__015_ sut__016_ = match cmd__015_ with | Is_empty -> Res (bool, (is_empty sut__016_)) @@ -545,11 +299,436 @@ module Spec = | Take_opt_l -> Res ((option int), (take_opt_l sut__016_)) | Take_opt_r -> Res ((option int), (take_opt_r sut__016_)) end -module STMTests = (STM_sequential.Make)(Spec) +module STMTests = (Ortac_runtime.Make)(Spec) let check_init_state () = () -let agree_prop cs = check_init_state (); STMTests.agree_prop cs +let ortac_postcond cmd__005_ state__006_ res__007_ = + let open Spec in + let open STM in + let new_state__008_ = lazy (next_state cmd__005_ state__006_) in + match (cmd__005_, res__007_) with + | (Is_empty, Res ((Bool, _), b)) -> + if + (try + (b = true) = + ((Lazy.force new_state__008_).contents = + Ortac_runtime.Gospelstdlib.Sequence.empty) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 51; + pos_bol = 2194; + pos_cnum = 2208 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 51; + pos_bol = 2194; + pos_cnum = 2241 + } + }))) + then None + else + Some + (Ortac_runtime.report "is_empty" + [("b <-> s.contents = Sequence.empty", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 51; + pos_bol = 2194; + pos_cnum = 2208 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 51; + pos_bol = 2194; + pos_cnum = 2241 + } + })]) + | (Length, Res ((Int, _), l_1)) -> + if + (try + (Ortac_runtime.Gospelstdlib.integer_of_int l_1) = + (Ortac_runtime.Gospelstdlib.Sequence.length + (Lazy.force new_state__008_).contents) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 58; + pos_bol = 2649; + pos_cnum = 2663 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 58; + pos_bol = 2649; + pos_cnum = 2693 + } + }))) + then None + else + Some + (Ortac_runtime.report "length" + [("l = Sequence.length s.contents", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 58; + pos_bol = 2649; + pos_cnum = 2663 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 58; + pos_bol = 2649; + pos_cnum = 2693 + } + })]) + | (Add_l a_1, Res ((Node (Int), _), n)) -> None + | (Add_r a_2, Res ((Node (Int), _), n_1)) -> None + | (Take_l, Res ((Result (Int, Exn), _), a_3)) -> + (match a_3 with + | Ok a_3 -> + if + (try + if + state__006_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty + then false + else + a_3 = + (Ortac_runtime.Gospelstdlib.Sequence.hd + state__006_.contents) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 85; + pos_bol = 4320; + pos_cnum = 4334 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 87; + pos_bol = 4394; + pos_cnum = 4445 + } + }))) + then None + else + Some + (Ortac_runtime.report "take_l" + [("if old s.contents = Sequence.empty\n then false\n else a = Sequence.hd (old s.contents)", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 85; + pos_bol = 4320; + pos_cnum = 4334 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 87; + pos_bol = 4394; + pos_cnum = 4445 + } + })]) + | Error (Empty) -> + if + (try + let __t1__009_ = + state__006_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty in + let __t2__010_ = + Ortac_runtime.Gospelstdlib.Sequence.empty = + (Lazy.force new_state__008_).contents in + __t1__009_ && __t2__010_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 88; + pos_bol = 4446; + pos_cnum = 4468 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 88; + pos_bol = 4446; + pos_cnum = 4512 + } + }))) + then None + else + Some + (Ortac_runtime.report "take_l" + [("old s.contents = Sequence.empty = s.contents", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 88; + pos_bol = 4446; + pos_cnum = 4468 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 88; + pos_bol = 4446; + pos_cnum = 4512 + } + })]) + | _ -> None) + | (Take_r, Res ((Result (Int, Exn), _), a_4)) -> + (match a_4 with + | Ok a_4 -> + if + (try + if + state__006_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty + then false + else + a_4 = + (Ortac_runtime.Gospelstdlib.__mix_Bub + state__006_.contents + (Ortac_runtime.Gospelstdlib.(-) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__006_.contents) + (Ortac_runtime.Gospelstdlib.integer_of_int 1))) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 99; + pos_bol = 5153; + pos_cnum = 5167 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 101; + pos_bol = 5227; + pos_cnum = 5304 + } + }))) + then None + else + Some + (Ortac_runtime.report "take_r" + [("if old s.contents = Sequence.empty\n then false\n else a = (old s.contents)[Sequence.length (old s.contents) - 1]", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 99; + pos_bol = 5153; + pos_cnum = 5167 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 101; + pos_bol = 5227; + pos_cnum = 5304 + } + })]) + | Error (Empty) -> + if + (try + let __t1__011_ = + state__006_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty in + let __t2__012_ = + Ortac_runtime.Gospelstdlib.Sequence.empty = + (Lazy.force new_state__008_).contents in + __t1__011_ && __t2__012_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 102; + pos_bol = 5305; + pos_cnum = 5327 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 102; + pos_bol = 5305; + pos_cnum = 5371 + } + }))) + then None + else + Some + (Ortac_runtime.report "take_r" + [("old s.contents = Sequence.empty = s.contents", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 102; + pos_bol = 5305; + pos_cnum = 5327 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 102; + pos_bol = 5305; + pos_cnum = 5371 + } + })]) + | _ -> None) + | (Take_opt_l, Res ((Option (Int), _), o)) -> + if + (try + state__006_.contents = + (match o with + | None -> Ortac_runtime.Gospelstdlib.Sequence.empty + | Some a_5 -> + Ortac_runtime.Gospelstdlib.Sequence.cons a_5 + (Lazy.force new_state__008_).contents) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 112; + pos_bol = 6030; + pos_cnum = 6044 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 114; + pos_bol = 6131; + pos_cnum = 6201 + } + }))) + then None + else + Some + (Ortac_runtime.report "take_opt_l" + [("old s.contents = match o with\n | None -> Sequence.empty\n | Some a -> Sequence.cons a s.contents", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 112; + pos_bol = 6030; + pos_cnum = 6044 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 114; + pos_bol = 6131; + pos_cnum = 6201 + } + })]) + | (Take_opt_r, Res ((Option (Int), _), o_1)) -> + if + (try + state__006_.contents = + (match o_1 with + | None -> Ortac_runtime.Gospelstdlib.Sequence.empty + | Some a_6 -> + Ortac_runtime.Gospelstdlib.Sequence.snoc + (Lazy.force new_state__008_).contents a_6) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 124; + pos_bol = 6869; + pos_cnum = 6883 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 126; + pos_bol = 6970; + pos_cnum = 7040 + } + }))) + then None + else + Some + (Ortac_runtime.report "take_opt_r" + [("old s.contents = match o with\n | None -> Sequence.empty\n | Some a -> Sequence.snoc s.contents a", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 124; + pos_bol = 6869; + pos_cnum = 6883 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 126; + pos_bol = 6970; + pos_cnum = 7040 + } + })]) + | _ -> None let _ = QCheck_base_runner.run_tests_main (let count = 1000 in - [QCheck.Test.make ~count ~name:"Lwt_dllist_spec STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + [STMTests.agree_test ~count ~name:"Lwt_dllist_spec STM tests" + check_init_state ortac_postcond]) diff --git a/examples/varray_circular_tests.ml b/examples/varray_circular_tests.ml index ff5c789d..3ca9f4ff 100644 --- a/examples/varray_circular_tests.ml +++ b/examples/varray_circular_tests.ml @@ -1,6 +1,8 @@ (* This file is generated by ortac qcheck-stm, edit how you run the tool instead *) +[@@@ocaml.warning "-26-27"] open Varray_circular_spec +module Ortac_runtime = Ortac_runtime_qcheck_stm let inside i s = try if @@ -60,7 +62,6 @@ let proj e = module Spec = struct open STM - [@@@ocaml.warning "-26-27"] include Varray_circular_incl type sut = char t type cmd = @@ -668,215 +669,122 @@ module Spec = | Length -> true | Is_empty -> true | Fill (pos, len, x_3) -> true - let postcond cmd__016_ state__017_ res__018_ = + let postcond _ _ _ = true + let run cmd__032_ sut__033_ = + match cmd__032_ with + | Push_back x -> Res (unit, (push_back sut__033_ x)) + | Pop_back -> + Res + ((result (elt char) exn), + (protect (fun () -> pop_back sut__033_) ())) + | Push_front x_1 -> Res (unit, (push_front sut__033_ x_1)) + | Pop_front -> + Res + ((result (elt char) exn), + (protect (fun () -> pop_front sut__033_) ())) + | Insert_at (i_1, x_2) -> + Res + ((result unit exn), + (protect (fun () -> insert_at sut__033_ i_1 x_2) ())) + | Pop_at i_2 -> + Res + ((result (elt char) exn), + (protect (fun () -> pop_at sut__033_ i_2) ())) + | Delete_at i_3 -> + Res + ((result unit exn), + (protect (fun () -> delete_at sut__033_ i_3) ())) + | Get i_4 -> + Res + ((result (elt char) exn), + (protect (fun () -> get sut__033_ i_4) ())) + | Set (i_5, v) -> + Res + ((result unit exn), (protect (fun () -> set sut__033_ i_5 v) ())) + | Length -> Res (int, (length sut__033_)) + | Is_empty -> Res (bool, (is_empty sut__033_)) + | Fill (pos, len, x_3) -> + Res + ((result unit exn), + (protect (fun () -> fill sut__033_ pos len x_3) ())) + end +module STMTests = (Ortac_runtime.Make)(Spec) +let check_init_state () = () +let ortac_postcond cmd__016_ state__017_ res__018_ = + let open Spec in + let open STM in let new_state__019_ = lazy (next_state cmd__016_ state__017_) in match (cmd__016_, res__018_) with - | (Push_back x, Res ((Unit, _), _)) -> true + | (Push_back x, Res ((Unit, _), _)) -> None | (Pop_back, Res ((Result (Elt (Char), Exn), _), x_4)) -> (match x_4 with | Ok x_4 -> - (try - if - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty - then false - else - (proj x_4) = - (Ortac_runtime.Gospelstdlib.__mix_Bub - state__017_.contents - (Ortac_runtime.Gospelstdlib.(-) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) - (Ortac_runtime.Gospelstdlib.integer_of_int 1))) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 33; - pos_bol = 2340; - pos_cnum = 2354 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 35; - pos_bol = 2414; - pos_cnum = 2496 - } - }))) - | Error (Not_found) -> - (try - let __t1__020_ = - (Lazy.force new_state__019_).contents = - state__017_.contents in - let __t2__021_ = - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty in - __t1__020_ && __t2__021_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 36; - pos_bol = 2497; - pos_cnum = 2523 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 36; - pos_bol = 2497; - pos_cnum = 2567 - } - }))) - | _ -> false) - | (Push_front x_1, Res ((Unit, _), _)) -> true - | (Pop_front, Res ((Result (Elt (Char), Exn), _), x_5)) -> - (match x_5 with - | Ok x_5 -> - (try - if - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty - then false - else - (proj x_5) = - (Ortac_runtime.Gospelstdlib.Sequence.hd - state__017_.contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 56; - pos_bol = 3884; - pos_cnum = 3898 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 58; - pos_bol = 3958; - pos_cnum = 4014 - } - }))) + if + (try + if + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty + then false + else + (proj x_4) = + (Ortac_runtime.Gospelstdlib.__mix_Bub + state__017_.contents + (Ortac_runtime.Gospelstdlib.(-) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) + (Ortac_runtime.Gospelstdlib.integer_of_int 1))) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 33; + pos_bol = 2340; + pos_cnum = 2354 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 35; + pos_bol = 2414; + pos_cnum = 2496 + } + }))) + then None + else + Some + (Ortac_runtime.report "pop_back" + [("if old t.contents = Sequence.empty\n then false\n else proj x = (old t.contents)[Sequence.length (old t.contents) - 1]", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 33; + pos_bol = 2340; + pos_cnum = 2354 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 35; + pos_bol = 2414; + pos_cnum = 2496 + } + })]) | Error (Not_found) -> - (try - let __t1__022_ = - (Lazy.force new_state__019_).contents = - state__017_.contents in - let __t2__023_ = - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty in - __t1__022_ && __t2__023_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 59; - pos_bol = 4015; - pos_cnum = 4041 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 59; - pos_bol = 4015; - pos_cnum = 4085 - } - }))) - | _ -> false) - | (Insert_at (i_1, x_2), Res ((Result (Unit, Exn), _), res)) -> - if - (try - let __t1__024_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in - let __t2__025_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) in - __t1__024_ && __t2__025_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 72; - pos_bol = 4784; - pos_cnum = 4797 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 72; - pos_bol = 4784; - pos_cnum = 4833 - } - }))) - then (match res with | Ok _ -> true | _ -> false) - else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (Pop_at i_2, Res ((Result (Elt (Char), Exn), _), x_6)) -> - if - (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_2) - state__017_.contents) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 89; - pos_bol = 5727; - pos_cnum = 5740 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 89; - pos_bol = 5727; - pos_cnum = 5759 - } - }))) - then - (match x_6 with - | Ok x_6 -> + if (try - (proj x_6) = - (Ortac_runtime.Gospelstdlib.__mix_Bub - state__017_.contents - (Ortac_runtime.Gospelstdlib.integer_of_int i_2)) + let __t1__020_ = + (Lazy.force new_state__019_).contents = + state__017_.contents in + let __t2__021_ = + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty in + __t1__020_ && __t2__021_ with | e -> raise @@ -886,59 +794,54 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 92; - pos_bol = 5864; - pos_cnum = 5878 + pos_lnum = 36; + pos_bol = 2497; + pos_cnum = 2523 }; Ortac_runtime.stop = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 92; - pos_bol = 5864; - pos_cnum = 5906 + pos_lnum = 36; + pos_bol = 2497; + pos_cnum = 2567 } }))) - | _ -> false) - else - (match x_6 with | Error (Invalid_argument _) -> true | _ -> false) - | (Delete_at i_3, Res ((Result (Unit, Exn), _), res)) -> - if - (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_3) - state__017_.contents) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 102; - pos_bol = 6426; - pos_cnum = 6439 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 102; - pos_bol = 6426; - pos_cnum = 6458 - } - }))) - then - (match res with - | Ok _ -> + then None + else + Some + (Ortac_runtime.report "pop_back" + [("t.contents = old t.contents = Sequence.empty", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 36; + pos_bol = 2497; + pos_cnum = 2523 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 36; + pos_bol = 2497; + pos_cnum = 2567 + } + })]) + | _ -> None) + | (Push_front x_1, Res ((Unit, _), _)) -> None + | (Pop_front, Res ((Result (Elt (Char), Exn), _), x_5)) -> + (match x_5 with + | Ok x_5 -> + if (try - (Ortac_runtime.Gospelstdlib.Sequence.length - (Lazy.force new_state__019_).contents) - = - (Ortac_runtime.Gospelstdlib.(-) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) - (Ortac_runtime.Gospelstdlib.integer_of_int 1)) + if + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty + then false + else + (proj x_5) = + (Ortac_runtime.Gospelstdlib.Sequence.hd + state__017_.contents) with | e -> raise @@ -948,56 +851,49 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 105; - pos_bol = 6563; - pos_cnum = 6577 + pos_lnum = 56; + pos_bol = 3884; + pos_cnum = 3898 }; Ortac_runtime.stop = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 105; - pos_bol = 6563; - pos_cnum = 6642 + pos_lnum = 58; + pos_bol = 3958; + pos_cnum = 4014 } }))) - | _ -> false) - else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (Get i_4, Res ((Result (Elt (Char), Exn), _), x_7)) -> - if - (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_4) - state__017_.contents) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 128; - pos_bol = 7616; - pos_cnum = 7629 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 128; - pos_bol = 7616; - pos_cnum = 7648 - } - }))) - then - (match x_7 with - | Ok x_7 -> + then None + else + Some + (Ortac_runtime.report "pop_front" + [("if old t.contents = Sequence.empty\n then false\n else proj x = Sequence.hd (old t.contents)", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 56; + pos_bol = 3884; + pos_cnum = 3898 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 58; + pos_bol = 3958; + pos_cnum = 4014 + } + })]) + | Error (Not_found) -> + if (try - (proj x_7) = - (Ortac_runtime.Gospelstdlib.__mix_Bub - (Lazy.force new_state__019_).contents - (Ortac_runtime.Gospelstdlib.integer_of_int i_4)) + let __t1__022_ = + (Lazy.force new_state__019_).contents = + state__017_.contents in + let __t2__023_ = + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty in + __t1__022_ && __t2__023_ with | e -> raise @@ -1007,27 +903,741 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 127; - pos_bol = 7577; - pos_cnum = 7591 + pos_lnum = 59; + pos_bol = 4015; + pos_cnum = 4041 }; Ortac_runtime.stop = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 127; - pos_bol = 7577; - pos_cnum = 7615 + pos_lnum = 59; + pos_bol = 4015; + pos_cnum = 4085 } }))) - | _ -> false) - else - (match x_7 with | Error (Invalid_argument _) -> true | _ -> false) + then None + else + Some + (Ortac_runtime.report "pop_front" + [("t.contents = old t.contents = Sequence.empty", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 59; + pos_bol = 4015; + pos_cnum = 4041 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 59; + pos_bol = 4015; + pos_cnum = 4085 + } + })]) + | _ -> None) + | (Insert_at (i_1, x_2), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + let __t1__024_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__025_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__024_ && __t2__025_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4797 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4833 + } + })) + then None + else + Some + (Ortac_runtime.report "insert_at" + [("0 <= i <= Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4797 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4833 + } + })]) + with + | None -> (match res with | Ok _ -> None | _ -> None) + | _ -> + (match res with + | Error (Invalid_argument _) -> None + | _ -> + if + (try + let __t1__024_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__025_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__024_ && __t2__025_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4797 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4833 + } + }))) + then None + else + Some + (Ortac_runtime.report "insert_at" + [("0 <= i <= Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4797 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4833 + } + })]))) + | (Pop_at i_2, Res ((Result (Elt (Char), Exn), _), x_6)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_2) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5740 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5759 + } + })) + then None + else + Some + (Ortac_runtime.report "pop_at" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5740 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5759 + } + })]) + with + | None -> + (match x_6 with + | Ok x_6 -> + if + (try + (proj x_6) = + (Ortac_runtime.Gospelstdlib.__mix_Bub + state__017_.contents + (Ortac_runtime.Gospelstdlib.integer_of_int i_2)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 92; + pos_bol = 5864; + pos_cnum = 5878 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 92; + pos_bol = 5864; + pos_cnum = 5906 + } + }))) + then None + else + Some + (Ortac_runtime.report "pop_at" + [("(proj x) = old t.contents[i]", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 92; + pos_bol = 5864; + pos_cnum = 5878 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 92; + pos_bol = 5864; + pos_cnum = 5906 + } + })]) + | _ -> None) + | _ -> + (match x_6 with + | Error (Invalid_argument _) -> None + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_2) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5740 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5759 + } + }))) + then None + else + Some + (Ortac_runtime.report "pop_at" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5740 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5759 + } + })]))) + | (Delete_at i_3, Res ((Result (Unit, Exn), _), res)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_3) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6439 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6458 + } + })) + then None + else + Some + (Ortac_runtime.report "delete_at" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6439 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6458 + } + })]) + with + | None -> + (match res with + | Ok _ -> + if + (try + (Ortac_runtime.Gospelstdlib.Sequence.length + (Lazy.force new_state__019_).contents) + = + (Ortac_runtime.Gospelstdlib.(-) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) + (Ortac_runtime.Gospelstdlib.integer_of_int 1)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 105; + pos_bol = 6563; + pos_cnum = 6577 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 105; + pos_bol = 6563; + pos_cnum = 6642 + } + }))) + then None + else + Some + (Ortac_runtime.report "delete_at" + [("Sequence.length t.contents = Sequence.length (old t.contents) - 1", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 105; + pos_bol = 6563; + pos_cnum = 6577 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 105; + pos_bol = 6563; + pos_cnum = 6642 + } + })]) + | _ -> None) + | _ -> + (match res with + | Error (Invalid_argument _) -> None + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_3) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6439 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6458 + } + }))) + then None + else + Some + (Ortac_runtime.report "delete_at" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6439 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6458 + } + })]))) + | (Get i_4, Res ((Result (Elt (Char), Exn), _), x_7)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_4) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7629 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7648 + } + })) + then None + else + Some + (Ortac_runtime.report "get" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7629 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7648 + } + })]) + with + | None -> + (match x_7 with + | Ok x_7 -> + if + (try + (proj x_7) = + (Ortac_runtime.Gospelstdlib.__mix_Bub + (Lazy.force new_state__019_).contents + (Ortac_runtime.Gospelstdlib.integer_of_int i_4)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 127; + pos_bol = 7577; + pos_cnum = 7591 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 127; + pos_bol = 7577; + pos_cnum = 7615 + } + }))) + then None + else + Some + (Ortac_runtime.report "get" + [("(proj x) = t.contents[i]", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 127; + pos_bol = 7577; + pos_cnum = 7591 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 127; + pos_bol = 7577; + pos_cnum = 7615 + } + })]) + | _ -> None) + | _ -> + (match x_7 with + | Error (Invalid_argument _) -> None + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_4) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7629 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7648 + } + }))) + then None + else + Some + (Ortac_runtime.report "get" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7629 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7648 + } + })]))) | (Set (i_5, v), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_5) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8090 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8109 + } + })) + then None + else + Some + (Ortac_runtime.report "set" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8090 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8109 + } + })]) + with + | None -> (match res with | Ok _ -> None | _ -> None) + | _ -> + (match res with + | Error (Invalid_argument _) -> None + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_5) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8090 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8109 + } + }))) + then None + else + Some + (Ortac_runtime.report "set" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8090 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8109 + } + })]))) + | (Length, Res ((Int, _), l)) -> if (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_5) - state__017_.contents) - = true + (Ortac_runtime.Gospelstdlib.integer_of_int l) = + (Ortac_runtime.Gospelstdlib.Sequence.length + (Lazy.force new_state__019_).contents) with | e -> raise @@ -1037,94 +1647,45 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 137; - pos_bol = 8077; - pos_cnum = 8090 + pos_lnum = 144; + pos_bol = 8634; + pos_cnum = 8648 }; Ortac_runtime.stop = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 137; - pos_bol = 8077; - pos_cnum = 8109 + pos_lnum = 144; + pos_bol = 8634; + pos_cnum = 8678 } }))) - then (match res with | Ok _ -> true | _ -> false) + then None else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (Length, Res ((Int, _), l)) -> - (try - (Ortac_runtime.Gospelstdlib.integer_of_int l) = - (Ortac_runtime.Gospelstdlib.Sequence.length - (Lazy.force new_state__019_).contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 144; - pos_bol = 8634; - pos_cnum = 8648 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 144; - pos_bol = 8634; - pos_cnum = 8678 - } - }))) + Some + (Ortac_runtime.report "length" + [("l = Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 144; + pos_bol = 8634; + pos_cnum = 8648 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 144; + pos_bol = 8634; + pos_cnum = 8678 + } + })]) | (Is_empty, Res ((Bool, _), b)) -> - (try - (b = true) = - ((Lazy.force new_state__019_).contents = - Ortac_runtime.Gospelstdlib.Sequence.empty) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 171; - pos_bol = 10238; - pos_cnum = 10252 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 171; - pos_bol = 10238; - pos_cnum = 10285 - } - }))) - | (Fill (pos, len, x_3), Res ((Result (Unit, Exn), _), res)) -> if (try - let __t1__026_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int pos) in - let __t2__027_ = - let __t1__028_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int len) in - let __t2__029_ = - Ortac_runtime.Gospelstdlib.(<) - (Ortac_runtime.Gospelstdlib.(+) - (Ortac_runtime.Gospelstdlib.integer_of_int pos) - (Ortac_runtime.Gospelstdlib.integer_of_int len)) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) in - __t1__028_ && __t2__029_ in - __t1__026_ && __t2__027_ + (b = true) = + ((Lazy.force new_state__019_).contents = + Ortac_runtime.Gospelstdlib.Sequence.empty) with | e -> raise @@ -1134,65 +1695,177 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 211; - pos_bol = 12981; - pos_cnum = 12994 + pos_lnum = 171; + pos_bol = 10238; + pos_cnum = 10252 }; Ortac_runtime.stop = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 211; - pos_bol = 12981; - pos_cnum = 13056 + pos_lnum = 171; + pos_bol = 10238; + pos_cnum = 10285 } }))) - then (match res with | Ok _ -> true | _ -> false) + then None else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | _ -> true - let run cmd__032_ sut__033_ = - match cmd__032_ with - | Push_back x -> Res (unit, (push_back sut__033_ x)) - | Pop_back -> - Res - ((result (elt char) exn), - (protect (fun () -> pop_back sut__033_) ())) - | Push_front x_1 -> Res (unit, (push_front sut__033_ x_1)) - | Pop_front -> - Res - ((result (elt char) exn), - (protect (fun () -> pop_front sut__033_) ())) - | Insert_at (i_1, x_2) -> - Res - ((result unit exn), - (protect (fun () -> insert_at sut__033_ i_1 x_2) ())) - | Pop_at i_2 -> - Res - ((result (elt char) exn), - (protect (fun () -> pop_at sut__033_ i_2) ())) - | Delete_at i_3 -> - Res - ((result unit exn), - (protect (fun () -> delete_at sut__033_ i_3) ())) - | Get i_4 -> - Res - ((result (elt char) exn), - (protect (fun () -> get sut__033_ i_4) ())) - | Set (i_5, v) -> - Res - ((result unit exn), (protect (fun () -> set sut__033_ i_5 v) ())) - | Length -> Res (int, (length sut__033_)) - | Is_empty -> Res (bool, (is_empty sut__033_)) - | Fill (pos, len, x_3) -> - Res - ((result unit exn), - (protect (fun () -> fill sut__033_ pos len x_3) ())) - end -module STMTests = (STM_sequential.Make)(Spec) -let check_init_state () = () -let agree_prop cs = check_init_state (); STMTests.agree_prop cs + Some + (Ortac_runtime.report "is_empty" + [("b <-> t.contents = Sequence.empty", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 171; + pos_bol = 10238; + pos_cnum = 10252 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 171; + pos_bol = 10238; + pos_cnum = 10285 + } + })]) + | (Fill (pos, len, x_3), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + let __t1__026_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int pos) in + let __t2__027_ = + let __t1__028_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int len) in + let __t2__029_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int pos) + (Ortac_runtime.Gospelstdlib.integer_of_int len)) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__028_ && __t2__029_ in + __t1__026_ && __t2__027_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 12994 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 13056 + } + })) + then None + else + Some + (Ortac_runtime.report "fill" + [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 12994 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 13056 + } + })]) + with + | None -> (match res with | Ok _ -> None | _ -> None) + | _ -> + (match res with + | Error (Invalid_argument _) -> None + | _ -> + if + (try + let __t1__026_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int pos) in + let __t2__027_ = + let __t1__028_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int len) in + let __t2__029_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int + pos) + (Ortac_runtime.Gospelstdlib.integer_of_int + len)) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__028_ && __t2__029_ in + __t1__026_ && __t2__027_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 12994 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 13056 + } + }))) + then None + else + Some + (Ortac_runtime.report "fill" + [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 12994 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 13056 + } + })]))) + | _ -> None let _ = QCheck_base_runner.run_tests_main (let count = 1000 in - [QCheck.Test.make ~count ~name:"Varray_circular_spec STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + [STMTests.agree_test ~count ~name:"Varray_circular_spec STM tests" + check_init_state ortac_postcond]) diff --git a/examples/varray_tests.ml b/examples/varray_tests.ml index 2425a0aa..8154cd67 100644 --- a/examples/varray_tests.ml +++ b/examples/varray_tests.ml @@ -1,6 +1,8 @@ (* This file is generated by ortac qcheck-stm, edit how you run the tool instead *) +[@@@ocaml.warning "-26-27"] open Varray_spec +module Ortac_runtime = Ortac_runtime_qcheck_stm let inside i s = try if @@ -60,7 +62,6 @@ let proj e = module Spec = struct open STM - [@@@ocaml.warning "-26-27"] include Varray_incl type sut = char t type cmd = @@ -668,215 +669,122 @@ module Spec = | Length -> true | Is_empty -> true | Fill (pos, len, x_3) -> true - let postcond cmd__016_ state__017_ res__018_ = + let postcond _ _ _ = true + let run cmd__032_ sut__033_ = + match cmd__032_ with + | Push_back x -> Res (unit, (push_back sut__033_ x)) + | Pop_back -> + Res + ((result (elt char) exn), + (protect (fun () -> pop_back sut__033_) ())) + | Push_front x_1 -> Res (unit, (push_front sut__033_ x_1)) + | Pop_front -> + Res + ((result (elt char) exn), + (protect (fun () -> pop_front sut__033_) ())) + | Insert_at (i_1, x_2) -> + Res + ((result unit exn), + (protect (fun () -> insert_at sut__033_ i_1 x_2) ())) + | Pop_at i_2 -> + Res + ((result (elt char) exn), + (protect (fun () -> pop_at sut__033_ i_2) ())) + | Delete_at i_3 -> + Res + ((result unit exn), + (protect (fun () -> delete_at sut__033_ i_3) ())) + | Get i_4 -> + Res + ((result (elt char) exn), + (protect (fun () -> get sut__033_ i_4) ())) + | Set (i_5, v) -> + Res + ((result unit exn), (protect (fun () -> set sut__033_ i_5 v) ())) + | Length -> Res (int, (length sut__033_)) + | Is_empty -> Res (bool, (is_empty sut__033_)) + | Fill (pos, len, x_3) -> + Res + ((result unit exn), + (protect (fun () -> fill sut__033_ pos len x_3) ())) + end +module STMTests = (Ortac_runtime.Make)(Spec) +let check_init_state () = () +let ortac_postcond cmd__016_ state__017_ res__018_ = + let open Spec in + let open STM in let new_state__019_ = lazy (next_state cmd__016_ state__017_) in match (cmd__016_, res__018_) with - | (Push_back x, Res ((Unit, _), _)) -> true + | (Push_back x, Res ((Unit, _), _)) -> None | (Pop_back, Res ((Result (Elt (Char), Exn), _), x_4)) -> (match x_4 with | Ok x_4 -> - (try - if - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty - then false - else - (proj x_4) = - (Ortac_runtime.Gospelstdlib.__mix_Bub - state__017_.contents - (Ortac_runtime.Gospelstdlib.(-) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) - (Ortac_runtime.Gospelstdlib.integer_of_int 1))) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 33; - pos_bol = 2160; - pos_cnum = 2174 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 35; - pos_bol = 2234; - pos_cnum = 2316 - } - }))) - | Error (Not_found) -> - (try - let __t1__020_ = - (Lazy.force new_state__019_).contents = - state__017_.contents in - let __t2__021_ = - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty in - __t1__020_ && __t2__021_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 36; - pos_bol = 2317; - pos_cnum = 2343 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 36; - pos_bol = 2317; - pos_cnum = 2387 - } - }))) - | _ -> false) - | (Push_front x_1, Res ((Unit, _), _)) -> true - | (Pop_front, Res ((Result (Elt (Char), Exn), _), x_5)) -> - (match x_5 with - | Ok x_5 -> - (try - if - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty - then false - else - (proj x_5) = - (Ortac_runtime.Gospelstdlib.Sequence.hd - state__017_.contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 56; - pos_bol = 3632; - pos_cnum = 3646 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 58; - pos_bol = 3706; - pos_cnum = 3762 - } - }))) + if + (try + if + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty + then false + else + (proj x_4) = + (Ortac_runtime.Gospelstdlib.__mix_Bub + state__017_.contents + (Ortac_runtime.Gospelstdlib.(-) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) + (Ortac_runtime.Gospelstdlib.integer_of_int 1))) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 33; + pos_bol = 2160; + pos_cnum = 2174 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 35; + pos_bol = 2234; + pos_cnum = 2316 + } + }))) + then None + else + Some + (Ortac_runtime.report "pop_back" + [("if old t.contents = Sequence.empty\n then false\n else proj x = (old t.contents)[Sequence.length (old t.contents) - 1]", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 33; + pos_bol = 2160; + pos_cnum = 2174 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 35; + pos_bol = 2234; + pos_cnum = 2316 + } + })]) | Error (Not_found) -> - (try - let __t1__022_ = - (Lazy.force new_state__019_).contents = - state__017_.contents in - let __t2__023_ = - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty in - __t1__022_ && __t2__023_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 59; - pos_bol = 3763; - pos_cnum = 3789 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 59; - pos_bol = 3763; - pos_cnum = 3833 - } - }))) - | _ -> false) - | (Insert_at (i_1, x_2), Res ((Result (Unit, Exn), _), res)) -> - if - (try - let __t1__024_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in - let __t2__025_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) in - __t1__024_ && __t2__025_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 72; - pos_bol = 4496; - pos_cnum = 4509 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 72; - pos_bol = 4496; - pos_cnum = 4545 - } - }))) - then (match res with | Ok _ -> true | _ -> false) - else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (Pop_at i_2, Res ((Result (Elt (Char), Exn), _), x_6)) -> - if - (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_2) - state__017_.contents) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 89; - pos_bol = 5403; - pos_cnum = 5416 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 89; - pos_bol = 5403; - pos_cnum = 5435 - } - }))) - then - (match x_6 with - | Ok x_6 -> + if (try - (proj x_6) = - (Ortac_runtime.Gospelstdlib.__mix_Bub - state__017_.contents - (Ortac_runtime.Gospelstdlib.integer_of_int i_2)) + let __t1__020_ = + (Lazy.force new_state__019_).contents = + state__017_.contents in + let __t2__021_ = + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty in + __t1__020_ && __t2__021_ with | e -> raise @@ -886,59 +794,54 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_spec.mli"; - pos_lnum = 92; - pos_bol = 5540; - pos_cnum = 5554 + pos_lnum = 36; + pos_bol = 2317; + pos_cnum = 2343 }; Ortac_runtime.stop = { pos_fname = "varray_spec.mli"; - pos_lnum = 92; - pos_bol = 5540; - pos_cnum = 5582 + pos_lnum = 36; + pos_bol = 2317; + pos_cnum = 2387 } }))) - | _ -> false) - else - (match x_6 with | Error (Invalid_argument _) -> true | _ -> false) - | (Delete_at i_3, Res ((Result (Unit, Exn), _), res)) -> - if - (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_3) - state__017_.contents) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 102; - pos_bol = 6066; - pos_cnum = 6079 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 102; - pos_bol = 6066; - pos_cnum = 6098 - } - }))) - then - (match res with - | Ok _ -> + then None + else + Some + (Ortac_runtime.report "pop_back" + [("t.contents = old t.contents = Sequence.empty", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 36; + pos_bol = 2317; + pos_cnum = 2343 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 36; + pos_bol = 2317; + pos_cnum = 2387 + } + })]) + | _ -> None) + | (Push_front x_1, Res ((Unit, _), _)) -> None + | (Pop_front, Res ((Result (Elt (Char), Exn), _), x_5)) -> + (match x_5 with + | Ok x_5 -> + if (try - (Ortac_runtime.Gospelstdlib.Sequence.length - (Lazy.force new_state__019_).contents) - = - (Ortac_runtime.Gospelstdlib.(-) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) - (Ortac_runtime.Gospelstdlib.integer_of_int 1)) + if + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty + then false + else + (proj x_5) = + (Ortac_runtime.Gospelstdlib.Sequence.hd + state__017_.contents) with | e -> raise @@ -948,56 +851,49 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_spec.mli"; - pos_lnum = 105; - pos_bol = 6203; - pos_cnum = 6217 + pos_lnum = 56; + pos_bol = 3632; + pos_cnum = 3646 }; Ortac_runtime.stop = { pos_fname = "varray_spec.mli"; - pos_lnum = 105; - pos_bol = 6203; - pos_cnum = 6282 + pos_lnum = 58; + pos_bol = 3706; + pos_cnum = 3762 } }))) - | _ -> false) - else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (Get i_4, Res ((Result (Elt (Char), Exn), _), x_7)) -> - if - (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_4) - state__017_.contents) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 128; - pos_bol = 7220; - pos_cnum = 7233 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 128; - pos_bol = 7220; - pos_cnum = 7252 - } - }))) - then - (match x_7 with - | Ok x_7 -> + then None + else + Some + (Ortac_runtime.report "pop_front" + [("if old t.contents = Sequence.empty\n then false\n else proj x = Sequence.hd (old t.contents)", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 56; + pos_bol = 3632; + pos_cnum = 3646 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 58; + pos_bol = 3706; + pos_cnum = 3762 + } + })]) + | Error (Not_found) -> + if (try - (proj x_7) = - (Ortac_runtime.Gospelstdlib.__mix_Bub - (Lazy.force new_state__019_).contents - (Ortac_runtime.Gospelstdlib.integer_of_int i_4)) + let __t1__022_ = + (Lazy.force new_state__019_).contents = + state__017_.contents in + let __t2__023_ = + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty in + __t1__022_ && __t2__023_ with | e -> raise @@ -1007,27 +903,725 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_spec.mli"; - pos_lnum = 127; - pos_bol = 7181; - pos_cnum = 7195 + pos_lnum = 59; + pos_bol = 3763; + pos_cnum = 3789 }; Ortac_runtime.stop = { pos_fname = "varray_spec.mli"; - pos_lnum = 127; - pos_bol = 7181; - pos_cnum = 7219 + pos_lnum = 59; + pos_bol = 3763; + pos_cnum = 3833 } }))) - | _ -> false) - else - (match x_7 with | Error (Invalid_argument _) -> true | _ -> false) + then None + else + Some + (Ortac_runtime.report "pop_front" + [("t.contents = old t.contents = Sequence.empty", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 59; + pos_bol = 3763; + pos_cnum = 3789 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 59; + pos_bol = 3763; + pos_cnum = 3833 + } + })]) + | _ -> None) + | (Insert_at (i_1, x_2), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + let __t1__024_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__025_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__024_ && __t2__025_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4509 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4545 + } + })) + then None + else + Some + (Ortac_runtime.report "insert_at" + [("0 <= i <= Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4509 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4545 + } + })]) + with + | None -> (match res with | Ok _ -> None | _ -> None) + | _ -> + (match res with + | Error (Invalid_argument _) -> None + | _ -> + if + (try + let __t1__024_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__025_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__024_ && __t2__025_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4509 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4545 + } + }))) + then None + else + Some + (Ortac_runtime.report "insert_at" + [("0 <= i <= Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4509 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4545 + } + })]))) + | (Pop_at i_2, Res ((Result (Elt (Char), Exn), _), x_6)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_2) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5416 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5435 + } + })) + then None + else + Some + (Ortac_runtime.report "pop_at" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5416 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5435 + } + })]) + with + | None -> + (match x_6 with + | Ok x_6 -> + if + (try + (proj x_6) = + (Ortac_runtime.Gospelstdlib.__mix_Bub + state__017_.contents + (Ortac_runtime.Gospelstdlib.integer_of_int i_2)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 92; + pos_bol = 5540; + pos_cnum = 5554 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 92; + pos_bol = 5540; + pos_cnum = 5582 + } + }))) + then None + else + Some + (Ortac_runtime.report "pop_at" + [("(proj x) = old t.contents[i]", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 92; + pos_bol = 5540; + pos_cnum = 5554 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 92; + pos_bol = 5540; + pos_cnum = 5582 + } + })]) + | _ -> None) + | _ -> + (match x_6 with + | Error (Invalid_argument _) -> None + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_2) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5416 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5435 + } + }))) + then None + else + Some + (Ortac_runtime.report "pop_at" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5416 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5435 + } + })]))) + | (Delete_at i_3, Res ((Result (Unit, Exn), _), res)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_3) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6079 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6098 + } + })) + then None + else + Some + (Ortac_runtime.report "delete_at" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6079 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6098 + } + })]) + with + | None -> + (match res with + | Ok _ -> + if + (try + (Ortac_runtime.Gospelstdlib.Sequence.length + (Lazy.force new_state__019_).contents) + = + (Ortac_runtime.Gospelstdlib.(-) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) + (Ortac_runtime.Gospelstdlib.integer_of_int 1)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 105; + pos_bol = 6203; + pos_cnum = 6217 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 105; + pos_bol = 6203; + pos_cnum = 6282 + } + }))) + then None + else + Some + (Ortac_runtime.report "delete_at" + [("Sequence.length t.contents = Sequence.length (old t.contents) - 1", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 105; + pos_bol = 6203; + pos_cnum = 6217 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 105; + pos_bol = 6203; + pos_cnum = 6282 + } + })]) + | _ -> None) + | _ -> + (match res with + | Error (Invalid_argument _) -> None + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_3) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6079 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6098 + } + }))) + then None + else + Some + (Ortac_runtime.report "delete_at" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6079 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6098 + } + })]))) + | (Get i_4, Res ((Result (Elt (Char), Exn), _), x_7)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_4) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7233 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7252 + } + })) + then None + else + Some + (Ortac_runtime.report "get" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7233 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7252 + } + })]) + with + | None -> + (match x_7 with + | Ok x_7 -> + if + (try + (proj x_7) = + (Ortac_runtime.Gospelstdlib.__mix_Bub + (Lazy.force new_state__019_).contents + (Ortac_runtime.Gospelstdlib.integer_of_int i_4)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 127; + pos_bol = 7181; + pos_cnum = 7195 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 127; + pos_bol = 7181; + pos_cnum = 7219 + } + }))) + then None + else + Some + (Ortac_runtime.report "get" + [("(proj x) = t.contents[i]", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 127; + pos_bol = 7181; + pos_cnum = 7195 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 127; + pos_bol = 7181; + pos_cnum = 7219 + } + })]) + | _ -> None) + | _ -> + (match x_7 with + | Error (Invalid_argument _) -> None + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_4) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7233 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7252 + } + }))) + then None + else + Some + (Ortac_runtime.report "get" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7233 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7252 + } + })]))) | (Set (i_5, v), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_5) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7658 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7677 + } + })) + then None + else + Some + (Ortac_runtime.report "set" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7658 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7677 + } + })]) + with + | None -> (match res with | Ok _ -> None | _ -> None) + | _ -> + (match res with + | Error (Invalid_argument _) -> None + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_5) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7658 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7677 + } + }))) + then None + else + Some + (Ortac_runtime.report "set" + [("inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7658 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7677 + } + })]))) + | (Length, Res ((Int, _), l)) -> if (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_5) - state__017_.contents) - = true + (Ortac_runtime.Gospelstdlib.integer_of_int l) = + (Ortac_runtime.Gospelstdlib.Sequence.length + (Lazy.force new_state__019_).contents) with | e -> raise @@ -1037,94 +1631,45 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_spec.mli"; - pos_lnum = 137; - pos_bol = 7645; - pos_cnum = 7658 + pos_lnum = 144; + pos_bol = 8166; + pos_cnum = 8180 }; Ortac_runtime.stop = { pos_fname = "varray_spec.mli"; - pos_lnum = 137; - pos_bol = 7645; - pos_cnum = 7677 + pos_lnum = 144; + pos_bol = 8166; + pos_cnum = 8210 } }))) - then (match res with | Ok _ -> true | _ -> false) + then None else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (Length, Res ((Int, _), l)) -> - (try - (Ortac_runtime.Gospelstdlib.integer_of_int l) = - (Ortac_runtime.Gospelstdlib.Sequence.length - (Lazy.force new_state__019_).contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 144; - pos_bol = 8166; - pos_cnum = 8180 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 144; - pos_bol = 8166; - pos_cnum = 8210 - } - }))) + Some + (Ortac_runtime.report "length" + [("l = Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 144; + pos_bol = 8166; + pos_cnum = 8180 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 144; + pos_bol = 8166; + pos_cnum = 8210 + } + })]) | (Is_empty, Res ((Bool, _), b)) -> - (try - (b = true) = - ((Lazy.force new_state__019_).contents = - Ortac_runtime.Gospelstdlib.Sequence.empty) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 171; - pos_bol = 9662; - pos_cnum = 9676 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 171; - pos_bol = 9662; - pos_cnum = 9709 - } - }))) - | (Fill (pos, len, x_3), Res ((Result (Unit, Exn), _), res)) -> if (try - let __t1__026_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int pos) in - let __t2__027_ = - let __t1__028_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int len) in - let __t2__029_ = - Ortac_runtime.Gospelstdlib.(<) - (Ortac_runtime.Gospelstdlib.(+) - (Ortac_runtime.Gospelstdlib.integer_of_int pos) - (Ortac_runtime.Gospelstdlib.integer_of_int len)) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) in - __t1__028_ && __t2__029_ in - __t1__026_ && __t2__027_ + (b = true) = + ((Lazy.force new_state__019_).contents = + Ortac_runtime.Gospelstdlib.Sequence.empty) with | e -> raise @@ -1134,65 +1679,175 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_spec.mli"; - pos_lnum = 211; - pos_bol = 12225; - pos_cnum = 12238 + pos_lnum = 171; + pos_bol = 9662; + pos_cnum = 9676 }; Ortac_runtime.stop = { pos_fname = "varray_spec.mli"; - pos_lnum = 211; - pos_bol = 12225; - pos_cnum = 12300 + pos_lnum = 171; + pos_bol = 9662; + pos_cnum = 9709 } }))) - then (match res with | Ok _ -> true | _ -> false) + then None else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | _ -> true - let run cmd__032_ sut__033_ = - match cmd__032_ with - | Push_back x -> Res (unit, (push_back sut__033_ x)) - | Pop_back -> - Res - ((result (elt char) exn), - (protect (fun () -> pop_back sut__033_) ())) - | Push_front x_1 -> Res (unit, (push_front sut__033_ x_1)) - | Pop_front -> - Res - ((result (elt char) exn), - (protect (fun () -> pop_front sut__033_) ())) - | Insert_at (i_1, x_2) -> - Res - ((result unit exn), - (protect (fun () -> insert_at sut__033_ i_1 x_2) ())) - | Pop_at i_2 -> - Res - ((result (elt char) exn), - (protect (fun () -> pop_at sut__033_ i_2) ())) - | Delete_at i_3 -> - Res - ((result unit exn), - (protect (fun () -> delete_at sut__033_ i_3) ())) - | Get i_4 -> - Res - ((result (elt char) exn), - (protect (fun () -> get sut__033_ i_4) ())) - | Set (i_5, v) -> - Res - ((result unit exn), (protect (fun () -> set sut__033_ i_5 v) ())) - | Length -> Res (int, (length sut__033_)) - | Is_empty -> Res (bool, (is_empty sut__033_)) - | Fill (pos, len, x_3) -> - Res - ((result unit exn), - (protect (fun () -> fill sut__033_ pos len x_3) ())) - end -module STMTests = (STM_sequential.Make)(Spec) -let check_init_state () = () -let agree_prop cs = check_init_state (); STMTests.agree_prop cs + Some + (Ortac_runtime.report "is_empty" + [("b <-> t.contents = Sequence.empty", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 171; + pos_bol = 9662; + pos_cnum = 9676 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 171; + pos_bol = 9662; + pos_cnum = 9709 + } + })]) + | (Fill (pos, len, x_3), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + let __t1__026_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int pos) in + let __t2__027_ = + let __t1__028_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int len) in + let __t2__029_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int pos) + (Ortac_runtime.Gospelstdlib.integer_of_int len)) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__028_ && __t2__029_ in + __t1__026_ && __t2__027_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12238 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12300 + } + })) + then None + else + Some + (Ortac_runtime.report "fill" + [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12238 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12300 + } + })]) + with + | None -> (match res with | Ok _ -> None | _ -> None) + | _ -> + (match res with + | Error (Invalid_argument _) -> None + | _ -> + if + (try + let __t1__026_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int pos) in + let __t2__027_ = + let __t1__028_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int len) in + let __t2__029_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int + pos) + (Ortac_runtime.Gospelstdlib.integer_of_int + len)) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__028_ && __t2__029_ in + __t1__026_ && __t2__027_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12238 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12300 + } + }))) + then None + else + Some + (Ortac_runtime.report "fill" + [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12238 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12300 + } + })]))) + | _ -> None let _ = QCheck_base_runner.run_tests_main (let count = 1000 in - [QCheck.Test.make ~count ~name:"Varray_spec STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + [STMTests.agree_test ~count ~name:"Varray_spec STM tests" + check_init_state ortac_postcond]) diff --git a/ortac-runtime-qcheck-stm.opam b/ortac-runtime-qcheck-stm.opam new file mode 100644 index 00000000..ff6e938c --- /dev/null +++ b/ortac-runtime-qcheck-stm.opam @@ -0,0 +1,40 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "Runtime support library for Ortac/QCheck-STM-generated code" +description: """ +The ortac-runtime-qcheck-stm library provides support for the code +generated by the Ortac/QCheck-STM plugin (provided by the +ortac-qcheck-stm package). + +Ortac (OCaml Runtime Assertion Checking) is a tool to turn +executable Gospel specifications into code to test they hold. +""" +maintainer: ["Nicolas Osborne "] +authors: ["Nicolas Osborne "] +license: "MIT" +homepage: "https://github.com/ocaml-gospel/ortac" +bug-reports: "https://github.com/ocaml-gospel/ortac/issues" +depends: [ + "dune" {>= "3.8"} + "ocaml" {>= "4.11.0"} + "qcheck-stm" + "ortac-runtime" + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "--promote-install-files=false" + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] + ["dune" "install" "-p" name "--create-install-files" name] +] +dev-repo: "git+https://github.com/ocaml-gospel/ortac.git" diff --git a/plugins/dune-rules/src/qcheck_stm.ml b/plugins/dune-rules/src/qcheck_stm.ml index 3adf03b8..0acd2601 100644 --- a/plugins/dune-rules/src/qcheck_stm.ml +++ b/plugins/dune-rules/src/qcheck_stm.ml @@ -61,7 +61,7 @@ let libraries = let k ppf config = pf ppf "libraries@ %s@ qcheck-stm.stm@ qcheck-stm.sequential@ \ - qcheck-multicoretests-util@ ortac-runtime" + qcheck-multicoretests-util@ ortac-runtime-qcheck-stm" config.interface_file in stanza k diff --git a/plugins/dune-rules/test/test.t b/plugins/dune-rules/test/test.t index 289d7bc7..14ed7bc2 100644 --- a/plugins/dune-rules/test/test.t +++ b/plugins/dune-rules/test/test.t @@ -57,7 +57,7 @@ generated. qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime) + ortac-runtime-qcheck-stm) (package my_package) (action (run @@ -127,7 +127,7 @@ this fact. qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime) + ortac-runtime-qcheck-stm) (package my_package) (action (run diff --git a/plugins/qcheck-stm/src/ir.ml b/plugins/qcheck-stm/src/ir.ml index 5e48129b..92a956bf 100644 --- a/plugins/qcheck-stm/src/ir.ml +++ b/plugins/qcheck-stm/src/ir.ml @@ -1,14 +1,26 @@ open Gospel module Ident = Identifier.Ident -type xpost = Ttypes.xsymbol * Tterm.pattern option * Tterm.term +type term = { term : Tterm.term; text : string } + +let term ~prj_txt ~prj_loc spec term = + let text = Ortac_core.Utils.term_printer (prj_txt spec) (prj_loc spec) term in + { term; text } + +let term_val = + term ~prj_txt:(fun s -> s.Tast.sp_text) ~prj_loc:(fun s -> s.Tast.sp_loc) + +let term_type = + term ~prj_txt:(fun s -> s.Tast.ty_text) ~prj_loc:(fun s -> s.Tast.ty_loc) + +type xpost = Ttypes.xsymbol * Tterm.pattern option * term type new_state_formulae = { model : Ident.t; (* the name of the model's field *) description : Tterm.term; (* the new value for the model's field *) } -type term = int * Tterm.term +type indexed_term = int * term (* XXX TODO decide whether we need checks here (if checks is false, state does not change) *) @@ -20,9 +32,9 @@ type next_state = { } type postcond = { - normal : term list; + normal : indexed_term list; exceptional : xpost list; - checks : Tterm.term list; + checks : term list; } type value = { @@ -56,7 +68,7 @@ let value id ty inst sut_var args ret next_state precond postcond = type t = { state : (Ident.t * Ppxlib.core_type) list; - invariants : (Ident.t * Tterm.term list) option; + invariants : (Ident.t * term list) option; init_state : init_state; ghost_functions : Tast.function_ list; values : value list; diff --git a/plugins/qcheck-stm/src/ir_of_gospel.ml b/plugins/qcheck-stm/src/ir_of_gospel.ml index ad508a4b..1d6a2acf 100644 --- a/plugins/qcheck-stm/src/ir_of_gospel.ml +++ b/plugins/qcheck-stm/src/ir_of_gospel.ml @@ -168,24 +168,34 @@ let next_state sut state spec = ok Ir.{ formulae; modifies } let postcond spec = - let normal = List.mapi (fun i x -> (i, x)) spec.sp_post + let normal = List.mapi (fun i x -> (i, Ir.term_val spec x)) spec.sp_post and exceptional = List.concat_map (fun (x, l) -> match l with - | [] -> [ (x, None, Tterm_helper.t_true Ppxlib.Location.none) ] + | [] -> + [ + ( x, + None, + Ir. + { + term = Tterm_helper.t_true Ppxlib.Location.none; + text = "true"; + } ); + ] | _ -> List.rev_map (fun (p, t) -> let open Tterm in match p.p_node with | Papp (ls, []) when Symbols.(ls_equal ls (fs_tuple 0)) -> - (x, None, t) - | _ -> (x, Some p, t)) + (x, None, Ir.term_val spec t) + | _ -> (x, Some p, Ir.term_val spec t)) l) spec.sp_xpost in - Ir.{ normal; exceptional; checks = spec.sp_checks } + Ir. + { normal; exceptional; checks = List.map (Ir.term_val spec) spec.sp_checks } let val_desc config state vd = let open Reserr in @@ -254,7 +264,9 @@ let state_and_invariants config sigs = | xs -> List.map process_model xs |> ok in let invariants = - Option.map (fun (vs, xs) -> (vs.Symbols.vs_name, xs)) spec.ty_invariants + Option.map + (fun (vs, xs) -> (vs.Symbols.vs_name, List.map (Ir.term_type spec) xs)) + spec.ty_invariants in ok (state, invariants) diff --git a/plugins/qcheck-stm/src/runtime/dune b/plugins/qcheck-stm/src/runtime/dune new file mode 100644 index 00000000..5f367d15 --- /dev/null +++ b/plugins/qcheck-stm/src/runtime/dune @@ -0,0 +1,10 @@ +(library + (name ortac_runtime_qcheck_stm) + (public_name ortac-runtime-qcheck-stm) + (libraries + qcheck-core + qcheck-core.runner + qcheck-stm.stm + qcheck-stm.sequential + qcheck-multicoretests-util + ortac-runtime)) diff --git a/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml b/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml new file mode 100644 index 00000000..a3b453a3 --- /dev/null +++ b/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml @@ -0,0 +1,73 @@ +open STM +include Ortac_runtime + +type report = { cmd : string; terms : (string * location) list } + +let report cmd terms = { cmd; terms } + +let append a b = + match (a, b) with + | None, None -> None + | Some _, None -> a + | None, Some _ -> b + | Some { cmd = cmd0; terms = terms0 }, Some { cmd = cmd1; terms = terms1 } -> + assert (cmd0 = cmd1); + Some (report cmd0 (terms0 @ terms1)) + +module Make (Spec : Spec) = struct + open QCheck + module Internal = Internal.Make (Spec) [@alert "-internal"] + + let pp_trace ppf trace = + let open Fmt in + let pp_aux ppf (c, r) = pf ppf "%s : %s" (Spec.show_cmd c) (show_res r) in + pf ppf "@[%a@]" (list ~sep:(any "@\n") pp_aux) trace + + let pp_terms ppf err = + let open Fmt in + let pp_aux ppf (term, l) = pf ppf "@[%a@\n @[%s@]@]@\n" pp_loc l term in + pf ppf "%a" (list ~sep:(any "@\n") pp_aux) err + + let message trace report = + Test.fail_reportf + "Gospel specification violation in function %s\n\ + @;\ + \ @[%a@]@\n\ + when executing the following sequence of operations:@\n\ + @;\ + \ @[%a@]@." report.cmd pp_terms report.terms pp_trace trace + + let rec check_disagree postcond s sut cs = + match cs with + | [] -> None + | c :: cs -> ( + let res = Spec.run c sut in + (* This functor will be called after a modified postcond has been + defined, returning a list of 3-plets containing the command, the + term and the location *) + match postcond c s res with + | None -> ( + let s' = Spec.next_state c s in + match check_disagree postcond s' sut cs with + | None -> None + | Some (rest, report) -> Some ((c, res) :: rest, report)) + | Some report -> Some ([ (c, res) ], report)) + + let agree_prop check_init_state postcond cs = + check_init_state (); + assume (Internal.cmds_ok Spec.init_state cs); + let sut = Spec.init_sut () in + (* reset system's state *) + let res = + try Ok (check_disagree postcond Spec.init_state sut cs) + with exn -> Error exn + in + let () = Spec.cleanup sut in + let res = match res with Ok res -> res | Error exn -> raise exn in + match res with None -> true | Some (trace, report) -> message trace report + + let agree_test ~count ~name wrapped_init_state postcond = + Test.make ~name ~count + (Internal.arb_cmds Spec.init_state) + (agree_prop wrapped_init_state postcond) +end diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml index 43044dd8..06c665d2 100644 --- a/plugins/qcheck-stm/src/stm_of_ir.ml +++ b/plugins/qcheck-stm/src/stm_of_ir.ml @@ -8,6 +8,7 @@ let ty_default = Ptyp_constr (noloc (Lident "char"), []) let pat_default = ppat_construct (lident "Char") None let exp_default = evar "char" let res_default = Ident.create ~loc:Location.none "res" +let list_append = list_fold_expr (qualify [ "Ortac_runtime" ] "append") "None" let may_raise_exception v = match (v.postcond.exceptional, v.postcond.checks) with @@ -138,7 +139,7 @@ let subst_term state ?(out_of_scope = []) ~gos_t ?(old_lz = false) ~old_t let translate_checks config state value state_ident t = let open Reserr in subst_term state ~gos_t:value.sut_var ~old_t:(Some state_ident) - ~new_t:(Some state_ident) t + ~new_t:(Some state_ident) t.term >>= ocaml_of_term config let str_of_ident = Fmt.str "%a" Ident.pp @@ -424,12 +425,22 @@ let postcond_case config state invariants idx state_ident new_state_ident value let open Reserr in let translate_postcond t = subst_term state ~gos_t:value.sut_var ~old_t:(Some state_ident) ~new_lz:true - ~new_t:(Some new_state_ident) t + ~new_t:(Some new_state_ident) t.term >>= ocaml_of_term config and translate_invariants id t = subst_term state ~gos_t:id ~old_t:None ~new_t:(Some new_state_ident) - ~new_lz:true t + ~new_lz:true t.term >>= ocaml_of_term config + and wrap_check t e = + let term = estring t.text + and cmd = Fmt.str "%a" Ident.pp value.id |> estring + and l = t.Ir.term.Gospel.Tterm.t_loc |> elocation in + pexp_ifthenelse e enone + (Some + (esome + @@ pexp_apply + (qualify [ "Ortac_runtime" ] "report") + [ (Nolabel, cmd); (Nolabel, elist [ pexp_tuple [ term; l ] ]) ])) in let idx = List.sort Int.compare idx in let lhs0 = mk_cmd_pattern value in @@ -480,13 +491,14 @@ let postcond_case config state invariants idx state_ident new_state_ident value in aux idx value.postcond.normal in - let* postcond = map translate_postcond normal + let* postcond = map (fun t -> wrap_check t <$> translate_postcond t) normal and* invariants = Option.fold ~none:(ok []) - ~some:(fun (id, xs) -> map (translate_invariants id) xs) + ~some:(fun (id, xs) -> + map (fun t -> wrap_check t <$> translate_invariants id t) xs) invariants in - list_and (postcond @ invariants) |> ok + list_append (postcond @ invariants) |> ok in let res, pat_ret = match value.ret with @@ -505,7 +517,7 @@ let postcond_case config state invariants idx state_ident new_state_ident value case ~lhs:(ppat_construct (lident "Ok") (Some pat_ret)) ~guard:None ~rhs in let* cases_error = - Fun.flip ( @ ) [ case ~lhs:ppat_any ~guard:None ~rhs:(ebool false) ] + Fun.flip ( @ ) [ case ~lhs:ppat_any ~guard:None ~rhs:enone ] <$> map (fun (x, p, t) -> let lhs = @@ -514,7 +526,7 @@ let postcond_case config state invariants idx state_ident new_state_ident value (Option.map Ortac_core.Ocaml_of_gospel.pattern p) in let lhs = ppat_construct (lident "Error") (Some lhs) in - let* rhs = translate_postcond t in + let* rhs = wrap_check t <$> translate_postcond t in case ~lhs ~guard:None ~rhs |> ok) value.postcond.exceptional in @@ -523,22 +535,29 @@ let postcond_case config state invariants idx state_ident new_state_ident value in let* rhs = let translate_checks = translate_checks config state value state_ident in - let* checks = map translate_checks value.postcond.checks in + let* checks = + map (fun t -> wrap_check t <$> translate_checks t) value.postcond.checks + in match checks with | [] -> ok rhs | _ -> let inv_arg = ppat_construct (lident "Invalid_argument") (Some ppat_any) in - pexp_ifthenelse (list_and checks) rhs - (Some - (pexp_match res - [ - case - ~lhs:(ppat_construct (lident "Error") (Some inv_arg)) - ~guard:None ~rhs:(ebool true); - case ~lhs:ppat_any ~guard:None ~rhs:(ebool false); - ])) + let validate_inv_arg = + pexp_match res + [ + case + ~lhs:(ppat_construct (lident "Error") (Some inv_arg)) + ~guard:None ~rhs:enone; + case ~lhs:ppat_any ~guard:None ~rhs:(list_append checks); + ] + in + pexp_match (list_append checks) + [ + case ~lhs:(ppat_construct (lident "None") None) ~guard:None ~rhs; + case ~lhs:ppat_any ~guard:None ~rhs:validate_inv_arg; + ] |> ok in ok (case ~lhs ~guard:None ~rhs) @@ -566,7 +585,7 @@ let postcond config idx ir = let new_state_ident = Ident.create ~loc:Location.none new_state_name in let open Reserr in let* cases = - (Fun.flip ( @ )) [ case ~lhs:ppat_any ~guard:None ~rhs:(ebool true) ] + (Fun.flip ( @ )) [ case ~lhs:ppat_any ~guard:None ~rhs:enone ] <$> map (fun v -> postcond_case config ir.state ir.invariants (List.assoc v.id idx) @@ -574,10 +593,14 @@ let postcond config idx ir = ir.values in let body = - pexp_match (pexp_tuple [ evar cmd_name; evar res_name ]) cases - |> new_state_let - in - let pat = pvar "postcond" in + pexp_open + Ast_helper.(Opn.mk (Mod.ident (lident "Spec"))) + (pexp_open + Ast_helper.(Opn.mk (Mod.ident (lident "STM"))) + (pexp_match (pexp_tuple [ evar cmd_name; evar res_name ]) cases + |> new_state_let)) + in + let pat = pvar "ortac_postcond" in let expr = efun [ @@ -589,6 +612,14 @@ let postcond config idx ir = in pstr_value Nonrecursive [ value_binding ~pat ~expr ] |> ok +let dummy_postcond = + let expr = + efun + [ (Nolabel, ppat_any); (Nolabel, ppat_any); (Nolabel, ppat_any) ] + (ebool true) + and pat = pvar "postcond" in + pstr_value Nonrecursive [ value_binding ~pat ~expr ] + let cmd_constructor value = let name = String.capitalize_ascii value.id.Ident.id_str |> noloc in let args = @@ -737,7 +768,7 @@ let check_init_state config ir = and state_id = Ident.create ~loc:Location.none state_name in let translate_invariants id t = enot - <$> (subst_term ir.state ~gos_t:id ~old_t:None ~new_t:(Some state_id) t + <$> (subst_term ir.state ~gos_t:id ~old_t:None ~new_t:(Some state_id) t.term >>= ocaml_of_term config) and msg = let f = qualify [ "QCheck"; "Test" ] "fail_report" @@ -845,8 +876,7 @@ let stm include_ config ir = let open_mod m = pstr_open Ast_helper.(Opn.mk (Mod.ident (lident m))) in let spec_expr = pmod_structure - ([ open_mod "STM"; warn ] - @ incl + ((open_mod "STM" :: incl) @ [ sut; cmd; @@ -858,7 +888,7 @@ let stm include_ config ir = arb_cmd; next_state; precond; - postcond; + dummy_postcond; run; ]) in @@ -870,7 +900,7 @@ let stm include_ config ir = (module_binding ~name:(noloc (Some "STMTests")) ~expr: (pmod_apply - (pmod_ident (Ldot (Lident "STM_sequential", "Make") |> noloc)) + (pmod_ident (Ldot (Lident "Ortac_runtime", "Make") |> noloc)) (pmod_ident (lident "Spec")))) in let module_name = Ortac_core.Context.module_name config.context in @@ -882,12 +912,13 @@ let stm include_ config ir = QCheck_base_runner.run_tests_main (let count = 1000 in [ - QCheck.Test.make ~count ~name:[%e descr] - (STMTests.arb_cmds Spec.init_state) - agree_prop; + STMTests.agree_test ~count ~name:[%e descr] check_init_state + ortac_postcond; ])] in ok - ([ open_mod module_name ] - @ ghost_functions - @ [ stm_spec; tests; check_init_state; agree_prop; call_tests ]) + (warn + :: open_mod module_name + :: [%stri module Ortac_runtime = Ortac_runtime_qcheck_stm] + :: ghost_functions + @ [ stm_spec; tests; check_init_state; postcond; call_tests ]) diff --git a/plugins/qcheck-stm/test/array_stm_tests.expected.ml b/plugins/qcheck-stm/test/array_stm_tests.expected.ml index 5da66780..5a5c22cd 100644 --- a/plugins/qcheck-stm/test/array_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/array_stm_tests.expected.ml @@ -1,10 +1,11 @@ (* This file is generated by ortac qcheck-stm, edit how you run the tool instead *) +[@@@ocaml.warning "-26-27"] open Array +module Ortac_runtime = Ortac_runtime_qcheck_stm module Spec = struct open STM - [@@@ocaml.warning "-26-27"] type sut = char t type cmd = | Length @@ -311,45 +312,33 @@ module Spec = | Fill (i_2, j, a_2) -> true | To_list -> true | Mem a_3 -> true - let postcond cmd__008_ state__009_ res__010_ = + let postcond _ _ _ = true + let run cmd__018_ sut__019_ = + match cmd__018_ with + | Length -> Res (int, (length sut__019_)) + | Get i -> + Res ((result char exn), (protect (fun () -> get sut__019_ i) ())) + | Set (i_1, a_1) -> + Res + ((result unit exn), + (protect (fun () -> set sut__019_ i_1 a_1) ())) + | Fill (i_2, j, a_2) -> + Res + ((result unit exn), + (protect (fun () -> fill sut__019_ i_2 j a_2) ())) + | To_list -> Res ((list char), (to_list sut__019_)) + | Mem a_3 -> Res (bool, (mem a_3 sut__019_)) + end +module STMTests = (Ortac_runtime.Make)(Spec) +let check_init_state () = () +let ortac_postcond cmd__008_ state__009_ res__010_ = + let open Spec in + let open STM in let new_state__011_ = lazy (next_state cmd__008_ state__009_) in match (cmd__008_, res__010_) with | (Length, Res ((Int, _), i_3)) -> - (try i_3 = (Lazy.force new_state__011_).size - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "array.mli"; - pos_lnum = 7; - pos_bol = 238; - pos_cnum = 250 - }; - Ortac_runtime.stop = - { - pos_fname = "array.mli"; - pos_lnum = 7; - pos_bol = 238; - pos_cnum = 260 - } - }))) - | (Get i, Res ((Result (Char, Exn), _), a_4)) -> if - (try - let __t1__012_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int i) in - let __t2__013_ = - Ortac_runtime.Gospelstdlib.(<) - (Ortac_runtime.Gospelstdlib.integer_of_int i) - (Ortac_runtime.Gospelstdlib.integer_of_int - state__009_.size) in - __t1__012_ && __t2__013_ + (try i_3 = (Lazy.force new_state__011_).size with | e -> raise @@ -359,63 +348,625 @@ module Spec = Ortac_runtime.start = { pos_fname = "array.mli"; - pos_lnum = 11; - pos_bol = 378; - pos_cnum = 389 + pos_lnum = 7; + pos_bol = 238; + pos_cnum = 250 }; Ortac_runtime.stop = { pos_fname = "array.mli"; - pos_lnum = 11; - pos_bol = 378; - pos_cnum = 404 + pos_lnum = 7; + pos_bol = 238; + pos_cnum = 260 } }))) - then - (match a_4 with - | Ok a_4 -> - (try - a_4 = - (Ortac_runtime.Gospelstdlib.List.nth - (Lazy.force new_state__011_).contents - (Ortac_runtime.Gospelstdlib.integer_of_int i)) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "array.mli"; - pos_lnum = 12; - pos_bol = 405; - pos_cnum = 417 - }; - Ortac_runtime.stop = - { - pos_fname = "array.mli"; - pos_lnum = 12; - pos_bol = 405; - pos_cnum = 442 - } - }))) - | _ -> false) + then None else - (match a_4 with | Error (Invalid_argument _) -> true | _ -> false) + Some + (Ortac_runtime.report "length" + [("i = t.size", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 7; + pos_bol = 238; + pos_cnum = 250 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 7; + pos_bol = 238; + pos_cnum = 260 + } + })]) + | (Get i, Res ((Result (Char, Exn), _), a_4)) -> + (match if + try + let __t1__012_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i) in + let __t2__013_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.integer_of_int i) + (Ortac_runtime.Gospelstdlib.integer_of_int + state__009_.size) in + __t1__012_ && __t2__013_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 389 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 404 + } + })) + then None + else + Some + (Ortac_runtime.report "get" + [("0 <= i < t.size", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 389 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 404 + } + })]) + with + | None -> + (match a_4 with + | Ok a_4 -> + if + (try + a_4 = + (Ortac_runtime.Gospelstdlib.List.nth + (Lazy.force new_state__011_).contents + (Ortac_runtime.Gospelstdlib.integer_of_int i)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 12; + pos_bol = 405; + pos_cnum = 417 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 12; + pos_bol = 405; + pos_cnum = 442 + } + }))) + then None + else + Some + (Ortac_runtime.report "get" + [("a = List.nth t.contents i", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 12; + pos_bol = 405; + pos_cnum = 417 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 12; + pos_bol = 405; + pos_cnum = 442 + } + })]) + | _ -> None) + | _ -> + (match a_4 with + | Error (Invalid_argument _) -> None + | _ -> + if + (try + let __t1__012_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i) in + let __t2__013_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.integer_of_int i) + (Ortac_runtime.Gospelstdlib.integer_of_int + state__009_.size) in + __t1__012_ && __t2__013_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 389 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 404 + } + }))) + then None + else + Some + (Ortac_runtime.report "get" + [("0 <= i < t.size", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 389 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 404 + } + })]))) | (Set (i_1, a_1), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + let __t1__014_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__015_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.integer_of_int + state__009_.size) in + __t1__014_ && __t2__015_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 593 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 608 + } + })) + then None + else + Some + (Ortac_runtime.report "set" + [("0 <= i < t.size", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 593 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 608 + } + })]) + with + | None -> (match res with | Ok _ -> None | _ -> None) + | _ -> + (match res with + | Error (Invalid_argument _) -> None + | _ -> + if + (try + let __t1__014_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__015_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.integer_of_int + state__009_.size) in + __t1__014_ && __t2__015_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 593 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 608 + } + }))) + then None + else + Some + (Ortac_runtime.report "set" + [("0 <= i < t.size", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 593 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 608 + } + })]))) + | (Fill (i_2, j, a_2), Res ((Result (Unit, Exn), _), res)) -> + (match Ortac_runtime.append + (if + try + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_2) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1194 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1200 + } + })) + then None + else + Some + (Ortac_runtime.report "fill" + [("0 <= i", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1194 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1200 + } + })])) + (Ortac_runtime.append + (if + try + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int j) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1212 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1218 + } + })) + then None + else + Some + (Ortac_runtime.report "fill" + [("0 <= j", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1212 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1218 + } + })])) + (if + try + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int + i_2) + (Ortac_runtime.Gospelstdlib.integer_of_int j)) + (Ortac_runtime.Gospelstdlib.integer_of_int + state__009_.size) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1230 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1245 + } + })) + then None + else + Some + (Ortac_runtime.report "fill" + [("i + j <= t.size", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1230 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1245 + } + })]))) + with + | None -> (match res with | Ok _ -> None | _ -> None) + | _ -> + (match res with + | Error (Invalid_argument _) -> None + | _ -> + Ortac_runtime.append + (if + try + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_2) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1194 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1200 + } + })) + then None + else + Some + (Ortac_runtime.report "fill" + [("0 <= i", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1194 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1200 + } + })])) + (Ortac_runtime.append + (if + try + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int j) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1212 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1218 + } + })) + then None + else + Some + (Ortac_runtime.report "fill" + [("0 <= j", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1212 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1218 + } + })])) + (if + try + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int + i_2) + (Ortac_runtime.Gospelstdlib.integer_of_int + j)) + (Ortac_runtime.Gospelstdlib.integer_of_int + state__009_.size) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1230 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1245 + } + })) + then None + else + Some + (Ortac_runtime.report "fill" + [("i + j <= t.size", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1230 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1245 + } + })]))))) + | (To_list, Res ((List (Char), _), l)) -> if - (try - let __t1__014_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in - let __t2__015_ = - Ortac_runtime.Gospelstdlib.(<) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) - (Ortac_runtime.Gospelstdlib.integer_of_int - state__009_.size) in - __t1__014_ && __t2__015_ + (try l = (Lazy.force new_state__011_).contents with | e -> raise @@ -425,27 +976,45 @@ module Spec = Ortac_runtime.start = { pos_fname = "array.mli"; - pos_lnum = 16; - pos_bol = 582; - pos_cnum = 593 + pos_lnum = 36; + pos_bol = 1559; + pos_cnum = 1571 }; Ortac_runtime.stop = { pos_fname = "array.mli"; - pos_lnum = 16; - pos_bol = 582; - pos_cnum = 608 + pos_lnum = 36; + pos_bol = 1559; + pos_cnum = 1585 } }))) - then (match res with | Ok _ -> true | _ -> false) + then None else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (Fill (i_2, j, a_2), Res ((Result (Unit, Exn), _), res)) -> + Some + (Ortac_runtime.report "to_list" + [("l = t.contents", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 36; + pos_bol = 1559; + pos_cnum = 1571 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 36; + pos_bol = 1559; + pos_cnum = 1585 + } + })]) + | (Mem a_3, Res ((Bool, _), b)) -> if (try - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int i_2) + (b = true) = + (Ortac_runtime.Gospelstdlib.List.mem a_3 + (Lazy.force new_state__011_).contents) with | e -> raise @@ -455,147 +1024,42 @@ module Spec = Ortac_runtime.start = { pos_fname = "array.mli"; - pos_lnum = 28; - pos_bol = 1183; - pos_cnum = 1194 + pos_lnum = 40; + pos_bol = 1709; + pos_cnum = 1721 }; Ortac_runtime.stop = { pos_fname = "array.mli"; - pos_lnum = 28; - pos_bol = 1183; - pos_cnum = 1200 + pos_lnum = 40; + pos_bol = 1709; + pos_cnum = 1746 } }))) - && - ((try - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int j) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "array.mli"; - pos_lnum = 29; - pos_bol = 1201; - pos_cnum = 1212 - }; - Ortac_runtime.stop = - { - pos_fname = "array.mli"; - pos_lnum = 29; - pos_bol = 1201; - pos_cnum = 1218 - } - }))) - && - ((try - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.(+) - (Ortac_runtime.Gospelstdlib.integer_of_int i_2) - (Ortac_runtime.Gospelstdlib.integer_of_int j)) - (Ortac_runtime.Gospelstdlib.integer_of_int - state__009_.size) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "array.mli"; - pos_lnum = 30; - pos_bol = 1219; - pos_cnum = 1230 - }; - Ortac_runtime.stop = - { - pos_fname = "array.mli"; - pos_lnum = 30; - pos_bol = 1219; - pos_cnum = 1245 - } - }))))) - then (match res with | Ok _ -> true | _ -> false) + then None else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (To_list, Res ((List (Char), _), l)) -> - (try l = (Lazy.force new_state__011_).contents - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "array.mli"; - pos_lnum = 36; - pos_bol = 1559; - pos_cnum = 1571 - }; - Ortac_runtime.stop = - { - pos_fname = "array.mli"; - pos_lnum = 36; - pos_bol = 1559; - pos_cnum = 1585 - } - }))) - | (Mem a_3, Res ((Bool, _), b)) -> - (try - (b = true) = - (Ortac_runtime.Gospelstdlib.List.mem a_3 - (Lazy.force new_state__011_).contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "array.mli"; - pos_lnum = 40; - pos_bol = 1709; - pos_cnum = 1721 - }; - Ortac_runtime.stop = - { - pos_fname = "array.mli"; - pos_lnum = 40; - pos_bol = 1709; - pos_cnum = 1746 - } - }))) - | _ -> true - let run cmd__018_ sut__019_ = - match cmd__018_ with - | Length -> Res (int, (length sut__019_)) - | Get i -> - Res ((result char exn), (protect (fun () -> get sut__019_ i) ())) - | Set (i_1, a_1) -> - Res - ((result unit exn), - (protect (fun () -> set sut__019_ i_1 a_1) ())) - | Fill (i_2, j, a_2) -> - Res - ((result unit exn), - (protect (fun () -> fill sut__019_ i_2 j a_2) ())) - | To_list -> Res ((list char), (to_list sut__019_)) - | Mem a_3 -> Res (bool, (mem a_3 sut__019_)) - end -module STMTests = (STM_sequential.Make)(Spec) -let check_init_state () = () -let agree_prop cs = check_init_state (); STMTests.agree_prop cs + Some + (Ortac_runtime.report "mem" + [("b = List.mem a t.contents", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 40; + pos_bol = 1709; + pos_cnum = 1721 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 40; + pos_bol = 1709; + pos_cnum = 1746 + } + })]) + | _ -> None let _ = QCheck_base_runner.run_tests_main (let count = 1000 in - [QCheck.Test.make ~count ~name:"Array STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + [STMTests.agree_test ~count ~name:"Array STM tests" check_init_state + ortac_postcond]) 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 38056870..5a4c7ed6 100644 --- a/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml @@ -1,6 +1,8 @@ (* This file is generated by ortac qcheck-stm, edit how you run the tool instead *) +[@@@ocaml.warning "-26-27"] open Conjunctive_clauses +module Ortac_runtime = Ortac_runtime_qcheck_stm let set_contents c i a_1 = try Ortac_runtime.Gospelstdlib.List.mapi @@ -29,7 +31,6 @@ let set_contents c i a_1 = module Spec = struct open STM - [@@@ocaml.warning "-26-27"] type sut = char t type cmd = | Set of int * char @@ -146,47 +147,7 @@ module Spec = else state__003_ let precond cmd__012_ state__013_ = match cmd__012_ with | Set (i_1, a_2) -> true - let postcond cmd__006_ state__007_ res__008_ = - let new_state__009_ = lazy (next_state cmd__006_ state__007_) in - match (cmd__006_, res__008_) with - | (Set (i_1, a_2), Res ((Result (Unit, Exn), _), res)) -> - if - (try - let __t1__010_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in - let __t2__011_ = - Ortac_runtime.Gospelstdlib.(<) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) - (Ortac_runtime.Gospelstdlib.List.length - state__007_.contents) in - __t1__010_ && __t2__011_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 13; - pos_bol = 806; - pos_cnum = 817 - }; - Ortac_runtime.stop = - { - pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 13; - pos_bol = 806; - pos_cnum = 848 - } - }))) - then (match res with | Ok _ -> true | _ -> false) - else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | _ -> true + let postcond _ _ _ = true let run cmd__014_ sut__015_ = match cmd__014_ with | Set (i_1, a_2) -> @@ -194,11 +155,131 @@ module Spec = ((result unit exn), (protect (fun () -> set sut__015_ i_1 a_2) ())) end -module STMTests = (STM_sequential.Make)(Spec) +module STMTests = (Ortac_runtime.Make)(Spec) let check_init_state () = () -let agree_prop cs = check_init_state (); STMTests.agree_prop cs +let ortac_postcond cmd__006_ state__007_ res__008_ = + let open Spec in + let open STM in + let new_state__009_ = lazy (next_state cmd__006_ state__007_) in + match (cmd__006_, res__008_) with + | (Set (i_1, a_2), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + let __t1__010_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__011_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.List.length + state__007_.contents) in + __t1__010_ && __t2__011_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 817 + }; + Ortac_runtime.stop = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 848 + } + })) + then None + else + Some + (Ortac_runtime.report "set" + [("0 <= i < List.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 817 + }; + Ortac_runtime.stop = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 848 + } + })]) + with + | None -> (match res with | Ok _ -> None | _ -> None) + | _ -> + (match res with + | Error (Invalid_argument _) -> None + | _ -> + if + (try + let __t1__010_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__011_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.List.length + state__007_.contents) in + __t1__010_ && __t2__011_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 817 + }; + Ortac_runtime.stop = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 848 + } + }))) + then None + else + Some + (Ortac_runtime.report "set" + [("0 <= i < List.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 817 + }; + Ortac_runtime.stop = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 848 + } + })]))) + | _ -> None let _ = QCheck_base_runner.run_tests_main (let count = 1000 in - [QCheck.Test.make ~count ~name:"Conjunctive_clauses STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + [STMTests.agree_test ~count ~name:"Conjunctive_clauses STM tests" + check_init_state ortac_postcond]) diff --git a/plugins/qcheck-stm/test/dune.inc b/plugins/qcheck-stm/test/dune.inc index b90555f8..b5bfa7b4 100644 --- a/plugins/qcheck-stm/test/dune.inc +++ b/plugins/qcheck-stm/test/dune.inc @@ -32,7 +32,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm array) (action (echo @@ -85,7 +85,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm hashtbl) (action (echo @@ -138,7 +138,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm record) (action (echo @@ -191,7 +191,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm ref) (action (echo @@ -244,7 +244,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm conjunctive_clauses) (action (echo @@ -297,7 +297,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm sequence_model) (action (echo @@ -350,7 +350,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm invariants) (action (echo diff --git a/plugins/qcheck-stm/test/dune_gen.ml b/plugins/qcheck-stm/test/dune_gen.ml index e373efbf..57e5fe29 100644 --- a/plugins/qcheck-stm/test/dune_gen.ml +++ b/plugins/qcheck-stm/test/dune_gen.ml @@ -45,7 +45,7 @@ let rec print_rules pos = qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm %s) (action (echo diff --git a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml index df18799e..335b4c10 100644 --- a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml @@ -1,6 +1,8 @@ (* This file is generated by ortac qcheck-stm, edit how you run the tool instead *) +[@@@ocaml.warning "-26-27"] open Hashtbl +module Ortac_runtime = Ortac_runtime_qcheck_stm let rec remove_first x xs_1 = try match xs_1 with @@ -31,7 +33,6 @@ let rec remove_first x xs_1 = module Spec = struct open STM - [@@@ocaml.warning "-26-27"] type sut = (char, int) t type cmd = | Clear @@ -261,193 +262,7 @@ module Spec = | Remove a_7 -> true | Replace (a_8, b_3) -> true | Length -> true - let postcond cmd__004_ state__005_ res__006_ = - let new_state__007_ = lazy (next_state cmd__004_ state__005_) in - match (cmd__004_, res__006_) with - | (Clear, Res ((Unit, _), _)) -> true - | (Reset, Res ((Unit, _), _)) -> true - | (Add (a_2, b_2), Res ((Unit, _), _)) -> true - | (Find a_3, Res ((Result (Int, Exn), _), b_4)) -> - (match b_4 with - | Ok b_4 -> - (try - Ortac_runtime.Gospelstdlib.List.mem (a_3, b_4) - (Lazy.force new_state__007_).contents - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 32; - pos_bol = 1360; - pos_cnum = 1372 - }; - Ortac_runtime.stop = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 32; - pos_bol = 1360; - pos_cnum = 1398 - } - }))) - | Error (Not_found) -> - (try - not - (Ortac_runtime.Gospelstdlib.List.mem a_3 - (Ortac_runtime.Gospelstdlib.List.map - Ortac_runtime.Gospelstdlib.fst - (Lazy.force new_state__007_).contents)) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 31; - pos_bol = 1293; - pos_cnum = 1317 - }; - Ortac_runtime.stop = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 31; - pos_bol = 1293; - pos_cnum = 1359 - } - }))) - | _ -> false) - | (Find_opt a_4, Res ((Option (Int), _), o)) -> - (try - (match o with - | None -> - if - not - (Ortac_runtime.Gospelstdlib.List.mem a_4 - (Ortac_runtime.Gospelstdlib.List.map - Ortac_runtime.Gospelstdlib.fst - (Lazy.force new_state__007_).contents)) - then true - else false - | Some b_5 -> - if - Ortac_runtime.Gospelstdlib.List.mem (a_4, b_5) - (Lazy.force new_state__007_).contents - then true - else false) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 36; - pos_bol = 1559; - pos_cnum = 1571 - }; - Ortac_runtime.stop = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 38; - pos_bol = 1643; - pos_cnum = 1687 - } - }))) - | (Find_all a_5, Res ((List (Int), _), bs)) -> - (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 new_state__007_).contents)) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 42; - pos_bol = 1853; - pos_cnum = 1865 - }; - Ortac_runtime.stop = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 42; - pos_bol = 1853; - pos_cnum = 1947 - } - }))) - | (Mem a_6, Res ((Bool, _), b_6)) -> - (try - (b_6 = true) = - (Ortac_runtime.Gospelstdlib.List.mem a_6 - (Ortac_runtime.Gospelstdlib.List.map - Ortac_runtime.Gospelstdlib.fst - (Lazy.force new_state__007_).contents)) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 46; - pos_bol = 2149; - pos_cnum = 2161 - }; - Ortac_runtime.stop = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 46; - pos_bol = 2149; - pos_cnum = 2201 - } - }))) - | (Remove a_7, Res ((Unit, _), _)) -> true - | (Replace (a_8, b_3), Res ((Unit, _), _)) -> true - | (Length, Res ((Int, _), i)) -> - (try - (Ortac_runtime.Gospelstdlib.integer_of_int i) = - (Ortac_runtime.Gospelstdlib.List.length - (Lazy.force new_state__007_).contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 76; - pos_bol = 3727; - pos_cnum = 3739 - }; - Ortac_runtime.stop = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 76; - pos_bol = 3727; - pos_cnum = 3765 - } - }))) - | _ -> true + let postcond _ _ _ = true let run cmd__010_ sut__011_ = match cmd__010_ with | Clear -> Res (unit, (clear sut__011_)) @@ -462,11 +277,331 @@ module Spec = | Replace (a_8, b_3) -> Res (unit, (replace sut__011_ a_8 b_3)) | Length -> Res (int, (length sut__011_)) end -module STMTests = (STM_sequential.Make)(Spec) +module STMTests = (Ortac_runtime.Make)(Spec) let check_init_state () = () -let agree_prop cs = check_init_state (); STMTests.agree_prop cs +let ortac_postcond cmd__004_ state__005_ res__006_ = + let open Spec in + let open STM in + let new_state__007_ = lazy (next_state cmd__004_ state__005_) in + match (cmd__004_, res__006_) with + | (Clear, Res ((Unit, _), _)) -> None + | (Reset, Res ((Unit, _), _)) -> 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 -> + if + (try + Ortac_runtime.Gospelstdlib.List.mem (a_3, b_4) + (Lazy.force new_state__007_).contents + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 32; + pos_bol = 1360; + pos_cnum = 1372 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 32; + pos_bol = 1360; + pos_cnum = 1398 + } + }))) + then None + else + Some + (Ortac_runtime.report "find" + [("List.mem (a, b) h.contents", + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 32; + pos_bol = 1360; + pos_cnum = 1372 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 32; + pos_bol = 1360; + pos_cnum = 1398 + } + })]) + | Error (Not_found) -> + if + (try + not + (Ortac_runtime.Gospelstdlib.List.mem a_3 + (Ortac_runtime.Gospelstdlib.List.map + Ortac_runtime.Gospelstdlib.fst + (Lazy.force new_state__007_).contents)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 31; + pos_bol = 1293; + pos_cnum = 1317 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 31; + pos_bol = 1293; + pos_cnum = 1359 + } + }))) + then None + else + Some + (Ortac_runtime.report "find" + [("not (List.mem a (List.map fst h.contents))", + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 31; + pos_bol = 1293; + pos_cnum = 1317 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 31; + pos_bol = 1293; + pos_cnum = 1359 + } + })]) + | _ -> None) + | (Find_opt a_4, Res ((Option (Int), _), o)) -> + if + (try + (match o with + | None -> + if + not + (Ortac_runtime.Gospelstdlib.List.mem a_4 + (Ortac_runtime.Gospelstdlib.List.map + Ortac_runtime.Gospelstdlib.fst + (Lazy.force new_state__007_).contents)) + then true + else false + | Some b_5 -> + if + Ortac_runtime.Gospelstdlib.List.mem (a_4, b_5) + (Lazy.force new_state__007_).contents + then true + else false) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 36; + pos_bol = 1559; + pos_cnum = 1571 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 38; + pos_bol = 1643; + pos_cnum = 1687 + } + }))) + then None + else + Some + (Ortac_runtime.report "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", + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 36; + pos_bol = 1559; + pos_cnum = 1571 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 38; + pos_bol = 1643; + pos_cnum = 1687 + } + })]) + | (Find_all a_5, Res ((List (Int), _), bs)) -> + if + (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 new_state__007_).contents)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 42; + pos_bol = 1853; + pos_cnum = 1865 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 42; + pos_bol = 1853; + pos_cnum = 1947 + } + }))) + then None + else + Some + (Ortac_runtime.report "find_all" + [("bs = Sequence.filter_map (fun (x, y) -> if x = a then Some y else None) h.contents", + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 42; + pos_bol = 1853; + pos_cnum = 1865 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 42; + pos_bol = 1853; + pos_cnum = 1947 + } + })]) + | (Mem a_6, Res ((Bool, _), b_6)) -> + if + (try + (b_6 = true) = + (Ortac_runtime.Gospelstdlib.List.mem a_6 + (Ortac_runtime.Gospelstdlib.List.map + Ortac_runtime.Gospelstdlib.fst + (Lazy.force new_state__007_).contents)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 46; + pos_bol = 2149; + pos_cnum = 2161 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 46; + pos_bol = 2149; + pos_cnum = 2201 + } + }))) + then None + else + Some + (Ortac_runtime.report "mem" + [("b = List.mem a (List.map fst h.contents)", + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 46; + pos_bol = 2149; + pos_cnum = 2161 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 46; + pos_bol = 2149; + pos_cnum = 2201 + } + })]) + | (Remove a_7, Res ((Unit, _), _)) -> None + | (Replace (a_8, b_3), Res ((Unit, _), _)) -> None + | (Length, Res ((Int, _), i)) -> + if + (try + (Ortac_runtime.Gospelstdlib.integer_of_int i) = + (Ortac_runtime.Gospelstdlib.List.length + (Lazy.force new_state__007_).contents) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 76; + pos_bol = 3727; + pos_cnum = 3739 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 76; + pos_bol = 3727; + pos_cnum = 3765 + } + }))) + then None + else + Some + (Ortac_runtime.report "length" + [("i = List.length h.contents", + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 76; + pos_bol = 3727; + pos_cnum = 3739 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 76; + pos_bol = 3727; + pos_cnum = 3765 + } + })]) + | _ -> None let _ = QCheck_base_runner.run_tests_main (let count = 1000 in - [QCheck.Test.make ~count ~name:"Hashtbl STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + [STMTests.agree_test ~count ~name:"Hashtbl STM tests" check_init_state + ortac_postcond]) diff --git a/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml b/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml index e39fff22..fcf667ad 100644 --- a/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml @@ -1,10 +1,11 @@ (* This file is generated by ortac qcheck-stm, edit how you run the tool instead *) +[@@@ocaml.warning "-26-27"] open Invariants +module Ortac_runtime = Ortac_runtime_qcheck_stm module Spec = struct open STM - [@@@ocaml.warning "-26-27"] type sut = int t type cmd = | Push of int @@ -76,41 +77,11 @@ module Spec = } let precond cmd__008_ state__009_ = match cmd__008_ with | Push a_1 -> true - let postcond cmd__004_ state__005_ res__006_ = - let new_state__007_ = lazy (next_state cmd__004_ state__005_) in - match (cmd__004_, res__006_) with - | (Push a_1, Res ((Unit, _), _)) -> - (try - Ortac_runtime.Gospelstdlib.(>) - (Ortac_runtime.Gospelstdlib.List.length - (Lazy.force new_state__007_).contents) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "invariants.mli"; - pos_lnum = 4; - pos_bol = 110; - pos_cnum = 124 - }; - Ortac_runtime.stop = - { - pos_fname = "invariants.mli"; - pos_lnum = 4; - pos_bol = 110; - pos_cnum = 150 - } - }))) - | _ -> true + let postcond _ _ _ = true let run cmd__010_ sut__011_ = match cmd__010_ with | Push a_1 -> Res (unit, (push a_1 sut__011_)) end -module STMTests = (STM_sequential.Make)(Spec) +module STMTests = (Ortac_runtime.Make)(Spec) let check_init_state () = let __state__012_ = Spec.init_state in if @@ -141,9 +112,63 @@ let check_init_state () = } }))) then QCheck.Test.fail_report "INIT_SUT violates type invariants for SUT" -let agree_prop cs = check_init_state (); STMTests.agree_prop cs +let ortac_postcond cmd__004_ state__005_ res__006_ = + let open Spec in + let open STM in + let new_state__007_ = lazy (next_state cmd__004_ state__005_) in + match (cmd__004_, res__006_) with + | (Push a_1, Res ((Unit, _), _)) -> + if + (try + Ortac_runtime.Gospelstdlib.(>) + (Ortac_runtime.Gospelstdlib.List.length + (Lazy.force new_state__007_).contents) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "invariants.mli"; + pos_lnum = 4; + pos_bol = 110; + pos_cnum = 124 + }; + Ortac_runtime.stop = + { + pos_fname = "invariants.mli"; + pos_lnum = 4; + pos_bol = 110; + pos_cnum = 150 + } + }))) + then None + else + Some + (Ortac_runtime.report "push" + [("List.length x.contents > 0", + { + Ortac_runtime.start = + { + pos_fname = "invariants.mli"; + pos_lnum = 4; + pos_bol = 110; + pos_cnum = 124 + }; + Ortac_runtime.stop = + { + pos_fname = "invariants.mli"; + pos_lnum = 4; + pos_bol = 110; + pos_cnum = 150 + } + })]) + | _ -> None let _ = QCheck_base_runner.run_tests_main (let count = 1000 in - [QCheck.Test.make ~count ~name:"Invariants STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + [STMTests.agree_test ~count ~name:"Invariants STM tests" + check_init_state ortac_postcond]) diff --git a/plugins/qcheck-stm/test/record_stm_tests.expected.ml b/plugins/qcheck-stm/test/record_stm_tests.expected.ml index e173eace..e05824d3 100644 --- a/plugins/qcheck-stm/test/record_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/record_stm_tests.expected.ml @@ -1,6 +1,8 @@ (* This file is generated by ortac qcheck-stm, edit how you run the tool instead *) +[@@@ocaml.warning "-26-27"] open Record +module Ortac_runtime = Ortac_runtime_qcheck_stm let plus1_1 i = try Ortac_runtime.Gospelstdlib.(+) i @@ -29,7 +31,6 @@ let plus1_1 i = module Spec = struct open STM - [@@@ocaml.warning "-26-27"] type sut = t type cmd = | Get @@ -72,97 +73,166 @@ module Spec = let next_state cmd__002_ state__003_ = match cmd__002_ with | Get -> state__003_ let precond cmd__008_ state__009_ = match cmd__008_ with | Get -> true - let postcond cmd__004_ state__005_ res__006_ = + let postcond _ _ _ = true + let run cmd__010_ sut__011_ = + match cmd__010_ with | Get -> Res (int, (get sut__011_)) + end +module STMTests = (Ortac_runtime.Make)(Spec) +let check_init_state () = () +let ortac_postcond cmd__004_ state__005_ res__006_ = + let open Spec in + let open STM in let new_state__007_ = lazy (next_state cmd__004_ state__005_) in match (cmd__004_, res__006_) with | (Get, Res ((Int, _), i_1)) -> - (try - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) = - (Lazy.force new_state__007_).value - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "record.mli"; - pos_lnum = 23; - pos_bol = 868; - pos_cnum = 880 - }; - Ortac_runtime.stop = + Ortac_runtime.append + (if + try + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) = + (Lazy.force new_state__007_).value + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, { - pos_fname = "record.mli"; - pos_lnum = 23; - pos_bol = 868; - pos_cnum = 891 - } - }))) - && - ((try - (plus1_1 (Ortac_runtime.Gospelstdlib.integer_of_int i_1)) = - (Ortac_runtime.Gospelstdlib.(+) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) - (Ortac_runtime.Gospelstdlib.integer_of_int 1)) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = + Ortac_runtime.start = + { + pos_fname = "record.mli"; + pos_lnum = 23; + pos_bol = 868; + pos_cnum = 880 + }; + Ortac_runtime.stop = + { + pos_fname = "record.mli"; + pos_lnum = 23; + pos_bol = 868; + pos_cnum = 891 + } + })) + then None + else + Some + (Ortac_runtime.report "get" + [("i = r.value", + { + Ortac_runtime.start = + { + pos_fname = "record.mli"; + pos_lnum = 23; + pos_bol = 868; + pos_cnum = 880 + }; + Ortac_runtime.stop = + { + pos_fname = "record.mli"; + pos_lnum = 23; + pos_bol = 868; + pos_cnum = 891 + } + })])) + (Ortac_runtime.append + (if + try + (plus1_1 (Ortac_runtime.Gospelstdlib.integer_of_int i_1)) + = + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.integer_of_int 1)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, { - pos_fname = "record.mli"; - pos_lnum = 25; - pos_bol = 912; - pos_cnum = 924 - }; - Ortac_runtime.stop = + Ortac_runtime.start = + { + pos_fname = "record.mli"; + pos_lnum = 25; + pos_bol = 912; + pos_cnum = 924 + }; + Ortac_runtime.stop = + { + pos_fname = "record.mli"; + pos_lnum = 25; + pos_bol = 912; + pos_cnum = 939 + } + })) + then None + else + Some + (Ortac_runtime.report "get" + [("plus1 i = i + 1", + { + Ortac_runtime.start = + { + pos_fname = "record.mli"; + pos_lnum = 25; + pos_bol = 912; + pos_cnum = 924 + }; + Ortac_runtime.stop = + { + pos_fname = "record.mli"; + pos_lnum = 25; + pos_bol = 912; + pos_cnum = 939 + } + })])) + (if + try + (Ortac_runtime.Gospelstdlib.integer_of_int (plus2 i_1)) = + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.integer_of_int 2)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, { - pos_fname = "record.mli"; - pos_lnum = 25; - pos_bol = 912; - pos_cnum = 939 - } - }))) - && - ((try - (Ortac_runtime.Gospelstdlib.integer_of_int (plus2 i_1)) = - (Ortac_runtime.Gospelstdlib.(+) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) - (Ortac_runtime.Gospelstdlib.integer_of_int 2)) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "record.mli"; - pos_lnum = 26; - pos_bol = 940; - pos_cnum = 952 - }; - Ortac_runtime.stop = - { - pos_fname = "record.mli"; - pos_lnum = 26; - pos_bol = 940; - pos_cnum = 967 - } - }))))) - | _ -> true - let run cmd__010_ sut__011_ = - match cmd__010_ with | Get -> Res (int, (get sut__011_)) - end -module STMTests = (STM_sequential.Make)(Spec) -let check_init_state () = () -let agree_prop cs = check_init_state (); STMTests.agree_prop cs + Ortac_runtime.start = + { + pos_fname = "record.mli"; + pos_lnum = 26; + pos_bol = 940; + pos_cnum = 952 + }; + Ortac_runtime.stop = + { + pos_fname = "record.mli"; + pos_lnum = 26; + pos_bol = 940; + pos_cnum = 967 + } + })) + then None + else + Some + (Ortac_runtime.report "get" + [("plus2 i = i + 2", + { + Ortac_runtime.start = + { + pos_fname = "record.mli"; + pos_lnum = 26; + pos_bol = 940; + pos_cnum = 952 + }; + Ortac_runtime.stop = + { + pos_fname = "record.mli"; + pos_lnum = 26; + pos_bol = 940; + pos_cnum = 967 + } + })]))) + | _ -> None let _ = QCheck_base_runner.run_tests_main (let count = 1000 in - [QCheck.Test.make ~count ~name:"Record STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + [STMTests.agree_test ~count ~name:"Record STM tests" check_init_state + ortac_postcond]) diff --git a/plugins/qcheck-stm/test/ref_stm_tests.expected.ml b/plugins/qcheck-stm/test/ref_stm_tests.expected.ml index 0e0ba5b0..393d67ee 100644 --- a/plugins/qcheck-stm/test/ref_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/ref_stm_tests.expected.ml @@ -1,10 +1,11 @@ (* This file is generated by ortac qcheck-stm, edit how you run the tool instead *) +[@@@ocaml.warning "-26-27"] open Ref +module Ortac_runtime = Ortac_runtime_qcheck_stm module Spec = struct open STM - [@@@ocaml.warning "-26-27"] type sut = t type cmd = | Get @@ -47,43 +48,67 @@ module Spec = let next_state cmd__002_ state__003_ = match cmd__002_ with | Get -> state__003_ let precond cmd__008_ state__009_ = match cmd__008_ with | Get -> true - let postcond cmd__004_ state__005_ res__006_ = - let new_state__007_ = lazy (next_state cmd__004_ state__005_) in - match (cmd__004_, res__006_) with - | (Get, Res ((Int, _), i)) -> - (try - (Ortac_runtime.Gospelstdlib.integer_of_int i) = - (Lazy.force new_state__007_).value - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "ref.mli"; - pos_lnum = 11; - pos_bol = 346; - pos_cnum = 358 - }; - Ortac_runtime.stop = - { - pos_fname = "ref.mli"; - pos_lnum = 11; - pos_bol = 346; - pos_cnum = 369 - } - }))) - | _ -> true + let postcond _ _ _ = true let run cmd__010_ sut__011_ = match cmd__010_ with | Get -> Res (int, (get sut__011_)) end -module STMTests = (STM_sequential.Make)(Spec) +module STMTests = (Ortac_runtime.Make)(Spec) let check_init_state () = () -let agree_prop cs = check_init_state (); STMTests.agree_prop cs +let ortac_postcond cmd__004_ state__005_ res__006_ = + let open Spec in + let open STM in + let new_state__007_ = lazy (next_state cmd__004_ state__005_) in + match (cmd__004_, res__006_) with + | (Get, Res ((Int, _), i)) -> + if + (try + (Ortac_runtime.Gospelstdlib.integer_of_int i) = + (Lazy.force new_state__007_).value + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "ref.mli"; + pos_lnum = 11; + pos_bol = 346; + pos_cnum = 358 + }; + Ortac_runtime.stop = + { + pos_fname = "ref.mli"; + pos_lnum = 11; + pos_bol = 346; + pos_cnum = 369 + } + }))) + then None + else + Some + (Ortac_runtime.report "get" + [("i = r.value", + { + Ortac_runtime.start = + { + pos_fname = "ref.mli"; + pos_lnum = 11; + pos_bol = 346; + pos_cnum = 358 + }; + Ortac_runtime.stop = + { + pos_fname = "ref.mli"; + pos_lnum = 11; + pos_bol = 346; + pos_cnum = 369 + } + })]) + | _ -> None let _ = QCheck_base_runner.run_tests_main (let count = 1000 in - [QCheck.Test.make ~count ~name:"Ref STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + [STMTests.agree_test ~count ~name:"Ref STM tests" check_init_state + ortac_postcond]) diff --git a/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml b/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml index 1563ad81..9a679d8b 100644 --- a/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml @@ -1,6 +1,8 @@ (* This file is generated by ortac qcheck-stm, edit how you run the tool instead *) +[@@@ocaml.warning "-26-27"] open Sequence_model +module Ortac_runtime = Ortac_runtime_qcheck_stm let length_opt s = try Some (Ortac_runtime.Gospelstdlib.Sequence.length s) with @@ -27,7 +29,6 @@ let length_opt s = module Spec = struct open STM - [@@@ocaml.warning "-26-27"] type sut = char t type cmd = | Add of char @@ -177,24 +178,26 @@ module Spec = } let precond cmd__010_ state__011_ = match cmd__010_ with | Add v -> true | Remove -> true | Remove_ -> true - let postcond cmd__006_ state__007_ res__008_ = - let new_state__009_ = lazy (next_state cmd__006_ state__007_) in - match (cmd__006_, res__008_) with - | (Add v, Res ((Unit, _), _)) -> true - | (Remove, Res ((Option (Char), _), o)) -> true - | (Remove_, Res ((Option (Char), _), o_1)) -> true - | _ -> true + let postcond _ _ _ = true let run cmd__012_ sut__013_ = match cmd__012_ with | Add v -> Res (unit, (add v sut__013_)) | Remove -> Res ((option char), (remove sut__013_)) | Remove_ -> Res ((option char), (remove_ sut__013_)) end -module STMTests = (STM_sequential.Make)(Spec) +module STMTests = (Ortac_runtime.Make)(Spec) let check_init_state () = () -let agree_prop cs = check_init_state (); STMTests.agree_prop cs +let ortac_postcond cmd__006_ state__007_ res__008_ = + let open Spec in + let open STM in + let new_state__009_ = lazy (next_state cmd__006_ state__007_) in + match (cmd__006_, res__008_) with + | (Add v, Res ((Unit, _), _)) -> None + | (Remove, Res ((Option (Char), _), o)) -> None + | (Remove_, Res ((Option (Char), _), o_1)) -> None + | _ -> None let _ = QCheck_base_runner.run_tests_main (let count = 1000 in - [QCheck.Test.make ~count ~name:"Sequence_model STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + [STMTests.agree_test ~count ~name:"Sequence_model STM tests" + check_init_state ortac_postcond]) diff --git a/plugins/wrapper/src/ir_of_gospel.ml b/plugins/wrapper/src/ir_of_gospel.ml index 2eae4bec..61f3a168 100644 --- a/plugins/wrapper/src/ir_of_gospel.ml +++ b/plugins/wrapper/src/ir_of_gospel.ml @@ -7,6 +7,7 @@ open Ir open Ppxlib open Ortac_core.Builder module Ident = Identifier.Ident +open Ortac_core.Utils let term ~context fail t = try @@ -313,13 +314,6 @@ end let register_name = gen_symbol ~prefix:"__error" -let term_printer text global_loc (t : Tterm.term) = - try - String.sub text - (t.t_loc.loc_start.pos_cnum - global_loc.loc_start.pos_cnum) - (t.t_loc.loc_end.pos_cnum - t.t_loc.loc_start.pos_cnum) - with Invalid_argument _ -> Fmt.str "%a" Tterm_printer.print_term t - let type_of_ty ~ir (ty : Ttypes.ty) = match ty.ty_node with | Tyvar a -> diff --git a/src/core/builder.ml b/src/core/builder.ml index 37a7dfee..2fc9f208 100644 --- a/src/core/builder.ml +++ b/src/core/builder.ml @@ -65,14 +65,12 @@ let list_fold_right1 op v xs = in match xs with [] -> v | _ -> aux xs -let list_and xs = - let ( &&& ) e1 e2 = - pexp_apply (pexp_ident (lident "&&")) [ (Nolabel, e1); (Nolabel, e2) ] - and etrue = pexp_construct (lident "true") None in - list_fold_right1 ( &&& ) etrue xs +let list_fold_expr op base = + let ( ** ) e1 e2 = pexp_apply op [ (Nolabel, e1); (Nolabel, e2) ] + and ebase = pexp_construct (lident base) None in + list_fold_right1 ( ** ) ebase -let list_or xs = - let ( ||| ) e1 e2 = - pexp_apply (pexp_ident (lident "||")) [ (Nolabel, e1); (Nolabel, e2) ] - and efalse = pexp_construct (lident "false") None in - list_fold_right1 ( ||| ) efalse xs +let list_and = list_fold_expr (pexp_ident (lident "&&")) "true" +let list_or = list_fold_expr (pexp_ident (lident "||")) "false" +let enone = pexp_construct (lident "None") None +let esome e = pexp_construct (lident "Some") (Some e) diff --git a/src/core/builder.mli b/src/core/builder.mli index 9c4435d0..913fc2f1 100644 --- a/src/core/builder.mli +++ b/src/core/builder.mli @@ -10,5 +10,8 @@ val enot : expression -> expression val elocation : location -> expression val efun : (arg_label * pattern) list -> expression -> expression val lident : label -> longident loc +val list_fold_expr : expression -> string -> expression list -> expression val list_and : expression list -> expression val list_or : expression list -> expression +val enone : expression +val esome : expression -> expression diff --git a/src/core/utils.ml b/src/core/utils.ml index fbb171ee..d3d99cdf 100644 --- a/src/core/utils.ml +++ b/src/core/utils.ml @@ -1,14 +1,22 @@ +open Gospel + +let term_printer text global_loc (t : Tterm.term) = + let open Ppxlib.Location in + try + String.sub text + (t.t_loc.loc_start.pos_cnum - global_loc.loc_start.pos_cnum) + (t.t_loc.loc_end.pos_cnum - t.t_loc.loc_start.pos_cnum) + with Invalid_argument _ -> Fmt.str "%a" Tterm_printer.print_term t + let module_name_of_path p = let filename = Filename.basename p in String.index filename '.' |> String.sub filename 0 |> String.capitalize_ascii let type_check load_path name sigs = - let md = Gospel.Tmodule.init_muc name in + let md = Tmodule.init_muc name in let penv = - module_name_of_path name - |> Gospel.Utils.Sstr.singleton - |> Gospel.Typing.penv load_path + module_name_of_path name |> Utils.Sstr.singleton |> Typing.penv load_path in - let gfile = List.fold_left (Gospel.Typing.type_sig_item penv) md sigs in - let sigs = Gospel.Tmodule.wrap_up_muc gfile |> fun file -> file.fl_sigs in + let gfile = List.fold_left (Typing.type_sig_item penv) md sigs in + let sigs = Tmodule.wrap_up_muc gfile |> fun file -> file.fl_sigs in (gfile.muc_import, sigs) diff --git a/src/core/utils.mli b/src/core/utils.mli index 4139d4f7..bd62989c 100644 --- a/src/core/utils.mli +++ b/src/core/utils.mli @@ -1,3 +1,9 @@ +val term_printer : string -> Ppxlib.Location.t -> Gospel.Tterm.term -> string +(** [term_printer text global_loc term] fetch the initial text representation of + [term] provided that [text] is the specification's text and [global_loc] the + specification's location. Fall back on the Gospel term pretty printer if + something goes wrong when extracting the substring. *) + val module_name_of_path : string -> string (** [module_name_of_path p] turn the path to an OCaml file [p] into the corresponding OCaml module identifier *) diff --git a/src/runtime/ortac_runtime_intf.ml b/src/runtime/ortac_runtime_intf.ml index 04c4e351..64dfa74c 100644 --- a/src/runtime/ortac_runtime_intf.ml +++ b/src/runtime/ortac_runtime_intf.ml @@ -22,6 +22,7 @@ module type S = sig mutable errors : error list; } + val pp_loc : Format.formatter -> location -> unit val pp_error_report : Format.formatter -> error_report -> unit exception Error of error_report