diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 9b0c27a..a900c41 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -59,26 +59,22 @@ struct (* value model & memory model *) - (* type deepvalue = ZeroDV *) - (* | SmthDV *) - (* | BotDV *) - (* | FunDV of ((* data list * *) stmt) list *) - (* | RefDV of deepvalue *) - (* | TupleDV of deepvalue list *) + type deepvalue = ZeroDV + | SmthDV + | BotDV + | FunDV of ((* data list * *) stmt) list + | RefDV of deepvalue + | TupleDV of deepvalue list - type memval = ZeroMV | SmthMV | BotMV (* | TopMV ?? *) - type readval = ZeroRV | OneRV | TopRV - type writeval = ZeroWV | SmthWV | OneWV - - type value = UnitV of memval * readval * writeval + type value = ZeroV + | SmthV + | BotV | FunV of ((* data list * *) stmt) list | RefV of memid | TupleV of value list type revpath = VarRP | DerefRP of revpath | AccessRP of revpath * data - type action = ReadA | AlwaysWriteA | MayWriteA - (* TODO: any additional difference between rvalue and lvalue now ?? *) (* --- *) @@ -142,17 +138,16 @@ struct let mem_set (mem : mem) (id : memid) (v : value) : mem = (list_replace (fst mem) (snd mem - id - 1) v, snd mem) - (* let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with *) - (* | ZeroV -> ZeroDV *) - (* | SmthV -> SmthDV *) - (* | BotV -> BotDV *) - (* | FunV s -> FunDV s *) - (* | RefV id -> RefDV (v_to_deepv mem @@ mem_get mem id) *) - (* | TupleV vs -> TupleDV (List.map (v_to_deepv mem) vs) *) + let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with + | ZeroV -> ZeroDV + | SmthV -> SmthDV + | BotV -> BotDV + | FunV s -> FunDV s + | RefV id -> RefDV (v_to_deepv mem @@ mem_get mem id) + | TupleV vs -> TupleDV (List.map (v_to_deepv mem) vs) - let is_trivial_v (v : value) : bool = - match v with | UnitV (_, _, _) -> true - | _ -> false + let is_trivial_v (v : value) : bool = + v == ZeroV || v == SmthV || v == BotV (* --- path accessors --- *) @@ -196,12 +191,22 @@ struct (* - value construction *) let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = - match t, v with - | UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV)) - | UnitT (NRd, _), UnitV _ -> (mem, UnitV (BotMV, ZeroRV, ZeroWV)) + if is_trivial_v v + then match t with + | UnitT (Rd, _) -> (mem, v) + | UnitT (NRd, _) -> (mem, BotV) + | _ -> raise @@ Typing_error "valcopy: trivial value, wrong type" + else match t, v with + (* NOTE: replaced with if | best choice ?? *) + (* | UnitT (Rd, w), ZeroV -> (mem, v) *) + (* | UnitT (Rd, w), SmthV -> (mem, v) *) + (* | UnitT (Rd, w), BotV -> (mem, v) *) + (* | UnitT (NRd, w), ZeroV -> (mem, BotV) *) + (* | UnitT (NRd, w), SmthV -> (mem, BotV) *) + (* | UnitT (NRd, w), BotV -> (mem, BotV) *) | FunT _, FunV _ -> (mem, v) - (* | RefT (Rf, _), RefV _ -> (mem, v) *) - | RefT (_, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in + | RefT (Rf, _), RefV _ -> (mem, v) + | RefT (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in let (mem'', id'') = mem_add mem' v' in (mem'', RefV id'') | TupleT ts, TupleV vs -> let folder = fun (mem, vs') v t -> let (mem', v') = valcopy mem v t in @@ -210,76 +215,25 @@ struct (mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *) | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type" - (* - action rules *) - - let memvmod (a : action) (v_m : memval) : memval = - match a, v_m with - | ReadA, ZeroMV -> ZeroMV - | ReadA, _ -> raise @@ Eval_error "memvmod: forbidden read" - | AlwaysWriteA, _ -> ZeroMV - | MayWriteA, ZeroMV -> ZeroMV - | MayWriteA, _ -> SmthMV - - let readvmod (a : action) (v_r : readval) : readval = - match a, v_r with - | _, TopRV -> TopRV - | _, OneRV -> OneRV - | ReadA, ZeroRV -> OneRV - | AlwaysWriteA, ZeroRV -> TopRV - | MayWriteA, ZeroRV -> ZeroRV - - let writevmod (a : action) (v_w : writeval) : writeval = - match a, v_w with - | ReadA, v -> v - | AlwaysWriteA, _ -> OneWV - | MayWriteA, OneWV -> OneWV - | MayWriteA, v -> v - (* - value update *) - let rec valchange (mem : mem) (v : value) (p : revpath) (b : value) : mem * value = match p, v with + let rec valupd (mem : mem) (v : value) (p : revpath) (b : value) : mem * value = match p, v with | VarRP, _ -> (mem, b) - | DerefRP p, RefV id -> let (mem', v') = valchange mem (mem_get mem id) p b in + | DerefRP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p b in (mem_set mem' id v', RefV id) - | AccessRP (p, id), TupleV vs -> let (mem', v') = valchange mem (List.nth vs id) p b in - (mem', TupleV (list_replace vs id v')) - | _, _ -> raise @@ Typing_error "valupd" - - 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)) - | 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 + | AccessRP (p, id), TupleV vs -> let (mem', v') = (* FIXME TMP Printf.printf "vs size=%i id=%i\n" (List.length vs) id; *) + valupd mem (List.nth vs id) p b in + (* FIXME TMP Printf.printf "before return\n"; *) (mem', TupleV (list_replace vs id v')) | _, _ -> raise @@ Typing_error "valupd" (* - value combination *) - let memvalcomb (u : memval) (v : memval) : memval = - match u, v with - | ZeroMV, ZeroMV -> ZeroMV - | BotMV, BotMV -> BotMV - | _, _ -> SmthMV - - let readvalcomb (u : readval) (v : readval) : readval = - match u, v with - | TopRV, TopRV -> TopRV - | ZeroRV, ZeroRV -> ZeroRV - | TopRV, ZeroRV -> ZeroRV - | ZeroRV, TopRV -> ZeroRV - | _, _ -> OneRV - - let writevalcomb (u : writeval) (v : writeval) : writeval = - match u, v with - | OneWV, OneWV -> OneWV - | ZeroWV, ZeroWV -> ZeroWV - | _, _ -> SmthWV - let rec valcomb (u : value) (v : value) : value = - match u, v with - | UnitV (u_m, u_r, u_w), UnitV (v_m, v_r, v_w) -> - UnitV (memvalcomb u_m v_m, readvalcomb u_r v_r, writevalcomb u_w v_w) - | FunV ustmts, FunV vstmts -> FunV (ustmts @ vstmts) + if is_trivial_v u && is_trivial_v v + then (if u == v then u else BotV) + else match u, v with + | FunV ustmts, FunV vstmts -> FunV (ustmts @ vstmts) | RefV a, RefV b -> if a == b then u else raise @@ Typing_error "valcomb: ref" | TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs) | _, _ -> raise @@ Typing_error "valcomb" @@ -292,7 +246,7 @@ struct (* - expression evaluation *) let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with - | UnitE -> UnitV (ZeroMV, ZeroRV, ZeroWV) + | UnitE -> ZeroV | PathE p -> pathval mem vals p | RefE x -> RefV (vals_assoc x vals) | TupleE es -> TupleV (List.map (exprval mem vals) es) @@ -333,64 +287,48 @@ struct (* - call values spoil *) - (* TODO: check assignment type matches types separately later ?? *) - let is_correct_tags (r : read_cap) (w : write_cap) - (m : mode) (c : copy_cap) : bool = - (snd m != Out || c == Rf) && + (* TODO: check all cases *) + let is_correct_tags (v : value) (r : read_cap) (w : write_cap) + (r' : read_cap) (w' : write_cap) (m : mode) + (c : copy_cap) : bool = + (* FIXME TMP *) + (* Printf.printf "%b %b %b %b %b\n" *) + (* (r != Rd || v == ZeroV) *) + (* (r != Rd || fst m == In) *) + (* (snd m != Out || w == AlwaysWr) *) + (* (* TODO: FIXME: why always write ?? *) *) + (* (((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr)) *) + (* (is_trivial_v v); *) + (r != Rd || v == ZeroV) && + (r != Rd || fst m == In) && (snd m != Out || w == AlwaysWr) && - (r != Rd || fst m == In) - - let tryread (r : read_cap) (v_m : memval) - (v_r : readval) (v_w : writeval) : value = - match r with - | Rd -> UnitV (memvmod ReadA v_m, - readvmod ReadA v_r, - writevmod ReadA v_w) - | NRd -> UnitV (v_m, v_r, v_w) - - let tryspoil (m : mode) (w : write_cap) (v_m : memval) : memval = - match m, w with - | (_, Out), AlwaysWr -> v_m - | (_, Out), MayWr -> v_m - | (_, NOut), AlwaysWr -> BotMV - | (_, NOut), MayWr -> SmthMV - | _ -> raise @@ Typing_error "tryspoil: unexpected pair mode + write cap" + (* TODO: FIXME: check *) + ((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr) && + is_trivial_v v let rec valspoil (mem : mem) (v : value) (t : atype) - (m : mode) (c : copy_cap) - : mem * value = match t, v with - | UnitT (r, w), UnitV (v_m, v_r, v_w) -> - if not @@ is_correct_tags r w m c - then raise @@ Typing_error "valspoil: trivial type tags combination is not correct" - else - let v' = tryread r v_m v_r v_w in - if c == Cp || w == NeverWr - then (mem, v') - else (match v' with - | UnitV (v_m', v_r', v_w') -> - let (v_m'', v_r'', v_w'') = - (if w == AlwaysWr - then (memvmod AlwaysWriteA v_m', - readvmod AlwaysWriteA v_r', - writevmod AlwaysWriteA v_w') - else (* MayWr *) - (memvmod MayWriteA v_m', - readvmod MayWriteA v_r', - writevmod MayWriteA v_w')) - in - let v_m''' = tryspoil m w v_m'' in - (mem, UnitV (v_m''', v_r'', v_w'')) - | _ -> raise @@ Typing_error "valspoil: value after tryread is not unit") - | FunT ts, FunV _ -> (mem, v) - | RefT (ct, t), RefV id -> - let (mem', v') = valspoil mem (mem_get mem id) t m ct in + (u : atype) (m : mode) (c : copy_cap) + : mem * value = match t, u, v with + | UnitT (r, w), UnitT (r', w'), _ -> + if not @@ is_trivial_v v + then raise @@ Typing_error "valspoil: unit, not trivial" + else if not @@ is_correct_tags v r w r' w' m c + then raise @@ Typing_error "valspoil: unit, not correct" + else if snd m == NOut && c == Rf && (w == AlwaysWr || w == MayWr) + then (mem, BotV) + else if snd m == Out && w == AlwaysWr + then (mem, ZeroV) + else (mem, v) + | FunT ts, FunT us, FunV _ -> if ts == us then (mem, v) else raise @@ Typing_error "valspoil: fun" + | RefT (ct, t), RefT (cu, u), RefV id -> + let (mem', v') = valspoil mem (mem_get mem id) t u m ct in (mem_set mem id v', RefV id) - | TupleT ts, TupleV vs -> - let folder = fun (mem, vs') t v -> - let (mem', v') = valspoil mem v t m c in (mem', v' :: vs') in - let (mem', vs') = List.fold_left2 folder (mem, []) ts vs in + | TupleT ts, TupleT us, TupleV vs -> + let folder = fun (mem, vs') t u v -> + let (mem', v') = valspoil mem v t u m c in (mem', v' :: vs') in + let (mem', vs') = list_foldl3 folder (mem, []) ts us vs in (mem', TupleV (List.rev vs')) - | _, _ -> raise @@ Typing_error "valspoil" + | _, _, _ -> raise @@ Typing_error "valspoil" (* full spoil *) @@ -399,11 +337,11 @@ struct let x = pathvar p in let id = vals_assoc x vals in (* base var address *) let b = pathval mem vals p in (* subvalue in var *) - (* let t' = pathtype types p in (* type of subvalue *) *) - let (mem', b') = valspoil mem b t m Cp in (* spoil subvalue *) + let t' = pathtype types p in (* type of subvalue *) + let (mem', b') = valspoil mem b t t' m Cp in (* spoil subvalue *) (* TODO: FIXME: why copy (Cp)? maybe sometimes use top-level capability ? *) let pi = pathrev p VarRP in - let (mem'', v'') = valchange mem' (mem_get mem' id) pi b' in (* set subvalue into var *) + let (mem'', v'') = valupd mem' (mem_get mem' id) pi b' in (* set subvalue into var *) mem_set mem'' id v'' let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem = @@ -431,34 +369,15 @@ struct (* NOTE: not needed due to performed optimization in stmt_eval *) (* let func_eval (mem : mem) (vals : vals) (s : stmt) (ts : mtype list) (es : expr list) = *) - let writeval_to_cap (v_w : writeval) : write_cap = - match v_w with - | ZeroWV -> NeverWr - | SmthWV -> MayWr - | OneWV -> AlwaysWr - - let rec tags_check (mem : mem) (v : value) (t : atype) : unit = - match v, t with - | UnitV (v_m, v_r, v_w), UnitT (r, w) -> - if (r == Rd) && (v_r != OneRV) - then raise @@ Eval_error "tags_check: wrong read tag" - else if (r == NRd) && (v_r == OneRV) - then raise @@ Eval_error "tags_check: wrong not read tag" - else if writeval_to_cap v_w != w - then raise @@ Eval_error "tags_check: wrong write tag" - else () - | FunV _, FunT _ -> () - | RefV id, RefT (_, t) -> tags_check mem (mem_get mem id) t - | TupleV vs, TupleT ts -> ignore @@ List.map2 (tags_check mem) vs ts - | _, _ -> raise @@ Typing_error "tags_check" - (* - statement evaluation *) let rec stmt_eval (state : state) (s : stmt) : state = match state with (mem, types, vals, visited) -> match s with | SkipS -> state - | CallS (f, es) -> let v = pathval mem vals f in - let t = pathtype types f in + | CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *) + pathval mem vals f in + let t = (* FIXME TMP Printf.printf "call, before t\n"; *) + pathtype types f in let types' : types = (fst types, fst types) in let vals' : vals = (fst vals, fst vals) in (match v, t with @@ -475,14 +394,7 @@ struct if List.mem stmt visited_old then stmt :: visited_old else match stmt_eval (mem_swa, types_swa, vals_swa, stmt :: visited_old) stmt with - (mem_after_stmt, _, vals_after_stmt, visited_after_stmt) -> - ignore @@ List.fold_left - (fun x (_, t) -> - let id = vals_assoc x vals_after_stmt in - let v = mem_get mem_after_stmt id in - tags_check mem_after_stmt v t; x + 1) - 0 ts; - visited_after_stmt) + (_, _, _, visited_after_stmt) -> visited_after_stmt) visited_swa fstmts in let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *) @@ -500,28 +412,16 @@ struct 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 + let (mem', v') = valupd mem (mem_get mem id) pi ZeroV 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") - (* 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" *) + | ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV + then raise @@ Eval_error "read: spoiled value" + else if pathval mem vals p != ZeroV + then raise @@ Eval_error "read: nontrivial value" + else state | SeqS (sl, sr) -> let statel = stmt_eval state sl in stmt_eval statel sr | ChoiceS (sl, sr) -> let statel = stmt_eval state sl in @@ -570,7 +470,6 @@ struct let vg8 = VarP (globals_min_id + 8) let vg9 = VarP (globals_min_id + 9) let vg10 = VarP (globals_min_id + 10) - let vg11 = VarP (globals_min_id + 11) let rf0E = RefE 0 let rf1E = RefE 1 @@ -619,30 +518,23 @@ struct let rdS p = ReadS p let callS f args = CallS (f, args) - let uV m = UnitV (m, ZeroRV, ZeroWV) - (* - utils tests *) - let v_memval_is v m = - match v with - | UnitV (v_m, _, _) -> v_m == m - | _ -> false - let%expect_test "mem add / get / set" = let mem = empty_mem in - let (mem, id1) = mem_add mem @@ uV ZeroMV in - let (mem, id2) = mem_add mem @@ uV SmthMV in - let (mem, id3) = mem_add mem @@ uV BotMV in + let (mem, id1) = mem_add mem ZeroV in + let (mem, id2) = mem_add mem SmthV in + let (mem, id3) = mem_add mem BotV in Printf.printf "%i %i %i " id1 id2 id3; - Printf.printf "%b %b %b " (v_memval_is (mem_get mem id1) ZeroMV) - (v_memval_is (mem_get mem id2) SmthMV) - (v_memval_is (mem_get mem id3) BotMV); - let mem = mem_set mem id1 @@ uV BotMV in - let mem = mem_set mem id2 @@ uV ZeroMV in - let mem = mem_set mem id3 @@ uV SmthMV in - Printf.printf "%b %b %b" (v_memval_is (mem_get mem id1) BotMV) - (v_memval_is (mem_get mem id2) ZeroMV) - (v_memval_is (mem_get mem id3) SmthMV); + Printf.printf "%b %b %b " (mem_get mem id1 == ZeroV) + (mem_get mem id2 == SmthV) + (mem_get mem id3 == BotV); + let mem = mem_set mem id1 BotV in + let mem = mem_set mem id2 ZeroV in + let mem = mem_set mem id3 SmthV in + Printf.printf "%b %b %b" (mem_get mem id1 == BotV) + (mem_get mem id2 == ZeroV) + (mem_get mem id3 == SmthV); [%expect {| 0 1 2 true true true true true true |}] (* - basic var tests *) @@ -663,7 +555,7 @@ struct ReadS (VarP globals_min_id)); [%expect.unreachable]); with Eval_error msg -> Printf.printf "%s" msg; - [%expect {| memvmod: forbidden read |}] + [%expect {| read: spoiled value |}] let%expect_test "simple vars, no read & read" = prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE); @@ -729,10 +621,10 @@ struct let%expect_test "simple call with write, dsl" = prog_eval_noret ( [ - defgu uT_aw; - defg (rfT uT_aw) rfg0E; + defgu uT_r_mw; + defg (rfT uT_r_mw) rfg0E; FunD ( - [moded @@ cpT @@ uT_aw], + [moded @@ cpT @@ uT_r_mw], wrS @@ drf @@ v0 ) ], @@ -744,10 +636,10 @@ struct let%expect_test "simple call with read after write, dsl" = prog_eval_noret ( [ - defgu uT_aw; - defg (rfT uT_aw) rfg0E; + defgu uT_r_mw; + defg (rfT uT_r_mw) rfg0E; FunD ( - [moded @@ cpT @@ uT_aw], + [moded @@ cpT @@ uT_mw], (wrS @@ drf @@ v0) #. (rdS @@ drf @@ v0) ) @@ -804,7 +696,7 @@ struct ); [%expect.unreachable]); with Eval_error msg -> Printf.printf "%s" msg; - [%expect {| memvmod: forbidden read |}] + [%expect {| read: spoiled value |}] let%expect_test "simple call with write to ref with fix, dsl" = prog_eval_noret ( @@ -887,9 +779,9 @@ struct prog_eval_noret ( [ defgu uT_r_aw; - defg (rfT uT_r) rfg0E; + defg (rfT uT_r_aw) rfg0E; FunD ( - [moded @@ cpT @@ uT], + [moded @@ cpT @@ uT_aw], (wrS @@ vg0) #. (rdS @@ drf @@ vg1) ) @@ -903,10 +795,10 @@ struct let%expect_test "simple call with read & write (2 args), dsl" = prog_eval_noret ( [ - defgu uT_r; - defg (rfT uT_r) rfg0E; - defgu uT_aw; - defg (rfT uT_aw) rfg2E; + defgu uT_r_aw; + defg (rfT uT_r_aw) rfg0E; + defgu uT_r_aw; + defg (rfT uT_r_aw) rfg2E; FunD ( [ moded @@ rfT @@ uT_r; @@ -934,10 +826,10 @@ struct defg (rfT uT_r_aw) rfg6E; FunD ( [ - ((NIn, NOut), cpT @@ uT); + ((NIn, NOut), cpT @@ uT_aw); ((In, NOut), cpT @@ uT_r_aw); - ((NIn, Out), rfT @@ uT_aw); - ((In, Out), rfT @@ uT_r_aw); + ((NIn, Out), cpT @@ uT_aw); + ((In, Out), cpT @@ uT_r_aw); ], (rdS @@ drf @@ v1) #. (rdS @@ drf @@ v3) #. @@ -958,10 +850,10 @@ struct let%expect_test "simple call with different arguments modifiers, ref, dsl" = prog_eval_noret ( [ - defgu uT_r; - defg (rfT uT_r) rfg0E; - defgu uT_r; - defg (rfT uT_r) rfg2E; + defgu uT_r_aw; + defg (rfT uT_r_aw) rfg0E; + defgu uT_r_aw; + defg (rfT uT_r_aw) rfg2E; defgu uT_r_aw; defg (rfT uT_r_aw) rfg4E; defgu uT_r_aw; @@ -988,195 +880,83 @@ struct Printf.printf "done!"; [%expect {| done! |}] - (* - tests for presentation *) + (* - complex tests *) - let%expect_test "presentation test 1 (simple types), dsl" = + (* NOTE: path access isreversed to intuitive function application + by definition *) + let%expect_test "complex test: send, dsl" = prog_eval_noret ( + (* TODO: set optimal ref mods later *) + let user_utilsT = TupleT [uT_r_aw (* 0 id *); uT_r_aw] in + let user_infoT = TupleT [uT_r_aw (* 0 name *); uT_r_aw; uT_r_aw] in + let userT = TupleT [cpT user_utilsT (* 0 utils *); cpT user_infoT (* 1 info *)] in + let versionT = TupleT [uT_r_aw (* 0 id *); uT_r_aw; uT_r_aw] in + let utilsT = TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 1 id *)] in + let requestT = TupleT [cpT userT (* 0 user *); + cpT versionT (* 1 version *); + cpT utilsT (* 2 utils *); + cpT uT_r_aw (* 3 data *); + uT_r_aw (* 4 operation_date *)] in + let user_utilsE = TupleE [UnitE (* 0 id *); UnitE] in + let user_infoE = TupleE [UnitE (* 0 name *); UnitE; UnitE] in + let userE = TupleE [rfg0E (* 0 utils *); rfg1E (* 1 info *)] in + let versionE = TupleE [UnitE (* 0 id *); UnitE; UnitE] in + let utilsE = TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] in + let requestE = TupleE [rfg2E (* 0 user *); + rfg3E (* 1 version *); + rfg4E (* 2 utils *); + rfg5E (* 3 data *); + UnitE (* 4 operation_date *)] in + let get_version_idID = vg7 in + let updated_versionID = vg8 in + let sendID = vg9 in + let send_allID = vg10 in + let get_version_idF = FunD ([moded requestT], + (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in + let updated_versionF = FunD ([moded requestT], + (rdS @@ access 0 @@ drf @@ access 2 v0) #. + (* TODO: read all the substructure ?? *) + (rdS @@ access 0 @@ drf @@ access 1 v0) #. + (rdS @@ access 1 @@ drf @@ access 1 v0)) in + let sendF = FunD ([moded requestT], + (( + (wrS @@ access 0 @@ drf @@ access 2 v0) #. + (rdS @@ drf @@ access 3 v0) #. + (wrS @@ drf @@ access 3 v0) #. + (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0) + ) |. skp) #. + (wrS @@ access 4 v0) #. + (* TODO: read all the substructure ?? *) + (rdS @@ access 4 v0) (*rdS v0*)) in (* FIXME: TMP, parial read, should be full *) + let send_allF = FunD ([moded requestT], + (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *) + (callS sendID [pE v0]) #. + (callS get_version_idID [pE v0]) #. + (callS updated_versionID [pE v0]) #. + (* TODO: read all the substructure ?? *) + (wrS @@ access 0 @@ drf @@ access 1 v0) #. + (wrS @@ access 1 @@ drf @@ access 1 v0) #. + (* --- *) + ((rdS @@ access 0 @@ drf @@ access 0 @@ drf @@ access 0 v0) |. + (rdS @@ access 0 @@ drf @@ access 1 v0))) in + let varID = vg6 in [ + defg user_utilsT user_utilsE; + defg user_infoT user_infoE; + defg userT userE; + defg versionT versionE; + defg utilsT utilsE; defgu uT_r_aw; - defg (rfT uT_r_aw) rfg0E; (* x *) - defgu uT_r_aw; - defg (rfT uT_r_aw) rfg2E; (* y *) - defgu uT_r_aw; - defg (rfT uT_r_aw) rfg4E; (* z *) - defgu uT_r_aw; - defg (rfT uT_r_aw) rfg6E; (* k *) - FunD ( (* f *) - [ - (moded @@ rfT @@ uT_r_aw); - (moded @@ rfT @@ uT_r); - ], - (rdS @@ drf @@ v0) #. - (wrS @@ drf @@ v0) #. - (rdS @@ drf @@ v1) - ); - FunD ( (* w *) - [ - (moded @@ cpT @@ uT_mw); - ], - (wrS @@ drf @@ v0) |. skp - ); - FunD ( (* g *) - [ - (moded @@ rfT @@ uT_aw); - (moded @@ cpT @@ uT_r_mw); - ], - (wrS @@ drf @@ v0) #. - ((wrS @@ drf @@ v1) |. (wrS @@ drf @@ v0)) #. - (rdS @@ drf @@ v0) #. - (rdS @@ drf @@ v1) - ); - FunD ( (* r *) - [ - (moded @@ rfT @@ uT_r); - ], - (rdS @@ drf @@ v0) - ) + defg requestT requestE; + get_version_idF; + updated_versionF; + sendF; + send_allF ], - let xV = vg1 in - let yV = vg3 in - let zV = vg5 in - let kV = vg7 in - let fF = vg8 in - let wF = vg9 in - let gF = vg10 in - let rF = vg11 in - (callS wF [pE xV]) #. - (callS rF [pE xV]) #. - (callS fF [pE xV; pE yV]) #. - (callS rF [pE yV]) #. - (callS gF [pE zV; pE kV]) #. - (wrS @@ drf @@ zV) #. - (callS wF [pE zV]) #. - (callS fF [pE yV; pE zV]) #. - (callS rF [pE kV]) + callS send_allID [pE varID] ); Printf.printf "done!"; [%expect {| done! |}] - (* TODO tags, access *) - (* let%expect_test "presentation test 2 (complex types), dsl" = *) - (* prog_eval_noret ( *) - (* let userT = TupleT [uT_r_aw; uT_r_aw; uT_r_aw] in *) - (* let dataT = TupleT [uT_r_aw; uT_r_aw] in *) - (* let requestT = TupleT [cpT userT; *) - (* cpT dataT; *) - (* cpT dataT] in *) - (* let requestArgsT = TupleT [cpT userT; (* TODO: tags *) *) - (* cpT dataT; *) - (* cpT dataT] in *) - (* let userE = TupleE [UnitE; UnitE; UnitE] in *) - (* let dataE = TupleE [UnitE; UnitE] in *) - (* let requestE = TupleE [rfg0E; rfg1E; rfg2E] in *) - (* [ *) - (* defg userT userE; *) - (* defg dataT dataE; *) - (* defgu uT_r_aw; (* time *) *) - (* defg requestT requestE; *) - (* FunD ( (* send *) *) - (* [ *) - (* (moded @@ requestArgsT) *) - (* ], *) - (* ( *) - (* ( (* TODO access *) *) - (* (rdS @@ drf @@ v0) #. *) - (* (wrS @@ drf @@ v0) #. *) - (* (rdS @@ drf @@ v0) #. *) - (* (wrS @@ drf @@ v0) *) - (* ) |. *) - (* skp) #. *) - (* TODO access *) - (* (wrS @@ drf @@ v0) #. *) - (* (rdS @@ drf @@ v1) *) - (* ); *) - (* ], *) - (* (callS vg4 [pE vg3]) #. *) - (* TODO access *) - (* (wrS @@ drf @@ vg3) #. *) - (* ((rdS @@ drf @@ vg3) |. (rdS @@ drf @@ vg3)) #. *) - (* (rdS @@ drf @@ vg3) *) - (* ); *) - (* Printf.printf "done!"; *) - (* [%expect {| done! |}] *) - - (* - complex tests *) - - (* TODO: FIXME: rw tags *) - (* NOTE: path access isreversed to intuitive function application - by definition *) - (* let%expect_test "complex test: send, dsl" = *) - (* prog_eval_noret ( *) - (* TODO: set optimal ref mods later *) - (* let user_utilsT = TupleT [uT_r_aw (* 0 id *); uT_r_aw] in *) - (* let user_infoT = TupleT [uT_r_aw (* 0 name *); uT_r_aw; uT_r_aw] in *) - (* let userT = TupleT [cpT user_utilsT (* 0 utils *); cpT user_infoT (* 1 info *)] in *) - (* let versionT = TupleT [uT_r_aw (* 0 id *); uT_r_aw; uT_r_aw] in *) - (* let utilsT = TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 1 id *)] in *) - (* let requestT = TupleT [cpT userT (* 0 user *); *) - (* cpT versionT (* 1 version *); *) - (* cpT utilsT (* 2 utils *); *) - (* cpT uT_r_aw (* 3 data *); *) - (* uT_r_aw (* 4 operation_date *)] in *) - (* let user_utilsE = TupleE [UnitE (* 0 id *); UnitE] in *) - (* let user_infoE = TupleE [UnitE (* 0 name *); UnitE; UnitE] in *) - (* let userE = TupleE [rfg0E (* 0 utils *); rfg1E (* 1 info *)] in *) - (* let versionE = TupleE [UnitE (* 0 id *); UnitE; UnitE] in *) - (* let utilsE = TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] in *) - (* let requestE = TupleE [rfg2E (* 0 user *); *) - (* rfg3E (* 1 version *); *) - (* rfg4E (* 2 utils *); *) - (* rfg5E (* 3 data *); *) - (* UnitE (* 4 operation_date *)] in *) - (* let get_version_idID = vg7 in *) - (* let updated_versionID = vg8 in *) - (* let sendID = vg9 in *) - (* let send_allID = vg10 in *) - (* let get_version_idF = FunD ([moded requestT], *) - (* (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in *) - (* let updated_versionF = FunD ([moded requestT], *) - (* (rdS @@ access 0 @@ drf @@ access 2 v0) #. *) - (* TODO: read all the substructure ?? *) - (* (rdS @@ access 0 @@ drf @@ access 1 v0) #. *) - (* (rdS @@ access 1 @@ drf @@ access 1 v0)) in *) - (* let sendF = FunD ([moded requestT], *) - (* (( *) - (* (wrS @@ access 0 @@ drf @@ access 2 v0) #. *) - (* (rdS @@ drf @@ access 3 v0) #. *) - (* (wrS @@ drf @@ access 3 v0) #. *) - (* (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0) *) - (* ) |. skp) #. *) - (* (wrS @@ access 4 v0) #. *) - (* TODO: read all the substructure ?? *) - (* (rdS @@ access 4 v0) (*rdS v0*)) in (* FIXME: TMP, parial read, should be full *) *) - (* let send_allF = FunD ([moded requestT], *) - (* (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *) *) - (* (callS sendID [pE v0]) #. *) - (* (callS get_version_idID [pE v0]) #. *) - (* (callS updated_versionID [pE v0]) #. *) - (* TODO: read all the substructure ?? *) - (* (wrS @@ access 0 @@ drf @@ access 1 v0) #. *) - (* (wrS @@ access 1 @@ drf @@ access 1 v0) #. *) - (* --- *) - (* ((rdS @@ access 0 @@ drf @@ access 0 @@ drf @@ access 0 v0) |. *) - (* (rdS @@ access 0 @@ drf @@ access 1 v0))) in *) - (* let varID = vg6 in *) - (* [ *) - (* defg user_utilsT user_utilsE; *) - (* defg user_infoT user_infoE; *) - (* defg userT userE; *) - (* defg versionT versionE; *) - (* defg utilsT utilsE; *) - (* defgu uT_r_aw; *) - (* defg requestT requestE; *) - (* get_version_idF; *) - (* updated_versionF; *) - (* sendF; *) - (* send_allF *) - (* ], *) - (* callS send_allID [pE varID] *) - (* ); *) - (* Printf.printf "done!"; *) - (* [%expect {| done! |}] *) - (* TODO: version with more optimal modifiers *) end diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 42d7b14..ae6fc97 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -13,7 +13,7 @@ == Syntax -// *TODO: top-level value copy mode ??* // TODO: FIXME +*TODO: top-level value copy mode ??* // TODO: FIXME *TODO: add formal global env to all types and vals (as in code) ??* // TODO: FIXME @@ -48,9 +48,6 @@ #let cl = $chevron.l$ #let cr = $chevron.r$ -#let cdl = $chevron.l.double$ -#let cdr = $chevron.r.double$ - #let expr = `expr` #let stmt = `stmt` #let decl = `decl` @@ -154,73 +151,55 @@ == Value Model -// #let deepValue = `deepvalue` +#let deepValue = `deepvalue` #let value = `value` -#let vmem = $v_#[`mem`]$ -#let vread = $v_#[`read`]$ -#let vwrite = $v_#[`write`]$ #let revpath = $#[`path`]_#[`rev`]$ #bnf( - // Prod( - // $deepValue$, - // { - // Or[$0$][valid value of simple type] // `Unit` - // Or[$\#$][valid or spoiled value of simple type] // `Unit` - // Or[$bot$][spoiled value of simple type] // `Unit` - // Or[$lambda space (X+ stmt)+$][function pointer value, set of possible values] // `Fun` - // Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref` - // Or[$[deepValue+]$][tuple value] // `Prod` - // } - // ), Prod( - $vmem$, + $deepValue$, { - Or[$0$][valid value of simple type] - Or[$?$][valid or spoiled value of simple type] - Or[$bot$][spoiled value of simple type] - // NOTE: proably can't use correctly - // Or[$top$][value that is not spoiled because of the copy tag] - } - ), - Prod( - $vread$, - { - Or[$0_r$][argument not read] - Or[$1_r$][argument read] - Or[$top_r$][argument already written from the function beginning] - } - ), - Prod( - $vwrite$, - { - Or[$0_w$][no write] - Or[$?_w$][maybe write] - Or[$1_w$][always write] + Or[$0$][valid value of simple type] // `Unit` + Or[$\#$][valid or spoiled value of simple type] // `Unit` + Or[$bot$][spoiled value of simple type] // `Unit` + Or[$lambda space (X+ stmt)+$][function pointer value, set of possible values] // `Fun` + Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref` + Or[$[deepValue+]$][tuple value] // `Prod` } ), Prod( $value_mu$, { - Or[$cdl vmem, vread, vwrite cdr$][value of the simple type, contains cells for analysis] // `Unit` + Or[$0$][valid value of simple type] // `Unit` + Or[$\#$][valid or spoiled value of simple type] // `Unit` + Or[$bot$][spoiled value of simple type] // `Unit` Or[$lambda space (X+ stmt)+$][function pointer value, set of possible values] // `Fun` Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref` Or[$[value+]$][tuple value] // `Prod` } ), + Prod( + revpath, + { + Or[$\# .$][value by itself] + Or[$rf revpath$][reference to value] + Or[$n . revpath$][tuple with value as $n$-th element] + } + ), ) -// #deepValue - полное значение, -#value - слой значения, привязан к конкретной памяти $mu$ +#deepValue - полное значение, #value - слой значения, привязан к конкретной памяти $mu$ Значения, могут лежать в переменных и передаваться как аргументы функций (то, во что вычисляется $expr$) +$revpath$ - путь в обратную сторону, используется для обновления значений + $v in value$ - произвольное значение -// Получение #deepValue по #value: -// - $rf l xarrowSquiggly(mu)_#[deep] rf mu[l]$ -// - $* xarrowSquiggly(mu)_#[deep] *$ -// где $*$ - произвольный конструктор значения, кроме $rf$ +Получение #deepValue по #value: +- $rf l xarrowSquiggly(mu)_#[deep] rf mu[l]$ +- $* xarrowSquiggly(mu)_#[deep] *$ +где $*$ - произвольный конструктор значения, кроме $rf$ == Memory Model @@ -244,44 +223,13 @@ $v in value$ - произвольное значение == Semantics -#let action = `action` -#let readA = $#[`READ`]_a$ -#let writeA = $#[`WRITE`]_a$ -#let mbwriteA = $#[`MAYWRITE`]_a$ -// #let spoilA = $#[`SPOIL`]_a$ -// #let nospoilA = $#[`NOSPOIL`]_a$ - -#bnf( - Prod( - revpath, - { - Or[$\# .$][value by itself] - Or[$rf revpath$][reference to value] - Or[$n . revpath$][tuple with value as $n$-th element] - } - ), - Prod( - $action$, - { - Or[$readA$][value read] - Or[$writeA$][value written] - Or[$mbwriteA$][value maybe written] - // NOTE: not required, spoils only first element ? - // Or[$spoilA$][value passed as funciton argument and spoiled] - // NOTE: probably acutally can't reliebly forbid Cp - // Or[$nospoilA$][value passed as funciton argument and not changed, - // but could be spoiled if mode will be $Copy$ instead of $Ref$] - // TODO: better wording ?? - } - ), -) - // TODO: FIXME: add vars & funcs from global context in the beginnning // $V := memelem$ - значения памяти $X$ - можество переменных + #let vals = $Sigma$ #let types = $Gamma$ #let envv = $#[env]_Sigma$ @@ -289,11 +237,6 @@ $X$ - можество переменных $sigma : envv := X -> LL, space vals : envv$ - #[ метки памяти перменных контекста, частично определённая функция ] $sigma : envt := X -> type, space types : envt$ - #[ типы значений перменных контекста, частично определённая функция ] -$revpath$ - путь в обратную сторону, используется для обновления значений - -$action$ - действия, совершаемые с примитивным значением, - модифицирующие содержащуюся таминформацию - // $DD : X -> decl$ - глобальные определения, частично определённая функция // $d in decl, $ @@ -494,7 +437,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ // // $sigma temode x -> cr r' space w' cl$, // NOTE: not required, value passed // $(w = AlwaysWrite or w = MaybeWrite) and (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$, // // $sigma, mu teval x eqmu v$, // NOTE: not required, value passed -// $v in {0, ?, bot}$, +// $v in {0, \#, bot}$, // $r = Read => v = 0$, // $types, vals, mu, m, c tcorrect v : cl r', w' cr -> cl r, w cr$, // ) @@ -542,33 +485,18 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ rule( name: [ new trivial read value], - $v_m in {0, ?, bot}$, - $cl cdl v_m, v_r, v_w cdr, mu cr - xarrowSquiggly(cl Read \, w cr)_new - cl cdl v_m, 0, 0 cdr, mu cr$, + $v in {0, \#, bot}$, + $cl v, mu cr xarrowSquiggly(cl Read \, w cr)_new cl v, mu cr$, ) )) -// #align(center, prooftree( -// vertical-spacing: 4pt, -// rule( -// name: [ new trivial read $top$ value], - -// $cl cdl top, v_r, v_w cdr, mu cr -// xarrowSquiggly(cl Read \, w cr)_new -// cl cdl 0, 0, 0 cdr, mu cr$, -// ) -// )) - #align(center, prooftree( vertical-spacing: 4pt, rule( name: [ new trivial $not$ read value], - $v_m in {0, ?, bot/*, top */}$, - $cl cdl v_m, v_r, v_w cdr, mu cr - xarrowSquiggly(cl not Read \, w cr)_new - cl cdl bot, 0, 0 cdr, mu cr$, + $v in {0, \#, bot}$, + $cl v, mu cr xarrowSquiggly(cl not Read \, w cr)_new cl bot, mu cr$, ) )) @@ -577,30 +505,32 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ rule( name: [ new funciton pointer value], - $cl lambda overline(s), mu cr xarrowSquiggly(lambda space c space overline(t))_new cl lambda overline(s), mu cr$, + $cl lambda overline(t) s, mu cr xarrowSquiggly(lambda space c space overline(t))_new cl lambda overline(t) s, mu cr$, ) )) -// #align(center, prooftree( -// vertical-spacing: 4pt, -// rule( -// name: [ new reference ref value], - -// $cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$, -// ) -// )) - -// NOTE: due to new memory cells types (with rw subcells) valnue should always be copied #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ new reference /* copy */ value], + name: [ new reference ref value], + + // TODO: FIXME: recursive copy ?? (what heppens if ref field has copy substructure ??) + // <- forbidden ?? + + $cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$, + ) +)) + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ new reference copy value], $cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$, $mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$, - $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_new cl rf l', mu_a cr$, + $cl rf l, mu cr xarrowSquiggly(rf Copy t)_new cl rf l', mu_a cr$, ) )) @@ -617,152 +547,18 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ ) )) -=== Action Rules - -#let modM = $attach(<-, br: m)$ -#let modR = $attach(<-, br: r)$ -#let modW = $attach(<-, br: w)$ - -#align(center, grid( - columns: 3, - gutter: 10%, - align: center, - table( - columns: 3, - table.header( - [*a*], [*x*], $modM$ - ), - $readA$, $0$, $0$, - // $readA$, $top$, $0$, - $readA$, $?$, $-$, // err - $readA$, $bot$, $-$, // err - $writeA$, $0$, $0$, - // $writeA$, $top$, $-$, - $writeA$, $?$, $0$, - $writeA$, $bot$, $0$, - $mbwriteA$, $0$, $0$, - // $mbwriteA$, $top$, $top$, - $mbwriteA$, $?$, $?$, - $mbwriteA$, $bot$, $?$, - // $spoilA$, $0$, $bot$, - // // $spoilA$, $top$, $bot$, - // $spoilA$, $?$, $bot$, - // $spoilA$, $bot$, $bot$, - // $nospoilA$, $0$, $top$, - // $nospoilA$, $top$, $top$, - // $nospoilA$, $?$, $-$, // ?? - // $nospoilA$, $bot$, $-$, - ), - - table( - columns: 3, - table.header( - [*a*], [*x*], $modR$ - ), - $readA$, $1$, $1$, - $readA$, $0$, $1$, - $readA$, $top$, $top$, - $writeA$, $1$, $1$, - $writeA$, $0$, $top$, - $writeA$, $top$, $top$, - $mbwriteA$, $1$, $1$, - $mbwriteA$, $0$, $0$, - $mbwriteA$, $top$, $top$, - - // $spoilA$, $1$, $1$, - // $spoilA$, $0$, $0$, - // $spoilA$, $top$, $top$, - // $nospoilA$, $1$, $1$, - // $nospoilA$, $0$, $0$, - // $nospoilA$, $top$, $top$, - ), - - table( - columns: 3, - table.header( - [*a*], [*x*], $modW$ - ), - $readA$, $1$, $1$, - $readA$, $?$, $?$, - $readA$, $0$, $0$, - $writeA$, $1$, $1$, - $writeA$, $?$, $1$, - $writeA$, $0$, $1$, - $mbwriteA$, $1$, $1$, - $mbwriteA$, $?$, $?$, - $mbwriteA$, $0$, $?$, - - // $spoilA$, $1$, $1$, - // $spoilA$, $?$, $?$, - // $spoilA$, $0$, $0$, - // $nospoilA$, $1$, $1$, - // $nospoilA$, $?$, $?$, - // $nospoilA$, $0$, $0$, - ) -)) - -Прочерк \"$-$\" означает, что данная операция не определена. - === Value Update -==== Change - -Замена подзначения в значении по $revpath$, $b in value$. - -#let change = `change` - -// TODO: add type check ?? -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ change final value], - - // $v in {0, ?, bot}$, - $cl v, mu cr xarrowSquiggly(cl \# . \, b cr)_change cl b, mu cr$, - ) -)) - -#h(10pt) - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ change reference value], - - $cl mu[l], mu cr xarrowSquiggly(cl pi \, b cr)_change cl v', mu' cr$, - $cl rf l, mu cr xarrowSquiggly(cl rf pi \, b cr)_change cl rf l, mu'[l <- v'] cr$, - ) -)) - -#h(10pt) - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ change tuple value], - - $cl v_i, mu cr xarrowSquiggly(cl p \, b cr)_change cl v'_i, mu', cr$, - $cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl i.pi \, b cr)_change cl [v_1, ... v'_i, ... v_n], mu' cr$, - ) -)) - -#h(10pt) - -==== Modify - -Совершение операции над тривиальным подзначением в значении по $revpath$, $a in action$ - #let modify = `modify` // TODO: add type check ?? #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ modify final value], + name: [ modify end value], - $cl cdl v_m, v_r, v_w cdr, mu cr - xarrowSquiggly(cl \# . \, a cr)_modify - cl cdl v_m modM a, v_r modR a, v_w modW a cdr, mu cr$, + // $v in {0, \#, bot}$, + $cl v, mu cr xarrowSquiggly(cl \# . \, b cr)_modify cl b, mu cr$, ) )) @@ -771,10 +567,10 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ modify reference value], + name: [ new reference copy value], - $cl mu[l], mu cr xarrowSquiggly(cl pi \, a cr)_modify cl v', mu' cr$, - $cl rf l, mu cr xarrowSquiggly(cl rf pi \, a cr)_modify cl rf l, mu'[l <- v'] cr$, + $cl mu[l], mu cr xarrowSquiggly(cl pi \, b cr)_modify cl v', mu' cr$, + $cl rf l, mu cr xarrowSquiggly(cl rf pi \, b cr)_modify cl rf l, mu'[l <- v'] cr$, ) )) @@ -785,8 +581,8 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ rule( name: [ modify tuple value], - $cl v_i, mu cr xarrowSquiggly(cl p \, a cr)_modify cl v'_i, mu', cr$, - $cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl i.pi \, a cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$, + $cl v_i, mu cr xarrowSquiggly(cl p \, b cr)_modify cl v'_i, mu', cr$, + $cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl i.pi \, b cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$, ) )) @@ -794,74 +590,29 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ === Value Combination -#align(center, grid( - columns: 3, - gutter: 20%, - align: center, - table( - columns: 3, - table.header( - [*x*], [*y*], $plus.o_m$ - ), - $0$, $0$, $0$, - // $0$, $top$, $0$, - $0$, $?$, $?$, - $0$, $bot$, $?$, - $?$, $0$, $?$, - $?$, $?$, $?$, - $?$, $bot$, $?$, - // $?$, $top$, $?$, - $bot$, $0$, $?$, - $bot$, $?$, $?$, - // $bot$, $top$, $?$, - // $top$, $0$, $?$, - // $top$, $?$, $?$, - // $top$, $bot$, $?$, - $bot$, $bot$, $bot$, - // $top$, $top$, $top$, - ), +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ combine same trivial values], - table( - columns: 3, - table.header( - [*x*], [*y*], $plus.o_r$ - ), - $1$, $1$, $1$, - $1$, $0$, $1$, - $1$, $top$, $1$, - $0$, $1$, $1$, - $top$, $1$, $1$, - $0$, $0$, $0$, - $0$, $top$, $0$, - $top$, $0$, $0$, - $top$, $top$, $top$, - ), - - table( - columns: 3, - table.header( - [*x*], [*y*], $plus.o_w$ - ), - $1$, $1$, $1$, - $1$, $?$, $?$, - $1$, $0$, $?$, - $?$, $1$, $?$, - $?$, $?$, $?$, - $?$, $0$, $?$, - $0$, $1$, $?$, - $0$, $?$, $?$, - $0$, $0$, $0$, + $v_1 in {0, \#, bot}$, + $v_2 in {0, \#, bot}$, + $v_1 = v_2$, + $v_1 plus.o v_2 = v_1$ ) )) +#h(10pt) + #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ combine trivial values], + name: [ combine different trivial values], - $v_1 = cdl v_1_m, v_1_r, v_1_w cdr$, - $v_2 = cdl v_2_m, v_2_r, v_2_w cdr$, - $v_1 plus.o v_2 = cdl v_1_m plus.o_m v_2_m, v_1_r plus.o_r v_2_r, v_1_w plus.o_w v_2_w cdr$ + $v_1 in {0, \#, bot}$, + $v_2 in {0, \#, bot}$, + $v_1 != v_2$, + $v_1 plus.o v_2 = \#$ ) )) @@ -940,7 +691,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ rule( name: [ unit expr value], - $vals, mu texpre () eqmu cdl 0_m, 0_r, 0_w cdr$, + $vals, mu texpre () eqmu 0$, ) )) @@ -1061,20 +812,37 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ === Call Values Spoil #let spoil = `spoil` -#let tryread = `try read` -#let tryspoil = `try spoil` +// TODO: FIXME: complete rule check #let tcorrectnew = $attach(tack.r.double, br: #[correct])$ #align(center, prooftree( vertical-spacing: 4pt, rule( name: [ correctness], - $m = (\_, Out) => c = Ref$, - $m = (\_, Out) => w = AlwaysWrite$, + $r = Read => v = 0$, $r = Read => m = (In, \_)$, + $m = (\_, Out) => w = AlwaysWrite$, + $(w = AlwaysWrite or w = MaybeWrite) and (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$, - $ tcorrectnew cl r, w, m, c cr $, + $v in {0, \#, bot}$, + + $ tcorrectnew cl v, r, w, r', w', m, c cr $, + ) +)) + +// TODO: extract correctness + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ spoil step], + + $ tcorrectnew cl v, r, w, r', w', m, c cr $, + + $w = AlwaysWrite or w = MaybeWrite$, + $v in {0, \#, bot}$, + $cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \, (\_, not Out) \, not Copy)_spoil cl bot, mu cr$, ) )) @@ -1083,103 +851,13 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ argument read], + name: [ fix step], - $cl v_m, v_r, v_w cr, - xarrowSquiggly(Read)_tryread - cl v_m modW readA, v_r modR readA, v_w modW readA cr$, - ) -)) + $ tcorrectnew cl v, r, w, r', w', m, c cr $, -#h(10pt) - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ argument not read], - - $cl v_m, v_r, v_w cr, - xarrowSquiggly(not Read)_tryread - cl v_m, v_r, v_w cr$, - ) -)) - -#h(10pt) - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ value maybe spoiled], - - $v_m, - xarrowSquiggly(not Out \, MaybeWrite)_tryspoil - ?$, - ) -)) - -#h(10pt) - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ value always spoiled], - - $v_m, - xarrowSquiggly(not Out \, AlwaysWrite)_tryspoil - bot$, - ) -)) - -#h(10pt) - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ value not spoiled], - - $v_m, - xarrowSquiggly(Out \, w)_tryspoil - v_m$, - ) -)) - -#h(10pt) - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ write spoil step], - - $ tcorrectnew cl r, w, m, c cr $, - $cl v_m, v_r, v_w cr, - xarrowSquiggly(r)_tryread - cl v_m', v_r', v_w' cr$, - - $v_m' modW writeA xarrowSquiggly(o \, AlwaysWrite)_tryspoil v_m''$, - - $cl cdl v_m, v_r, v_w cdr, mu cr - xarrowSquiggly(cl r \, AlwaysWrite cr \, (\_, o) \, Ref)_spoil - cl cdl v_m'', v_r' modR writeA, v_w' modW writeA cdr, cdr, mu cr$, - ) -)) - -#h(10pt) - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ maybe write step], - - $ tcorrectnew cl r, w, m, c cr $, - $cl v_m, v_r, v_w cr, - xarrowSquiggly(r)_tryread - cl v_m', v_r', v_w' cr$, - - $v_m' modW mbwriteA xarrowSquiggly(o \, MaybeWrite)_tryspoil v_m''$, - - $cl cdl v_m, v_r, v_w cdr, mu cr - xarrowSquiggly(cl r \, MaybeWrite cr \, (\_, o) \, Ref)_spoil - cl cdl v_m'', v_r' modR mbwriteA, v_w' modW mbwriteA cdr, mu cr$, + $w = AlwaysWrite$, + $v in {0, \#, bot}$, + $cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \, (\_, Out) \, c)_spoil cl 0, mu cr$, ) )) @@ -1190,16 +868,12 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ rule( name: [ skip step], - $ tcorrectnew cl r, w, m, c cr $, - $cl v_m, v_r, v_w cr, - xarrowSquiggly(r)_tryread - cl v_m', v_r', v_w' cr$, + $ tcorrectnew cl v, r, w, r', w', m, c cr $, - $c = Copy or w = NotWrite$, - - $cl cdl v_m, v_r, v_w cdr, mu cr - xarrowSquiggly(cl r \, w cr cr \, (\_, \_) \, c)_spoil - cl cdl v_m', v_r', v_w' cdr mu cr$, + $not "spoil step"$, + $not "fix step"$, + $v in {0, \#, bot}$, + $cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \, (\_, not Out) \, c)_spoil cl v, mu cr$, ) )) @@ -1271,7 +945,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ // FIXME depends on parent ?? $cl b, mu cr xarrowSquiggly(t \, t' \, m \, Copy)_spoil cl b', mu' cr$, $p arrrevpath^(\#.) pi$, - $cl mu'[l], mu' cr xarrowSquiggly(cl pi \, b' cr)_change cl v'', mu'' cr$, + $cl mu'[l], mu' cr xarrowSquiggly(cl pi \, b' cr)_modify cl v'', mu'' cr$, $mu stretch(=>)^(m space t space p)_(cl vals, types cr) mu''[l <- v'']$, ) @@ -1335,80 +1009,6 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ === Function Evaluation -#align(center, grid( - columns: 2, - gutter: 20%, - align: center, - - [ - $ x ~_r t$ - - #table( - columns: 2, - table.header( - [*x*], [*t*] - ), - $1$, $Read$, - $0$, $not Read$, - $top$, $not Read$, - ) - ], - - [ - $x ~_w t$ - #table( - columns: 2, - table.header( - [*x*], [*t*] - ), - $0$, $NotWrite$, - $?$, $MaybeWrite$, - $1$, $AlwaysWrite$, - ) - ] -)) - -#let ttags = $attach(tack.r, br: #[`tags`])$ - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ trivial type check], - - $v_r ~_r r$, - $v_w ~_w w$, - $mu ttags cdl v_m, v_r, v_w cdr : cl r, w cr$, - ) -)) -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ lambda check], - - $mu ttags lambda space overline(s) :$, - ) -)) -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ reference check], - - $mu ttags mu[l] : t$, - $mu ttags rf l : rf t$, - ) -)) -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ tuple check], - - $mu ttags v_1 : t_1$, - $...$, - $mu ttags v_n : t_n$, - $mu ttags [v_1, ... v_n] : [t_1, ... t_n]$, - ) -)) - #let tfunceval = $attach(tack.r.double, br: #[func eval])$ #align(center, prooftree( vertical-spacing: 4pt, @@ -1428,16 +1028,10 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ xarrowDashed(x_n space t_n space e_n)_vals cl types_n, vals_n, mu_n cr$, - // NOTE: eval function body $cl types_n, vals_n, mu_n cr xarrow(s) cl types', vals', mu' cr$, - // NOTE: check that read and write tags are used properly - $mu' ttags mu'[vals'[x_1]] : t_1$, - $...$, - $mu' ttags mu'[vals'[x_n]] : t_n$, - $vals, mu_0 tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$, ) )) @@ -1472,7 +1066,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ $...$, $vals, mu_0 tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] cr$, - // NOTE: "spoil" context for each argument usage + // NOTE: thick arrow to "spoil" context $mu_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) mu_1$, $...$, $mu_(n - 1) stretch(=>)^(m_n space t_n space e_n)_(cl vals, types cr) mu_n$, @@ -1495,7 +1089,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ $p arrpath x$, $l = vals[x]$, $p arrrevpath^(\#.) pi$, - $mu[l] xarrowSquiggly(cl pi \, writeA cr)_modify v'$, + $mu[l] xarrowSquiggly(cl pi \, 0 cr)_modify v'$, $cl types, vals, mu cr xarrow("WRITE" p) @@ -1508,25 +1102,18 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$ rule( name: [ READ $p$], - // TODO: already handled in modify ? - // $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$, - $mu[l] xarrowSquiggly(cl pi \, readA cr)_modify v'$, + $vals, mu tval p eqmu 0$, $cl types, vals, mu cr xarrow("READ" p) - cl types, vals, mu[l <- v'] cr$, + cl types, vals, mu cr$, ) )) #h(10pt) +#h(10pt) + #align(center, prooftree( vertical-spacing: 4pt, rule( diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index f4216ff..57b4207 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -164,44 +164,12 @@ struct (* NOTE: deepvalue - not used (?) *) - module MemVal = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - [%%ocanren_inject - type nonrec t = ZeroMV | SmthMV | BotMV - [@@deriving gt ~options:{ show; gmap }] - type ground = t - ] - end - - module ReadVal = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - [%%ocanren_inject - type nonrec t = ZeroRV | OneRV | TopRV - [@@deriving gt ~options:{ show; gmap }] - type ground = t - ] - end - - module WriteVal = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - [%%ocanren_inject - type nonrec t = ZeroWV | SmthWV | OneWV - [@@deriving gt ~options:{ show; gmap }] - type ground = t - ] - end - module Value = struct [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [%%ocanren_inject - type nonrec ('vm, 'vr, 'vw, 'sl, 'd, 'vl) t = UnitV of 'vm * 'vr * 'vw - | FunV of 'sl - | RefV of 'd - | TupleV of 'vl + type nonrec ('sl, 'd, 'vl) t = ZeroV | SmthV | BotV | FunV of 'sl | RefV of 'd | TupleV of 'vl [@@deriving gt ~options:{ show; gmap }] - type ground = (MemVal.ground, ReadVal.ground, WriteVal.ground, - ((* Nat.ground List.ground * *) Stmt.ground) List.ground, - Nat.ground, ground List.ground) t + type ground = (((* Nat.ground List.ground * *) Stmt.ground) List.ground, Nat.ground, ground List.ground) t ] end @@ -214,15 +182,6 @@ struct ] end - module Action = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - [%%ocanren_inject - type nonrec t = ReadA | AlwaysWriteA | MayWriteA - [@@deriving gt ~options:{ show; gmap }] - type ground = t - ] - end - (* --- *) module MemEnv = struct @@ -381,17 +340,6 @@ struct { xs == [] & ys == [] & zs == [] } } - (* NOTE: unrequired ? *) - (* let list_map2o f xs ys zs = ocanren { *) - (* { xs == [] & ys == [] } | *) - (* { fresh x', xs', y', ys', z', zs' in *) - (* xs == x' :: xs' & *) - (* ys == y' :: ys' & *) - (* f x' y' z' *) - (* mapo f xs' ys' zs' & *) - (* zs == z' :: zs' } *) - (* } *) - (* - state utils *) let types_assoco id types tp = @@ -511,8 +459,7 @@ struct let is_trivial_vo v = let open Value in ocanren { - fresh v_m, v_r, v_w in - v == UnitV (v_m, v_r, v_w) + v == ZeroV | v == SmthV | v == BotV } let rec pathvaro p x = @@ -569,11 +516,11 @@ struct pathvalo mem vals p' v' & v' == RefV id & mem_geto mem id v } | - { fresh p', id', v', vs in - p == AccessP (p', id') & + { fresh p', id, v', vs in + p == AccessP (p', id) & pathvalo mem vals p' v' & v' == TupleV vs & - list_ntho vs id' v } + list_ntho vs id v } } (* --- eval rules --- *) @@ -592,20 +539,13 @@ struct let open Type in let open Value in let open ReadCap in - (* let open CopyCap in *) - let open MemVal in - let open ReadVal in - let open WriteVal in + let open CopyCap in ocanren { { fresh r, w in is_trivial_vo v & tp == UnitT (r, w) & - { { fresh v_m, _v_r, _v_w in - r == Rd & - v == UnitV (v_m, _v_r, _v_w) & - mem_with_id' == Std.pair mem (UnitV (v_m, ZeroRV, ZeroWV)) } | - { r == NRd & - mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } | + { { r == Rd & mem_with_id' == Std.pair mem v } | + { r == NRd & mem_with_id' == Std.pair mem BotV } } } | { fresh stmts, ts in v == FunV stmts & tp == FunT ts & @@ -613,13 +553,13 @@ struct { fresh c, tp', id in v == RefV id & tp == RefT (c, tp') & - (* { c == Rf & mem_with_id' == Std.pair mem v } | *) - { fresh v', mem_cp, v_cp, mem_add, id_add in - (* c == Cp & *) - mem_geto mem id v' & - valcopyo mem v' tp' (Std.pair mem_cp v_cp) & - mem_addo mem_cp v_cp (Std.pair mem_add id_add) & - mem_with_id' == (mem_add, RefV id_add) } } | + { { c == Rf & mem_with_id' == Std.pair mem v } | + { fresh v', mem_cp, v_cp, mem_add, id_add in + c == Cp & + mem_geto mem id v' & + valcopyo mem v' tp' (Std.pair mem_cp v_cp) & + mem_addo mem_cp v_cp (Std.pair mem_add id_add) & + mem_with_id' == (mem_add, RefV id_add) } } } | { fresh vs, tps, mem', vs' in v == TupleV vs & tp == TupleT tps & @@ -627,43 +567,10 @@ struct mem_with_id' == Std.pair mem' (TupleV vs') } } - (* - action rules *) - - let memvmodo a v_m v_m' = - let open MemVal in - let open Action in - ocanren { - { a == ReadA & v_m == ZeroMV & v_m' == ZeroMV } | - { a == AlwaysWriteA & v_m' == ZeroMV } | - { a == MayWriteA & v_m == ZeroMV & v_m' == ZeroMV } | - { a == MayWriteA & v_m =/= ZeroMV & v_m' == SmthMV } - } - - let readvmodo a v_r v_r' = - let open ReadVal in - let open Action in - ocanren { - { v_r == TopRV & v_r' == TopRV } | - { v_r == OneRV & v_r' == OneRV } | - { a == ReadA & v_r == ZeroRV & v_r' == OneRV } | - { a == AlwaysWriteA & v_r == ZeroRV & v_r' == TopRV } | - { a == MayWriteA & v_r == ZeroRV & v_r' == ZeroRV } - } - - let writevmodo a v_w v_w' = - let open WriteVal in - let open Action in - ocanren { - { a == ReadA & v_w' == v_w } | - { a == AlwaysWriteA & v_w' == OneWV } | - { a == MayWriteA & v_w == OneWV & v_w' == OneWV } | - { a == MayWriteA & v_w =/= OneWV & v_w' == v_w } - } - (* - value update *) (* NOTE: reversed path used *) - let rec valchangeo mem v rp b mem_with_v' = + let rec valupdo mem v rp b mem_with_v' = let open RevPath in let open Value in ocanren { @@ -673,7 +580,7 @@ struct rp == DerefRP rp' & v == RefV id & mem_geto mem id v' & - valchangeo mem v' rp' b mem_with_v_upd & + valupdo mem v' rp' b 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) } | @@ -681,40 +588,7 @@ struct rp == AccessRP (rp', id) & v == TupleV vs' & list_ntho vs' id v' & - valchangeo mem v' rp' b mem_with_v_upd & - Std.pair mem_upd v_upd == mem_with_v_upd & - list_replaceo vs' id v_upd vs_upd & - mem_with_v' == Std.pair mem_upd (TupleV vs_upd) } - } - - (* NOTE: reversed path used *) - let rec valupdo mem v rp a mem_with_v' = - let open RevPath in - let open Value in - ocanren { - { fresh v_m, v_r, v_w, - v_m', v_r', v_w', - v' in - rp == VarRP & - v == UnitV (v_m, v_r, v_w) & - memvmodo a v_m v_m' & - readvmodo a v_r v_r' & - writevmodo a v_w v_w' & - 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' & - 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 - rp == AccessRP (rp', id) & - v == TupleV vs' & - list_ntho vs' id v' & - valupdo mem v' rp' a mem_with_v_upd & + valupdo mem v' rp' b mem_with_v_upd & Std.pair mem_upd v_upd == mem_with_v_upd & list_replaceo vs' id v_upd vs_upd & mem_with_v' == Std.pair mem_upd (TupleV vs_upd) } @@ -722,50 +596,13 @@ struct (* - value combination *) - let memvalcombo u v u' = - let open MemVal in - ocanren { - { u == ZeroMV & v == ZeroMV & u' == ZeroMV } | - { u == BotMV & v == BotMV & u' == BotMV } | - { { u =/= ZeroMV | { u == ZeroMV & v =/= ZeroMV } } & - { u =/= BotMV | { u == BotMV & v =/= BotMV } } & - u' == SmthMV } - } - - let readvalcombo u v u' = - let open ReadVal in - ocanren { - { u == TopRV & v == TopRV & u' == TopRV } | - { u == ZeroRV & v == ZeroRV & u' == ZeroRV } | - { u == TopRV & v == ZeroRV & u' == ZeroRV } | - { u == ZeroRV & v == TopRV & u' == ZeroRV } | - { u =/= TopRV & v =/= TopRV & - u =/= ZeroRV & v =/= ZeroRV & - u' == OneRV } - } - - let writevalcombo u v u' = - let open WriteVal in - ocanren { - { u == OneWV & v == OneWV & u' == OneWV } | - { u == ZeroWV & v == ZeroWV & u' == ZeroWV } | - { { u =/= ZeroWV | { u == ZeroWV & v =/= ZeroWV } } & - { u =/= OneWV | { u == OneWV & v =/= OneWV } } & - u' == SmthWV } - } - let rec valcombo u v u' = let open Value in ocanren { - { fresh u_m, u_r, u_w, - v_m, v_r, v_w, - u_m', u_r', u_w' in - u == UnitV (u_m, u_r, u_w) & - v == UnitV (v_m, v_r, v_w) & - memvalcombo u_m v_m u_m' & - readvalcombo u_r v_r u_r' & - writevalcombo u_w v_w u_w' & - u' == UnitV (u_m', u_r', u_w') } | + { is_trivial_vo u & + is_trivial_vo v & + (* TODO: do not use disequality constraint ? *) + { { u == v & u' == u } | { u =/= v & u' == BotV } } } | { fresh ustmts, vstmts, ustmts' in u == FunV ustmts & v == FunV vstmts & @@ -775,8 +612,7 @@ struct { fresh a, b in u == RefV a & v == RefV b & - a == b & - u' == RefV a } | + a == b } | { fresh us, vs, us' in u == TupleV us & v == TupleV vs & @@ -806,11 +642,8 @@ struct exprvalo mem vals e v' = let open Expr in let open Value in - let open MemVal in - let open ReadVal in - let open WriteVal in ocanren { - { e == UnitE & v' == UnitV (ZeroMV, ZeroRV, ZeroWV) } | + { e == UnitE & v' == ZeroV } | { fresh p in e == PathE p & pathvalo mem vals p v' } | @@ -865,6 +698,7 @@ struct types', vals' in d == VarD (tp, e) & exprvalo mem vals e v & + (* v == TupleV [ZeroV; ZeroV] & (* FIXME TMP *) *) valcopyo mem v tp (Pair.pair mem_cp v_cp) & (* mem_cp == mem & v_cp == v & *) mem_addo mem_cp v_cp (Pair.pair mem_add id_add) & @@ -926,100 +760,76 @@ struct (* - call values spoil *) (* TODO: check that negation is interpreted correctly *) - let is_correct_tagso r w m c = + let is_correct_tagso v r w _r' w' m c = + let open Value in let open ReadCap in let open WriteCap in 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 & c == Rf } + { is_not_outo m | is_outo m & w == AlwaysWr } & + { w == NeverWr | + w =/= NeverWr & w' =/= AlwaysWr & is_not_outo m & c == Cp | + w =/= NeverWr & w' == AlwaysWr } & + is_trivial_vo v } - let tryreado r v_m v_r v_w v' = - let open Action in - let open Value in - let open ReadCap in - ocanren { - { fresh v_m', v_r', v_w' in - r == Rd & - memvmodo ReadA v_m v_m' & - readvmodo ReadA v_r v_r' & - writevmodo ReadA v_w v_w' & - v' == UnitV (v_m', v_r', v_w') } | - { r == NRd & - v' == UnitV (v_m, v_r, v_w)} - } - - let tryspoilo m w v_m v_m' = - let open Mode in - let open WriteCap in - let open MemVal in - ocanren { - { is_outo m & { w == AlwaysWr | w == MayWr } & v_m' == v_m } | - { is_not_outo m & w == AlwaysWr & v_m' == BotMV } | - { is_not_outo m & w == MayWr & v_m' == SmthMV } - } - - let rec valspoil_foldero m c mem_with_vs tp v mem_with_vs' = ocanren { + let rec valspoil_foldero m c mem_with_vs tp u v mem_with_vs' = ocanren { fresh mem, vs, mem', v' in Std.pair mem vs == mem_with_vs & - valspoilo mem v tp m c (Std.pair mem' v') & + valspoilo mem v tp u m c (Std.pair mem' v') & mem_with_vs' == Std.pair mem' (v' :: vs) } - and valspoilo mem v tp m c mem_with_v' = + and valspoilo mem v tp u m c mem_with_v' = let open Type in let open Value in + let open Mode in let open WriteCap in let open CopyCap in - let open Action in ocanren { - { fresh r, w, - v_m, v_r, v_w, - v', v'' in + { fresh r, w, r', w' in tp == UnitT (r, w) & - v == UnitV (v_m, v_r, v_w) & - is_correct_tagso r w m c & - tryreado r v_m v_r v_w v' & + u == UnitT (r', w') & + is_trivial_vo v & + is_correct_tagso v r w r' w' m c & { - { { c == Cp | { c == Rf & w == NeverWr } } & - mem_with_v' == Std.pair mem v' } | - { fresh v_m', v_r', v_w', - v_m'', v_r'', v_w'', - v_m''' in + { is_not_outo m & c == Rf & { w == AlwaysWr | w == MayWr } & - v' == UnitV (v_m', v_r', v_w') & - { - { w == AlwaysWr & - memvmodo AlwaysWriteA v_m' v_m'' & - readvmodo AlwaysWriteA v_r' v_r'' & - writevmodo AlwaysWriteA v_w' v_w'' } | - { w == MayWr & - memvmodo MayWriteA v_m' v_m'' & - readvmodo MayWriteA v_r' v_r'' & - writevmodo MayWriteA v_w' v_w'' } - } & - tryspoilo m w v_m'' v_m''' & - v'' == UnitV (v_m''', v_r'', v_w'') & - mem_with_v' == Std.pair mem v'' } + mem_with_v' == Std.pair mem BotV } | + { 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 } & + mem_with_v' == Std.pair mem v } } } | - { fresh ts, _stmts in + { fresh ts, us, _stmts in tp == FunT ts & + u == FunT us & v == FunV _stmts & + ts == us & mem_with_v' == Std.pair mem v } | - { fresh ctp', tp', id', v', mem_sp, v_sp, mem_set in + { fresh ctp', tp', cu', u', id', v', mem_sp, v_sp, mem_set in tp == RefT (ctp', tp') & + u == RefT (cu', u') & v == RefV id' & mem_geto mem id' v' & - valspoilo mem v' tp' m ctp' (Std.pair mem_sp v_sp) & + valspoilo mem v' tp' u' m ctp' (Std.pair mem_sp v_sp) & mem_seto mem_sp id' v_sp mem_set & mem_with_v' == Std.pair mem_set (RefV id') } | - { fresh tps, vs, mem_sp, vs_sp in + { fresh tps, us, vs, mem_sp, vs_sp in tp == TupleT tps & + u == TupleT us & v == TupleV vs & - list_foldr2o (valspoil_foldero m c) - (Std.pair mem []) tps vs + list_foldr3o (valspoil_foldero m c) + (Std.pair mem []) tps us vs (Std.pair mem_sp vs_sp) & mem_with_v' == Std.pair mem_sp (TupleV vs_sp) } @@ -1027,34 +837,34 @@ struct (* full spoil *) - let argsspoilpo st m tp p mem' = + let argspoilpo st m tp p mem' = let open StEnv in let open CopyCap in let open RevPath in ocanren { fresh mem, types, vals, visited, - x, id, b(* , tp' *), rp, + x, id, b, tp', rp, mem_sp, b_sp, v_sp, mem_upd, v_upd in st == StEnv (mem, types, vals, visited) & pathvaro p x & vals_assoco x vals id & pathvalo mem vals p b & - (* pathtypeo types p tp' & *) - valspoilo mem b tp m Cp (Std.pair mem_sp b_sp) & - pathrevo p VarRP rp & + pathtypeo types p tp' & + valspoilo mem b tp tp' m Cp (Std.pair mem_sp b_sp) & mem_geto mem_sp id v_sp & - valchangeo mem_sp v_sp rp b_sp (Std.pair mem_upd v_upd) & + pathrevo p VarRP rp & + valupdo mem_sp v_sp rp b_sp (Std.pair mem_upd v_upd) & mem_seto mem_upd id v_upd mem' } - let rec argsspoile_foldero types vals visited m mem tp e mem' = + let rec argspoile_foldero types vals visited m mem tp e mem' = let open StEnv in ocanren { fresh st in st == StEnv (mem, types, vals, visited) & - argsspoileo st m tp e mem' + argspoileo st m tp e mem' } - and argsspoileo st m tp e mem' = + and argspoileo st m tp e mem' = let open StEnv in let open Expr in let open Type in @@ -1068,14 +878,14 @@ struct mem' == mem } | { fresh p in e == PathE p & - argsspoilpo st m tp p mem' } | + argspoilpo st m tp p mem' } | { fresh x in e == RefE x & - argsspoilpo st m tp (VarP x) mem' } | + argspoilpo st m tp (VarP x) mem' } | { fresh es, tps in e == TupleE es & tp == TupleT tps & - list_foldl2o (argsspoile_foldero types vals visited m) mem tps es mem'} + list_foldl2o (argspoile_foldero types vals visited m) mem tps es mem'} } } @@ -1100,47 +910,8 @@ struct (* - function evaluation *) (* NOTE: not needed due to performed optimization in stmt_eval ? *) - let writeval_to_capo v_w w' = - let open WriteVal in - let open WriteCap in - ocanren { - { v_w == ZeroWV & w' == NeverWr } | - { v_w == SmthWV & w' == MayWr } | - { v_w == OneWV & w' == AlwaysWr } - } - - let rec tags_checko mem v tp = - let open ReadVal in - let open ReadCap in - let open Type in - let open Value in - ocanren { - { fresh v_m, v_r, v_w, - r, w in - v == UnitV (v_m, v_r, v_w) & - tp == UnitT (r, w) & - { - { r == Rd & v_r == OneRV } | - { r == NRd & v_r == ZeroRV } | - { r == NRd & v_r == TopRV } - } & - writeval_to_capo v_w w - } | - { fresh _stmts, _ts in - v == FunV _stmts & - tp == FunT _ts } | - { fresh id, _c, tp', v' in - v == RefV id & - tp == RefT (_c, tp') & - mem_geto mem id v' & - tags_checko mem v' tp' } | - { fresh vs, tps in - v == TupleV vs & - tp == TupleT tps & - List.mapo (tags_checko mem) vs tps } - } - (* - statement evaluation *) + (* TODO *) let rec stmt_addarg_foldero vals st_with_id mtp e st_with_id' = ocanren { fresh st, x, m, tp, st' in @@ -1149,28 +920,16 @@ struct addargo st vals x tp e st' & st_with_id' == Std.pair st' (Nat.s x) } - and f_tags_check_foldero mem vals x mtp x' = ocanren { - fresh m, tp, id', v' in - mtp == Std.pair m tp & - vals_assoco x vals id' & - mem_geto mem id' v' & - tags_checko mem v' tp & - x' == Nat.s x - } - and stmt_eval_func_foldero mem types vals tps visited stmt visited' = + and stmt_eval_func_foldero mem types vals visited stmt visited' = let open StEnv in ocanren { { fresh visited_add, st, - st', mem', types', vals', - _x', visited'' in + st', mem', types', vals' in not_visited_checko visited stmt & visited_addo visited stmt visited_add & st == StEnv (mem, types, vals, visited_add) & stmt_evalo st stmt st' & - st' == StEnv (mem', types', vals', visited'') & - list_foldlo (f_tags_check_foldero mem' vals') 0 tps _x' & - visited' == visited'' - } | + st' == StEnv (mem', types', vals', visited') } | { visited_checko visited stmt & visited == visited' } } @@ -1180,7 +939,7 @@ struct fresh m, tp, st in Std.pair m tp == mtp & st == StEnv (mem, types, vals, visited) & - argsspoileo st m tp e mem' + argspoileo st m tp e mem' } and stmt_evalo st s st' = let open StEnv in @@ -1191,7 +950,6 @@ struct let open TypesEnv in let open ValsEnv in let open RevPath in - let open Action in ocanren { fresh mem, types, vals, visited in st == StEnv (mem, types, vals, visited) & @@ -1221,7 +979,7 @@ struct (Std.pair st_call 0) tps es (Std.pair state_with_args _arg_id) & state_with_args == StEnv (mem_swa, types_swa, vals_swa, visited_swa) & - list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa tps) visited_swa fstmts visited' & + list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa) visited_swa fstmts visited' & (* TODO: FIXME check left or right order *) list_foldl2o (stmt_eval_spoil_foldero types vals (* NOTE: not important*) visited') mem tps es mem_spoiled & @@ -1237,25 +995,13 @@ struct vals_assoco x vals id & mem_geto mem id v & pathrevo p VarRP rp & - valupdo mem v rp AlwaysWriteA (Std.pair mem_upd v_upd) & + valupdo mem v rp ZeroV (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, - mem_upd, v_upd, mem_set in + { fresh p 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 & - pathrevo p VarRP rp & - valupdo mem v rp ReadA (Std.pair mem_upd v_upd) & - mem_seto mem_upd id v_upd mem_set & - st' == StEnv (mem_set, types, vals, visited) } | - (* { fresh p in *) - (* s == ReadS p & *) - (* pathvalo mem vals p ZeroV & *) - (* st == st' } | *) + pathvalo mem vals p ZeroV & + st == st' } | { fresh sl, sr, stl in s == SeqS (sl, sr) & stmt_evalo st sl stl & diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml index 3c73dcb..db667a7 100644 --- a/model_with_structures/tests.ml +++ b/model_with_structures/tests.ml @@ -7,103 +7,84 @@ open Relational let%expect_test "prog eval test: empty" = print_endline (prog_eval_t_empty ()); [%expect {| [StEnv (MemEnv ([], O), TypesEnv ([], []), ValsEnv ([], []), VisitedEnv ([]))] |}] let%expect_test "prog eval test: simple var" = print_endline(prog_eval_t_simple_var ()); - [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, OneRV, ZeroWV)], 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)]), VisitedEnv ([]))] |}] + [%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)]), VisitedEnv ([]))] |}] 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 ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (BotMV, ZeroRV, ZeroWV)], 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)]), VisitedEnv ([]))] |}] + [%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)]), VisitedEnv ([]))] |}] let%expect_test "simple var, write" = print_endline(prog_eval_t_simple_var_wr ()); - [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, TopRV, OneWV)], 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)]), VisitedEnv ([]))] |}] + [%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)]), VisitedEnv ([]))] |}] 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 ([UnitV (ZeroMV, TopRV, OneWV)], 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)]), VisitedEnv ([]))] |}] + [%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)]), VisitedEnv ([]))] |}] (* - 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))]); 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))]))] |}] + [%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)]), 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 (O); ZeroV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (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)))]))] |}] 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 (O); ZeroV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, MayWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, 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 (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)))]))] |}] 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 (O); BotV], 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))))]))] |}] 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 (O); BotV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), 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 (O); ZeroV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), 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 (O); ZeroV], 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 (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (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))))]))] |}] 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 (O); ZeroV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), 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 (O); ZeroV], 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)))]))] |}] 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 (O); ZeroV], S (S (S (O)))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), 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 (O))); BotV; RefV (O); ZeroV], 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)))))]))] |}] 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))))), WriteS (DerefP (VarP (S (S (S (O))))))))))]); RefV (S (S (S (S (S (S (O))))))); ZeroV; RefV (S (S (S (S (O))))); ZeroV; RefV (S (S (O))); ZeroV; RefV (O); ZeroV], S (S (S (S (S (S (S (S (S (O)))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Cp, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Cp, 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, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); (Mode (NIn, Out), RefT (Cp, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Cp, 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))))), WriteS (DerefP (VarP (S (S (S (O))))))))))]))] |}] 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))))), WriteS (DerefP (VarP (S (S (S (O)))))))))]); RefV (S (S (S (S (S (S (O))))))); ZeroV; RefV (S (S (S (S (O))))); ZeroV; RefV (S (S (O))); ZeroV; RefV (O); ZeroV], S (S (S (S (S (S (S (S (S (O)))))))))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (NIn, NOut), RefT (Rf, UnitT (NRd, NeverWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), UnitT (Rd, AlwaysWr)); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), RefT (Rf, UnitT (Rd, AlwaysWr))); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, AlwaysWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), S (S (S (S (S (S (S (S (O))))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), S (S (S (S (S (S (S (O)))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), S (S (S (S (S (S (O))))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))), S (S (S (S (S (O)))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))), S (S (S (S (O))))); (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))), S (S (S (O)))); (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))), S (S (O))); (S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([SeqS (ReadS (DerefP (VarP (S (O)))), SeqS (ReadS (DerefP (VarP (S (S (S (O)))))), SeqS (WriteS (DerefP (VarP (S (S (O))))), WriteS (DerefP (VarP (S (S (S (O)))))))))]))] |}] (* - basic synthesis tests *) let%expect_test "simple synthesis test" = print_endline(prog_cp_cap_synt_t_simple_call_ref_wr ()); - [%expect {| [Cp; Rf] |}] + [%expect {| [Rf; Cp] |}] let%expect_test "simple synthesis test, no read write caps constraints" = print_endline(prog_cp_cap_synt_t_simple_call_ref_wr' ()); - [%expect {| [Cp; Rf] |}] + [%expect {| [Rf; Rf; Rf; Rf; Cp; Cp; Cp; Cp] |}] let%expect_test "simple synthesis test, reference forbidden write" = print_endline(prog_cp_cap_synt_t_simple_call_ref_fbd_wr ()); [%expect {| [Cp] |}] let%expect_test "simple synthesis test, reference forbidden write, no read write caps constraints" = print_endline(prog_cp_cap_synt_t_simple_call_ref_fbd_wr' ()); - [%expect {| [Cp] |}] - -(* - presentation tests *) - -let%expect_test "presentation test 1 (simple types), eval" = print_endline(prog_eval_t_presentation_simple_tp ()); - [%expect {| [StEnv (MemEnv ([FunV ([ReadS (DerefP (VarP (O)))]); FunV ([SeqS (WriteS (DerefP (VarP (O))), SeqS (ChoiceS (WriteS (DerefP (VarP (S (O)))), WriteS (DerefP (VarP (O)))), SeqS (ReadS (DerefP (VarP (O))), SeqS (ReadS (DerefP (VarP (S (O)))), SkipS))))]); FunV ([ChoiceS (WriteS (DerefP (VarP (O))), SkipS)]); FunV ([SeqS (ReadS (DerefP (VarP (O))), SeqS (WriteS (DerefP (VarP (O))), SeqS (ReadS (DerefP (VarP (S (O)))), SkipS)))]); RefV (S (S (S (S (S (S (S (S (S (S (O))))))))))); UnitV (ZeroMV, OneRV, ZeroWV); 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 (BotMV, OneRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV); RefV (S (O)); UnitV (BotMV, OneRV, OneWV); UnitV (ZeroMV, ZeroRV, ZeroWV)], S (S (S (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 (S (S (S (O))))))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))])); (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 (S (S (S (O))))))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, MayWr)))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))])); (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 (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 (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 (O))))))))))))))); (S (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 (S (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)], [(S (S (S (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 (S (S (S (O)))))))))))))))); (S (S (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 (S (S (O))))))))))))))); (S (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 (S (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 (WriteS (DerefP (VarP (O))), SeqS (ChoiceS (WriteS (DerefP (VarP (S (O)))), WriteS (DerefP (VarP (O)))), SeqS (ReadS (DerefP (VarP (O))), SeqS (ReadS (DerefP (VarP (S (O)))), SkipS)))); SeqS (ReadS (DerefP (VarP (O))), SeqS (WriteS (DerefP (VarP (O))), SeqS (ReadS (DerefP (VarP (S (O)))), SkipS))); ReadS (DerefP (VarP (O))); ChoiceS (WriteS (DerefP (VarP (O))), SkipS); ChoiceS (WriteS (DerefP (VarP (O))), SkipS); SeqS (WriteS (DerefP (VarP (O))), SeqS (ChoiceS (WriteS (DerefP (VarP (S (O)))), WriteS (DerefP (VarP (O)))), SeqS (ReadS (DerefP (VarP (O))), SeqS (ReadS (DerefP (VarP (S (O)))), SkipS)))); SeqS (ReadS (DerefP (VarP (O))), SeqS (WriteS (DerefP (VarP (O))), SeqS (ReadS (DerefP (VarP (S (O)))), SkipS))); ReadS (DerefP (VarP (O))); ChoiceS (WriteS (DerefP (VarP (O))), SkipS); ChoiceS (WriteS (DerefP (VarP (O))), SkipS)]))] |}] - -let%expect_test "presentation test 1 (simple types), synt" = print_endline(prog_synt_t_presentation_simple_tp ()); - [%expect {| [[Cp; Cp; Cp; Cp; Cp; Cp]; [Cp; Cp; Cp; Cp; Cp; Rf]; [Cp; Cp; Cp; Rf; Cp; Cp]; [Cp; Cp; Cp; Rf; Cp; Rf]; [Cp; Rf; Cp; Cp; Cp; Cp]; [Cp; Rf; Cp; Cp; Cp; Rf]; [Cp; Rf; Cp; Rf; Cp; Cp]; [Cp; Rf; Cp; Rf; Cp; Rf]; [Rf; Cp; Cp; Cp; Cp; Cp]; [Rf; Rf; Cp; Cp; Cp; Cp]; [Rf; Cp; Cp; Cp; Cp; Rf]; [Rf; Rf; Cp; Cp; Cp; Rf]; [Rf; Cp; Cp; Rf; Cp; Cp]; [Rf; Rf; Cp; Rf; Cp; Cp]; [Rf; Cp; Cp; Rf; Cp; Rf]; [Rf; Rf; Cp; Rf; Cp; Rf]] |}] - -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 ()); - [%expect {| [[Cp; Cp; Cp]; [Cp; Cp; Rf]; [Cp; Rf; Cp]; [Cp; Rf; Rf]] |}] + [%expect {| [Cp; Cp; Cp; Cp] |}] (* - complex test: send example *) -(* TODO: correct tags (at least rw) *) -(* let%expect_test "complex test: send" = print_endline(prog_eval_compl_test_send ()); *) - (* [%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)))))))))]); FunV ([SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O))))))))]); FunV ([SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O)))))]); FunV ([ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS)]); TupleV ([RefV (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))); RefV (S (S (S (S (S (S (S (S (S (S (O))))))))))); RefV (S (S (S (S (S (S (S (S (S (O)))))))))); RefV (S (S (S (S (S (S (S (S (O))))))))); ZeroV]); TupleV ([RefV (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))); RefV (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))]); TupleV ([ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV]); ZeroV; ZeroV; TupleV ([ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([RefV (S (S (S (O)))); RefV (S (S (O)))]); TupleV ([ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV])], S (S (S (S (S (S (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 (S (S (O)))))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)])); (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 (O)))))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (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 (O)))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); (S (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 (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)])); (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 (O)))))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (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 (O)))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); (S (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 (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))]), ValsEnv ([(S (S (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 (S (S (S (S (S (S (O))))))))))))))))))); (S (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 (S (S (S (S (S (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 (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 (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 (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 (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 (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 (S (S (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 (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 (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 (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 (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 (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 (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 (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 (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)))))))))]))] |}] *) +let%expect_test "complex test: send" = print_endline(prog_eval_compl_test_send ()); + [%expect {| [StEnv (MemEnv ([FunV ([SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)))))))))]); FunV ([SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O))))))))]); FunV ([SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O)))))]); FunV ([ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS)]); TupleV ([RefV (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))); RefV (S (S (S (S (S (S (S (S (S (S (O))))))))))); RefV (S (S (S (S (S (S (S (S (S (O)))))))))); RefV (S (S (S (S (S (S (S (S (O))))))))); ZeroV]); TupleV ([RefV (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))); RefV (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))]); TupleV ([ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV]); ZeroV; ZeroV; TupleV ([ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([RefV (S (S (S (O)))); RefV (S (S (O)))]); TupleV ([ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV; ZeroV]); TupleV ([ZeroV; ZeroV])], S (S (S (S (S (S (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 (S (S (O)))))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)])); (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 (O)))))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (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 (O)))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); (S (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 (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))], [(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))), FunT ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)]))])); (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); 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)); UnitT (Rd, AlwaysWr)])); (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 (O)))))))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); (S (S (S (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 (O)))))))))))), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); (S (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 (O)))))))))), TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))]), ValsEnv ([(S (S (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 (S (S (S (S (S (S (O))))))))))))))))))); (S (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 (S (S (S (S (S (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 (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 (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 (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 (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 (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 (S (S (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 (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 (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 (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 (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 (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 (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 (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 (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SkipS); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O))))))))); SeqS (ChoiceS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (S (O)))), O)), SeqS (ReadS (DerefP (AccessP (VarP (O), S (S (S (O)))))), SeqS (WriteS (DerefP (AccessP (VarP (O), S (S (S (O)))))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), S (O))), O))))), SkipS), SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), ReadS (AccessP (VarP (O), S (S (S (S (O)))))))); SeqS (WriteS (AccessP (VarP (O), S (S (S (S (O)))))), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O)))))))))))))))))), [PathE (VarP (O))]), SeqS (CallS (VarP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (O))))))))))))))))))), [PathE (VarP (O))]), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)), SeqS (WriteS (AccessP (DerefP (AccessP (VarP (O), S (O))), S (O))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (O), O)), O)), O)), ReadS (AccessP (DerefP (AccessP (VarP (O), S (O))), O)))))))))]))] |}] -(* TODO: slow *) -(* let%expect_test "complex test: send" = print_endline(prog_synt_compl_test_send ()); *) - (* [%expect {| [[Rf; Cp; Cp; Cp; Cp; Cp]; [Cp; Cp; Cp; Cp; Cp; Cp]] |}] *) - -(* let%expect_test "complex test: send" = print_endline(prog_synt_compl_test_send ()); *) - (* [%expect {| [[Rf; Cp; Cp; Cp; Cp; Cp]; [Cp; Cp; Cp; Cp; Cp; Cp]] |}] (* TODO: FIXME *) *) +let%expect_test "complex test: send" = print_endline(prog_synt_compl_test_send ()); + [%expect {| [Cp] |}] (* TODO *) diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index 4690159..adfad04 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -16,7 +16,6 @@ open WriteCap open InCap open OutCap open Mode -open StEnv @type answer = StEnv.ground GT.list with show @@ -27,31 +26,19 @@ open StEnv (* - shortcuts *) +(* TODO *) + (* NOTE: redo with fold ?? *) -let seq_foldero stmt_acc stmt stmt_acc' = ocanren { - stmt_acc' == SeqS(stmt, stmt_acc) - } -let seqo stmts stmt' = ocanren { - list_foldro seq_foldero SkipS stmts stmt' - } -(* ocanren { *) - (* { stmts == [] & stmt' == SkipS } | *) - (* { fresh s in *) - (* stmts == [s] & *) - (* stmt' == s } | *) - (* { fresh s, s', ss, stmt_rest' in *) - (* stmts == s :: s' :: ss & *) - (* seqo (s' :: ss) stmt_rest' & *) - (* stmt' == SeqS(s, stmt_rest') *) - (* } *) - (* } *) - -let deref_accesso id v p' = ocanren { - p' == DerefP (AccessP (VarP v, id)) - } - -let access_deref_accesso id_ext id_int v p' = ocanren { - p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext) +let rec seqo stmts stmt' = ocanren { + { stmts == [] & stmt' == SkipS } | + { fresh s in + stmts == [s] & + stmt' == s } | + { fresh s, s', ss, stmt_rest' in + stmts == s :: s' :: ss & + seqo (s' :: ss) stmt_rest' & + stmt' == SeqS(s, stmt_rest') + } } (* - basic var tests *) @@ -133,18 +120,6 @@ let prog_eval_t_simple_var_wr_rd _ = show(answer) (Stream.take (run q (* - basic call tests *) -(* NOTE: should add ? *) -(* let prog_eval_t_simple_call_noarg _ = show(answer) (Stream.take (run q *) - (* (fun q -> ocanren { *) - (* fresh prog, xg, fg, xd, fd in *) - (* globals_min_ido xg & *) - (* fg == Nat.s xg & *) - (* xd == VarD (UnitT (Rd, NeverWr), UnitE) & *) - (* fd == FunD ([], SkipS) & *) - (* prog == Prg ([xd; fd], CallS (VarP fg, [])) & *) - (* prog_evalo prog q }) *) - (* (fun q -> q#reify (StEnv.prj_exn)))) *) - let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q (fun q -> ocanren { fresh prog, xg, fg, xd, fd in @@ -162,9 +137,9 @@ let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (Rd, NeverWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, NeverWr)), RefE xg) & - fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))], + xd == VarD (UnitT (Rd, MayWr), UnitE) & + yd == VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE xg) & + fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))], ReadS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & prog_evalo prog q }) @@ -176,9 +151,9 @@ let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (NRd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) & - fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], + xd == VarD (UnitT (Rd, MayWr), UnitE) & + yd == VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE xg) & + fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))], WriteS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & prog_evalo prog q }) @@ -219,9 +194,9 @@ let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (NRd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) & - fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], + xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & + fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & prog_evalo prog q }) @@ -248,9 +223,9 @@ let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q globals_min_ido xg & yg == Nat.s xg & fg == Nat.s yg & - xd == VarD (UnitT (NRd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) & - fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], + xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & + yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & + fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), SeqS (WriteS (DerefP (VarP yg)), @@ -267,9 +242,9 @@ let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q f2g == Nat.s fg & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & - fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], + fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & - f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], + f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))], SeqS (CallS (VarP fg, [PathE (VarP 0)]), WriteS (DerefP (VarP 0)))) & prog == Prg ([xd; yd; fd; f2d], SeqS (CallS (VarP f2g, [PathE (VarP yg)]), @@ -285,7 +260,7 @@ let prog_eval_t_call_in_call_rec _ = show(answer) (Stream.take (run q fg == Nat.s yg & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & - fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], + fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))], SeqS (CallS (VarP fg, [PathE (VarP 0)]), WriteS (DerefP (VarP 0)))) & prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), @@ -320,7 +295,7 @@ let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q fg == Nat.s yg & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & - fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))], + fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))], SeqS (WriteS (VarP xg), ReadS (DerefP (VarP 0)))) & prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), @@ -388,10 +363,10 @@ let prog_eval_t_call_with_dif_mods_cp _ = show(answer) (Stream.take (run q WriteS (DerefP (VarP 1)); WriteS (DerefP (VarP 2)); WriteS (DerefP (VarP 3))] fstmts & - fd == FunD ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, NeverWr))); + fd == FunD ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr))); - (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr))); - (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))], + (Mode (NIn, Out), RefT (Cp, UnitT (NRd, AlwaysWr))); + (Mode (In, Out), RefT (Cp, UnitT (Rd, AlwaysWr)))], fstmts) & seqo [CallS (VarP fg, [PathE (VarP yg); PathE (VarP y2g); @@ -479,7 +454,7 @@ let prog_cp_cap_synt_t_simple_call_ref_wr _ = show(answerCpCap) (Stream.take (ru fg == Nat.s yg & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & - fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (NRd, AlwaysWr)))], + fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (Rd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & prog_evalo prog st }) @@ -508,7 +483,7 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr _ = show(answerCpCap) (Stream.take fg == Nat.s yg & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) & - fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (NRd, AlwaysWr)))], + fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (Rd, AlwaysWr)))], WriteS (DerefP (VarP 0))) & prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), ReadS (DerefP (VarP yg)))) & @@ -531,158 +506,7 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak prog_evalo prog st }) (fun q -> q#reify (CopyCap.prj_exn)))) -(* - presentation tests *) - -(* simple types *) - -let prog_eval_t_presentation_simple_tp _ = show(answer) (Stream.take (run q - (fun q -> ocanren { - fresh prog, xbg, xg, - ybg, yg, - zbg, zg, - kbg, kg, - fg, wg, gg, rg, - xbd, xd, - ybd, yd, - zbd, zd, - kbd, kd, - fd, wd, gd, rd, - fstmts, gstmts, - stmts in - globals_min_ido xbg & - xg == Nat.s xbg & - ybg == Nat.s xg & - yg == Nat.s ybg & - zbg == Nat.s yg & - zg == Nat.s zbg & - kbg == Nat.s zg & - kg == Nat.s kbg & - fg == Nat.s kg & - wg == Nat.s fg & - gg == Nat.s wg & - rg == Nat.s gg & - xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) & - ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) & - zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) & - kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) & - seqo [ReadS (DerefP (VarP 0)); - WriteS (DerefP (VarP 0)); - ReadS (DerefP (VarP 1))] fstmts & - fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr))); - (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))], - fstmts) & - wd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, MayWr)))], - ChoiceS (WriteS (DerefP (VarP 0)), SkipS)) & - seqo [WriteS (DerefP (VarP 0)); - ChoiceS (WriteS (DerefP (VarP 1)), WriteS (DerefP (VarP 0))); - ReadS (DerefP (VarP 0)); - ReadS (DerefP (VarP 1))] gstmts & - gd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr))); - (Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))], - gstmts) & - rd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))], - ReadS (DerefP (VarP 0))) & - seqo [ - CallS (VarP wg, [PathE (VarP xg)]); - CallS (VarP rg, [PathE (VarP xg)]); - CallS (VarP fg, [PathE (VarP xg); PathE (VarP yg)]); - CallS (VarP rg, [PathE (VarP yg)]); - CallS (VarP gg, [PathE (VarP zg); PathE (VarP kg)]); - CallS (VarP wg, [PathE (VarP zg)]); - WriteS (DerefP (VarP zg)); - CallS (VarP fg, [PathE (VarP yg); PathE (VarP zg)]); - CallS (VarP rg, [PathE (VarP kg)]) - ] stmts & - prog == Prg ([xbd; xd; - ybd; yd; - zbd; zd; - kbd; kd; - fd; wd; gd; rd], - stmts) & - prog_evalo prog q - }) - (fun q -> q#reify (StEnv.prj_exn)))) - -let prog_synt_t_presentation_simple_tp _ = show(answerCpCapList) (Stream.take (run q - (fun q -> ocanren { - fresh prog, xbg, xg, - ybg, yg, - zbg, zg, - kbg, kg, - fg, wg, gg, rg, - xbd, xd, - ybd, yd, - zbd, zd, - kbd, kd, - fd, wd, gd, rd, - fstmts, gstmts, - stmts, - c_fx, c_fy, c_wx, c_gx, c_gy, c_rx, - st in - globals_min_ido xbg & - xg == Nat.s xbg & - ybg == Nat.s xg & - yg == Nat.s ybg & - zbg == Nat.s yg & - zg == Nat.s zbg & - kbg == Nat.s zg & - kg == Nat.s kbg & - fg == Nat.s kg & - wg == Nat.s fg & - gg == Nat.s wg & - rg == Nat.s gg & - xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) & - ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) & - zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) & - kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) & - kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) & - seqo [ReadS (DerefP (VarP 0)); - WriteS (DerefP (VarP 0)); - ReadS (DerefP (VarP 1))] fstmts & - fd == FunD ([(Mode (In, NOut), RefT (c_fx, UnitT (Rd, AlwaysWr))); - (Mode (In, NOut), RefT (c_fy, UnitT (Rd, NeverWr)))], - fstmts) & - wd == FunD ([(Mode (In, NOut), RefT (c_wx, UnitT (NRd, MayWr)))], - ChoiceS (WriteS (DerefP (VarP 0)), SkipS)) & - seqo [WriteS (DerefP (VarP 0)); - ChoiceS (WriteS (DerefP (VarP 1)), WriteS (DerefP (VarP 0))); - ReadS (DerefP (VarP 0)); - ReadS (DerefP (VarP 1))] gstmts & - gd == FunD ([(Mode (In, NOut), RefT (c_gx, UnitT (NRd, AlwaysWr))); - (Mode (In, NOut), RefT (c_gy, UnitT (Rd, MayWr)))], - gstmts) & - rd == FunD ([(Mode (In, NOut), RefT (c_rx, UnitT (Rd, NeverWr)))], - ReadS (DerefP (VarP 0))) & - seqo [ - CallS (VarP wg, [PathE (VarP xg)]); - CallS (VarP rg, [PathE (VarP xg)]); - CallS (VarP fg, [PathE (VarP xg); PathE (VarP yg)]); - CallS (VarP rg, [PathE (VarP yg)]); - CallS (VarP gg, [PathE (VarP zg); PathE (VarP kg)]); - CallS (VarP wg, [PathE (VarP zg)]); - WriteS (DerefP (VarP zg)); - CallS (VarP fg, [PathE (VarP yg); PathE (VarP zg)]); - CallS (VarP rg, [PathE (VarP kg)]) - ] stmts & - prog == Prg ([xbd; xd; - ybd; yd; - zbd; zd; - kbd; kd; - fd; wd; gd; rd], - stmts) & - prog_evalo prog st & - q == [c_fx; c_fy; c_wx; c_gx; c_gy; c_rx] - }) - (fun q -> q#reify (List.prj_exn CopyCap.prj_exn)))) - -(* complex type *) +(* - complex tests *) let deref_accesso id v p' = ocanren { p' == DerefP (AccessP (VarP v, id)) @@ -692,256 +516,6 @@ let access_deref_accesso id_ext id_int v p' = ocanren { p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext) } -(* --- *) - -let p_rw_unitTo tp = ocanren { - (* fresh r, w in *) - tp == UnitT (Rd, AlwaysWr) - } - -let p_rw_userTo tp = ocanren { - fresh x, y, z in - p_rw_unitTo x & - p_rw_unitTo y & - p_rw_unitTo z & - tp == TupleT [x; y; z] - } - -let p_rw_dataTo tp = ocanren { - fresh x, y in - p_rw_unitTo x & - p_rw_unitTo y & - tp == TupleT [x; y] - } - -let p_rw_timeTo tp = ocanren { - p_rw_unitTo tp - } - -let p_rw_requestTo cu cd ct tp = ocanren { - fresh userT, dataT, timeT in - p_rw_userTo userT & - p_rw_dataTo dataT & - p_rw_timeTo timeT & - tp == TupleT [RefT (cu, userT); - RefT (cd, dataT); - RefT (ct, timeT)] - } - -(* --- *) - -let p_any_unitTo tp = ocanren { - fresh r, w in - tp == UnitT (r, w) - } - -let p_any_userTo tp = ocanren { - fresh x, y, z in - p_any_unitTo x & - p_any_unitTo y & - p_any_unitTo z & - tp == TupleT [x; y; z] - } - -let p_any_dataTo tp = ocanren { - fresh x, y in - p_any_unitTo x & - p_any_unitTo y & - tp == TupleT [x; y] - } - -let p_any_timeTo tp = ocanren { - p_any_unitTo tp - } - -let p_any_requestTo cu cd ct tp = ocanren { - fresh userT, dataT, timeT in - p_any_userTo userT & - p_any_dataTo dataT & - p_any_timeTo timeT & - tp == TupleT [RefT (cu, userT); - RefT (cd, dataT); - RefT (ct, timeT)] - } - -(* --- *) - -let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q - (fun q -> ocanren { - fresh prog, - userT, dataT, timeT, requestT, - requestArgsT, - userE, dataE, timeE, requestE, - userVID, dataVID, timeVID, requestVID, - sendFID, sendD, sendBranchStmts, sendStmts, - stmts in - globals_min_ido userVID & - dataVID == Nat.s userVID & - timeVID == Nat.s dataVID & - requestVID == Nat.s timeVID & - sendFID == Nat.s requestVID & - - p_rw_userTo userT & - p_rw_dataTo dataT & - p_rw_timeTo timeT & - p_rw_requestTo Cp Cp Cp requestT & - p_any_requestTo Cp Cp Cp requestArgsT & (* NOTE: for now *) - - userE == TupleE [UnitE; UnitE; UnitE] & - dataE == TupleE [UnitE; UnitE] & - timeE == UnitE & - requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] & - - fresh data_p0, data_p1, 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 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; - - ReadS user_name_p; - WriteS user_name_p] sendBranchStmts & - seqo [sendBranchStmts; (* TMP *) - (* 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 & - (* sendStmts == SkipS & *) - sendD == FunD ([(Mode (In, NOut), requestArgsT)], sendStmts) & - - fresh time_gp, user_name_gp, user_surname_gp in - deref_accesso 2 requestVID time_gp & - access_deref_accesso 1 0 requestVID user_name_gp & - access_deref_accesso 2 0 requestVID user_surname_gp & - seqo [ - CallS (VarP sendFID, [PathE (VarP requestVID)]); - WriteS time_gp; - (* TODO: FIXME *) - (* ChoiceS (ReadS user_name_gp, *) - (* ReadS user_surname_gp); *) - ReadS user_name_gp; (* TMP *) - ReadS user_surname_gp; (* TMP *) - ReadS time_gp - ] stmts & - prog == Prg ([ - VarD (userT, userE); - VarD (dataT, dataE); - VarD (timeT, timeE); - VarD (requestT, requestE); - sendD - ], - stmts - ) & - prog_evalo prog q - }) - (fun q -> q#reify (StEnv.prj_exn)))) - -let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take (run q - (fun q -> ocanren { - fresh prog, - userT, dataT, timeT, requestT, - requestArgsT, - userE, dataE, timeE, requestE, - userVID, dataVID, timeVID, requestVID, - sendFID, sendD, sendBranchStmts, sendStmts, - stmts, - st, c_u, c_d, c_t in - globals_min_ido userVID & - dataVID == Nat.s userVID & - timeVID == Nat.s dataVID & - requestVID == Nat.s timeVID & - sendFID == Nat.s requestVID & - - p_rw_userTo userT & - p_rw_dataTo dataT & - p_rw_timeTo timeT & - p_rw_requestTo Cp Cp Cp requestT & - p_any_requestTo c_u c_d c_t requestArgsT & (* NOTE: for now *) - - userE == TupleE [UnitE; UnitE; UnitE] & - dataE == TupleE [UnitE; UnitE] & - timeE == UnitE & - requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] & - - fresh data_p0, data_p1, 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 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; - - ReadS user_name_p; - WriteS user_name_p] sendBranchStmts & - seqo [sendBranchStmts; (* TMP *) - (* 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 & - (* sendStmts == SkipS & *) - sendD == FunD ([(Mode (In, NOut), requestArgsT)], sendStmts) & - - fresh time_gp, user_name_gp, user_surname_gp in - deref_accesso 2 requestVID time_gp & - access_deref_accesso 1 0 requestVID user_name_gp & - access_deref_accesso 2 0 requestVID user_surname_gp & - seqo [ - CallS (VarP sendFID, [PathE (VarP requestVID)]); - WriteS time_gp; - (* TODO: FIXME *) - (* ChoiceS (ReadS user_name_gp, *) - (* ReadS user_surname_gp); *) - ReadS user_name_gp; (* TMP *) - ReadS user_surname_gp; (* TMP *) - ReadS time_gp - ] stmts & - prog == Prg ([ - VarD (userT, userE); - VarD (dataT, dataE); - VarD (timeT, timeE); - VarD (requestT, requestE); - sendD - ], - stmts - ) & - prog_evalo prog st & - q == [c_u; c_d; c_t] - }) - (fun q -> q#reify (List.prj_exn CopyCap.prj_exn)))) - -(* - complex tests *) - -(* let deref_accesso id v p' = ocanren { *) - (* p' == DerefP (AccessP (VarP v, id)) *) - (* } *) - -(* let access_deref_accesso id_ext id_int v p' = ocanren { *) - (* p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext) *) - (* } *) - let access_deref_access_deref_accesso id_ext id_mid id_int v p' = ocanren { p' == AccessP (DerefP (AccessP (DerefP (AccessP (VarP v, id_int)), id_mid)), id_ext) } @@ -1081,84 +655,11 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q prog_evalo prog q }) (fun q -> q#reify (StEnv.prj_exn)))) -(* rw versions *) - let rw_unitTo tp = ocanren { (* fresh r, w in *) tp == UnitT (Rd, AlwaysWr) } -let rw_user_utilsTo tp = ocanren { - fresh x, y in - rw_unitTo x & - rw_unitTo y & - tp == TupleT [x; y] - } - -let rw_user_infoTo tp = ocanren { - fresh x, y, z in - rw_unitTo x & - rw_unitTo y & - rw_unitTo z & - tp == TupleT [x; y; z] - } - -let rw_versionTo tp = ocanren { - fresh x, y, z in - rw_unitTo x & - rw_unitTo y & - rw_unitTo z & - tp == TupleT [x; y; z] - } - -let rw_utilsTo tp = ocanren { - fresh x, y in - rw_unitTo x & - rw_unitTo y & - tp == TupleT [x; y] - } - -let rw_dataTo tp = ocanren { - rw_unitTo tp - } - -let rw_op_dateTo tp = ocanren { - rw_unitTo tp - } - -let rw_userTo cu ci tp = ocanren { - fresh utilsT, infoT in - rw_user_infoTo infoT & - rw_user_utilsTo utilsT & - tp == TupleT [RefT (cu, utilsT) (* 0 utils *); - RefT (ci, infoT) (* 1 info *)] - } - -let rw_requestTo cus cv cut cd cus_u cus_i tp = ocanren { - fresh userT, versionT, utilsT, dataT, op_dateT in - rw_userTo cus_u cus_i userT & - rw_versionTo versionT & - rw_utilsTo utilsT & - rw_dataTo dataT & - rw_op_dateTo op_dateT & - tp == TupleT [RefT (cus, userT) (* 0 user *); - RefT (cv, versionT) (* 1 version *); - RefT (cut, utilsT) (* 2 utils *); - RefT (cd, dataT) (* 3 data *); - op_dateT (* 4 operation_date *)] - } -let rw_moded_requestTo cus cv cut cd cus_u cus_i tp = ocanren { - fresh requestT in - rw_requestTo cus cv cut cd cus_u cus_i requestT & - tp == (Mode (In, NOut), requestT) - } -let rw_boxed_moded_requestTo tp = ocanren { - fresh cus, cv, cut, cd, cus_u, cus_i in - rw_moded_requestTo cus cv cut cd cus_u cus_i tp - } - -(* any versions *) - let any_unitTo tp = ocanren { fresh r, w in tp == UnitT (r, w) @@ -1166,40 +667,40 @@ let any_unitTo tp = ocanren { let any_user_utilsTo tp = ocanren { fresh x, y in - any_unitTo x & - any_unitTo y & + rw_unitTo x & + rw_unitTo y & tp == TupleT [x; y] } let any_user_infoTo tp = ocanren { fresh x, y, z in - any_unitTo x & - any_unitTo y & - any_unitTo z & + rw_unitTo x & + rw_unitTo y & + rw_unitTo z & tp == TupleT [x; y; z] } let any_versionTo tp = ocanren { fresh x, y, z in - any_unitTo x & - any_unitTo y & - any_unitTo z & + rw_unitTo x & + rw_unitTo y & + rw_unitTo z & tp == TupleT [x; y; z] } let any_utilsTo tp = ocanren { fresh x, y in - any_unitTo x & - any_unitTo y & + rw_unitTo x & + rw_unitTo y & tp == TupleT [x; y] } let any_dataTo tp = ocanren { - any_unitTo tp + rw_unitTo tp } let any_op_dateTo tp = ocanren { - any_unitTo tp + rw_unitTo tp } let any_userTo cu ci tp = ocanren { @@ -1266,13 +767,13 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q (* synt *) st in (* types *) - rw_unitTo uT_r_aw & - rw_user_utilsTo user_utilsT & - rw_user_infoTo user_infoT & - rw_userTo Cp Cp userT & - rw_versionTo versionT & - rw_utilsTo utilsT & - rw_requestTo Cp Cp Cp Cp Cp Cp requestT & + any_unitTo uT_r_aw & + any_user_utilsTo user_utilsT & + any_user_infoTo user_infoT & + any_userTo Cp Cp userT & + any_versionTo versionT & + any_utilsTo utilsT & + any_requestTo Cp Cp Cp Cp Cp Cp requestT & (* moded_requestTo moded_requestT & *) (* global vars init exprs *) user_utilsE == TupleE [UnitE (* 0 id *); UnitE] & @@ -1348,16 +849,15 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q send_allF & fresh mrT_gvi, mrT_uv, mrT_s, mrT_sa in - (* fresh gvi_c0, gvi_c1, gvi_c2, gvi_c3, gvi_c4, gvi_c5, mrT' in *) - (* any_moded_requestTo gvi_c0 gvi_c1 gvi_c2 gvi_c3 gvi_c4 gvi_c5 mrT' & *) + fresh gvi_c0, gvi_c1, gvi_c2, gvi_c3, gvi_c4, gvi_c5, mrT' in + any_moded_requestTo gvi_c0 gvi_c1 gvi_c2 gvi_c3 gvi_c4 gvi_c5 mrT' & (* TODO *) - any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_gvi & - any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_uv & - any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_s & - any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_sa & + (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_gvi & *) + (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_uv & *) + (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_s & *) + (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_sa & *) - q == [Cp] & - (* [gvi_c0; gvi_c1; gvi_c2; gvi_c3; gvi_c4; gvi_c5] & *) + q == [gvi_c0; gvi_c1; gvi_c2; gvi_c3; gvi_c4; gvi_c5] & prog == Prg ([ VarD (user_utilsT, user_utilsE); @@ -1367,17 +867,17 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q VarD (utilsT, utilsE); VarD (uT_r_aw, UnitE); (* data *) VarD (requestT, requestE); - (* FunD ([mrT'], get_version_idF); *) - (* FunD ([mrT'], updated_versionF); *) - (* FunD ([mrT'], sendF); *) - (* FunD ([mrT'], send_allF) *) - FunD ([mrT_gvi], get_version_idF); - FunD ([mrT_uv], updated_versionF); - FunD ([mrT_s], sendF); - FunD ([mrT_sa], send_allF) + FunD ([mrT'], get_version_idF); + FunD ([mrT'], updated_versionF); + FunD ([mrT'], sendF); + FunD ([mrT'], send_allF) + (* FunD ([mrT_gvi], get_version_idF); *) + (* FunD ([mrT_uv], updated_versionF); *) + (* FunD ([mrT_s], sendF); *) + (* FunD ([mrT_sa], send_allF) *) ], (* SkipS *) CallS (VarP send_allID, [PathE (VarP requestID)]) ) & prog_evalo prog st }) - (fun q -> q#reify (List.prj_exn CopyCap.prj_exn)))) + (fun q -> q#reify (List.prj_exn CopyCap.prj_exn)))) (* TODO: list *)