Merge pull request #374 from n-osborne/invariant-bis

Propagate non-optional name to typed ast

CHANGES.md

@@ -9,7 +9,8 @@
 ## Improved
 
 - Make the `with` necessary when declaring type invariants
-  [\#372](https://github.com/ocaml-gospel/gospel/pull/372)
+  [\#372](https://github.com/ocaml-gospel/gospel/pull/372) and
+  [\#374](https://github.com/ocaml-gospel/gospel/pull/374)
 
 ## Internals
 

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,21 +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) 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 =
-    match spec.ty_invariant with
-    | None -> []
-    | Some (_, xs) -> List.map (fmla Invariant kid crcm ns env) xs
-  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 kid crcm ns r tdl =

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