more tests, foldr fix

lib/relational_semantic_interpreter_oc.ml

@@ -239,8 +239,8 @@ struct
     xs == [] & acc' == acc |
     { fresh x', xs', acc_upd in
       xs == x' :: xs' &
-      f acc x' acc' &
+      f acc x' acc_upd &
-      list_foldro f acc' xs' acc_upd }
+      list_foldro f acc_upd xs' acc' }
     (* TODO: inf search on swap, investigate *)
   }
 
@@ -304,23 +304,18 @@ struct
       env_addo state' id mem_len_prev' state'' }
   }
 
-  let st_spoil_foldero mem_len state mem id mem' =
+  let st_spoil_foldero state id state' =
     let open Value in
     ocanren {
-    fresh mem_id', mem_id_inv' in
+    mem_seto state id Bot state'
-      env_geto state id mem_id' &
-      inv_ido mem_len mem_id' mem_id_inv' &
-      list_replaceo mem mem_id_inv' Bot mem'
   }
 
   let st_spoil_assignmentso state state' =
     let open St in
     ocanren {
-    fresh env, mem, mem', mem_len, assignments, nil' in
+    fresh _env, _mem, _mem_len, assignments in
-      state == St (env, mem, mem_len, assignments) &
+      state == St (_env, _mem, _mem_len, assignments) &
-      list_foldlo (st_spoil_foldero mem_len state) mem assignments mem' &
+      list_foldlo st_spoil_foldero state assignments state'
-      nil' == [] &
-      state' == St (env, mem', mem_len, nil')
   }
 
   (* --- *)
@@ -472,6 +467,51 @@ struct
           st_add_argo s  s' Nat.o Val RValue q })
       (fun q -> q#reify (St.prj_exn))))
 
+    let _ = Printf.printf "write stmt eval test: %s\n" @@ 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 1; Std.pair 0 0], [Bot; Bot], 2, []) &
+          p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
+          stmt == Write 0 &
+          eval_stmto s p stmt q})
+      (fun q -> q#reify (St.prj_exn))))
+
+    let _ = Printf.printf "write stmt eval test 2: %s\n" @@ 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 1; Std.pair 0 0], [Bot; Bot], 2, []) &
+          p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
+          stmt == Write 1 &
+          eval_stmto s p stmt q})
+      (fun q -> q#reify (St.prj_exn))))
+
+    let _ = Printf.printf "write stmt body eval test 2: %s\n" @@ 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 1; Std.pair 0 0], [Bot; Bot], 2, []) &
+          p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
+          stmts == [Write 0; Write 1] &
+          eval_bodyo s p stmts q})
+      (fun q -> q#reify (St.prj_exn))))
+
     let _ = Printf.printf "call stmt eval test: %s\n" @@ show(answer) (Stream.take (run q
       (fun q -> let open Arg in
                 let open Tag in
@@ -517,6 +557,36 @@ struct
           eval_stmto s p stmt q})
       (fun q -> q#reify (St.prj_exn))))
 
+    let _ = Printf.printf "call stmt eval test 4: %s\n" @@ 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 1; Std.pair 0 0], [Unit; Unit], 2, []) &
+          p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
+          stmt == Call (0, [0; 1]) &
+          eval_stmto s p stmt q})
+      (fun q -> q#reify (St.prj_exn))))
+
+    let _ = Printf.printf "call stmt eval test 5: %s\n" @@ 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 1; Std.pair 0 0], [Unit; Unit], 2, []) &
+          p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
+          stmt == Call (0, [1; 0]) &
+          eval_stmto s p stmt q})
+      (fun q -> q#reify (St.prj_exn))))
+
     let _ = Printf.printf "mem set test: %s\n" @@ show(answer) (Stream.take (run q
       (fun q -> let open Arg in
                 let open Tag in
@@ -635,6 +705,19 @@ struct
                             eval_fun_empty_argso s p d q })
       (fun q -> q#reify (St.prj_exn))))
 
+    (* fun eval test *)
+    let _ = Printf.printf "fun eval test (wrong call 3): %s\n" @@ 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 ([Ref; Ref], [Write 0; Write 1])] &
+                            d == FunDecl ([Val; 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))))
+
     (* prog eval test *)
     let _ = Printf.printf "prog eval test: %s\n" @@ show(answer) (Stream.take (run q
       (fun q -> let open Prog in
@@ -701,7 +784,6 @@ struct
                 ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))})
       (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
 
-    (* TODO *)
     (* annotation gen prog test *)
     let _ = Printf.printf "synt test 4: %s\n" @@ show(answerTags) (Stream.take (run q
       (fun q -> let open Prog in
@@ -712,7 +794,6 @@ struct
                 ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val; Val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, []))})
       (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *)
 
-    (* TODO *)
     (* annotation gen prog test *)
     let _ = Printf.printf "synt test 5: %s\n" @@ show(answerTags) (Stream.take (run qr
       (fun q r -> let open Prog in
@@ -723,7 +804,6 @@ struct
                 ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], FunDecl ([Val; 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 *)
 
-    (* TODO *)
     (* annotation gen prog test *)
     let _ = Printf.printf "synt test 5' (swap call args): %s\n" @@ show(answerTags) (Stream.take (run qr
       (fun q r -> let open Prog in
@@ -734,7 +814,6 @@ struct
                 ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], FunDecl ([Val; 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 *)
 
-    (* TODO *)
     (* annotation gen prog test *)
     let _ = Printf.printf "synt test 5'' (swap def args): %s\n" @@ show(answerTags) (Stream.take (run qr
       (fun q r -> let open Prog in
@@ -745,7 +824,6 @@ struct
                 ocanren {eval_progo (Prog ([FunDecl ([r; q], [Write 0])], FunDecl ([Val; 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 *)
 
-    (* TODO *)
     (* annotation gen prog test *)
     let _ = Printf.printf "synt test 6: %s\n" @@ show(answerTags) (Stream.take (run qr
       (fun q r -> let open Prog in
@@ -756,6 +834,28 @@ struct
                 ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])], FunDecl ([Val; 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)])))
 
+    (* TODO FIXME *)
+    (* annotation gen prog test *)
+    let _ = Printf.printf "synt test 6' (swap call args): %s\n" @@ show(answerTags) (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 ([Val; 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)])))
+
+    (* annotation gen prog test *)
+    let _ = Printf.printf "synt test 6'' (swap def args): %s\n" @@ show(answerTags) (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 ([r; q], [Write 0; Write 1])], FunDecl ([Val; 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)])))
+
+    (* TODO: test with assymetric args order *)
   end
 
   (* let eval_test () = *)