diff --git a/simplest_model_with_mods/analyzer_cap.ml b/simplest_model_with_mods/analyzer_cap.ml index b4c3898..84c6623 100644 --- a/simplest_model_with_mods/analyzer_cap.ml +++ b/simplest_model_with_mods/analyzer_cap.ml @@ -131,18 +131,22 @@ struct else let state_ext = env_add state id arg_tag mem_id in mem_set state_ext id BotV + (* TODO: FIXME: not enough tests on incorrect const cast (passed without ref or out check) *) (* TODO; FIXME: forbid duplicates, collect lists of all spoils & checks ? *) let st_spoil_by_args (state : state) (arg_tags : tag list) (args : data list) : state = match state with (env, mem, mem_len, _visited) -> let state_before = state in let spoil_folder (state : state) (tag : tag) (id : data) : state = let parent_tag = fst (env_get state id) in - if is_write tag > is_write parent_tag then raise @@ Incorrect_const_cast id - else let state = if is_read tag then (mem_check state_before id; state) else state (* NOTE: state override *) + (* NOTE: replaced with later condition *) + (* if is_write tag > is_write parent_tag && (not (is_copy tag) || is_out tag) then raise @@ Incorrect_const_cast idi else *) + let state = if is_read tag then (mem_check state_before id; state) else state (* NOTE: state override *) in if not @@ is_write tag then state else match is_out tag with - | true -> mem_set state id UnitV + | true -> if not @@ is_write parent_tag then raise @@ Incorrect_const_cast id + else mem_set state id UnitV | false -> if is_copy tag then state + else if not @@ is_write parent_tag then raise @@ Incorrect_const_cast id else mem_set state id BotV in List.fold_left2 spoil_folder state arg_tags args diff --git a/simplest_model_with_mods/synthesizer.ml b/simplest_model_with_mods/synthesizer.ml index 328d947..93c8c46 100644 --- a/simplest_model_with_mods/synthesizer.ml +++ b/simplest_model_with_mods/synthesizer.ml @@ -116,37 +116,59 @@ struct let open OutCap in ocanren { Tag (NRd, NWr, Ref, In, NOut) } + (* constraints *) + let x_any tag = let open InCap in + let open OutCap in + ocanren { fresh r, w, c in + tag == Tag (r, w, c, NIn, NOut) } + let i_any tag = let open InCap in + let open OutCap in + ocanren { fresh r, w, c in + tag == Tag (r, w, c, In, NOut) } + let o_any tag = let open InCap in + let open OutCap in + ocanren { fresh r, w, c in + tag == Tag (r, w, c, NIn, Out) } + let io_any tag = let open InCap in + let open OutCap in + ocanren { fresh r, w, c in + tag == Tag (r, w, c, In, Out) } + (* accessors *) let is_reado tag = let open ReadCap in ocanren { - fresh w_, c_, i_, o_ in - tag == Tag (Rd, w_, c_, i_, o_) } + fresh w_, c_, i_, o_ in + tag == Tag (Rd, w_, c_, i_, o_) } let is_not_reado tag = let open ReadCap in ocanren { - fresh w_, c_, i_, o_ in - tag == Tag (NRd, w_, c_, i_, o_) } + fresh w_, c_, i_, o_ in + tag == Tag (NRd, w_, c_, i_, o_) } let is_writeo tag = let open WriteCap in ocanren { - fresh r_, c_, i_, o_ in - tag == Tag (r_, Wr, c_, i_, o_) } + fresh r_, c_, i_, o_ in + tag == Tag (r_, Wr, c_, i_, o_) } let is_not_writeo tag = let open WriteCap in ocanren { - fresh r_, c_, i_, o_ in - tag == Tag (r_, NWr, c_, i_, o_) } + fresh r_, c_, i_, o_ in + tag == Tag (r_, NWr, c_, i_, o_) } let is_refo tag = let open CopyCap in ocanren { - fresh r_, w_, i_, o_ in + fresh r_, w_, i_, o_ in tag == Tag (r_, w_, Ref, i_, o_) } let is_valueo tag = let open CopyCap in ocanren { - fresh r_, w_, i_, o_ in - tag == Tag (r_, w_, Val, i_, o_) } + fresh r_, w_, i_, o_ in + tag == Tag (r_, w_, Val, i_, o_) } let is_ino tag = let open InCap in ocanren { - fresh r_, w_, c_, o_ in - tag == Tag (r_, w_, c_, In, o_) } + fresh r_, w_, c_, o_ in + tag == Tag (r_, w_, c_, In, o_) } let is_not_ino tag = let open InCap in ocanren { - fresh r_, w_, c_, o_ in - tag == Tag (r_, w_, c_, NIn, o_) } + fresh r_, w_, c_, o_ in + tag == Tag (r_, w_, c_, NIn, o_) } let is_outo tag = let open OutCap in ocanren { - fresh r_, w_, c_, i_ in + fresh r_, w_, c_, i_ in tag == Tag (r_, w_, c_, i_, Out) } let is_not_outo tag = let open OutCap in ocanren { - fresh r_, w_, c_, i_ in - tag == Tag (r_, w_, c_, i_, NOut) } + fresh r_, w_, c_, i_ in + tag == Tag (r_, w_, c_, i_, NOut) } + + let eq_copyo tag cp = let open CopyCap in ocanren { + fresh r_, w_, i_, o_ in + tag == Tag (r_, w_, cp, i_, o_) } module Test = struct @type answer = logic GT.list with show @@ -161,23 +183,6 @@ struct end end - (* TODO: tmp *) - module Tag' = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - [%%ocanren_inject - type nonrec t = Ref | Val - [@@deriving gt ~options:{ show; gmap }] - type nonrec ground = t - ] - - module Test = struct - @type answer = logic GT.list with show - - let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == Ref}) - (fun q -> q#reify reify))) - end - end - module Stmt = struct [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [%%ocanren_inject @@ -433,8 +438,8 @@ struct let tag_correcto tg = let open Tag in ocanren { - {is_not_outo tg | is_writeo tg} & - {is_not_reado tg | is_ino tg} + {is_not_outo tg | { is_outo tg & is_writeo tg } } & + {is_not_reado tg | { is_reado tg & is_ino tg } } } let st_add_argo state state_before id arg_tag arg state'' = @@ -456,7 +461,7 @@ struct arg == LValue arg' & env_geto state_before id parent_tag mem_id & env_addo state id arg_tag mem_id state' & - { is_not_writeo arg_tag | is_writeo parent_tag } & + { is_not_writeo arg_tag | { is_writeo arg_tag & is_writeo parent_tag } } & { { is_reado arg_tag & state' == state'' } | { is_not_reado arg_tag & mem_seto state' id Bot state'' } @@ -473,14 +478,16 @@ struct fresh env, mem, mem_len, _visited, parent_tg, _mem_id in state == St (env, mem, mem_len, _visited) & env_geto state id parent_tg _mem_id & - { is_not_writeo tg | is_writeo parent_tg } & - { is_not_reado tg | mem_checko state_before id } & + (* NOTE: replaced with later condition (this one needs fix) *) + (* { is_not_writeo tg | { is_writeo tg & is_writeo parent_tg } } & *) + { is_not_reado tg | { is_reado tg & mem_checko state_before id } } & { { is_not_writeo tg & state == state'} | - { is_outo tg & mem_seto state id Unit state' } | - { is_not_outo tg & is_valueo tg & state == state' } | - { is_not_outo tg & is_refo tg & mem_seto state id Bot state' } - } & - mem_seto state id Bot state' + { is_writeo tg & { + { is_outo tg & is_writeo parent_tg & mem_seto state id Unit state' } | + { is_not_outo tg & is_valueo tg & state == state' } | + { is_not_outo tg & is_refo tg & is_writeo parent_tg & mem_seto state id Bot state' } + } } + } } let st_spoil_by_argso state arg_tags args state' = @@ -529,7 +536,6 @@ struct ocanren { fresh env, mem, mem_len, visited, visited' in state == St (env, mem, mem_len, visited) & - List.membero visited f_id & visited' == f_id :: visited & state' == St (env,mem, mem_len, visited') } @@ -538,6 +544,7 @@ struct let open Stmt in let open Value in let open FunDecl in + let open Tag in ocanren { { fresh f_id, args, f, args', state_after_call, state_with_visited, arg_tags, _body in stmt == Call (f_id, args) & @@ -548,11 +555,12 @@ struct eval_funo state prog f args' state_after_call & (* NOTE: tmp simplification for less branching (TODO?) *) visited_addo state_after_call f_id state_with_visited & - st_spoil_by_argso state_with_visited arg_tags args state'} | + st_spoil_by_argso state_with_visited arg_tags args state' } | { fresh id in stmt == Read id & mem_checko state id & state == state' } | { fresh id, tag, _mem_id in - stmt === Write id & + stmt == Write id & env_geto state id tag _mem_id & + is_writeo tag & mem_seto state id Unit state' } } diff --git a/simplest_model_with_mods/tests.ml b/simplest_model_with_mods/tests.ml index ff779cc..02660db 100644 --- a/simplest_model_with_mods/tests.ml +++ b/simplest_model_with_mods/tests.ml @@ -19,41 +19,45 @@ let%expect_test "inv_id test 3" = print_endline (inv_id_t3 ()); [%expect {| [S ( let%expect_test "list_drop test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}] let%expect_test "list_replace test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}] let%expect_test "arG_to_value test 1" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}] -let%expect_test "st_add_arg test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), []); St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), [])] |}] +let%expect_test "st_add_arg test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), [])] |}] let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [])] |}] let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [])] |}] let%expect_test "multiple writes eval test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit; Unit], S (S (O)), [])] |}] -(* let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot], S (O), [])] |}] *) (* FIXME *) -(* let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [])] |}] *) (* FIXME *) -(* let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [])] |}] *) (* FIXME *) -(* let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [])] |}] *) (* FIXME *) -(* let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [])] |}] *) (* FIXME *) +let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot], S (O), [O])] |}] +let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [O])] |}] +let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [O])] |}] +let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}] +let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}] let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit], S (O), [])] |}] let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot], S (O), [])] |}] let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), S (O)))], [Bot; Unit], S (S (O)), [])] |}] -(* let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit], S (O), [])] |}] *) (* FIXME *) -let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), []); St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), [])] |}] +let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), [])] |}] +let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), [])] |}] let%expect_test "rvalue test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}] let%expect_test "empty_state test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}] let%expect_test "function eval test 1" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] -(* let%expect_test "function eval test 2" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}] *) (* FIXME *) +let%expect_test "function eval test 2" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}] let%expect_test "function eval test 3" = print_endline (fun_eval_t3 ()); [%expect {| [] |}] let%expect_test "function eval test 4" = print_endline (fun_eval_t4 ()); [%expect {| [] |}] let%expect_test "function eval test 5" = print_endline (fun_eval_t5 ()); [%expect {| [] |}] -(* let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] *) (* FIXME *) -(* let%expect_test "prog eval test 2" = print_endline (prog_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}] *) (* FIXME *) -(* let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [])] |}] *) (* FIXME *) +let%expect_test "function eval test 6" = print_endline (fun_eval_t6 ()); [%expect {| [St ([], [], O, [O])] |}] +let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] +let%expect_test "prog eval test 2" = print_endline (prog_eval_t2 ()); [%expect {| [St ([], [], O, [O])] |}] +let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [O])] |}] let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}] -(* let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Val] |}] (* FIXME *) *) -(* let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Ref; Val] |}] *) (* FIXME *) -(* let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}] *) (* FIXME *) -(* let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Val]] |}] (* FIXME *) *) -(* let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Ref; Ref]; [Ref; Val]; [Val; Ref]; [Val; Val]] |}] *) -(* let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Ref; Ref]; [Val; Ref]; [Ref; Val]; [Val; Val]] |}] *) -(* let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}] *) -(* let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] *) -(* let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] *) +let%expect_test "prog eval test 5" = print_endline (prog_eval_t5 ()); [%expect {| [St ([], [], O, [O])] |}] +let%expect_test "prog eval test 6" = print_endline (prog_eval_t6 ()); [%expect {| [] |}] +let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Tag (Rd, Wr, Val, In, NOut); Tag (NRd, Wr, Val, In, NOut)] |}] +let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Tag (NRd, Wr, Val, In, NOut); Tag (NRd, Wr, Ref, In, NOut)] |}] +let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Tag (NRd, Wr, Val, In, NOut); Tag (NRd, Wr, Val, In, NOut)]; [Tag (NRd, Wr, Ref, In, NOut); Tag (NRd, Wr, Val, In, NOut)]] |}] +let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Tag (NRd, Wr, Val, In, NOut)]] |}] +let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Val]; [Ref; Ref]] |}] +let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Ref]; [Ref; Val]] |}] +let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Val; Val]; [Ref; Val]] |}] +let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Val]; [Val; Ref]] |}] +let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] +(* TODO: FIXME: implement memoization cuts *) (* NOTE: inf test in current model (without additional functional interfaces and ) *) (* let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [])] |}] *) diff --git a/simplest_model_with_mods/tests_f.ml b/simplest_model_with_mods/tests_f.ml index 30a5807..8960b38 100644 --- a/simplest_model_with_mods/tests_f.ml +++ b/simplest_model_with_mods/tests_f.ml @@ -11,6 +11,8 @@ open OCanren.Std @type answerNats = (Nat.ground List.ground) GT.list with show @type answerTag = Tag.ground GT.list with show @type answerTags = (Tag.ground List.ground) GT.list with show +@type answerCopyCap = CopyCap.ground GT.list with show +@type answerCopyCaps = (CopyCap.ground List.ground) GT.list with show let inv_id_t _ = show(answerNat) (Stream.take (run q (fun q -> ocanren { inv_ido 2 1 q }) @@ -301,6 +303,19 @@ let fun_eval_t5 _ = show(answer) (Stream.take (run q eval_fun_empty_argso s p d q }) (fun q -> q#reify (St.prj_exn)))) +(* fun eval test *) +let fun_eval_t6 _ = show(answer) (Stream.take (run q + (fun q -> (* let open Prog in *) + let open FunDecl in + let open Tag in + let open Stmt in + ocanren { fresh s, p, d in + empty_stateo s & + p == [FunDecl ([wi_val], [Write 0])] & + d == FunDecl ([wi_val], [Call (0, [0])]) & + eval_fun_empty_argso s p d q }) + (fun q -> q#reify (St.prj_exn)))) + (* prog eval test *) let prog_eval_t1 _ = show(answer) (Stream.take (run q (fun q -> let open Prog in @@ -340,6 +355,26 @@ let prog_eval_t4 _ = show(answer) (Stream.take (run q FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) (fun q -> q#reify (St.prj_exn)))) +(* prog with func eval test *) +let prog_eval_t5 _ = show(answer) (Stream.take (run q + (fun q -> let open Prog in + let open FunDecl in + let open Tag in + let open Stmt in + ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0])], + FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) + (fun q -> q#reify (St.prj_exn)))) + +(* prog with func eval test *) +let prog_eval_t6 _ = show(answer) (Stream.take (run q + (fun q -> let open Prog in + let open FunDecl in + let open Tag in + let open Stmt in + ocanren {eval_progo (Prog ([FunDecl ([ri_val], [Write 0])], + FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) + (fun q -> q#reify (St.prj_exn)))) + (* annotation gen prog test *) let synt_t1 _ = show(answerTag) (Stream.take (run q (fun q -> let open Prog in @@ -347,8 +382,9 @@ let synt_t1 _ = show(answerTag) (Stream.take (run q let open Tag in let open Stmt in let open St in - ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], - FunDecl ([wi_val], [Call (0, [0]); Read 0]))) (St ([], [], 0, []))}) + ocanren {i_any q & + eval_progo (Prog ([FunDecl ([q], [Write 0])], + FunDecl ([wi_val], [Call (0, [0]); Read 0]))) (St ([], [], 0, [0]))}) (fun q -> q#reify (Tag.prj_exn)))) (* annotation gen prog test *) @@ -358,8 +394,9 @@ let synt_t2 _ = show(answerTag) (Stream.take (run q let open Tag in let open Stmt in let open St in - ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], - FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))}) + ocanren {i_any q & is_not_reado q & + eval_progo (Prog ([FunDecl ([q], [Write 0])], + FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) (fun q -> q#reify (Tag.prj_exn)))) (* annotation gen prog test *) @@ -369,8 +406,9 @@ let synt_t3 _ = show(answerTags) (Stream.take (run qr let open Tag in let open Stmt in let open St in - ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], - FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))}) + ocanren {i_any q & is_not_reado q & i_any r & is_not_reado r & + eval_progo (Prog ([FunDecl ([q], [Write 0])], + FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* annotation gen prog test *) @@ -380,72 +418,92 @@ let synt_t4 _ = show(answerTags) (Stream.take (run q let open Tag in let open Stmt in let open St in - ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], - FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, []))}) + ocanren {i_any q & is_not_reado q & + eval_progo (Prog ([FunDecl ([q], [Write 0])], + FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, [0]))}) (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *) (* annotation gen prog test *) -let synt_t5 _ = show(answerTags) (Stream.take (run qr +let synt_t5 _ = show(answerCopyCaps) (Stream.take (run qr (fun q r -> let open Prog in let open FunDecl in let open Tag in let open Stmt in let open St in - ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], - FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, []))}) - (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *) + ocanren {fresh q', r' in + i_any q' & is_not_reado q' & + i_any r' & is_not_reado r' & is_not_writeo r' & + eq_copyo q' q & eq_copyo r' r & + eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])], + FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) + (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *) (* annotation gen prog test *) -let synt_t6 _ = show(answerTags) (Stream.take (run qr +let synt_t6 _ = show(answerCopyCaps) (Stream.take (run qr (fun q r -> let open Prog in let open FunDecl in let open Tag in let open Stmt in let open St in - ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], - FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, []))}) - (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *) + ocanren {fresh q', r' in + i_any q' & is_not_reado q' & + i_any r' & is_not_reado r' & is_not_writeo r' & + eq_copyo q' q & eq_copyo r' r & + eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])], + FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) + (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *) (* annotation gen prog test *) -let synt_t7 _ = show(answerTags) (Stream.take (run qr +let synt_t7 _ = show(answerCopyCaps) (Stream.take (run qr (fun q r -> let open Prog in let open FunDecl in let open Tag in let open Stmt in let open St in - ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])], - FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))}) - (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) + ocanren {fresh q', r' in + i_any q' & is_not_reado q' & i_any r' & is_not_reado r' & + eq_copyo q' q & eq_copyo r' r & + eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])], + FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))}) + (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* annotation gen prog test *) -let synt_t8 _ = show(answerTags) (Stream.take (run qr +let synt_t8 _ = show(answerCopyCaps) (Stream.take (run qr (fun q r -> let open Prog in let open FunDecl in let open Tag in let open Stmt in let open St in - ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])], - FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))}) - (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) + ocanren {fresh q', r' in + i_any q' & is_not_reado q' & i_any r' & is_not_reado r' & + eq_copyo q' q & eq_copyo r' r & + eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])], + FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))}) + (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* annotation gen prog test *) -let synt_t9 _ = show(answerTags) (Stream.take (run qr +let synt_t9 _ = show(answerCopyCaps) (Stream.take (run qr (fun q r -> let open Prog in let open FunDecl in let open Tag in let open Stmt in let open St in - ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Read 1])], - FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, []))}) - (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) + ocanren {fresh q', r' in + i_any q' & is_not_reado q' & + i_any r' & is_reado r' & is_not_writeo r' & + eq_copyo q' q & eq_copyo r' r & + eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Read 1])], + FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, [0]))}) + (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* TODO: FIXME: implement memoization cuts *) (* prog with recursive function call *) -(* let rec_eval_t _ = show(answer) (Stream.take (run q *) - (* (fun q -> let open Prog in *) - (* let open FunDecl in *) - (* let open Tag in *) - (* let open Stmt in *) - (* ocanren {eval_progo (Prog ([FunDecl ([Ref], [Write 0; Call (0, [0])])], FunDecl ([Val], [Call (0, [0]); Write 0; Read 0]))) q}) *) - (* (fun q -> q#reify (St.prj_exn)))) *) +let rec_eval_t _ = show(answer) (Stream.take (run q + (fun q -> let open Prog in + let open FunDecl in + let open Tag in + let open Stmt in + ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Call (0, [0])])], + FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) q}) + (fun q -> q#reify (St.prj_exn))))