diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 9b0c27a..d9a604b 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -247,6 +247,13 @@ struct let rec valupd (mem : mem) (v : value) (p : revpath) (a : action) : mem * value = match p, v with | VarRP, UnitV (v_m, v_r, v_w) -> (mem, UnitV (memvmod a v_m, readvmod a v_r, writevmod a v_w)) + | VarRP, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p a in + (mem_set mem' id v', RefV id) + (* TODO: add test on foldl vs foldr in this situation *) + | VarRP, TupleV vs -> let (mem', vs') = List.fold_right + (fun v (mem, vs') -> let (mem', v') = valupd mem v p a in + (mem', v' :: vs')) vs (mem, []) in + (mem', TupleV vs') | DerefRP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p a in (mem_set mem' id v', RefV id) | AccessRP (p, id), TupleV vs -> let (mem', v') = valupd mem (List.nth vs id) p a in @@ -452,6 +459,15 @@ struct | TupleV vs, TupleT ts -> ignore @@ List.map2 (tags_check mem) vs ts | _, _ -> raise @@ Typing_error "tags_check" + (* - writable type *) + + let rec is_all_type_writable (t : atype) : bool = + match t with + | UnitT (_, w) -> w == MayWr || w == AlwaysWr + | FunT _ -> true + | RefT (_, t) -> is_all_type_writable t + | TupleT ts -> List.for_all is_all_type_writable ts + (* - statement evaluation *) let rec stmt_eval (state : state) (s : stmt) : state = @@ -493,32 +509,18 @@ struct | FunV _, _ -> raise @@ Eval_error "call: function type" | _, FunT _ -> raise @@ Eval_error "call: function val" | _, _ -> raise @@ Eval_error "call: function type & val") - | WriteS p -> (match pathtype types p with - | UnitT (_, w) -> - if w == NeverWr - then raise @@ Eval_error "write: write tag" - else let x = pathvar p in - let id = vals_assoc x vals in - let pi = pathrev p VarRP in - let (mem', v') = valupd mem (mem_get mem id) pi AlwaysWriteA in - (mem_set mem' id v', types, vals, visited) - | RefT _ -> raise @@ Eval_error "write: ref type" - | TupleT _ -> raise @@ Eval_error "write: tuple type" - | _ -> raise @@ Eval_error "write: type") - | ReadS p -> (match pathtype types p with - | UnitT (_, _) -> - (* NOTE: not required *) - (* if r == NRd *) - (* then raise @@ Eval_error "read: not read tag" *) - (* else *) - let x = pathvar p in - let id = vals_assoc x vals in - let pi = pathrev p VarRP in - let (mem', v') = valupd mem (mem_get mem id) pi ReadA in - (mem_set mem' id v', types, vals, visited) - | RefT _ -> raise @@ Eval_error "read: ref type" - | TupleT _ -> raise @@ Eval_error "read: tuple type" - | _ -> raise @@ Eval_error "read: type") + | WriteS p -> if not @@ is_all_type_writable @@ pathtype types p + then raise @@ Eval_error "write: write tag" + else let x = pathvar p in + let id = vals_assoc x vals in + let pi = pathrev p VarRP in + let (mem', v') = valupd mem (mem_get mem id) pi AlwaysWriteA in + (mem_set mem' id v', types, vals, visited) + | ReadS p -> let x = pathvar p in + let id = vals_assoc x vals in + let pi = pathrev p VarRP in + let (mem', v') = valupd mem (mem_get mem id) pi ReadA in + (mem_set mem' id v', types, vals, visited) (* NOTE: handled inside through undefined in memvmod *) (* if pathval mem vals p == SmthV || pathval mem vals p == BotV *) (* then raise @@ Eval_error "read: spoiled value" *) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 8d61739..3f21ae3 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -1471,6 +1471,69 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ #h(10pt) +=== Writable Type + +#let twrite = $attach(tack.r, br: #[`write`])$ + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ writable unit type: MaybeWrite], + + $twrite cl r, MaybeWrite cr$, + ) +)) + +#h(10pt) + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ writable unit type: AlwaysWrite], + + $twrite cl r, AlwaysWrite cr$, + ) +)) + +#h(10pt) + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ writable ref type], + + $twrite t$, + $twrite rf c space t$, + ) +)) + +#h(10pt) + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ writable lambda type], + + $twrite lambda space overline(t)$, + ) +)) + +#h(10pt) + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ writable tuple type], + + $twrite t_1$, + $...$, + $twrite t_n$, + $twrite [t_1, ... t_n]$, + ) +)) + +#h(10pt) + === Statement Evaluation #align(center, prooftree( @@ -1517,8 +1580,8 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ rule( name: [ WRITE $p$], - $types ttype p : cl r, w cr$, - $w = MaybeWrite or w = AlwaysWrite$, + $types ttype p : t$, + $twrite t$, $p arrpath x$, $l = vals[x]$, $p arrrevpath^(\#.) pi$, @@ -1539,8 +1602,6 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ // $vals, mu tval p eqmu cdr v_m, \_, \_ cdl$, // $v_m in { 0, top }$, - $types ttype p : cl r, w cr$, - $r = Read$, $p arrpath x$, $l = vals[x]$, $p arrrevpath^(\#.) pi$, diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index f4216ff..7a61927 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -381,6 +381,14 @@ struct { xs == [] & ys == [] & zs == [] } } + let rec list_checko f xs = ocanren { + { xs == [] } | + { fresh x', xs' in + xs == x' :: xs' & + f x' & + list_checko f xs' } + } + (* NOTE: unrequired ? *) (* let list_map2o f xs ys zs = ocanren { *) (* { xs == [] & ys == [] } | *) @@ -388,7 +396,7 @@ struct (* xs == x' :: xs' & *) (* ys == y' :: ys' & *) (* f x' y' z' *) - (* mapo f xs' ys' zs' & *) + (* list_map2o f xs' ys' zs' & *) (* zs == z' :: zs' } *) (* } *) @@ -688,7 +696,13 @@ struct } (* NOTE: reversed path used *) - let rec valupdo mem v rp a mem_with_v' = + let rec substructure_tuple_foldero rp a mem_with_vs v mem_with_vs' = ocanren { + fresh mem, vs, mem', v' in + Std.pair mem vs == mem_with_vs & + valupdo mem v rp a (Std.pair mem' v') & + mem_with_vs' == Std.pair mem' (v' :: vs) + } + and valupdo mem v rp a mem_with_v' = let open RevPath in let open Value in ocanren { @@ -703,19 +717,23 @@ struct v' == UnitV (v_m', v_r', v_w') & mem_with_v' == Std.pair mem v' } | { fresh rp', id, v', mem_upd, v_upd, mem_with_v_upd, mem_st in - rp == DerefRP rp' & + { rp == DerefRP rp' | { rp == VarRP & rp' == VarRP } } & (* ref path or substructure *) v == RefV id & mem_geto mem id v' & valupdo mem v' rp' a mem_with_v_upd & Std.pair mem_upd v_upd == mem_with_v_upd & mem_seto mem_upd id v_upd mem_st & mem_with_v' == Std.pair mem_st (RefV id) } | - { fresh rp', id, vs', v', mem_upd, v_upd, mem_with_v_upd, vs_upd in + { fresh vs', mem_upd, vs_upd in + rp == VarRP & + v == TupleV vs' & + list_foldro (substructure_tuple_foldero rp a) (Std.pair mem []) vs' (Std.pair mem_upd vs_upd) & + mem_with_v' == Std.pair mem_upd (TupleV vs_upd) } | + { fresh rp', id, vs', v', mem_upd, v_upd, vs_upd in rp == AccessRP (rp', id) & v == TupleV vs' & list_ntho vs' id v' & - valupdo mem v' rp' a mem_with_v_upd & - Std.pair mem_upd v_upd == mem_with_v_upd & + valupdo mem v' rp' a (Std.pair mem_upd v_upd) & list_replaceo vs' id v_upd vs_upd & mem_with_v' == Std.pair mem_upd (TupleV vs_upd) } } @@ -1140,6 +1158,25 @@ struct List.mapo (tags_checko mem) vs tps } } + (* - writable type *) + + let rec is_all_type_writableo tp = + let open Type in + let open WriteCap in + ocanren { + { fresh _r, w in + tp == UnitT (_r, w) & + { w == MayWr | w == AlwaysWr } } | + { fresh _tps in + tp == FunT _tps } | + { fresh _c, tp' in + tp == RefT (_c, tp') & + is_all_type_writableo tp' } | + { fresh tps' in + tp == TupleT tps' & + list_checko is_all_type_writableo tps' } + } + (* - statement evaluation *) let rec stmt_addarg_foldero vals st_with_id mtp e st_with_id' = ocanren { @@ -1187,7 +1224,7 @@ struct let open Stmt in let open Value in let open Type in - let open WriteCap in + (* let open WriteCap in *) let open TypesEnv in let open ValsEnv in let open RevPath in @@ -1227,12 +1264,11 @@ struct mem tps es mem_spoiled & st' == StEnv (mem_spoiled, types, vals, visited') } | - { fresh p, tp, _r, w, x, id, v, rp, + { fresh p, tp, x, id, v, rp, mem_upd, v_upd, mem_set in s == WriteS p & pathtypeo types p tp & - tp == UnitT (_r, w) & - { w == AlwaysWr | w == MayWr } & + is_all_type_writableo tp & pathvaro p x & vals_assoco x vals id & mem_geto mem id v & @@ -1240,11 +1276,9 @@ struct valupdo mem v rp AlwaysWriteA (Std.pair mem_upd v_upd) & mem_seto mem_upd id v_upd mem_set & st' == StEnv (mem_set, types, vals, visited) } | - { fresh p, tp, _r, _w, x, id, v, rp, + { fresh p, _tp, _r, _w, x, id, v, rp, mem_upd, v_upd, mem_set in s == ReadS p & - pathtypeo types p tp & - tp == UnitT (_r, _w) & pathvaro p x & vals_assoco x vals id & mem_geto mem id v & diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index 3c73dcb..2325fee 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -25,46 +25,46 @@ let%expect_test "simple call with read" = print_endline(prog_eval_t_simple_call_ [%expect {| [StEnv (MemEnv ([FunV ([ReadS (VarP (O))]); UnitV (ZeroMV, OneRV, ZeroWV)], 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)]), VisitedEnv ([ReadS (VarP (O))]))] |}] let%expect_test "simple call with ref read" = print_endline(prog_eval_t_simple_call_rd_ref ()); - [%expect {| [StEnv (MemEnv ([FunV ([ReadS (DerefP (VarP (O)))]); RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (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)]), VisitedEnv ([ReadS (DerefP (VarP (O)))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([ReadS (DerefP (VarP (O)))]); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (S (O)))))))))))), S (S (S (O)))); (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 (O)))))))))), O)], [(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 (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([ReadS (DerefP (VarP (O)))]))] |}] let%expect_test "simple call with write" = print_endline(prog_eval_t_simple_call_wr ()); - [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, 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)]), VisitedEnv ([WriteS (DerefP (VarP (O)))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (S (O)); UnitV (BotMV, ZeroRV, ZeroWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))]), ValsEnv ([(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 (O))))))))))), S (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 (S (O)))); (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 (O)))))))))), O)]), VisitedEnv ([WriteS (DerefP (VarP (O)))]))] |}] let%expect_test "simple call with read after write" = print_endline(prog_eval_t_simple_call_wr_rd ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (DerefP (VarP (O))), ReadS (DerefP (VarP (O))))]); RefV (O); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, 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 (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (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)]), VisitedEnv ([SeqS (WriteS (DerefP (VarP (O))), ReadS (DerefP (VarP (O))))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (DerefP (VarP (O))), ReadS (DerefP (VarP (O))))]); RefV (S (O)); UnitV (BotMV, ZeroRV, ZeroWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, 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 (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (S (S (O)))))))))))), S (S (S (O)))); (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 (O)))))))))), O)], [(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 (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([SeqS (WriteS (DerefP (VarP (O))), ReadS (DerefP (VarP (O))))]))] |}] let%expect_test "simple call with forbidden write" = print_endline(prog_eval_t_simple_call_fbd_wr ()); [%expect {| [] |}] let%expect_test "simple call with write to ref" = print_endline(prog_eval_t_simple_call_ref_wr ()); - [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); UnitV (BotMV, TopRV, OneWV)], 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 (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, 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)]), VisitedEnv ([WriteS (DerefP (VarP (O)))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (S (O)); UnitV (BotMV, TopRV, OneWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (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 (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))]), ValsEnv ([(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 (O))))))))))), S (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 (S (O)))); (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 (O)))))))))), O)]), VisitedEnv ([WriteS (DerefP (VarP (O)))]))] |}] 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); UnitV (ZeroMV, TopRV, OneWV)], 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 (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, 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)]), VisitedEnv ([WriteS (DerefP (VarP (O)))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); RefV (S (O)); UnitV (ZeroMV, TopRV, OneWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (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 (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (NRd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, AlwaysWr))]), ValsEnv ([(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 (O))))))))))), S (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 (S (O)))); (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 (O)))))))))), O)]), VisitedEnv ([WriteS (DerefP (VarP (O)))]))] |}] let%expect_test "call inside call" = print_endline(prog_eval_t_call_in_call ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]); FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (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 (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)]), VisitedEnv ([WriteS (DerefP (VarP (O))); SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]); FunV ([WriteS (DerefP (VarP (O)))]); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O))))))))))))), S (S (S (S (O))))); (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 (O))))))))))), S (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 (O))))))))))))), S (S (S (S (O))))); (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 (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([WriteS (DerefP (VarP (O))); SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]))] |}] let%expect_test "call inside call, recursive" = print_endline(prog_eval_t_call_in_call_rec ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]); RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, 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 (Cp, UnitT (NRd, 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)]), VisitedEnv ([SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, 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 (Cp, UnitT (NRd, 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 (S (O)))); (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 (O)))))))))), O)], [(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 (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), [PathE (VarP (O))]), WriteS (DerefP (VarP (O))))]))] |}] let%expect_test "call to fix after call" = print_endline(prog_eval_t_fix_call_after_call ()); - [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); FunV ([WriteS (DerefP (VarP (O)))]); RefV (O); UnitV (ZeroMV, TopRV, OneWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O))))))))))))), FunT ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (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 (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)]), VisitedEnv ([WriteS (DerefP (VarP (O)))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([WriteS (DerefP (VarP (O)))]); FunV ([WriteS (DerefP (VarP (O)))]); RefV (S (O)); UnitV (ZeroMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O))))))))))))), FunT ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O))))))))))))), S (S (S (S (O))))); (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 (O))))))))))), S (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 (O))))))))))))), S (S (S (S (O))))); (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 (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([WriteS (DerefP (VarP (O)))]))] |}] let%expect_test "simple call with global variable usage" = print_endline(prog_eval_t_call_with_glob_usage ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (VarP (S (S (S (S (S (S (S (S (S (S (O)))))))))))), ReadS (DerefP (VarP (O))))]); RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (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 (Cp, UnitT (Rd, NeverWr)))])); (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)]), VisitedEnv ([SeqS (WriteS (VarP (S (S (S (S (S (S (S (S (S (S (O)))))))))))), ReadS (DerefP (VarP (O))))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (VarP (S (S (S (S (S (S (S (S (S (S (O)))))))))))), ReadS (DerefP (VarP (O))))]); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (O))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))])); (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 (Cp, UnitT (Rd, NeverWr)))])); (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 (S (O)))); (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 (O)))))))))), O)], [(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 (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([SeqS (WriteS (VarP (S (S (S (S (S (S (S (S (S (S (O)))))))))))), ReadS (DerefP (VarP (O))))]))] |}] let%expect_test "simple call with read & write (2 args)" = print_endline(prog_eval_t_call_with_rd_wr_2_args ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (O))), WriteS (DerefP (VarP (S (O)))))]); RefV (S (S (O))); UnitV (BotMV, TopRV, OneWV); RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], S (S (S (S (S (O)))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (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 (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)]), VisitedEnv ([SeqS (ReadS (DerefP (VarP (O))), WriteS (DerefP (VarP (S (O)))))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (O))), WriteS (DerefP (VarP (S (O)))))]); RefV (S (S (S (S (O))))); UnitV (BotMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (S (S (S (O)))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O)))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (NRd, 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 (O)))))))))))))), S (S (S (S (S (S (O))))))); (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 (O)))))))))))), S (S (S (O)))); (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 (O)))))))))), O)], [(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 (O))))))))))))), S (S (S (S (S (O)))))); (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 (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([SeqS (ReadS (DerefP (VarP (O))), WriteS (DerefP (VarP (S (O)))))]))] |}] let%expect_test "simple call with different arguments modifiers, copy" = print_endline(prog_eval_t_call_with_dif_mods_cp ()); - [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (O)))), SeqS (WriteS (DerefP (VarP (S (S (O))))), SeqS (WriteS (DerefP (VarP (S (S (S (O)))))), SkipS)))))]); RefV (S (S (S (S (S (S (O))))))); UnitV (ZeroMV, OneRV, OneWV); RefV (S (S (S (S (O))))); UnitV (ZeroMV, TopRV, OneWV); RefV (S (S (O))); UnitV (ZeroMV, OneRV, ZeroWV); RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], 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 (Cp, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (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 (Cp, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (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)]), VisitedEnv ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (O)))), SeqS (WriteS (DerefP (VarP (S (S (O))))), SeqS (WriteS (DerefP (VarP (S (S (S (O)))))), SkipS)))))]))] |}] + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (O)))), SeqS (WriteS (DerefP (VarP (S (S (O))))), SeqS (WriteS (DerefP (VarP (S (S (S (O)))))), SkipS)))))]); RefV (S (S (S (S (S (S (S (S (S (S (O))))))))))); UnitV (ZeroMV, OneRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (S (S (S (S (S (S (O)))))))); UnitV (ZeroMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (S (S (S (O))))); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (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 (Cp, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (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 (Cp, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (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 (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 (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 (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 (S (S (S (O))))))))); (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 (O))))))))))))), S (S (S (S (S (O)))))); (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 (O))))))))))), S (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 (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 (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 (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 (S (S (S (O))))))))); (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 (O))))))))))))), S (S (S (S (S (O)))))); (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 (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (O)))), SeqS (WriteS (DerefP (VarP (S (S (O))))), SeqS (WriteS (DerefP (VarP (S (S (S (O)))))), SkipS)))))]))] |}] 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))))), SeqS (WriteS (DerefP (VarP (S (S (S (O)))))), SkipS))))]); RefV (S (S (S (S (S (S (O))))))); UnitV (ZeroMV, OneRV, OneWV); RefV (S (S (S (S (O))))); UnitV (ZeroMV, TopRV, OneWV); RefV (S (S (O))); UnitV (ZeroMV, OneRV, ZeroWV); RefV (O); UnitV (ZeroMV, OneRV, ZeroWV)], 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)]), VisitedEnv ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (S (O))))), SeqS (WriteS (DerefP (VarP (S (S (S (O)))))), SkipS))))]))] |}] + [%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))))), SeqS (WriteS (DerefP (VarP (S (S (S (O)))))), SkipS))))]); RefV (S (S (S (S (S (S (S (S (S (S (O))))))))))); UnitV (ZeroMV, OneRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (S (S (S (S (S (S (O)))))))); UnitV (ZeroMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (S (S (S (O))))); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (O)); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (S (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 (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 (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 (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 (S (S (S (O))))))))); (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 (O))))))))))))), S (S (S (S (S (O)))))); (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 (O))))))))))), S (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 (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 (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 (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 (S (S (S (O))))))))); (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 (O))))))))))))), S (S (S (S (S (O)))))); (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 (O))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (S (O))))), SeqS (WriteS (DerefP (VarP (S (S (S (O)))))), SkipS))))]))] |}] (* - basic synthesis tests *) @@ -91,7 +91,7 @@ let%expect_test "presentation test 1 (simple types), synt" = print_endline(prog_ let%expect_test "presentation test 2 (complex types), eval" = print_endline(prog_eval_t_presentation_complex_tp ()); [%expect {| [StEnv (MemEnv ([FunV ([SeqS (SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (S (O)))), SkipS))))))))]); TupleV ([RefV (S (S (S (S (S (O)))))); RefV (S (S (S (S (O))))); RefV (S (S (S (O))))]); TupleV ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV)]); TupleV ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (ZeroMV, OneRV, ZeroWV)]); UnitV (ZeroMV, TopRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); TupleV ([UnitV (ZeroMV, ZeroRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)]); TupleV ([UnitV (ZeroMV, ZeroRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV); UnitV (ZeroMV, ZeroRV, ZeroWV)])], S (S (S (S (S (S (S (S (O))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, AlwaysWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (NRd, AlwaysWr))]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, 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))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, AlwaysWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (NRd, AlwaysWr))]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, 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))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (S (S (S (S (S (S (S (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))]), ValsEnv ([(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 (O))))))))))))), S (S (S (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 (O)))))))))))))), S (S (S (S (S (S (S (O)))))))); (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 (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)]), VisitedEnv ([SeqS (SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SkipS)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (O))))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), O)), S (S (O)))), SkipS))))))))]))] |}] -let%expect_test "presentation test 2 (complex types), esynt" = print_endline(prog_synt_t_presentation_complex_tp ()); +let%expect_test "presentation test 2 (complex types), synt" = print_endline(prog_synt_t_presentation_complex_tp ()); [%expect {| [[Cp; Cp; Cp]; [Cp; Cp; Rf]; [Cp; Rf; Cp]; [Cp; Rf; Rf]] |}] (* - complex test: send example *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 4690159..8022138 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -875,18 +875,15 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take ( timeE == UnitE & requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] & - fresh data_p0, data_p1, time_p, + fresh data_p, time_p, user_id_p, user_name_p, user_surname_p in - access_deref_accesso 0 1 0 data_p0 & - access_deref_accesso 1 1 0 data_p1 & + deref_accesso 1 0 data_p & deref_accesso 2 0 time_p & access_deref_accesso 0 0 0 user_id_p & access_deref_accesso 1 0 0 user_name_p & access_deref_accesso 2 0 0 user_surname_p & - seqo [ReadS data_p0; - ReadS data_p1; - WriteS data_p0; - WriteS data_p1; + seqo [ReadS data_p; + WriteS data_p; ReadS user_name_p; WriteS user_name_p] sendBranchStmts & @@ -894,13 +891,8 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take ( (* TODO: FIXME *) (* ChoiceS (sendBranchStmts, SkipS); *) WriteS time_p; - - ReadS data_p0; - ReadS data_p1; - ReadS time_p; - ReadS user_id_p; - ReadS user_name_p; - ReadS user_surname_p] sendStmts & + ReadS (VarP 0) + ] sendStmts & (* sendStmts == SkipS & *) sendD == FunD ([(Mode (In, NOut), requestArgsT)], sendStmts) &