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. ambuity fixes, simple read call test

Browse source
This commit is contained in:
ProgramSnail 2026-05-08 12:46:53 +00:00
parent 130079f7bd
commit 68f2569922
2 changed files with 12 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

18
model_with_structures/synthesizer.ml
View file

@ -686,12 +686,12 @@ struct
let open Mode in let open Mode in
let open CopyCap in let open CopyCap in
ocanren { ocanren {
{ r == NRd | v == ZeroV } & { r == NRd | r == Rd & v == ZeroV } &
{ r == NRd | is_ino m } & { r == NRd | r == Rd & is_ino m } &
{ is_not_outo m | w == AlwaysWr } & { is_not_outo m | is_outo m & w == AlwaysWr } &
{ w == NeverWr | { w == NeverWr |
{ is_not_outo m & c == Cp } | w =/= NeverWr & w' =/= AlwaysWr & is_not_outo m & c == Cp |
w' == AlwaysWr } & w =/= NeverWr & w' == AlwaysWr } &
is_trivial_vo v is_trivial_vo v
} }
@ -721,8 +721,12 @@ struct
{ is_outo m & { is_outo m &
w == AlwaysWr & w == AlwaysWr &
mem_with_v' == Std.pair mem ZeroV } | mem_with_v' == Std.pair mem ZeroV } |
{ { is_outo m | c == Cp | w == NeverWr } & { { is_outo m |
{ is_not_outo m | w == MayWr | w == NeverWr } & is_not_outo m & c == Cp |
is_not_outo m & c == Rf & w == NeverWr } &
{ is_not_outo m |
is_outo m & w == MayWr |
is_outo m & w == NeverWr } &
mem_with_v' == Std.pair mem v } mem_with_v' == Std.pair mem v }
} } | } } |
{ fresh ts, us, _stmts in { fresh ts, us, _stmts in

2
model_with_structures/tests.ml
View file

@ -22,7 +22,7 @@ let%expect_test "simple var, write & read" = print_endline(prog_eval_t_simple_va
(* - basic call tests *) (* - basic call tests *)
let%expect_test "simple call with read" = print_endline(prog_eval_t_simple_call_rd ()); let%expect_test "simple call with read" = print_endline(prog_eval_t_simple_call_rd ());
[%expect {| [123] |}] [%expect {| [StEnv (MemEnv ([FunV ([ReadS (VarP (O))]); ZeroV], S (S (O))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), UnitT (Rd, NeverWr))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, NeverWr))], [(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), FunT ([(Mode (In, NOut), UnitT (Rd, NeverWr))])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, NeverWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
(* type tests *) (* 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)] |}] *)