struct: synt. ambuity fixes, simple read call test

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!"; *)

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 {
@@ -675,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
   }
 
@@ -710,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
@@ -845,8 +860,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 +869,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 +922,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'
   }

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 {| [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)] |}] *)

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 *)