Add support for functional models

CHANGES.md

@@ -1,5 +1,7 @@
 # 0.3.0
 
+- Add support for functional type in model
+  [\#230](https://github.com/ocaml-gospel/ortac/pull/230)
 - Remove bug in qcheck-stm plugin when returning integers
 - [\#240](https://github.com/ocaml-gospel/ortac/pull/240)
 - Add support for testing functions with tuple arguments/return values

plugins/qcheck-stm/test/dune.inc

@@ -634,3 +634,56 @@
  (action
   (run %{dep:tuples_stm_tests.exe} -v)))
 
+(library
+ (name functional_model)
+ (modules functional_model))
+
+(rule
+ (target functional_model_stm_tests.ml)
+ (package ortac-qcheck-stm)
+ (deps
+  (package ortac-core)
+  (package ortac-qcheck-stm))
+ (action
+  (setenv
+   ORTAC_ONLY_PLUGIN
+   qcheck-stm
+   (with-stderr-to
+    functional_model_errors
+    (run
+     ortac
+     qcheck-stm
+     %{dep:functional_model.mli}
+     %{dep:functional_model_config.ml}
+     -o
+     %{target})))))
+
+(test
+ (name functional_model_stm_tests)
+ (package ortac-qcheck-stm)
+ (modules functional_model_stm_tests)
+ (libraries
+  qcheck-core
+  qcheck-core.runner
+  qcheck-stm.stm
+  qcheck-stm.sequential
+  qcheck-multicoretests-util
+  ortac-runtime-qcheck-stm
+  functional_model)
+ (action
+  (echo
+   "\n%{dep:functional_model_stm_tests.exe} has been generated with the ortac-qcheck-stm plugin.\n")))
+
+(rule
+ (alias runtest)
+ (package ortac-qcheck-stm)
+ (action
+  (progn
+   (diff functional_model_errors.expected functional_model_errors)
+   (diff functional_model_stm_tests.expected.ml functional_model_stm_tests.ml))))
+
+(rule
+ (alias launchtests)
+ (action
+  (run %{dep:functional_model_stm_tests.exe} -v)))
+

plugins/qcheck-stm/test/dune_gen.args

@@ -21,4 +21,6 @@ custom_config_config
 test_without_sut
 test_without_sut_config
 tuples
-tuples_config
+tuples_config
+functional_model
+functional_model_config

plugins/qcheck-stm/test/functional_model.ml

@@ -0,0 +1,4 @@
+type ('a, 'b) t = ('a, 'b) Hashtbl.t
+
+let empty () = Hashtbl.create 42
+let add = Hashtbl.add

plugins/qcheck-stm/test/functional_model.mli

@@ -0,0 +1,11 @@
+type ('a, 'b) t
+(*@ mutable model m : 'a -> 'b option *)
+
+val empty : unit -> ('a, 'b) t
+(*@ t = empty ()
+    ensures t.m = fun _ -> None *)
+
+val add : ('a, 'b) t -> 'a -> 'b -> unit
+(*@ add t a b
+    modifies t.m
+    ensures t.m = fun x -> if x = a then Some b else (old t.m) x *)

plugins/qcheck-stm/test/functional_model_config.ml

@@ -0,0 +1,3 @@
+type sut = (char, int) t
+
+let init_sut = empty ()

plugins/qcheck-stm/test/functional_model_stm_tests.expected.ml

@@ -0,0 +1,106 @@
+(* This file is generated by ortac qcheck-stm,
+   edit how you run the tool instead *)
+[@@@ocaml.warning "-26-27-69-32"]
+open Functional_model
+module Ortac_runtime = Ortac_runtime_qcheck_stm
+module Spec =
+  struct
+    open STM
+    type _ ty +=  
+      | Integer: Ortac_runtime.integer ty 
+    let integer = (Integer, Ortac_runtime.string_of_integer)
+    type sut = (char, int) t
+    type cmd =
+      | Add of char * int 
+    let show_cmd cmd__001_ =
+      match cmd__001_ with
+      | Add (a_1, b_1) ->
+          Format.asprintf "%s sut %a %a" "add" (Util.Pp.pp_char true) a_1
+            (Util.Pp.pp_int true) b_1
+    type nonrec state = {
+      m: char -> int option }
+    let init_state =
+      let () = () in
+      {
+        m =
+          (try fun _ -> None
+           with
+           | e ->
+               raise
+                 (Ortac_runtime.Partial_function
+                    (e,
+                      {
+                        Ortac_runtime.start =
+                          {
+                            pos_fname = "functional_model.mli";
+                            pos_lnum = 6;
+                            pos_bol = 275;
+                            pos_cnum = 293
+                          };
+                        Ortac_runtime.stop =
+                          {
+                            pos_fname = "functional_model.mli";
+                            pos_lnum = 6;
+                            pos_bol = 275;
+                            pos_cnum = 306
+                          }
+                      })))
+      }
+    let init_sut () = empty ()
+    let cleanup _ = ()
+    let arb_cmd _ =
+      let open QCheck in
+        make ~print:show_cmd
+          (let open Gen in
+             oneof
+               [((pure (fun a_1 -> fun b_1 -> Add (a_1, b_1))) <*> char) <*>
+                  int])
+    let next_state cmd__002_ state__003_ =
+      match cmd__002_ with
+      | Add (a_1, b_1) ->
+          {
+            m =
+              ((try fun x -> if x = a_1 then Some b_1 else state__003_.m x
+                with
+                | e ->
+                    raise
+                      (Ortac_runtime.Partial_function
+                         (e,
+                           {
+                             Ortac_runtime.start =
+                               {
+                                 pos_fname = "functional_model.mli";
+                                 pos_lnum = 11;
+                                 pos_bol = 482;
+                                 pos_cnum = 500
+                               };
+                             Ortac_runtime.stop =
+                               {
+                                 pos_fname = "functional_model.mli";
+                                 pos_lnum = 11;
+                                 pos_bol = 482;
+                                 pos_cnum = 546
+                               }
+                           }))))
+          }
+    let precond cmd__008_ state__009_ =
+      match cmd__008_ with | Add (a_1, b_1) -> true
+    let postcond _ _ _ = true
+    let run cmd__010_ sut__011_ =
+      match cmd__010_ with
+      | Add (a_1, b_1) -> Res (unit, (add sut__011_ a_1 b_1))
+  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
+      | (Add (a_1, b_1), Res ((Unit, _), _)) -> None
+      | _ -> None
+let _ =
+  QCheck_base_runner.run_tests_main
+    (let count = 1000 in
+     [STMTests.agree_test ~count ~name:"Functional_model STM tests"
+        check_init_state ortac_postcond])

src/core/ocaml_of_gospel.ml

@@ -222,12 +222,18 @@ let core_type_of_ty_aux ~context f =
     | None -> str_of_ident ts.ts_ident)
     |> Builder.lident
   in
+  let rec arrow = function
+    | [ a; b ] -> Builder.ptyp_arrow Nolabel a b
+    | a :: bs -> Builder.ptyp_arrow Nolabel a (arrow bs)
+    | _ -> invalid_arg "arrow"
+  in
   let rec aux ty =
     match ty.ty_node with
     | Tyvar v -> f (str_of_ident v.tv_name)
     | Tyapp (ts, args) ->
         let args = List.map aux args in
-        if is_ts_tuple ts then Builder.ptyp_tuple args
+        if is_ts_arrow ts then arrow args
+        else if is_ts_tuple ts then Builder.ptyp_tuple args
         else Builder.ptyp_constr (lident_of_tysymbol ts) args
   in
   aux