st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-06-11 03:38:15 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

struct: synt. tests fixes, simple forward tests done

Browse source
This commit is contained in:
ProgramSnail 2026-05-09 14:35:21 +00:00
parent 2cc87d74df
commit 10cea01338
2 changed files with 33 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

21
model_with_structures/tests.ml
View file

@ -42,6 +42,27 @@ let%expect_test "simple call with write to ref" = print_endline(prog_eval_t_simp
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 ());
[%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); ZeroV], 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, 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))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), 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)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(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)], [(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)]))] |}]
let%expect_test "call inside call" = print_endline(prog_eval_t_call_in_call ());
[%expect {| [StEnv (MemEnv ([FunV ([SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]); FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); ZeroV], 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 (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), 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)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), 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)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (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 (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)], [(S (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 (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)]))] |}]
let%expect_test "call to fix after call" = print_endline(prog_eval_t_fix_call_after_call ());
[%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); ZeroV], 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))], [(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 (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)], [(S (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 (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)]))] |}]
let%expect_test "simple call with global variable usage" = print_endline(prog_eval_t_call_with_glob_usage ());
[%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (VarP (S (S (S (S (S (S (S (S (S (S (O)))))))))))), ReadS (DerefP (VarP (O))))]); RefV (O); ZeroV], 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, 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))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, 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 (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)], [(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)]))] |}]
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 ([SeqS (ReadS (DerefP (VarP (O))), WriteS (DerefP (VarP (S (O)))))]); RefV (O); ZeroV; RefV (O); BotV], 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))], [(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 (O))))); (S (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 (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)], [(S (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 (S (O))))))))))))), 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)]))] |}]
(* TODO: dif. ref modifiers tests ? *)
(* TODO: synthesis tests ? *)
(* type tests *) (* type tests *)
(* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *) (* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *)
(* let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}] *) (* let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}] *)

18
model_with_structures/tests_f.ml
View file

@ -227,9 +227,9 @@ let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q
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))) &
f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))], f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))],
SeqS (CallS (VarP f2g, [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 f2g, [PathE (VarP yg)]), prog == Prg ([xd; 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))))
@ -243,11 +243,11 @@ let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q
f2g == Nat.s fg & f2g == Nat.s fg &
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, 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 (Rd, AlwaysWr)))], f2d == FunD ([(Mode (In, Out), 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 ([xd; 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 })
@ -261,7 +261,7 @@ let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))], fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))],
SeqS (WriteS (VarP xg), SeqS (WriteS (VarP xg),
ReadS (DerefP (VarP 0)))) & ReadS (DerefP (VarP 0)))) &
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
@ -270,7 +270,7 @@ let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q
}) })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
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, st in fresh prog, xg, yg, x2g, y2g, fg, xd, yd, x2d, y2d, fd, st in
globals_min_ido xg & globals_min_ido xg &
@ -286,7 +286,9 @@ let prog_eval_t_call_with_rd_wr_2_args_ = show(answer) (Stream.take (run q
(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; fd], CallS (VarP fg, [PathE (VarP yg); PathE (VarP y2g)])) & prog == Prg ([xd; yd; x2d; y2d; fd],
CallS (VarP fg, [PathE (VarP yg);
PathE (VarP y2g)])) &
prog_evalo prog q prog_evalo prog q
}) })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))