From 130079f7bd515a07707e70395b728607db7dfa50 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Fri, 8 May 2026 12:06:53 +0000 Subject: [PATCH 1/2] struct: synt. left & right fold fix (swap), simple var synt. tests, fixes, not working (yet) call test --- model_with_structures/analyzer.ml | 25 ++++--- model_with_structures/synthesizer.ml | 100 +++++++++++++------------ model_with_structures/tests.ml | 21 +++++- model_with_structures/tests_f.ml | 106 ++++++++++++++++++++++++++- 4 files changed, 191 insertions(+), 61 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 826bde5..248e366 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -519,12 +519,14 @@ struct [%expect {| done! |}] let%expect_test "simple var" = - prog_eval_noret ([VarD (UnitT (Rd, MayWr), UnitE)], ReadS (VarP globals_min_id)); + prog_eval_noret ([VarD (UnitT (Rd, MayWr), UnitE)], + ReadS (VarP globals_min_id)); Printf.printf "done!"; [%expect {| done! |}] - let%expect_test "simple var, no read" = - try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], ReadS (VarP globals_min_id)); + let%expect_test "simple var, forbidden read" = + try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], + ReadS (VarP globals_min_id)); [%expect.unreachable]); with Eval_error msg -> Printf.printf "%s" msg; [%expect {| read: spoiled value |}] @@ -537,19 +539,22 @@ struct [%expect {| done! |}] let%expect_test "simple var, write" = - prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], WriteS (VarP globals_min_id)); + prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], + WriteS (VarP globals_min_id)); Printf.printf "done!"; [%expect {| done! |}] - let%expect_test "simple var, no write" = - try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr), UnitE)], WriteS (VarP globals_min_id)); + let%expect_test "simple var, forbidden write" = + try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr), UnitE)], + WriteS (VarP globals_min_id)); [%expect.unreachable]); with Eval_error msg -> Printf.printf "%s" msg; [%expect {| write: write tag |}] let%expect_test "simple var, write & read" = - prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], SeqS (WriteS (VarP globals_min_id), - ReadS (VarP globals_min_id))); + prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], + SeqS (WriteS (VarP globals_min_id), + ReadS (VarP globals_min_id))); Printf.printf "done!"; [%expect {| done! |}] @@ -557,7 +562,7 @@ struct (* let%expect_test "simple call with read" = *) (* prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE); *) - (* FunD ([(In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0))], *) + (* FunD ([((In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0)))], *) (* CallS (VarP (globals_min_id + 1), *) (* [PathE (VarP globals_min_id)])); *) (* Printf.printf "done!"; *) @@ -566,7 +571,7 @@ struct (* let%expect_test "simple call with write" = *) (* prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE); *) (* VarD (RefT (Rf, (UnitT (Rd, MayWr))), RefE globals_min_id); *) - (* FunD ([(In, NOut), RefT (Cp, UnitT (Rd, MayWr))], WriteS (DerefP (VarP 0)))], *) + (* FunD ([((In, NOut), RefT (Cp, UnitT (Rd, MayWr)))], WriteS (DerefP (VarP 0)))], *) (* CallS (VarP (globals_min_id + 2), *) (* [PathE (VarP (globals_min_id + 1))])); *) (* Printf.printf "done!"; *) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index 1908033..6c50ed9 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -1,3 +1,6 @@ +(* NOTE: in previous models foldl & foldr are probably spapped + <- TODO: fix ? *) + module Relational = struct open GT @@ -145,9 +148,9 @@ struct module Decl = struct [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [%%ocanren_inject - type nonrec ((* 'd, *) 't, 'e, 'dl, 'mtl, 's) t = VarD of (* 'd * *) 't * 'e | FunD of (* 'd * *) 'dl * 'mtl * 's + type nonrec ((* 'd, *) 't, 'e, (* 'dl, *) 'mtl, 's) t = VarD of (* 'd * *) 't * 'e | FunD of (* 'd * 'dl * *) 'mtl * 's [@@deriving gt ~options:{ show; gmap }] - type ground = ((* Nat.ground, *) Type.ground, Expr.ground, Nat.ground List.ground, (Mode.ground * Type.ground) List.ground, Stmt.ground) t + type ground = ((* Nat.ground, *) Type.ground, Expr.ground, (* Nat.ground List.ground, *) (Mode.ground * Type.ground) List.ground, Stmt.ground) t ] end @@ -291,50 +294,40 @@ struct } - let rec list_foldlo f acc xs acc' = ocanren { - xs == [] & acc' == acc | - { fresh x', xs', acc_upd in - xs == x' :: xs' & - list_foldlo f acc xs' acc_upd & - f acc_upd x' acc' } - } - let rec list_foldro f acc xs acc' = ocanren { + xs == [] & acc' == acc | + { fresh x', xs', acc_upd in + xs == x' :: xs' & + list_foldro f acc xs' acc_upd & + f acc_upd x' acc' } + } + + let rec list_foldlo f acc xs acc' = ocanren { xs == [] & acc' == acc | { fresh x', xs', acc_upd in xs == x' :: xs' & f acc x' acc_upd & - list_foldro f acc_upd xs' acc' } + list_foldlo f acc_upd xs' acc' } (* TODO: inf search on swap, investigate *) } - let rec list_foldr2o f acc xs ys acc' = ocanren { - xs == [] & ys == [] & acc' == acc | - { fresh x', xs', y', ys', acc_upd in - xs == x' :: xs' & - ys == y' :: ys' & - f acc x' y' acc_upd & - list_foldr2o f acc_upd xs' ys' acc' } - } - let rec list_foldl2o f acc xs ys acc' = ocanren { xs == [] & ys == [] & acc' == acc | { fresh x', xs', y', ys', acc_upd in xs == x' :: xs' & ys == y' :: ys' & - list_foldl2o f acc xs' ys' acc_upd & - f acc_upd x' y' acc' } + f acc x' y' acc_upd & + list_foldl2o f acc_upd xs' ys' acc' } } - let rec list_foldr3o f acc xs ys zs acc' = ocanren { - xs == [] & ys == [] & zs == [] & acc' == acc | - { fresh x', xs', y', ys', z', zs', acc_upd in + let rec list_foldr2o f acc xs ys acc' = ocanren { + xs == [] & ys == [] & acc' == acc | + { fresh x', xs', y', ys', acc_upd in xs == x' :: xs' & ys == y' :: ys' & - zs == z' :: zs' & - f acc x' y' z' acc_upd & - list_foldr3o f acc_upd xs' ys' zs' acc' } + list_foldr2o f acc xs' ys' acc_upd & + f acc_upd x' y' acc' } } let rec list_foldl3o f acc xs ys zs acc' = ocanren { @@ -343,7 +336,17 @@ struct xs == x' :: xs' & ys == y' :: ys' & zs == z' :: zs' & - list_foldl3o f acc xs' ys' zs' acc_upd & + f acc x' y' z' acc_upd & + list_foldl3o f acc_upd xs' ys' zs' acc' } + } + + let rec list_foldr3o f acc xs ys zs acc' = ocanren { + xs == [] & ys == [] & zs == [] & acc' == acc | + { fresh x', xs', y', ys', z', zs', acc_upd in + xs == x' :: xs' & + ys == y' :: ys' & + zs == z' :: zs' & + list_foldr3o f acc xs' ys' zs' acc_upd & f acc_upd x' y' z' acc' } } @@ -608,24 +611,32 @@ struct let add_declo st x d st' = let open StEnv in let open Decl in + let open Value in + let open Type in ocanren { fresh mem, types, vals in st == StEnv (mem, types, vals) & { { fresh tp, e, v, - mem_with_v_cp, mem_cp, v_cp, - mem_with_id_add, mem_add, id_add, + mem_cp, v_cp, + mem_add, id_add, types', vals' in d == VarD (tp, e) & exprvalo mem vals e v & - valcopyo mem v tp mem_with_v_cp & - Pair.pair mem_cp v_cp == mem_with_v_cp & - mem_addo mem_cp v_cp mem_with_id_add & - Pair.pair mem_add id_add == mem_with_id_add & + valcopyo mem v tp (Pair.pair mem_cp v_cp) & + mem_addo mem_cp v_cp (Pair.pair mem_add id_add) & types_glob_addo types x tp types' & vals_glob_addo vals x id_add vals' & + st' == StEnv (mem_add, types', vals') } | + { fresh tps, s, + mem_add, id_add, + types', vals' in + d == FunD (tps, s) & + mem_addo mem (FunV [s]) (Pair.pair mem_add id_add) & + types_glob_addo types x (FunT tps) types' & + vals_glob_addo vals x id_add vals' & st' == StEnv (mem_add, types', vals') - } + } } } @@ -644,7 +655,7 @@ struct } (* TODO: better way ??? *) - let globals_min_ido x = ocanren { x == 1000 } + let globals_min_ido x = ocanren { x == 10 } let prog_init_foldero st_with_id d st_with_id' = ocanren { @@ -845,8 +856,8 @@ struct { fresh f, es, v, tp, glob_tps, _tps, glob_vs, _vs, - types', vals', - fstmts, tps, st', + types_call, vals_call, + fstmts, tps, st_call, state_with_args, _arg_id, _states_evaled, mem_spoiled in s == CallS (f, es) & @@ -854,13 +865,13 @@ struct pathtypeo types f tp & types == TypesEnv (glob_tps, _tps) & vals == ValsEnv (glob_vs, _vs) & - types' == TypesEnv (glob_tps, glob_tps) & - vals' == ValsEnv (glob_vs, glob_vs) & + types_call == TypesEnv (glob_tps, glob_tps) & + vals_call == ValsEnv (glob_vs, glob_vs) & v == FunV fstmts & tp == FunT tps & - st' == StEnv (mem, types', vals') & + st_call == StEnv (mem, types_call, vals_call) & list_foldl2o (stmt_addarg_foldero vals) - (Std.pair st' 0) tps es + (Std.pair st_call 0) tps es (Std.pair state_with_args _arg_id) & List.mapo (stmt_evalo state_with_args) fstmts _states_evaled & (* TODO: FIXME check left or right order *) @@ -907,12 +918,9 @@ struct let prog_evalo prog st' = let open Prg in - let open Stmt in ocanren { fresh decls, s, init_st in prog == Prg (decls, s) & - decls == [] & - s == SkipS & prog_inito prog init_st & stmt_evalo init_st s st' } diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index 8e3ae24..14d1bd0 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -2,8 +2,27 @@ open Tests_f open Synthesizer open Relational -let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); + (* - basic var tests *) + +let%expect_test "prog eval test: empty" = print_endline (prog_eval_t_empty ()); [%expect {| [StEnv (MemEnv ([], O), TypesEnv ([], []), ValsEnv ([], []))] |}] +let%expect_test "prog eval test: simple var" = print_endline(prog_eval_t_simple_var ()); + [%expect {| [StEnv (MemEnv ([ZeroV], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] +let%expect_test "simple var, forbidden read" = print_endline(prog_eval_t_simple_var_fbd_rd ()); + [%expect {| [] |}] +let%expect_test "simple vars, no read & read" = print_endline(prog_eval_t_simple_vars_fbd_rd_rd ()); + [%expect {| [StEnv (MemEnv ([ZeroV; BotV], S (S (O))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), UnitT (Rd, MayWr)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), UnitT (Rd, 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 (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)]))] |}] +let%expect_test "simple var, write" = print_endline(prog_eval_t_simple_var_wr ()); + [%expect {| [StEnv (MemEnv ([ZeroV], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), 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 (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] +let%expect_test "simple var, forbidden write" = print_endline(prog_eval_t_simple_var_fbd_wr ()); + [%expect {| [] |}] +let%expect_test "simple var, write & read" = print_endline(prog_eval_t_simple_var_wr_rd ()); + [%expect {| [StEnv (MemEnv ([ZeroV], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), 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 (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}] + + (* - basic call tests *) + +let%expect_test "simple call with read" = print_endline(prog_eval_t_simple_call_rd ()); + [%expect {| [123] |}] (* type tests *) (* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 6737d97..69a5113 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -4,17 +4,115 @@ open GT open OCanren open OCanren.Std +open Prg +open Stmt +open Decl +open Type +open Expr +open Path +open ReadCap +open WriteCap +open InCap +open OutCap +open Mode + @type answer = StEnv.ground GT.list with show -let prog_eval_t1 _ = show(answer) (Stream.take (run q - (fun q -> let open Prg in - let open Stmt in - ocanren { + (* - shortcuts *) + +(* TODO *) + + (* - basic var tests *) + +let prog_eval_t_empty _ = show(answer) (Stream.take (run q + (fun q -> ocanren { fresh prog in prog == Prg ([], SkipS) & prog_evalo prog q}) (fun q -> q#reify (StEnv.prj_exn)))) +let prog_eval_t_simple_var _ = show(answer) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg in + globals_min_ido xg & + prog == Prg ([VarD (UnitT (Rd, MayWr), UnitE)], + ReadS (VarP xg)) & + prog_evalo prog q }) + (fun q -> q#reify (StEnv.prj_exn)))) + +(* NOTE: does not work well for tests :( *) +(* let prog_eval_t2_simple_var_ans _ = show(answer) (Stream.take (run q *) + (* (fun q -> ocanren { *) + (* fresh xg in *) + (* globals_min_ido xg & *) + (* q == StEnv (MemEnv ([ZeroV], 1), *) + (* TypesEnv ([(xg, UnitT (Rd, MayWr))], *) + (* [(xg, UnitT (Rd, MayWr))]), *) + (* ValsEnv ([(xg, 0)], [(xg, 0)])) }) *) + (* (fun q -> q#reify (StEnv.prj_exn)))) *) + +let prog_eval_t_simple_var_fbd_rd _ = show(answer) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg in + globals_min_ido xg & + prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)], + ReadS (VarP xg)) & + prog_evalo prog q }) + (fun q -> q#reify (StEnv.prj_exn)))) + +let prog_eval_t_simple_vars_fbd_rd_rd _ = show(answer) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg, yg in + globals_min_ido xg & + yg == Nat.s xg & + prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE); + VarD (UnitT (Rd, MayWr), UnitE)], + ReadS (VarP yg)) & + prog_evalo prog q }) + (fun q -> q#reify (StEnv.prj_exn)))) + +let prog_eval_t_simple_var_wr _ = show(answer) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg in + globals_min_ido xg & + prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)], + WriteS (VarP xg)) & + prog_evalo prog q }) + (fun q -> q#reify (StEnv.prj_exn)))) + +let prog_eval_t_simple_var_fbd_wr _ = show(answer) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg in + globals_min_ido xg & + prog == Prg ([VarD (UnitT (NRd, NeverWr), UnitE)], + WriteS (VarP xg)) & + prog_evalo prog q }) + (fun q -> q#reify (StEnv.prj_exn)))) + +let prog_eval_t_simple_var_wr_rd _ = show(answer) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg in + globals_min_ido xg & + prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)], + SeqS (WriteS (VarP xg), + ReadS (VarP xg))) & + prog_evalo prog q }) + (fun q -> q#reify (StEnv.prj_exn)))) + + (* - basic call tests *) + +let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg, fg, xd, fd, st in + globals_min_ido xg & + fg == Nat.s xg & + xd == VarD (UnitT (Rd, NeverWr), UnitE) & + fd == FunD ([(Mode (In, NOut), UnitT (Rd, NeverWr))], ReadS (VarP 0)) & + prog == Prg ([xd; fd], CallS (VarP fg, [PathE (VarP xg)])) & + prog_evalo prog q + }) + (fun q -> q#reify (StEnv.prj_exn)))) + (* @type answerArgs = (Arg.ground List.ground) GT.list with show *) (* @type answerValue = Value.ground GT.list with show *) (* @type answerNat = Nat.ground GT.list with show *) From 68f2569922986334894d303b68b9b93d6db6db31 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Fri, 8 May 2026 12:46:53 +0000 Subject: [PATCH 2/2] struct: synt. ambuity fixes, simple read call test --- model_with_structures/synthesizer.ml | 18 +++++++++++------- model_with_structures/tests.ml | 2 +- 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index 6c50ed9..b100a82 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -686,12 +686,12 @@ struct let open Mode in let open CopyCap in ocanren { - { r == NRd | v == ZeroV } & - { r == NRd | is_ino m } & - { is_not_outo m | w == AlwaysWr } & + { r == NRd | r == Rd & v == ZeroV } & + { r == NRd | r == Rd & is_ino m } & + { is_not_outo m | is_outo m & w == AlwaysWr } & { w == NeverWr | - { is_not_outo m & c == Cp } | - w' == AlwaysWr } & + w =/= NeverWr & w' =/= AlwaysWr & is_not_outo m & c == Cp | + w =/= NeverWr & w' == AlwaysWr } & is_trivial_vo v } @@ -721,8 +721,12 @@ struct { is_outo m & w == AlwaysWr & mem_with_v' == Std.pair mem ZeroV } | - { { is_outo m | c == Cp | w == NeverWr } & - { is_not_outo m | w == MayWr | w == NeverWr } & + { { is_outo m | + 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 } } } | { fresh ts, us, _stmts in diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index 14d1bd0..f82b186 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -22,7 +22,7 @@ let%expect_test "simple var, write & read" = print_endline(prog_eval_t_simple_va (* - basic call tests *) 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 *) (* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *)