Merge pull request ocaml-gospel#158 from shym/tystdlib

Translate types of the Gospelstdlib

plugins/qcheck-stm/src/ir_of_gospel.ml

@@ -245,7 +245,7 @@ let state config sigs =
   let open Ortac_core in
   let* subst =
     Fun.flip List.assoc_opt
-    <$> (Ocaml_of_gospel.core_type_of_tysymbol ty.td_ts
+    <$> (Ocaml_of_gospel.core_type_of_tysymbol ~context:config.context ty.td_ts
         |> unify (`Type ty) config.sut_core_type)
   in
   let* spec =
@@ -256,8 +256,9 @@ let state config sigs =
   let process_model (ls, _) =
     let open Symbols in
     ( ls.ls_name,
-      Option.get ls.ls_value |> Ocaml_of_gospel.core_type_of_ty_with_subst subst
-    )
+      Option.get ls.ls_value
+      |> Ocaml_of_gospel.core_type_of_ty_with_subst ~context:config.context
+           subst )
   in
   match spec.ty_fields with
   | [] -> error (No_models sut_name, spec.ty_loc)

plugins/qcheck-stm/test/dune

@@ -257,3 +257,57 @@
    (diff
     conjunctive_clauses_stm_tests.expected.ml
     conjunctive_clauses_stm_tests.ml))))
+
+(rule
+ (target sequence_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
+    sequence_model_errors
+    (run
+     ortac
+     qcheck-stm
+     %{dep:sequence_model.mli}
+     "create ()"
+     "char t"
+     -o
+     %{target})))))
+
+(rule
+ (alias runtest)
+ (package ortac-qcheck-stm)
+ (action
+  (progn
+   (diff sequence_model_errors.expected sequence_model_errors)
+   (diff sequence_model_stm_tests.expected.ml sequence_model_stm_tests.ml))))
+
+(library
+ (name sequence_model)
+ (modules sequence_model))
+
+(test
+ (name sequence_model_stm_tests)
+ (package ortac-qcheck-stm)
+ (modules sequence_model_stm_tests)
+ (libraries
+  qcheck-core
+  qcheck-core.runner
+  qcheck-stm.stm
+  qcheck-stm.sequential
+  qcheck-multicoretests-util
+  ortac-runtime
+  sequence_model)
+ (action
+  (echo
+   "\n%{dep:sequence_model_stm_tests.exe} has been generated with the ortac-qcheck-stm plugin.\n")))
+
+(rule
+ (alias launchtests)
+ (action
+  (run %{dep:sequence_model_stm_tests.exe} -v)))

plugins/qcheck-stm/test/sequence_model.ml

@@ -0,0 +1,4 @@
+type 'a t = 'a list ref
+
+let create () = ref []
+let add x s = s := x :: !s

plugins/qcheck-stm/test/sequence_model.mli

@@ -0,0 +1,11 @@
+type 'a t
+(*@ mutable model contents : 'a sequence *)
+
+val create : unit -> 'a t
+(*@ t = create ()
+    ensures t.contents = Sequence.empty *)
+
+val add : 'a -> 'a t -> unit
+(*@ add v t
+    modifies t.contents
+    ensures t.contents = Sequence.cons v (old t.contents) *)

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

@@ -0,0 +1,90 @@
+open Sequence_model
+module Spec =
+  struct
+    open STM
+    [@@@ocaml.warning "-26-27"]
+    type sut = char t
+    type cmd =
+      | Add of char 
+    let show_cmd cmd__001_ =
+      match cmd__001_ with
+      | Add v -> Format.asprintf "%s %a" "add" (Util.Pp.pp_char true) v
+    type nonrec state = {
+      contents: char Ortac_runtime.Gospelstdlib.sequence }
+    let init_state =
+      let () = () in
+      {
+        contents =
+          (try Ortac_runtime.Gospelstdlib.Sequence.empty
+           with
+           | e ->
+               raise
+                 (Ortac_runtime.Partial_function
+                    (e,
+                      {
+                        Ortac_runtime.start =
+                          {
+                            pos_fname = "sequence_model.mli";
+                            pos_lnum = 6;
+                            pos_bol = 263;
+                            pos_cnum = 288
+                          };
+                        Ortac_runtime.stop =
+                          {
+                            pos_fname = "sequence_model.mli";
+                            pos_lnum = 6;
+                            pos_bol = 263;
+                            pos_cnum = 302
+                          }
+                      })))
+      }
+    let init_sut () = create ()
+    let cleanup _ = ()
+    let arb_cmd _ =
+      let open QCheck in
+        make ~print:show_cmd
+          (let open Gen in oneof [(pure (fun v -> Add v)) <*> char])
+    let next_state cmd__002_ state__003_ =
+      match cmd__002_ with
+      | Add v ->
+          {
+            contents =
+              ((try
+                  Ortac_runtime.Gospelstdlib.Sequence.cons v
+                    state__003_.contents
+                with
+                | e ->
+                    raise
+                      (Ortac_runtime.Partial_function
+                         (e,
+                           {
+                             Ortac_runtime.start =
+                               {
+                                 pos_fname = "sequence_model.mli";
+                                 pos_lnum = 11;
+                                 pos_bol = 475;
+                                 pos_cnum = 500
+                               };
+                             Ortac_runtime.stop =
+                               {
+                                 pos_fname = "sequence_model.mli";
+                                 pos_lnum = 11;
+                                 pos_bol = 475;
+                                 pos_cnum = 532
+                               }
+                           }))))
+          }
+    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
+      | (Add v, Res ((Unit, _), _)) -> true
+      | _ -> true
+    let run cmd__010_ sut__011_ =
+      match cmd__010_ with | Add v -> Res (unit, (add v sut__011_))
+  end
+module STMTests = (STM_sequential.Make)(Spec)
+let _ =
+  QCheck_base_runner.run_tests_main
+    (let count = 1000 in
+     [STMTests.agree_test ~count ~name:"STM Lib test sequential"])

src/core/context.ml

@@ -1,9 +1,11 @@
 open Gospel.Tmodule
 module L = Map.Make (Gospel.Symbols.LS)
+module T = Map.Make (Gospel.Ttypes.Ts)
 
 type t = {
   module_name : string;
   stdlib : string L.t;
+  tystdlib : string T.t;
   env : namespace;
   functions : string L.t;
 }
@@ -18,6 +20,7 @@ let get_env get ns path =
 
 let get_ls_env = get_env ns_find_ls
 let translate_stdlib ls t = L.find_opt ls t.stdlib
+let translate_tystdlib ts t = T.find_opt ts t.tystdlib
 let add_function ls i t = { t with functions = L.add ls i t.functions }
 let find_function ls t = L.find ls t.functions
 let is_function ls t = L.mem ls t.functions
@@ -33,6 +36,19 @@ let builtins =
     ([ "infix =" ], "(=)");
   ]
 
+let tybuiltins =
+  [
+    ([ "unit" ], "unit");
+    ([ "string" ], "string");
+    ([ "char" ], "char");
+    ([ "float" ], "float");
+    ([ "bool" ], "bool");
+    ([ "int" ], "int");
+    ([ "option" ], "option");
+    ([ "list" ], "list");
+    ([ "integer" ], "Ortac_runtime.integer");
+  ]
+
 (** [unsupported_stdlib] contains all the entries of the Gospel Stdlib that
     cannot be translated *)
 let unsupported_stdlib =
@@ -86,24 +102,24 @@ let process_name name =
     Some ("__mix_" ^ String.map convert_mix_symbol (drop p_mix))
   else Some name
 
-let fold_namespace f path ns v =
+let fold_namespace proj f path ns v =
   let rec aux path ns v =
-    let v = Gospel.Tmodule.Mstr.fold (f path) ns.ns_ls v in
+    let v = Gospel.Tmodule.Mstr.fold (f path) (proj ns) v in
     Gospel.Tmodule.Mstr.fold (fun s -> aux (path @ [ s ])) ns.ns_ns v
   in
   aux path ns v
 
 let init module_name env =
   let gostd = Gospel.Tmodule.Mstr.find "Gospelstdlib" env.ns_ns in
-  let process_gostd_entry path name ls lib =
+  let process_gostd_entry add path name sym lib =
     match process_name name with
     | None -> lib
     | Some name ->
         let fullpath = path @ [ name ] in
         if Hashtbl.mem unsupported_stdlib fullpath then lib
         else
           let fullpath = "Ortac_runtime" :: fullpath in
-          L.add ls (String.concat "." fullpath) lib
+          add sym (String.concat "." fullpath) lib
   in
   let stdlib =
     List.fold_left
@@ -113,8 +129,24 @@ let init module_name env =
       L.empty builtins
   in
   let stdlib =
-    fold_namespace process_gostd_entry [ "Gospelstdlib" ] gostd stdlib
+    fold_namespace
+      (fun ns -> ns.ns_ls)
+      (process_gostd_entry L.add)
+      [ "Gospelstdlib" ] gostd stdlib
+  in
+  let tystdlib =
+    List.fold_left
+      (fun acc (path, ocaml) ->
+        let ts = get_env ns_find_ts env path in
+        T.add ts ocaml acc)
+      T.empty tybuiltins
+  in
+  let tystdlib =
+    fold_namespace
+      (fun ns -> ns.ns_ts)
+      (process_gostd_entry T.add)
+      [ "Gospelstdlib" ] gostd tystdlib
   in
-  { module_name; stdlib; env; functions = L.empty }
+  { module_name; stdlib; tystdlib; env; functions = L.empty }
 
 let module_name t = t.module_name

src/core/context.mli

@@ -14,7 +14,12 @@ val module_name : t -> string
 
 val translate_stdlib : Symbols.lsymbol -> t -> string option
 (** [translate_stdlib ls t] finds the name of the OCaml function to call to
-    translate [ls] if it is a symbol of the Gospel standard library *)
+    translate [ls] if it is a symbol of the Gospel standard library or a
+    built-in *)
+
+val translate_tystdlib : Ttypes.tysymbol -> t -> string option
+(** [translate_tystdlib ls t] finds the name of the OCaml type to use to
+    translate [ts] if it is a type of the Gospel standard library or a built-in *)
 
 val get_ls : t -> string list -> Symbols.lsymbol
 (** [get_ls context qualid_name] gets the Gospel logical symbol corresponding to

src/core/ocaml_of_gospel.ml

@@ -162,11 +162,12 @@ let term_with_catch ~context t =
     with e ->
       raise (Ortac_runtime.Partial_function (e, [%e elocation t.t_loc]))]
 
-let core_type_of_ty_with_subst subst ty =
+let core_type_of_ty_with_subst ~context subst ty =
   let open Ttypes in
   let lident_of_tysymbol ts =
-    (if ty_equal ty_integer ty then "Ortac_runtime.integer"
-     else Fmt.str "%a" Ident.pp ts.ts_ident)
+    (match Context.translate_tystdlib ts context with
+    | Some ty -> ty
+    | None -> Fmt.str "%a" Ident.pp ts.ts_ident)
     |> Builder.lident
   in
   let rec aux ty =
@@ -181,13 +182,16 @@ let core_type_of_ty_with_subst subst ty =
   in
   aux ty
 
-let core_type_of_tysymbol (ts : Ttypes.tysymbol) : Ppxlib.core_type =
-  let lid = Fmt.str "%a" Ident.pp ts.ts_ident |> Builder.lident in
+let core_type_of_tysymbol ~context ts =
+  let lid =
+    (match Context.translate_tystdlib ts context with
+    | Some ty -> ty
+    | None -> Fmt.str "%a" Ident.pp ts.Ttypes.ts_ident)
+    |> Builder.lident
+  in
   let args =
     List.map
-      (fun tv ->
-        let open Ttypes in
-        Builder.ptyp_var (Fmt.str "%a" Ident.pp tv.tv_name))
+      (fun tv -> Builder.ptyp_var (Fmt.str "%a" Ident.pp tv.Ttypes.tv_name))
       ts.ts_args
   in
   Builder.ptyp_constr lid args

src/core/ocaml_of_gospel.mli

@@ -13,10 +13,14 @@ val term_with_catch :
     the exception *)
 
 val core_type_of_ty_with_subst :
-  (string -> Ppxlib.core_type option) -> Gospel.Ttypes.ty -> Ppxlib.core_type
+  context:Context.t ->
+  (string -> Ppxlib.core_type option) ->
+  Gospel.Ttypes.ty ->
+  Ppxlib.core_type
 (** [core_type_of_ty_with_subst subst ty] translates a Gospel type into the
     corresponding OCaml [core_type] applying [subst] on the type variables *)
 
-val core_type_of_tysymbol : Gospel.Ttypes.tysymbol -> Ppxlib.core_type
+val core_type_of_tysymbol :
+  context:Context.t -> Gospel.Ttypes.tysymbol -> Ppxlib.core_type
 (** [core_type_of_tysymbol ts] translates a Gospel type symbol into the
     corresponding OCaml [core_type] **)