Add a guard testing equality for integer constant pattern

Fixes ocaml-gospel#172

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

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) *)

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 _ =

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) ->