From 036322903bc40f9b06120c6adafd4afe67429f48 Mon Sep 17 00:00:00 2001
From: ProgramSnail <purpurebacterium@yandex.ru>
Date: Sun, 15 Mar 2026 12:26:47 +0000
Subject: [PATCH] model description fixes & additions, correct  memoisation in
 synthesizer (rec test passed)

---
 simplest_model_with_mods/model.typ      | 15 ++++++++++++-
 simplest_model_with_mods/synthesizer.ml | 30 ++++++++++++++++++++-----
 simplest_model_with_mods/tests.ml       |  4 +---
 3 files changed, 39 insertions(+), 10 deletions(-)

diff --git a/simplest_model_with_mods/model.typ b/simplest_model_with_mods/model.typ
index 4ae222e..8f8167d 100644
--- a/simplest_model_with_mods/model.typ
+++ b/simplest_model_with_mods/model.typ
@@ -9,6 +9,19 @@
 
 *TODO: проблемы с добавлением if в будущем: как записать write and not write ?*
 
+Нужно будет добавить во write-flag модальности: `not write` | `may write` | `always write`
+
+Добавление condition-исполнения - выбор из нескольких блоков. Варианты:
+- & of | of & -вложенные блоки ?
+- добавить несколько альтернативны тел функциям. Но тогда придётся при трансляции if-блоки выносить в функции
+
+Лямбды - нужно тоже будет как-то находить лямбды и ля них тоже синтезировать атрибуты
+вызов лямбд будет нужен в модели?
+- lambda-аргумент - вложенные теги?, должна быть одна и та же сигнтура
+можно ввести отдельные сигнатуры-определения?
+
+проблема простой семантики: вызов лямбд: могут быть модифицируемые функции
+
 == Синтаксис
 
 #h(10pt)
@@ -146,7 +159,7 @@ $d space @ space overline(x)$ - запись применения функции
     name: [ is correct],
     $isOut tag -> isWrite tag$, // NOTE; strong requirment should write
     $isRead tag -> isIn tag$,
-    $isWrite tag -> isWrite sigma(x)$, // NOTE: may tag => should sigma(x)
+    $isWrite tag and (isOut tag or not isCopy tag) -> isWrite sigma(x)$, // NOTE: may tag => should sigma(x)
     $isRead tag -> mu (sigma(x)) != bot$, // NOTE: may tag -> ... 
 
     $isCorrect_(cl sigma, mu cr) (tag, x)$,
diff --git a/simplest_model_with_mods/synthesizer.ml b/simplest_model_with_mods/synthesizer.ml
index 93c8c46..3c013ec 100644
--- a/simplest_model_with_mods/synthesizer.ml
+++ b/simplest_model_with_mods/synthesizer.ml
@@ -520,6 +520,14 @@ struct
         list_dropo n' ys xs' }
   }
 
+  let rec list_not_membero xs x = ocanren {
+    xs == [] |
+    { fresh x', xs' in
+        xs == x' :: xs' &
+        x' =/= x &
+        list_not_membero xs' x }
+  }
+
   let visited_checko state f_id =
     let open St in
     ocanren {
@@ -528,8 +536,13 @@ struct
       List.membero visited f_id
     }
 
-  (* TODO *)
-  (* let visited_not_checko state f_id = ??? *)
+  let not_visited_checko state f_id =
+    let open St in
+    ocanren {
+      fresh _env, _mem, _mem_len, visited in
+      state == St (_env, _mem, _mem_len, visited) &
+      list_not_membero visited f_id
+    }
 
   let visited_addo state f_id state' =
     let open St in
@@ -546,16 +559,21 @@ struct
     let open FunDecl in
     let open Tag in
     ocanren {
-    { fresh f_id, args, f, args', state_after_call, state_with_visited, arg_tags, _body in
+    { fresh f_id, args, f, args', state_after_call, arg_tags, _body in
       stmt == Call (f_id, args) &
       list_ntho prog f_id f &
       FunDecl (arg_tags, _body) == f &
       List.mapo arg_to_lvalueo args args' &
       (* TODO: FIXME: memoisation, do not do calls on check successfull *)
-      eval_funo state prog f args' state_after_call &
+      
       (* NOTE: tmp simplification for less branching (TODO?) *)
-      visited_addo state_after_call f_id state_with_visited &
-      st_spoil_by_argso state_with_visited arg_tags args state' } |
+      { { fresh state_with_visited in
+          not_visited_checko state f_id &
+          visited_addo state f_id state_with_visited &
+          eval_funo state_with_visited prog f args' state_after_call } |
+        { visited_checko state f_id &
+          state_after_call == state } } &
+      st_spoil_by_argso state_after_call arg_tags args state' } |
     { fresh id in stmt == Read id & mem_checko state id & state == state' } |
     { fresh id, tag, _mem_id in
       stmt == Write id &
diff --git a/simplest_model_with_mods/tests.ml b/simplest_model_with_mods/tests.ml
index 02660db..b12c028 100644
--- a/simplest_model_with_mods/tests.ml
+++ b/simplest_model_with_mods/tests.ml
@@ -57,7 +57,5 @@ let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[V
 let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Val]; [Val; Ref]] |}]
 let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}]
 
-(* TODO: FIXME: implement memoization cuts *)
-(* NOTE: inf test in current model (without additional functional interfaces and ) *)
-(* let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [])] |}] *)
+let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [O])] |}]