diff --git a/.ocamlformat b/.ocamlformat index ea59eff6..8c36f40c 100644 --- a/.ocamlformat +++ b/.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 diff --git a/CHANGES.md b/CHANGES.md index 69ec680a..05e1209c 100644 --- a/CHANGES.md +++ b/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 diff --git a/README.md b/README.md index 012e3054..17498ee5 100644 --- a/README.md +++ b/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/)! -
- -
+```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 diff --git a/docs/docs/getting-started/container.mli b/docs/docs/getting-started/container.mli index ab313304..5094e48c 100644 --- a/docs/docs/getting-started/container.mli +++ b/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 diff --git a/docs/docs/language/type-specifications.md b/docs/docs/language/type-specifications.md index 45dfa361..0ee92f90 100644 --- a/docs/docs/language/type-specifications.md +++ b/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 diff --git a/examples/Stack.mli b/examples/Stack.mli new file mode 100644 index 00000000..b80476be --- /dev/null +++ b/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 diff --git a/screenshot.png b/screenshot.png deleted file mode 100644 index 41eb19bb..00000000 Binary files a/screenshot.png and /dev/null differ diff --git a/src/symbols.ml b/src/symbols.ml index 8191fbb9..7491e26e 100644 --- a/src/symbols.ml +++ b/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 diff --git a/src/tast.ml b/src/tast.ml index 0ca07230..8fd7d2a8 100644 --- a/src/tast.ml +++ b/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 *) diff --git a/src/tast_helper.mli b/src/tast_helper.mli index 923af497..191c04fc 100644 --- a/src/tast_helper.mli +++ b/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 diff --git a/src/tast_printer.ml b/src/tast_printer.ml index e23914f6..bb25e8bf 100644 --- a/src/tast_printer.ml +++ b/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)) = diff --git a/src/typing.ml b/src/typing.ml index 1a6e460b..a1892680 100644 --- a/src/typing.ml +++ b/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) | _, _ -> ()); diff --git a/src/uast.mli b/src/uast.mli index bfd149e1..961a5a0e 100644 --- a/src/uast.mli +++ b/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; } diff --git a/src/uparser.mly b/src/uparser.mly index 3dba9ef6..8c6a4bef 100644 --- a/src/uparser.mly +++ b/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: diff --git a/src/upretty_printer.ml b/src/upretty_printer.ml index ee1aa204..561aee90 100644 --- a/src/upretty_printer.ml +++ b/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 "@[%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 () diff --git a/test/coercions/basic.mli b/test/coercions/basic.mli index 9485e49d..4ef5d588 100644 --- a/test/coercions/basic.mli +++ b/test/coercions/basic.mli @@ -3,7 +3,3 @@ type t2 (*@ function c (x: t1) : t2 *) (*@ coercion *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/coercions/constr_literal.mli b/test/coercions/constr_literal.mli index cdce3668..bbeec6ca 100644 --- a/test/coercions/constr_literal.mli +++ b/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} *) diff --git a/test/literals/ints.mli b/test/literals/ints.mli index fa87cbac..8c0887db 100644 --- a/test/literals/ints.mli +++ b/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} *) diff --git a/test/locations/test_location.t b/test/locations/test_location.t index b21d48c7..97053793 100644 --- a/test/locations/test_location.t +++ b/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 }); diff --git a/test/patterns/allsorts.mli b/test/patterns/allsorts.mli index fe15d637..e5f3d92d 100644 --- a/test/patterns/allsorts.mli +++ b/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} *) diff --git a/test/patterns/allsorts2.mli b/test/patterns/allsorts2.mli index a21bdcf0..f1cf02ca 100644 --- a/test/patterns/allsorts2.mli +++ b/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} *) diff --git a/test/patterns/expressions_raises.mli b/test/patterns/expressions_raises.mli index 140bb80f..4e9cbb72 100644 --- a/test/patterns/expressions_raises.mli +++ b/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} *) diff --git a/test/patterns/fun_option.mli b/test/patterns/fun_option.mli index f8a1103d..03fb62a4 100644 --- a/test/patterns/fun_option.mli +++ b/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} *) diff --git a/test/patterns/fun_pair.mli b/test/patterns/fun_pair.mli index 57e59019..1c505f80 100644 --- a/test/patterns/fun_pair.mli +++ b/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} *) diff --git a/test/patterns/fun_triple.mli b/test/patterns/fun_triple.mli index b05c564a..4c1f1f13 100644 --- a/test/patterns/fun_triple.mli +++ b/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} *) diff --git a/test/patterns/inner_cast.mli b/test/patterns/inner_cast.mli index c9bed137..fb424cb9 100644 --- a/test/patterns/inner_cast.mli +++ b/test/patterns/inner_cast.mli @@ -3,7 +3,3 @@ val f : int option -> int requires match x with | Some (y:int) -> y >= 0 | None -> true *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/ppx/odoc_of_gospel.expected.mli b/test/ppx/odoc_of_gospel.expected.mli index 9b731e75..65e5a999 100644 --- a/test/ppx/odoc_of_gospel.expected.mli +++ b/test/ppx/odoc_of_gospel.expected.mli @@ -28,8 +28,9 @@ [@@@ocaml.text "{@gospel[\nGospel declaration:\n type casper ]}"] type 'a t[@@ocaml.doc {| A program type declaration with specifications |}] [@@gospel {| model m : 'a sequence + with x invariant true |}][@@ocaml.doc - "{@gospel[\nGospel specification:\n model m : 'a sequence\n invariant true ]}"] + "{@gospel[\nGospel specification:\n model m : 'a sequence\n with x\n invariant true ]}"] val prog_fun : int -> int[@@ocaml.doc {| A program function with specifications |}] [@@gospel {| y = prog_fun x diff --git a/test/ppx/odoc_of_gospel.mli b/test/ppx/odoc_of_gospel.mli index 5f048adc..b748ee27 100644 --- a/test/ppx/odoc_of_gospel.mli +++ b/test/ppx/odoc_of_gospel.mli @@ -29,6 +29,7 @@ type 'a t (** A program type declaration with specifications *) (*@ model m : 'a sequence + with x invariant true *) val prog_fun : int -> int diff --git a/test/ppx/odoc_output.t b/test/ppx/odoc_output.t index 0c1c29db..7aa3beea 100644 --- a/test/ppx/odoc_output.t +++ b/test/ppx/odoc_output.t @@ -56,6 +56,7 @@ columns: A program type declaration with specifications Gospel specification: model m : 'a sequence + with x invariant true \f[CB]val\fR prog_fun : int \f[CB]\->\fR int diff --git a/test/pure/pure_promoted.mli b/test/pure/pure_promoted.mli index 043f161b..4d45055d 100644 --- a/test/pure/pure_promoted.mli +++ b/test/pure/pure_promoted.mli @@ -6,7 +6,3 @@ val f : int -> int val g : int -> int (*@ y = g x requires f x > 0 *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/semantic/invariant1.mli b/test/semantic/invariant1.mli index 6e213827..aaff6680 100644 --- a/test/semantic/invariant1.mli +++ b/test/semantic/invariant1.mli @@ -1,9 +1,9 @@ type t = { a : int } -(*@ invariant a >= 0 *) +(*@ with t invariant t.a >= 0 *) (* {gospel_expected| - [125] File "invariant1.mli", line 1, characters 0-44: + [125] File "invariant1.mli", line 1, characters 0-53: 1 | type t = { a : int } - 2 | (*@ invariant a >= 0 *) + 2 | (*@ with t invariant t.a >= 0 *) Error: Invariant on public type t. |gospel_expected} *) diff --git a/test/semantic/invariant2.mli b/test/semantic/invariant2.mli index b2efe94a..eb394c11 100644 --- a/test/semantic/invariant2.mli +++ b/test/semantic/invariant2.mli @@ -1,9 +1,9 @@ type t = A | B -(*@ invariant 1 >= 0 *) +(*@ with x invariant 1 >= 0 *) (* {gospel_expected| - [125] File "invariant2.mli", line 1, characters 0-38: + [125] File "invariant2.mli", line 1, characters 0-45: 1 | type t = A | B - 2 | (*@ invariant 1 >= 0 *) + 2 | (*@ with x invariant 1 >= 0 *) Error: Invariant on public type t. |gospel_expected} *) diff --git a/test/semantic/invariant3.mli b/test/semantic/invariant3.mli index 76cbfa27..0f7f9619 100644 --- a/test/semantic/invariant3.mli +++ b/test/semantic/invariant3.mli @@ -1,9 +1,9 @@ type t = int * int -(*@ invariant 1 > 0 *) +(*@ with x invariant 1 > 0 *) (* {gospel_expected| - [125] File "invariant3.mli", line 1, characters 0-41: + [125] File "invariant3.mli", line 1, characters 0-48: 1 | type t = int * int - 2 | (*@ invariant 1 > 0 *) + 2 | (*@ with x invariant 1 > 0 *) Error: Invariant on public type t. |gospel_expected} *) diff --git a/test/syntax/abstract_functions.mli b/test/syntax/abstract_functions.mli index 26dd4a2e..f48eb0c0 100644 --- a/test/syntax/abstract_functions.mli +++ b/test/syntax/abstract_functions.mli @@ -61,7 +61,3 @@ (*@ function h14 (x: 'a): test *) (*@ function h15 (x: test): integer *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/allsorts_labels.mli b/test/syntax/allsorts_labels.mli index 2e6589fd..de6c60ce 100644 --- a/test/syntax/allsorts_labels.mli +++ b/test/syntax/allsorts_labels.mli @@ -54,7 +54,3 @@ val f : int ref -> unit val f : int ref -> unit (*@ f x modifies x *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/basic_functions_axioms.mli b/test/syntax/basic_functions_axioms.mli index 85bb24eb..1d370cf1 100644 --- a/test/syntax/basic_functions_axioms.mli +++ b/test/syntax/basic_functions_axioms.mli @@ -125,7 +125,3 @@ type 'a t6 = { xx : 'a; yy : int } | {y = B; x} -> {yy=int_of_integer 10; xx = b.y } | {x; y} -> {xx=y;yy=x} *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/bitvector.mli b/test/syntax/bitvector.mli index 816f886f..403961cc 100644 --- a/test/syntax/bitvector.mli +++ b/test/syntax/bitvector.mli @@ -22,7 +22,3 @@ val mem : int -> t -> bool (*@ b = mem i bv checks 0 <= i < bv.size ensures b <-> mem i bv *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/constants.mli b/test/syntax/constants.mli index a2a1df2e..b9939c41 100644 --- a/test/syntax/constants.mli +++ b/test/syntax/constants.mli @@ -12,7 +12,3 @@ val y : t val modify_y : unit -> unit (*@ modify_y () modifies y *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/constructor_arity5.mli b/test/syntax/constructor_arity5.mli index 53e40aab..dbab198f 100644 --- a/test/syntax/constructor_arity5.mli +++ b/test/syntax/constructor_arity5.mli @@ -5,7 +5,3 @@ val f : (int * int) option -> unit | Some (_,_) -> true | _ -> false *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/exceptions.mli b/test/syntax/exceptions.mli index e75de0fb..0f7befc0 100644 --- a/test/syntax/exceptions.mli +++ b/test/syntax/exceptions.mli @@ -47,7 +47,3 @@ val f : 'a -> 'a raises E11 'a' -> true raises E11 ('a' | 'b') -> true raises E11 ('c'..'z') -> true *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/expressions.mli b/test/syntax/expressions.mli index 99b72b51..265917eb 100644 --- a/test/syntax/expressions.mli +++ b/test/syntax/expressions.mli @@ -30,7 +30,3 @@ val f : int -> int -> int ensures r = x + y ensures r > 2 ensures r = 3 *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/ghost_arg1.mli b/test/syntax/ghost_arg1.mli index 03284b1d..f21e39a2 100644 --- a/test/syntax/ghost_arg1.mli +++ b/test/syntax/ghost_arg1.mli @@ -19,7 +19,3 @@ val log2_existsb : int -> int (*@ r = log2_existsb x requires exists i. i >= 0 /\ x = pow 2 i ensures x = pow 2 r *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/ghost_arg2.mli b/test/syntax/ghost_arg2.mli index fa23eafe..4feead36 100644 --- a/test/syntax/ghost_arg2.mli +++ b/test/syntax/ghost_arg2.mli @@ -7,7 +7,3 @@ val fib : int -> int -> int -> int requires a = fibonacci i requires b = fibonacci (i+1) ensures r = fibonacci (i+n) *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/infix.mli b/test/syntax/infix.mli index 090d0a81..06ee431b 100644 --- a/test/syntax/infix.mli +++ b/test/syntax/infix.mli @@ -5,7 +5,3 @@ val ( == ) : 'a -> 'a -> bool val ( == ) : 'a -> 'a -> bool (*@ r = x == y ensures r <-> x = y *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/invariant5.mli b/test/syntax/invariant5.mli index d725a258..e600788f 100644 --- a/test/syntax/invariant5.mli +++ b/test/syntax/invariant5.mli @@ -1,10 +1,10 @@ type 'a t = private { a : 'a } -(*@ invariant self.a = self.a *) +(*@ with t invariant self.a = self.a *) (* {gospel_expected| - [125] File "invariant5.mli", line 2, characters 14-18: - 2 | (*@ invariant self.a = self.a *) - ^^^^ + [125] File "invariant5.mli", line 2, characters 21-25: + 2 | (*@ with t invariant self.a = self.a *) + ^^^^ Error: Symbol self not found in scope (see "Symbols in scope" documentation page). |gospel_expected} *) diff --git a/test/syntax/invariants.mli b/test/syntax/invariants.mli index e4fd78db..80104d87 100644 --- a/test/syntax/invariants.mli +++ b/test/syntax/invariants.mli @@ -2,11 +2,7 @@ type t1 = private { a : int } (*@ with x invariant x.a >= 0 *) type t2 = private A | B -(*@ invariant 1 > 0 *) +(*@ with x invariant 1 > 0 *) type t3 = private int * int -(*@ invariant 1 > 0 *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) +(*@ with x invariant 1 > 0 *) diff --git a/test/syntax/literals.mli b/test/syntax/literals.mli index 389aca7f..67078e3e 100644 --- a/test/syntax/literals.mli +++ b/test/syntax/literals.mli @@ -9,7 +9,3 @@ val g : char -> string (*@ y = g x requires x = 'c' ensures y = "c" *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/module_with.mli b/test/syntax/module_with.mli index 5f347561..61b82fec 100644 --- a/test/syntax/module_with.mli +++ b/test/syntax/module_with.mli @@ -7,7 +7,3 @@ module type B = sig module C : A with type t = t end - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/modules1.mli b/test/syntax/modules1.mli index 11c1b21d..f569d901 100644 --- a/test/syntax/modules1.mli +++ b/test/syntax/modules1.mli @@ -16,7 +16,3 @@ type int * module A : TA with type 'a t := 'a t1 *) (* @ function t1 (x:'a t1) : float = A.f x *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/modules2.mli b/test/syntax/modules2.mli index 78dc3072..b7f461b3 100644 --- a/test/syntax/modules2.mli +++ b/test/syntax/modules2.mli @@ -59,7 +59,3 @@ val default : MF.ft -> MF.ft requires MF.fp1 y ensures MF.fp2 x *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/no_specification.mli b/test/syntax/no_specification.mli index 9f3911a0..7477a256 100644 --- a/test/syntax/no_specification.mli +++ b/test/syntax/no_specification.mli @@ -1,5 +1 @@ val f : int -> unit - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/open2.mli b/test/syntax/open2.mli index 78bb1224..3623fc30 100644 --- a/test/syntax/open2.mli +++ b/test/syntax/open2.mli @@ -1,7 +1,3 @@ open Type type t2 = t - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/open3.mli b/test/syntax/open3.mli index 212252f1..d4ac2fab 100644 --- a/test/syntax/open3.mli +++ b/test/syntax/open3.mli @@ -3,7 +3,3 @@ open Types_functions type t3 = t1 * int t2 (*@ function f4 (x: int t2) (y: t1) : t3 = (y,x) *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/open_gospelstdlib_module.mli b/test/syntax/open_gospelstdlib_module.mli index 433377bb..fe72e63b 100644 --- a/test/syntax/open_gospelstdlib_module.mli +++ b/test/syntax/open_gospelstdlib_module.mli @@ -1,7 +1,3 @@ type 'a t = 'a list (*@ open Set *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/open_qualified.mli b/test/syntax/open_qualified.mli index f7d359e6..3f2e8865 100644 --- a/test/syntax/open_qualified.mli +++ b/test/syntax/open_qualified.mli @@ -4,7 +4,3 @@ type t4 = t3 type t5 = int Types_functions.t2 (*@ function f5 (x: 'a Types_functions.t2) : Types_functions.t1 *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/partial_application.mli b/test/syntax/partial_application.mli index bc888bb5..22fce72f 100644 --- a/test/syntax/partial_application.mli +++ b/test/syntax/partial_application.mli @@ -2,7 +2,3 @@ val scalar_product : int list -> int -> int list (*@ r = scalar_product v s ensures List.map integer_of_int r = List.map ((fun x y -> x * integer_of_int y) (integer_of_int s)) v *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/predicates.mli b/test/syntax/predicates.mli index bae81756..1561fea7 100644 --- a/test/syntax/predicates.mli +++ b/test/syntax/predicates.mli @@ -19,7 +19,3 @@ val merge : int array -> int array -> int array (*@ requires n >= 0 variant n ensures result >= 0 *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/pure.mli b/test/syntax/pure.mli index 336b90ca..ccd95dbf 100644 --- a/test/syntax/pure.mli +++ b/test/syntax/pure.mli @@ -3,7 +3,3 @@ val f : int -> int * int val f : int -> int * int * int (*@ pure *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/qualified.mli b/test/syntax/qualified.mli index 285178b3..2b86a3e7 100644 --- a/test/syntax/qualified.mli +++ b/test/syntax/qualified.mli @@ -1,7 +1,3 @@ (*@ type t3 = Open2.t2 *) (*@ type t4 = Type.t *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/recursive_invariants.mli b/test/syntax/recursive_invariants.mli index 6c49838c..191afa8d 100644 --- a/test/syntax/recursive_invariants.mli +++ b/test/syntax/recursive_invariants.mli @@ -12,7 +12,3 @@ type u = private { tag : int; next : u } val f : u -> u (*@ y = f x requires x.tag = 0 *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/stdlib_exceptions.mli b/test/syntax/stdlib_exceptions.mli index e2869db7..7bb8db9b 100644 --- a/test/syntax/stdlib_exceptions.mli +++ b/test/syntax/stdlib_exceptions.mli @@ -9,7 +9,3 @@ val find : ('a -> bool) -> 'a list -> 'a val invalid_arg : string -> 'a (*@ raises Invalid_argument _ -> true ensures false *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/type.mli b/test/syntax/type.mli index fbe8b1f5..63c57c4e 100644 --- a/test/syntax/type.mli +++ b/test/syntax/type.mli @@ -1,5 +1 @@ type t - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/type_decl.mli b/test/syntax/type_decl.mli index e1027af8..9c44fc43 100644 --- a/test/syntax/type_decl.mli +++ b/test/syntax/type_decl.mli @@ -43,7 +43,3 @@ and 'b t22 = C of 'b type t23 = u and u = C of v and v = t23 - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/types.mli b/test/syntax/types.mli index 2bb1bcab..591c6c9d 100644 --- a/test/syntax/types.mli +++ b/test/syntax/types.mli @@ -2,7 +2,3 @@ type t = int -> int type u = (int -> int) ref type v = private { x : int -> int } (*@ with self invariant self.x 0i = 0 *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/types_functions.mli b/test/syntax/types_functions.mli index 932956f7..5d991d8f 100644 --- a/test/syntax/types_functions.mli +++ b/test/syntax/types_functions.mli @@ -6,7 +6,3 @@ type 'a t2 (*@ function f2 (x: int) : t1 *) (*@ function f3 (x: int) : int t2 = f1 (f2 x) *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/syntax/types_functions2.mli b/test/syntax/types_functions2.mli index b5a8d7d6..656fa8a6 100644 --- a/test/syntax/types_functions2.mli +++ b/test/syntax/types_functions2.mli @@ -30,7 +30,3 @@ type ('a, 'b) t7 = 'a t6 match x with | {x;y} -> {x;y} *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/utils/testchecker.ml b/test/utils/testchecker.ml index e3d4cd2f..92ac2878 100644 --- a/test/utils/testchecker.ml +++ b/test/utils/testchecker.ml @@ -15,19 +15,14 @@ let print ppf file = aux ~first:true (); close_in ch -let print_and_delete ppf file = - let s = print ppf file in - Sys.remove file; - s - let test_file file = - let stdout = str "%s_stdout" file in let stderr = str "%s_stderr" file in - let command = str "gospel check %s > %s 2> %s" file stdout stderr in + let command = str "gospel check %s > %s 2> %s" file Filename.null stderr in let status = Sys.command command in - let output = if status = 0 then stdout else stderr in - pr "%a@\n(* @[{gospel_expected|@\n[%d] @[%a@]@\n|gospel_expected}@] *)@\n" - print file status print_and_delete output + pr "%a@\n" print file; + if status <> 0 then + pr "(* @[{gospel_expected|@\n[%d] @[%a@]@\n|gospel_expected}@] *)@\n" status + print stderr let () = let file = Sys.argv.(1) in diff --git a/test/vocal/Arrays.mli b/test/vocal/Arrays.mli index 199c1189..4291bbe6 100644 --- a/test/vocal/Arrays.mli +++ b/test/vocal/Arrays.mli @@ -73,7 +73,3 @@ val knuth_shuffle : 'a array -> unit (*@ knuth_shuffle a modifies a ensures Array.permut (old a) a *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/vocal/CountingSort.mli b/test/vocal/CountingSort.mli index 223c332b..3650081b 100644 --- a/test/vocal/CountingSort.mli +++ b/test/vocal/CountingSort.mli @@ -30,7 +30,3 @@ val in_place_counting_sort : int -> int array -> unit modifies a ensures sorted a ensures Array.permut (old a) a *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/vocal/FM19.mli b/test/vocal/FM19.mli index b484283f..f5c14636 100644 --- a/test/vocal/FM19.mli +++ b/test/vocal/FM19.mli @@ -110,7 +110,3 @@ val f : tt -> tt -> tt -> tt -> int -> tt * tt * int requires true (* P in the paper *) modifies p1, p2.left consumes p3 ensures true (* Q in the paper *) *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/vocal/HashTable.mli b/test/vocal/HashTable.mli index 94e08cc1..bcb99cab 100644 --- a/test/vocal/HashTable.mli +++ b/test/vocal/HashTable.mli @@ -115,7 +115,3 @@ module Make (K : HashedType) : sig (*@ b = mem h k ensures b <-> h.view k <> [] *) end - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/vocal/Lists.mli b/test/vocal/Lists.mli index e6095ad4..faa877c7 100644 --- a/test/vocal/Lists.mli +++ b/test/vocal/Lists.mli @@ -24,7 +24,3 @@ val map : ('a -> 'b) -> 'a list -> 'b list ensures forall i. 0 <= i < List.length l -> List.nth r i = f (List.nth l i) equivalent "List.rev (List.map f (List.rev l))" *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/vocal/Mjrty.mli b/test/vocal/Mjrty.mli index 2c41185d..14579396 100644 --- a/test/vocal/Mjrty.mli +++ b/test/vocal/Mjrty.mli @@ -26,7 +26,3 @@ val mjrty : string array -> string ensures 2 * num a r 0 (Array.length a) > Array.length a raises Not_found -> forall c. 2 * num a c 0 (Array.length a) <= Array.length a *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/vocal/PairingHeap.mli b/test/vocal/PairingHeap.mli index 355e32f9..212b3bc3 100644 --- a/test/vocal/PairingHeap.mli +++ b/test/vocal/PairingHeap.mli @@ -63,7 +63,3 @@ end) : sig ensures forall y. y <> minimum h -> Bag.occurrences y h'.bag = Bag.occurrences y h.bag ensures Bag.cardinal h'.bag = Bag.cardinal h.bag - 1 *) end - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/vocal/PriorityQueue.mli b/test/vocal/PriorityQueue.mli index 1ce8f485..d755c1c4 100644 --- a/test/vocal/PriorityQueue.mli +++ b/test/vocal/PriorityQueue.mli @@ -84,7 +84,3 @@ end) : sig modifies h ensures h.bag = Bag.add x (old h).bag *) end - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/vocal/Queue.mli b/test/vocal/Queue.mli index 6f81d9df..dcfeadff 100644 --- a/test/vocal/Queue.mli +++ b/test/vocal/Queue.mli @@ -41,7 +41,3 @@ val transfer : 'a t -> 'a t -> unit modifies q1.view, q2.view ensures q1.view = Sequence.empty ensures q2.view = old q2.view ++ old q1.view *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/vocal/RingBuffer.mli b/test/vocal/RingBuffer.mli index 3edff5e4..532fb727 100644 --- a/test/vocal/RingBuffer.mli +++ b/test/vocal/RingBuffer.mli @@ -62,7 +62,3 @@ val copy : 'a buffer -> 'a buffer ensures b.capacity = r.capacity ensures forall i. 0 <= i < length r.sequence -> b.sequence[i] = r.sequence[i] *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/vocal/UnionFind.mli b/test/vocal/UnionFind.mli index dab0ce82..edd4eb7a 100644 --- a/test/vocal/UnionFind.mli +++ b/test/vocal/UnionFind.mli @@ -121,7 +121,3 @@ val union : 'a elem -> 'a elem -> unit uf1.img x = if mem x (old uf1.dom) then old (uf1.img x) else old (uf2.img x) *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/vocal/Vector.mli b/test/vocal/Vector.mli index 6974ad0c..93c6ea64 100644 --- a/test/vocal/Vector.mli +++ b/test/vocal/Vector.mli @@ -330,7 +330,3 @@ val unsafe_resize: 'a t -> int -> unit val unsafe_get : 'a t -> int -> 'a val unsafe_set : 'a t -> int -> 'a -> unit *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *) diff --git a/test/vocal/ZipperList.mli b/test/vocal/ZipperList.mli index 88b78fac..ef924420 100644 --- a/test/vocal/ZipperList.mli +++ b/test/vocal/ZipperList.mli @@ -92,7 +92,3 @@ val focused : 'a t -> 'a option ensures match r with | None -> z.idx = Sequence.length z.seq | Some x -> z.idx < Sequence.length z.seq /\ x = z.seq[z.idx] *) - -(* {gospel_expected| - [0] OK - |gospel_expected} *)