Merge branch 'main' of github.com:mrjazzybread/gospel

.ocamlformat

@@ -1,4 +1,4 @@
-version = 0.26.0
+version = 0.26.1
 parse-docstrings = true
 break-infix = fit-or-vertical
 module-item-spacing = compact

CHANGES.md

@@ -1,3 +1,24 @@
+# 0.3
+
+## Added
+
+- Created a gallery of Gospel examples that might serve as a working ground
+  to experiment with Gospel syntax and future extensions of the language.
+  [#361] (https://github.com/ocaml-gospel/gospel/pull/361)
+
+## Improved
+
+- Make the `with` necessary when declaring type invariants
+  [\#372](https://github.com/ocaml-gospel/gospel/pull/372) and
+  [\#374](https://github.com/ocaml-gospel/gospel/pull/374)
+
+## Internals
+
+- Use unique identifiers rather than physical equality for `Symbols.ls_equal`
+  [\#380](https://github.com/ocaml-gospel/gospel/pull/380)
+- Remove the `gospel_expected` prologue at the end of successful tests
+  [\#363](https://github.com/ocaml-gospel/gospel/pull/363)
+
 # 0.2
 
 ## Added

README.md

@@ -22,9 +22,59 @@ interfaces with formal contracts that describe type invariants, mutability,
 function pre-conditions and post-conditions, effects, exceptions, and [much
 more](https://ocaml-gospel.github.io/gospel/)!
 
-<div align="center">
-<img src="screenshot.png" title="Gospel specification">
-</div>
+```ocaml
+type 'a t
+(*@ model capacity : integer
+    mutable model contents : 'a sequence
+    with s
+    invariant s.capacity > 0
+    invariant Sequence.length s.contents <= s.capacity *)
+
+exception Full
+exception Empty
+
+val create : int -> 'a t
+(*@ s = create n
+    requires n > 0
+    ensures s.capacity = n
+    ensures s.contents = Sequence.empty *)
+
+val is_empty : 'a t -> bool
+(*@ b = is_empty s
+    pure
+    ensures b <-> s.contents = Sequence.empty *)
+
+val clear : 'a t -> unit
+(*@ clear s
+    modifies s.contents
+    ensures s.contents = Sequence.empty *)
+
+val push : 'a -> 'a t -> unit
+(*@ push a s
+    modifies s.contents
+    ensures s.contents = Sequence.cons a (old s.contents)
+    raises Full -> Sequence.length (old s.contents) = s.capacity
+                /\ s.contents = old s.contents *)
+
+val pop : 'a t -> 'a
+(*@ a = pop s
+    modifies s.contents
+    ensures a = Sequence.hd (old s.contents)
+    ensures s.contents = Sequence.tl (old s.contents)
+    raises Empty -> old s.contents = Sequence.empty = s.contents *)
+
+val pop_opt : 'a t -> 'a option
+(*@ o = pop_opt s
+    modifies s.contents
+    ensures match o with
+                | None -> old s.contents = Sequence.empty = s.contents
+                | Some a -> old s.contents = Sequence.cons a s.contents *)
+
+val top : 'a t -> 'a
+(*@ a = top s
+    ensures a = Sequence.hd s.contents
+    raises Empty -> s.contents = Sequence.empty *)
+```
 
 We designed Gospel to provide a tool-agnostic frontend for bringing formal
 methods into the OCaml ecosystem, meaning that we make no assumptions on the

docs/docs/getting-started/container.mli

@@ -2,8 +2,9 @@ type 'a t
 (** The type for containers. *)
 (*@ model capacity: int
     mutable model contents: 'a set
-    invariant capacity > 0
-    invariant Set.cardinal contents <= capacity *)
+    with t
+    invariant t.capacity > 0
+    invariant Set.cardinal t.contents <= t.capacity *)
 
 exception Full
 

docs/docs/language/type-specifications.md

@@ -28,8 +28,9 @@ The specification of this type contains three elements:
 Type specifications can contain models, invariants, and mutability information.
 
 ```ebnf title="Type specification syntax"
-type_specification = "ephemeral"? model-clause* invariant-clause*
+type_specification = "ephemeral"? model-clause* invariant-block?
 model-clause = "mutable"? "model" identifier ":" type_expression
+invariant-block = "with" identifier invariant-clause+
 invariant-clause = "invariant" expr
 ```
 
@@ -75,7 +76,8 @@ Only use `ephemeral` when there is mutability that cannot be guessed otherwise.
 
 Type annotations may also contain invariants that hold at every function's entry
 and exit point that manipulates their values. Formulae expressing these
-properties may be added after the `invariant` keyword:
+properties may be added after the `invariant` keyword. The `with` keyword introduces
+a name for a value of the type being specified:
 
 ```ocaml {4}
 type 'a t

examples/Stack.mli

@@ -0,0 +1,38 @@
+module type S = sig
+  type 'a t
+  (*@ mutable model view : 'a sequence *)
+
+  val create : unit -> 'a t
+  (*@ s = create ()
+        ensures s.view = Sequence.empty *)
+
+  val size : 'a t -> int
+  (*@ n = size s
+        ensures n = Sequence.length s.view *)
+
+  val is_empty : 'a t -> bool
+  (*@ b = is_empty s
+        ensures b <-> s.view = Sequence.empty *)
+
+  val push : 'a -> 'a t -> unit
+  (*@ push x s
+        modifies s
+        ensures  s.view = Sequence.cons x (old s.view) *)
+
+  val pop : 'a t -> 'a
+  (*@ x = pop s
+        requires s.view <> Sequence.empty
+        modifies s
+        ensures  s.view = (old s.view)[1 ..] *)
+
+  val clear : 'a t -> unit
+  (*@ clear s
+        modifies s
+        ensures  s.view = Sequence.empty *)
+
+  val concat : 'a t -> 'a t -> unit
+  (*@ concat s1 s2
+        modifies s1, s2
+        ensures s1.view = (old s1.view ++ old s2.view)
+        ensures s2.view = Sequence.empty *)
+end

src/symbols.ml

@@ -39,7 +39,7 @@ type lsymbol = {
 [@@deriving show]
 
 (* CHECK *)
-let ls_equal : lsymbol -> lsymbol -> bool = ( == )
+let ls_equal l r = Ident.equal l.ls_name r.ls_name
 
 module LS = struct
   type t = lsymbol

src/tast.ml

@@ -57,7 +57,7 @@ type val_description = {
 type type_spec = {
   ty_ephemeral : bool;  (** Ephemeral *)
   ty_fields : (lsymbol * bool) list;  (** Models (field symbol * mutable) *)
-  ty_invariants : vsymbol option * term list;  (** Invariants *)
+  ty_invariants : (vsymbol * term list) option;  (** Invariants *)
   ty_text : string;
       (** String containing the original specificaion as written by the user *)
   ty_loc : Location.t; [@printer Utils.Fmt.pp_loc]  (** Specification location *)

src/tast_helper.mli

@@ -10,7 +10,7 @@ val vs_of_lb_arg : lb_arg -> vsymbol
 val type_spec :
   bool ->
   (lsymbol * bool) list ->
-  vsymbol option * term list ->
+  (vsymbol * term list) option ->
   string ->
   Location.t ->
   type_spec

src/tast_printer.ml

@@ -7,6 +7,7 @@ open Ttypes
 open Upretty_printer
 open Opprintast
 open Fmt
+module Option = Stdlib.Option
 
 let print_variant_field fmt ld =
   pp fmt "%s%a:%a"
@@ -45,7 +46,8 @@ let print_type_kind fmt = function
         (rd.rd_cs :: pjs)
 
 let print_type_spec fmt { ty_ephemeral; ty_fields; ty_invariants; _ } =
-  if (not ty_ephemeral) && ty_fields = [] && snd ty_invariants = [] then ()
+  if (not ty_ephemeral) && ty_fields = [] && Option.is_none ty_invariants then
+    ()
   else
     let print_ephemeral f e = if e then pp f "@[ephemeral@]" in
     let print_term f t = pp f "@[%a@]" print_term t in
@@ -55,16 +57,21 @@ let print_type_spec fmt { ty_ephemeral; ty_fields; ty_invariants; _ } =
         print_ls_nm ls print_ty
         (Stdlib.Option.get ls.ls_value)
     in
-    let print_invariant_vs ppf = pf ppf "with %a" print_vs in
-    pp fmt "(*@@ @[%a%a%a%a@] *)" print_ephemeral ty_ephemeral
+    let print_invariants ppf i =
+      pf ppf "with %a@;%a" print_vs (fst i)
+        (list
+           ~first:(newline ++ const string "invariant ")
+           ~sep:(const string "@\ninvariant")
+           print_term)
+        (snd i)
+    in
+    pp fmt "(*@@ @[%a%a%a@] *)" print_ephemeral ty_ephemeral
       (list ~first:newline ~sep:newline print_field)
       ty_fields
-      (option print_invariant_vs)
-      (fst ty_invariants)
-      (list
-         ~first:(newline ++ const string "invariant ")
-         ~sep:(const string "invariant") print_term)
-      (snd ty_invariants)
+      (* (option print_invariant_vs) *)
+      (* ty_invariants *)
+      (option print_invariants)
+      ty_invariants
 
 let print_type_declaration fmt td =
   let print_param fmt (tv, (v, i)) =

src/typing.ml

@@ -565,19 +565,14 @@ let process_type_spec kid crcm ns ty spec =
   in
   let ns, fields = List.fold_left field (ns, []) spec.ty_field in
   let fields = List.rev fields in
-  let self_vs =
-    Option.map (fun x -> create_vsymbol x ty) (fst spec.ty_invariant)
+  let aux = function
+    | vs, xs ->
+        let self_vs = create_vsymbol vs ty in
+        let env = Mstr.singleton self_vs.vs_name.id_str self_vs in
+        (self_vs, List.map (fmla Invariant kid crcm ns env) xs)
   in
-  let env =
-    match self_vs with
-    | Some vs -> Mstr.singleton vs.vs_name.id_str vs
-    | None -> Mstr.empty
-  in
-  let invariants =
-    List.map (fmla Invariant kid crcm ns env) (snd spec.ty_invariant)
-  in
-  type_spec spec.ty_ephemeral fields (self_vs, invariants) spec.ty_text
-    spec.ty_loc
+  let invariants = Option.map aux spec.ty_invariant in
+  type_spec spec.ty_ephemeral fields invariants spec.ty_text spec.ty_loc
 
 (* TODO compare manifest with td_kind *)
 let type_type_declaration path kid crcm ns r tdl =
@@ -718,7 +713,7 @@ let type_type_declaration path kid crcm ns r tdl =
     (* invariants are only allowed on abstract/private types *)
     (match ((td.tkind, td.tmanifest), td.tspec) with
     | ( ((Ptype_variant _ | Ptype_record _), _ | _, Some _),
-        Some { ty_invariant = _, _ :: _; _ } )
+        Some { ty_invariant = Some _; _ } )
       when td.tprivate = Public ->
         W.error ~loc:td.tloc (W.Public_type_invariant td_ts.ts_ident.id_str)
     | _, _ -> ());

src/uast.mli

@@ -116,7 +116,7 @@ type field = {
 type type_spec = {
   ty_ephemeral : bool;
   ty_field : field list;
-  ty_invariant : Preid.t option * term list;
+  ty_invariant : (Preid.t * term list) option;
   ty_text : string;
   ty_loc : Location.t;
 }

src/uparser.mly

@@ -200,8 +200,8 @@ ts_ephemeral:
 ;
 
 ts_invariants:
-| l=list(ts_invariant) { None, l }
-| WITH id=lident l=nonempty_list(ts_invariant) { Some id, l }
+| WITH id=lident l=nonempty_list(ts_invariant) { Some (id, l) }
+|                                              { None }
 ;
 
 ts_invariant:

src/upretty_printer.ml

@@ -11,6 +11,7 @@
 open Ppxlib
 open Uast
 open Opprintast
+module Option = Stdlib.Option
 open Utils.Fmt
 
 let const_hole s fmt _ = pp fmt "%s" s
@@ -43,9 +44,9 @@ let type_spec f ts =
     pp f "@[<v>%a%a%a@]" ephemeral ts.ty_ephemeral (list_keyword "model ...")
       ts.ty_field
       (list_keyword "invariant ...")
-      (snd ts.ty_invariant)
+      Option.(value ~default:[] (map snd ts.ty_invariant))
   in
-  if ts.ty_ephemeral || ts.ty_field != [] || snd ts.ty_invariant != [] then
+  if ts.ty_ephemeral || ts.ty_field != [] || Option.is_some ts.ty_invariant then
     pp f "@[%a@]" (spec print_tspec) ts
   else ()
 

test/coercions/basic.mli

@@ -3,7 +3,3 @@ type t2
 
 (*@ function c (x: t1) : t2 *)
 (*@ coercion *)
-
-(* {gospel_expected|
-   [0] OK
-   |gospel_expected} *)

test/coercions/constr_literal.mli

@@ -3,7 +3,3 @@
 val f : int -> int
 (*@ y = f x
     requires A 42i = A 42i *)
-
-(* {gospel_expected|
-   [0] OK
-   |gospel_expected} *)

test/literals/ints.mli

@@ -8,7 +8,3 @@ val f : int -> int
     requires 42 = 0x16
     requires A 42i = A 0x16i
     requires A 42i = A 43i *)
-
-(* {gospel_expected|
-   [0] OK
-   |gospel_expected} *)

test/locations/test_location.t

@@ -114,7 +114,7 @@ First, create a test artifact:
                          ls_constr = false; ls_field = true },
                        false)
                       ];
-                    ty_invariants = (None, []);
+                    ty_invariants = None;
                     ty_text =
                     " mutable model contents : 'a list\n    model size : int ";
                     ty_loc = foo.mli:5:3 });

test/patterns/allsorts.mli

@@ -202,7 +202,3 @@ val f16 : t16 -> int
            | C (y,z) when (match y with A -> true | _ -> false) -> true
            | _ -> true
 *)
-
-(* {gospel_expected|
-   [0] OK
-   |gospel_expected} *)

test/patterns/allsorts2.mli

@@ -26,7 +26,3 @@ type t2 = B of int * int
 
 (*@ function f (x: t2) : unit =
     match x with B _ -> () *)
-
-(* {gospel_expected|
-   [0] OK
-   |gospel_expected} *)

test/patterns/expressions_raises.mli

@@ -23,7 +23,3 @@ val f : int -> t -> bool
     (* raises E _ -> false *)
     raises F _ -> true
     raises F (_, _) -> true *)
-
-(* {gospel_expected|
-   [0] OK
-   |gospel_expected} *)

test/patterns/fun_option.mli

@@ -2,7 +2,3 @@ val f : 'a option list -> bool
 (*@ b = f os
     ensures List._exists (fun (None | Some _) -> false) os
 *)
-
-(* {gospel_expected|
-   [0] OK
-   |gospel_expected} *)

test/patterns/fun_pair.mli

@@ -2,7 +2,3 @@ val f : (int * 'a) list -> int list
 (*@ ys = f xs
     ensures ys = List.map (fun (x, _) -> x) xs
 *)
-
-(* {gospel_expected|
-   [0] OK
-   |gospel_expected} *)

test/patterns/fun_triple.mli

@@ -2,7 +2,3 @@ val f : ('a * 'b * 'c) list -> 'a list
 (*@ xs = f ys
     ensures xs = List.map (fun (x, _, _) : 'a -> x) ys
 *)
-
-(* {gospel_expected|
-   [0] OK
-   |gospel_expected} *)