st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-06-11 03:38:15 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Compare commits

base: st:31111947147d602b63830235a5016dd7a2f3b84f
Branches Tags
st:main
st:lambdas_no_value
st:memory_ext
..
compare: st:de71aea4e14ae4e2fc899ecb30f528c30a476ac6
Branches Tags
st:main
st:lambdas_no_value
st:memory_ext

No commits in common. "31111947147d602b63830235a5016dd7a2f3b84f" and "de71aea4e14ae4e2fc899ecb30f528c30a476ac6" have entirely different histories.
3111194714 ... de71aea4e1

6 changed files with 656 additions and 626 deletions
Download patch file Download diff file Expand all files Collapse all files

298
model_with_structures/analyzer.ml
View file

@ -38,7 +38,7 @@ struct
| SeqS of stmt * stmt | SeqS of stmt * stmt
| ChoiceS of stmt * stmt | ChoiceS of stmt * stmt
type decl = VarD of (* data * *) atype (* * expr *) type decl = VarD of (* data * *) atype * expr
| FunD of (* data * *) (* (data * *) mtype (* ) *) list * stmt | FunD of (* data * *) (* (data * *) mtype (* ) *) list * stmt
type prog = decl list * stmt type prog = decl list * stmt
@ -71,7 +71,7 @@ struct
type writeval = ZeroWV | SmthWV | OneWV type writeval = ZeroWV | SmthWV | OneWV
type value = UnitV of memval * readval * writeval type value = UnitV of memval * readval * writeval
| FunV (* of ((* data list * *) stmt) list *) | FunV of ((* data list * *) stmt) list
| RefV of memid | RefV of memid
| TupleV of value list | TupleV of value list
@ -84,9 +84,10 @@ struct
(* --- *) (* --- *)
type mem = value list * memid (* NOTE: memory and first free elem *) type mem = value list * memid (* NOTE: memory and first free elem *)
type types = (data * atype) list type types = (data * atype) list (* glob *) * (data * atype) list (* glob + loc *)
type vals = (data * memid) list type vals = (data * memid) list (* glob *) * (data * memid) list (* glob + loc *)
type state = mem * types * vals type visited = stmt list (* TODO: FIXME: optimize, use ids *)
type state = mem * types * vals * visited
(* --- *) (* --- *)
@ -95,17 +96,23 @@ struct
let types_assoc (x : data) (types : types) : atype = let types_assoc (x : data) (types : types) : atype =
(* try ( List.assoc x (fst types) ) *) (* try ( List.assoc x (fst types) ) *)
(* with Not_found -> *) (* with Not_found -> *)
List.assoc x types List.assoc x (snd types)
let vals_assoc (x : data) (vals : vals) : memid = let vals_assoc (x : data) (vals : vals) : memid =
(* try ( List.assoc x (fst vals) ) *) (* try ( List.assoc x (fst vals) ) *)
(* with Not_found -> *) (* with Not_found -> *)
List.assoc x vals List.assoc x (snd vals)
let types_glob_add (types : types) (x : data) (t : atype) =
((x, t) :: fst types, (x, t) :: snd types)
let types_add (types : types) (x : data) (t : atype) = let types_add (types : types) (x : data) (t : atype) =
(x, t) :: types (fst types, (x, t) :: snd types)
let vals_glob_add (vals : vals) (x : data) (id : memid) =
((x, id) :: fst vals, (x, id) :: snd vals)
let vals_add (vals : vals) (x : data) (id : memid) = let vals_add (vals : vals) (x : data) (id : memid) =
(x, id) :: vals (fst vals, (x, id) :: snd vals)
(* - utils *) (* - utils *)
@ -188,34 +195,20 @@ struct
(* - value construction *) (* - value construction *)
let rec valbuild (mem : mem) (t : atype) : mem * value = let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value =
match t with match t, v with
| UnitT (Rd, _) -> (mem, UnitV (ZeroMV, ZeroRV, ZeroWV)) | UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV))
| UnitT (NRd, _) -> (mem, UnitV (BotMV, ZeroRV, ZeroWV)) | UnitT (NRd, _), UnitV _ -> (mem, UnitV (BotMV, ZeroRV, ZeroWV))
| FunT _ -> raise @@ Typing_error "valbuild: funciton value is not supported" | FunT _, FunV _ -> (mem, v)
| RefT (_, t) -> let (mem', v') = valbuild mem t in
let (mem'', id'') = mem_add mem' v' in
(mem'', RefV id'')
| TupleT ts -> let folder = fun t (mem, vs') -> let (mem', v') = valbuild mem t in
(mem', v' :: vs') in
let mem', vs' = List.fold_right folder ts (mem, []) in
(mem', TupleV vs')
(* NOTE: not needed now *)
(* 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)) *)
(* | FunT _, FunV -> (mem, v) *)
(* | RefT (Rf, _), RefV _ -> (mem, v) *) (* | RefT (Rf, _), RefV _ -> (mem, v) *)
(* | RefT (_, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in *) | RefT (_, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
(* let (mem'', id'') = mem_add mem' v' in *) let (mem'', id'') = mem_add mem' v' in
(* (mem'', RefV id'') *) (mem'', RefV id'')
(* | TupleT ts, TupleV vs -> let folder = fun v t (mem, vs') -> let (mem', v') = valcopy mem v t in *) | TupleT ts, TupleV vs -> let folder = fun (mem, vs') v t -> let (mem', v') = valcopy mem v t in
(* (mem', v' :: vs') in *) (mem', v' :: vs') in
(* let mem', vs' = List.fold_right2 folder vs ts (mem, []) in *) let mem', vs' = List.fold_left2 folder (mem, []) vs ts in
(* (mem', TupleV vs') *) (mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *)
(* | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type" *) | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type"
(* - action rules *) (* - action rules *)
@ -293,7 +286,7 @@ struct
match u, v with match u, v with
| UnitV (u_m, u_r, u_w), UnitV (v_m, v_r, v_w) -> | 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) UnitV (memvalcomb u_m v_m, readvalcomb u_r v_r, writevalcomb u_w v_w)
| FunV, FunV -> FunV | FunV ustmts, FunV vstmts -> FunV (ustmts @ vstmts)
| RefV a, RefV b -> if a == b then u else raise @@ Typing_error "valcomb: ref" | 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) | TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs)
| _, _ -> raise @@ Typing_error "valcomb" | _, _ -> raise @@ Typing_error "valcomb"
@ -325,15 +318,16 @@ struct
(* TODO: check new in vars *) (* TODO: check new in vars *)
let add_decl (state : state) (x : data) (d : decl) : state = let add_decl (state : state) (x : data) (d : decl) : state =
match state with (mem, types, vals) -> match d with match state with (mem, types, vals, visited) -> match d with
| VarD t -> let (mem', v) = valbuild mem t in | VarD (t, e) -> let v = exprval mem vals e in
let (mem'', id) = mem_add mem' v in let (mem', v') = valcopy mem v t in
(mem'', types_add types x t, vals_add vals x id) let (mem'', id) = mem_add mem' v' in
| FunD (ts, s) -> let (mem', id) = mem_add mem FunV in (mem'', types_glob_add types x t, vals_glob_add vals x id, visited)
(mem', types_add types x (FunT ts), vals_add vals x id) | FunD (ts, s) -> let (mem', id) = mem_add mem (FunV [s]) in
(mem', types_glob_add types x (FunT ts), vals_glob_add vals x id, visited)
let empty_mem : mem = ([], 0) let empty_mem : mem = ([], 0)
let empty_state : state = (empty_mem, [], []) let empty_state : state = (empty_mem, ([], []), ([], []), [])
(* TODO: better way ??? *) (* TODO: better way ??? *)
let globals_min_id : data = 1000 let globals_min_id : data = 1000
@ -394,7 +388,7 @@ struct
let v_m''' = tryspoil m w v_m'' in let v_m''' = tryspoil m w v_m'' in
(mem, UnitV (v_m''', v_r'', v_w'')) (mem, UnitV (v_m''', v_r'', v_w''))
| _ -> raise @@ Typing_error "valspoil: value after tryread is not unit") | _ -> raise @@ Typing_error "valspoil: value after tryread is not unit")
| FunT ts, FunV -> (mem, v) | FunT ts, FunV _ -> (mem, v)
| RefT (ct, t), RefV id -> | RefT (ct, t), RefV id ->
let (mem', v') = valspoil mem (mem_get mem id) t m ct in let (mem', v') = valspoil mem (mem_get mem id) t m ct in
(mem_set mem id v', RefV id) (mem_set mem id v', RefV id)
@ -408,7 +402,7 @@ struct
(* full spoil *) (* full spoil *)
let argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem = let argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
match state with (mem, types, vals) -> match state with (mem, types, vals, visited) ->
let x = pathvar p in let x = pathvar p in
let id = vals_assoc x vals in (* base var address *) let id = vals_assoc x vals in (* base var address *)
let b = pathval mem vals p in (* subvalue in var *) let b = pathval mem vals p in (* subvalue in var *)
@ -420,25 +414,29 @@ struct
mem_set mem'' id v'' mem_set mem'' id v''
let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem = let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
match state with (mem, types, vals) -> match e, t with match state with (mem, types, vals, visited) -> match e, t with
| UnitE, UnitT _ -> mem | UnitE, UnitT _ -> mem
| PathE p, t -> argsspoilp state m t p | PathE p, t -> argsspoilp state m t p
| RefE x, t -> argsspoilp state m t (VarP x) | RefE x, t -> argsspoilp state m t (VarP x)
(* TODO: FIXME: check RefE case ? *) (* TODO: FIXME: check RefE case ? *)
| TupleE es, TupleT ts -> List.fold_left2 | TupleE es, TupleT ts -> List.fold_left2
(fun mem' t' e' -> argsspoile (mem', types, vals) m t' e') (fun mem' t' e' -> argsspoile (mem', types, vals, visited) m t' e')
mem ts es mem ts es
| _, _ -> raise @@ Typing_error "valspoile" | _, _ -> raise @@ Typing_error "valspoile"
(* - funciton argument addition *) (* - funciton argument addition *)
let addarg (state : state) (x : data) (t : atype) : state = let addarg (state : state) (oldvals : vals) (x : data) (t : atype) (e : expr) : state =
match state with (mem, types, vals) -> match state with (mem, types, vals, visited) ->
let (mem', v) = valbuild mem t in let v = exprval mem oldvals e in
let (mem'', id) = mem_add mem' v in (* let t' = pathtype types p in *)
(mem'', types_add types x t, vals_add vals x id) let (mem', v') = valcopy mem v t in
let (mem'', id) = mem_add mem' v' in
(mem'', types_add types x t, vals_add vals x id, visited)
(* --- *) (* - function evaluation *)
(* 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 = let writeval_to_cap (v_w : writeval) : write_cap =
match v_w with match v_w with
@ -456,7 +454,7 @@ struct
else if writeval_to_cap v_w != w else if writeval_to_cap v_w != w
then raise @@ Eval_error "tags_check: wrong write tag" then raise @@ Eval_error "tags_check: wrong write tag"
else () else ()
| FunV, FunT _ -> () | FunV _, FunT _ -> ()
| RefV id, RefT (_, t) -> tags_check mem (mem_get mem id) t | RefV id, RefT (_, t) -> tags_check mem (mem_get mem id) t
| TupleV vs, TupleT ts -> ignore @@ List.map2 (tags_check mem) vs ts | TupleV vs, TupleT ts -> ignore @@ List.map2 (tags_check mem) vs ts
| _, _ -> raise @@ Typing_error "tags_check" | _, _ -> raise @@ Typing_error "tags_check"
@ -473,17 +471,42 @@ struct
(* - statement evaluation *) (* - statement evaluation *)
let rec stmt_eval (state : state) (s : stmt) : state = let rec stmt_eval (state : state) (s : stmt) : state =
match state with (mem, types, vals) -> match s with match state with (mem, types, vals, visited) -> match s with
| SkipS -> state | SkipS -> state
| CallS (f, es) -> let v = pathval mem vals f in | CallS (f, es) -> let v = pathval mem vals f in
let t = pathtype types f in let t = pathtype types f in
let types' : types = (fst types, fst types) in
let vals' : vals = (fst vals, fst vals) in
(match v, t with (match v, t with
| FunV, FunT ts -> | FunV (* xs, *) fstmts (* ) *), FunT ts ->
let mem_spoiled = List.fold_left2 let (state_with_args, _) = (* FIXME TMP Printf.printf "call, before args\n"; *)
(fun mem (m, t) e -> argsspoile (mem, types, vals) m t e) List.fold_left2 (* TODO: FIXME: check x's order *)
(fun (st, x) (m, t) e -> (addarg st vals x t e, x + 1))
((mem, types', vals', visited), 0) ts es in
(* NOTE: same x's, so can use same args for all the statements *)
(match state_with_args with (mem_swa, types_swa, vals_swa, visited_swa) ->
let visited_new = (* FIXME TMP Printf.printf "call, before eval\n"; *)
List.fold_left
(fun visited_old stmt ->
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_swa
fstmts in
let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *)
List.fold_left2
(fun mem (m, t) e -> argsspoile (mem, types, vals, (* NOTE: not important *) visited_new) m t e)
mem ts es in mem ts es in
(mem_spoiled, types, vals) (mem_spoiled, types, vals, visited_new))
| FunV, _ -> raise @@ Eval_error "call: function type" | FunV _, _ -> raise @@ Eval_error "call: function type"
| _, FunT _ -> raise @@ Eval_error "call: function val" | _, FunT _ -> raise @@ Eval_error "call: function val"
| _, _ -> raise @@ Eval_error "call: function type & val") | _, _ -> raise @@ Eval_error "call: function type & val")
| WriteS p -> if not @@ is_all_type_writable @@ pathtype types p | WriteS p -> if not @@ is_all_type_writable @@ pathtype types p
@ -492,12 +515,12 @@ struct
let id = vals_assoc x vals in let id = vals_assoc x vals in
let pi = pathrev p VarRP 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 AlwaysWriteA in
(mem_set mem' id v', types, vals) (mem_set mem' id v', types, vals, visited)
| ReadS p -> let x = pathvar p in | ReadS p -> let x = pathvar p in
let id = vals_assoc x vals in let id = vals_assoc x vals in
let pi = pathrev p VarRP in let pi = pathrev p VarRP in
let (mem', v') = valupd mem (mem_get mem id) pi ReadA in let (mem', v') = valupd mem (mem_get mem id) pi ReadA in
(mem_set mem' id v', types, vals) (mem_set mem' id v', types, vals, visited)
(* NOTE: handled inside through undefined in memvmod *) (* NOTE: handled inside through undefined in memvmod *)
(* if pathval mem vals p == SmthV || pathval mem vals p == BotV *) (* if pathval mem vals p == SmthV || pathval mem vals p == BotV *)
(* then raise @@ Eval_error "read: spoiled value" *) (* then raise @@ Eval_error "read: spoiled value" *)
@ -505,36 +528,18 @@ struct
stmt_eval statel sr stmt_eval statel sr
| ChoiceS (sl, sr) -> let statel = stmt_eval state sl in | ChoiceS (sl, sr) -> let statel = stmt_eval state sl in
let stater = stmt_eval state sr in let stater = stmt_eval state sr in
match statel with (meml, typesl, valsl) -> match statel with (meml, typesl, valsl, visitedl) ->
match stater with (memr, typesr, valsr) -> match stater with (memr, typesr, valsr, visitedr) ->
if typesl != typesr || valsl != valsr if typesl != typesr || valsl != valsr
then raise @@ Eval_error "choice" then raise @@ Eval_error "choice"
(* TODO: FIXME: better list union ?? *) (* TODO: FIXME: better list union ?? *)
else (memcomb meml memr, typesl, valsl) else (memcomb meml memr, typesl, valsl, visitedl @ visitedr)
(* - function evaluation *)
let rec func_eval (state : state) (d : decl) : unit =
match d with
| FunD (ts, stmt) ->
(let (state_with_args, _) = List.fold_left
(fun (st, x) (m, t) -> (addarg st x t, x + 1))
(state, 0) ts in
match stmt_eval state_with_args stmt with (mem_after_stmt, _, vals_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)
| VarD _ -> ()
(* --- program execution --- *) (* --- program execution --- *)
let prog_eval (prog : prog) : state = let prog_eval (prog : prog) : state =
match prog with (decls, s) -> match prog with (decls, s) ->
let init_state = prog_init prog in let init_state = prog_init prog in
ignore @@ List.map (func_eval init_state) decls;
stmt_eval init_state s stmt_eval init_state s
let prog_eval_noret (prog : prog) : unit = let prog_eval_noret (prog : prog) : unit =
@ -609,7 +614,8 @@ struct
let moded t = ((In, NOut), t) let moded t = ((In, NOut), t)
let defg t = VarD t let defgu t = VarD (t, UnitE)
let defg t e = VarD (t, e)
let wrS p = WriteS p let wrS p = WriteS p
let rdS p = ReadS p let rdS p = ReadS p
@ -649,40 +655,40 @@ struct
[%expect {| done! |}] [%expect {| done! |}]
let%expect_test "simple var" = let%expect_test "simple var" =
prog_eval_noret ([VarD (UnitT (Rd, MayWr))], prog_eval_noret ([VarD (UnitT (Rd, MayWr), UnitE)],
ReadS (VarP globals_min_id)); ReadS (VarP globals_min_id));
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
let%expect_test "simple var, forbidden read" = let%expect_test "simple var, forbidden read" =
try(prog_eval_noret ([VarD (UnitT (NRd, MayWr))], try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)],
ReadS (VarP globals_min_id)); ReadS (VarP globals_min_id));
[%expect.unreachable]); [%expect.unreachable]);
with Eval_error msg -> Printf.printf "%s" msg; with Eval_error msg -> Printf.printf "%s" msg;
[%expect {| memvmod: forbidden read |}] [%expect {| memvmod: forbidden read |}]
let%expect_test "simple vars, no read & read" = let%expect_test "simple vars, no read & read" =
prog_eval_noret ([VarD (UnitT (NRd, MayWr)); prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE);
VarD (UnitT (Rd, MayWr))], VarD (UnitT (Rd, MayWr), UnitE)],
ReadS (VarP (globals_min_id + 1))); ReadS (VarP (globals_min_id + 1)));
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
let%expect_test "simple var, write" = let%expect_test "simple var, write" =
prog_eval_noret ([VarD (UnitT (NRd, MayWr))], prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)],
WriteS (VarP globals_min_id)); WriteS (VarP globals_min_id));
Printf.printf "done!"; Printf.printf "done!";
[%expect {| done! |}] [%expect {| done! |}]
let%expect_test "simple var, forbidden write" = let%expect_test "simple var, forbidden write" =
try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr))], try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr), UnitE)],
WriteS (VarP globals_min_id)); WriteS (VarP globals_min_id));
[%expect.unreachable]); [%expect.unreachable]);
with Eval_error msg -> Printf.printf "%s" msg; with Eval_error msg -> Printf.printf "%s" msg;
[%expect {| write: write tag |}] [%expect {| write: write tag |}]
let%expect_test "simple var, write & read" = let%expect_test "simple var, write & read" =
prog_eval_noret ([VarD (UnitT (NRd, MayWr))], prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)],
SeqS (WriteS (VarP globals_min_id), SeqS (WriteS (VarP globals_min_id),
ReadS (VarP globals_min_id))); ReadS (VarP globals_min_id)));
Printf.printf "done!"; Printf.printf "done!";
@ -691,7 +697,7 @@ struct
(* - basic call tests *) (* - basic call tests *)
(* let%expect_test "simple call with read" = *) (* let%expect_test "simple call with read" = *)
(* prog_eval_noret ([VarD (UnitT (Rd, NeverWr)); *) (* prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE); *)
(* FunD ([((In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0)))], *) (* FunD ([((In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0)))], *)
(* CallS (VarP (globals_min_id + 1), *) (* CallS (VarP (globals_min_id + 1), *)
(* [PathE (VarP globals_min_id)])); *) (* [PathE (VarP globals_min_id)])); *)
@ -699,7 +705,7 @@ struct
(* [%expect {| done! |}] *) (* [%expect {| done! |}] *)
(* let%expect_test "simple call with write" = *) (* let%expect_test "simple call with write" = *)
(* prog_eval_noret ([VarD ((UnitT (Rd, MayWr))); *) (* prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE); *)
(* VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE globals_min_id); *) (* VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE globals_min_id); *)
(* FunD ([((In, NOut), RefT (Cp, UnitT (Rd, MayWr)))], WriteS (DerefP (VarP 0)))], *) (* FunD ([((In, NOut), RefT (Cp, UnitT (Rd, MayWr)))], WriteS (DerefP (VarP 0)))], *)
(* CallS (VarP (globals_min_id + 2), *) (* CallS (VarP (globals_min_id + 2), *)
@ -710,8 +716,8 @@ struct
let%expect_test "simple call with read, dsl" = let%expect_test "simple call with read, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_mw; defgu uT_r_mw;
defg (rfT uT_r_mw); defg (rfT uT_r_mw) rfg0E;
FunD ( FunD (
[moded @@ cpT @@ uT_r], [moded @@ cpT @@ uT_r],
rdS @@ drf @@ v0 rdS @@ drf @@ v0
@ -725,8 +731,8 @@ struct
let%expect_test "simple call with write, dsl" = let%expect_test "simple call with write, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_aw; defgu uT_aw;
defg (rfT uT_aw); defg (rfT uT_aw) rfg0E;
FunD ( FunD (
[moded @@ cpT @@ uT_aw], [moded @@ cpT @@ uT_aw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
@ -740,8 +746,8 @@ struct
let%expect_test "simple call with read after write, dsl" = let%expect_test "simple call with read after write, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_aw; defgu uT_aw;
defg (rfT uT_aw); defg (rfT uT_aw) rfg0E;
FunD ( FunD (
[moded @@ cpT @@ uT_aw], [moded @@ cpT @@ uT_aw],
(wrS @@ drf @@ v0) #. (wrS @@ drf @@ v0) #.
@ -756,8 +762,8 @@ struct
let%expect_test "simple call with forbidden write, dsl" = let%expect_test "simple call with forbidden write, dsl" =
try (prog_eval_noret ( try (prog_eval_noret (
[ [
defg uT_r_mw; defgu uT_r_mw;
defg (rfT uT_r_mw); defg (rfT uT_r_mw) rfg0E;
FunD ( FunD (
[moded @@ cpT @@ uT_r], [moded @@ cpT @@ uT_r],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
@ -773,8 +779,8 @@ struct
let%expect_test "simple call with write to ref, dsl" = let%expect_test "simple call with write to ref, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw) rfg0E;
FunD ( FunD (
[moded @@ rfT @@ uT_aw], [moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
@ -788,8 +794,8 @@ struct
let%expect_test "simple call with forbidden write to ref, dsl" = let%expect_test "simple call with forbidden write to ref, dsl" =
try (prog_eval_noret ( try (prog_eval_noret (
[ [
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw) rfg0E;
FunD ( FunD (
[moded @@ rfT @@ uT_aw], [moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
@ -805,8 +811,8 @@ struct
let%expect_test "simple call with write to ref with fix, dsl" = let%expect_test "simple call with write to ref with fix, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw) rfg0E;
FunD ( FunD (
[moded @@ rfT @@ uT_aw], [moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
@ -822,8 +828,8 @@ struct
let%expect_test "call inside call, dsl" = let%expect_test "call inside call, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw) rfg0E;
FunD ( FunD (
[moded @@ rfT @@ uT_aw], [moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
@ -844,8 +850,8 @@ struct
let%expect_test "call inside call, recursive, dsl" = let%expect_test "call inside call, recursive, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw) rfg0E;
FunD ( FunD (
[moded @@ cpT @@ uT_aw], [moded @@ cpT @@ uT_aw],
(callS vg2 [pE v0]) #. (callS vg2 [pE v0]) #.
@ -861,8 +867,8 @@ struct
let%expect_test "call to fix after call, dsl" = let%expect_test "call to fix after call, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw) rfg0E;
FunD ( FunD (
[moded @@ rfT @@ uT_aw], [moded @@ rfT @@ uT_aw],
wrS @@ drf @@ v0 wrS @@ drf @@ v0
@ -882,8 +888,8 @@ struct
let%expect_test "simple call with global variable usage, dsl" = let%expect_test "simple call with global variable usage, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r); defg (rfT uT_r) rfg0E;
FunD ( FunD (
[moded @@ cpT @@ uT], [moded @@ cpT @@ uT],
(wrS @@ vg0) #. (wrS @@ vg0) #.
@ -899,10 +905,10 @@ struct
let%expect_test "simple call with read & write (2 args), dsl" = let%expect_test "simple call with read & write (2 args), dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r; defgu uT_r;
defg (rfT uT_r); defg (rfT uT_r) rfg0E;
defg uT_aw; defgu uT_aw;
defg (rfT uT_aw); defg (rfT uT_aw) rfg2E;
FunD ( FunD (
[ [
moded @@ rfT @@ uT_r; moded @@ rfT @@ uT_r;
@ -920,14 +926,14 @@ struct
let%expect_test "simple call with different arguments modifiers, copy, dsl" = let%expect_test "simple call with different arguments modifiers, copy, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw) rfg0E;
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw) rfg2E;
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw) rfg4E;
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw) rfg6E;
FunD ( FunD (
[ [
((NIn, NOut), cpT @@ uT); ((NIn, NOut), cpT @@ uT);
@ -954,14 +960,14 @@ struct
let%expect_test "simple call with different arguments modifiers, ref, dsl" = let%expect_test "simple call with different arguments modifiers, ref, dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r; defgu uT_r;
defg (rfT uT_r); defg (rfT uT_r) rfg0E;
defg uT_r; defgu uT_r;
defg (rfT uT_r); defg (rfT uT_r) rfg2E;
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw) rfg4E;
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); defg (rfT uT_r_aw) rfg6E;
FunD ( FunD (
[ [
((NIn, NOut), rfT @@ uT); ((NIn, NOut), rfT @@ uT);
@ -989,14 +995,14 @@ struct
let%expect_test "presentation test 1 (simple types), dsl" = let%expect_test "presentation test 1 (simple types), dsl" =
prog_eval_noret ( prog_eval_noret (
[ [
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); (* x *) defg (rfT uT_r_aw) rfg0E; (* x *)
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); (* y *) defg (rfT uT_r_aw) rfg2E; (* y *)
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); (* z *) defg (rfT uT_r_aw) rfg4E; (* z *)
defg uT_r_aw; defgu uT_r_aw;
defg (rfT uT_r_aw); (* k *) defg (rfT uT_r_aw) rfg6E; (* k *)
FunD ( (* f *) FunD ( (* f *)
[ [
(moded @@ rfT @@ uT_r_aw); (moded @@ rfT @@ uT_r_aw);
@ -1067,7 +1073,7 @@ struct
(* [ *) (* [ *)
(* defg userT userE; *) (* defg userT userE; *)
(* defg dataT dataE; *) (* defg dataT dataE; *)
(* defg uT_r_aw; (* time *) *) (* defgu uT_r_aw; (* time *) *)
(* defg requestT requestE; *) (* defg requestT requestE; *)
(* FunD ( (* send *) *) (* FunD ( (* send *) *)
(* [ *) (* [ *)
@ -1162,7 +1168,7 @@ struct
(* defg userT userE; *) (* defg userT userE; *)
(* defg versionT versionE; *) (* defg versionT versionE; *)
(* defg utilsT utilsE; *) (* defg utilsT utilsE; *)
(* defg uT_r_aw; *) (* defgu uT_r_aw; *)
(* defg requestT requestE; *) (* defg requestT requestE; *)
(* get_version_idF; *) (* get_version_idF; *)
(* updated_versionF; *) (* updated_versionF; *)

279
model_with_structures/model.typ
View file

@ -15,6 +15,8 @@
// *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
#h(10pt) #h(10pt)
#let rf = $\& #h(3pt)$ #let rf = $\& #h(3pt)$
@ -138,14 +140,14 @@
`decl`, `decl`,
{ {
// TODO: path not allowed ?? // TODO: path not allowed ??
Or[$"var" X : type$][global variable declaration] Or[$"var" X : type = expr$][global variable declaration]
Or[$"fun" X ((X : modedType)+) = stmt$][function declaration] Or[$"fun" X ((X : modedType)+) = stmt$][function declaration]
} }
), ),
Prod( Prod(
`prog`, `prog`,
{ {
Or[$decl+ stmt$][all program definitions and executed statement] Or[$decl+ space stmt$][declarations and executed statement]
} }
), ),
) )
@ -201,7 +203,7 @@
$value_mu$, $value_mu$,
{ {
Or[$cdl vmem, vread, vwrite cdr$][value of the simple type, contains cells for analysis] // `Unit` Or[$cdl vmem, vread, vwrite cdr$][value of the simple type, contains cells for analysis] // `Unit`
Or[$lambda$][function pointer value, carries no information] // `Fun` 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[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
Or[$[value+]$][tuple value] // `Prod` Or[$[value+]$][tuple value] // `Prod`
} }
@ -274,6 +276,8 @@ $v in value$ - произвольное значение
), ),
) )
// TODO: FIXME: add vars & funcs from global context in the beginnning
// $V := memelem$ - значения памяти // $V := memelem$ - значения памяти
$X$ - можество переменных $X$ - можество переменных
@ -282,25 +286,18 @@ $X$ - можество переменных
#let types = $Gamma$ #let types = $Gamma$
#let envv = $#[env]_Sigma$ #let envv = $#[env]_Sigma$
#let envt = $#[env]_Gamma$ #let envt = $#[env]_Gamma$
$envv := X -> LL, space vals : envv$ - #[ метки памяти перменных контекста, частично определённая функция ] $sigma : envv := X -> LL, space vals : envv$ - #[ метки памяти перменных контекста, частично определённая функция ]
$envt := X -> type, space types : envt$ - #[ типы значений перменных контекста, частично определённая функция ] $sigma : envt := X -> type, space types : envt$ - #[ типы значений перменных контекста, частично определённая функция ]
$revpath$ - путь в обратную сторону, используется для обновления значений $revpath$ - путь в обратную сторону, используется для обновления значений
$action$ - действия, совершаемые с примитивным значением, $action$ - действия, совершаемые с примитивным значением,
модифицирующие содержащуюся таминформацию модифицирующие содержащуюся таминформацию
- $r in readTag, w in writeTag$ // $DD : X -> decl$ - глобальные определения, частично определённая функция
- $c in copyTag$
- $i in inTag, o in outTag$ // $d in decl, $
- $s in stmt$ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
- $f, x, a in X$
- $a in action$
- $p in path$
- $v in value$
- $v_m in vmem, v_r in vread, v_w in vwrite$
- $t, u in type$
- $pi in revpath$
=== Path Accessors === Path Accessors
@ -536,150 +533,89 @@ $action$ - действия, совершаемые с примитивным з
=== Value Construction === Value Construction
#let build = `build`
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ build trivial read value],
$mu xarrowSquiggly(cl Read \, w cr)_build
cl cdl 0_m, 0_r, 0_w cdr, mu cr$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ build trivial $not$ read value],
$mu xarrowSquiggly(cl not Read \, w cr)_build
cl cdl bot, 0_r, 0_w cdr, mu cr$,
)
))
#h(10pt)
// TODO: function pointer type ??
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ build funciton pointer value],
$cl mu cr xarrowSquiggly(lambda space c space overline(t))_build cl lambda, mu cr$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ build reference value],
$mu xarrowSquiggly(t)_build cl v, mu_v cr$,
$mu_v xarrowSquiggly(v)_#[add] cl l, mu_a cr$,
$mu xarrowSquiggly(rf c t)_build cl rf l, mu_a cr$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ build tuple value],
$mu_0 xarrowSquiggly(t_1)_build cl v_1, mu_1 cr$,
$...$,
$mu_(n - 1) xarrowSquiggly(t_n)_build cl v_n, mu_n cr$,
$mu_0 xarrowSquiggly([t_1, ... t_n])_build cl [v_1, ... v_n], mu_n cr$,
)
))
#h(10pt)
// ---
// TODO: FIXME:add ref / copy modes correctness check ?? // TODO: FIXME:add ref / copy modes correctness check ??
// #let copy = `copy` #let new = `new`
#align(center, prooftree(
vertical-spacing: 4pt,
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$,
)
))
// #align(center, prooftree( // #align(center, prooftree(
// vertical-spacing: 4pt, // vertical-spacing: 4pt,
// rule( // rule(
// name: [ new trivial read value], // name: [ new trivial read $top$ value],
// // NOTE: should not be important to copy v_m, because spoil & tags // $cl cdl top, v_r, v_w cdr, mu cr
// // should care for this instead // xarrowSquiggly(cl Read \, w cr)_new
// $v_m in {0, ?, bot}$, // cl cdl 0, 0, 0 cdr, mu cr$,
// $cl cdl v_m, v_r, v_w cdr, mu cr
// xarrowSquiggly(cl Read \, w cr)_copy
// cl cdl v_m, 0_r, 0_w cdr, mu cr$,
// ) // )
// )) // ))
// #h(10pt) #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$,
)
))
#align(center, prooftree(
vertical-spacing: 4pt,
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$,
)
))
// #align(center, prooftree( // #align(center, prooftree(
// vertical-spacing: 4pt, // vertical-spacing: 4pt,
// rule( // rule(
// name: [ new trivial $not$ read value], // name: [ new reference ref value],
// $v_m in {0, ?, bot/*, top */}$, // $cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$,
// $cl cdl v_m, v_r, v_w cdr, mu cr
// xarrowSquiggly(cl not Read \, w cr)_copy
// cl cdl bot, 0_r, 0_w cdr, mu cr$,
// ) // )
// )) // ))
// #h(10pt)
// #align(center, prooftree(
// vertical-spacing: 4pt,
// rule(
// name: [ new funciton pointer value],
// $cl lambda, mu cr xarrowSquiggly(lambda space c space overline(t))_copy cl lambda, mu cr$,
// )
// ))
// #h(10pt)
// NOTE: due to new memory cells types (with rw subcells) valnue should always be copied // NOTE: due to new memory cells types (with rw subcells) valnue should always be copied
// #align(center, prooftree( #align(center, prooftree(
// vertical-spacing: 4pt, vertical-spacing: 4pt,
// rule( rule(
// name: [ new reference /* copy */ value], name: [ new reference /* copy */ value],
// $cl mu[l], mu cr xarrowSquiggly(t)_copy cl v, mu_v cr$, $cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$,
// $mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$, $mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
// $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_copy cl rf l', mu_a cr$, $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_new cl rf l', mu_a cr$,
// ) )
// )) ))
// #h(10pt) #align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ new tuple value],
// #align(center, prooftree( $cl v_1, mu_0 cr xarrowSquiggly(t_1)_new cl lambda v'_1, mu_1 cr$,
// vertical-spacing: 4pt, $...$,
// rule( $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_new cl lambda v'_n, mu_n cr$,
// name: [ new tuple value],
// $cl v_1, mu_0 cr xarrowSquiggly(t_1)_copy cl v'_1, mu_1 cr$, $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_new cl [v'_1, ... v'_n], mu_n cr$,
// $...$, )
// $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_copy cl v'_n, mu_n cr$, ))
// $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_copy cl [v'_1, ... v'_n], mu_n cr$,
// )
// ))
=== Action Rules === Action Rules
@ -962,7 +898,12 @@ $action$ - действия, совершаемые с примитивным з
rule( rule(
name: [ combine lambda values], name: [ combine lambda values],
$lambda plus.o lambda = lambda$ $overline(x_1) = overline(x_2)$,
$s_1 = s_2$,
$lambda space [overline(x^1_1) space s^1_1, ... overline(x^n_1) space s^n_1]
plus.o lambda space [overline(x^1_2) space s^1_2, ... overline(x^m_2) space s^m_2]
= lambda space [overline(x^1_1) space s^1_1, ... overline(x^n_1) space s^n_1,
overline(x^1_2) space s^1_2, ... overline(x^m_2) space s^m_2]$
) )
)) ))
@ -1118,10 +1059,11 @@ $action$ - действия, совершаемые с примитивным з
// NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers) // NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers)
// expect well typed program // expect well typed program
$cl mu cr xarrowSquiggly(t)_build cl v, mu' cr$, $vals, mu texpre e eqmu v$,
$mu' xarrowSquiggly(v)_#[add] cl l, mu'' cr$, $cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$, // TODO: FIXME check (required?)
$mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$,
$cl types, vals, mu cr xarrowSquiggly("var" x : t)_init cl types[x <- t], vals[x <- l], mu'' cr$ $cl types, vals, mu cr xarrowSquiggly("var" x : t = e)_init cl types[x <- t], vals[x <- l], mu'' cr$
) )
)) ))
@ -1132,7 +1074,7 @@ $action$ - действия, совершаемые с примитивным з
rule( rule(
name: [ add function declaration], name: [ add function declaration],
$mu xarrowSquiggly(lambda)_#[add] cl l, mu' cr$, $mu xarrowSquiggly(lambda space [[x_1, ... x_n] s])_#[add] cl l, mu' cr$,
$cl types, vals, mu cr $cl types, vals, mu cr
xarrowSquiggly("fun" f (x_1 space : space m_1 t_1, ... space x_n space : space m_n t_n) space = space s)_init xarrowSquiggly("fun" f (x_1 space : space m_1 t_1, ... space x_n space : space m_n t_n) space = space s)_init
@ -1312,6 +1254,8 @@ $action$ - действия, совершаемые с примитивным з
) )
)) ))
#h(10pt)
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
@ -1398,13 +1342,17 @@ $action$ - действия, совершаемые с примитивным з
rule( rule(
name: [ add argument], name: [ add argument],
// programs considired to be well-typed $vals_#[ctx], mu texpre e eqmu v$,
$cl v, mu cr xarrowSquiggly(t)_build cl v, mu' cr$, // $types ttype p : t'$, // TODO: not required if there is no check
$mu' xarrowSquiggly(v)_#[add] cl l, mu'' cr$, // TODO: check type compatibility for t and type for path p (?)
// [*TODO: check t ~ t' in sme way (?)*],
// <- programs considired to be well-typed
$cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$,
$mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$,
// TODO save type mode somewhere ?? // <- not needed because is described by other params <- ?? // TODO save type mode somewhere ?? // <- not needed because is described by other params <- ??
$cl types, vals, mu cr $cl types, vals, mu cr
xarrowDashed(x space t) xarrowDashed(x space t space e)_(vals_#[ctx])
cl types[x <- t], vals[x <- l], mu'' cr$, cl types[x <- t], vals[x <- l], mu'' cr$,
) )
)) ))
@ -1463,7 +1411,7 @@ $action$ - действия, совершаемые с примитивным з
rule( rule(
name: [ lambda check], name: [ lambda check],
$mu ttags lambda : lambda overline(t)$, $mu ttags lambda space overline(s) : lambda overline(t)$,
) )
)) ))
#align(center, prooftree( #align(center, prooftree(
@ -1491,15 +1439,20 @@ $action$ - действия, совершаемые с примитивным з
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ function declaration evaluation], name: [ new reference copy value],
// TODO: FIXME: introduce global types and vals
$types_0 = types_#[glob]$,
$vals_0 = vals_#[glob]$,
$mu_0 = mu$,
// NOTE: dashed arrow to fill context // NOTE: dashed arrow to fill context
$cl types_0, vals_0, mu_0 cr $cl types_0, vals_0, mu_0 cr
xarrowDashed(x_1 space t_1) xarrowDashed(x_1 space t_1 space e_1)_vals
cl types', vals_1, mu_1 cr$, cl types', vals_1, mu_1 cr$,
$...$, $...$,
$cl types_(n - 1), vals_(n - 1), mu_(n - 1) cr $cl types_(n - 1), vals_(n - 1), mu_(n - 1) cr
xarrowDashed(x_n space t_n) xarrowDashed(x_n space t_n space e_n)_vals
cl types_n, vals_n, mu_n cr$, cl types_n, vals_n, mu_n cr$,
// NOTE: eval function body // NOTE: eval function body
@ -1512,18 +1465,7 @@ $action$ - действия, совершаемые с примитивным з
$...$, $...$,
$mu' ttags mu'[vals'[x_n]] : t_n$, $mu' ttags mu'[vals'[x_n]] : t_n$,
$types_0, vals_0, mu_0 tfunceval "fun" f [(x_1 m_1 t_1), .. (x_n m_n x_n)] = s$, $vals, mu_0 tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ var declaration evaluation (skip)],
$types, vals, mu tfunceval "var" x : t$,
) )
)) ))
@ -1612,8 +1554,14 @@ $action$ - действия, совершаемые с примитивным з
rule( rule(
name: [ CALL $f space [e_1, ... e_n]$], name: [ CALL $f space [e_1, ... e_n]$],
$vals, mu_0 tval f eqmu lambda [overline(x)_1 space s_1, ... overline(x)_n space s_n]$,
$types ttype f : lambda [m_1 t_1, ... m_n t_n] $, $types ttype f : lambda [m_1 t_1, ... m_n t_n] $,
// NOTE: check that all the possible bodies are possible to eval
$vals, mu_0 tfunceval cl s_1, overline(x)_1, [t_1, ... t_n], [e_1, ... e_n] cr$,
$...$,
$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: "spoil" context for each argument usage
$mu_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) mu_1$, $mu_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) mu_1$,
$...$, $...$,
@ -1728,11 +1676,14 @@ $action$ - действия, совершаемые с примитивным з
$...$, $...$,
$cl types_(n - 1), vals_(n - 1), mu_(n - 1) cr xarrowSquiggly(d_n)_init cl types_n, vals_n, mu_n cr$, $cl types_(n - 1), vals_(n - 1), mu_(n - 1) cr xarrowSquiggly(d_n)_init cl types_n, vals_n, mu_n cr$,
$cl types_n, vals_n, mu_n tfunceval d_1$, // TODO: FIXME: some easy way to pass to eval ??
$...$, $types_#[glob] = types_n$,
$cl types_n, vals_n, mu_n tfunceval d_n$, $vals_#[glob] = vals_n$,
$mu_#[glob] = mu_n$,
$cl types_0, vals_0, mu_0 cr xarrowSquiggly(d_1 ... d_n)_prog_eval cl types_n, vals_n, mu_n cr$ $cl types_n, vals_n, mu_n cr xarrow(s) cl types', vals', mu' cr$,
$cl types_0, vals_0, mu_0 cr xarrowSquiggly(d_1 ... d_n s)_prog_eval cl types', vals', mu' cr$
) )
)) ))

