mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-06-11 03:38:15 +00:00
struct: synt. ref arg in call fix
This commit is contained in:
ProgramSnail
parent
68f2569922
commit
1bcf567839
4 changed files with 47 additions and 11 deletions
|
|
@ -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))])); *)
|
||||
|
|
|
|||
|
|
@ -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 &
|
||||
|
|
|
|||
|
|
@ -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))]] |}] *)
|
||||
|
|
|
|||
|
|
@ -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 *)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue