struct: synthesizer simple synthesis tests

model_with_structures/tests.ml

@@ -42,8 +42,6 @@ let%expect_test "simple call with write to ref" = print_endline(prog_eval_t_simp
 let%expect_test "simple call with forbidden write to ref" = print_endline(prog_eval_t_simple_call_ref_fbd_wr ());
   [%expect {| [] |}]
 
-(* --- *)
-
 let%expect_test "simple call with write to ref with fix" = print_endline(prog_eval_t_simple_call_ref_wr_with_fix ());
   [%expect {| [StEnv (MemEnv ([FunV ([WriteS (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 (Rf, 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 (Rf, 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)]))] |}]
 
@@ -65,64 +63,18 @@ let%expect_test "simple call with different arguments modifiers, copy" = print_e
 let%expect_test "simple call with different arguments modifiers, ref" = print_endline(prog_eval_t_call_with_dif_mods_rf ());
   [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O)))))))))]); RefV (S (S (S (S (S (S (O))))))); ZeroV; RefV (S (S (S (S (O))))); ZeroV; RefV (S (S (O))); ZeroV; RefV (O); ZeroV], S (S (S (S (S (S (S (S (S (O)))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (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 (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (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 (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (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 (S (S (O)))))))))))), 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 (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (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 (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (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 (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (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 (S (S (O)))))))))))), 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 (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (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)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (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)]))] |}]
 
-(* TODO: dif. ref modifiers tests ? *)
+(* - basic synthesis tests *)
 
-(* TODO: synthesis tests ? *)
+let%expect_test "simple synthesis test" = print_endline(prog_cp_cap_synt_t_simple_call_ref_wr ());
+  [%expect {| [Rf; Cp] |}]
 
-(* type tests *)
+let%expect_test "simple synthesis test, no read write caps constraints" = print_endline(prog_cp_cap_synt_t_simple_call_ref_wr' ());
-(* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *)
+  [%expect {| [Rf; Rf; Rf; Rf; Cp; Cp; Cp; Cp] |}]
-(* let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}] *)
-(* let%expect_test "Stmt type test (2)" = print_endline (Stmt.Test.test2 ()); [%expect {| [Call (S (O), [S (S (O))])] |}] *)
-(* let%expect_test "FunDecl type test" = print_endline (FunDecl.Test.test ()); [%expect {| [FunDecl ([Tag (Rd, AlwaysWr, Ref, In, NOut); Tag (Rd, AlwaysWr, Val, In, NOut)], [Call (S (O), [O]); Write (S (O))])] |}] *)
-(* let%expect_test "Prog type test" = print_endline (Prog.Test.test ()); [%expect {| [Prog ([], FunDecl ([Tag (Rd, NeverWr, Val, In, NOut)], [Write (O); Read (O)]))] |}] *)
-(* let%expect_test "Arg type test" = print_endline (Arg.Test.test ()); [%expect {| [LValue (S (S (S (O))))] |}] *)
-(* let%expect_test "Value type test" = print_endline (Value.Test.test ()); [%expect {| [Bot; Unit] |}] *)
-(* let%expect_test "St type test" = print_endline (St.Test.test ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Bot], S (O), [O])] |}] *)
 
-(* function tests *)
+let%expect_test "simple synthesis test, reference forbidden write" = print_endline(prog_cp_cap_synt_t_simple_call_ref_fbd_wr ());
-(* let%expect_test "inv_id test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}] *)
+  [%expect {| [Cp] |}]
-(* let%expect_test "inv_id test 2" = print_endline (inv_id_t2 ()); [%expect {| [S (O)] |}] *)
-(* let%expect_test "inv_id test 3" = print_endline (inv_id_t3 ()); [%expect {| [S (O)] |}] *)
-(* 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, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), O))], [Unit], S (O), [])] |}] *)
-(* let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [])] |}] *)
-(* let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, 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 (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *)
-(* let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, 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, [])] |}] *)
-(* 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 "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 "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, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)] |}] *)
-(* let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Ref, In, NOut)] |}] *)
-(* let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]; [Tag (NRd, AlwaysWr, Ref, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]] |}] *)
-(* let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Tag (NRd, AlwaysWr, 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]] |}] *)
 
