From da61d16ee1a038fef969dd5e4f2ab1ced11980f0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 18 Oct 2023 13:04:45 +0200
Subject: [PATCH] wip

---
 library/summary.ml | 104 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 104 insertions(+)

diff --git a/library/summary.ml b/library/summary.ml
index 17296e87c6fb7..96b399ad21807 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -227,3 +227,107 @@ let (:=) = (:=)
 end
 
 let dump = Dyn.dump
+
+module type S = sig
+
+(* this is a simple declaration but we also need something for goptions
+   goptions modifies a predeclared state (for instance Global.env) *)
+type ('frozen, 'state) decl = {
+  freeze : 'state -> 'frozen;
+  unfreeze : 'frozen -> 'state;
+  init : 'state;
+  idfreeze : ('frozen, 'state) Util.eq option; (* optim *)
+}
+
+(* we can also use covariant, readwrite = RW, read = RW|R, nothing = RW|R|Nothing
+   but the errors are worse IMO
+
+   or we make it invariant and use explicit cast functions? could get heavy
+*)
+type (-'synterp_rw, -'interp_rw) state
+
+type nothing = [`Nothing]
+
+type read = [`R|`Nothing]
+
+type readwrite = [`RW|`R|`Nothing]
+
+
+type 'v declared_synterp = {
+  sread : 'syn 'interp. ([>read] as 'syn, 'interp) state -> 'v;
+  swrite : 'interp. (readwrite, 'interp) state -> 'v -> unit;
+}
+
+type 'v declared_interp = {
+  read : 'syn 'interp. ('syn, [>read] as 'interp) state -> 'v;
+  write : 'syn. ('syn, readwrite) state -> 'v -> unit;
+}
+
+val decl_synterp : string -> ?make_marshallable:('frozen -> 'frozen) ->
+  ('frozen, 'state) decl ->
+  'state declared_synterp
+
+val decl_interp : string -> ?make_marshallable:('frozen -> 'frozen) ->
+  ('frozen, 'state) decl ->
+  'state declared_interp
+end
+
+module Test (S : S) = struct
+  open S
+
+  let { sread = read_nota; swrite = set_nota } = decl_synterp "nota"
+      { freeze = (fun x -> x);
+        unfreeze = (fun x -> x);
+        init = 0;
+        idfreeze = None }
+
+  let { read = read_env; write = set_env } = decl_interp "env"
+      { freeze = (fun x -> x);
+        unfreeze = (fun x -> x);
+        init = 0;
+        idfreeze = None }
+
+  type synterp_r = (read, nothing) state
+  type synterp_rw = (readwrite, nothing) state
+  type interp_r = (read, read) state
+  type interp_rw = (read, readwrite) state
+
+  let synterp_drop_w (s:synterp_rw) = (s:>synterp_r)
+
+  let drop_interp (s:(read,[>nothing]) state) = (s:>synterp_r)
+
+  let drop_interp_r (s:interp_r) = drop_interp s
+
+  let drop_interp_rw (s:interp_rw) = drop_interp s
+
+  let not_allowed_nothing (s:(nothing,nothing) state) =
+    read_nota (s:>synterp_r) (* error read is not a subtype of nothing: nothing does not allow R *)
+
+  let not_allowed_synterp_and_interp (s:interp_rw) =
+    let s = set_env s 0 in
+    let s = set_nota s 1 in
+    (* error         ^
+This expression has type (S.read, S.readwrite) S.state
+but an expression was expected of type (S.readwrite, S.nothing) S.state
+Type S.read = [ `Nothing | `R ] is not compatible with type
+  S.readwrite = [ `Nothing | `R | `RW ]
+The first variant type does not allow tag(s) `RW
+    *)
+    s
+
+  let just_get (s:interp_r) = read_env s
+
+  let get_then_set (s:interp_rw) =
+    let x = read_env s in
+    set_env s (x+1)
+
+  let set_then_get s =
+    let () = set_env s 2 in
+    read_env s
+
+  (* ends up as ('a, readwrite) state -> unit *)
+  let get_then_set_unnanotated s =
+    let x = read_env s in
+    set_env s (x+1)
+
+end