10
model_with_structures/send_example.md
View file

@ -49,19 +49,19 @@ struct Request {
Version* version; Version* version;
Utils* utils; Utils* utils;
Data* data; Data* data;
DateTime time; DateTime operaiton_date;
}; };
// example itself // example itself
int get_version_id(Request /*[?]*/ r) { int get_version_id(Request /*[?]*/ r) {
if (r.utils.has_version) { if (r.utils.has_version) {
return r.version.id; return r.version.id;
} }
return old_version_placeholder().id; return old_version_placeholder().id;
} }
Version updated_version(Request /*[?]*/ r) { Version updated_version(Request /*[?]*/ r) {
if (not r.utils.has_version) { if (not r.utils.has_version) {
return old_version_placeholder(); return old_version_placeholder();
} }
@ -114,12 +114,12 @@ Request := [& User; # user
& Version; # version & Version; # version
& Utils; # utils & Utils; # utils
& (); # data & (); # data
()] # time ()] # operation_date
# or Request := [& [& [(); ()], & [(); (); ()]]; # user # or Request := [& [& [(); ()], & [(); (); ()]]; # user
# & [(); (); ()]; # version # & [(); (); ()]; # version
# & [(); ()]; # utils # & [(); ()]; # utils
# & (); # data # & (); # data
# ()] # time # ()] # operation_date
# example itself # example itself

397
model_with_structures/synthesizer.ml
View file

@ -147,7 +147,7 @@ struct
module Decl = struct module Decl = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject [%%ocanren_inject
type nonrec ((* 'd, *) 't, 'e, (* 'dl, *) 'mtl, 's) t = VarD of (* 'd * *) 't | FunD of (* 'd * 'dl * *) 'mtl * 's type nonrec ((* 'd, *) 't, 'e, (* 'dl, *) 'mtl, 's) t = VarD of (* 'd * *) 't * 'e | FunD of (* 'd * 'dl * *) 'mtl * 's
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type ground = ((* Nat.ground, *) Type.ground, Expr.ground, (* Nat.ground List.ground, *) (Mode.ground * Type.ground) List.ground, Stmt.ground) t type ground = ((* Nat.ground, *) Type.ground, Expr.ground, (* Nat.ground List.ground, *) (Mode.ground * Type.ground) List.ground, Stmt.ground) t
] ]
@ -194,12 +194,13 @@ struct
module Value = struct module Value = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject [%%ocanren_inject
type nonrec ('vm, 'vr, 'vw, 'd, 'vl) t = UnitV of 'vm * 'vr * 'vw type nonrec ('vm, 'vr, 'vw, 'sl, 'd, 'vl) t = UnitV of 'vm * 'vr * 'vw
| FunV | FunV of 'sl
| RefV of 'd | RefV of 'd
| TupleV of 'vl | TupleV of 'vl
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type ground = (MemVal.ground, ReadVal.ground, WriteVal.ground, type ground = (MemVal.ground, ReadVal.ground, WriteVal.ground,
((* Nat.ground List.ground * *) Stmt.ground) List.ground,
Nat.ground, ground List.ground) t Nat.ground, ground List.ground) t
] ]
end end
@ -236,7 +237,7 @@ struct
module TypesEnv = struct module TypesEnv = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject [%%ocanren_inject
type nonrec 'dtl t = TypesEnv of 'dtl type nonrec 'dtl t = TypesEnv of 'dtl (* glob *) * 'dtl (* glob + loc *)
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = ((Nat.ground * Type.ground) List.ground) t type nonrec ground = ((Nat.ground * Type.ground) List.ground) t
] ]
@ -245,18 +246,27 @@ struct
module ValsEnv = struct module ValsEnv = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject [%%ocanren_inject
type nonrec 'ddl t = ValsEnv of 'ddl type nonrec 'ddl t = ValsEnv of 'ddl (* glob *) * 'ddl (* glob + loc *)
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = ((Nat.ground * Nat.ground) List.ground) t type nonrec ground = ((Nat.ground * Nat.ground) List.ground) t
] ]
end end
module VisitedEnv = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject
type nonrec 'sl t = VisitedEnv of 'sl
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (Stmt.ground List.ground) t
]
end
module StEnv = struct module StEnv = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject [%%ocanren_inject
type nonrec ('mem, 'types, 'vals) t = StEnv of 'mem * 'types * 'vals type nonrec ('mem, 'types, 'vals, 'visited) t = StEnv of 'mem * 'types * 'vals * 'visited
[@@deriving gt ~options:{ show; gmap }] [@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground) t type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground, VisitedEnv.ground) t
] ]
end end
@ -395,35 +405,87 @@ struct
let types_assoco id types tp = let types_assoco id types tp =
let open TypesEnv in let open TypesEnv in
ocanren { ocanren {
fresh tps in fresh _glob_tps, tps in
types == TypesEnv tps & types == TypesEnv (_glob_tps, tps) &
List.assoco id tps tp List.assoco id tps tp
} }
let vals_assoco id vals v = let vals_assoco id vals v =
let open ValsEnv in let open ValsEnv in
ocanren { ocanren {
fresh vs in fresh _glob_vs, vs in
vals == ValsEnv vs & vals == ValsEnv (_glob_vs, vs) &
List.assoco id vs v List.assoco id vs v
} }
let types_glob_addo types x tp types' =
let open TypesEnv in
ocanren {
fresh glob_tps, tps in
types == TypesEnv (glob_tps, tps) &
types' == TypesEnv ((Std.pair x tp) :: glob_tps,
(Std.pair x tp) :: tps)
}
let types_addo types x tp types' = let types_addo types x tp types' =
let open TypesEnv in let open TypesEnv in
ocanren { ocanren {
fresh tps in fresh glob_tps, tps in
types == TypesEnv tps & types == TypesEnv (glob_tps, tps) &
types' == TypesEnv ((Std.pair x tp) :: tps) types' == TypesEnv (glob_tps, (Std.pair x tp) :: tps)
}
let vals_glob_addo vals x v vals' =
let open ValsEnv in
ocanren {
fresh glob_vs, vs in
vals == ValsEnv (glob_vs, vs) &
vals' == ValsEnv ((Std.pair x v) :: glob_vs,
(Std.pair x v) :: vs)
} }
let vals_addo vals x v vals' = let vals_addo vals x v vals' =
let open ValsEnv in let open ValsEnv in
ocanren { ocanren {
fresh vs in fresh glob_vs, vs in
vals == ValsEnv vs & vals == ValsEnv (glob_vs, vs) &
vals' == ValsEnv ((Std.pair x v) :: vs) vals' == ValsEnv (glob_vs, (Std.pair x v) :: vs)
} }
let visited_appendo visitedl visitedr visited' =
let open VisitedEnv in
ocanren {
fresh vsl, vsr, vs' in
visitedl == VisitedEnv vsl &
visitedr == VisitedEnv vsr &
List.appendo vsl vsr vs' &
visited' == VisitedEnv vs'
}
let visited_checko visited stmt =
let open VisitedEnv in
ocanren {
fresh vs in
visited == VisitedEnv vs &
List.membero vs stmt
}
let not_visited_checko visited stmt =
let open VisitedEnv in
ocanren {
fresh vs in
visited == VisitedEnv vs &
list_not_membero vs stmt
}
let visited_addo visited stmt visited' =
let open VisitedEnv in
ocanren {
fresh vs in
visited == VisitedEnv vs &
visited' == VisitedEnv (stmt :: vs)
}
(* --- *) (* --- *)
let mem_geto mem id v = let mem_geto mem id v =
@ -526,15 +588,15 @@ struct
(* - value construction *) (* - value construction *)
let rec valbuild_foldero mem_with_vs tp mem_with_vs' = let rec valcopy_foldero mem_with_vs v tp mem_with_vs' =
ocanren { ocanren {
fresh mem, vs, mem', v', vs' in fresh mem, vs, mem', v', vs' in
Std.pair mem vs == mem_with_vs & Std.pair mem vs == mem_with_vs &
valbuildo mem tp (Std.pair mem' v') & valcopyo mem v tp (Std.pair mem' v') &
vs' == v' :: vs & vs' == v' :: vs &
mem_with_vs' == Std.pair mem' vs' mem_with_vs' == Std.pair mem' vs'
} }
and valbuildo mem tp mem_with_id' = and valcopyo mem v tp mem_with_id' =
let open Type in let open Type in
let open Value in let open Value in
let open ReadCap in let open ReadCap in
@ -544,72 +606,35 @@ struct
let open WriteVal in let open WriteVal in
ocanren { ocanren {
{ fresh r, w in { fresh r, w in
is_trivial_vo v &
tp == UnitT (r, w) & tp == UnitT (r, w) &
{ { r == Rd & { { fresh v_m, _v_r, _v_w in
mem_with_id' == Std.pair mem (UnitV (ZeroMV, ZeroRV, ZeroWV)) } | r == Rd &
v == UnitV (v_m, _v_r, _v_w) &
mem_with_id' == Std.pair mem (UnitV (v_m, ZeroRV, ZeroWV)) } |
{ r == NRd & { r == NRd &
mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } | mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } |
(* { fresh ts in *) { fresh stmts, ts in
(* tp == FunT ts & *) v == FunV stmts &
(* ??? } | *) tp == FunT ts &
{ fresh c, tp' in mem_with_id' == Std.pair mem v } |
{ fresh c, tp', id in
v == RefV id &
tp == RefT (c, tp') & tp == RefT (c, tp') &
{ fresh mem_cp, v_cp, mem_add, id_add in (* { c == Rf & mem_with_id' == Std.pair mem v } | *)
valbuildo mem tp' (Std.pair mem_cp v_cp) & { 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_addo mem_cp v_cp (Std.pair mem_add id_add) &
mem_with_id' == (mem_add, RefV id_add) } } | mem_with_id' == (mem_add, RefV id_add) } } |
{ fresh tps, mem', vs' in { fresh vs, tps, mem', vs' in
v == TupleV vs &
tp == TupleT tps & tp == TupleT tps &
list_foldro valbuild_foldero (Std.pair mem []) tps (Std.pair mem' vs') & list_foldr2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') &
mem_with_id' == Std.pair mem' (TupleV vs') } mem_with_id' == Std.pair mem' (TupleV vs') }
} }
(* let rec valcopy_foldero mem_with_vs v tp mem_with_vs' = *)
(* ocanren { *)
(* fresh mem, vs, mem', v', vs' in *)
(* Std.pair mem vs == mem_with_vs & *)
(* valcopyo mem v tp (Std.pair mem' v') & *)
(* vs' == v' :: vs & *)
(* mem_with_vs' == Std.pair mem' vs' *)
(* } *)
(* and valcopyo mem v tp mem_with_id' = *)
(* 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 *)
(* ocanren { *)
(* { fresh r, w in *)
(* 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)) } } } | *)
(* { fresh stmts, ts in *)
(* v == FunV stmts & *)
(* tp == FunT ts & *)
(* mem_with_id' == Std.pair mem v } | *)
(* { 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) } } | *)
(* { fresh vs, tps, mem', vs' in *)
(* v == TupleV vs & *)
(* tp == TupleT tps & *)
(* list_foldr2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') & *)
(* mem_with_id' == Std.pair mem' (TupleV vs') } *)
(* } *)
(* - action rules *) (* - action rules *)
let memvmodo a v_m v_m' = let memvmodo a v_m v_m' =
@ -732,7 +757,8 @@ struct
{ u == ZeroRV & v == ZeroRV & u' == ZeroRV } | { u == ZeroRV & v == ZeroRV & u' == ZeroRV } |
{ u == TopRV & v == ZeroRV & u' == ZeroRV } | { u == TopRV & v == ZeroRV & u' == ZeroRV } |
{ u == ZeroRV & v == TopRV & u' == ZeroRV } | { u == ZeroRV & v == TopRV & u' == ZeroRV } |
{ { u == OneRV | { u =/= OneRV & v == OneRV } } & { u =/= TopRV & v =/= TopRV &
u =/= ZeroRV & v =/= ZeroRV &
u' == OneRV } u' == OneRV }
} }
@ -758,9 +784,12 @@ struct
readvalcombo u_r v_r u_r' & readvalcombo u_r v_r u_r' &
writevalcombo u_w v_w u_w' & writevalcombo u_w v_w u_w' &
u' == UnitV (u_m', u_r', u_w') } | u' == UnitV (u_m', u_r', u_w') } |
{ u == FunV & { fresh ustmts, vstmts, ustmts' in
v == FunV & u == FunV ustmts &
u' == FunV } | v == FunV vstmts &
(* TODO: swap stmts order o efficiency ? *)
List.appendo ustmts vstmts ustmts' &
u' == FunV ustmts' } |
{ fresh a, b in { fresh a, b in
u == RefV a & u == RefV a &
v == RefV b & v == RefV b &
@ -845,26 +874,32 @@ struct
let open Value in let open Value in
let open Type in let open Type in
ocanren { ocanren {
fresh mem, types, vals in fresh mem, types, vals, visited in
st == StEnv (mem, types, vals) & st == StEnv (mem, types, vals, visited) &
{ {
{ fresh tp, mem_bd, v_bd, { fresh tp, e, v,
mem_cp, v_cp,
mem_add, id_add, mem_add, id_add,
types', vals' in types', vals' in
d == VarD tp & d == VarD (tp, e) &
valbuildo mem tp (Pair.pair mem_bd v_bd) & exprvalo mem vals e v &
mem_addo mem_bd v_bd (Pair.pair mem_add id_add) & valcopyo mem v tp (Pair.pair mem_cp v_cp) &
types_addo types x tp types' & (* mem_cp == mem & v_cp == v & *)
vals_addo vals x id_add vals' & mem_addo mem_cp v_cp (Pair.pair mem_add id_add) &
st' == StEnv (mem_add, types', vals') } | (* mem_add == mem_cp & *)
types_glob_addo types x tp types' &
(* types == types' & *)
(* vals == vals' & *)
vals_glob_addo vals x id_add vals' &
st' == StEnv (mem_add, types', vals', visited) } |
{ fresh tps, s, { fresh tps, s,
mem_add, id_add, mem_add, id_add,
types', vals' in types', vals' in
d == FunD (tps, s) & d == FunD (tps, s) &
mem_addo mem FunV (Pair.pair mem_add id_add) & mem_addo mem (FunV [s]) (Pair.pair mem_add id_add) &
types_addo types x (FunT tps) types' & types_glob_addo types x (FunT tps) types' &
vals_addo vals x id_add vals' & vals_glob_addo vals x id_add vals' &
st' == StEnv (mem_add, types', vals') st' == StEnv (mem_add, types', vals', visited)
} }
} }
} }
@ -877,10 +912,11 @@ struct
let open StEnv in let open StEnv in
let open TypesEnv in let open TypesEnv in
let open ValsEnv in let open ValsEnv in
let open VisitedEnv in
ocanren { ocanren {
fresh m in fresh m in
empty_memo m & empty_memo m &
st == StEnv (m, TypesEnv [], ValsEnv []) st == StEnv (m, TypesEnv ([], []), ValsEnv ([], []), VisitedEnv [])
} }
(* TODO: better way ??? *) (* TODO: better way ??? *)
@ -986,9 +1022,9 @@ struct
v'' == UnitV (v_m''', v_r'', v_w'') & v'' == UnitV (v_m''', v_r'', v_w'') &
mem_with_v' == Std.pair mem v'' } mem_with_v' == Std.pair mem v'' }
} } | } } |
{ fresh ts in { fresh ts, _stmts in
tp == FunT ts & tp == FunT ts &
v == FunV & v == FunV _stmts &
mem_with_v' == Std.pair mem v } | mem_with_v' == Std.pair mem v } |
{ fresh ctp', tp', id', v', mem_sp, v_sp, mem_set in { fresh ctp', tp', id', v', mem_sp, v_sp, mem_set in
tp == RefT (ctp', tp') & tp == RefT (ctp', tp') &
@ -1014,10 +1050,10 @@ struct
let open CopyCap in let open CopyCap in
let open RevPath in let open RevPath in
ocanren { ocanren {
fresh mem, types, vals, 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 mem_sp, b_sp, v_sp, mem_upd, v_upd in
st == StEnv (mem, types, vals) & st == StEnv (mem, types, vals, visited) &
pathvaro p x & pathvaro p x &
vals_assoco x vals id & vals_assoco x vals id &
pathvalo mem vals p b & pathvalo mem vals p b &
@ -1029,11 +1065,11 @@ struct
mem_seto mem_upd id v_upd mem' mem_seto mem_upd id v_upd mem'
} }
let rec argsspoile_foldero types vals m mem tp e mem' = let rec argsspoile_foldero types vals visited m mem tp e mem' =
let open StEnv in let open StEnv in
ocanren { ocanren {
fresh st in fresh st in
st == StEnv (mem, types, vals) & st == StEnv (mem, types, vals, visited) &
argsspoileo st m tp e mem' argsspoileo st m tp e mem'
} }
and argsspoileo st m tp e mem' = and argsspoileo st m tp e mem' =
@ -1042,8 +1078,8 @@ struct
let open Type in let open Type in
let open Path in let open Path in
ocanren { ocanren {
fresh _r, _w, mem, types, vals in fresh _r, _w, mem, types, vals, visited in
st == StEnv (mem, types, vals) & st == StEnv (mem, types, vals, visited) &
{ {
{ e == UnitE & { e == UnitE &
tp == UnitT (_r, _w) & tp == UnitT (_r, _w) &
@ -1057,28 +1093,30 @@ struct
{ fresh es, tps in { fresh es, tps in
e == TupleE es & e == TupleE es &
tp == TupleT tps & tp == TupleT tps &
list_foldl2o (argsspoile_foldero types vals m) mem tps es mem'} list_foldl2o (argsspoile_foldero types vals visited m) mem tps es mem'}
} }
} }
(* - funciton argument addition *) (* - funciton argument addition *)
let addargo st x tp st' = let addargo st oldvals x tp e st' =
let open StEnv in let open StEnv in
ocanren { ocanren {
fresh mem, types, vals, fresh mem, types, vals, visited, v,
mem_bd, v_bd, mem_cp, v_cp,
mem_add, id_add, mem_add, id_add,
types', vals' in types', vals' in
st == StEnv (mem, types, vals) & st == StEnv (mem, types, vals, visited) &
valbuildo mem tp (Std.pair mem_bd v_bd) & exprvalo mem oldvals e v &
mem_addo mem_bd v_bd (Std.pair mem_add id_add) & valcopyo mem v tp (Std.pair mem_cp v_cp) &
mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
types_addo types x tp types' & types_addo types x tp types' &
vals_addo vals x id_add vals' & vals_addo vals x id_add vals' &
st' == StEnv (mem_add, types', vals') st' == StEnv (mem_add, types', vals', visited)
} }
(* --- *) (* - function evaluation *)
(* NOTE: not needed due to performed optimization in stmt_eval ? *)
let writeval_to_capo v_w w' = let writeval_to_capo v_w w' =
let open WriteVal in let open WriteVal in
@ -1106,8 +1144,8 @@ struct
} & } &
writeval_to_capo v_w w writeval_to_capo v_w w
} | } |
{ fresh _ts in { fresh _stmts, _ts in
v == FunV & v == FunV _stmts &
tp == FunT _ts } | tp == FunT _ts } |
{ fresh id, _c, tp', v' in { fresh id, _c, tp', v' in
v == RefV id & v == RefV id &
@ -1141,34 +1179,90 @@ struct
(* - statement evaluation *) (* - statement evaluation *)
let rec stmt_eval_spoil_foldero types vals mem mtp e mem' = let rec stmt_addarg_foldero vals st_with_id mtp e st_with_id' = ocanren {
fresh st, x, m, tp, st' in
Std.pair st x == st_with_id &
Std.pair m tp == mtp &
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' =
let open StEnv in
ocanren {
{ fresh visited_add, st,
st', mem', types', vals',
_x', visited'' 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''
} |
{ visited_checko visited stmt &
visited == visited' }
}
and stmt_eval_spoil_foldero types vals visited mem mtp e mem' =
let open StEnv in let open StEnv in
ocanren { ocanren {
fresh m, tp, st in fresh m, tp, st in
Std.pair m tp == mtp & Std.pair m tp == mtp &
st == StEnv (mem, types, vals) & st == StEnv (mem, types, vals, visited) &
argsspoileo st m tp e mem' argsspoileo st m tp e mem'
} }
and stmt_evalo st s st' = and stmt_evalo st s st' =
let open StEnv in let open StEnv in
let open Stmt in let open Stmt in
let open Value in
let open Type in let open Type in
(* let open WriteCap in *)
let open TypesEnv in
let open ValsEnv in
let open RevPath in let open RevPath in
let open Action in let open Action in
ocanren { ocanren {
fresh mem, types, vals in fresh mem, types, vals, visited in
st == StEnv (mem, types, vals) & st == StEnv (mem, types, vals, visited) &
{ {
{ s == SkipS & st == st' } | { s == SkipS & st == st' } |
{ fresh f, es, tp, { fresh f, es, v, tp,
_tps, _vs, tps, glob_tps, _tps,
mem_spoiled in glob_vs, _vs,
types_call, vals_call,
fstmts, tps, st_call,
state_with_args,
mem_swa, types_swa,
vals_swa, visited_swa,
_arg_id, mem_spoiled,
visited' in
s == CallS (f, es) & s == CallS (f, es) &
pathvalo mem vals f v &
pathtypeo types f tp & pathtypeo types f tp &
types == TypesEnv (glob_tps, _tps) &
vals == ValsEnv (glob_vs, _vs) &
types_call == TypesEnv (glob_tps, glob_tps) &
vals_call == ValsEnv (glob_vs, glob_vs) &
v == FunV fstmts &
tp == FunT tps & tp == FunT tps &
list_foldl2o (stmt_eval_spoil_foldero types vals) st_call == StEnv (mem, types_call, vals_call, visited) &
list_foldl2o (stmt_addarg_foldero vals)
(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' &
(* TODO: FIXME check left or right order *)
list_foldl2o (stmt_eval_spoil_foldero types vals (* NOTE: not important*) visited')
mem tps es mem_spoiled & mem tps es mem_spoiled &
st' == StEnv (mem_spoiled, types, vals) st' == StEnv (mem_spoiled, types, vals, visited')
} | } |
{ fresh p, tp, x, id, v, rp, { fresh p, tp, x, id, v, rp,
mem_upd, v_upd, mem_set in mem_upd, v_upd, mem_set in
@ -1181,7 +1275,7 @@ struct
pathrevo p VarRP rp & pathrevo p VarRP rp &
valupdo mem v rp AlwaysWriteA (Std.pair mem_upd v_upd) & valupdo mem v rp AlwaysWriteA (Std.pair mem_upd v_upd) &
mem_seto mem_upd id v_upd mem_set & mem_seto mem_upd id v_upd mem_set &
st' == StEnv (mem_set, types, vals) } | st' == StEnv (mem_set, types, vals, visited) } |
{ fresh p, _tp, _r, _w, x, id, v, rp, { fresh p, _tp, _r, _w, x, id, v, rp,
mem_upd, v_upd, mem_set in mem_upd, v_upd, mem_set in
s == ReadS p & s == ReadS p &
@ -1191,7 +1285,7 @@ struct
pathrevo p VarRP rp & pathrevo p VarRP rp &
valupdo mem v rp ReadA (Std.pair mem_upd v_upd) & valupdo mem v rp ReadA (Std.pair mem_upd v_upd) &
mem_seto mem_upd id v_upd mem_set & mem_seto mem_upd id v_upd mem_set &
st' == StEnv (mem_set, types, vals) } | st' == StEnv (mem_set, types, vals, visited) } |
(* { fresh p in *) (* { fresh p in *)
(* s == ReadS p & *) (* s == ReadS p & *)
(* pathvalo mem vals p ZeroV & *) (* pathvalo mem vals p ZeroV & *)
@ -1201,58 +1295,22 @@ struct
stmt_evalo st sl stl & stmt_evalo st sl stl &
stmt_evalo stl sr st' } | stmt_evalo stl sr st' } |
{ fresh sl, sr, stl, str, { fresh sl, sr, stl, str,
meml, typesl, valsl, meml, typesl, valsl, visitedl,
memr, typesr, valsr, memr, typesr, valsr, visitedr,
mem' in visited', mem' in
s == ChoiceS (sl, sr) & s == ChoiceS (sl, sr) &
stmt_evalo st sl stl & stmt_evalo st sl stl &
stmt_evalo st sr str & stmt_evalo st sr str &
stl == StEnv (meml, typesl, valsl) & stl == StEnv (meml, typesl, valsl, visitedl) &
str == StEnv (memr, typesr, valsr) & str == StEnv (memr, typesr, valsr, visitedr) &
typesl == typesr & typesl == typesr &
valsl == valsr & valsl == valsr &
memcombo meml memr mem' & memcombo meml memr mem' &
st' == StEnv (mem', typesl, valsl) } visited_appendo visitedr visitedl visited' &
st' == StEnv (mem', typesl, valsl, visited') }
} }
} }
(* - function evaluation *)
let rec f_addarg_foldero st_with_id mtp st_with_id' = ocanren {
fresh st, x, m, tp, st' in
Std.pair st x == st_with_id &
Std.pair m tp == mtp &
addargo st x tp 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
}
(* list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa tps) visited_swa fstmts visited' & *)
and func_evalo st d =
let open StEnv in
let open Decl in
ocanren {
{ fresh tps, stmt,
state_with_args, _arg_id, st_after_stmt,
mem_after_stmt, _types_after_stmt, vals_after_stmt, _x' in
d == FunD (tps, stmt) &
list_foldlo f_addarg_foldero
(Std.pair st 0) tps
(Std.pair state_with_args _arg_id) &
stmt_evalo state_with_args stmt st_after_stmt &
st_after_stmt == StEnv (mem_after_stmt, _types_after_stmt, vals_after_stmt) &
list_foldlo (f_tags_check_foldero mem_after_stmt vals_after_stmt) 0 tps _x'
} |
{ fresh _tp in
d == VarD _tp }
}
(* --- program execution --- *) (* --- program execution --- *)
let prog_evalo prog st' = let prog_evalo prog st' =
@ -1261,7 +1319,6 @@ struct
fresh decls, s, init_st in fresh decls, s, init_st in
prog == Prg (decls, s) & prog == Prg (decls, s) &
prog_inito prog init_st & prog_inito prog init_st &
list_checko (func_evalo init_st) decls &
stmt_evalo init_st s st' stmt_evalo init_st s st'
} }
end end

40
model_with_structures/tests.ml
View file

File diff suppressed because one or more lines are too long

258
model_with_structures/tests_f.ml
View file

@ -67,7 +67,7 @@ let prog_eval_t_simple_var _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg in fresh prog, xg in
globals_min_ido xg & globals_min_ido xg &
prog == Prg ([VarD (UnitT (Rd, MayWr))], prog == Prg ([VarD (UnitT (Rd, MayWr), UnitE)],
ReadS (VarP xg)) & ReadS (VarP xg)) &
prog_evalo prog q }) prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
@ -87,7 +87,7 @@ let prog_eval_t_simple_var_fbd_rd _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg in fresh prog, xg in
globals_min_ido xg & globals_min_ido xg &
prog == Prg ([VarD (UnitT (NRd, MayWr))], prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)],
ReadS (VarP xg)) & ReadS (VarP xg)) &
prog_evalo prog q }) prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
@ -97,8 +97,8 @@ let prog_eval_t_simple_vars_fbd_rd_rd _ = show(answer) (Stream.take (run q
fresh prog, xg, yg in fresh prog, xg, yg in
globals_min_ido xg & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
prog == Prg ([VarD (UnitT (NRd, MayWr)); prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE);
VarD (UnitT (Rd, MayWr))], VarD (UnitT (Rd, MayWr), UnitE)],
ReadS (VarP yg)) & ReadS (VarP yg)) &
prog_evalo prog q }) prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
@ -107,7 +107,7 @@ let prog_eval_t_simple_var_wr _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg in fresh prog, xg in
globals_min_ido xg & globals_min_ido xg &
prog == Prg ([VarD (UnitT (NRd, MayWr))], prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)],
WriteS (VarP xg)) & WriteS (VarP xg)) &
prog_evalo prog q }) prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
@ -116,7 +116,7 @@ let prog_eval_t_simple_var_fbd_wr _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg in fresh prog, xg in
globals_min_ido xg & globals_min_ido xg &
prog == Prg ([VarD (UnitT (NRd, NeverWr))], prog == Prg ([VarD (UnitT (NRd, NeverWr), UnitE)],
WriteS (VarP xg)) & WriteS (VarP xg)) &
prog_evalo prog q }) prog_evalo prog q })
(fun q -> q#reify (StEnv.prj_exn)))) (fun q -> q#reify (StEnv.prj_exn))))
@ -125,7 +125,7 @@ let prog_eval_t_simple_var_wr_rd _ = show(answer) (Stream.take (run q
(fun q -> ocanren { (fun q -> ocanren {
fresh prog, xg in fresh prog, xg in
globals_min_ido xg & globals_min_ido xg &
prog == Prg ([VarD (UnitT (NRd, MayWr))], prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)],
SeqS (WriteS (VarP xg), SeqS (WriteS (VarP xg),
ReadS (VarP xg))) & ReadS (VarP xg))) &
prog_evalo prog q }) prog_evalo prog q })
@ -139,7 +139,7 @@ let prog_eval_t_simple_var_wr_rd _ = show(answer) (Stream.take (run q
(* fresh prog, xg, fg, xd, fd in *) (* fresh prog, xg, fg, xd, fd in *)
(* globals_min_ido xg & *) (* globals_min_ido xg & *)
(* fg == Nat.s xg & *) (* fg == Nat.s xg & *)
(* xd == VarD (UnitT (Rd, NeverWr)) & *) (* xd == VarD (UnitT (Rd, NeverWr), UnitE) & *)
(* fd == FunD ([], SkipS) & *) (* fd == FunD ([], SkipS) & *)
(* prog == Prg ([xd; fd], CallS (VarP fg, [])) & *) (* prog == Prg ([xd; fd], CallS (VarP fg, [])) & *)
(* prog_evalo prog q }) *) (* prog_evalo prog q }) *)
@ -150,7 +150,7 @@ let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q
fresh prog, xg, fg, xd, fd in fresh prog, xg, fg, xd, fd in
globals_min_ido xg & globals_min_ido xg &
fg == Nat.s xg & fg == Nat.s xg &
xd == VarD (UnitT (Rd, NeverWr)) & xd == VarD (UnitT (Rd, NeverWr), UnitE) &
fd == FunD ([(Mode (In, NOut), UnitT (Rd, NeverWr))], ReadS (VarP 0)) & fd == FunD ([(Mode (In, NOut), UnitT (Rd, NeverWr))], ReadS (VarP 0)) &
prog == Prg ([xd; fd], CallS (VarP fg, [PathE (VarP xg)])) & prog == Prg ([xd; fd], CallS (VarP fg, [PathE (VarP xg)])) &
prog_evalo prog q }) prog_evalo prog q })
@ -162,8 +162,8 @@ let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q
globals_min_ido xg & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, NeverWr)) & xd == VarD (UnitT (Rd, NeverWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, NeverWr))) & yd == VarD (RefT (Rf, UnitT (Rd, NeverWr)), RefE xg) &
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))], fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
ReadS (DerefP (VarP 0))) & ReadS (DerefP (VarP 0))) &
prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@ -176,8 +176,8 @@ let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q
globals_min_ido xg & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (NRd, AlwaysWr)) & xd == VarD (UnitT (NRd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) &
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@ -190,8 +190,8 @@ let prog_eval_t_simple_call_wr_rd _ = show(answer) (Stream.take (run q
globals_min_ido xg & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (NRd, MayWr)) & xd == VarD (UnitT (NRd, MayWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (NRd, MayWr))) & yd == VarD (RefT (Rf, UnitT (NRd, MayWr)), RefE xg) &
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
SeqS (WriteS (DerefP (VarP 0)), SeqS (WriteS (DerefP (VarP 0)),
ReadS (DerefP (VarP 0)))) & ReadS (DerefP (VarP 0)))) &
@ -205,8 +205,8 @@ let prog_eval_t_simple_call_fbd_wr _ = show(answer) (Stream.take (run q
globals_min_ido xg & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, MayWr)) & xd == VarD (UnitT (Rd, MayWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, MayWr))) & yd == VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE xg) &
fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))], fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@ -219,8 +219,8 @@ let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q
globals_min_ido xg & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (NRd, AlwaysWr)) & xd == VarD (UnitT (NRd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) &
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@ -233,8 +233,8 @@ let prog_eval_t_simple_call_ref_fbd_wr _ = show(answer) (Stream.take (run q
globals_min_ido xg & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, AlwaysWr)) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))], fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
@ -248,8 +248,8 @@ let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q
globals_min_ido xg & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (NRd, AlwaysWr)) & xd == VarD (UnitT (NRd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) &
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
@ -265,8 +265,8 @@ let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
f2g == Nat.s fg & f2g == Nat.s fg &
xd == VarD (UnitT (Rd, AlwaysWr)) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & 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 (NRd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))], f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
@ -283,8 +283,8 @@ let prog_eval_t_call_in_call_rec _ = show(answer) (Stream.take (run q
globals_min_ido xg & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, AlwaysWr)) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & 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 (NRd, AlwaysWr)))],
SeqS (CallS (VarP fg, [PathE (VarP 0)]), SeqS (CallS (VarP fg, [PathE (VarP 0)]),
WriteS (DerefP (VarP 0)))) & WriteS (DerefP (VarP 0)))) &
@ -300,8 +300,8 @@ let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
f2g == Nat.s fg & f2g == Nat.s fg &
xd == VarD (UnitT (Rd, AlwaysWr)) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & 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 (NRd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
f2d == FunD ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))], f2d == FunD ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))],
@ -318,8 +318,8 @@ let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q
globals_min_ido xg & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, AlwaysWr)) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & 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, NeverWr)))],
SeqS (WriteS (VarP xg), SeqS (WriteS (VarP xg),
ReadS (DerefP (VarP 0)))) & ReadS (DerefP (VarP 0)))) &
@ -337,10 +337,10 @@ let prog_eval_t_call_with_rd_wr_2_args _ = show(answer) (Stream.take (run q
x2g == Nat.s yg & x2g == Nat.s yg &
y2g == Nat.s x2g & y2g == Nat.s x2g &
fg == Nat.s y2g & fg == Nat.s y2g &
xd == VarD (UnitT (Rd, AlwaysWr)) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
x2d == VarD (UnitT (Rd, AlwaysWr)) & x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) &
fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr))); fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)));
(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))], (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
SeqS (ReadS (DerefP (VarP 0)), SeqS (ReadS (DerefP (VarP 0)),
@ -375,14 +375,14 @@ let prog_eval_t_call_with_dif_mods_cp _ = show(answer) (Stream.take (run q
x4g == Nat.s y3g & x4g == Nat.s y3g &
y4g == Nat.s x4g & y4g == Nat.s x4g &
fg == Nat.s y4g & fg == Nat.s y4g &
xd == VarD (UnitT (Rd, AlwaysWr)) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
x2d == VarD (UnitT (Rd, AlwaysWr)) & x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) &
x3d == VarD (UnitT (Rd, AlwaysWr)) & x3d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x3g) &
x4d == VarD (UnitT (Rd, AlwaysWr)) & x4d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x4g) &
seqo [ReadS (DerefP (VarP 1)); seqo [ReadS (DerefP (VarP 1));
ReadS (DerefP (VarP 3)); ReadS (DerefP (VarP 3));
WriteS (DerefP (VarP 1)); WriteS (DerefP (VarP 1));
@ -434,14 +434,14 @@ let prog_eval_t_call_with_dif_mods_rf _ = show(answer) (Stream.take (run q
x4g == Nat.s y3g & x4g == Nat.s y3g &
y4g == Nat.s x4g & y4g == Nat.s x4g &
fg == Nat.s y4g & fg == Nat.s y4g &
xd == VarD (UnitT (Rd, AlwaysWr)) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
x2d == VarD (UnitT (Rd, AlwaysWr)) & x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) &
x3d == VarD (UnitT (Rd, AlwaysWr)) & x3d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x3g) &
x4d == VarD (UnitT (Rd, AlwaysWr)) & x4d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x4g) &
seqo [ReadS (DerefP (VarP 1)); seqo [ReadS (DerefP (VarP 1));
ReadS (DerefP (VarP 3)); ReadS (DerefP (VarP 3));
WriteS (DerefP (VarP 2)); WriteS (DerefP (VarP 2));
@ -477,8 +477,8 @@ let prog_cp_cap_synt_t_simple_call_ref_wr _ = show(answerCpCap) (Stream.take (ru
globals_min_ido xg & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, AlwaysWr)) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & 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 (NRd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@ -492,8 +492,8 @@ let prog_cp_cap_synt_t_simple_call_ref_wr' _ = show(answerCpCap) (Stream.take (r
globals_min_ido xg & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, AlwaysWr)) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (rd_cap, wr_cap)))], fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (rd_cap, wr_cap)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) & prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@ -506,8 +506,8 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr _ = show(answerCpCap) (Stream.take
globals_min_ido xg & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, AlwaysWr)) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & 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 (NRd, AlwaysWr)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
@ -522,8 +522,8 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak
globals_min_ido xg & globals_min_ido xg &
yg == Nat.s xg & yg == Nat.s xg &
fg == Nat.s yg & fg == Nat.s yg &
xd == VarD (UnitT (Rd, AlwaysWr)) & xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (rd_cap, wr_cap)))], fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (rd_cap, wr_cap)))],
WriteS (DerefP (VarP 0))) & WriteS (DerefP (VarP 0))) &
prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]), prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
@ -561,14 +561,14 @@ let prog_eval_t_presentation_simple_tp _ = show(answer) (Stream.take (run q
wg == Nat.s fg & wg == Nat.s fg &
gg == Nat.s wg & gg == Nat.s wg &
rg == Nat.s gg & rg == Nat.s gg &
xbd == VarD (UnitT (Rd, AlwaysWr)) & xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) &
ybd == VarD (UnitT (Rd, AlwaysWr)) & ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) &
zbd == VarD (UnitT (Rd, AlwaysWr)) & zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) &
kbd == VarD (UnitT (Rd, AlwaysWr)) & kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) &
seqo [ReadS (DerefP (VarP 0)); seqo [ReadS (DerefP (VarP 0));
WriteS (DerefP (VarP 0)); WriteS (DerefP (VarP 0));
ReadS (DerefP (VarP 1))] fstmts & ReadS (DerefP (VarP 1))] fstmts &
@ -635,14 +635,14 @@ let prog_synt_t_presentation_simple_tp _ = show(answerCpCapList) (Stream.take (r
wg == Nat.s fg & wg == Nat.s fg &
gg == Nat.s wg & gg == Nat.s wg &
rg == Nat.s gg & rg == Nat.s gg &
xbd == VarD (UnitT (Rd, AlwaysWr)) & xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) &
ybd == VarD (UnitT (Rd, AlwaysWr)) & ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) &
zbd == VarD (UnitT (Rd, AlwaysWr)) & zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) &
kbd == VarD (UnitT (Rd, AlwaysWr)) & kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) & kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) &
seqo [ReadS (DerefP (VarP 0)); seqo [ReadS (DerefP (VarP 0));
WriteS (DerefP (VarP 0)); WriteS (DerefP (VarP 0));
ReadS (DerefP (VarP 1))] fstmts & ReadS (DerefP (VarP 1))] fstmts &
@ -792,27 +792,32 @@ let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q
timeE == UnitE & timeE == UnitE &
requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] & requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] &
fresh data_p, time_p, fresh data_p0, data_p1, time_p,
user_id_p, user_name_p in user_id_p, user_name_p, user_surname_p in
deref_accesso 1 0 data_p & access_deref_accesso 0 1 0 data_p0 &
access_deref_accesso 1 1 0 data_p1 &
deref_accesso 2 0 time_p & deref_accesso 2 0 time_p &
access_deref_accesso 0 0 0 user_id_p & access_deref_accesso 0 0 0 user_id_p &
access_deref_accesso 1 0 0 user_name_p & access_deref_accesso 1 0 0 user_name_p &
seqo [ReadS data_p; access_deref_accesso 2 0 0 user_surname_p &
WriteS data_p; seqo [ReadS data_p0;
ReadS data_p1;
WriteS data_p0;
WriteS data_p1;
ReadS user_name_p; ReadS user_name_p;
WriteS user_name_p] sendBranchStmts & WriteS user_name_p] sendBranchStmts &
seqo [ChoiceS (sendBranchStmts, SkipS); seqo [sendBranchStmts; (* TMP *)
(* TODO: FIXME *)
(* ChoiceS (sendBranchStmts, SkipS); *)
WriteS time_p; WriteS time_p;
ReadS (VarP 0) ReadS data_p0;
(* ReadS data_p0; *) ReadS data_p1;
(* ReadS data_p1; *) ReadS time_p;
(* ReadS time_p; *) ReadS user_id_p;
(* ReadS user_id_p; *) ReadS user_name_p;
(* ReadS user_name_p; *) ReadS user_surname_p] sendStmts &
(* ReadS user_surname_p *)
] sendStmts &
(* sendStmts == SkipS & *) (* sendStmts == SkipS & *)
sendD == FunD ([(Mode (In, NOut), requestArgsT)], sendStmts) & sendD == FunD ([(Mode (In, NOut), requestArgsT)], sendStmts) &
@ -823,15 +828,18 @@ let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q
seqo [ seqo [
CallS (VarP sendFID, [PathE (VarP requestVID)]); CallS (VarP sendFID, [PathE (VarP requestVID)]);
WriteS time_gp; WriteS time_gp;
ChoiceS (ReadS user_name_gp, (* TODO: FIXME *)
ReadS user_surname_gp); (* ChoiceS (ReadS user_name_gp, *)
(* ReadS user_surname_gp); *)
ReadS user_name_gp; (* TMP *)
ReadS user_surname_gp; (* TMP *)
ReadS time_gp ReadS time_gp
] stmts & ] stmts &
prog == Prg ([ prog == Prg ([
VarD userT; VarD (userT, userE);
VarD dataT; VarD (dataT, dataE);
VarD timeT; VarD (timeT, timeE);
VarD requestT; VarD (requestT, requestE);
sendD sendD
], ],
stmts stmts
@ -876,9 +884,12 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take (
access_deref_accesso 2 0 0 user_surname_p & access_deref_accesso 2 0 0 user_surname_p &
seqo [ReadS data_p; seqo [ReadS data_p;
WriteS data_p; WriteS data_p;
ReadS user_name_p; ReadS user_name_p;
WriteS user_name_p] sendBranchStmts & WriteS user_name_p] sendBranchStmts &
seqo [ChoiceS (sendBranchStmts, SkipS); seqo [sendBranchStmts; (* TMP *)
(* TODO: FIXME *)
(* ChoiceS (sendBranchStmts, SkipS); *)
WriteS time_p; WriteS time_p;
ReadS (VarP 0) ReadS (VarP 0)
] sendStmts & ] sendStmts &
@ -892,16 +903,18 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take (
seqo [ seqo [
CallS (VarP sendFID, [PathE (VarP requestVID)]); CallS (VarP sendFID, [PathE (VarP requestVID)]);
WriteS time_gp; WriteS time_gp;
ChoiceS (ReadS user_name_gp, (* TODO: FIXME *)
ReadS user_surname_gp); (* ChoiceS (ReadS user_name_gp, *)
(* ReadS user_surname_gp); *)
ReadS user_name_gp; (* TMP *)
ReadS user_surname_gp; (* TMP *) ReadS user_surname_gp; (* TMP *)
ReadS time_gp ReadS time_gp
] stmts & ] stmts &
prog == Prg ([ prog == Prg ([
VarD userT; VarD (userT, userE);
VarD dataT; VarD (dataT, dataE);
VarD timeT; VarD (timeT, timeE);
VarD requestT; VarD (requestT, requestE);
sendD sendD
], ],
stmts stmts
@ -1018,8 +1031,9 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
ReadS sb_access3] ReadS sb_access3]
sendFBranch & sendFBranch &
seqo [ChoiceS (sendFBranch, SkipS); seqo [ChoiceS (sendFBranch, SkipS);
WriteS (VarP 0); WriteS (AccessP (VarP 0, 4));
ReadS (VarP 0)] (* TODO: read all the substructure ?? *)
ReadS (AccessP (VarP 0, 4)) (*rdS v0*)] (* FIXME: TMP, parial read, should be full *)
sendF & sendF &
fresh sa_access0, sa_access1, sa_access2, sa_access3 in fresh sa_access0, sa_access1, sa_access2, sa_access3 in
@ -1027,7 +1041,7 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
access_deref_accesso 1 1 0 sa_access1 & access_deref_accesso 1 1 0 sa_access1 &
access_deref_access_deref_accesso 0 0 0 0 sa_access2 & access_deref_access_deref_accesso 0 0 0 0 sa_access2 &
access_deref_accesso 0 1 0 sa_access3 & access_deref_accesso 0 1 0 sa_access3 &
seqo [WriteS (VarP 0); seqo [WriteS (AccessP (VarP 0, 4)) (*wrS v0*); (* FIXME: TMP, parial write, should be full *)
CallS (VarP sendID, [PathE (VarP 0)]); CallS (VarP sendID, [PathE (VarP 0)]);
CallS (VarP get_version_idID, [PathE (VarP 0)]); CallS (VarP get_version_idID, [PathE (VarP 0)]);
CallS (VarP updated_versionID, [PathE (VarP 0)]); CallS (VarP updated_versionID, [PathE (VarP 0)]);
@ -1041,13 +1055,13 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
send_allF & send_allF &
prog == Prg ([ prog == Prg ([
VarD user_utilsT; VarD (user_utilsT, user_utilsE);
VarD user_infoT; VarD (user_infoT, user_infoE);
VarD userT; VarD (userT, userE);
VarD versionT; VarD (versionT, versionE);
VarD utilsT; VarD (utilsT, utilsE);
VarD uT_r_aw; (* data *) VarD (uT_r_aw, UnitE); (* data *)
VarD requestT; VarD (requestT, requestE);
FunD ([moded_requestT], get_version_idF); FunD ([moded_requestT], get_version_idF);
FunD ([moded_requestT], updated_versionF); FunD ([moded_requestT], updated_versionF);
FunD ([moded_requestT], sendF); FunD ([moded_requestT], sendF);
@ -1303,7 +1317,8 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
sendFBranch & sendFBranch &
seqo [ChoiceS (sendFBranch, SkipS); seqo [ChoiceS (sendFBranch, SkipS);
WriteS (AccessP (VarP 0, 4)); WriteS (AccessP (VarP 0, 4));
ReadS (VarP 0)] (* TODO: read all the substructure ?? *)
ReadS (AccessP (VarP 0, 4)) (*rdS v0*)] (* FIXME: TMP, parial read, should be full *)
sendF & sendF &
fresh sa_access0, sa_access1, sa_access2, sa_access3 in fresh sa_access0, sa_access1, sa_access2, sa_access3 in
@ -1311,10 +1326,11 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
access_deref_accesso 1 1 0 sa_access1 & access_deref_accesso 1 1 0 sa_access1 &
access_deref_access_deref_accesso 0 0 0 0 sa_access2 & access_deref_access_deref_accesso 0 0 0 0 sa_access2 &
access_deref_accesso 0 1 0 sa_access3 & access_deref_accesso 0 1 0 sa_access3 &
seqo [WriteS (AccessP (VarP 0, 4)); seqo [WriteS (AccessP (VarP 0, 4)) (*wrS v0*); (* FIXME: TMP, parial write, should be full *)
CallS (VarP sendID, [PathE (VarP 0)]); CallS (VarP sendID, [PathE (VarP 0)]);
CallS (VarP get_version_idID, [PathE (VarP 0)]); CallS (VarP get_version_idID, [PathE (VarP 0)]);
CallS (VarP updated_versionID, [PathE (VarP 0)]); CallS (VarP updated_versionID, [PathE (VarP 0)]);
(* TODO: read all the substructure ?? *)
WriteS sa_access0; WriteS sa_access0;
WriteS sa_access1; WriteS sa_access1;
ChoiceS ( ChoiceS (
@ -1336,13 +1352,13 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
(* [gvi_c0; gvi_c1; gvi_c2; gvi_c3; gvi_c4; gvi_c5] & *) (* [gvi_c0; gvi_c1; gvi_c2; gvi_c3; gvi_c4; gvi_c5] & *)
prog == Prg ([ prog == Prg ([
VarD user_utilsT; VarD (user_utilsT, user_utilsE);
VarD user_infoT; VarD (user_infoT, user_infoE);
VarD userT; VarD (userT, userE);
VarD versionT; VarD (versionT, versionE);
VarD utilsT; VarD (utilsT, utilsE);
VarD uT_r_aw; (* data *) VarD (uT_r_aw, UnitE); (* data *)
VarD requestT; VarD (requestT, requestE);
(* FunD ([mrT'], get_version_idF); *) (* FunD ([mrT'], get_version_idF); *)
(* FunD ([mrT'], updated_versionF); *) (* FunD ([mrT'], updated_versionF); *)
(* FunD ([mrT'], sendF); *) (* FunD ([mrT'], sendF); *)