From 0246a95d4a43426014f95497ffb50acb46346d47 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Mon, 6 Nov 2023 17:40:18 +0100 Subject: [PATCH] Add a guard testing equality for integer constant pattern Fixes #172 --- plugins/qcheck-stm/test/sequence_model.ml | 3 + plugins/qcheck-stm/test/sequence_model.mli | 7 +++ .../test/sequence_model_stm_tests.expected.ml | 57 ++++++++++++++++--- src/core/ocaml_of_gospel.ml | 29 +++++++++- 4 files changed, 86 insertions(+), 10 deletions(-) diff --git a/plugins/qcheck-stm/test/sequence_model.ml b/plugins/qcheck-stm/test/sequence_model.ml index 847555d7..c8d466c3 100644 --- a/plugins/qcheck-stm/test/sequence_model.ml +++ b/plugins/qcheck-stm/test/sequence_model.ml @@ -2,3 +2,6 @@ type 'a t = 'a list ref let create () = ref [] let add x s = s := x :: !s +let remove s = match !s with + | [] -> None + | x :: xs -> s := xs; Some x diff --git a/plugins/qcheck-stm/test/sequence_model.mli b/plugins/qcheck-stm/test/sequence_model.mli index 939ae4be..b1dc1b2d 100644 --- a/plugins/qcheck-stm/test/sequence_model.mli +++ b/plugins/qcheck-stm/test/sequence_model.mli @@ -9,3 +9,10 @@ val add : 'a -> 'a t -> unit (*@ add v t modifies t.contents ensures t.contents = Sequence.cons v (old t.contents) *) + +val remove : 'a t -> 'a option +(*@ o = remove t + modifies t.contents + ensures t.contents = match Sequence.length (old t.contents) with + | 0 -> Sequence.empty + | _ -> Sequence.tl (old t.contents) *) 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 a51d50f9..d107dfad 100644 --- a/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml @@ -6,9 +6,11 @@ module Spec = type sut = char t type cmd = | Add of char + | Remove let show_cmd cmd__001_ = match cmd__001_ with | Add v -> Format.asprintf "%s %a" "add" (Util.Pp.pp_char true) v + | Remove -> Format.asprintf "%s" "remove" type nonrec state = { contents: char Ortac_runtime.Gospelstdlib.sequence } let init_state = @@ -43,7 +45,8 @@ module Spec = let arb_cmd _ = let open QCheck in make ~print:show_cmd - (let open Gen in oneof [(pure (fun v -> Add v)) <*> char]) + (let open Gen in + oneof [(pure (fun v -> Add v)) <*> char; pure Remove]) let next_state cmd__002_ state__003_ = match cmd__002_ with | Add v -> @@ -74,14 +77,54 @@ module Spec = } })))) } - let precond cmd__008_ state__009_ = match cmd__008_ with | Add v -> 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 + | Remove -> + { + contents = + ((try + match Ortac_runtime.Gospelstdlib.Sequence.length + state__003_.contents + with + | __x__004_ when + (=) __x__004_ + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + -> Ortac_runtime.Gospelstdlib.Sequence.empty + | _ -> + Ortac_runtime.Gospelstdlib.Sequence.tl + state__003_.contents + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "sequence_model.mli"; + pos_lnum = 16; + pos_bol = 732; + pos_cnum = 757 + }; + Ortac_runtime.stop = + { + pos_fname = "sequence_model.mli"; + pos_lnum = 18; + pos_bol = 849; + pos_cnum = 910 + } + })))) + } + let precond cmd__009_ state__010_ = + match cmd__009_ with | Add v -> true | Remove -> 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 | (Add v, Res ((Unit, _), _)) -> true + | (Remove, Res ((Option (Char), _), o)) -> true | _ -> true - let run cmd__010_ sut__011_ = - match cmd__010_ with | Add v -> Res (unit, (add v sut__011_)) + let run cmd__011_ sut__012_ = + match cmd__011_ with + | Add v -> Res (unit, (add v sut__012_)) + | Remove -> Res ((option char), (remove sut__012_)) end module STMTests = (STM_sequential.Make)(Spec) let _ = diff --git a/src/core/ocaml_of_gospel.ml b/src/core/ocaml_of_gospel.ml index 31d9c693..a804a0e5 100644 --- a/src/core/ocaml_of_gospel.ml +++ b/src/core/ocaml_of_gospel.ml @@ -58,6 +58,29 @@ let rec bounds ~context ~loc (var : Symbols.vsymbol) (t1 : Tterm.term) | Inf start, Sup stop | Sup stop, Inf start -> (start, stop) | _ -> unsupported () +and case ~context (p, g, t) = + let guard = Option.map (term ~context) g in + let open Tterm in + let lhs, guard = + match p.p_node with + | Pconst (Pconst_integer (_, _) as c) -> + let i = econst c in + let var = gen_symbol ~prefix:"__x" () in + let extra = + pexp_apply + (pexp_ident (lident "(=)")) + [ (Nolabel, evar var); (Nolabel, i) ] + in + let guard = Option.fold ~none:extra ~some:(fun guard -> + pexp_apply + (pexp_ident (lident "(&&)")) + [ (Nolabel, extra); (Nolabel, guard) ]) guard + in + (ppat_var (noloc var), Some guard) + | _ -> (pattern p, guard) + in + Builder.case ~lhs ~guard ~rhs:(term ~context t) + and term ~context (t : Tterm.term) : expression = let term = term ~context in let loc = t.t_loc in @@ -97,9 +120,9 @@ and term ~context (t : Tterm.term) : expression = let [%p pvar x] = [%e term t1] in [%e term t2]] | Tcase (t, ptl) -> - List.map - (fun (p, g, t) -> - case ~guard:(Option.map term g) ~lhs:(pattern p) ~rhs:(term t)) + List.map (case ~context) + (* (fun (p, g, t) -> *) + (* case ~guard:(Option.map term g) ~lhs:(pattern p) ~rhs:(term t)) *) ptl |> pexp_match (term t) | Tlambda (ps, t) ->