From 250776f1f7b64d6ff30e4dfdcb2c83288a9fa083 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Wed, 29 Apr 2026 09:16:24 +0000 Subject: [PATCH] structures: semantics fixes, another part of analyzer (up to most part of stmt eval) --- model_with_structures/analyzer.ml | 129 ++++++++++++++++++++++++------ model_with_structures/model.typ | 48 +++++------ 2 files changed, 130 insertions(+), 47 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 1b5740e..2144e8c 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -52,6 +52,8 @@ 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 *) @@ -73,19 +75,31 @@ struct (* --- *) - type mem = (memid * 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 vals = (data * memid) list type state = mem * types * vals (* --- *) - (* TODO: FIXME: use list_replace for memory instead ?? *) - let mem_get (mem : mem) (id : memid) : value = List.assoc id (fst mem) + (* - 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 let mem_add (mem : mem) (v : value) : mem * memid = - (((snd mem, v) :: fst mem, snd mem + 1), 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) + (list_replace (fst mem) id v, snd mem) let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with | ZeroV -> ZeroDV @@ -125,12 +139,11 @@ struct (* --- eval rules --- *) - (* - 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 + (* 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 (* - value construction *) @@ -168,17 +181,16 @@ struct if is_trivial_v u && is_trivial_v v then (if u == v then u else BotV) else match u, v with - (* TODO: FIXME: combining semanticsfor funcitons statements *) + (* TODO: FIXME: combining semantics for 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" + | _, _ -> raise @@ Typing_error "valcomb" - (* 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) *) + 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 *) @@ -188,7 +200,7 @@ struct (c : copy_cap) : bool = (r != Rd || v == ZeroV) && (r != Rd || fst m == In) && - (o != Out || w == AlwaysWr) && + (snd m != Out || w == AlwaysWr) && (* TODO: check *) ((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr) && is_trivial_v v @@ -196,17 +208,88 @@ 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'), _ -> (* TODO FIXME *) raise Not_found + | UnitT (r, w), UnitT (r', w'), _ -> + if not @@ is_trivial_v v + then raise @@ Typing_error "valspoil: unit, not trivial" + else if not @@ is_correct_tags v r w r' w' m c + then raise @@ Typing_error "valspoil: unit, not correct" + else if snd m == NOut && c == Rf && (w == AlwaysWr || w == MayWr) + then (mem, BotV) + else if snd m == Out && w == AlwaysWr + then (mem, ZeroV) + else (mem, v) | FunT ts, FunT us, FunV _ -> if ts == us then (mem, v) else raise @@ Typing_error "valspoil: fun" | RefT (ct, t), RefT (cu, u), RefV id -> let (mem', v') = valspoil mem (mem_get mem id) t u m ct in (mem_set mem id v', RefV id) - | TupleT ts, TupleT us, TupleV vs -> (* TODO FIXME *) raise Not_found + | 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') | _, _, _ -> raise @@ Typing_error "valspoil" -(* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *) + (* full spoil *) + let rec argsspoil (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 argsspoil (* full spoil *) *) + (* - 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) + + (* - funciton argument addition *) + + let addarg (state : state) (x : data) (t : atype) (p : path) : state = + match state with (mem, types, vals) -> + let v = pathval mem vals p 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) + + let rec stmt_eval (state : state) (s : stmt) : state = + match state with (mem, types, vals) -> match s with + | CallS (f, ps) -> raise Not_found (* TODO: FIXME: write call *) + | 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) + + (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *) (* --- *) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 3449afc..4ca391a 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -200,7 +200,7 @@ $v in value$ - произвольное значение $l = #[next] (mu)$, - $cl mu cr xarrowSquiggly(v)_#[add] cl l, mu [l <- v] cr$, + $mu xarrowSquiggly(v)_#[add] cl l, mu [l <- v] cr$, ) )) @@ -234,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(mu)_path$ +#let arrpath = $xarrowSquiggly(space)_path$ #let ttype = $attach(tack.r, br: type)$ #let tmode = $attach(tack.r, br: mode)$ @@ -480,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$, - $cl mu_v cr 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 Copy t)_new cl rf l', mu_a cr$, ) @@ -762,9 +762,9 @@ $s in stmt, f in X, x in X, a in X$ // 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'']$, ) )) @@ -780,19 +780,19 @@ $s in stmt, f in X, x in X, a in X$ #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ path type], + name: [ unit value type], - $vals, mu tval p eqmu v$, - $vals, mu texpre p eqmu v$, + $vals, mu texpre () eqmu 0$, ) )) #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ unit value type], + name: [ path type], - $vals, mu texpre () eqmu 0$, + $vals, mu tval p eqmu v$, + $vals, mu texpre p eqmu v$, ) )) @@ -833,19 +833,19 @@ $s in stmt, f in X, x in X, a in X$ #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ path type], + name: [ unit value type], - $types ttype p : t$, - $types texprt p : t$, + $types texprt () : cl Read, NotWrite cr$, ) )) #align(center, prooftree( vertical-spacing: 4pt, rule( - name: [ unit value type], + name: [ path type], - $types texprt () : cl Read, NotWrite cr$, + $types ttype p : t$, + $types texprt p : t$, ) )) @@ -882,17 +882,17 @@ $s in stmt, f in X, x in X, a in X$ $vals, mu tval p eqmu v$, - $types ttype p : t'$, + // $types ttype p : t'$, // TODO: not required if there is no check // 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$, - + $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 <- ?? $cl types, vals, mu cr xarrowDashed(x space t space p) - cl types[x <- t], vals[x <- v], mu' cr$, + cl types[x <- t], vals[x <- l], mu'' cr$, ) )) @@ -933,9 +933,9 @@ $s in stmt, f in X, x in X, a in X$ $...$, $gamma_(n - 1) stretch(=>)^(m_n space t_n space p_n)_(cl vals, types cr) gamma_n$, - $cl vals, types, mu, l cr + $cl vals, types, mu cr xarrow("CALL" f space [p_1, ... p_n]) - cl vals, types, gamma_n, l cr$, + cl vals, types, gamma_n cr$, ) )) @@ -946,7 +946,7 @@ $s in stmt, f in X, x in X, a in X$ rule( name: [ READ $p$], - $mu, types, vals tval p eqmu 0$, + $vals, mu tval p eqmu 0$, $cl types, vals, mu cr xarrow("READ" p) @@ -964,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 @@ -988,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$, )