mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-06-11 03:38:15 +00:00
Compare commits
No commits in common. "1bacb6dfd77072ae74c1eb4fe7d05996c9d1e818" and "0be430a59b3dc4d0553a719b8c4c8cf04daed556" have entirely different histories.
1bacb6dfd7
...
0be430a59b
3 changed files with 443 additions and 486 deletions
|
|
@ -21,7 +21,7 @@ struct
|
|||
type atype = UnitT of read_cap * write_cap
|
||||
| RefT of copy_cap * atype
|
||||
| TupleT of atype list
|
||||
| FunT of (mode * atype) list (* TODO: declaration id for ease of impl / performance instead (?) *)
|
||||
| FunT of data (* declaration id for ease of impl (?) *)
|
||||
|
||||
type mtype = mode * atype
|
||||
|
||||
|
|
@ -30,8 +30,7 @@ struct
|
|||
(* | RefE *)
|
||||
| TupleE of expr list
|
||||
|
||||
type stmt = SkipS
|
||||
| CallS of path * expr list
|
||||
type stmt = CallS of path * expr list
|
||||
| WriteS of path
|
||||
| ReadS of path
|
||||
| SeqS of stmt * stmt
|
||||
|
|
@ -53,22 +52,20 @@ struct
|
|||
(* exception Incompatible_path_and_mem *)
|
||||
(* exception Incompatible_path_and_type_for_tag *)
|
||||
exception Typing_error of string
|
||||
exception Eval_error of string
|
||||
exception Cant_fold3_error
|
||||
|
||||
(* value model & memory model *)
|
||||
|
||||
type deepvalue = ZeroDV
|
||||
| SmthDV
|
||||
| BotDV
|
||||
| FunDV of ((* data list * *) stmt) list
|
||||
| FunDV of (* data list * *) stmt
|
||||
| RefDV of deepvalue
|
||||
| TupleDV of deepvalue list
|
||||
|
||||
type value = ZeroV
|
||||
| SmthV
|
||||
| BotV
|
||||
| FunV of ((* data list * *) stmt) list
|
||||
| FunV of (* data list * *) stmt
|
||||
| RefV of memid
|
||||
| TupleV of value list
|
||||
|
||||
|
|
@ -76,31 +73,19 @@ struct
|
|||
|
||||
(* --- *)
|
||||
|
||||
type mem = value list * memid (* NOTE: memory and first free elem *)
|
||||
type mem = (memid * value) list * memid (* NOTE: memory and first free elem *)
|
||||
type types = (data * atype) list
|
||||
type vals = (data * memid) list
|
||||
type state = mem * types * vals
|
||||
|
||||
(* --- *)
|
||||
|
||||
(* - utils *)
|
||||
|
||||
let rec list_replace (xs : 'a list) (id : int) (y : 'a) : 'a list = match xs, id with
|
||||
| _ :: xs, 0 -> y :: xs
|
||||
| x :: xs, _ -> x :: list_replace xs (id - 1) y
|
||||
| [], _ -> raise Not_found
|
||||
|
||||
(* NOTE: old variant with assoc array *)
|
||||
(* let mem_get (mem : mem) (id : memid) : value = List.assoc id (fst mem) *)
|
||||
(* let mem_add (mem : mem) (v : value) : mem * memid = *)
|
||||
(* (((snd mem, v) :: fst mem, snd mem + 1), snd mem) *)
|
||||
(* let mem_set (mem : mem) (id : memid) (v : value) : mem = *)
|
||||
(* ((id, v) :: fst mem, snd mem) *)
|
||||
let mem_get (mem : mem) (id : memid) : value = List.nth (fst mem) id
|
||||
(* TODO: FIXME: use list_replace for memory instead ?? *)
|
||||
let mem_get (mem : mem) (id : memid) : value = List.assoc id (fst mem)
|
||||
let mem_add (mem : mem) (v : value) : mem * memid =
|
||||
((v :: fst mem, snd mem + 1), snd mem)
|
||||
(((snd mem, v) :: fst mem, snd mem + 1), snd mem)
|
||||
let mem_set (mem : mem) (id : memid) (v : value) : mem =
|
||||
(list_replace (fst mem) id v, snd mem)
|
||||
((id, v) :: fst mem, snd mem)
|
||||
|
||||
let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with
|
||||
| ZeroV -> ZeroDV
|
||||
|
|
@ -140,11 +125,12 @@ struct
|
|||
|
||||
(* --- eval rules --- *)
|
||||
|
||||
(* TODO: FIXME: check if this foldl or foldr *)
|
||||
let rec list_foldl3 f (acc : 'a) (xs : 'b list) (ys : 'c list) (zs : 'd list) : 'a = match xs, ys, zs with
|
||||
| x :: xs, y :: ys, z :: zs -> list_foldl3 f (f acc x y z) xs ys zs
|
||||
| [], [], [] -> acc
|
||||
| _, _, _ -> raise Cant_fold3_error
|
||||
(* - utils *)
|
||||
|
||||
let rec list_replace (xs : 'a list) (id : int) (y : 'a) : 'a list = match xs, id with
|
||||
| _ :: xs, 0 -> y :: xs
|
||||
| x :: xs, _ -> x :: list_replace xs (id - 1) y
|
||||
| [], _ -> raise Not_found
|
||||
|
||||
(* - value construction *)
|
||||
|
||||
|
|
@ -182,54 +168,17 @@ struct
|
|||
if is_trivial_v u && is_trivial_v v
|
||||
then (if u == v then u else BotV)
|
||||
else match u, v with
|
||||
| FunV ustmts, FunV vstmts -> FunV (ustmts @ vstmts)
|
||||
(* TODO: FIXME: combining semanticsfor funcitons statements *)
|
||||
| FunV s, FunV t -> if s == t then u else raise @@ Typing_error "valcomb: fun"
|
||||
| RefV a, RefV b -> if a == b then u else raise @@ Typing_error "valcomb: ref"
|
||||
| TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs)
|
||||
| _, _ -> raise @@ Typing_error "valcomb"
|
||||
|
||||
let rec memcomb (m : mem) (n : mem) : mem =
|
||||
if snd m != snd n
|
||||
then raise @@ Typing_error "memcomb"
|
||||
else (List.map2 valcomb (fst m) (fst n), snd m)
|
||||
|
||||
(* - expression evaluation *)
|
||||
|
||||
let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with
|
||||
| UnitE -> ZeroV
|
||||
| PathE p -> pathval mem vals p
|
||||
| TupleE es -> TupleV (List.map (exprval mem vals) es)
|
||||
|
||||
(* - expression typing *)
|
||||
|
||||
let rec exprtype (types : types) (e : expr) : atype = match e with
|
||||
| UnitE -> UnitT (Rd, NeverWr)
|
||||
| PathE p -> pathtype types p
|
||||
| TupleE es -> TupleT (List.map (exprtype types) es)
|
||||
|
||||
(* - context initialization *)
|
||||
|
||||
(* let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = match t, v with *)
|
||||
|
||||
(* TODO: check new in vars *)
|
||||
let add_decl (state : state) (x : data) (d : decl) : state =
|
||||
match state with (mem, types, vals) -> match d with
|
||||
| VarD (t, e) -> let v = exprval mem vals e in
|
||||
let (mem', v') = valcopy mem v t in
|
||||
let (mem'', id) = mem_add mem' v' in
|
||||
(mem'', (x, t) :: types, (x, id) :: vals)
|
||||
| FunD (ts, s) -> let (mem', id) = mem_add mem (FunV [s]) in
|
||||
(mem', (x, FunT ts) :: types, (x, id) :: vals)
|
||||
|
||||
let empty_state : state = (([], 0), [], [])
|
||||
|
||||
(* TODO: better way ??? *)
|
||||
let globals_min_id : data = 1000
|
||||
|
||||
let prog_init (prog : prog) : state =
|
||||
match prog with (decls, _) -> fst @@ List.fold_left (* TODO: FIXME: check x's order *)
|
||||
(fun (st, x) d -> (add_decl st x d, x + 1))
|
||||
(empty_state, globals_min_id)
|
||||
decls
|
||||
(* TODO: func for list memory, not assoc list *)
|
||||
(* let rec memcomb (m : mem) (n : mem) : mem = *)
|
||||
(* if snd m != snd n *)
|
||||
(* then raise @@ Typing_error "memcomb" *)
|
||||
(* else (List.map2 valcomb (fst m) (fst n), snd m) *)
|
||||
|
||||
(* - call values spoil *)
|
||||
|
||||
|
|
@ -239,7 +188,7 @@ struct
|
|||
(c : copy_cap) : bool =
|
||||
(r != Rd || v == ZeroV) &&
|
||||
(r != Rd || fst m == In) &&
|
||||
(snd m != Out || w == AlwaysWr) &&
|
||||
(o != Out || w == AlwaysWr) &&
|
||||
(* TODO: check *)
|
||||
((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr) &&
|
||||
is_trivial_v v
|
||||
|
|
@ -247,161 +196,262 @@ struct
|
|||
let rec valspoil (mem : mem) (v : value) (t : atype)
|
||||
(u : atype) (m : mode) (c : copy_cap)
|
||||
: mem * value = match t, u, v with
|
||||
| UnitT (r, w), UnitT (r', w'), _ ->
|
||||
if not @@ is_trivial_v v
|
||||
then raise @@ Typing_error "valspoil: unit, not trivial"
|
||||
else if not @@ is_correct_tags v r w r' w' m c
|
||||
then raise @@ Typing_error "valspoil: unit, not correct"
|
||||
else if snd m == NOut && c == Rf && (w == AlwaysWr || w == MayWr)
|
||||
then (mem, BotV)
|
||||
else if snd m == Out && w == AlwaysWr
|
||||
then (mem, ZeroV)
|
||||
else (mem, v)
|
||||
| UnitT (r, w), UnitT (r', w'), _ -> (* TODO FIXME *) raise Not_found
|
||||
| FunT ts, FunT us, FunV _ -> if ts == us then (mem, v) else raise @@ Typing_error "valspoil: fun"
|
||||
| RefT (ct, t), RefT (cu, u), RefV id ->
|
||||
let (mem', v') = valspoil mem (mem_get mem id) t u m ct in
|
||||
(mem_set mem id v', RefV id)
|
||||
| TupleT ts, TupleT us, TupleV vs ->
|
||||
let folder = fun (mem, vs') t u v ->
|
||||
let (mem', v') = valspoil mem v t u m c in (mem', v' :: vs') in
|
||||
let (mem', vs') = list_foldl3 folder (mem, []) ts us vs in
|
||||
(mem', TupleV vs')
|
||||
| TupleT ts, TupleT us, TupleV vs -> (* TODO FIXME *) raise Not_found
|
||||
| _, _, _ -> raise @@ Typing_error "valspoil"
|
||||
|
||||
(* full spoil *)
|
||||
|
||||
let rec argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
|
||||
match state with (mem, types, vals) ->
|
||||
let x = pathvar p in
|
||||
let id = List.assoc x vals in
|
||||
let b = pathval mem vals p in
|
||||
let t' = pathtype types p in
|
||||
let (mem', b') = valspoil mem b t t' m Rf in
|
||||
let (mem'', v'') = valupd mem' (mem_get mem' id) p b' in
|
||||
mem_set mem'' id v''
|
||||
|
||||
let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
|
||||
match state with (mem, types, vals) -> match e, t with
|
||||
| UnitE, UnitT _ -> mem
|
||||
| PathE p, t -> argsspoilp state m t p
|
||||
| TupleE es, TupleT ts -> List.fold_left2
|
||||
(fun mem' t' e' -> argsspoile (mem', types, vals) m t' e')
|
||||
mem ts es
|
||||
| _, _ -> raise @@ Typing_error "valspoile"
|
||||
|
||||
(* - funciton argument addition *)
|
||||
|
||||
let addarg (state : state) (x : data) (t : atype) (e : expr) : state =
|
||||
match state with (mem, types, vals) ->
|
||||
let v = exprval mem vals e in
|
||||
(* let t' = pathtype types p in *)
|
||||
let (mem', v') = valcopy mem v t in
|
||||
let (mem'', id) = mem_add mem' v in
|
||||
(mem', (x, t) :: types, (x, id) :: vals)
|
||||
|
||||
(* - 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) = *)
|
||||
|
||||
(* - statement evaluation *)
|
||||
|
||||
let rec stmt_eval (state : state) (s : stmt) : state =
|
||||
match state with (mem, types, vals) -> match s with
|
||||
(* TODO: FIXME: Add memoisation *)
|
||||
| SkipS -> state
|
||||
| CallS (f, es) -> let v = pathval mem vals f in
|
||||
let t = pathtype types f in
|
||||
let types' : types = [] in
|
||||
let vals' : vals = [] in
|
||||
(match v, t with
|
||||
| FunV (* xs, *) fstmts (* ) *), FunT ts ->
|
||||
(* TODO: memoisation of the called functions *)
|
||||
let (state_with_args, _) = List.fold_left2 (* TODO: FIXME: check x's order *)
|
||||
(fun (st, x) (m, t) p -> (addarg st x t p, x + 1))
|
||||
((mem, types', vals'), 0) ts es in
|
||||
(* NOTE: same x's, so can use same args for all the statements *)
|
||||
let _states_evaled = List.map (stmt_eval state_with_args) fstmts in
|
||||
let mem_spoiled = List.fold_left2
|
||||
(fun mem (m, t) e -> argsspoile (mem, types, vals) m t e)
|
||||
mem ts es in
|
||||
(mem_spoiled, types, vals)
|
||||
| _, _ -> raise @@ Eval_error "call: function")
|
||||
| WriteS p -> (match pathtype types p with
|
||||
| UnitT (_, w) ->
|
||||
if w == NeverWr
|
||||
then raise @@ Eval_error "write: write tag"
|
||||
else let x = pathvar p in
|
||||
let id = List.assoc x vals in
|
||||
let (mem', v') = valupd mem (mem_get mem id) p ZeroV in
|
||||
(mem_set mem' id v', types, vals)
|
||||
| _ -> raise @@ Eval_error "write: type")
|
||||
| ReadS p -> if pathval mem vals p != ZeroV
|
||||
then raise @@ Eval_error "read"
|
||||
else state
|
||||
| SeqS (sl, sr) -> let statel = stmt_eval state sl in
|
||||
stmt_eval statel sr
|
||||
| ChoiceS (sl, sr) -> let statel = stmt_eval state sl in
|
||||
let stater = stmt_eval state sr in
|
||||
match statel with (meml, typesl, valsl) ->
|
||||
match stater with (memr, typesr, valsr) ->
|
||||
if typesl != typesr || valsl != valsr
|
||||
then raise @@ Eval_error "choice"
|
||||
else (memcomb meml memr, typesl, valsl)
|
||||
|
||||
(* --- program execution --- *)
|
||||
|
||||
let prog_eval (prog : prog) : state =
|
||||
match prog with (decls, s) ->
|
||||
let init_state = prog_init prog in
|
||||
stmt_eval init_state s
|
||||
|
||||
let prog_eval_noret (prog : prog) : unit =
|
||||
ignore @@ prog_eval prog
|
||||
|
||||
(* --- tests --- *)
|
||||
|
||||
(* - tests without functions *)
|
||||
|
||||
let%expect_test "empty" =
|
||||
prog_eval_noret ([], SkipS);
|
||||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
let%expect_test "simple var" =
|
||||
prog_eval_noret ([VarD (UnitT (Rd, MayWr), UnitE)], ReadS (VarP globals_min_id));
|
||||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
let%expect_test "simple var, no read" =
|
||||
try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], ReadS (VarP globals_min_id));
|
||||
[%expect.unreachable]);
|
||||
with Eval_error msg -> Printf.printf "%s" msg;
|
||||
[%expect {| read |}]
|
||||
|
||||
(* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
|
||||
|
||||
(* --- tests --- *)
|
||||
(* let rec argsspoil (* full spoil *) *)
|
||||
|
||||
(* let rwi_value : tag = (Rd, AlwaysWr, Cp, In, NOut) *)
|
||||
(* let rmwi_value : tag = (Rd, MayWr, Cp, In, NOut) *)
|
||||
(* let ri_value : tag = (Rd, NeverWr, Cp, In, NOut) *)
|
||||
(* let wi_value : tag = (NRd, AlwaysWr, Cp, In, NOut) *)
|
||||
(* let mwi_value : tag = (NRd, MayWr, Cp, In, NOut) *)
|
||||
(* let i_value : tag = (NRd, NeverWr, Cp, In, NOut) *)
|
||||
(* let rwi_ref : tag = (Rd, AlwaysWr, Rf, In, NOut) *)
|
||||
(* let rmwi_ref : tag = (Rd, MayWr, Rf, In, NOut) *)
|
||||
(* let ri_ref : tag = (Rd, NeverWr, Rf, In, NOut) *)
|
||||
(* let wi_ref : tag = (NRd, AlwaysWr, Rf, In, NOut) *)
|
||||
(* let mwi_ref : tag = (NRd, MayWr, Rf, In, NOut) *)
|
||||
(* let i_ref : tag = (NRd, NeverWr, Rf, In, NOut) *)
|
||||
(* --- *)
|
||||
|
||||
let rec list_zip_with f xs ys = match xs, ys with (* TODO: alternative from stdlib *)
|
||||
| x :: xs, y :: ys -> f x y :: list_zip_with f xs ys
|
||||
| _, _ -> []
|
||||
|
||||
(* --- combination --- *)
|
||||
|
||||
let value_combine (left : value) (right : value) : value = match left, right with
|
||||
| UnitV, UnitV -> UnitV
|
||||
| BotV, BotV -> BotV
|
||||
| _, _ -> UndefV (* NOTE: should be expanded in relational interpreter to not use ineq (?) *)
|
||||
|
||||
let memory_combine (left : value list) (right : value list) : value list =
|
||||
list_zip_with value_combine left right
|
||||
|
||||
let state_combine (left : state) (right : state) : state = match left, right with
|
||||
(lenv, lmem, lmem_len, lvisited), (renv, rmem, rmem_len, rvisited) ->
|
||||
if lenv != renv || lmem_len != rmem_len then raise Incompatible_states
|
||||
else (lenv, memory_combine lmem rmem, lmem_len, List.append lvisited rvisited)
|
||||
(* TODO: union visited lists instead ? *)
|
||||
|
||||
(* --- tag accessors --- *)
|
||||
|
||||
let is_read (tag : tag) : bool = match tag with
|
||||
| (Rd, _, _, _, _) -> true
|
||||
| _ -> false
|
||||
|
||||
let is_always_write (tag : tag) : bool = match tag with
|
||||
| (_, AlwaysWr, _, _, _) -> true
|
||||
| _ -> false
|
||||
|
||||
let is_may_write (tag : tag) : bool = match tag with
|
||||
| (_, AlwaysWr, _, _, _) -> true
|
||||
| (_, MayWr, _, _, _) -> true
|
||||
| _ -> false
|
||||
|
||||
let is_never_write (tag : tag) : bool = match tag with
|
||||
| (_, NeverWr, _, _, _) -> true
|
||||
| _ -> false
|
||||
|
||||
let is_copy (tag : tag) : bool = match tag with
|
||||
| (_, _, Cp, _, _) -> true
|
||||
| _ -> false
|
||||
|
||||
let is_in (tag : tag) : bool = match tag with
|
||||
| (_, _, _, In, _) -> true
|
||||
| _ -> false
|
||||
|
||||
let is_out (tag : tag) : bool = match tag with
|
||||
| (_, _, _, _, Out) -> true
|
||||
| _ -> false
|
||||
|
||||
(* --- *)
|
||||
|
||||
let rec list_replace xs id value = match (xs, id) with
|
||||
| (_x :: xs, 0) -> value :: xs
|
||||
| (x :: xs, _n) -> x :: list_replace xs (id - 1) value
|
||||
| ([], _) -> raise Not_found
|
||||
|
||||
let inv_id (mem_len : int) (id : data) : data = mem_len - id - 1
|
||||
|
||||
(* --- path accessors --- *)
|
||||
|
||||
let rec pathtype (t : argtype) (p : path) : argtype = match t, p with
|
||||
| t, VarP x -> t
|
||||
| RefT (tag, t), DerefP p -> pathtype t p
|
||||
| TupleT ts, AccessP (p, n) -> pathtype (List.nth ts n) p
|
||||
| _, _ -> raise Incompatible_path_and_type
|
||||
|
||||
let rec pathmem (m : argmem) (p : path) : data = match m, p with
|
||||
| VarM m, VarP x -> m
|
||||
| RefM m, DerefP p -> pathmem m p
|
||||
| TupleM ms, AccessP (p, n) -> pathmem (List.nth ms n) p
|
||||
| _, _ -> raise Incompatible_path_and_mem
|
||||
|
||||
let rec pathtag (t : argtype) (p : path) : tag = match t, p with
|
||||
| RefT (tag, t), VarP x -> tag
|
||||
| RefT (tag, t), DerefP p -> pathtag t p
|
||||
| TupleT ts, AccessP (p, n) -> pathtag (List.nth ts n) p
|
||||
| _, _ -> raise Incompatible_path_and_type_for_tag
|
||||
|
||||
let rec pathvar (p : path) : data = match p with
|
||||
| VarP x -> x
|
||||
| DerefP p -> pathvar p
|
||||
| AccessP (p, n) -> pathvar p
|
||||
|
||||
let typeof (env : env) (p : path) : argtype = pathtype (snd (List.assoc (pathvar p) env)) p
|
||||
let accessmem (env : env) (p : path) : data = pathmem (fst (List.assoc (pathvar p) env)) p
|
||||
let argtag (env : env) (p : path) : tag = pathtag (snd (List.assoc (pathvar p) env)) p
|
||||
(* TODO: check indices *)
|
||||
let access_get (env : env) (mem : value list) (mem_len : data) (p : path) : value = List.nth mem @@ inv_id mem_len @@ accessmem env p
|
||||
let access_set (env : env) (mem : value list) (mem_len : data) (p : path) (value : value) : value list = list_replace mem (inv_id mem_len @@ accessmem env p) value
|
||||
|
||||
(* --- *)
|
||||
|
||||
let visited_add (state : state) (id : data) : state =
|
||||
match state with (env, mem, mem_len, visited) -> (env, mem, mem_len, id :: visited)
|
||||
|
||||
let visited_check (state : state) (id : data) : bool =
|
||||
match state with (_, _, _, visited) -> List.exists (fun i -> i == id) visited
|
||||
|
||||
(* --- *)
|
||||
|
||||
(* TODO: replacewith more useful path versions *)
|
||||
let env_get (state : state) (id : data) : (argmem * argtype) =
|
||||
match state with (env, _mem, _mem_len, _visited) -> List.assoc id env
|
||||
|
||||
let env_add (state : state) (id : data) (argmem : argmem) (argtype : argtype) : state = match state with
|
||||
(env, mem, mem_len, visited) -> let env = (id, (argmem, argtype)) :: env in
|
||||
(env, mem, mem_len, visited)
|
||||
|
||||
let mem_get (state : state) (p : path) : value = match state with
|
||||
(env, mem, mem_len, _visited) -> access_get env mem mem_len p
|
||||
|
||||
let mem_set (state : state) (p : path) (value : value) : state = match state with
|
||||
(env, mem, mem_len, visited) -> (env, access_set env mem mem_len p value, mem_len, visited)
|
||||
|
||||
let mem_add (state : state) (value : value) : state = match state with
|
||||
(env, mem, mem_len, visited) -> let mem = value :: mem in (env, mem, mem_len + 1, visited)
|
||||
|
||||
let mem_check (state : state) (p : path) : unit =
|
||||
(* TODO: use path in error instead *)
|
||||
if mem_get state p == BotV then raise @@ Incorrect_memory_access (pathvar p) else ()
|
||||
|
||||
(* --- *)
|
||||
|
||||
let arg_to_value (state : state) (arg : arg) : value = match arg with
|
||||
| RValue -> UnitV
|
||||
| LValue p -> mem_get state p
|
||||
(* TODO: FIXME: args as argmem ?? *)
|
||||
|
||||
let st_mem_len (state : state) : int =
|
||||
match state with (_, _, mem_len, _) -> mem_len
|
||||
|
||||
let check_tag_correct (tag : tag) (id : data) : unit =
|
||||
if (* (is_in tag && not (is_read tag)) || *) (* TODO: required ?? *)
|
||||
is_out tag > is_always_write tag ||
|
||||
is_read tag > is_in tag
|
||||
(* || is_copy tag && is_out tag *) (* ?? *)
|
||||
then raise @@ Invalid_argument_tag id
|
||||
else ()
|
||||
|
||||
let st_add_arg (state : state) (state_before : state)
|
||||
(id : data) (arg_tag : tag) (arg : arg) : state =
|
||||
check_tag_correct arg_tag id;
|
||||
if is_copy arg_tag
|
||||
then let state = mem_add state (arg_to_value state_before arg) in
|
||||
env_add state id arg_tag (st_mem_len state - 1)
|
||||
else match arg with
|
||||
| RValue -> raise @@ Ref_rvalue_argument id (* TODO: allow later ?? *)
|
||||
| LValue arg -> let (parent_tag, mem_id) = env_get state_before arg in
|
||||
if is_may_write arg_tag > is_always_write parent_tag (* TODO: FIXME: not updated semantics ?? *)
|
||||
then raise @@ Incorrect_const_cast id
|
||||
else if is_read arg_tag
|
||||
then env_add state id arg_tag mem_id
|
||||
(* TODO: parent state is spoiled, check that this is correct *)
|
||||
else let state_ext = env_add state id arg_tag mem_id in
|
||||
mem_set state_ext id BotV
|
||||
|
||||
(* TODO: FIXME: not enough tests on incorrect const cast (passed without ref or out check) *)
|
||||
(* TODO; FIXME: forbid duplicates, collect lists of all spoils & checks ? *)
|
||||
let st_spoil_by_args (state : state) (arg_tags : tag list) (args : data list) : state =
|
||||
match state with (env, mem, mem_len, _visited) ->
|
||||
let state_before = state in
|
||||
let spoil_folder (state : state) (tag : tag) (id : data) : state =
|
||||
let parent_tag = fst (env_get state id) in
|
||||
(* NOTE: replaced with later condition *)
|
||||
(* if is_write tag > is_write parent_tag && (not (is_copy tag) || is_out tag) then raise @@ Incorrect_const_cast idi else *)
|
||||
let state = if is_read tag then (mem_check state_before id; state) else state (* NOTE: state override *)
|
||||
in if is_never_write tag then state (* TODO: FIXME: check *)
|
||||
else match is_out tag with
|
||||
| true -> if not @@ is_always_write parent_tag then raise @@ Incorrect_const_cast id
|
||||
else mem_set state id UnitV
|
||||
| false -> if is_copy tag then state
|
||||
else if not @@ is_may_write parent_tag then raise @@ Incorrect_const_cast id (* TODO: check that may modifier correct *)
|
||||
else mem_set state id BotV
|
||||
in List.fold_left2 spoil_folder state arg_tags args
|
||||
|
||||
let list_drop n xs = List.of_seq @@ Seq.drop n @@ List.to_seq xs
|
||||
|
||||
let rec eval_stmt (state : state) (prog : fun_decl list) (stmt : stmt) : state =
|
||||
match stmt with
|
||||
| Call (f_id, args) -> let (arg_tags, _) as f_decl = List.nth prog f_id in
|
||||
let state_with_visited = if visited_check state f_id
|
||||
then state
|
||||
else let new_state_with_visited = visited_add state f_id in
|
||||
let state_fun = eval_fun new_state_with_visited prog f_decl (List.map (fun arg -> LValue arg) args) in
|
||||
(* NOTE: now memory in function is not spoiled *)
|
||||
state_fun
|
||||
in st_spoil_by_args state_with_visited arg_tags args
|
||||
| Read id -> mem_check state id; state
|
||||
| Write id -> if is_may_write @@ fst @@ env_get state id
|
||||
then mem_set state id UnitV
|
||||
else raise @@ Incorrect_const_cast id
|
||||
| Choice (xs, ys) -> let state_x = eval_body state prog xs in
|
||||
let state_y = eval_body state prog ys in
|
||||
state_combine state_x state_y
|
||||
(* TODO: FIXME: additional may write / always write checks ?? *)
|
||||
|
||||
and eval_body (state : state) (prog : fun_decl list) (body : body) : state =
|
||||
List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body
|
||||
|
||||
and eval_fun (state : state) (prog : fun_decl list) (decl : fun_decl) (args : arg list) : state =
|
||||
match decl with (arg_tags, body) ->
|
||||
match state with (env_before, mem_before, len_before, visited_before) as state_before ->
|
||||
let state : state = ([], mem_before, len_before, visited_before) in
|
||||
let (state, _) = List.fold_left2 (fun (state, id) arg_tag arg -> (st_add_arg state state_before id arg_tag arg, id + 1))
|
||||
(state, 0) arg_tags args in
|
||||
let state = eval_body state prog body in
|
||||
match state with (_env, mem, len, visited) ->
|
||||
(env_before, mem_before, len_before, visited)
|
||||
(* (env_before, list_drop (len - len_before) mem, len_before, visited) (* TODO: save some assignments ?? *) *)
|
||||
|
||||
and eval_fun_empty_args (state : state) (prog : fun_decl list) (decl : fun_decl) : state =
|
||||
match decl with (arg_tags, _) ->
|
||||
let args = List.map (fun _ -> RValue) arg_tags in
|
||||
eval_fun state prog decl args
|
||||
|
||||
let empty_state : state = ([], [], 0, [])
|
||||
|
||||
let eval_prog ((prog, main_decl) : prog) = ignore @@ eval_fun_empty_args empty_state prog main_decl
|
||||
|
||||
(* tests *)
|
||||
|
||||
let rwi_value : tag = (Rd, AlwaysWr, Cp, In, NOut)
|
||||
let rmwi_value : tag = (Rd, MayWr, Cp, In, NOut)
|
||||
let ri_value : tag = (Rd, NeverWr, Cp, In, NOut)
|
||||
let wi_value : tag = (NRd, AlwaysWr, Cp, In, NOut)
|
||||
let mwi_value : tag = (NRd, MayWr, Cp, In, NOut)
|
||||
let i_value : tag = (NRd, NeverWr, Cp, In, NOut)
|
||||
let rwi_ref : tag = (Rd, AlwaysWr, Rf, In, NOut)
|
||||
let rmwi_ref : tag = (Rd, MayWr, Rf, In, NOut)
|
||||
let ri_ref : tag = (Rd, NeverWr, Rf, In, NOut)
|
||||
let wi_ref : tag = (NRd, AlwaysWr, Rf, In, NOut)
|
||||
let mwi_ref : tag = (NRd, MayWr, Rf, In, NOut)
|
||||
let i_ref : tag = (NRd, NeverWr, Rf, In, NOut)
|
||||
|
||||
(* >> tests without functions *)
|
||||
|
||||
(* let%expect_test "empty" = *)
|
||||
(* eval_prog ([], ([], [])); *)
|
||||
(* Printf.printf "done!"; *)
|
||||
(* [%expect {| done! |}] *)
|
||||
let%expect_test "empty" =
|
||||
eval_prog ([], ([], []));
|
||||
Printf.printf "done!";
|
||||
[%expect {| done! |}]
|
||||
|
||||
(* let%expect_test "ref param in main failure" = *)
|
||||
(* try (eval_prog ([], ([i_ref], [])); *)
|
||||
|
|
|
|||
|
|
@ -13,52 +13,52 @@
|
|||
(preprocess
|
||||
(pps GT.ppx GT.ppx_all ppx_expect ppx_inline_test)))
|
||||
|
||||
; (library
|
||||
; (name tests_st)
|
||||
; (modules tests)
|
||||
; (flags (-rectypes))
|
||||
; (libraries synthesizer_st tests_f_st)
|
||||
; (inline_tests)
|
||||
; (wrapped false)
|
||||
; (preprocess
|
||||
; (pps ppx_expect ppx_inline_test)))
|
||||
(library
|
||||
(name tests_st)
|
||||
(modules tests)
|
||||
(flags (-rectypes))
|
||||
(libraries synthesizer_st tests_f_st)
|
||||
(inline_tests)
|
||||
(wrapped false)
|
||||
(preprocess
|
||||
(pps ppx_expect ppx_inline_test)))
|
||||
|
||||
; (library
|
||||
; (name tests_f_st)
|
||||
; (modules tests_f)
|
||||
; (flags (-rectypes))
|
||||
; (libraries OCanren OCanren.tester synthesizer_st)
|
||||
; (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
|
||||
; (wrapped false)
|
||||
; (preprocess
|
||||
; (pps
|
||||
; OCanren-ppx.ppx_repr
|
||||
; OCanren-ppx.ppx_deriving_reify
|
||||
; OCanren-ppx.ppx_fresh
|
||||
; GT.ppx
|
||||
; GT.ppx_all
|
||||
; OCanren-ppx.ppx_distrib
|
||||
; --
|
||||
; -pp
|
||||
; camlp5/pp5+gt+plugins+ocanren+dump.exe)))
|
||||
(library
|
||||
(name tests_f_st)
|
||||
(modules tests_f)
|
||||
(flags (-rectypes))
|
||||
(libraries OCanren OCanren.tester synthesizer_st)
|
||||
(preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
|
||||
(wrapped false)
|
||||
(preprocess
|
||||
(pps
|
||||
OCanren-ppx.ppx_repr
|
||||
OCanren-ppx.ppx_deriving_reify
|
||||
OCanren-ppx.ppx_fresh
|
||||
GT.ppx
|
||||
GT.ppx_all
|
||||
OCanren-ppx.ppx_distrib
|
||||
--
|
||||
-pp
|
||||
camlp5/pp5+gt+plugins+ocanren+dump.exe)))
|
||||
|
||||
; (library
|
||||
; (name synthesizer_st)
|
||||
; (modules synthesizer)
|
||||
; (flags
|
||||
; ; (-dsource)
|
||||
; (:standard -rectypes))
|
||||
; (libraries OCanren OCanren.tester)
|
||||
; (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
|
||||
; (wrapped false)
|
||||
; (preprocess
|
||||
; (pps
|
||||
; OCanren-ppx.ppx_repr
|
||||
; OCanren-ppx.ppx_deriving_reify
|
||||
; OCanren-ppx.ppx_fresh
|
||||
; GT.ppx
|
||||
; GT.ppx_all
|
||||
; OCanren-ppx.ppx_distrib
|
||||
; --
|
||||
; -pp
|
||||
; camlp5/pp5+gt+plugins+ocanren+dump.exe)))
|
||||
(library
|
||||
(name synthesizer_st)
|
||||
(modules synthesizer)
|
||||
(flags
|
||||
; (-dsource)
|
||||
(:standard -rectypes))
|
||||
(libraries OCanren OCanren.tester)
|
||||
(preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
|
||||
(wrapped false)
|
||||
(preprocess
|
||||
(pps
|
||||
OCanren-ppx.ppx_repr
|
||||
OCanren-ppx.ppx_deriving_reify
|
||||
OCanren-ppx.ppx_fresh
|
||||
GT.ppx
|
||||
GT.ppx_all
|
||||
OCanren-ppx.ppx_distrib
|
||||
--
|
||||
-pp
|
||||
camlp5/pp5+gt+plugins+ocanren+dump.exe)))
|
||||
|
|
|
|||
|
|
@ -120,12 +120,11 @@
|
|||
Prod(
|
||||
`stmt`,
|
||||
{
|
||||
Or[`SKIP`][do nothing]
|
||||
Or[`CALL` $path expr+$][call function]
|
||||
Or[`WRITE` $path$][write to variable]
|
||||
Or[`READ` $path$][read from variable]
|
||||
Or[$stmt ; stmt$][sequence of two statements]
|
||||
Or[$stmt | stmt$][choice between the statements]
|
||||
Or[$stmt ; stmt$][control flow operator, xecution ]
|
||||
Or[$stmt | stmt$][control flow operator, excution of one statements]
|
||||
}
|
||||
),
|
||||
Prod(
|
||||
|
|
@ -156,7 +155,7 @@
|
|||
Or[$0$][valid value of simple type] // `Unit`
|
||||
Or[$\#$][valid or spoiled value of simple type] // `Unit`
|
||||
Or[$bot$][spoiled value of simple type] // `Unit`
|
||||
Or[$lambda space (X+ stmt)+$][function pointer value, set of possible values] // `Fun`
|
||||
Or[$lambda space overline(x) stmt$][function pointer value] // `Fun`
|
||||
Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref`
|
||||
Or[$[deepValue+]$][tuple value] // `Prod`
|
||||
}
|
||||
|
|
@ -167,7 +166,7 @@
|
|||
Or[$0$][valid value of simple type] // `Unit`
|
||||
Or[$\#$][valid or spoiled value of simple type] // `Unit`
|
||||
Or[$bot$][spoiled value of simple type] // `Unit`
|
||||
Or[$lambda space (X+ stmt)+$][function pointer value, set of possible values] // `Fun`
|
||||
Or[$lambda space overline(x) stmt$][function pointer value] // `Fun`
|
||||
Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
|
||||
Or[$[value+]$][tuple value] // `Prod`
|
||||
}
|
||||
|
|
@ -201,7 +200,7 @@ $v in value$ - произвольное значение
|
|||
|
||||
$l = #[next] (mu)$,
|
||||
|
||||
$mu xarrowSquiggly(v)_#[add] cl l, mu [l <- v] cr$,
|
||||
$cl mu cr xarrowSquiggly(v)_#[add] cl l, mu [l <- v] cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -235,7 +234,7 @@ $s in stmt, f in X, x in X, a in X$
|
|||
#let eqmu = $attach(=, br: mu)$
|
||||
#let arrmu = $attach(->, br: mu)$
|
||||
|
||||
#let arrpath = $xarrowSquiggly(space)_path$
|
||||
#let arrpath = $xarrowSquiggly(mu)_path$
|
||||
|
||||
#let ttype = $attach(tack.r, br: type)$
|
||||
#let tmode = $attach(tack.r, br: mode)$
|
||||
|
|
@ -481,7 +480,7 @@ $s in stmt, f in X, x in X, a in X$
|
|||
|
||||
$cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$,
|
||||
|
||||
$mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
|
||||
$cl mu_v cr xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
|
||||
|
||||
$cl rf l, mu cr xarrowSquiggly(rf Copy t)_new cl rf l', mu_a cr$,
|
||||
)
|
||||
|
|
@ -586,12 +585,11 @@ $s in stmt, f in X, x in X, a in X$
|
|||
rule(
|
||||
name: [ combine lambda values],
|
||||
|
||||
// TODO: FIXME: how to combine statments in the right way? should check both
|
||||
[*TODO: combining semantics for lambda values (sets?)*],
|
||||
$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]$
|
||||
$lambda space overline(x_1) space s_2 plus.o lambda space overline(x_2) space s_2 = lambda$
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -642,145 +640,6 @@ $s in stmt, f in X, x in X, a in X$
|
|||
|
||||
#h(10pt)
|
||||
|
||||
=== Expression Evaluation
|
||||
|
||||
// TODO: check
|
||||
|
||||
#let eval = `eval`
|
||||
#let texpre = $attach(tack.r.double, br: eval)$
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ unit value type],
|
||||
|
||||
$vals, mu texpre () eqmu 0$,
|
||||
)
|
||||
))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ path type],
|
||||
|
||||
$vals, mu tval p eqmu v$,
|
||||
$vals, mu texpre p eqmu v$,
|
||||
)
|
||||
))
|
||||
|
||||
// NOTE: tmp removed
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ unit value type],
|
||||
|
||||
// $vals, mu texpre e : t$,
|
||||
|
||||
// [*TODO*],
|
||||
|
||||
// // TODO: reference to what ??
|
||||
// $vals, mu texpre rf e eqmu rf ??$,
|
||||
// )
|
||||
// ))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ unit value type],
|
||||
|
||||
$vals, mu texpre e_1 eqmu v_1$,
|
||||
$...$,
|
||||
$vals, mu texpre e_n eqmu v_n$,
|
||||
$vals, mu texpre [e_1, ... e_n] eqmu [v_1, ... v_n]$,
|
||||
)
|
||||
))
|
||||
|
||||
=== Expresion Typing
|
||||
|
||||
// TODO: check
|
||||
|
||||
#let texprt = $attach(tack.r.double, br: type)$
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ unit value type],
|
||||
|
||||
$types texprt () : cl Read, NotWrite cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ path type],
|
||||
|
||||
$types ttype p : t$,
|
||||
$types texprt p : t$,
|
||||
)
|
||||
))
|
||||
|
||||
// NOTE: tmp removed
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ unit value type],
|
||||
|
||||
// $types texprt e : t$,
|
||||
// // TODO: why Ref mode ?? <- due to immutability ??
|
||||
// $types texprt rf e : rf Ref t$,
|
||||
// )
|
||||
// ))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ unit value type],
|
||||
|
||||
$types texprt e_1 : t_1$,
|
||||
$...$,
|
||||
$types texprt e_n : t_n$,
|
||||
$types texprt [e_1, ... e_n] : [t_1, ... t_n]$,
|
||||
)
|
||||
))
|
||||
|
||||
=== Context Initialization
|
||||
|
||||
#let init = `init`
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ add variable declaration],
|
||||
|
||||
// NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers)
|
||||
// expect well typed program
|
||||
|
||||
$vals, mu texpre e eqmu v$,
|
||||
$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 = e)_init cl types[x <- t], vals[x <- l], mu'' cr$
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ add function declaration],
|
||||
|
||||
$mu xarrowSquiggly(lambda space [[x_1, ... x_n] s])_#[add] cl l, 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
|
||||
cl types[f <- lambda space [t_1, ... t_n]], vals[f <- l], mu' cr$
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
=== Call Values Spoil
|
||||
|
||||
#let spoil = `spoil`
|
||||
|
|
@ -894,50 +753,125 @@ $s in stmt, f in X, x in X, a in X$
|
|||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ full spoil for unit expr],
|
||||
name: [ full spoil],
|
||||
|
||||
$mu stretch(=>)^(m space cl r, w cr space ())_(cl vals, types cr) mu$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ full spoil for path expr],
|
||||
|
||||
$p : path$,
|
||||
$p arrpath x$,
|
||||
$l = vals[x]$,
|
||||
$vals, mu texpre p eqmu b$,
|
||||
$vals, mu tval p eqmu b$,
|
||||
$types ttype p : t'$,
|
||||
// TODO: FIXME: Ref or Copy ?? in root <- Ref ??, because otherwise there could not b any Refs
|
||||
// FIXME depends on parent ??
|
||||
$cl b, mu cr xarrowSquiggly(t \, t' \, m \, Ref)_spoil cl b', mu' cr$,
|
||||
$cl mu'[l], mu' cr xarrowSquiggly(cl p \, b' cr)_modify cl v'', mu'' cr$,
|
||||
$cl mu[l], mu cr xarrowSquiggly(cl p \, b' cr)_modify cl v', mu' cr$,
|
||||
|
||||
$mu stretch(=>)^(m space t space p)_(cl vals, types cr) mu''[l <- v'']$,
|
||||
$mu stretch(=>)^(m space t space p)_(cl vals, types cr) mu'[l <- v']$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
=== Expression Evaluation
|
||||
|
||||
// TODO: check
|
||||
|
||||
#let eval = `eval`
|
||||
#let texpre = $attach(tack.r.double, br: eval)$
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ full spoil for tuple expr],
|
||||
name: [ path type],
|
||||
|
||||
$e = [e_1, ... e_n]$,
|
||||
$mu_0 stretch(=>)^(m space t_1 space e_1)_(cl vals, types cr) mu_1$,
|
||||
$...$,
|
||||
$mu_(n - 1) stretch(=>)^(m space t_n space e_n)_(cl vals, types cr) mu_n$,
|
||||
|
||||
$mu_0 stretch(=>)^(m space [t_1, ... t_n] space [e_1, ... e_n]_(cl vals, types cr) mu_n$,
|
||||
$vals, mu tval p eqmu v$,
|
||||
$vals, mu texpre p eqmu v$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ unit value type],
|
||||
|
||||
$vals, mu texpre () eqmu 0$,
|
||||
)
|
||||
))
|
||||
|
||||
// NOTE: tmp removed
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ unit value type],
|
||||
|
||||
// $vals, mu texpre e : t$,
|
||||
|
||||
// [*TODO*],
|
||||
|
||||
// // TODO: reference to what ??
|
||||
// $vals, mu texpre rf e eqmu rf ??$,
|
||||
// )
|
||||
// ))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ unit value type],
|
||||
|
||||
$vals, mu texpre e_1 eqmu v_1$,
|
||||
$...$,
|
||||
$vals, mu texpre e_n eqmu v_n$,
|
||||
$vals, mu texpre [e_1, ... e_n] eqmu [v_1, ... v_n]$,
|
||||
)
|
||||
))
|
||||
|
||||
|
||||
=== Expresion Typing
|
||||
|
||||
// TODO: check
|
||||
|
||||
#let texprt = $attach(tack.r.double, br: type)$
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ path type],
|
||||
|
||||
$types ttype p : t$,
|
||||
$types texprt p : t$,
|
||||
)
|
||||
))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ unit value type],
|
||||
|
||||
$types texprt () : cl Read, NotWrite cr$,
|
||||
)
|
||||
))
|
||||
|
||||
// NOTE: tmp removed
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ unit value type],
|
||||
|
||||
// $types texprt e : t$,
|
||||
// // TODO: why Ref mode ?? <- due to immutability ??
|
||||
// $types texprt rf e : rf Ref t$,
|
||||
// )
|
||||
// ))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ unit value type],
|
||||
|
||||
$types texprt e_1 : t_1$,
|
||||
$...$,
|
||||
$types texprt e_n : t_n$,
|
||||
$types texprt [e_1, ... e_n] : [t_1, ... t_n]$,
|
||||
)
|
||||
))
|
||||
|
||||
=== Function Argument Addition
|
||||
|
||||
|
|
@ -946,48 +880,19 @@ $s in stmt, f in X, x in X, a in X$
|
|||
rule(
|
||||
name: [ add argument],
|
||||
|
||||
$vals_#[ctx], mu texpre e eqmu v$,
|
||||
// $types ttype p : t'$, // TODO: not required if there is no check
|
||||
|
||||
$vals, mu tval p eqmu v$,
|
||||
$types ttype p : t'$,
|
||||
// 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$,
|
||||
$cl v', mu cr xarrowSquiggly(t)_new cl v, mu' cr$,
|
||||
|
||||
|
||||
// TODO save type mode somewhere ?? // <- not needed because is described by other params <- ??
|
||||
$cl types, vals, mu cr
|
||||
xarrowDashed(x space t space e)_(vals_#[ctx])
|
||||
cl types[x <- t], vals[x <- l], mu'' cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
=== Function Evaluation
|
||||
|
||||
#let tfunceval = $attach(tack.r.double, br: #[func eval])$
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ new reference copy value],
|
||||
|
||||
$types_0 = []$,
|
||||
$vals_0 = []$,
|
||||
|
||||
// NOTE: dashed arrow to fill context
|
||||
$cl types_0, vals_0, mu_0 cr
|
||||
xarrowDashed(x_1 space t_1 space e_1)_vals
|
||||
cl types', vals_1, mu_1 cr$,
|
||||
$...$,
|
||||
$cl types_(n - 1), vals_(n - 1), mu_(n - 1) cr
|
||||
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
|
||||
xarrow(s)
|
||||
cl types', vals', mu' cr$,
|
||||
|
||||
$cl vals, mu_0 cr tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$,
|
||||
xarrowDashed(x space t space p)
|
||||
cl types[x <- t], vals[x <- v], mu' cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -998,37 +903,39 @@ $s in stmt, f in X, x in X, a in X$
|
|||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ SKIP],
|
||||
name: [ CALL $f space [p_1, ... p_n]$],
|
||||
|
||||
$cl types, vals, mu cr
|
||||
xarrow("SKIP")
|
||||
cl types, vals, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
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]$,
|
||||
$vals, mu texpre f eqmu lambda [x_1, ... x_n] space s$,
|
||||
$types ttype f : lambda [m_1 t_1, ... m_n t_n] $,
|
||||
|
||||
// NOTE: check that all the possible bodies are possible to eval
|
||||
$cl vals, mu_0 cr tfunceval cl s_1, overline(x)_1, [t_1, ... t_n], [e_1, ... e_n] cr$,
|
||||
// TODO: add args before statement eval
|
||||
|
||||
$types_0 = []$,
|
||||
$vals_0 = []$,
|
||||
$mu_0 = mu$,
|
||||
|
||||
// NOTE: dashed arrow to fill context
|
||||
$cl types_0, vals_0, mu_0, l cr
|
||||
xarrowDashed(x_1 space t_1 space p_1)
|
||||
cl types', vals_1, mu_1, l' cr$,
|
||||
$...$,
|
||||
$cl vals, mu_0 cr tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] cr$,
|
||||
$cl types_(n - 1), vals_(n - 1), mu_(n - 1), l cr
|
||||
xarrowDashed(x_n space t_n space p_n)
|
||||
cl types', vals_n, mu_n, l' cr$,
|
||||
|
||||
$cl types_n, vals_n, mu_n, l cr
|
||||
xarrow(s)
|
||||
cl types', vals', mu', l' cr$,
|
||||
|
||||
// NOTE: thick arrow to "spoil" context
|
||||
$mu_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) mu_1$,
|
||||
$gamma_0 = mu$,
|
||||
$gamma_0 stretch(=>)^(x_1 space m_1 space t_1 space p_1)_(cl vals, types cr) gamma_1$,
|
||||
$...$,
|
||||
$mu_(n - 1) stretch(=>)^(m_n space t_n space e_n)_(cl vals, types cr) mu_n$,
|
||||
$gamma_(n - 1) stretch(=>)^(m_n space t_n space p_n)_(cl vals, types cr) gamma_n$,
|
||||
|
||||
$cl types, vals, mu_0 cr
|
||||
xarrow("CALL" f space [e_1, ... e_n])
|
||||
cl types, vals, mu_n cr$,
|
||||
$cl vals, types, mu, l cr
|
||||
xarrow("CALL" f space [p_1, ... p_n])
|
||||
cl vals, types, gamma_n, l cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -1039,7 +946,7 @@ $s in stmt, f in X, x in X, a in X$
|
|||
rule(
|
||||
name: [ READ $p$],
|
||||
|
||||
$vals, mu tval p eqmu 0$,
|
||||
$mu, types, vals tval p eqmu 0$,
|
||||
|
||||
$cl types, vals, mu cr
|
||||
xarrow("READ" p)
|
||||
|
|
@ -1057,7 +964,7 @@ $s in stmt, f in X, x in X, a in X$
|
|||
$types ttype p : cl r, w cr$,
|
||||
$w = MaybeWrite or w = AlwaysWrite$,
|
||||
$p arrpath x$,
|
||||
$l = vals[x]$,
|
||||
$l = vals(x)$,
|
||||
$mu[l] xarrowSquiggly(cl p \, 0 cr)_modify v'$,
|
||||
|
||||
$cl types, vals, mu cr
|
||||
|
|
@ -1081,7 +988,7 @@ $s in stmt, f in X, x in X, a in X$
|
|||
stretch(->)^t
|
||||
cl types_t, vals_t, mu_t cr$,
|
||||
|
||||
$cl types, vals, mu cr
|
||||
$cl types, vals, mu, cr
|
||||
xarrow(s \; t)
|
||||
cl types_t, vals_t, mu_t cr$,
|
||||
)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue