From 68f2569922986334894d303b68b9b93d6db6db31 Mon Sep 17 00:00:00 2001
From: ProgramSnail <purpurebacterium@yandex.ru>
Date: Fri, 8 May 2026 12:46:53 +0000
Subject: [PATCH] struct: synt. ambuity fixes, simple read call test

---
 model_with_structures/synthesizer.ml | 18 +++++++++++-------
 model_with_structures/tests.ml       |  2 +-
 2 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml
index 6c50ed9..b100a82 100644
--- a/model_with_structures/synthesizer.ml
+++ b/model_with_structures/synthesizer.ml
@@ -686,12 +686,12 @@ struct
     let open Mode in
     let open CopyCap in
     ocanren {
-      { r == NRd | v == ZeroV } &
-      { r == NRd | is_ino m } &
-      { is_not_outo m | w == AlwaysWr } &
+      { r == NRd | r == Rd & v == ZeroV } &
+      { r == NRd | r == Rd & is_ino m } &
+      { is_not_outo m | is_outo m & w == AlwaysWr } &
       { w == NeverWr |
-        { is_not_outo m & c == Cp } |
-        w' == AlwaysWr } &
+        w =/= NeverWr & w' =/= AlwaysWr & is_not_outo m & c == Cp |
+        w =/= NeverWr & w' == AlwaysWr } &
       is_trivial_vo v
   }
 
@@ -721,8 +721,12 @@ struct
           { is_outo m &
             w == AlwaysWr &
             mem_with_v' == Std.pair mem ZeroV } |
-          { { is_outo m | c == Cp | w == NeverWr } &
-            { is_not_outo m | w == MayWr | w == NeverWr } &
+          { { is_outo m |
+              is_not_outo m & c == Cp |
+              is_not_outo m & c == Rf & w == NeverWr } &
+            { is_not_outo m |
+              is_outo m & w == MayWr |
+              is_outo m & w == NeverWr } &
             mem_with_v' == Std.pair mem v }
         } } |
       { fresh ts, us, _stmts in
diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml
index 14d1bd0..f82b186 100644
--- a/model_with_structures/tests.ml
+++ b/model_with_structures/tests.ml
@@ -22,7 +22,7 @@ let%expect_test "simple var, write & read" = print_endline(prog_eval_t_simple_va
   (* - basic call tests *)
 
 let%expect_test "simple call with read" = print_endline(prog_eval_t_simple_call_rd ());
-  [%expect {| [123] |}]
+  [%expect {| [StEnv (MemEnv ([FunV ([ReadS (VarP (O))]); ZeroV], S (S (O))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), UnitT (Rd, NeverWr))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, NeverWr))], [(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), UnitT (Rd, NeverWr))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, NeverWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
 
 (* type tests *)
 (* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *)