st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-06-10 19:28:16 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

struct: remove test parts that are not required now (with new lambda model)

Browse source
This commit is contained in:
ProgramSnail 2026-05-22 12:50:47 +00:00
parent 441b383762
commit 06f69ec4c2
4 changed files with 191 additions and 460 deletions
Download patch file Download diff file Expand all files Collapse all files

153
model_with_structures/analyzer.ml
View file

@ -571,25 +571,6 @@ struct
let vg10 = VarP (globals_min_id + 10) let vg10 = VarP (globals_min_id + 10)
let vg11 = VarP (globals_min_id + 11) 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 pE p = PathE p
let drf p = DerefP p let drf p = DerefP p
@ -712,14 +693,13 @@ struct
let%expect_test "simple call with read, dsl" = let%expect_test "simple call with read, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_mw;
defg (rfT uT_r_mw); defg (rfT uT_r_mw);
FunD ( FunD (
[moded @@ cpT @@ uT_r], [moded @@ cpT @@ uT_r],
rdS @@ drf @@ v0 rdS @@ drf @@ v0
) )
], ],
callS vg2 [pE vg1] callS vg1 [pE vg0]
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -727,14 +707,13 @@ struct
let%expect_test "simple call with write, dsl" = let%expect_test "simple call with write, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_aw;
defg (rfT uT_aw); defg (rfT uT_aw);
FunD ( FunD (
[moded @@ cpT @@ uT_aw], [moded @@ cpT @@ uT_aw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
) )
], ],
callS vg2 [pE vg1] callS vg1 [pE vg0]
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -742,7 +721,6 @@ struct
let%expect_test "simple call with read after write, dsl" = let%expect_test "simple call with read after write, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_aw;
defg (rfT uT_aw); defg (rfT uT_aw);
FunD ( FunD (
[moded @@ cpT @@ uT_aw], [moded @@ cpT @@ uT_aw],
@ -750,7 +728,7 @@ struct
(rdS @@ drf @@ v0) (rdS @@ drf @@ v0)
) )
], ],
callS vg2 [pE vg1] callS vg1 [pE vg0]
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -758,31 +736,28 @@ struct
let%expect_test "simple call with forbidden write, dsl" = let%expect_test "simple call with forbidden write, dsl" =
try (prog_eval_noret ( try (prog_eval_noret (
[ [
defg uT_r_mw;
defg (rfT uT_r_mw); defg (rfT uT_r_mw);
FunD ( FunD (
[moded @@ cpT @@ uT_r], [moded @@ cpT @@ uT_r],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
) )
], ],
callS vg2 [pE vg1] callS vg1 [pE vg0]
); );
[%expect.unreachable]); [%expect.unreachable]);
with Eval_error msg -> Printf.printf "%s" msg; with Eval_error msg -> Printf.printf "%s" msg;
[%expect {| write: write tag |}] [%expect {| write: write tag |}]
(* TODO: FIXME: why is condition on always write in parent ?? *)
let%expect_test "simple call with write to ref, dsl" = let%expect_test "simple call with write to ref, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
FunD ( FunD (
[moded @@ rfT @@ uT_aw], [moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
) )
], ],
callS vg2 [pE vg1] callS vg1 [pE vg0]
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -790,15 +765,14 @@ struct
let%expect_test "simple call with forbidden write to ref, dsl" = let%expect_test "simple call with forbidden write to ref, dsl" =
try (prog_eval_noret ( try (prog_eval_noret (
[ [
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
FunD ( FunD (
[moded @@ rfT @@ uT_aw], [moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
) )
], ],
(callS vg2 [pE vg1]) #. (callS vg1 [pE vg0]) #.
(rdS @@ drf @@ vg1) (rdS @@ drf @@ vg0)
); );
[%expect.unreachable]); [%expect.unreachable]);
with Eval_error msg -> Printf.printf "%s" msg; 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" = let%expect_test "simple call with write to ref with fix, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
FunD ( FunD (
[moded @@ rfT @@ uT_aw], [moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
) )
], ],
(callS vg2 [pE vg1]) #. (callS vg1 [pE vg0]) #.
(wrS @@ drf @@ vg1) #. (wrS @@ drf @@ vg0) #.
(rdS @@ drf @@ vg1) (rdS @@ drf @@ vg0)
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -824,7 +797,6 @@ struct
let%expect_test "call inside call, dsl" = let%expect_test "call inside call, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
FunD ( FunD (
[moded @@ rfT @@ uT_aw], [moded @@ rfT @@ uT_aw],
@ -832,38 +804,36 @@ struct
); );
FunD ( FunD (
[moded @@ cpT @@ uT_aw], [moded @@ cpT @@ uT_aw],
(callS vg2 [pE v0]) #. (callS vg1 [pE v0]) #.
(wrS @@ drf @@ v0) (wrS @@ drf @@ v0)
) )
], ],
(callS vg3 [pE vg1]) #. (callS vg2 [pE vg0]) #.
(rdS @@ drf @@ vg1) (rdS @@ drf @@ vg0)
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
(* NOTE: memoization used *) (* NOTE: does not work for annalyzer rw to the sequenced declaration addition to calculate tags *)
let%expect_test "call inside call, recursive, dsl" = (* let%expect_test "call inside call, recursive, dsl" = *)
prog_eval_noret ( (* prog_eval_noret ( *)
[ (* [ *)
defg uT_r_aw; (* defg (rfT uT_r_aw); *)
defg (rfT uT_r_aw); (* FunD ( *)
FunD ( (* [moded @@ cpT @@ uT_aw], *)
[moded @@ cpT @@ uT_aw], (* (callS vg1 [pE v0]) #. *)
(callS vg2 [pE v0]) #. (* (wrS @@ drf @@ v0) *)
(wrS @@ drf @@ v0) (* ) *)
) (* ], *)
], (* (callS vg1 [pE vg0]) #. *)
(callS vg2 [pE vg1]) #. (* (rdS @@ drf @@ vg0) *)
(rdS @@ drf @@ vg1) (* ); *)
); (* Printf.printf "done!"; *)
Printf.printf "done!"; (* [%expect {| done! |}] *)
[%expect {| done! |}]
let%expect_test "call to fix after call, dsl" = let%expect_test "call to fix after call, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
FunD ( FunD (
[moded @@ rfT @@ uT_aw], [moded @@ rfT @@ uT_aw],
@ -874,9 +844,9 @@ struct
wrS @@ drf @@ v0 wrS @@ drf @@ v0
) )
], ],
(callS vg2 [pE vg1]) #. (callS vg1 [pE vg0]) #.
(callS vg3 [pE vg1]) #. (callS vg2 [pE vg0]) #.
(rdS @@ drf @@ vg1) (rdS @@ drf @@ vg0)
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -884,16 +854,15 @@ struct
let%expect_test "simple call with global variable usage, dsl" = let%expect_test "simple call with global variable usage, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw; defg (rfT uT_r_aw);
defg (rfT uT_r);
FunD ( FunD (
[moded @@ cpT @@ uT], [moded @@ cpT @@ uT],
(wrS @@ vg0) #. (wrS @@ drf @@ vg0) #.
(rdS @@ drf @@ vg1) (rdS @@ drf @@ vg0)
) )
], ],
(callS vg2 [pE vg1]) #. (callS vg1 [pE vg0]) #.
(rdS @@ drf @@ vg1) (rdS @@ drf @@ vg0)
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -901,9 +870,7 @@ struct
let%expect_test "simple call with read & write (2 args), dsl" = let%expect_test "simple call with read & write (2 args), dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r;
defg (rfT uT_r); defg (rfT uT_r);
defg uT_aw;
defg (rfT uT_aw); defg (rfT uT_aw);
FunD ( FunD (
[ [
@ -914,7 +881,7 @@ struct
(wrS @@ drf @@ v1) (wrS @@ drf @@ v1)
) )
], ],
callS vg4 [pE vg1; pE vg3] callS vg2 [pE vg0; pE vg1]
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -922,13 +889,9 @@ struct
let%expect_test "simple call with different arguments modifiers, copy, dsl" = let%expect_test "simple call with different arguments modifiers, copy, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
FunD ( FunD (
[ [
@ -944,11 +907,11 @@ struct
(wrS @@ drf @@ v3) (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 @@ vg1) #.
(rdS @@ drf @@ vg3) #. (rdS @@ drf @@ vg2) #.
(rdS @@ drf @@ vg5) #. (rdS @@ drf @@ vg3)
(rdS @@ drf @@ vg7)
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -956,13 +919,9 @@ struct
let%expect_test "simple call with different arguments modifiers, ref, dsl" = let%expect_test "simple call with different arguments modifiers, ref, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r;
defg (rfT uT_r); defg (rfT uT_r);
defg uT_r;
defg (rfT uT_r); defg (rfT uT_r);
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
FunD ( FunD (
[ [
@ -977,11 +936,11 @@ struct
(wrS @@ drf @@ v3) (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 @@ vg1) #.
(rdS @@ drf @@ vg3) #. (rdS @@ drf @@ vg2) #.
(rdS @@ drf @@ vg5) #. (rdS @@ drf @@ vg3)
(rdS @@ drf @@ vg7)
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -991,13 +950,9 @@ struct
let%expect_test "presentation test 1 (simple types), dsl" = let%expect_test "presentation test 1 (simple types), dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw;
defg (rfT uT_r_aw); (* x *) defg (rfT uT_r_aw); (* x *)
defg uT_r_aw;
defg (rfT uT_r_aw); (* y *) defg (rfT uT_r_aw); (* y *)
defg uT_r_aw;
defg (rfT uT_r_aw); (* z *) defg (rfT uT_r_aw); (* z *)
defg uT_r_aw;
defg (rfT uT_r_aw); (* k *) defg (rfT uT_r_aw); (* k *)
FunD ( (* f *) FunD ( (* f *)
[ [
@ -1031,14 +986,14 @@ struct
(rdS @@ drf @@ v0) (rdS @@ drf @@ v0)
) )
], ],
let xV = vg1 in let xV = vg0 in
let yV = vg3 in let yV = vg1 in
let zV = vg5 in let zV = vg2 in
let kV = vg7 in let kV = vg3 in
let fF = vg8 in let fF = vg4 in
let wF = vg9 in let wF = vg5 in
let gF = vg10 in let gF = vg6 in
let rF = vg11 in let rF = vg7 in
(callS wF [pE xV]) #. (callS wF [pE xV]) #.
(callS rF [pE xV]) #. (callS rF [pE xV]) #.
(callS fF [pE xV; pE yV]) #. (callS fF [pE xV; pE yV]) #.

127
model_with_structures/analyzer_rw.ml
View file

@ -615,25 +615,6 @@ struct
let vg10 = VarP (globals_min_id + 10) let vg10 = VarP (globals_min_id + 10)
let vg11 = VarP (globals_min_id + 11) 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 pE p = PathE p
let drf p = DerefP p let drf p = DerefP p
@ -837,14 +818,13 @@ struct
let%expect_test "simple call with read, dsl" = let%expect_test "simple call with read, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_mw;
defg (rfT uT_r_mw); defg (rfT uT_r_mw);
FunD ( FunD (
[moded @@ cpT @@ uT_r], [moded @@ cpT @@ uT_r],
rdS @@ drf @@ v0 rdS @@ drf @@ v0
) )
], ],
callS vg2 [pE vg1] callS vg1 [pE vg0]
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -852,14 +832,13 @@ struct
let%expect_test "simple call with write, dsl" = let%expect_test "simple call with write, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_aw;
defg (rfT uT_aw); defg (rfT uT_aw);
FunD ( FunD (
[moded @@ cpT @@ uT_aw], [moded @@ cpT @@ uT_aw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
) )
], ],
callS vg2 [pE vg1] callS vg1 [pE vg0]
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -867,7 +846,6 @@ struct
let%expect_test "simple call with read after write, dsl" = let%expect_test "simple call with read after write, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_aw;
defg (rfT uT_aw); defg (rfT uT_aw);
FunD ( FunD (
[moded @@ cpT @@ uT_aw], [moded @@ cpT @@ uT_aw],
@ -875,7 +853,7 @@ struct
(rdS @@ drf @@ v0) (rdS @@ drf @@ v0)
) )
], ],
callS vg2 [pE vg1] callS vg1 [pE vg0]
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -883,31 +861,28 @@ struct
let%expect_test "simple call with forbidden write, dsl" = let%expect_test "simple call with forbidden write, dsl" =
try (prog_eval_noret ( try (prog_eval_noret (
[ [
defg uT_r_mw;
defg (rfT uT_r_mw); defg (rfT uT_r_mw);
FunD ( FunD (
[moded @@ cpT @@ uT_r], [moded @@ cpT @@ uT_r],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
) )
], ],
callS vg2 [pE vg1] callS vg1 [pE vg0]
); );
[%expect.unreachable]); [%expect.unreachable]);
with Eval_error msg -> Printf.printf "%s" msg; with Eval_error msg -> Printf.printf "%s" msg;
[%expect {| write: write tag |}] [%expect {| write: write tag |}]
(* TODO: FIXME: why is condition on always write in parent ?? *)
let%expect_test "simple call with write to ref, dsl" = let%expect_test "simple call with write to ref, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
FunD ( FunD (
[moded @@ rfT @@ uT_aw], [moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
) )
], ],
callS vg2 [pE vg1] callS vg1 [pE vg0]
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -915,15 +890,14 @@ struct
let%expect_test "simple call with forbidden write to ref, dsl" = let%expect_test "simple call with forbidden write to ref, dsl" =
try (prog_eval_noret ( try (prog_eval_noret (
[ [
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
FunD ( FunD (
[moded @@ rfT @@ uT_aw], [moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
) )
], ],
(callS vg2 [pE vg1]) #. (callS vg1 [pE vg0]) #.
(rdS @@ drf @@ vg1) (rdS @@ drf @@ vg0)
); );
[%expect.unreachable]); [%expect.unreachable]);
with Eval_error msg -> Printf.printf "%s" msg; 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" = let%expect_test "simple call with write to ref with fix, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
FunD ( FunD (
[moded @@ rfT @@ uT_aw], [moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
) )
], ],
(callS vg2 [pE vg1]) #. (callS vg1 [pE vg0]) #.
(wrS @@ drf @@ vg1) #. (wrS @@ drf @@ vg0) #.
(rdS @@ drf @@ vg1) (rdS @@ drf @@ vg0)
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -949,7 +922,6 @@ struct
let%expect_test "call inside call, dsl" = let%expect_test "call inside call, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
FunD ( FunD (
[moded @@ rfT @@ uT_aw], [moded @@ rfT @@ uT_aw],
@ -957,12 +929,12 @@ struct
); );
FunD ( FunD (
[moded @@ cpT @@ uT_aw], [moded @@ cpT @@ uT_aw],
(callS vg2 [pE v0]) #. (callS vg1 [pE v0]) #.
(wrS @@ drf @@ v0) (wrS @@ drf @@ v0)
) )
], ],
(callS vg3 [pE vg1]) #. (callS vg2 [pE vg0]) #.
(rdS @@ drf @@ vg1) (rdS @@ drf @@ vg0)
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -971,16 +943,15 @@ struct
(* let%expect_test "call inside call, recursive, dsl" = *) (* let%expect_test "call inside call, recursive, dsl" = *)
(* prog_eval_noret ( *) (* prog_eval_noret ( *)
(* [ *) (* [ *)
(* defg uT_r_aw; *)
(* defg (rfT uT_r_aw); *) (* defg (rfT uT_r_aw); *)
(* FunD ( *) (* FunD ( *)
(* [moded @@ cpT @@ uT_aw], *) (* [moded @@ cpT @@ uT_aw], *)
(* (callS vg2 [pE v0]) #. *) (* (callS vg1 [pE v0]) #. *)
(* (wrS @@ drf @@ v0) *) (* (wrS @@ drf @@ v0) *)
(* ) *) (* ) *)
(* ], *) (* ], *)
(* (callS vg2 [pE vg1]) #. *) (* (callS vg1 [pE vg0]) #. *)
(* (rdS @@ drf @@ vg1) *) (* (rdS @@ drf @@ vg0) *)
(* ); *) (* ); *)
(* Printf.printf "done!"; *) (* Printf.printf "done!"; *)
(* [%expect {| done! |}] *) (* [%expect {| done! |}] *)
@ -988,7 +959,6 @@ struct
let%expect_test "call to fix after call, dsl" = let%expect_test "call to fix after call, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
FunD ( FunD (
[moded @@ rfT @@ uT_aw], [moded @@ rfT @@ uT_aw],
@ -999,9 +969,9 @@ struct
wrS @@ drf @@ v0 wrS @@ drf @@ v0
) )
], ],
(callS vg2 [pE vg1]) #. (callS vg1 [pE vg0]) #.
(callS vg3 [pE vg1]) #. (callS vg2 [pE vg0]) #.
(rdS @@ drf @@ vg1) (rdS @@ drf @@ vg0)
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -1009,16 +979,15 @@ struct
let%expect_test "simple call with global variable usage, dsl" = let%expect_test "simple call with global variable usage, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw; defg (rfT uT_r_aw);
defg (rfT uT_r);
FunD ( FunD (
[moded @@ cpT @@ uT], [moded @@ cpT @@ uT],
(wrS @@ vg0) #. (wrS @@ drf @@ vg0) #.
(rdS @@ drf @@ vg1) (rdS @@ drf @@ vg0)
) )
], ],
(callS vg2 [pE vg1]) #. (callS vg1 [pE vg0]) #.
(rdS @@ drf @@ vg1) (rdS @@ drf @@ vg0)
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -1026,9 +995,7 @@ struct
let%expect_test "simple call with read & write (2 args), dsl" = let%expect_test "simple call with read & write (2 args), dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r;
defg (rfT uT_r); defg (rfT uT_r);
defg uT_aw;
defg (rfT uT_aw); defg (rfT uT_aw);
FunD ( FunD (
[ [
@ -1039,7 +1006,7 @@ struct
(wrS @@ drf @@ v1) (wrS @@ drf @@ v1)
) )
], ],
callS vg4 [pE vg1; pE vg3] callS vg2 [pE vg0; pE vg1]
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -1047,13 +1014,9 @@ struct
let%expect_test "simple call with different arguments modifiers, copy, dsl" = let%expect_test "simple call with different arguments modifiers, copy, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
FunD ( FunD (
[ [
@ -1069,11 +1032,11 @@ struct
(wrS @@ drf @@ v3) (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 @@ vg1) #.
(rdS @@ drf @@ vg3) #. (rdS @@ drf @@ vg2) #.
(rdS @@ drf @@ vg5) #. (rdS @@ drf @@ vg3)
(rdS @@ drf @@ vg7)
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -1081,13 +1044,9 @@ struct
let%expect_test "simple call with different arguments modifiers, ref, dsl" = let%expect_test "simple call with different arguments modifiers, ref, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r;
defg (rfT uT_r); defg (rfT uT_r);
defg uT_r;
defg (rfT uT_r); defg (rfT uT_r);
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
defg uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw);
FunD ( FunD (
[ [
@ -1102,11 +1061,11 @@ struct
(wrS @@ drf @@ v3) (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 @@ vg1) #.
(rdS @@ drf @@ vg3) #. (rdS @@ drf @@ vg2) #.
(rdS @@ drf @@ vg5) #. (rdS @@ drf @@ vg3)
(rdS @@ drf @@ vg7)
); );
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
@ -1116,13 +1075,9 @@ struct
let%expect_test "presentation test 1 (simple types), dsl" = let%expect_test "presentation test 1 (simple types), dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw;
defg (rfT uT_r_aw); (* x *) defg (rfT uT_r_aw); (* x *)
defg uT_r_aw;
defg (rfT uT_r_aw); (* y *) defg (rfT uT_r_aw); (* y *)
defg uT_r_aw;
defg (rfT uT_r_aw); (* z *) defg (rfT uT_r_aw); (* z *)
defg uT_r_aw;
defg (rfT uT_r_aw); (* k *) defg (rfT uT_r_aw); (* k *)
FunD ( (* f *) FunD ( (* f *)
[ [
@ -1156,14 +1111,14 @@ struct
(rdS @@ drf @@ v0) (rdS @@ drf @@ v0)
) )
], ],
let xV = vg1 in let xV = vg0 in
let yV = vg3 in let yV = vg1 in
let zV = vg5 in let zV = vg2 in
let kV = vg7 in let kV = vg3 in
let fF = vg8 in let fF = vg4 in
let wF = vg9 in let wF = vg5 in
let gF = vg10 in let gF = vg6 in
let rF = vg11 in let rF = vg7 in
(callS wF [pE xV]) #. (callS wF [pE xV]) #.
(callS rF [pE xV]) #. (callS rF [pE xV]) #.
(callS fF [pE xV; pE yV]) #. (callS fF [pE xV; pE yV]) #.

28
model_with_structures/tests.ml
View file

@ -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)]))] |}] [%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 ()); 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 ()); 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 ()); 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 ()); let%expect_test "simple call with forbidden write" = print_endline(prog_eval_t_simple_call_fbd_wr ());
[%expect {| [] |}] [%expect {| [] |}]
let%expect_test "simple call with write to ref" = print_endline(prog_eval_t_simple_call_ref_wr ()); 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 ()); let%expect_test "simple call with forbidden write to ref" = print_endline(prog_eval_t_simple_call_ref_fbd_wr ());
[%expect {| [] |}] [%expect {| [] |}]
let%expect_test "simple call with write to ref with fix" = print_endline(prog_eval_t_simple_call_ref_wr_with_fix ()); 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 ()); 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 ()); 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 ()); 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 ()); 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 ()); 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 ()); 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 ()); 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 *) (* - basic synthesis tests *)
@ -83,13 +83,13 @@ let%expect_test "simple synthesis test, reference forbidden write, no read write
(* - presentation tests *) (* - presentation tests *)
let%expect_test "presentation test 1 (simple types), eval" = print_endline(prog_eval_t_presentation_simple_tp ()); 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 ()); 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]] |}] [%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 ()); 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 ()); 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]] |}] [%expect {| [[Cp; Cp; Cp]; [Cp; Cp; Rf]; [Cp; Rf; Cp]; [Cp; Rf; Rf]] |}]

