Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use more idiomatic specifications #148

Merged
merged 1 commit into from
Sep 28, 2023
Merged

Use more idiomatic specifications #148

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion plugins/qcheck-stm/test/all_warnings.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ type s

val make : int -> 'a -> 'a t
(*@ t = make i a
ensures t.contents = List.init i (fun x -> a) *)
ensures t.contents = List.init i (fun _ -> a) *)

val constant : unit
(*@ constant
Expand Down
14 changes: 7 additions & 7 deletions plugins/qcheck-stm/test/hashtbl.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,22 +28,22 @@ val add : ('a, 'b) t -> 'a -> 'b -> unit
val find : ('a, 'b) t -> 'a -> 'b
(*@ b = find h a
raises Not_found -> forall x. not (List.mem (a, x) h.contents)
raises Not_found -> not (List.mem a (List.map (fun x -> fst x) h.contents))
raises Not_found -> not (List.mem a (List.map fst h.contents))
ensures List.mem (a, b) h.contents *)

val find_opt : ('a, 'b) t -> 'a -> 'b option
(*@ o = find_opt h a
ensures match o with
| None -> not (List.mem a (List.map (fun x -> fst x) h.contents))
| None -> not (List.mem a (List.map fst h.contents))
| Some b -> List.mem (a, b) h.contents *)

val find_all : ('a, 'b) t -> 'a -> 'b list
(*@ bs = find_all h a
ensures bs = Sequence.filter_map (fun x -> if fst x = a then Some (snd x) else None) h.contents *)
ensures bs = Sequence.filter_map (fun (x, y) -> if x = a then Some y else None) h.contents *)

val mem : ('a, 'b) t -> 'a -> bool
(*@ b = mem h a
ensures b = List.mem a (List.map (fun x -> fst x) h.contents) *)
ensures b = List.mem a (List.map fst h.contents) *)

(*@ function rec remove_first (x: 'a) (xs : ('a * 'b) list) : ('a * 'b) list =
match xs with
Expand All @@ -65,9 +65,9 @@ val filter_map_inplace : ('a -> 'b -> 'b option) -> ('a, 'b) t -> unit
(*@ filter_map_inplace f h
modifies h
ensures h.contents = Sequence.filter_map
(fun x -> match f (fst x) (snd x) with
| None -> None
| Some b' -> Some (fst x, b'))
(fun (x,y) -> match f x y with
| None -> None
| Some b' -> Some (x, b'))
(old h.contents) *)

val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c
Expand Down
11 changes: 4 additions & 7 deletions plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ module Spec =
not
(Ortac_runtime.Gospelstdlib.List.mem a_3
(Ortac_runtime.Gospelstdlib.List.map
(fun x_1 -> Ortac_runtime.Gospelstdlib.fst x_1)
Ortac_runtime.Gospelstdlib.fst
(Lazy.force new_state__007_).contents))
| _ -> false)
| (Find_opt a_4, Res ((Option (Int), _), o)) ->
Expand All @@ -115,7 +115,7 @@ module Spec =
not
(Ortac_runtime.Gospelstdlib.List.mem a_4
(Ortac_runtime.Gospelstdlib.List.map
(fun x_2 -> Ortac_runtime.Gospelstdlib.fst x_2)
Ortac_runtime.Gospelstdlib.fst
(Lazy.force new_state__007_).contents))
then true
else false
Expand All @@ -129,17 +129,14 @@ module Spec =
| (Find_all a_5, Res ((List (Int), _), bs)) ->
(Ortac_runtime.Gospelstdlib.List.to_seq bs) =
(Ortac_runtime.Gospelstdlib.Sequence.filter_map
(fun x_3 ->
if (Ortac_runtime.Gospelstdlib.fst x_3) = a_5
then Some (Ortac_runtime.Gospelstdlib.snd x_3)
else None)
(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))
| (Mem a_6, Res ((Bool, _), b_6)) ->
(b_6 = true) =
(Ortac_runtime.Gospelstdlib.List.mem a_6
(Ortac_runtime.Gospelstdlib.List.map
(fun x_4 -> Ortac_runtime.Gospelstdlib.fst x_4)
Ortac_runtime.Gospelstdlib.fst
(Lazy.force new_state__007_).contents))
| (Remove a_7, Res ((Unit, _), _)) -> true
| (Replace (a_8, b_3), Res ((Unit, _), _)) -> true
Expand Down