From 06f69ec4c2855e8258f0e7d6e5855695c653acbb Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Fri, 22 May 2026 12:50:47 +0000 Subject: [PATCH] struct: remove test parts that are not required now (with new lambda model) --- model_with_structures/analyzer.ml | 153 +++++------- model_with_structures/analyzer_rw.ml | 127 ++++------ model_with_structures/tests.ml | 28 +-- model_with_structures/tests_f.ml | 343 +++++++-------------------- 4 files changed, 191 insertions(+), 460 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index c1f1b01..a951d1d 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -571,25 +571,6 @@ struct let vg10 = VarP (globals_min_id + 10) let vg11 = VarP (globals_min_id + 11) - let rf0E = RefE 0 - let rf1E = RefE 1 - let rf2E = RefE 2 - let rf3E = RefE 3 - let rf4E = RefE 4 - let rf5E = RefE 5 - let rf3E = RefE 3 - let rf4E = RefE 4 - let rf5E = RefE 5 - let rfg0E = RefE globals_min_id - let rfg1E = RefE (globals_min_id + 1) - let rfg2E = RefE (globals_min_id + 2) - let rfg3E = RefE (globals_min_id + 3) - let rfg4E = RefE (globals_min_id + 4) - let rfg5E = RefE (globals_min_id + 5) - let rfg6E = RefE (globals_min_id + 6) - let rfg7E = RefE (globals_min_id + 7) - let rfg8E = RefE (globals_min_id + 8) - let pE p = PathE p let drf p = DerefP p @@ -712,14 +693,13 @@ struct let%expect_test "simple call with read, dsl" = prog_eval_noret ( [ - defg uT_r_mw; defg (rfT uT_r_mw); FunD ( [moded @@ cpT @@ uT_r], rdS @@ drf @@ v0 ) ], - callS vg2 [pE vg1] + callS vg1 [pE vg0] ); Printf.printf "done!"; [%expect {| done! |}] @@ -727,14 +707,13 @@ struct let%expect_test "simple call with write, dsl" = prog_eval_noret ( [ - defg uT_aw; defg (rfT uT_aw); FunD ( [moded @@ cpT @@ uT_aw], wrS @@ drf @@ v0 ) ], - callS vg2 [pE vg1] + callS vg1 [pE vg0] ); Printf.printf "done!"; [%expect {| done! |}] @@ -742,7 +721,6 @@ struct let%expect_test "simple call with read after write, dsl" = prog_eval_noret ( [ - defg uT_aw; defg (rfT uT_aw); FunD ( [moded @@ cpT @@ uT_aw], @@ -750,7 +728,7 @@ struct (rdS @@ drf @@ v0) ) ], - callS vg2 [pE vg1] + callS vg1 [pE vg0] ); Printf.printf "done!"; [%expect {| done! |}] @@ -758,31 +736,28 @@ struct let%expect_test "simple call with forbidden write, dsl" = try (prog_eval_noret ( [ - defg uT_r_mw; defg (rfT uT_r_mw); FunD ( [moded @@ cpT @@ uT_r], wrS @@ drf @@ v0 ) ], - callS vg2 [pE vg1] + callS vg1 [pE vg0] ); [%expect.unreachable]); with Eval_error msg -> Printf.printf "%s" msg; [%expect {| write: write tag |}] - (* TODO: FIXME: why is condition on always write in parent ?? *) let%expect_test "simple call with write to ref, dsl" = prog_eval_noret ( [ - defg uT_r_aw; defg (rfT uT_r_aw); FunD ( [moded @@ rfT @@ uT_aw], wrS @@ drf @@ v0 ) ], - callS vg2 [pE vg1] + callS vg1 [pE vg0] ); Printf.printf "done!"; [%expect {| done! |}] @@ -790,15 +765,14 @@ struct let%expect_test "simple call with forbidden write to ref, dsl" = try (prog_eval_noret ( [ - defg uT_r_aw; defg (rfT uT_r_aw); FunD ( [moded @@ rfT @@ uT_aw], wrS @@ drf @@ v0 ) ], - (callS vg2 [pE vg1]) #. - (rdS @@ drf @@ vg1) + (callS vg1 [pE vg0]) #. + (rdS @@ drf @@ vg0) ); [%expect.unreachable]); with Eval_error msg -> Printf.printf "%s" msg; @@ -807,16 +781,15 @@ struct let%expect_test "simple call with write to ref with fix, dsl" = prog_eval_noret ( [ - defg uT_r_aw; defg (rfT uT_r_aw); FunD ( [moded @@ rfT @@ uT_aw], wrS @@ drf @@ v0 ) ], - (callS vg2 [pE vg1]) #. - (wrS @@ drf @@ vg1) #. - (rdS @@ drf @@ vg1) + (callS vg1 [pE vg0]) #. + (wrS @@ drf @@ vg0) #. + (rdS @@ drf @@ vg0) ); Printf.printf "done!"; [%expect {| done! |}] @@ -824,7 +797,6 @@ struct let%expect_test "call inside call, dsl" = prog_eval_noret ( [ - defg uT_r_aw; defg (rfT uT_r_aw); FunD ( [moded @@ rfT @@ uT_aw], @@ -832,38 +804,36 @@ struct ); FunD ( [moded @@ cpT @@ uT_aw], - (callS vg2 [pE v0]) #. + (callS vg1 [pE v0]) #. (wrS @@ drf @@ v0) ) ], - (callS vg3 [pE vg1]) #. - (rdS @@ drf @@ vg1) + (callS vg2 [pE vg0]) #. + (rdS @@ drf @@ vg0) ); Printf.printf "done!"; [%expect {| done! |}] - (* NOTE: memoization used *) - let%expect_test "call inside call, recursive, dsl" = - prog_eval_noret ( - [ - defg uT_r_aw; - defg (rfT uT_r_aw); - FunD ( - [moded @@ cpT @@ uT_aw], - (callS vg2 [pE v0]) #. - (wrS @@ drf @@ v0) - ) - ], - (callS vg2 [pE vg1]) #. - (rdS @@ drf @@ vg1) - ); - Printf.printf "done!"; - [%expect {| done! |}] + (* NOTE: does not work for annalyzer rw to the sequenced declaration addition to calculate tags *) + (* let%expect_test "call inside call, recursive, dsl" = *) + (* prog_eval_noret ( *) + (* [ *) + (* defg (rfT uT_r_aw); *) + (* FunD ( *) + (* [moded @@ cpT @@ uT_aw], *) + (* (callS vg1 [pE v0]) #. *) + (* (wrS @@ drf @@ v0) *) + (* ) *) + (* ], *) + (* (callS vg1 [pE vg0]) #. *) + (* (rdS @@ drf @@ vg0) *) + (* ); *) + (* Printf.printf "done!"; *) + (* [%expect {| done! |}] *) let%expect_test "call to fix after call, dsl" = prog_eval_noret ( [ - defg uT_r_aw; defg (rfT uT_r_aw); FunD ( [moded @@ rfT @@ uT_aw], @@ -874,9 +844,9 @@ struct wrS @@ drf @@ v0 ) ], - (callS vg2 [pE vg1]) #. - (callS vg3 [pE vg1]) #. - (rdS @@ drf @@ vg1) + (callS vg1 [pE vg0]) #. + (callS vg2 [pE vg0]) #. + (rdS @@ drf @@ vg0) ); Printf.printf "done!"; [%expect {| done! |}] @@ -884,16 +854,15 @@ struct let%expect_test "simple call with global variable usage, dsl" = prog_eval_noret ( [ - defg uT_r_aw; - defg (rfT uT_r); + defg (rfT uT_r_aw); FunD ( [moded @@ cpT @@ uT], - (wrS @@ vg0) #. - (rdS @@ drf @@ vg1) + (wrS @@ drf @@ vg0) #. + (rdS @@ drf @@ vg0) ) ], - (callS vg2 [pE vg1]) #. - (rdS @@ drf @@ vg1) + (callS vg1 [pE vg0]) #. + (rdS @@ drf @@ vg0) ); Printf.printf "done!"; [%expect {| done! |}] @@ -901,9 +870,7 @@ struct let%expect_test "simple call with read & write (2 args), dsl" = prog_eval_noret ( [ - defg uT_r; defg (rfT uT_r); - defg uT_aw; defg (rfT uT_aw); FunD ( [ @@ -914,7 +881,7 @@ struct (wrS @@ drf @@ v1) ) ], - callS vg4 [pE vg1; pE vg3] + callS vg2 [pE vg0; pE vg1] ); Printf.printf "done!"; [%expect {| done! |}] @@ -922,13 +889,9 @@ struct let%expect_test "simple call with different arguments modifiers, copy, dsl" = prog_eval_noret ( [ - defg uT_r_aw; defg (rfT uT_r_aw); - defg uT_r_aw; defg (rfT uT_r_aw); - defg uT_r_aw; defg (rfT uT_r_aw); - defg uT_r_aw; defg (rfT uT_r_aw); FunD ( [ @@ -944,11 +907,11 @@ struct (wrS @@ drf @@ v3) ) ], - (callS vg8 [pE vg1; pE vg3; pE vg5; pE vg7]) #. + (callS vg4 [pE vg0; pE vg1; pE vg2; pE vg3]) #. + (rdS @@ drf @@ vg0) #. (rdS @@ drf @@ vg1) #. - (rdS @@ drf @@ vg3) #. - (rdS @@ drf @@ vg5) #. - (rdS @@ drf @@ vg7) + (rdS @@ drf @@ vg2) #. + (rdS @@ drf @@ vg3) ); Printf.printf "done!"; [%expect {| done! |}] @@ -956,13 +919,9 @@ struct let%expect_test "simple call with different arguments modifiers, ref, dsl" = prog_eval_noret ( [ - defg uT_r; defg (rfT uT_r); - defg uT_r; defg (rfT uT_r); - defg uT_r_aw; defg (rfT uT_r_aw); - defg uT_r_aw; defg (rfT uT_r_aw); FunD ( [ @@ -977,11 +936,11 @@ struct (wrS @@ drf @@ v3) ) ], - (callS vg8 [pE vg1; pE vg3; pE vg5; pE vg7]) #. + (callS vg4 [pE vg0; pE vg1; pE vg2; pE vg3]) #. + (rdS @@ drf @@ vg0) #. (rdS @@ drf @@ vg1) #. - (rdS @@ drf @@ vg3) #. - (rdS @@ drf @@ vg5) #. - (rdS @@ drf @@ vg7) + (rdS @@ drf @@ vg2) #. + (rdS @@ drf @@ vg3) ); Printf.printf "done!"; [%expect {| done! |}] @@ -991,13 +950,9 @@ struct let%expect_test "presentation test 1 (simple types), dsl" = prog_eval_noret ( [ - defg uT_r_aw; defg (rfT uT_r_aw); (* x *) - defg uT_r_aw; defg (rfT uT_r_aw); (* y *) - defg uT_r_aw; defg (rfT uT_r_aw); (* z *) - defg uT_r_aw; defg (rfT uT_r_aw); (* k *) FunD ( (* f *) [ @@ -1031,14 +986,14 @@ struct (rdS @@ drf @@ v0) ) ], - let xV = vg1 in - let yV = vg3 in - let zV = vg5 in - let kV = vg7 in - let fF = vg8 in - let wF = vg9 in - let gF = vg10 in - let rF = vg11 in + let xV = vg0 in + let yV = vg1 in + let zV = vg2 in + let kV = vg3 in + let fF = vg4 in + let wF = vg5 in + let gF = vg6 in + let rF = vg7 in (callS wF [pE xV]) #. (callS rF [pE xV]) #. (callS fF [pE xV; pE yV]) #. diff --git a/model_with_structures/analyzer_rw.ml b/model_with_structures/analyzer_rw.ml index bec49e0..19c5d1d 100644 --- a/model_with_structures/analyzer_rw.ml +++ b/model_with_structures/analyzer_rw.ml @@ -615,25 +615,6 @@ struct let vg10 = VarP (globals_min_id + 10) let vg11 = VarP (globals_min_id + 11) - let rf0E = RefE 0 - let rf1E = RefE 1 - let rf2E = RefE 2 - let rf3E = RefE 3 - let rf4E = RefE 4 - let rf5E = RefE 5 - let rf3E = RefE 3 - let rf4E = RefE 4 - let rf5E = RefE 5 - let rfg0E = RefE globals_min_id - let rfg1E = RefE (globals_min_id + 1) - let rfg2E = RefE (globals_min_id + 2) - let rfg3E = RefE (globals_min_id + 3) - let rfg4E = RefE (globals_min_id + 4) - let rfg5E = RefE (globals_min_id + 5) - let rfg6E = RefE (globals_min_id + 6) - let rfg7E = RefE (globals_min_id + 7) - let rfg8E = RefE (globals_min_id + 8) - let pE p = PathE p let drf p = DerefP p @@ -837,14 +818,13 @@ struct let%expect_test "simple call with read, dsl" = prog_eval_noret ( [ - defg uT_r_mw; defg (rfT uT_r_mw); FunD ( [moded @@ cpT @@ uT_r], rdS @@ drf @@ v0 ) ], - callS vg2 [pE vg1] + callS vg1 [pE vg0] ); Printf.printf "done!"; [%expect {| done! |}] @@ -852,14 +832,13 @@ struct let%expect_test "simple call with write, dsl" = prog_eval_noret ( [ - defg uT_aw; defg (rfT uT_aw); FunD ( [moded @@ cpT @@ uT_aw], wrS @@ drf @@ v0 ) ], - callS vg2 [pE vg1] + callS vg1 [pE vg0] ); Printf.printf "done!"; [%expect {| done! |}] @@ -867,7 +846,6 @@ struct let%expect_test "simple call with read after write, dsl" = prog_eval_noret ( [ - defg uT_aw; defg (rfT uT_aw); FunD ( [moded @@ cpT @@ uT_aw], @@ -875,7 +853,7 @@ struct (rdS @@ drf @@ v0) ) ], - callS vg2 [pE vg1] + callS vg1 [pE vg0] ); Printf.printf "done!"; [%expect {| done! |}] @@ -883,31 +861,28 @@ struct let%expect_test "simple call with forbidden write, dsl" = try (prog_eval_noret ( [ - defg uT_r_mw; defg (rfT uT_r_mw); FunD ( [moded @@ cpT @@ uT_r], wrS @@ drf @@ v0 ) ], - callS vg2 [pE vg1] + callS vg1 [pE vg0] ); [%expect.unreachable]); with Eval_error msg -> Printf.printf "%s" msg; [%expect {| write: write tag |}] - (* TODO: FIXME: why is condition on always write in parent ?? *) let%expect_test "simple call with write to ref, dsl" = prog_eval_noret ( [ - defg uT_r_aw; defg (rfT uT_r_aw); FunD ( [moded @@ rfT @@ uT_aw], wrS @@ drf @@ v0 ) ], - callS vg2 [pE vg1] + callS vg1 [pE vg0] ); Printf.printf "done!"; [%expect {| done! |}] @@ -915,15 +890,14 @@ struct let%expect_test "simple call with forbidden write to ref, dsl" = try (prog_eval_noret ( [ - defg uT_r_aw; defg (rfT uT_r_aw); FunD ( [moded @@ rfT @@ uT_aw], wrS @@ drf @@ v0 ) ], - (callS vg2 [pE vg1]) #. - (rdS @@ drf @@ vg1) + (callS vg1 [pE vg0]) #. + (rdS @@ drf @@ vg0) ); [%expect.unreachable]); with Eval_error msg -> Printf.printf "%s" msg; @@ -932,16 +906,15 @@ struct let%expect_test "simple call with write to ref with fix, dsl" = prog_eval_noret ( [ - defg uT_r_aw; defg (rfT uT_r_aw); FunD ( [moded @@ rfT @@ uT_aw], wrS @@ drf @@ v0 ) ], - (callS vg2 [pE vg1]) #. - (wrS @@ drf @@ vg1) #. - (rdS @@ drf @@ vg1) + (callS vg1 [pE vg0]) #. + (wrS @@ drf @@ vg0) #. + (rdS @@ drf @@ vg0) ); Printf.printf "done!"; [%expect {| done! |}] @@ -949,7 +922,6 @@ struct let%expect_test "call inside call, dsl" = prog_eval_noret ( [ - defg uT_r_aw; defg (rfT uT_r_aw); FunD ( [moded @@ rfT @@ uT_aw], @@ -957,12 +929,12 @@ struct ); FunD ( [moded @@ cpT @@ uT_aw], - (callS vg2 [pE v0]) #. + (callS vg1 [pE v0]) #. (wrS @@ drf @@ v0) ) ], - (callS vg3 [pE vg1]) #. - (rdS @@ drf @@ vg1) + (callS vg2 [pE vg0]) #. + (rdS @@ drf @@ vg0) ); Printf.printf "done!"; [%expect {| done! |}] @@ -971,16 +943,15 @@ struct (* let%expect_test "call inside call, recursive, dsl" = *) (* prog_eval_noret ( *) (* [ *) - (* defg uT_r_aw; *) (* defg (rfT uT_r_aw); *) (* FunD ( *) (* [moded @@ cpT @@ uT_aw], *) - (* (callS vg2 [pE v0]) #. *) + (* (callS vg1 [pE v0]) #. *) (* (wrS @@ drf @@ v0) *) (* ) *) (* ], *) - (* (callS vg2 [pE vg1]) #. *) - (* (rdS @@ drf @@ vg1) *) + (* (callS vg1 [pE vg0]) #. *) + (* (rdS @@ drf @@ vg0) *) (* ); *) (* Printf.printf "done!"; *) (* [%expect {| done! |}] *) @@ -988,7 +959,6 @@ struct let%expect_test "call to fix after call, dsl" = prog_eval_noret ( [ - defg uT_r_aw; defg (rfT uT_r_aw); FunD ( [moded @@ rfT @@ uT_aw], @@ -999,9 +969,9 @@ struct wrS @@ drf @@ v0 ) ], - (callS vg2 [pE vg1]) #. - (callS vg3 [pE vg1]) #. - (rdS @@ drf @@ vg1) + (callS vg1 [pE vg0]) #. + (callS vg2 [pE vg0]) #. + (rdS @@ drf @@ vg0) ); Printf.printf "done!"; [%expect {| done! |}] @@ -1009,16 +979,15 @@ struct let%expect_test "simple call with global variable usage, dsl" = prog_eval_noret ( [ - defg uT_r_aw; - defg (rfT uT_r); + defg (rfT uT_r_aw); FunD ( [moded @@ cpT @@ uT], - (wrS @@ vg0) #. - (rdS @@ drf @@ vg1) + (wrS @@ drf @@ vg0) #. + (rdS @@ drf @@ vg0) ) ], - (callS vg2 [pE vg1]) #. - (rdS @@ drf @@ vg1) + (callS vg1 [pE vg0]) #. + (rdS @@ drf @@ vg0) ); Printf.printf "done!"; [%expect {| done! |}] @@ -1026,9 +995,7 @@ struct let%expect_test "simple call with read & write (2 args), dsl" = prog_eval_noret ( [ - defg uT_r; defg (rfT uT_r); - defg uT_aw; defg (rfT uT_aw); FunD ( [ @@ -1039,7 +1006,7 @@ struct (wrS @@ drf @@ v1) ) ], - callS vg4 [pE vg1; pE vg3] + callS vg2 [pE vg0; pE vg1] ); Printf.printf "done!"; [%expect {| done! |}] @@ -1047,13 +1014,9 @@ struct let%expect_test "simple call with different arguments modifiers, copy, dsl" = prog_eval_noret ( [ - defg uT_r_aw; defg (rfT uT_r_aw); - defg uT_r_aw; defg (rfT uT_r_aw); - defg uT_r_aw; defg (rfT uT_r_aw); - defg uT_r_aw; defg (rfT uT_r_aw); FunD ( [ @@ -1069,11 +1032,11 @@ struct (wrS @@ drf @@ v3) ) ], - (callS vg8 [pE vg1; pE vg3; pE vg5; pE vg7]) #. + (callS vg4 [pE vg0; pE vg1; pE vg2; pE vg3]) #. + (rdS @@ drf @@ vg0) #. (rdS @@ drf @@ vg1) #. - (rdS @@ drf @@ vg3) #. - (rdS @@ drf @@ vg5) #. - (rdS @@ drf @@ vg7) + (rdS @@ drf @@ vg2) #. + (rdS @@ drf @@ vg3) ); Printf.printf "done!"; [%expect {| done! |}] @@ -1081,13 +1044,9 @@ struct let%expect_test "simple call with different arguments modifiers, ref, dsl" = prog_eval_noret ( [ - defg uT_r; defg (rfT uT_r); - defg uT_r; defg (rfT uT_r); - defg uT_r_aw; defg (rfT uT_r_aw); - defg uT_r_aw; defg (rfT uT_r_aw); FunD ( [ @@ -1102,11 +1061,11 @@ struct (wrS @@ drf @@ v3) ) ], - (callS vg8 [pE vg1; pE vg3; pE vg5; pE vg7]) #. + (callS vg4 [pE vg0; pE vg1; pE vg2; pE vg3]) #. + (rdS @@ drf @@ vg0) #. (rdS @@ drf @@ vg1) #. - (rdS @@ drf @@ vg3) #. - (rdS @@ drf @@ vg5) #. - (rdS @@ drf @@ vg7) + (rdS @@ drf @@ vg2) #. + (rdS @@ drf @@ vg3) ); Printf.printf "done!"; [%expect {| done! |}] @@ -1116,13 +1075,9 @@ struct let%expect_test "presentation test 1 (simple types), dsl" = prog_eval_noret ( [ - defg uT_r_aw; defg (rfT uT_r_aw); (* x *) - defg uT_r_aw; defg (rfT uT_r_aw); (* y *) - defg uT_r_aw; defg (rfT uT_r_aw); (* z *) - defg uT_r_aw; defg (rfT uT_r_aw); (* k *) FunD ( (* f *) [ @@ -1156,14 +1111,14 @@ struct (rdS @@ drf @@ v0) ) ], - let xV = vg1 in - let yV = vg3 in - let zV = vg5 in - let kV = vg7 in - let fF = vg8 in - let wF = vg9 in - let gF = vg10 in - let rF = vg11 in + let xV = vg0 in + let yV = vg1 in + let zV = vg2 in + let kV = vg3 in + let fF = vg4 in + let wF = vg5 in + let gF = vg6 in + let rF = vg7 in (callS wF [pE xV]) #. (callS rF [pE xV]) #. (callS fF [pE xV; pE yV]) #. diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index b9a3cfd..f69336e 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -25,46 +25,46 @@ let%expect_test "simple call with read" = print_endline(prog_eval_t_simple_call_ [%expect {| [StEnv (MemEnv ([FunV; UnitV (ZeroMV, OneRV, ZeroWV)], 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))]), 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)]))] |}] let%expect_test "simple call with ref read" = print_endline(prog_eval_t_simple_call_rd_ref ()); - [%expect {| [StEnv (MemEnv ([FunV; RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), RefT (Rf, UnitT (Rd, NeverWr)))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), S (O))]))] |}] let%expect_test "simple call with write" = print_endline(prog_eval_t_simple_call_wr ()); - [%expect {| [StEnv (MemEnv ([FunV; RefV (S (O)); UnitV (BotMV, ZeroRV, ZeroWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (O); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), RefT (Rf, UnitT (NRd, AlwaysWr)))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), S (O))]))] |}] let%expect_test "simple call with read after write" = print_endline(prog_eval_t_simple_call_wr_rd ()); - [%expect {| [StEnv (MemEnv ([FunV; RefV (S (O)); UnitV (BotMV, ZeroRV, ZeroWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (O); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), RefT (Rf, UnitT (NRd, MayWr)))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), S (O))]))] |}] let%expect_test "simple call with forbidden write" = print_endline(prog_eval_t_simple_call_fbd_wr ()); [%expect {| [] |}] let%expect_test "simple call with write to ref" = print_endline(prog_eval_t_simple_call_ref_wr ()); - [%expect {| [StEnv (MemEnv ([FunV; RefV (S (O)); UnitV (BotMV, TopRV, OneWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (O); UnitV (BotMV, TopRV, OneWV)], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), RefT (Rf, UnitT (NRd, AlwaysWr)))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), S (O))]))] |}] let%expect_test "simple call with forbidden write to ref" = print_endline(prog_eval_t_simple_call_ref_fbd_wr ()); [%expect {| [] |}] let%expect_test "simple call with write to ref with fix" = print_endline(prog_eval_t_simple_call_ref_wr_with_fix ()); - [%expect {| [StEnv (MemEnv ([FunV; RefV (S (O)); UnitV (ZeroMV, TopRV, OneWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (O); UnitV (ZeroMV, TopRV, OneWV)], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), RefT (Rf, UnitT (NRd, AlwaysWr)))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), S (O))]))] |}] let%expect_test "call inside call" = print_endline(prog_eval_t_call_in_call ()); - [%expect {| [StEnv (MemEnv ([FunV; FunV; RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; FunV; RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), RefT (Rf, UnitT (Rd, AlwaysWr)))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), S (O))]))] |}] let%expect_test "call inside call, recursive" = print_endline(prog_eval_t_call_in_call_rec ()); - [%expect {| [StEnv (MemEnv ([FunV; RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), RefT (Rf, UnitT (Rd, AlwaysWr)))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), S (O))]))] |}] let%expect_test "call to fix after call" = print_endline(prog_eval_t_fix_call_after_call ()); - [%expect {| [StEnv (MemEnv ([FunV; FunV; RefV (S (O)); UnitV (ZeroMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; FunV; RefV (O); UnitV (ZeroMV, TopRV, OneWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), RefT (Rf, UnitT (Rd, AlwaysWr)))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), S (O))]))] |}] let%expect_test "simple call with global variable usage" = print_endline(prog_eval_t_call_with_glob_usage ()); - [%expect {| [StEnv (MemEnv ([FunV; RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), RefT (Rf, UnitT (Rd, AlwaysWr)))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), S (O))]))] |}] let%expect_test "simple call with read & write (2 args)" = print_endline(prog_eval_t_call_with_rd_wr_2_args ()); - [%expect {| [StEnv (MemEnv ([FunV; RefV (S (S (S (S (O))))); UnitV (BotMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (S (S (S (O)))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (S (S (O))); UnitV (BotMV, TopRV, OneWV); RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), RefT (Rf, UnitT (Rd, AlwaysWr)))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), S (O))]))] |}] let%expect_test "simple call with different arguments modifiers, copy" = print_endline(prog_eval_t_call_with_dif_mods_cp ()); - [%expect {| [StEnv (MemEnv ([FunV; RefV (S (S (S (S (S (S (S (S (S (S (O))))))))))); UnitV (ZeroMV, OneRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (S (S (S (S (S (S (O)))))))); UnitV (ZeroMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (S (S (S (O))))); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (O)))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (S (S (S (O)))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (S (S (S (S (S (S (O))))))); UnitV (ZeroMV, OneRV, OneWV); RefV (S (S (S (S (O))))); UnitV (ZeroMV, TopRV, OneWV); RefV (S (S (O))); UnitV (ZeroMV, OneRV, ZeroWV); RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], S (S (S (S (S (S (S (S (S (O)))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), RefT (Rf, UnitT (Rd, AlwaysWr)))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), S (O))]))] |}] let%expect_test "simple call with different arguments modifiers, ref" = print_endline(prog_eval_t_call_with_dif_mods_rf ()); - [%expect {| [StEnv (MemEnv ([FunV; RefV (S (S (S (S (S (S (S (S (S (S (O))))))))))); UnitV (ZeroMV, OneRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (S (S (S (S (S (S (O)))))))); UnitV (ZeroMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (S (S (S (O))))); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (O)))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (S (S (S (O)))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; RefV (S (S (S (S (S (S (O))))))); UnitV (ZeroMV, OneRV, OneWV); RefV (S (S (S (S (O))))); UnitV (ZeroMV, TopRV, OneWV); RefV (S (S (O))); UnitV (ZeroMV, OneRV, ZeroWV); RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], S (S (S (S (S (S (S (S (S (O)))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), RefT (Rf, UnitT (Rd, AlwaysWr)))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), S (O))]))] |}] (* - basic synthesis tests *) @@ -83,13 +83,13 @@ let%expect_test "simple synthesis test, reference forbidden write, no read write (* - presentation tests *) let%expect_test "presentation test 1 (simple types), eval" = print_endline(prog_eval_t_presentation_simple_tp ()); - [%expect {| [StEnv (MemEnv ([FunV; FunV; FunV; FunV; RefV (S (S (S (S (S (S (S (S (S (S (O))))))))))); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (S (S (S (S (S (S (O)))))))); UnitV (ZeroMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (S (S (S (O))))); UnitV (BotMV, OneRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (O)); UnitV (BotMV, OneRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (O)))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (S (S (S (O)))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; FunV; FunV; FunV; RefV (S (S (S (S (S (S (O))))))); UnitV (ZeroMV, OneRV, ZeroWV); RefV (S (S (S (S (O))))); UnitV (ZeroMV, TopRV, OneWV); RefV (S (S (O))); UnitV (BotMV, OneRV, OneWV); RefV (O); UnitV (BotMV, OneRV, OneWV)], S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), RefT (Rf, UnitT (Rd, AlwaysWr)))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (S (S (S (S (O)))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (S (S (S (S (O))))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (S (S (S (S (O)))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), S (O))]))] |}] let%expect_test "presentation test 1 (simple types), synt" = print_endline(prog_synt_t_presentation_simple_tp ()); [%expect {| [[Cp; Cp; Cp; Cp; Cp; Cp]; [Cp; Cp; Cp; Cp; Cp; Rf]; [Cp; Cp; Cp; Rf; Cp; Cp]; [Cp; Cp; Cp; Rf; Cp; Rf]; [Cp; Rf; Cp; Cp; Cp; Cp]; [Cp; Rf; Cp; Cp; Cp; Rf]; [Cp; Rf; Cp; Rf; Cp; Cp]; [Cp; Rf; Cp; Rf; Cp; Rf]; [Rf; Cp; Cp; Cp; Cp; Cp]; [Rf; Rf; Cp; Cp; Cp; Cp]; [Rf; Cp; Cp; Cp; Cp; Rf]; [Rf; Rf; Cp; Cp; Cp; Rf]; [Rf; Cp; Cp; Rf; Cp; Cp]; [Rf; Rf; Cp; Rf; Cp; Cp]; [Rf; Cp; Cp; Rf; Cp; Rf]; [Rf; Rf; Cp; Rf; Cp; Rf]] |}] let%expect_test "presentation test 2 (complex types), eval" = print_endline(prog_eval_t_presentation_complex_tp ()); - [%expect {| [StEnv (MemEnv ([FunV; TupleV ([RefV (S (S (S (S (S (O)))))); RefV (S (S (S (S (O))))); RefV (S (S (S (O))))]); TupleV ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV)]); TupleV ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV)]); UnitV (ZeroMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); TupleV ([UnitV (ZeroMV, ZeroRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)]); TupleV ([UnitV (ZeroMV, ZeroRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)])], S (S (S (S (S (S (S (S (O))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, MayWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, MayWr); UnitT (Rd, MayWr)])); RefT (Cp, UnitT (NRd, AlwaysWr))]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (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)]))] |}] + [%expect {| [StEnv (MemEnv ([FunV; TupleV ([RefV (S (S (O))); RefV (S (O)); RefV (O)]); TupleV ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV)]); TupleV ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV)]); UnitV (ZeroMV, TopRV, OneWV)], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, MayWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, MayWr); UnitT (Rd, MayWr)])); RefT (Cp, UnitT (NRd, AlwaysWr))]))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr))]))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), S (S (S (O))))]))] |}] let%expect_test "presentation test 2 (complex types), synt" = print_endline(prog_synt_t_presentation_complex_tp ()); [%expect {| [[Cp; Cp; Cp]; [Cp; Cp; Rf]; [Cp; Rf; Cp]; [Cp; Rf; Rf]] |}] diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 0ca2d5c..073f818 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -158,194 +158,168 @@ let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd in - globals_min_ido xg & - yg == Nat.s xg & + fresh prog, yg, fg, yd, fd in + globals_min_ido yg & fg == Nat.s yg & - xd == VarD (UnitT (Rd, NeverWr)) & yd == VarD (RefT (Rf, UnitT (Rd, NeverWr))) & fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))], ReadS (DerefP (VarP 0))) & - prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & + prog == Prg ([yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd in - globals_min_ido xg & - yg == Nat.s xg & + fresh prog, yg, fg, yd, fd in + globals_min_ido yg & fg == Nat.s yg & - xd == VarD (UnitT (NRd, AlwaysWr)) & yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & - prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & + prog == Prg ([yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) let prog_eval_t_simple_call_wr_rd _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd in - globals_min_ido xg & - yg == Nat.s xg & + fresh prog, yg, fg, yd, fd in + globals_min_ido yg & fg == Nat.s yg & - xd == VarD (UnitT (NRd, MayWr)) & yd == VarD (RefT (Rf, UnitT (NRd, MayWr))) & fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], SeqS (WriteS (DerefP (VarP 0)), ReadS (DerefP (VarP 0)))) & - prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & + prog == Prg ([yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) let prog_eval_t_simple_call_fbd_wr _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd in - globals_min_ido xg & - yg == Nat.s xg & + fresh prog, yg, fg, yd, fd in + globals_min_ido yg & fg == Nat.s yg & - xd == VarD (UnitT (Rd, MayWr)) & yd == VarD (RefT (Rf, UnitT (Rd, MayWr))) & fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))], WriteS (DerefP (VarP 0))) & - prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & + prog == Prg ([yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd in - globals_min_ido xg & - yg == Nat.s xg & + fresh prog, yg, fg, yd, fd in + globals_min_ido yg & fg == Nat.s yg & - xd == VarD (UnitT (NRd, AlwaysWr)) & yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & - prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & + prog == Prg ([yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) let prog_eval_t_simple_call_ref_fbd_wr _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd in - globals_min_ido xg & - yg == Nat.s xg & + fresh prog, yg, fg, yd, fd in + globals_min_ido yg & fg == Nat.s yg & - xd == VarD (UnitT (Rd, AlwaysWr)) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & - prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), - ReadS (DerefP (VarP yg)))) & + prog == Prg ([yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), + ReadS (DerefP (VarP yg)))) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd in - globals_min_ido xg & - yg == Nat.s xg & + fresh prog, yg, fg, yd, fd in + globals_min_ido yg & fg == Nat.s yg & - xd == VarD (UnitT (NRd, AlwaysWr)) & yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & - prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), - SeqS (WriteS (DerefP (VarP yg)), - ReadS (DerefP (VarP yg))))) & + prog == Prg ([yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), + SeqS (WriteS (DerefP (VarP yg)), + ReadS (DerefP (VarP yg))))) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, f2g, xd, yd, fd, f2d in - globals_min_ido xg & - yg == Nat.s xg & + fresh prog, yg, fg, f2g, yd, fd, f2d in + globals_min_ido yg & fg == Nat.s yg & f2g == Nat.s fg & - xd == VarD (UnitT (Rd, AlwaysWr)) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], SeqS (CallS (VarP fg, [PathE (VarP 0)]), WriteS (DerefP (VarP 0)))) & - prog == Prg ([xd; yd; fd; f2d], SeqS (CallS (VarP f2g, [PathE (VarP yg)]), - ReadS (DerefP (VarP yg)))) & + prog == Prg ([yd; fd; f2d], SeqS (CallS (VarP f2g, [PathE (VarP yg)]), + ReadS (DerefP (VarP yg)))) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) let prog_eval_t_call_in_call_rec _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd in - globals_min_ido xg & - yg == Nat.s xg & + fresh prog, yg, fg, yd, fd in + globals_min_ido yg & fg == Nat.s yg & - xd == VarD (UnitT (Rd, AlwaysWr)) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], SeqS (CallS (VarP fg, [PathE (VarP 0)]), WriteS (DerefP (VarP 0)))) & - prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), - ReadS (DerefP (VarP yg)))) & + prog == Prg ([yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), + ReadS (DerefP (VarP yg)))) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, f2g, xd, yd, fd, f2d in - globals_min_ido xg & - yg == Nat.s xg & + fresh prog, yg, fg, f2g, yd, fd, f2d in + globals_min_ido yg & fg == Nat.s yg & f2g == Nat.s fg & - xd == VarD (UnitT (Rd, AlwaysWr)) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & f2d == FunD ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & - prog == Prg ([xd; yd; fd; f2d], SeqS (CallS (VarP fg, [PathE (VarP yg)]), - SeqS (CallS (VarP f2g, [PathE (VarP yg)]), - ReadS (DerefP (VarP yg))))) & + prog == Prg ([yd; fd; f2d], SeqS (CallS (VarP fg, [PathE (VarP yg)]), + SeqS (CallS (VarP f2g, [PathE (VarP yg)]), + ReadS (DerefP (VarP yg))))) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, fg, xd, yd, fd in - globals_min_ido xg & - yg == Nat.s xg & + fresh prog, yg, fg, yd, fd in + globals_min_ido yg & fg == Nat.s yg & - xd == VarD (UnitT (Rd, AlwaysWr)) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))], - SeqS (WriteS (VarP xg), + SeqS (WriteS (DerefP (VarP yg)), ReadS (DerefP (VarP 0)))) & - prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), - ReadS (DerefP (VarP yg)))) & + prog == Prg ([yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), + ReadS (DerefP (VarP yg)))) & prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) let prog_eval_t_call_with_rd_wr_2_args _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, x2g, y2g, fg, xd, yd, x2d, y2d, fd in - globals_min_ido xg & - yg == Nat.s xg & - x2g == Nat.s yg & - y2g == Nat.s x2g & + fresh prog, yg, y2g, fg, yd, y2d, fd in + globals_min_ido yg & + y2g == Nat.s yg & fg == Nat.s y2g & - xd == VarD (UnitT (Rd, AlwaysWr)) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & - x2d == VarD (UnitT (Rd, AlwaysWr)) & y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], SeqS (ReadS (DerefP (VarP 0)), WriteS (DerefP (VarP 1)))) & - prog == Prg ([xd; yd; x2d; y2d; fd], + prog == Prg ([yd; y2d; fd], CallS (VarP fg, [PathE (VarP yg); PathE (VarP y2g)])) & prog_evalo prog q @@ -354,34 +328,20 @@ let prog_eval_t_call_with_rd_wr_2_args _ = show(answer) (Stream.take (run q let prog_eval_t_call_with_dif_mods_cp _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, - x2g, y2g, - x3g, y3g, - x4g, y4g, + fresh prog, yg, y2g, y3g, y4g, fg, - xd, yd, - x2d, y2d, - x3d, y3d, - x4d, y4d, + yd, y2d, y3d, y4d, fd, fstmts, stmts in - globals_min_ido xg & - yg == Nat.s xg & - x2g == Nat.s yg & - y2g == Nat.s x2g & - x3g == Nat.s y2g & - y3g == Nat.s x3g & - x4g == Nat.s y3g & - y4g == Nat.s x4g & + globals_min_ido yg & + y2g == Nat.s yg & + y3g == Nat.s y2g & + y4g == Nat.s y3g & fg == Nat.s y4g & - xd == VarD (UnitT (Rd, AlwaysWr)) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & - x2d == VarD (UnitT (Rd, AlwaysWr)) & y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & - x3d == VarD (UnitT (Rd, AlwaysWr)) & y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & - x4d == VarD (UnitT (Rd, AlwaysWr)) & y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & seqo [ReadS (DerefP (VarP 1)); ReadS (DerefP (VarP 3)); @@ -401,10 +361,7 @@ let prog_eval_t_call_with_dif_mods_cp _ = show(answer) (Stream.take (run q ReadS (DerefP (VarP y2g)); ReadS (DerefP (VarP y3g)); ReadS (DerefP (VarP y4g))] stmts & - prog == Prg ([xd; yd; - x2d; y2d; - x3d; y3d; - x4d; y4d; + prog == Prg ([yd; y2d; y3d; y4d; fd], stmts) & prog_evalo prog q @@ -413,34 +370,20 @@ let prog_eval_t_call_with_dif_mods_cp _ = show(answer) (Stream.take (run q let prog_eval_t_call_with_dif_mods_rf _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xg, yg, - x2g, y2g, - x3g, y3g, - x4g, y4g, + fresh prog, yg, y2g, y3g, y4g, fg, - xd, yd, - x2d, y2d, - x3d, y3d, - x4d, y4d, + yd, y2d, y3d, y4d, fd, fstmts, stmts in - globals_min_ido xg & - yg == Nat.s xg & - x2g == Nat.s yg & - y2g == Nat.s x2g & - x3g == Nat.s y2g & - y3g == Nat.s x3g & - x4g == Nat.s y3g & - y4g == Nat.s x4g & + globals_min_ido yg & + y2g == Nat.s yg & + y3g == Nat.s y2g & + y4g == Nat.s y3g & fg == Nat.s y4g & - xd == VarD (UnitT (Rd, AlwaysWr)) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & - x2d == VarD (UnitT (Rd, AlwaysWr)) & y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & - x3d == VarD (UnitT (Rd, AlwaysWr)) & y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & - x4d == VarD (UnitT (Rd, AlwaysWr)) & y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & seqo [ReadS (DerefP (VarP 1)); ReadS (DerefP (VarP 3)); @@ -459,10 +402,7 @@ let prog_eval_t_call_with_dif_mods_rf _ = show(answer) (Stream.take (run q ReadS (DerefP (VarP y2g)); ReadS (DerefP (VarP y3g)); ReadS (DerefP (VarP y4g))] stmts & - prog == Prg ([xd; yd; - x2d; y2d; - x3d; y3d; - x4d; y4d; + prog == Prg ([yd; y2d; y3d; y4d; fd], stmts) & prog_evalo prog q @@ -537,37 +477,23 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak let prog_eval_t_presentation_simple_tp _ = show(answer) (Stream.take (run q (fun q -> ocanren { - fresh prog, xbg, xg, - ybg, yg, - zbg, zg, - kbg, kg, + fresh prog, xg, yg, zg, kg, fg, wg, gg, rg, - xbd, xd, - ybd, yd, - zbd, zd, - kbd, kd, + xd, yd, zd, kd, fd, wd, gd, rd, fstmts, gstmts, stmts in - globals_min_ido xbg & - xg == Nat.s xbg & - ybg == Nat.s xg & - yg == Nat.s ybg & - zbg == Nat.s yg & - zg == Nat.s zbg & - kbg == Nat.s zg & - kg == Nat.s kbg & + globals_min_ido xg & + yg == Nat.s xg & + zg == Nat.s yg & + kg == Nat.s zg & fg == Nat.s kg & wg == Nat.s fg & gg == Nat.s wg & rg == Nat.s gg & - xbd == VarD (UnitT (Rd, AlwaysWr)) & xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & - ybd == VarD (UnitT (Rd, AlwaysWr)) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & - zbd == VarD (UnitT (Rd, AlwaysWr)) & zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & - kbd == VarD (UnitT (Rd, AlwaysWr)) & kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & seqo [ReadS (DerefP (VarP 0)); WriteS (DerefP (VarP 0)); @@ -597,10 +523,7 @@ let prog_eval_t_presentation_simple_tp _ = show(answer) (Stream.take (run q CallS (VarP fg, [PathE (VarP yg); PathE (VarP zg)]); CallS (VarP rg, [PathE (VarP kg)]) ] stmts & - prog == Prg ([xbd; xd; - ybd; yd; - zbd; zd; - kbd; kd; + prog == Prg ([xd; yd; zd; kd; fd; wd; gd; rd], stmts) & prog_evalo prog q @@ -609,39 +532,25 @@ let prog_eval_t_presentation_simple_tp _ = show(answer) (Stream.take (run q let prog_synt_t_presentation_simple_tp _ = show(answerCpCapList) (Stream.take (run q (fun q -> ocanren { - fresh prog, xbg, xg, - ybg, yg, - zbg, zg, - kbg, kg, + fresh prog, xg, yg, zg, kg, fg, wg, gg, rg, - xbd, xd, - ybd, yd, - zbd, zd, - kbd, kd, + xd, yd, zd, kd, fd, wd, gd, rd, fstmts, gstmts, stmts, c_fx, c_fy, c_wx, c_gx, c_gy, c_rx, st in - globals_min_ido xbg & - xg == Nat.s xbg & - ybg == Nat.s xg & - yg == Nat.s ybg & - zbg == Nat.s yg & - zg == Nat.s zbg & - kbg == Nat.s zg & - kg == Nat.s kbg & + globals_min_ido xg & + yg == Nat.s xg & + zg == Nat.s yg & + kg == Nat.s zg & fg == Nat.s kg & wg == Nat.s fg & gg == Nat.s wg & rg == Nat.s gg & - xbd == VarD (UnitT (Rd, AlwaysWr)) & xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & - ybd == VarD (UnitT (Rd, AlwaysWr)) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & - zbd == VarD (UnitT (Rd, AlwaysWr)) & zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & - kbd == VarD (UnitT (Rd, AlwaysWr)) & kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & seqo [ReadS (DerefP (VarP 0)); WriteS (DerefP (VarP 0)); @@ -671,10 +580,7 @@ let prog_synt_t_presentation_simple_tp _ = show(answerCpCapList) (Stream.take (r CallS (VarP fg, [PathE (VarP yg); PathE (VarP zg)]); CallS (VarP rg, [PathE (VarP kg)]) ] stmts & - prog == Prg ([xbd; xd; - ybd; yd; - zbd; zd; - kbd; kd; + prog == Prg ([xd; yd; zd; kd; fd; wd; gd; rd], stmts) & prog_evalo prog st & @@ -771,14 +677,10 @@ let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q fresh prog, userT, dataT, timeT, requestT, requestArgsT, - userE, dataE, timeE, requestE, - userVID, dataVID, timeVID, requestVID, + requestVID, sendFID, sendD, sendBranchStmts, sendStmts, stmts in - globals_min_ido userVID & - dataVID == Nat.s userVID & - timeVID == Nat.s dataVID & - requestVID == Nat.s timeVID & + globals_min_ido requestVID & sendFID == Nat.s requestVID & p_rw_userTo userT & @@ -787,11 +689,6 @@ let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q p_rw_requestTo Cp Cp Cp requestT & p_any_requestTo Cp Cp Cp requestArgsT & (* NOTE: for now *) - userE == TupleE [UnitE; UnitE; UnitE] & - dataE == TupleE [UnitE; UnitE] & - timeE == UnitE & - requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] & - fresh data_p, time_p, user_id_p, user_name_p in deref_accesso 1 0 data_p & @@ -828,9 +725,6 @@ let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q ReadS time_gp ] stmts & prog == Prg ([ - VarD userT; - VarD dataT; - VarD timeT; VarD requestT; sendD ], @@ -845,15 +739,11 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take ( fresh prog, userT, dataT, timeT, requestT, requestArgsT, - userE, dataE, timeE, requestE, - userVID, dataVID, timeVID, requestVID, + requestVID, sendFID, sendD, sendBranchStmts, sendStmts, stmts, st, c_u, c_d, c_t in - globals_min_ido userVID & - dataVID == Nat.s userVID & - timeVID == Nat.s dataVID & - requestVID == Nat.s timeVID & + globals_min_ido requestVID & sendFID == Nat.s requestVID & p_rw_userTo userT & @@ -862,11 +752,6 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take ( p_rw_requestTo Cp Cp Cp requestT & p_any_requestTo c_u c_d c_t requestArgsT & (* NOTE: for now *) - userE == TupleE [UnitE; UnitE; UnitE] & - dataE == TupleE [UnitE; UnitE] & - timeE == UnitE & - requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] & - fresh data_p, time_p, user_id_p, user_name_p, user_surname_p in deref_accesso 1 0 data_p & @@ -898,9 +783,6 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take ( ReadS time_gp ] stmts & prog == Prg ([ - VarD userT; - VarD dataT; - VarD timeT; VarD requestT; sendD ], @@ -933,14 +815,8 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q userT, versionT, utilsT, requestT, moded_requestT, - (* global vars init exprs *) - user_utilsE, user_infoE, - userE, versionE, utilsE, - requestE, (* global vars ids *) - user_utilsID, user_infoID, - userID, versionID, utilsID, - dataID, requestID, + requestID, (* function ids *) get_version_idID, updated_versionID, @@ -968,26 +844,8 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q RefT (Cp, uT_r_aw) (* 3 data *); uT_r_aw (* 4 operation_date *)] & moded_requestT == (Mode (In, NOut), requestT) & - (* global vars init exprs *) - user_utilsE == TupleE [UnitE (* 0 id *); UnitE] & - user_infoE == TupleE [UnitE (* 0 name *); UnitE; UnitE] & - userE == TupleE [RefE user_utilsID (* 0 utils *); - RefE user_infoID (* 1 info *)] & - versionE == TupleE [UnitE (* 0 id *); UnitE; UnitE] & - utilsE == TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] & - requestE == TupleE [RefE userID (* 0 user *); - RefE versionID (* 1 version *); - RefE utilsID (* 2 utils *); - RefE dataID (* 3 data *); - UnitE (* 4 operation_date *)] & (* global vars ids *) - globals_min_ido user_utilsID & - user_infoID == Nat.s user_utilsID & - userID == Nat.s user_infoID & - versionID == Nat.s userID & - utilsID == Nat.s versionID & - dataID == Nat.s utilsID & - requestID == Nat.s dataID & + globals_min_ido requestID & (* function ids *) get_version_idID == Nat.s requestID & updated_versionID == Nat.s get_version_idID & @@ -1041,12 +899,6 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q send_allF & prog == Prg ([ - VarD user_utilsT; - VarD user_infoT; - VarD userT; - VarD versionT; - VarD utilsT; - VarD uT_r_aw; (* data *) VarD requestT; FunD ([moded_requestT], get_version_idF); FunD ([moded_requestT], updated_versionF); @@ -1220,14 +1072,7 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q userT, versionT, utilsT, requestT, (* moded_requestT, *) - (* global vars init exprs *) - user_utilsE, user_infoE, - userE, versionE, utilsE, - requestE, - (* global vars ids *) - user_utilsID, user_infoID, - userID, versionID, utilsID, - dataID, requestID, + requestID, (* function ids *) get_version_idID, updated_versionID, @@ -1252,26 +1097,8 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q rw_utilsTo utilsT & rw_requestTo Cp Cp Cp Cp Cp Cp requestT & (* moded_requestTo moded_requestT & *) - (* global vars init exprs *) - user_utilsE == TupleE [UnitE (* 0 id *); UnitE] & - user_infoE == TupleE [UnitE (* 0 name *); UnitE; UnitE] & - userE == TupleE [RefE user_utilsID (* 0 utils *); - RefE user_infoID (* 1 info *)] & - versionE == TupleE [UnitE (* 0 id *); UnitE; UnitE] & - utilsE == TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] & - requestE == TupleE [RefE userID (* 0 user *); - RefE versionID (* 1 version *); - RefE utilsID (* 2 utils *); - RefE dataID (* 3 data *); - UnitE (* 4 operation_date *)] & (* global vars ids *) - globals_min_ido user_utilsID & - user_infoID == Nat.s user_utilsID & - userID == Nat.s user_infoID & - versionID == Nat.s userID & - utilsID == Nat.s versionID & - dataID == Nat.s utilsID & - requestID == Nat.s dataID & + globals_min_ido requestID & (* function ids *) get_version_idID == Nat.s requestID & updated_versionID == Nat.s get_version_idID & @@ -1336,12 +1163,6 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q (* [gvi_c0; gvi_c1; gvi_c2; gvi_c3; gvi_c4; gvi_c5] & *) prog == Prg ([ - VarD user_utilsT; - VarD user_infoT; - VarD userT; - VarD versionT; - VarD utilsT; - VarD uT_r_aw; (* data *) VarD requestT; (* FunD ([mrT'], get_version_idF); *) (* FunD ([mrT'], updated_versionF); *)