From 1bcf5678390bcc115e3076406d199776fc972703 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Fri, 8 May 2026 14:50:36 +0000 Subject: [PATCH] struct: synt. ref arg in call fix --- model_with_structures/analyzer.ml | 4 ++-- model_with_structures/synthesizer.ml | 17 +++++++-------- model_with_structures/tests.ml | 6 ++++++ model_with_structures/tests_f.ml | 31 ++++++++++++++++++++++++++++ 4 files changed, 47 insertions(+), 11 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 248e366..039f8e5 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -290,7 +290,7 @@ struct (r != Rd || v == ZeroV) && (r != Rd || fst m == In) && (snd m != Out || w == AlwaysWr) && - (* TODO: check *) + (* TODO: FIXME: check *) ((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr) && is_trivial_v v @@ -570,7 +570,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); *) + (* VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE globals_min_id); *) (* FunD ([((In, NOut), RefT (Cp, UnitT (Rd, MayWr)))], WriteS (DerefP (VarP 0)))], *) (* CallS (VarP (globals_min_id + 2), *) (* [PathE (VarP (globals_min_id + 1))])); *) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index b100a82..09b7eb4 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -482,14 +482,11 @@ struct v == RefV id & tp == RefT (c, tp') & { { c == Rf & mem_with_id' == Std.pair mem v } | - { fresh v, mem_cp, v_cp, mem_with_v_cp, - mem_add, id_add, mem_with_id_add in + { fresh v', mem_cp, v_cp, mem_add, id_add in c == Cp & - mem_geto mem id v & - valcopyo mem v tp mem_with_v_cp & - Std.pair mem v_cp == mem_with_v_cp & - mem_addo mem_cp v_cp mem_with_id_add & - Std.pair mem_add id_add == mem_with_id_add & + mem_geto mem id v' & + valcopyo mem v' tp' (Std.pair mem_cp v_cp) & + mem_addo mem_cp v_cp (Std.pair mem_add id_add) & mem_with_id' == (mem_add, RefV id_add) } } } | { fresh vs, tps, init_mem_with_vs, mem_with_vs', mem', vs' in v == TupleV vs & @@ -877,11 +874,13 @@ struct list_foldl2o (stmt_addarg_foldero vals) (Std.pair st_call 0) tps es (Std.pair state_with_args _arg_id) & - List.mapo (stmt_evalo state_with_args) fstmts _states_evaled & + (* List.mapo (stmt_evalo state_with_args) fstmts _states_evaled & *) (* TODO: FIXME check left or right order *) list_foldl2o (stmt_eval_spoil_foldero types vals) mem tps es mem_spoiled & - st' == StEnv (mem_spoiled, types, vals) } | + (* st' == state_with_args *) + st' == StEnv (mem_spoiled, types, vals) + } | { fresh p, tp, _r, w, x, id, v, mem_upd, v_upd, mem_set in s == WriteS p & diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index f82b186..5b0698c 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -24,6 +24,12 @@ let%expect_test "simple var, write & read" = print_endline(prog_eval_t_simple_va let%expect_test "simple call with read" = print_endline(prog_eval_t_simple_call_rd ()); [%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)]))] |}] +let%expect_test "simple call with ref read" = print_endline(prog_eval_t_simple_call_rd_ref ()); + [%expect {| [StEnv (MemEnv ([FunV ([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 write" = print_endline(prog_eval_t_simple_call_wr ()); + [%expect {| [StEnv (MemEnv ([FunV ([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)]))] |}] + (* type tests *) (* 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))]] |}] *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 69a5113..355bada 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -10,6 +10,7 @@ open Decl open Type open Expr open Path +open CopyCap open ReadCap open WriteCap open InCap @@ -113,6 +114,36 @@ let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q }) (fun q -> q#reify (StEnv.prj_exn)))) +let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg, yg, fg, xd, yd, fd, st in + globals_min_ido xg & + yg == Nat.s xg & + fg == Nat.s yg & + xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & + fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))], + ReadS (DerefP (VarP 0))) & + prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & + prog_evalo prog q + }) + (fun q -> q#reify (StEnv.prj_exn)))) + +let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q + (fun q -> ocanren { + fresh prog, xg, yg, fg, xd, yd, fd, st in + globals_min_ido xg & + yg == Nat.s xg & + fg == Nat.s yg & + xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & + fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))], + ReadS (DerefP (VarP 0))) & + prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & + 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 *)