Skip to content

Commit

Permalink
update to latest gospel (#194)
Browse files Browse the repository at this point in the history
* Add a pin to last version of gospel

Representation of type invariants were modified.

* Update ortac wrapper to new gospel
  • Loading branch information
n-osborne authored Jan 16, 2024
1 parent 5f6756a commit 167a983
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 11 deletions.
3 changes: 3 additions & 0 deletions ortac-wrapper.opam
Original file line number Diff line number Diff line change
Expand Up @@ -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" ]
]
3 changes: 3 additions & 0 deletions ortac-wrapper.opam.template
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
pin-depends: [
[ "gospel.0.2.0+dev" "git+https://github.com/ocaml-gospel/gospel#044f1d5b1f6eba47ee9ad001a5ce1dcb3b49c03a" ]
]
24 changes: 13 additions & 11 deletions plugins/wrapper/src/ir_of_gospel.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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) =
Expand Down

0 comments on commit 167a983

Please sign in to comment.