From 167a983a32145121f4d80f86c2d93e20ec824cc7 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Tue, 16 Jan 2024 11:02:00 +0100
Subject: [PATCH] update to latest gospel (#194)

* Add a pin to last version of gospel

Representation of type invariants were modified.

* Update ortac wrapper to new gospel
---
 ortac-wrapper.opam                  |  3 +++
 ortac-wrapper.opam.template         |  3 +++
 plugins/wrapper/src/ir_of_gospel.ml | 24 +++++++++++++-----------
 3 files changed, 19 insertions(+), 11 deletions(-)
 create mode 100644 ortac-wrapper.opam.template

diff --git a/ortac-wrapper.opam b/ortac-wrapper.opam
index 557c78b7..88241651 100644
--- a/ortac-wrapper.opam
+++ b/ortac-wrapper.opam
@@ -46,3 +46,6 @@ build: [
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git+https://github.com/ocaml-gospel/ortac.git"
+pin-depends: [
+  [ "gospel.0.2.0+dev" "git+https://github.com/ocaml-gospel/gospel#044f1d5b1f6eba47ee9ad001a5ce1dcb3b49c03a" ]
+]
diff --git a/ortac-wrapper.opam.template b/ortac-wrapper.opam.template
new file mode 100644
index 00000000..465b4535
--- /dev/null
+++ b/ortac-wrapper.opam.template
@@ -0,0 +1,3 @@
+pin-depends: [
+  [ "gospel.0.2.0+dev" "git+https://github.com/ocaml-gospel/gospel#044f1d5b1f6eba47ee9ad001a5ce1dcb3b49c03a" ]
+]
diff --git a/plugins/wrapper/src/ir_of_gospel.ml b/plugins/wrapper/src/ir_of_gospel.ml
index 63a6b21b..2eae4bec 100644
--- a/plugins/wrapper/src/ir_of_gospel.ml
+++ b/plugins/wrapper/src/ir_of_gospel.ml
@@ -95,16 +95,15 @@ let subst_invariant_fields var (t : Tterm.term) =
 
 let invariant ~context ~term_printer self (invariant : Tterm.term) =
   let function_name = gen_symbol ~prefix:"__invariant_" () in
-  let instance_id =
-    match self with
-    | None -> Ident.create ~loc (gen_symbol ~prefix:"__self_" ())
-    | Some self -> self.Symbols.vs_name
+  let instance_arg =
+    (Nolabel, pvar (Fmt.str "%a" Ident.pp self.Symbols.vs_name))
   in
-  let instance_arg = (Nolabel, pvar (Fmt.str "%a" Ident.pp instance_id)) in
   let instance_term =
     (* XXX This is not the correct type or location, but it doesn't matter for
        the translation *)
-    Tterm_helper.t_var { vs_name = instance_id; vs_ty = Ttypes.ty_unit } loc
+    Tterm_helper.t_var
+      { vs_name = self.Symbols.vs_name; vs_ty = Ttypes.ty_unit }
+      loc
   in
 
   let register_name = gen_symbol ~prefix:"__error_" () in
@@ -131,11 +130,14 @@ let invariant ~context ~term_printer self (invariant : Tterm.term) =
   in
   { txt; loc; translation }
 
-let with_invariants ~context ~term_printer (self, invariants) (type_ : type_) =
-  let invariants =
-    List.map (invariant ~context ~term_printer self) invariants
-  in
-  { type_ with invariants }
+let with_invariants ~context ~term_printer invariants (type_ : type_) =
+  Option.fold ~none:type_
+    ~some:(fun (self, invariants) ->
+      let invariants =
+        List.map (invariant ~context ~term_printer self) invariants
+      in
+      { type_ with invariants })
+    invariants
 
 let with_consumes consumes (value : value) =
   let name (t : Tterm.term) =