diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 248e366..826bde5 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -519,14 +519,12 @@ 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, forbidden read" = - try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], - ReadS (VarP globals_min_id)); + let%expect_test "simple var, no 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 |}] @@ -539,22 +537,19 @@ 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, forbidden write" = - try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr), UnitE)], - WriteS (VarP globals_min_id)); + let%expect_test "simple var, no 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! |}] @@ -562,7 +557,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!"; *) @@ -571,7 +566,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!"; *) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index b100a82..1908033 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -1,6 +1,3 @@ -(* NOTE: in previous models foldl & foldr are probably spapped - <- TODO: fix ? *) - module Relational = struct open GT @@ -148,9 +145,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 @@ -294,50 +291,40 @@ struct } - 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' & + 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' & f acc x' acc_upd & - list_foldlo f acc_upd xs' acc' } + list_foldro f acc_upd xs' acc' } (* TODO: inf search on swap, investigate *) } - 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' & - f acc x' y' acc_upd & - list_foldl2o f acc_upd xs' ys' acc' } - } - 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' & - list_foldr2o f acc xs' ys' acc_upd & - f acc_upd x' y' acc' } + f acc x' y' acc_upd & + list_foldr2o f acc_upd xs' ys' acc' } } - let rec list_foldl3o 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_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' & - zs == z' :: zs' & - f acc x' y' z' acc_upd & - list_foldl3o f acc_upd xs' ys' zs' acc' } + list_foldl2o f acc xs' ys' acc_upd & + f acc_upd x' y' acc' } } let rec list_foldr3o f acc xs ys zs acc' = ocanren { @@ -346,7 +333,17 @@ struct xs == x' :: xs' & ys == y' :: ys' & zs == z' :: zs' & - list_foldr3o f acc xs' ys' zs' acc_upd & + f acc x' y' z' acc_upd & + list_foldr3o f acc_upd xs' ys' zs' acc' } + } + + let rec list_foldl3o 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_foldl3o f acc xs' ys' zs' acc_upd & f acc_upd x' y' z' acc' } } @@ -611,32 +608,24 @@ 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_cp, v_cp, - mem_add, id_add, + mem_with_v_cp, mem_cp, v_cp, + mem_with_id_add, mem_add, id_add, types', vals' in d == VarD (tp, e) & exprvalo mem vals e v & - valcopyo mem v tp (Pair.pair mem_cp v_cp) & - mem_addo mem_cp v_cp (Pair.pair mem_add id_add) & + 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 & 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') - } + } } } @@ -655,7 +644,7 @@ struct } (* TODO: better way ??? *) - let globals_min_ido x = ocanren { x == 10 } + let globals_min_ido x = ocanren { x == 1000 } let prog_init_foldero st_with_id d st_with_id' = ocanren { @@ -686,12 +675,12 @@ struct let open Mode in let open CopyCap in ocanren { - { r == NRd | r == Rd & v == ZeroV } & - { r == NRd | r == Rd & is_ino m } & - { is_not_outo m | is_outo m & w == AlwaysWr } & + { r == NRd | v == ZeroV } & + { r == NRd | is_ino m } & + { is_not_outo m | w == AlwaysWr } & { w == NeverWr | - w =/= NeverWr & w' =/= AlwaysWr & is_not_outo m & c == Cp | - w =/= NeverWr & w' == AlwaysWr } & + { is_not_outo m & c == Cp } | + w' == AlwaysWr } & is_trivial_vo v } @@ -721,12 +710,8 @@ struct { is_outo m & w == AlwaysWr & mem_with_v' == Std.pair mem ZeroV } | - { { 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 } & + { { is_outo m | c == Cp | w == NeverWr } & + { is_not_outo m | w == MayWr | w == NeverWr } & mem_with_v' == Std.pair mem v } } } | { fresh ts, us, _stmts in @@ -860,8 +845,8 @@ struct { fresh f, es, v, tp, glob_tps, _tps, glob_vs, _vs, - types_call, vals_call, - fstmts, tps, st_call, + types', vals', + fstmts, tps, st', state_with_args, _arg_id, _states_evaled, mem_spoiled in s == CallS (f, es) & @@ -869,13 +854,13 @@ struct pathtypeo types f tp & types == TypesEnv (glob_tps, _tps) & vals == ValsEnv (glob_vs, _vs) & - types_call == TypesEnv (glob_tps, glob_tps) & - vals_call == ValsEnv (glob_vs, glob_vs) & + types' == TypesEnv (glob_tps, glob_tps) & + vals' == ValsEnv (glob_vs, glob_vs) & v == FunV fstmts & tp == FunT tps & - st_call == StEnv (mem, types_call, vals_call) & + st' == StEnv (mem, types', vals') & list_foldl2o (stmt_addarg_foldero vals) - (Std.pair st_call 0) tps es + (Std.pair st' 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 *) @@ -922,9 +907,12 @@ 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' } diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index f82b186..8e3ae24 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -2,27 +2,8 @@ open Tests_f open Synthesizer open Relational - (* - basic var tests *) - -let%expect_test "prog eval test: empty" = print_endline (prog_eval_t_empty ()); +let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%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)] |}] *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 69a5113..6737d97 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -4,115 +4,17 @@ 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 - (* - shortcuts *) - -(* TODO *) - - (* - basic var tests *) - -let prog_eval_t_empty _ = show(answer) (Stream.take (run q - (fun q -> ocanren { +let prog_eval_t1 _ = show(answer) (Stream.take (run q + (fun q -> let open Prg in + let open Stmt in + 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 *)