327
model_with_structures/tests_f.ml
View file

@ -158,101 +158,87 @@ 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 let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg, yg, fg, xd, yd, fd in fresh prog, yg, fg, yd, fd in
globals_min_ido xg & globals_min_ido yg &
yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, NeverWr)) &
yd == VarD (RefT (Rf, UnitT (Rd, NeverWr))) & yd == VarD (RefT (Rf, UnitT (Rd, NeverWr))) &
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))], fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
ReadS (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 }) prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg, yg, fg, xd, yd, fd in fresh prog, yg, fg, yd, fd in
globals_min_ido xg & globals_min_ido yg &
yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (NRd, AlwaysWr)) &
yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) &
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & 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 }) prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_simple_call_wr_rd _ = show(answer) (Stream.take (run q let prog_eval_t_simple_call_wr_rd _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg, yg, fg, xd, yd, fd in fresh prog, yg, fg, yd, fd in
globals_min_ido xg & globals_min_ido yg &
yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (NRd, MayWr)) &
yd == VarD (RefT (Rf, UnitT (NRd, MayWr))) & yd == VarD (RefT (Rf, UnitT (NRd, MayWr))) &
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
SeqS (WriteS (DerefP (VarP 0)), SeqS (WriteS (DerefP (VarP 0)),
ReadS (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 }) prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_simple_call_fbd_wr _ = show(answer) (Stream.take (run q let prog_eval_t_simple_call_fbd_wr _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg, yg, fg, xd, yd, fd in fresh prog, yg, fg, yd, fd in
globals_min_ido xg & globals_min_ido yg &
yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, MayWr)) &
yd == VarD (RefT (Rf, UnitT (Rd, MayWr))) & yd == VarD (RefT (Rf, UnitT (Rd, MayWr))) &
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))], fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
WriteS (DerefP (VarP 0))) & 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 }) prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg, yg, fg, xd, yd, fd in fresh prog, yg, fg, yd, fd in
globals_min_ido xg & globals_min_ido yg &
yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (NRd, AlwaysWr)) &
yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) &
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & 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 }) prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_simple_call_ref_fbd_wr _ = show(answer) (Stream.take (run q let prog_eval_t_simple_call_ref_fbd_wr _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg, yg, fg, xd, yd, fd in fresh prog, yg, fg, yd, fd in
globals_min_ido xg & globals_min_ido yg &
yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, AlwaysWr)) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))], fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), prog == Prg ([yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
ReadS (DerefP (VarP yg)))) & ReadS (DerefP (VarP yg)))) &
prog_evalo prog q }) prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg, yg, fg, xd, yd, fd in fresh prog, yg, fg, yd, fd in
globals_min_ido xg & globals_min_ido yg &
yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (NRd, AlwaysWr)) &
yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) &
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), prog == Prg ([yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
SeqS (WriteS (DerefP (VarP yg)), SeqS (WriteS (DerefP (VarP yg)),
ReadS (DerefP (VarP yg))))) & ReadS (DerefP (VarP yg))))) &
prog_evalo prog q }) prog_evalo prog q })
@ -260,53 +246,47 @@ let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q
let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg, yg, fg, f2g, xd, yd, fd, f2d in fresh prog, yg, fg, f2g, yd, fd, f2d in
globals_min_ido xg & globals_min_ido yg &
yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
f2g == Nat.s fg & f2g == Nat.s fg &
xd == VarD (UnitT (Rd, AlwaysWr)) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
SeqS (CallS (VarP fg, [PathE (VarP 0)]), SeqS (CallS (VarP fg, [PathE (VarP 0)]),
WriteS (DerefP (VarP 0)))) & WriteS (DerefP (VarP 0)))) &
prog == Prg ([xd; yd; fd; f2d], SeqS (CallS (VarP f2g, [PathE (VarP yg)]), prog == Prg ([yd; fd; f2d], SeqS (CallS (VarP f2g, [PathE (VarP yg)]),
ReadS (DerefP (VarP yg)))) & ReadS (DerefP (VarP yg)))) &
prog_evalo prog q }) prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_call_in_call_rec _ = show(answer) (Stream.take (run q let prog_eval_t_call_in_call_rec _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg, yg, fg, xd, yd, fd in fresh prog, yg, fg, yd, fd in
globals_min_ido xg & globals_min_ido yg &
yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, AlwaysWr)) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
SeqS (CallS (VarP fg, [PathE (VarP 0)]), SeqS (CallS (VarP fg, [PathE (VarP 0)]),
WriteS (DerefP (VarP 0)))) & WriteS (DerefP (VarP 0)))) &
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), prog == Prg ([yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
ReadS (DerefP (VarP yg)))) & ReadS (DerefP (VarP yg)))) &
prog_evalo prog q }) prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg, yg, fg, f2g, xd, yd, fd, f2d in fresh prog, yg, fg, f2g, yd, fd, f2d in
globals_min_ido xg & globals_min_ido yg &
yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
f2g == Nat.s fg & f2g == Nat.s fg &
xd == VarD (UnitT (Rd, AlwaysWr)) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
f2d == FunD ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))], f2d == FunD ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
prog == Prg ([xd; yd; fd; f2d], SeqS (CallS (VarP fg, [PathE (VarP yg)]), prog == Prg ([yd; fd; f2d], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
SeqS (CallS (VarP f2g, [PathE (VarP yg)]), SeqS (CallS (VarP f2g, [PathE (VarP yg)]),
ReadS (DerefP (VarP yg))))) & ReadS (DerefP (VarP yg))))) &
prog_evalo prog q }) prog_evalo prog q })
@ -314,16 +294,14 @@ let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q
let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg, yg, fg, xd, yd, fd in fresh prog, yg, fg, yd, fd in
globals_min_ido xg & globals_min_ido yg &
yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, AlwaysWr)) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))], fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
SeqS (WriteS (VarP xg), SeqS (WriteS (DerefP (VarP yg)),
ReadS (DerefP (VarP 0)))) & ReadS (DerefP (VarP 0)))) &
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), prog == Prg ([yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
ReadS (DerefP (VarP yg)))) & ReadS (DerefP (VarP yg)))) &
prog_evalo prog q prog_evalo prog q
}) })
@ -331,21 +309,17 @@ let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q
let prog_eval_t_call_with_rd_wr_2_args _ = show(answer) (Stream.take (run q let prog_eval_t_call_with_rd_wr_2_args _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg, yg, x2g, y2g, fg, xd, yd, x2d, y2d, fd in fresh prog, yg, y2g, fg, yd, y2d, fd in
globals_min_ido xg & globals_min_ido yg &
yg == Nat.s xg & y2g == Nat.s yg &
x2g == Nat.s yg &
y2g == Nat.s x2g &
fg == Nat.s y2g & fg == Nat.s y2g &
xd == VarD (UnitT (Rd, AlwaysWr)) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
x2d == VarD (UnitT (Rd, AlwaysWr)) &
y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)));
(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
SeqS (ReadS (DerefP (VarP 0)), SeqS (ReadS (DerefP (VarP 0)),
WriteS (DerefP (VarP 1)))) & WriteS (DerefP (VarP 1)))) &
prog == Prg ([xd; yd; x2d; y2d; fd], prog == Prg ([yd; y2d; fd],
CallS (VarP fg, [PathE (VarP yg); CallS (VarP fg, [PathE (VarP yg);
PathE (VarP y2g)])) & PathE (VarP y2g)])) &
prog_evalo prog q 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 let prog_eval_t_call_with_dif_mods_cp _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg, yg, fresh prog, yg, y2g, y3g, y4g,
x2g, y2g,
x3g, y3g,
x4g, y4g,
fg, fg,
xd, yd, yd, y2d, y3d, y4d,
x2d, y2d,
x3d, y3d,
x4d, y4d,
fd, fd,
fstmts, fstmts,
stmts in stmts in
globals_min_ido xg & globals_min_ido yg &
yg == Nat.s xg & y2g == Nat.s yg &
x2g == Nat.s yg & y3g == Nat.s y2g &
y2g == Nat.s x2g & y4g == Nat.s y3g &
x3g == Nat.s y2g &
y3g == Nat.s x3g &
x4g == Nat.s y3g &
y4g == Nat.s x4g &
fg == Nat.s y4g & fg == Nat.s y4g &
xd == VarD (UnitT (Rd, AlwaysWr)) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
x2d == VarD (UnitT (Rd, AlwaysWr)) &
y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
x3d == VarD (UnitT (Rd, AlwaysWr)) &
y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
x4d == VarD (UnitT (Rd, AlwaysWr)) &
y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
seqo [ReadS (DerefP (VarP 1)); seqo [ReadS (DerefP (VarP 1));
ReadS (DerefP (VarP 3)); 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 y2g));
ReadS (DerefP (VarP y3g)); ReadS (DerefP (VarP y3g));
ReadS (DerefP (VarP y4g))] stmts & ReadS (DerefP (VarP y4g))] stmts &
prog == Prg ([xd; yd; prog == Prg ([yd; y2d; y3d; y4d;
x2d; y2d;
x3d; y3d;
x4d; y4d;
fd], fd],
stmts) & stmts) &
prog_evalo prog q 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 let prog_eval_t_call_with_dif_mods_rf _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg, yg, fresh prog, yg, y2g, y3g, y4g,
x2g, y2g,
x3g, y3g,
x4g, y4g,
fg, fg,
xd, yd, yd, y2d, y3d, y4d,
x2d, y2d,
x3d, y3d,
x4d, y4d,
fd, fd,
fstmts, fstmts,
stmts in stmts in
globals_min_ido xg & globals_min_ido yg &
yg == Nat.s xg & y2g == Nat.s yg &
x2g == Nat.s yg & y3g == Nat.s y2g &
y2g == Nat.s x2g & y4g == Nat.s y3g &
x3g == Nat.s y2g &
y3g == Nat.s x3g &
x4g == Nat.s y3g &
y4g == Nat.s x4g &
fg == Nat.s y4g & fg == Nat.s y4g &
xd == VarD (UnitT (Rd, AlwaysWr)) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
x2d == VarD (UnitT (Rd, AlwaysWr)) &
y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
x3d == VarD (UnitT (Rd, AlwaysWr)) &
y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
x4d == VarD (UnitT (Rd, AlwaysWr)) &
y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
seqo [ReadS (DerefP (VarP 1)); seqo [ReadS (DerefP (VarP 1));
ReadS (DerefP (VarP 3)); 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 y2g));
ReadS (DerefP (VarP y3g)); ReadS (DerefP (VarP y3g));
ReadS (DerefP (VarP y4g))] stmts & ReadS (DerefP (VarP y4g))] stmts &
prog == Prg ([xd; yd; prog == Prg ([yd; y2d; y3d; y4d;
x2d; y2d;
x3d; y3d;
x4d; y4d;
fd], fd],
stmts) & stmts) &
prog_evalo prog q 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 let prog_eval_t_presentation_simple_tp _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xbg, xg, fresh prog, xg, yg, zg, kg,
ybg, yg,
zbg, zg,
kbg, kg,
fg, wg, gg, rg, fg, wg, gg, rg,
xbd, xd, xd, yd, zd, kd,
ybd, yd,
zbd, zd,
kbd, kd,
fd, wd, gd, rd, fd, wd, gd, rd,
fstmts, gstmts, fstmts, gstmts,
stmts in stmts in
globals_min_ido xbg & globals_min_ido xg &
xg == Nat.s xbg & yg == Nat.s xg &
ybg == Nat.s xg & zg == Nat.s yg &
yg == Nat.s ybg & kg == Nat.s zg &
zbg == Nat.s yg &
zg == Nat.s zbg &
kbg == Nat.s zg &
kg == Nat.s kbg &
fg == Nat.s kg & fg == Nat.s kg &
wg == Nat.s fg & wg == Nat.s fg &
gg == Nat.s wg & gg == Nat.s wg &
rg == Nat.s gg & rg == Nat.s gg &
xbd == VarD (UnitT (Rd, AlwaysWr)) &
xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
ybd == VarD (UnitT (Rd, AlwaysWr)) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
zbd == VarD (UnitT (Rd, AlwaysWr)) &
zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
kbd == VarD (UnitT (Rd, AlwaysWr)) &
kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
seqo [ReadS (DerefP (VarP 0)); seqo [ReadS (DerefP (VarP 0));
WriteS (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 fg, [PathE (VarP yg); PathE (VarP zg)]);
CallS (VarP rg, [PathE (VarP kg)]) CallS (VarP rg, [PathE (VarP kg)])
] stmts & ] stmts &
prog == Prg ([xbd; xd; prog == Prg ([xd; yd; zd; kd;
ybd; yd;
zbd; zd;
kbd; kd;
fd; wd; gd; rd], fd; wd; gd; rd],
stmts) & stmts) &
prog_evalo prog q 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 let prog_synt_t_presentation_simple_tp _ = show(answerCpCapList) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xbg, xg, fresh prog, xg, yg, zg, kg,
ybg, yg,
zbg, zg,
kbg, kg,
fg, wg, gg, rg, fg, wg, gg, rg,
xbd, xd, xd, yd, zd, kd,
ybd, yd,
zbd, zd,
kbd, kd,
fd, wd, gd, rd, fd, wd, gd, rd,
fstmts, gstmts, fstmts, gstmts,
stmts, stmts,
c_fx, c_fy, c_wx, c_gx, c_gy, c_rx, c_fx, c_fy, c_wx, c_gx, c_gy, c_rx,
st in st in
globals_min_ido xbg & globals_min_ido xg &
xg == Nat.s xbg & yg == Nat.s xg &
ybg == Nat.s xg & zg == Nat.s yg &
yg == Nat.s ybg & kg == Nat.s zg &
zbg == Nat.s yg &
zg == Nat.s zbg &
kbg == Nat.s zg &
kg == Nat.s kbg &
fg == Nat.s kg & fg == Nat.s kg &
wg == Nat.s fg & wg == Nat.s fg &
gg == Nat.s wg & gg == Nat.s wg &
rg == Nat.s gg & rg == Nat.s gg &
xbd == VarD (UnitT (Rd, AlwaysWr)) &
xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
ybd == VarD (UnitT (Rd, AlwaysWr)) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
zbd == VarD (UnitT (Rd, AlwaysWr)) &
zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
kbd == VarD (UnitT (Rd, AlwaysWr)) &
kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
seqo [ReadS (DerefP (VarP 0)); seqo [ReadS (DerefP (VarP 0));
WriteS (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 fg, [PathE (VarP yg); PathE (VarP zg)]);
CallS (VarP rg, [PathE (VarP kg)]) CallS (VarP rg, [PathE (VarP kg)])
] stmts & ] stmts &
prog == Prg ([xbd; xd; prog == Prg ([xd; yd; zd; kd;
ybd; yd;
zbd; zd;
kbd; kd;
fd; wd; gd; rd], fd; wd; gd; rd],
stmts) & stmts) &
prog_evalo prog st & prog_evalo prog st &
@ -771,14 +677,10 @@ let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q
fresh prog, fresh prog,
userT, dataT, timeT, requestT, userT, dataT, timeT, requestT,
requestArgsT, requestArgsT,
userE, dataE, timeE, requestE, requestVID,
userVID, dataVID, timeVID, requestVID,
sendFID, sendD, sendBranchStmts, sendStmts, sendFID, sendD, sendBranchStmts, sendStmts,
stmts in stmts in
globals_min_ido userVID & globals_min_ido requestVID &
dataVID == Nat.s userVID &
timeVID == Nat.s dataVID &
requestVID == Nat.s timeVID &
sendFID == Nat.s requestVID & sendFID == Nat.s requestVID &
p_rw_userTo userT & 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_rw_requestTo Cp Cp Cp requestT &
p_any_requestTo Cp Cp Cp requestArgsT & (* NOTE: for now *) 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, fresh data_p, time_p,
user_id_p, user_name_p in user_id_p, user_name_p in
deref_accesso 1 0 data_p & 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 ReadS time_gp
] stmts & ] stmts &
prog == Prg ([ prog == Prg ([
VarD userT;
VarD dataT;
VarD timeT;
VarD requestT; VarD requestT;
sendD sendD
], ],
@ -845,15 +739,11 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take (
fresh prog, fresh prog,
userT, dataT, timeT, requestT, userT, dataT, timeT, requestT,
requestArgsT, requestArgsT,
userE, dataE, timeE, requestE, requestVID,
userVID, dataVID, timeVID, requestVID,
sendFID, sendD, sendBranchStmts, sendStmts, sendFID, sendD, sendBranchStmts, sendStmts,
stmts, stmts,
st, c_u, c_d, c_t in st, c_u, c_d, c_t in
globals_min_ido userVID & globals_min_ido requestVID &
dataVID == Nat.s userVID &
timeVID == Nat.s dataVID &
requestVID == Nat.s timeVID &
sendFID == Nat.s requestVID & sendFID == Nat.s requestVID &
p_rw_userTo userT & 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_rw_requestTo Cp Cp Cp requestT &
p_any_requestTo c_u c_d c_t requestArgsT & (* NOTE: for now *) 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, fresh data_p, time_p,
user_id_p, user_name_p, user_surname_p in user_id_p, user_name_p, user_surname_p in
deref_accesso 1 0 data_p & deref_accesso 1 0 data_p &
@ -898,9 +783,6 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take (
ReadS time_gp ReadS time_gp
] stmts & ] stmts &
prog == Prg ([ prog == Prg ([
VarD userT;
VarD dataT;
VarD timeT;
VarD requestT; VarD requestT;
sendD sendD
], ],
@ -933,14 +815,8 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
userT, versionT, utilsT, userT, versionT, utilsT,
requestT, requestT,
moded_requestT, moded_requestT,
(* global vars init exprs *)
user_utilsE, user_infoE,
userE, versionE, utilsE,
requestE,
(* global vars ids *) (* global vars ids *)
user_utilsID, user_infoID, requestID,
userID, versionID, utilsID,
dataID, requestID,
(* function ids *) (* function ids *)
get_version_idID, get_version_idID,
updated_versionID, 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 *); RefT (Cp, uT_r_aw) (* 3 data *);
uT_r_aw (* 4 operation_date *)] & uT_r_aw (* 4 operation_date *)] &
moded_requestT == (Mode (In, NOut), requestT) & 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 *) (* global vars ids *)
globals_min_ido user_utilsID & globals_min_ido requestID &
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 &
(* function ids *) (* function ids *)
get_version_idID == Nat.s requestID & get_version_idID == Nat.s requestID &
updated_versionID == Nat.s get_version_idID & 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 & send_allF &
prog == Prg ([ prog == Prg ([
VarD user_utilsT;
VarD user_infoT;
VarD userT;
VarD versionT;
VarD utilsT;
VarD uT_r_aw; (* data *)
VarD requestT; VarD requestT;
FunD ([moded_requestT], get_version_idF); FunD ([moded_requestT], get_version_idF);
FunD ([moded_requestT], updated_versionF); FunD ([moded_requestT], updated_versionF);
@ -1220,14 +1072,7 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
userT, versionT, utilsT, userT, versionT, utilsT,
requestT, requestT,
(* moded_requestT, *) (* moded_requestT, *)
(* global vars init exprs *) requestID,
user_utilsE, user_infoE,
userE, versionE, utilsE,
requestE,
(* global vars ids *)
user_utilsID, user_infoID,
userID, versionID, utilsID,
dataID, requestID,
(* function ids *) (* function ids *)
get_version_idID, get_version_idID,
updated_versionID, updated_versionID,
@ -1252,26 +1097,8 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
rw_utilsTo utilsT & rw_utilsTo utilsT &
rw_requestTo Cp Cp Cp Cp Cp Cp requestT & rw_requestTo Cp Cp Cp Cp Cp Cp requestT &
(* moded_requestTo moded_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 *) (* global vars ids *)
globals_min_ido user_utilsID & globals_min_ido requestID &
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 &
(* function ids *) (* function ids *)
get_version_idID == Nat.s requestID & get_version_idID == Nat.s requestID &
updated_versionID == Nat.s get_version_idID & 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] & *) (* [gvi_c0; gvi_c1; gvi_c2; gvi_c3; gvi_c4; gvi_c5] & *)
prog == Prg ([ prog == Prg ([
VarD user_utilsT;
VarD user_infoT;
VarD userT;
VarD versionT;
VarD utilsT;
VarD uT_r_aw; (* data *)
VarD requestT; VarD requestT;
(* FunD ([mrT'], get_version_idF); *) (* FunD ([mrT'], get_version_idF); *)
(* FunD ([mrT'], updated_versionF); *) (* FunD ([mrT'], updated_versionF); *)