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:66ea0e53da2fdc4867f0fd110491cc7b343736c1
Branches Tags
st:main
st:lambdas_no_value
st:memory_ext
..
compare: st:1bacb6dfd77072ae74c1eb4fe7d05996c9d1e818
Branches Tags
st:main
st:lambdas_no_value
st:memory_ext

No commits in common. "66ea0e53da2fdc4867f0fd110491cc7b343736c1" and "1bacb6dfd77072ae74c1eb4fe7d05996c9d1e818" have entirely different histories.
66ea0e53da ... 1bacb6dfd7

4 changed files with 621 additions and 741 deletions
Download patch file Download diff file Expand all files Collapse all files

147
model_with_structures/analyzer.ml
View file

@ -27,8 +27,7 @@ struct
type expr = UnitE type expr = UnitE
| PathE of path | PathE of path
(* TODO: extend to include arbitrary path *) (* | RefE *)
| RefE of data
| TupleE of expr list | TupleE of expr list
type stmt = SkipS type stmt = SkipS
@ -97,11 +96,11 @@ struct
(* (((snd mem, 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 = *) (* let mem_set (mem : mem) (id : memid) (v : value) : mem = *)
(* ((id, v) :: fst mem, snd mem) *) (* ((id, v) :: fst mem, snd mem) *)
let mem_get (mem : mem) (id : memid) : value = (* FIXME TMP Printf.printf "l%i i%i %i: access\n" (snd mem) id (snd mem - id - 1); *) List.nth (fst mem) (snd mem - id - 1) let mem_get (mem : mem) (id : memid) : value = List.nth (fst mem) id
let mem_add (mem : mem) (v : value) : mem * memid = let mem_add (mem : mem) (v : value) : mem * memid =
((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 = let mem_set (mem : mem) (id : memid) (v : value) : mem =
(list_replace (fst mem) (snd mem - id - 1) v, snd mem) (list_replace (fst mem) id v, snd mem)
let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with
| ZeroV -> ZeroDV | ZeroV -> ZeroDV
@ -131,12 +130,7 @@ struct
| _ -> raise @@ Typing_error "pathtype: access" | _ -> raise @@ Typing_error "pathtype: access"
let rec pathval (mem : mem) (vals : vals) (p : path) : value = match p with let rec pathval (mem : mem) (vals : vals) (p : path) : value = match p with
| VarP x -> mem_get mem @@ ((* Printf.printf "%i: " x; (* FIXME TMP *) | VarP x -> mem_get mem @@ List.assoc x vals
ignore @@ List.map (fun (x, _) -> Printf.printf "%i " x) vals;
Printf.printf "mem size: %i, " (List.length (fst mem));
Printf.printf "mem size stored: %i " (snd mem);
Printf.printf "\n"; *)
List.assoc x vals)
| DerefP p -> (match pathval mem vals p with | DerefP p -> (match pathval mem vals p with
| RefV id -> mem_get mem id | RefV id -> mem_get mem id
| _ -> raise @@ Typing_error "pathval: deref") | _ -> raise @@ Typing_error "pathval: deref")
@ -203,7 +197,6 @@ struct
let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with
| UnitE -> ZeroV | UnitE -> ZeroV
| PathE p -> pathval mem vals p | PathE p -> pathval mem vals p
| RefE x -> RefV (List.assoc x vals)
| TupleE es -> TupleV (List.map (exprval mem vals) es) | TupleE es -> TupleV (List.map (exprval mem vals) es)
(* - expression typing *) (* - expression typing *)
@ -211,7 +204,6 @@ struct
let rec exprtype (types : types) (e : expr) : atype = match e with let rec exprtype (types : types) (e : expr) : atype = match e with
| UnitE -> UnitT (Rd, NeverWr) | UnitE -> UnitT (Rd, NeverWr)
| PathE p -> pathtype types p | PathE p -> pathtype types p
| RefE x -> RefT (Rf, List.assoc x types)
| TupleE es -> TupleT (List.map (exprtype types) es) | TupleE es -> TupleT (List.map (exprtype types) es)
(* - context initialization *) (* - context initialization *)
@ -228,8 +220,7 @@ struct
| FunD (ts, s) -> let (mem', id) = mem_add mem (FunV [s]) in | FunD (ts, s) -> let (mem', id) = mem_add mem (FunV [s]) in
(mem', (x, FunT ts) :: types, (x, id) :: vals) (mem', (x, FunT ts) :: types, (x, id) :: vals)
let empty_mem : mem = ([], 0) let empty_state : state = (([], 0), [], [])
let empty_state : state = (empty_mem, [], [])
(* TODO: better way ??? *) (* TODO: better way ??? *)
let globals_min_id : data = 1000 let globals_min_id : data = 1000
@ -246,18 +237,11 @@ struct
let is_correct_tags (v : value) (r : read_cap) (w : write_cap) let is_correct_tags (v : value) (r : read_cap) (w : write_cap)
(r' : read_cap) (w' : write_cap) (m : mode) (r' : read_cap) (w' : write_cap) (m : mode)
(c : copy_cap) : bool = (c : copy_cap) : bool =
(* FIXME TMP
Printf.printf "%b %b %b %b %b\n"
(r != Rd || v == ZeroV)
(r != Rd || fst m == In)
(snd m != Out || w == AlwaysWr)
(((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr))
(is_trivial_v v); *)
(r != Rd || v == ZeroV) && (r != Rd || v == ZeroV) &&
(r != Rd || fst m == In) && (r != Rd || fst m == In) &&
(snd m != Out || w == AlwaysWr) && (snd m != Out || w == AlwaysWr) &&
(* TODO: check *) (* TODO: check *)
((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr) && ((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr) &&
is_trivial_v v is_trivial_v v
let rec valspoil (mem : mem) (v : value) (t : atype) let rec valspoil (mem : mem) (v : value) (t : atype)
@ -307,13 +291,13 @@ struct
(* - funciton argument addition *) (* - funciton argument addition *)
let addarg (state : state) (oldvals : vals) (x : data) (t : atype) (e : expr) : 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 = exprval mem oldvals e 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)
(* - function evaluation *) (* - function evaluation *)
@ -326,25 +310,23 @@ struct
match state with (mem, types, vals) -> match s with match state with (mem, types, vals) -> match s with
(* TODO: FIXME: Add memoisation *) (* TODO: FIXME: Add memoisation *)
| SkipS -> state | SkipS -> state
| CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *) pathval mem vals f in | CallS (f, es) -> let v = pathval mem vals f in
let t = (* FIXME TMP Printf.printf "call, before t\n"; *) pathtype types f in let t = pathtype types f in
let types' : types = [] in let types' : types = [] in
let vals' : vals = [] in let vals' : vals = [] in
(match v, t with (match v, t with
| FunV (* xs, *) fstmts (* ) *), FunT ts -> | FunV (* xs, *) fstmts (* ) *), FunT ts ->
(* TODO: memoisation of the called functions *) (* TODO: memoisation of the called functions *)
let (state_with_args, _) = (* FIXME TMP Printf.printf "call, before args\n"; *) List.fold_left2 (* TODO: FIXME: check x's order *) let (state_with_args, _) = List.fold_left2 (* TODO: FIXME: check x's order *)
(fun (st, x) (m, t) p -> (addarg st vals x t p, x + 1)) (fun (st, x) (m, t) p -> (addarg st x t p, x + 1))
((mem, types', vals'), 0) ts es in ((mem, types', vals'), 0) ts es in
(* NOTE: same x's, so can use same args for all the statements *) (* NOTE: same x's, so can use same args for all the statements *)
let _states_evaled = (* FIXME TMP Printf.printf "call, before eval\n"; *) List.map (stmt_eval state_with_args) fstmts in let _states_evaled = List.map (stmt_eval state_with_args) fstmts in
let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *) List.fold_left2 let mem_spoiled = List.fold_left2
(fun mem (m, t) e -> argsspoile (mem, types, vals) m t e) (fun mem (m, t) e -> argsspoile (mem, types, vals) m t e)
mem ts es in mem ts es in
(mem_spoiled, types, vals) (mem_spoiled, types, vals)
| FunV _, _ -> raise @@ Eval_error "call: function type" | _, _ -> raise @@ Eval_error "call: function")
| _, FunT _ -> raise @@ Eval_error "call: function val"
| _, _ -> raise @@ Eval_error "call: function type & val")
| WriteS p -> (match pathtype types p with | WriteS p -> (match pathtype types p with
| UnitT (_, w) -> | UnitT (_, w) ->
if w == NeverWr if w == NeverWr
@ -379,59 +361,7 @@ struct
(* --- tests --- *) (* --- tests --- *)
(* - shortcuts *) (* - tests without functions *)
let ( #. ) x y = SeqS (x, y)
let vx = VarP 0
let vy = VarP 1
let vz = VarP 2
let vgx = VarP (globals_min_id)
let vgy = VarP (globals_min_id + 1)
let vgz = VarP (globals_min_id + 2)
let drf p = DerefP p
let access p i = AccessP (p, i)
let wr x = ReadS x
let rd x = WriteS x
let skp = SkipS
let uT_r_aw = UnitT (Rd, AlwaysWr)
let uT_r_mw = UnitT (Rd, MayWr)
let uT_aw = UnitT (NRd, AlwaysWr)
let uT_mw = UnitT (NRd, MayWr)
let uT_r = UnitT (Rd, NeverWr)
let uT = UnitT (NRd, NeverWr)
let rfT t = RefT (Rf, t)
let cpT t = RefT (Cp, t)
let moded t = ((In, NOut), t)
let defg t = VarD (t, UnitE)
(* - utils tests *)
let%expect_test "mem add / get / set" =
let mem = empty_mem in
let (mem, id1) = mem_add mem ZeroV in
let (mem, id2) = mem_add mem SmthV in
let (mem, id3) = mem_add mem BotV in
Printf.printf "%i %i %i " id1 id2 id3;
Printf.printf "%b %b %b " (mem_get mem id1 == ZeroV)
(mem_get mem id2 == SmthV)
(mem_get mem id3 == BotV);
let mem = mem_set mem id1 BotV in
let mem = mem_set mem id2 ZeroV in
let mem = mem_set mem id3 SmthV in
Printf.printf "%b %b %b" (mem_get mem id1 == BotV)
(mem_get mem id2 == ZeroV)
(mem_get mem id3 == SmthV);
[%expect {| 0 1 2 true true true true true true |}]
(* - basic var tests *)
let%expect_test "empty" = let%expect_test "empty" =
prog_eval_noret ([], SkipS); prog_eval_noret ([], SkipS);
@ -449,49 +379,6 @@ struct
with Eval_error msg -> Printf.printf "%s" msg; with Eval_error msg -> Printf.printf "%s" msg;
[%expect {| read |}] [%expect {| read |}]
let%expect_test "simple vars, no read & read" =
prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE);
VarD (UnitT (Rd, MayWr), UnitE)],
ReadS (VarP (globals_min_id + 1)));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "simple var, write" =
prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], WriteS (VarP globals_min_id));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "simple var, no write" =
try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr), UnitE)], WriteS (VarP globals_min_id));
[%expect.unreachable]);
with Eval_error msg -> Printf.printf "%s" msg;
[%expect {| write: write tag |}]
let%expect_test "simple var, write & read" =
prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], SeqS (WriteS (VarP globals_min_id),
ReadS (VarP globals_min_id)));
Printf.printf "done!";
[%expect {| done! |}]
(* - basic call tests *)
let%expect_test "simple call with read" =
prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE);
FunD ([(In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0))],
CallS (VarP (globals_min_id + 1),
[PathE (VarP globals_min_id)]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "simple call with write" =
prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE);
VarD (RefT (Rf, (UnitT (Rd, MayWr))), RefE globals_min_id);
FunD ([(In, NOut), RefT (Cp, UnitT (Rd, MayWr))], WriteS (DerefP (VarP 0)))],
CallS (VarP (globals_min_id + 2),
[PathE (VarP (globals_min_id + 1))]));
Printf.printf "done!";
[%expect {| done! |}]
(* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *) (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
(* --- tests --- *) (* --- tests --- *)

40
model_with_structures/dune
View file

@ -42,23 +42,23 @@
; -pp ; -pp
; camlp5/pp5+gt+plugins+ocanren+dump.exe))) ; camlp5/pp5+gt+plugins+ocanren+dump.exe)))
(library ; (library
(name synthesizer_st) ; (name synthesizer_st)
(modules synthesizer) ; (modules synthesizer)
(flags ; (flags
; (-dsource) ; ; (-dsource)
(:standard -rectypes)) ; (:standard -rectypes))
(libraries OCanren OCanren.tester) ; (libraries OCanren OCanren.tester)
(preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe) ; (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
(wrapped false) ; (wrapped false)
(preprocess ; (preprocess
(pps ; (pps
OCanren-ppx.ppx_repr ; OCanren-ppx.ppx_repr
OCanren-ppx.ppx_deriving_reify ; OCanren-ppx.ppx_deriving_reify
OCanren-ppx.ppx_fresh ; OCanren-ppx.ppx_fresh
GT.ppx ; GT.ppx
GT.ppx_all ; GT.ppx_all
OCanren-ppx.ppx_distrib ; OCanren-ppx.ppx_distrib
-- ; --
-pp ; -pp
camlp5/pp5+gt+plugins+ocanren+dump.exe))) ; camlp5/pp5+gt+plugins+ocanren+dump.exe)))

70
model_with_structures/model.typ
View file

@ -112,9 +112,8 @@
{ {
Or[$()$][value of simple type] // `Unit` Or[$()$][value of simple type] // `Unit`
Or[$path$][value from variable] // `Path` Or[$path$][value from variable] // `Path`
// TODO FIXME: expand to support arbitrary paths (that do lead to lvalue) // TODO: decide what is the result of ref expr eval
// add relation to calc lvalue / rvalue for each element ? // Or[$rf expr$][reference expr] // `Ref`
Or[$rf X$][reference expr] // `Ref`
Or[$[expr+]$][tuple expr] // `Prod` Or[$[expr+]$][tuple expr] // `Prod`
} }
), ),
@ -653,7 +652,7 @@ $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: [ unit expr value], name: [ unit value type],
$vals, mu texpre () eqmu 0$, $vals, mu texpre () eqmu 0$,
) )
@ -662,26 +661,32 @@ $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: [ path expr value], name: [ path type],
$vals, mu tval p eqmu v$, $vals, mu tval p eqmu v$,
$vals, mu texpre p eqmu v$, $vals, mu texpre p eqmu v$,
) )
)) ))
#align(center, prooftree( // NOTE: tmp removed
vertical-spacing: 4pt, // #align(center, prooftree(
rule( // vertical-spacing: 4pt,
name: [ ref expr value], // rule(
// name: [ unit value type],
$vals, mu texpre rf x eqmu rf vals[x]$, // $vals, mu texpre e : t$,
)
)) // [*TODO*],
// // TODO: reference to what ??
// $vals, mu texpre rf e eqmu rf ??$,
// )
// ))
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ tuple expr value], name: [ unit value type],
$vals, mu texpre e_1 eqmu v_1$, $vals, mu texpre e_1 eqmu v_1$,
$...$, $...$,
@ -699,7 +704,7 @@ $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: [ unit value expr type], name: [ unit value type],
$types texprt () : cl Read, NotWrite cr$, $types texprt () : cl Read, NotWrite cr$,
) )
@ -708,26 +713,29 @@ $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: [ path expr type], name: [ path type],
$types ttype p : t$, $types ttype p : t$,
$types texprt p : t$, $types texprt p : t$,
) )
)) ))
#align(center, prooftree( // NOTE: tmp removed
vertical-spacing: 4pt, // #align(center, prooftree(
rule( // vertical-spacing: 4pt,
name: [ ref expr type], // rule(
// name: [ unit value type],
$types texprt rf x : rf Ref types[x]$, // $types texprt e : t$,
) // // TODO: why Ref mode ?? <- due to immutability ??
)) // $types texprt rf e : rf Ref t$,
// )
// ))
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ tuple expr type], name: [ unit value type],
$types texprt e_1 : t_1$, $types texprt e_1 : t_1$,
$...$, $...$,
@ -920,21 +928,7 @@ $s in stmt, f in X, x in X, a in X$
rule( rule(
name: [ full spoil for tuple expr], name: [ full spoil for tuple expr],
// NOTE: x as path $e = [e_1, ... e_n]$,
$mu stretch(=>)^(m space t space x)_(cl vals, types cr) mu'$,
// TODO:: is c important ?
$mu stretch(=>)^(m space rf c t space rf x_(cl vals, types cr) mu'$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ full spoil for tuple expr],
$mu_0 stretch(=>)^(m space t_1 space e_1)_(cl vals, types cr) mu_1$, $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_(n - 1) stretch(=>)^(m space t_n space e_n)_(cl vals, types cr) mu_n$,

1105
model_with_structures/synthesizer.ml
View file

File diff suppressed because it is too large Load diff