st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-04-30 17:52:41 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

structures: call stmt in analyzer, addarg & spoil for expressions, semantics fixes

Browse source
This commit is contained in:
ProgramSnail 2026-04-29 11:03:52 +00:00
parent 250776f1f7
commit 40e02c0e5a
2 changed files with 186 additions and 130 deletions
Download patch file Download diff file Expand all files Collapse all files

63
model_with_structures/analyzer.ml
View file

@ -21,7 +21,7 @@ struct
type atype = UnitT of read_cap * write_cap type atype = UnitT of read_cap * write_cap
| RefT of copy_cap * atype | RefT of copy_cap * atype
| TupleT of atype list | TupleT of atype list
| FunT of data (* declaration id for ease of impl (?) *) | FunT of (mode * atype) list (* TODO: declaration id for ease of impl / performance instead (?) *)
type mtype = mode * atype type mtype = mode * atype
@ -192,6 +192,20 @@ struct
then raise @@ Typing_error "memcomb" then raise @@ Typing_error "memcomb"
else (List.map2 valcomb (fst m) (fst n), snd m) 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)
(* - call values spoil *) (* - call values spoil *)
(* TODO: check all cases *) (* TODO: check all cases *)
@ -230,7 +244,7 @@ struct
| _, _, _ -> raise @@ Typing_error "valspoil" | _, _, _ -> raise @@ Typing_error "valspoil"
(* full spoil *) (* full spoil *)
let rec argsspoil (state : state) (m : mode) (t : atype) (p : path) : mem = let rec argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
match state with (mem, types, vals) -> match state with (mem, types, vals) ->
let x = pathvar p in let x = pathvar p in
let id = List.assoc x vals in let id = List.assoc x vals in
@ -240,33 +254,46 @@ struct
let (mem'', v'') = valupd mem' (mem_get mem' id) p b' in let (mem'', v'') = valupd mem' (mem_get mem' id) p b' in
mem_set mem'' id v'' mem_set mem'' id v''
(* - expression evaluation *) let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
match state with (mem, types, vals) -> match e, t with
let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with | UnitE, UnitT _ -> mem
| UnitE -> ZeroV | PathE p, t -> argsspoilp state m t p
| PathE p -> pathval mem vals p | TupleE es, TupleT ts -> List.fold_left2
| TupleE es -> TupleV (List.map (exprval mem vals) es) (fun mem' t' e' -> argsspoile (mem', types, vals) m t' e')
mem ts es
(* - expression typing *) | _, _ -> raise @@ Typing_error "valspoile"
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 *) (* - funciton argument addition *)
let addarg (state : state) (x : data) (t : atype) (p : path) : state = let addarg (state : state) (x : data) (t : atype) (e : expr) : state =
match state with (mem, types, vals) -> match state with (mem, types, vals) ->
let v = pathval mem vals p in let v = exprval mem vals e in
(* let t' = pathtype types p in *) (* let t' = pathtype types p in *)
let (mem', v') = valcopy mem v t in let (mem', v') = valcopy mem v t in
let (mem'', id) = mem_add mem' v in let (mem'', id) = mem_add mem' v in
(mem', (x, t) :: types, (x, id) :: vals) (mem', (x, t) :: types, (x, id) :: vals)
(* - 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) -> match s with
| CallS (f, ps) -> raise Not_found (* TODO: FIXME: write call *) (* TODO: FIXME: Add memoisation *)
| 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, *) fs (* ) *), 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
let _state_evaled = stmt_eval state_with_args fs 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 | WriteS p -> (match pathtype types p with
| UnitT (_, w) -> | UnitT (_, w) ->
if w == NeverWr if w == NeverWr

251
model_with_structures/model.typ
View file

@ -640,6 +640,109 @@ $s in stmt, f in X, x in X, a in X$
#h(10pt) #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]$,
)
))
=== Call Values Spoil === Call Values Spoil
#let spoil = `spoil` #let spoil = `spoil`
@ -753,11 +856,23 @@ $s in stmt, f in X, x in X, a in X$
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ full spoil], name: [ full spoil for unit expr],
$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$, $p arrpath x$,
$l = vals[x]$, $l = vals[x]$,
$vals, mu tval p eqmu b$, $vals, mu texpre p eqmu b$,
$types ttype p : t'$, $types ttype p : t'$,
// TODO: FIXME: Ref or Copy ?? in root <- Ref ??, because otherwise there could not b any Refs // TODO: FIXME: Ref or Copy ?? in root <- Ref ??, because otherwise there could not b any Refs
// FIXME depends on parent ?? // FIXME depends on parent ??
@ -770,108 +885,21 @@ $s in stmt, f in X, x in X, a in X$
#h(10pt) #h(10pt)
=== Expression Evaluation
// TODO: check
#let eval = `eval`
#let texpre = $attach(tack.r.double, br: eval)$
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ unit value type], name: [ full spoil for tuple expr],
$vals, mu texpre () eqmu 0$, $e = [e_1, ... e_n]$,
) $mu_0 stretch(=>)^(m space t_1 space e_1)_(cl vals, types cr) mu_1$,
))
#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$, $mu_(n - 1) stretch(=>)^(m space t_n space e_n)_(cl vals, types cr) mu_n$,
$vals, mu texpre [e_1, ... e_n] eqmu [v_1, ... v_n]$,
$mu_0 stretch(=>)^(m space [t_1, ... t_n] space [e_1, ... e_n]_(cl vals, types cr) mu_n$,
) )
)) ))
#h(10pt)
=== 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]$,
)
))
=== Function Argument Addition === Function Argument Addition
@ -881,7 +909,7 @@ $s in stmt, f in X, x in X, a in X$
name: [ add argument], name: [ add argument],
$vals, mu tval p eqmu v$, $vals, mu texpre e eqmu v$,
// $types ttype p : t'$, // TODO: not required if there is no check // $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 type compatibility for t and type for path p (?)
// [*TODO: check t ~ t' in sme way (?)*], // [*TODO: check t ~ t' in sme way (?)*],
@ -891,7 +919,7 @@ $s in stmt, f in X, x in X, a in X$
// 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 space p) xarrowDashed(x space t space e)
cl types[x <- t], vals[x <- l], mu'' cr$, cl types[x <- t], vals[x <- l], mu'' cr$,
) )
)) ))
@ -903,9 +931,10 @@ $s in stmt, f in X, x in X, a in X$
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ CALL $f space [p_1, ... p_n]$], name: [ CALL $f space [e_1, ... e_n]$],
$vals, mu texpre f eqmu lambda [x_1, ... x_n] space s$, // TODO: why there was texpre ? // texpre is unrequired ?
$vals, mu tval f eqmu lambda [x_1, ... x_n] space s$,
$types ttype f : lambda [m_1 t_1, ... m_n t_n] $, $types ttype f : lambda [m_1 t_1, ... m_n t_n] $,
// TODO: add args before statement eval // TODO: add args before statement eval
@ -915,26 +944,26 @@ $s in stmt, f in X, x in X, a in X$
$mu_0 = mu$, $mu_0 = mu$,
// NOTE: dashed arrow to fill context // NOTE: dashed arrow to fill context
$cl types_0, vals_0, mu_0, l cr $cl types_0, vals_0, mu_0 cr
xarrowDashed(x_1 space t_1 space p_1) xarrowDashed(x_1 space t_1 space e_1)
cl types', vals_1, mu_1, l' cr$, cl types', vals_1, mu_1 cr$,
$...$, $...$,
$cl types_(n - 1), vals_(n - 1), mu_(n - 1), l cr $cl types_(n - 1), vals_(n - 1), mu_(n - 1) cr
xarrowDashed(x_n space t_n space p_n) xarrowDashed(x_n space t_n space e_n)
cl types', vals_n, mu_n, l' cr$, cl types_n, vals_n, mu_n cr$,
$cl types_n, vals_n, mu_n, l cr $cl types_n, vals_n, mu_n cr
xarrow(s) xarrow(s)
cl types', vals', mu', l' cr$, cl types', vals', mu' cr$,
// NOTE: thick arrow to "spoil" context // NOTE: thick arrow to "spoil" context
$gamma_0 = mu$, $gamma_0 = mu$,
$gamma_0 stretch(=>)^(x_1 space m_1 space t_1 space p_1)_(cl vals, types cr) gamma_1$, $gamma_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) gamma_1$,
$...$, $...$,
$gamma_(n - 1) stretch(=>)^(m_n space t_n space p_n)_(cl vals, types cr) gamma_n$, $gamma_(n - 1) stretch(=>)^(m_n space t_n space e_n)_(cl vals, types cr) gamma_n$,
$cl vals, types, mu cr $cl vals, types, mu cr
xarrow("CALL" f space [p_1, ... p_n]) xarrow("CALL" f space [e_1, ... e_n])
cl vals, types, gamma_n cr$, cl vals, types, gamma_n cr$,
) )
)) ))