-(* let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [O])] |}] *)
+let%expect_test "simple synthesis test, reference forbidden write, no read write caps constraints" = print_endline(prog_cp_cap_synt_t_simple_call_ref_fbd_wr' ());
+  [%expect {| [Cp; Cp; Cp; Cp] |}]
 
+(* TODO *)

model_with_structures/tests_f.ml

@@ -17,9 +17,10 @@ open InCap
 open OutCap
 open Mode
 
-@type answer  = StEnv.ground GT.list with show
+@type answer = StEnv.ground GT.list with show
+@type answerCpCap = CopyCap.ground GT.list with show
 
-  (* - shortcuts *)
+(* - shortcuts *)
 
 (* TODO *)
 
@@ -423,387 +424,67 @@ let prog_eval_t_call_with_dif_mods_rf _ = show(answer) (Stream.take (run q
               })
   (fun q -> q#reify (StEnv.prj_exn))))
 
-(* @type answerArgs = (Arg.ground List.ground) GT.list with show *)
+(* - basic synthesis tests *)
-(* @type answerValue = Value.ground GT.list with show *)
-(* @type answerNat = Nat.ground GT.list with show *)
-(* @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 *)
+let prog_cp_cap_synt_t_simple_call_ref_wr _ = show(answerCpCap) (Stream.take (run q
-  (* (fun q -> ocanren { inv_ido 2 1 q }) *)
+  (fun q -> ocanren {
-  (* (fun q -> q#reify Nat.prj_exn))) *)
+              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 (q, UnitT (Rd, AlwaysWr)))],
+                          WriteS (DerefP (VarP 0))) &
+              prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
+              prog_evalo prog st })
+  (fun q -> q#reify (CopyCap.prj_exn))))
 
-(* let inv_id_t2 _ = show(answerNat) (Stream.take (run q *)
+let prog_cp_cap_synt_t_simple_call_ref_wr' _ = show(answerCpCap) (Stream.take (run q
-  (* (fun q -> ocanren { inv_ido 2 0 q }) *)
+  (fun q -> ocanren {
-  (* (fun q -> q#reify Nat.prj_exn))) *)
+              fresh prog, xg, yg, fg, xd, yd, fd,
+                    st, rd_cap, wr_cap 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 (q, UnitT (rd_cap, wr_cap)))],
+                          WriteS (DerefP (VarP 0))) &
+              prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
+              prog_evalo prog st })
+  (fun q -> q#reify (CopyCap.prj_exn))))
 
-(* let inv_id_t3 _ = show(answerNat) (Stream.take (run q *)
+let prog_cp_cap_synt_t_simple_call_ref_fbd_wr _ = show(answerCpCap) (Stream.take (run q
-  (* (fun q -> ocanren { inv_ido 2 q 0 }) *)
+  (fun q -> ocanren {
-  (* (fun q -> q#reify Nat.prj_exn))) *)
+              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 (q, UnitT (Rd, AlwaysWr)))],
+                          WriteS (DerefP (VarP 0))) &
+              prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
+                                               ReadS (DerefP (VarP yg)))) &
+              prog_evalo prog st })
+  (fun q -> q#reify (CopyCap.prj_exn))))
 
-(* let list_drop_t _ = show(answerNats) (Stream.take (run q *)
+let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.take (run q
-  (* (fun q -> ocanren { list_dropo 2 [1; 2; 3] q }) *)
+  (fun q -> ocanren {
-  (* (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) *)
+              fresh prog, xg, yg, fg, xd, yd, fd,
-
+                    st, rd_cap, wr_cap in
-(* let list_replace_t  _ = show(answerNats) (Stream.take (run q *)
+              globals_min_ido xg &
-  (* (fun q -> ocanren { list_replaceo [1; 2; 3; 4] 1 0 q }) *)
+              yg == Nat.s xg &
-  (* (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) *)
+              fg == Nat.s yg &
-
+              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-(* let arg_to_value_t _ = show(answerValue) (Stream.take (run q *)
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
-  (* (fun q -> let open Arg in *)
+              fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (rd_cap, wr_cap)))],
-            (* ocanren { *)
+                          WriteS (DerefP (VarP 0))) &
-    (* fresh s in *)
+              prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
-      (* empty_stateo s & *)
+                                               ReadS (DerefP (VarP yg)))) &
-      (* arg_to_valueo s RValue q }) *)
+              prog_evalo prog st })
-  (* (fun q -> q#reify (Value.prj_exn)))) *)
+  (fun q -> q#reify (CopyCap.prj_exn))))
-
-(* let st_add_arg_t _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* ocanren { *)
-    (* fresh s, s', cnt in *)
-      (* empty_stateo s & *)
-      (* empty_stateo s' & *)
-      (* st_add_argo s  s' Nat.o rwi_val RValue q }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let write_eval_t1 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmt in *)
-      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) & *)
-      (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
-      (* stmt == Write 0 & *)
-      (* eval_stmto s p stmt q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let write_eval_t2 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmt in *)
-      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) & *)
-      (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
-      (* stmt == Write 1 & *)
-      (* eval_stmto s p stmt q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let writes_eval_t _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmts in *)
-      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) & *)
-      (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
-      (* stmts == [Write 0; Write 1] & *)
-      (* eval_bodyo s p stmts q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let call_eval_t1 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmt in *)
-      (* s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) & *)
-      (* p == [FunDecl ([wi_ref], [Write 0])] & *)
-      (* stmt == Call (0, [0]) & *)
-      (* eval_stmto s p stmt q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let call_eval_t2 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmt in *)
-      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
-      (* p == [FunDecl ([wi_ref], [Write 0])] & *)
-      (* stmt == Call (0, [0]) & *)
-      (* eval_stmto s p stmt q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let call_eval_t3 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmt in *)
-      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
-      (* p == [FunDecl ([wi_ref], [Write 0])] & *)
-      (* stmt == Call (0, [1]) & *)
-      (* eval_stmto s p stmt q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let call_eval_t4 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmt in *)
-      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
-      (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
-      (* stmt == Call (0, [0; 1]) & *)
-      (* eval_stmto s p stmt q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let call_eval_t5 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmt in *)
-      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
-      (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
-      (* stmt == Call (0, [1; 0]) & *)
-      (* eval_stmto s p stmt q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let mem_set_t1 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* ocanren { *)
-    (* fresh s in *)
-      (* s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Bot], 1, []) & *)
-      (* mem_seto s 0 Unit q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let mem_set_t2 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* ocanren { *)
-    (* fresh s in *)
-      (* s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) & *)
-      (* mem_seto s 0 Bot q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let meem_set_t3 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* ocanren { *)
-    (* fresh s in *)
-      (* s == St ([Std.pair 0 (Std.pair wi_ref 1)], [Unit; Unit], 2, []) & *)
-      (* mem_seto s 0 Bot q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let add_arg_folder_t _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* ocanren { *)
-    (* fresh s, s', cnt in *)
-      (* empty_stateo s & *)
-      (* empty_stateo s' & *)
-      (* add_arg_foldero s (Std.pair s' Nat.o) rwi_val RValue (Std.pair q cnt) }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let foldl2_t _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* ocanren { *)
-    (* fresh s, s', cnt, arg_tags, args in *)
-      (* arg_tags == [rwi_val] & *)
-      (* args == [RValue] & *)
-      (* empty_stateo s & *)
-      (* empty_stateo s' & *)
-      (* list_foldl2o (add_arg_foldero s) (Std.pair s' Nat.o) arg_tags args (Std.pair q cnt) }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-
-(* let rvalue_t _ = show(answerArgs) (Stream.take ~n:3 (run q *)
-  (* (fun q -> let open Arg in *)
-            (* ocanren {fresh v in List.mapo arg_to_rvalueo v q}) *)
-  (* (fun q -> q#reify (List.prj_exn Arg.prj_exn)))) *)
-
-(* empty state test *)
-(* let empty_state_t _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> ocanren {empty_stateo q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* fun eval test *)
-(* let fun_eval_t1 _ = 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 == [] & *)
-                        (* d == FunDecl ([], []) & *)
-                        (* eval_fun_empty_argso s p d q }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* fun eval test *)
-(* let fun_eval_t2 _ = 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 == [] & *)
-                        (* d == FunDecl ([wi_val], [Write 0; Read 0]) & *)
-                        (* eval_fun_empty_argso s p d q }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* fun eval test *)
-(* let fun_eval_t3 _ = 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_ref], [Write 0])] & *)
-                        (* d == FunDecl ([wi_val], [Call (0, [0]); Read 0]) & *)
-                        (* eval_fun_empty_argso s p d q }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* fun eval test *)
-(* let fun_eval_t4 _ = 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_ref], [Write 0])] & *)
-                        (* d == FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]) & *)
-                        (* eval_fun_empty_argso s p d q }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* fun eval test *)
-(* let fun_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 { fresh s, p, d in *)
-                        (* empty_stateo s & *)
-                        (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
-                        (* d == FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]) & *)
-                        (* 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 *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* ocanren {eval_progo (Prog ([], FunDecl ([wi_val], [Write 0; Read 0]))) q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* prog with func eval test *)
-(* let prog_eval_t2 _ = 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; Read 0])], *)
-                                       (* FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* prog with func eval test *)
-(* let prog_eval_t3 _ = 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; Read 0])], *)
-                                       (* FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* prog with func eval test *)
-(* let prog_eval_t4 _ = 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])], *)
-                                       (* 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 *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* let open St in *)
-            (* 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 *)
 (* let synt_t2 _ = show(answerTag) (Stream.take (run q *)
@@ -913,15 +594,3 @@ let prog_eval_t_call_with_dif_mods_rf _ = show(answer) (Stream.take (run q
                      (* 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 ([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)))) *)
-