Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@n-osborne
n-osborne committed Feb 21, 2024
1 parent 7ea2365 commit 8164e85
Show file tree
Hide file tree
Showing 15 changed files with 186 additions and 97 deletions.
16 changes: 8 additions & 8 deletions examples/lwt_dllist_tests.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -335,7 +335,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("is_empty",
(None, "is_empty",
[("b <-> s.contents = Sequence.empty",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -383,7 +383,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("length",
(None, "length",
[("l = Sequence.length s.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -440,7 +440,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("take_l",
(None, "take_l",
[("if old s.contents = Sequence.empty\n then false\n else a = Sequence.hd (old s.contents)",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -492,7 +492,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("take_l",
(None, "take_l",
[("old s.contents = Sequence.empty = s.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -552,7 +552,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("take_r",
(None, "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 =
Expand Down Expand Up @@ -604,7 +604,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("take_r",
(None, "take_r",
[("old s.contents = Sequence.empty = s.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -656,7 +656,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("take_opt_l",
(None, "take_opt_l",
[("old s.contents = match o with\n | None -> Sequence.empty\n | Some a -> Sequence.cons a s.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -707,7 +707,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
then None
else
Some
("take_opt_r",
(None, "take_opt_r",
[("old s.contents = match o with\n | None -> Sequence.empty\n | Some a -> Sequence.snoc s.contents a",
{
Ortac_runtime.start =
Expand Down
42 changes: 21 additions & 21 deletions examples/varray_circular_tests.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -759,7 +759,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("pop_back",
(None, "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 =
Expand Down Expand Up @@ -811,7 +811,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("pop_back",
(None, "pop_back",
[("t.contents = old t.contents = Sequence.empty",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -868,7 +868,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("pop_front",
(None, "pop_front",
[("if old t.contents = Sequence.empty\n then false\n else proj x = Sequence.hd (old t.contents)",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -920,7 +920,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("pop_front",
(None, "pop_front",
[("t.contents = old t.contents = Sequence.empty",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -976,7 +976,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("insert_at",
((Some (Res (unit, ()))), "insert_at",
[("0 <= i <= Sequence.length t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1038,7 +1038,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("insert_at",
((Some (Res (unit, ()))), "insert_at",
[("0 <= i <= Sequence.length t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1086,7 +1086,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("pop_at",
(None, "pop_at",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1140,7 +1140,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("pop_at",
(None, "pop_at",
[("(proj x) = old t.contents[i]",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1195,7 +1195,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("pop_at",
(None, "pop_at",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1243,7 +1243,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("delete_at",
((Some (Res (unit, ()))), "delete_at",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1300,7 +1300,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("delete_at",
((Some (Res (unit, ()))), "delete_at",
[("Sequence.length t.contents = Sequence.length (old t.contents) - 1",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1355,7 +1355,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("delete_at",
((Some (Res (unit, ()))), "delete_at",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1403,7 +1403,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("get",
(None, "get",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1457,7 +1457,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("get",
(None, "get",
[("(proj x) = t.contents[i]",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1512,7 +1512,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("get",
(None, "get",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1560,7 +1560,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("set",
((Some (Res (unit, ()))), "set",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1616,7 +1616,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("set",
((Some (Res (unit, ()))), "set",
[("inside i t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1664,7 +1664,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("length",
(None, "length",
[("l = Sequence.length t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1712,7 +1712,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("is_empty",
(None, "is_empty",
[("b <-> t.contents = Sequence.empty",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1775,7 +1775,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("fill",
((Some (Res (unit, ()))), "fill",
[("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents",
{
Ortac_runtime.start =
Expand Down Expand Up @@ -1847,7 +1847,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
then None
else
Some
("fill",
((Some (Res (unit, ()))), "fill",
[("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents",
{
Ortac_runtime.start =
Expand Down
Loading

0 comments on commit 8164e85

Please sign in to comment.