st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-04-26 16:24:50 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

init new separate mode to implement control flow

Browse source
This commit is contained in:
ProgramSnail 2026-03-15 14:24:43 +00:00
parent 036322903b
commit df26d40669
8 changed files with 2173 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

1
model_with_control_flow/.gitignore vendored Normal file
View file

@ -0,0 +1 @@
*.pdf

478
model_with_control_flow/analyzer.ml Normal file
View file

@ -0,0 +1,478 @@
module Functional =
struct
(* --- types --- *)
type data = int
type read_cap = Rd | NRd
type write_cap = Wr | NWr
type copy_cap = Cp | NCp
type in_cap = In | NIn
type out_cap = Out | NOut
type tag = read_cap * write_cap * copy_cap * in_cap * out_cap
type stmt = Call of data * data list | Read of data | Write of data
type body = stmt list
type fun_decl = tag list * body
type prog = fun_decl list * fun_decl
(* --- exceptions --- *)
exception Incorrect_memory_access of int
exception Ref_rvalue_argument of int
exception Incorrect_const_cast of int
exception Invalid_argument_tag of int
(* --- static interpreter (no rec) --- *)
(* TODO: allow data (rvalue) in calls ?? *)
type arg = RValue | LValue of data
type value = UnitV | BotV (* NOTE: RefV of data - not needed for now *)
type env = (int * (tag * data)) list
(* env * memory * last unused memory * visited functions *)
type state = env * value list * int * int list
(* --- *)
let is_read (tag : tag) : bool = match tag with
| (Rd, _, _, _, _) -> true
| (NRd, _, _, _, _) -> false
let is_write (tag : tag) : bool = match tag with
| (_, Wr, _, _, _) -> true
| (_, NWr, _, _, _) -> false
let is_copy (tag : tag) : bool = match tag with
| (_, _, Cp, _, _) -> true
| (_, _, NCp, _, _) -> false
let is_in (tag : tag) : bool = match tag with
| (_, _, _, In, _) -> true
| (_, _, _, NIn, _) -> false
let is_out (tag : tag) : bool = match tag with
| (_, _, _, _, Out) -> true
| (_, _, _, _, NOut) -> 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 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
let env_get (state : state) (id : data) : (tag * data) =
match state with (env, _mem, _mem_len, _visited) -> List.assoc id env
let env_add (state : state) (id : data) (mode : tag) (mem_id : data) : state = match state with
(env, mem, mem_len, visited) -> let env = (id, (mode, mem_id)) :: env in
(env, mem, mem_len, visited)
let inv_id (mem_len : int) (id : data) : data = mem_len - id - 1
let mem_get (state : state) (id : data) : value = match state with
(_env, mem, mem_len, _visited) -> List.nth mem @@ inv_id mem_len @@ snd @@ env_get state id
let mem_set (state : state) (id : data) (value : value) : state = match state with
(env, mem, mem_len, visited) -> let mem_id = inv_id mem_len @@ snd @@ env_get state id in
let mem = list_replace mem mem_id value in (env, mem, 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) (id : data) : unit =
if mem_get state id == BotV then raise @@ Incorrect_memory_access id else ()
let arg_to_value (state : state) (arg : arg) : value = match arg with
| RValue -> UnitV
| LValue id -> mem_get state id
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_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_write arg_tag > is_write parent_tag
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 not @@ is_write tag then state
else match is_out tag with
| true -> if not @@ is_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_write parent_tag then raise @@ Incorrect_const_cast id
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_write @@ fst @@ env_get state id
then mem_set state id UnitV
else raise @@ Incorrect_const_cast id
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, Wr, Cp, In, NOut)
let ri_value : tag = (Rd, NWr, Cp, In, NOut)
let wi_value : tag = (NRd, Wr, Cp, In, NOut)
let i_value : tag = (NRd, NWr, Cp, In, NOut)
let rwi_ref : tag = (Rd, Wr, NCp, In, NOut)
let ri_ref : tag = (Rd, NWr, NCp, In, NOut)
let wi_ref : tag = (NRd, Wr, NCp, In, NOut)
let i_ref : tag = (NRd, NWr, NCp, In, NOut)
(* >> tests without functions *)
let%expect_test "empty" =
eval_prog ([], ([], []));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "ref param in main failure" =
try (eval_prog ([], ([i_ref], []));
[%expect.unreachable])
with Ref_rvalue_argument id -> Printf.printf "%i" id;
[%expect {| 0 |}]
let%expect_test "read empty args" =
try (eval_prog ([], ([], [Read 0]));
[%expect.unreachable])
with Not_found -> Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "write empty args" =
try (eval_prog ([], ([], [Write 0]));
[%expect.unreachable])
with Not_found -> Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "simple write" =
eval_prog ([], ([wi_value], [Write 0]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "simple read" = (* NOTE: should not work with read-before-write check*)
eval_prog ([], ([ri_value], [Read 0]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "multiple read & write" =
eval_prog ([], ([rwi_value], [Write 0; Read 0; Write 0; Write 0; Read 0; Read 0]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "multiple read & write, multiple args" =
eval_prog ([], ([wi_value; wi_value; wi_value], [Write 0; Read 0; Write 1; Write 0; Write 2; Read 1; Write 2; Read 0; Read 2]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "main, access out of range" =
try(eval_prog ([], ([wi_value], [Write 0; Read 5 ]));
[%expect.unreachable])
with Not_found -> Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "main, access out of range" =
try(eval_prog ([], ([wi_value], [Write 0; Write 5 ]));
[%expect.unreachable])
with Not_found -> Printf.printf "done!";
[%expect {| done! |}]
(* >> tests with one function *)
let%expect_test "simple function call with value arg" =
eval_prog ([([wi_value], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "simple function call with ref arg" =
eval_prog ([([wi_ref], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "function with value arg & read" =
eval_prog ([([wi_value], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Read 0 ]));
Printf.printf "done!";
[%expect {| done! |}]
(* --- *)
let%expect_test "function with ref arg & read" =
try (eval_prog ([([rwi_ref], [Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Read 0 ]));
[%expect.unreachable])
with Incorrect_memory_access id -> Printf.printf "%i" id;
[%expect {| 0 |}]
let%expect_test "function with ref arg & call twice" =
try (eval_prog ([([rwi_ref], [Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Call (0, [0]) ]));
[%expect.unreachable])
with Incorrect_memory_access id -> Printf.printf "%i" id;
[%expect {| 0 |}]
(* NOTE: behaviour is fixed with new capabilities *)
let%expect_test "function with ref arg, write first & call twice" =
eval_prog ([([wi_ref], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Call (0, [0]) ]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "function with ref arg & read, write" =
try (eval_prog ([([rwi_ref], [Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Read 0; Write 0 ]));
[%expect.unreachable])
with Incorrect_memory_access id -> Printf.printf "%i" id;
[%expect {| 0 |}]
let%expect_test "function with ref arg & write, read" =
eval_prog ([([rwi_ref], [Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Write 0; Read 0 ]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "function with ref arg, no write inside & read" =
eval_prog ([([ri_ref], [Read 0; Read 0])], ([wi_value], [Write 0; Call (0, [0]); Read 0 ]));
Printf.printf "done!";
[%expect {| done! |}]
(* --- *)
let%expect_test "function with value arg, read out of range" =
try(eval_prog ([([ri_ref], [Read 0; Read 1])], ([wi_value; i_value], [Write 0; Call (0, [0]); Read 0 ]));
[%expect.unreachable])
with Not_found -> Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "function with ref arg, read out of range" =
try(eval_prog ([([ri_ref], [Read 0; Read 1])], ([wi_value; i_value], [Write 0; Call (0, [0]); Read 0 ]));
[%expect.unreachable])
with Not_found -> Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "function with value arg, write out of range" =
try(eval_prog ([([rwi_value], [Read 0; Write 1])], ([wi_value; i_value], [Write 0; Call (0, [0]); Read 0 ]));
[%expect.unreachable])
with Not_found -> Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "function with value arg, call out of range" =
try(eval_prog ([([ri_value], [Read 0])], ([wi_value; i_value], [Write 0; Call (0, [2]); Read 0 ]));
[%expect.unreachable])
with Not_found -> Printf.printf "done!";
[%expect {| done! |}]
(* --- *)
let%expect_test "function with ref & value args, no write inside & read" =
eval_prog (
[([ri_ref; ri_value], [Read 0; Read 1])],
([wi_value; wi_value], [Write 0; Write 1; Call (0, [0; 1]); Read 0; Read 1 ]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "function with ref & value args, write value inside & read" =
eval_prog (
[([ri_ref; rwi_value], [Read 0; Read 1; Write 1; Read 1])],
([wi_value; wi_value], [Write 0; Write 1; Call (0, [0; 1]); Read 0; Read 1 ]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "function with ref & value args, write both inside & read" =
try (eval_prog (
[([rwi_ref; rwi_value],[Read 0; Read 1; Write 0; Write 1; Read 1])],
([wi_value; wi_value], [Write 0; Write 1; Call (0, [0; 1]); Read 0; Read 1 ]));
[%expect.unreachable])
with Incorrect_memory_access id -> Printf.printf "%i" id;
[%expect {| 0 |}]
(* --- *)
(* NOTE: maybe important case in the future *)
let%expect_test "function with ref two same ref args, read both & read" =
eval_prog (
[([ri_ref; ri_ref],[Read 0; Read 1; Read 1])],
([wi_value], [Write 0; Call (0, [0; 0]); Read 0 ]));
Printf.printf "done!";
[%expect {| done! |}]
(* NOTE: changed semantics by comporasion with prev analyzer, new test *)
let%expect_test "function with ref two same ref args, read both & nothing" =
eval_prog (
[([ri_ref; ri_ref],[Read 0; Read 1; Read 1])],
([wi_value], [Write 0; Call (0, [0; 0]); ]));
Printf.printf "done!";
[%expect {| done! |}]
(* NOTE: changed semantics by comporasion with prev analyzer, new test *)
let%expect_test "function with ref & copy of the same arg, read & write both & nothing" =
eval_prog (
[([rwi_ref; rwi_value],[Read 0; Read 1; Write 0; Write 1; Read 1])],
([wi_value], [Write 0; Call (0, [0; 0]); ]));
Printf.printf "done!";
[%expect {| done! |}]
(* NOTE: changed semantics by comporasion with prev analyzer, new test *)
let%expect_test "function with copy & ref of the same arg, read & write both & nothing" =
eval_prog (
[([rwi_value; rwi_ref],[Read 0; Read 1; Write 0; Write 1; Read 1])],
([wi_value], [Write 0; Call (0, [0; 0]); ]));
Printf.printf "done!";
[%expect {| done! |}]
(* TODO: FIXME: now correct (use state before for mem check), is this good ?, proper way to fix ? *)
(* NOTE: maybe important case in the future *)
let%expect_test "function with ref two same ref args, read & write both, error" =
(* try ( *)
eval_prog (
[([rwi_ref; rwi_ref],[Read 0; Read 1; Write 0; Write 1; Read 1])],
([wi_value], [Write 0; Call (0, [0; 0]); ]));
(* [%expect.unreachable]) *)
(* with Incorrect_memory_access id -> Printf.printf "%i" id; *)
(* [%expect {| 0 |}] *)
Printf.printf "done!";
[%expect {| done! |}]
(* >> tests with several functions *)
let%expect_test "two functions with ref arg, read func -> write func" =
eval_prog (
[([ri_ref], [Read 0]); ([wi_ref], [Write 0])],
([wi_value], [Write 0; Call (0, [0]); Read 0; Call (1, [0]) ]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "two functions with ref arg, write func -> read func" =
try (eval_prog (
[([ri_ref], [Read 0]); ([wi_ref], [Write 0])],
([wi_value], [Write 0; Call (1, [0]); Call (0, [0]) ]));
[%expect.unreachable])
with Incorrect_memory_access id -> Printf.printf "%i" id;
[%expect {| 0 |}]
let%expect_test "two functions: ref arg after value arg" =
eval_prog (
[([rwi_ref], [Read 0; Write 0]); ([rwi_value], [Read 0; Write 0])],
([wi_value], [Write 0; Call (1, [0]); Read 0; Call (0, [0]) ]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "two functions: value arg after spoiled ref arg" =
try (eval_prog (
[([rwi_ref], [Read 0; Write 0]); ([rwi_value], [Read 0; Write 0])],
([wi_value], [Write 0; Call (0, [0]); Call (1, [0]) ]));
[%expect.unreachable])
with Incorrect_memory_access id -> Printf.printf "%i" id;
[%expect {| 0 |}]
(* --- *)
let%expect_test "simple function call with value arg, const cast error" =
try (eval_prog ([([ri_value], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ]));
[%expect.unreachable])
with Incorrect_const_cast id -> Printf.printf "%i" id;
[%expect {| 0 |}]
let%expect_test "simple function call with ref arg, const cast error" =
try (eval_prog ([([ri_ref], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ]));
[%expect.unreachable])
with Incorrect_const_cast id -> Printf.printf "%i" id;
[%expect {| 0 |}]
let%expect_test "simple function call with value arg, const cast ok" =
eval_prog ([([ri_value], [Read 0])], ([wi_value], [Write 0; Call (0, [0]) ]));
Printf.printf "done!";
[%expect {| done! |}]
let%expect_test "simple function call with ref arg, const cast ok" =
eval_prog ([([ri_ref], [Read 0])], ([wi_value], [Write 0; Call (0, [0]) ]));
Printf.printf "done!";
[%expect {| done! |}]
(* --- *)
let%expect_test "simple function call with arg, recursive calls" =
eval_prog ([([rwi_value], [Write 0; Read 0; Write 0; Call (0, [0])])], ([wi_value], [Write 0; Call (0, [0]) ]));
Printf.printf "done!";
[%expect {| done! |}]
(* --- *)
(* TODO: out arguments test, etc. *)
end

64
model_with_control_flow/dune Normal file
View file

@ -0,0 +1,64 @@
; (env
; (_
; (flags
; (:standard -warn-error +5))))
(library
(name analyzer_cf)
(modules analyzer)
(flags (-rectypes))
(libraries OCanren OCanren.tester)
(inline_tests)
(wrapped false)
(preprocess
(pps GT.ppx GT.ppx_all ppx_expect ppx_inline_test)))
(library
(name tests_cf)
(modules tests)
(flags (-rectypes))
(libraries synthesizer_mods tests_f_mods)
(inline_tests)
(wrapped false)
(preprocess
(pps ppx_expect ppx_inline_test)))
(library
(name tests_f_cf)
(modules tests_f)
(flags (-rectypes))
(libraries OCanren OCanren.tester synthesizer_mods)
(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_cf)
(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)))

407
model_with_control_flow/model.typ Normal file
View file

@ -0,0 +1,407 @@
// #import "@preview/polylux:0.4.0": *
#import "@preview/simplebnf:0.1.1": *
// #import "@preview/zebraw:0.5.0": *
// #show: zebraw
#import "@preview/curryst:0.6.0": rule, prooftree, rule-set
#import "@preview/xarrow:0.4.0": xarrow, xarrowDashed
= Формальная модель используемого языка
*TODO: добавить лямбды, control flow, локальные переменные в каком-то виде*
*TODO: проблемы с добавлением if в будущем: как записать write and not write ?*
Нужно будет добавить во write-flag модальности: `not write` | `may write` | `always write`
Добавление condition-исполнения - выбор из нескольких блоков. Варианты:
- & of | of & -вложенные блоки ?
- добавить несколько альтернативны тел функциям. Но тогда придётся при трансляции if-блоки выносить в функции
Лямбды - нужно тоже будет как-то находить лямбды и ля них тоже синтезировать атрибуты
вызов лямбд будет нужен в модели?
- lambda-аргумент - вложенные теги?, должна быть одна и та же сигнтура
можно ввести отдельные сигнатуры-определения?
проблема простой семантики: вызов лямбд: могут быть модифицируемые функции
== Синтаксис
#h(10pt)
#let isCorrect = `isCorrect`
#let isRead = `isRead`
#let isWrite = `isWrite`
#let isRef = `isRef`
#let isCopy = `isCopy`
#let isIn = `isIn`
#let isOut = `isOut`
#let tag = `tag`
#let value = `value`
#let stmt = `stmt`
#let decl = `decl`
#let prog = `prog`
#bnf(
Prod(`read`,
{ Or[Read][read passed value]
Or[Not Read][] } ),
Prod(`write`,
{ Or[Write][write to passed variable]
Or[Not Write][] } ),
Prod(`copy`,
{ Or[Ref][pass reference to the value]
Or[Value][pass copy of te value] } ),
Prod(`in`,
{ Or[In][parameter value used as input]
Or[Not In][] } ),
Prod(`out`,
{ Or[Out][parametr value returned]
Or[Not Out][] } ),
Prod(
`tag`,
{
Or[`read` #h(3pt) `write` #h(3pt) `copy` #h(3pt) `in` #h(3pt) `out`][]
}
),
Prod(
`value`,
{
Or[$0$][cell with some value]
Or[$bot$][spoiled cell]
}
),
// Prod(
// `arg`,
// {
// Or[$0$][new value, no associated variable]
// Or[$ amp d$][value from some variable]
// }
// ),
Prod(
`stmt`,
{
Or[`CALL` $f space overline(x)$][call function by id]
Or[`WRITE` $x$][write to variable]
Or[`READ` $x$][read from variable]
}
),
Prod(
`decl`,
{
Or[ovreline(stmt)][function body]
Or[$lambda #[`tag`] a.$ `decl`][with argument pass strategy annotation]
}
),
Prod(
`prog`,
{
Or[`decl`][main function]
Or[`decl` `prog`][with supplimentary funcitons]
}
),
)
== Семантика статического интерпретатора
#h(10pt)
$V := value$ - значения памяти
$L := NN$ - позиции в памяти
$X$ - можество переменных
*TODO: специфицировать доступ*
*TODO: формально описать accessor-ы tag*
$sigma : X -> tag times L$ - #[ позиции памяти, соответстующие переменным контекста,
частично определённая функция ]
$mu : NN -> V$ - память, частично определённая функция
$l in NN$ - длина используемого фрагмента памяти
$DD : NN -> decl$ - определения функций, частично определённая функция
$d in decl, s in stmt, f in NN, x in X, a in NN$
$d space @ space overline(x)$ - запись применения функции (вида #decl) к аргументам
#let args = `args`
#[
#let ref = `ref`
#let copy = `copy`
#let read = `read`
#let cl = $chevron.l$
#let cr = $chevron.r$
// #align(center, grid(
// columns: 3,
// gutter: 5%,
// align(bottom, prooftree(
// ...
// )),
// align(bottom, prooftree(
// ...
// )),
// align(bottom, prooftree(
// ...
// )),
// ))
// TODO: introduce spep env argument ??
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ is correct],
$isOut tag -> isWrite tag$, // NOTE; strong requirment should write
$isRead tag -> isIn tag$,
$isWrite tag and (isOut tag or not isCopy tag) -> isWrite sigma(x)$, // NOTE: may tag => should sigma(x)
$isRead tag -> mu (sigma(x)) != bot$, // NOTE: may tag -> ...
$isCorrect_(cl sigma, mu cr) (tag, x)$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ spoil init],
$mu stretch(=>)^nothing_(cl sigma, mu cr) mu$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ spoil step],
$mu stretch(=>)^args_sigma gamma$,
$isWrite tag$, // NOTE: weak requirement: may write
$not isCopy tag$,
$not isOut tag$,
$isCorrect_(cl sigma, mu cr) (tag, x)$,
// mu
$gamma stretch(=>)^((tag, x) : args)_sigma gamma[sigma(x) <- bot]$
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ fix step],
$mu stretch(=>)^args_sigma gamma$,
$isWrite tag$, // NOTE: strong requirement: should write
$isOut tag$,
$isCorrect_(cl sigma, mu cr) (tag, x)$,
// mu
$gamma stretch(=>)^((tag, x) : args)_sigma gamma[sigma(x) <- 0]$
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ skip step],
$mu stretch(=>)^args_sigma gamma$,
$not "spoil step"$,
$not "fix step"$,
$isCorrect_(cl sigma, mu cr) (tag, x)$,
// mu
$gamma stretch(=>)^((tag, x) : args)_sigma gamma$
)
))
#h(10pt)
#align(center, line())
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ $(lambda tag a. d) x, ref + read$],
$cl sigma, mu, l cr
xarrowDashed(d space @ space overline(y))
cl sigma, mu', l' cr$,
$isRead tag$,
$not isCopy tag$,
// NOTE: correctness checked in CALL f
$cl sigma, mu, l cr
xarrowDashed((lambda tag a. d) space @ space x space overline(y))
cl sigma, mu', l' cr$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ $(lambda tag a. d) x, ref - read$],
$cl sigma, mu [sigma(x) <- bot], l cr
xarrowDashed(d space @ space overline(y))
cl sigma, mu', l' cr$,
$not isRead tag$,
$not isCopy tag$,
// NOTE: correctness checked in CALL f
$cl sigma, mu, l cr
xarrowDashed((lambda tag a. d) space @ space x space overline(y))
cl sigma, mu', l' cr$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ $(lambda tag a. d) x, copy + read$],
$cl sigma [a <- l], mu [l <- 0], l + 1 cr
xarrowDashed(d space @ space overline(y))
cl sigma', mu', l' cr$,
$isRead tag$,
$isCopy tag$,
// NOTE: correctness checked in CALL f
$cl sigma, mu, l cr
xarrowDashed((lambda tag a. d) space @ space x space overline(y))
cl sigma', mu', l' cr$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ $(lambda tag a. d) x, copy - read$],
$cl sigma [a <- l], mu [l <- bot], l + 1 cr
xarrowDashed(d space @ space overline(y))
cl sigma', mu', l' cr$,
$not isRead tag$,
$isCopy tag$,
// NOTE: correctness checked in CALL f
$cl sigma, mu, l cr
xarrowDashed((lambda tag a. d) space @ space x space overline(y))
cl sigma', mu', l' cr$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [decl body],
$cl sigma, mu, l cr
attach(stretch(->)^overline(s), tr: *)
cl sigma', mu', l' cr$,
$d = overline(s)$,
$cl sigma, mu, l cr
xarrowDashed(d space @)
cl sigma', mu', l' cr$,
)
))
#h(10pt)
#align(center, line())
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ CALL $f space overline(x)$],
$cl [], mu, l cr
xarrowDashed(d space @ space overline(x))
cl sigma', mu', l' cr$,
// TODO: FIXME define args in some way
$mu attach(stretch(=>)^args_sigma, tr: *) gamma$,
$DD(f) := d$,
$cl sigma, mu, l cr
xarrow("CALL" f space overline(x))
cl sigma, gamma, l cr$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ READ $x$],
$mu(sigma(x)) != bot$,
$cl sigma, mu, l cr
xarrow("READ" x)
cl sigma, mu, l cr$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ WRITE $x$],
$isWrite sigma(x)$,
$cl sigma, mu, l cr
xarrow("WRITE" x)
cl sigma, mu[x <- 0], l union {sigma(x)} cr$,
)
))
]

653
model_with_control_flow/synthesizer.ml Normal file
View file

@ -0,0 +1,653 @@
module Relational =
struct
open GT
open OCanren
open OCanren.Std
type data_ground = Nat.ground (* with show, gmap *)
[@@deriving gt ~options:{ show; gmap }]
type data_logic = Nat.logic
[@@deriving gt ~options:{ show; gmap }]
type data_injected = Nat.injected
module ReadCap = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject
type nonrec t = Rd | NRd
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = t
]
end
module WriteCap = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject
type nonrec t = Wr | NWr
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = t
]
end
(* NOTE: rename names ?? *)
module CopyCap = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject
type nonrec t = Ref | Val
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = t
]
end
module InCap = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject
type nonrec t = In | NIn
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = t
]
end
module OutCap = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject
type nonrec t = Out | NOut
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = t
]
end
module Tag = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject
type nonrec ('r, 'w, 'c, 'i, 'o) t = Tag of 'r * 'w * 'c * 'i * 'o
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (ReadCap.ground, WriteCap.ground, CopyCap.ground, InCap.ground, OutCap.ground) t
]
(* TODO: less repeats *)
(* common constructors *)
let rwi_val = let open ReadCap in
let open WriteCap in
let open CopyCap in
let open InCap in
let open OutCap in
ocanren { Tag (Rd, Wr, Val, In, NOut) }
let ri_val = let open ReadCap in
let open WriteCap in
let open CopyCap in
let open InCap in
let open OutCap in
ocanren { Tag (Rd, NWr, Val, In, NOut) }
let wi_val = let open ReadCap in
let open WriteCap in
let open CopyCap in
let open InCap in
let open OutCap in
ocanren { Tag (NRd, Wr, Val, In, NOut) }
let i_val = let open ReadCap in
let open WriteCap in
let open CopyCap in
let open InCap in
let open OutCap in
ocanren { Tag (NRd, NWr, Val, In, NOut) }
let rwi_ref = let open ReadCap in
let open WriteCap in
let open CopyCap in
let open InCap in
let open OutCap in
ocanren { Tag (Rd, Wr, Ref, In, NOut) }
let ri_ref = let open ReadCap in
let open WriteCap in
let open CopyCap in
let open InCap in
let open OutCap in
ocanren { Tag (Rd, NWr, Ref, In, NOut) }
let wi_ref = let open ReadCap in
let open WriteCap in
let open CopyCap in
let open InCap in
let open OutCap in
ocanren { Tag (NRd, Wr, Ref, In, NOut) }
let i_ref = let open ReadCap in
let open WriteCap in
let open CopyCap in
let open InCap in
let open OutCap in
ocanren { Tag (NRd, NWr, Ref, In, NOut) }
(* constraints *)
let x_any tag = let open InCap in
let open OutCap in
ocanren { fresh r, w, c in
tag == Tag (r, w, c, NIn, NOut) }
let i_any tag = let open InCap in
let open OutCap in
ocanren { fresh r, w, c in
tag == Tag (r, w, c, In, NOut) }
let o_any tag = let open InCap in
let open OutCap in
ocanren { fresh r, w, c in
tag == Tag (r, w, c, NIn, Out) }
let io_any tag = let open InCap in
let open OutCap in
ocanren { fresh r, w, c in
tag == Tag (r, w, c, In, Out) }
(* accessors *)
let is_reado tag = let open ReadCap in ocanren {
fresh w_, c_, i_, o_ in
tag == Tag (Rd, w_, c_, i_, o_) }
let is_not_reado tag = let open ReadCap in ocanren {
fresh w_, c_, i_, o_ in
tag == Tag (NRd, w_, c_, i_, o_) }
let is_writeo tag = let open WriteCap in ocanren {
fresh r_, c_, i_, o_ in
tag == Tag (r_, Wr, c_, i_, o_) }
let is_not_writeo tag = let open WriteCap in ocanren {
fresh r_, c_, i_, o_ in
tag == Tag (r_, NWr, c_, i_, o_) }
let is_refo tag = let open CopyCap in ocanren {
fresh r_, w_, i_, o_ in
tag == Tag (r_, w_, Ref, i_, o_) }
let is_valueo tag = let open CopyCap in ocanren {
fresh r_, w_, i_, o_ in
tag == Tag (r_, w_, Val, i_, o_) }
let is_ino tag = let open InCap in ocanren {
fresh r_, w_, c_, o_ in
tag == Tag (r_, w_, c_, In, o_) }
let is_not_ino tag = let open InCap in ocanren {
fresh r_, w_, c_, o_ in
tag == Tag (r_, w_, c_, NIn, o_) }
let is_outo tag = let open OutCap in ocanren {
fresh r_, w_, c_, i_ in
tag == Tag (r_, w_, c_, i_, Out) }
let is_not_outo tag = let open OutCap in ocanren {
fresh r_, w_, c_, i_ in
tag == Tag (r_, w_, c_, i_, NOut) }
let eq_copyo tag cp = let open CopyCap in ocanren {
fresh r_, w_, i_, o_ in
tag == Tag (r_, w_, cp, i_, o_) }
module Test = struct
@type answer = logic GT.list with show
let test _ = show(answer) (Stream.take (run q (fun q -> let open ReadCap in
let open WriteCap in
let open CopyCap in
let open InCap in
let open OutCap in
ocanren {q == Tag (Rd, NWr, Ref, In, NOut)})
(fun q -> q#reify reify)))
end
end
module Stmt = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject
type nonrec ('d, 'dl) t = Call of 'd * 'dl | Read of 'd | Write of 'd
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (Nat.ground, Nat.ground List.ground) t
]
module Test = struct
@type answer = Nat.ground List.ground GT.list with show
@type answer' = ground GT.list with show
let test1 _ = show(answer) (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == Call (1, q)})
(fun q -> q#reify (List.prj_exn Nat.prj_exn))))
let test2 _ = show(answer') (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == q})
(fun q -> q#reify (prj_exn))))
end
end
module FunDecl = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject
type nonrec ('l, 'b) t = FunDecl of 'l * 'b
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (Tag.ground List.ground, Stmt.ground List.ground) t
]
module Test = struct
@type answer = ground GT.list with show
let test _ = show(answer) (Stream.take (run q (fun q -> let open Tag in
let open Stmt in
ocanren {FunDecl ([rwi_ref; rwi_val], [Call (1, [0]); Write 1]) == q})
(fun q -> q#reify (prj_exn))))
end
end
module Prog = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject
type nonrec ('l, 'f) t = Prog of 'l * 'f
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (FunDecl.ground List.ground, FunDecl.ground) t
]
module Test = struct
@type answer = ground GT.list with show
let test _ = show(answer) (Stream.take (run q (fun q -> let open FunDecl in
let open Tag in
let open Stmt in
ocanren {Prog ([], FunDecl ([ri_val], [Write 0; Read 0])) == q})
(fun q -> q#reify (prj_exn))))
end
end
module Arg = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject
type nonrec 'd t = RValue | LValue of 'd
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = Nat.ground t
]
module Test = struct
@type answer = logic GT.list with show
let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == LValue 3})
(fun q -> q#reify reify)))
end
end
module Value = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject
type nonrec t = Unit | Bot
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = t
]
module Test = struct
@type answer = logic GT.list with show
let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == Bot | q == Unit})
(fun q -> q#reify reify)))
end
end
module St = struct
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
[%%ocanren_inject
type nonrec ('env, 'mem, 'last_mem, 'visited) t = St of 'env * 'mem * 'last_mem * 'visited
[@@deriving gt ~options:{ show; gmap }]
type nonrec ground = (((Nat.ground, ((Tag.ground, Nat.ground) Pair.ground)) Pair.ground) List.ground,
Value.ground List.ground, Nat.ground, Nat.ground List.ground) t
]
module Test = struct
@type answer = ground GT.list with show
let test _ = show(answer) (Stream.take (run q (fun q -> let open Value in
let open Tag in
ocanren {St ([Std.pair 0 (Std.pair rwi_val 0)], [Bot], 1, [0]) == q})
(fun q -> q#reify (prj_exn))))
end
end
let rec list_replaceo xs id value ys = ocanren {
(* xs == [] & ys == [] | (* NOTE: error *) *)
{ fresh x, xs' in
xs == x :: xs' &
id == Nat.o &
ys == value :: xs' } |
{ fresh x, xs', id', ys' in
xs == x :: xs' &
id == Nat.s id' &
ys == x :: ys' &
list_replaceo xs' id' value ys' }
}
let env_geto state id tag' mem_id' =
let open St in
ocanren {
fresh env, _mem, _mem_len, _visited, elem in
state == St (env, _mem, _mem_len, _visited) &
List.assoco id env elem &
Std.pair tag' mem_id' == elem
}
let env_addo state id tg mem_id state' =
let open St in
ocanren {
fresh env, env', mem, mem_len, visited, elem in
state == St (env, mem, mem_len, visited) &
Std.pair tg mem_id == elem &
(Std.pair id elem) :: env == env' &
state' == St (env', mem, mem_len, visited)
}
let inv_ido mem_len id id' = ocanren {
fresh inv_id_inc in
Nat.addo inv_id_inc id mem_len &
Nat.addo id' 1 inv_id_inc
}
(* --- *)
let rec list_ntho xs id x' = ocanren {
(* xs == [] | (* NOTE: error *) *)
{ fresh y', xs' in
id == Nat.o &
y' :: xs' == xs &
x' == y' } |
{ fresh id', y', xs' in
Nat.s id' == id &
y' :: xs' == xs &
list_ntho xs' id' x' }
}
let mem_geto state id value' =
let open St in
ocanren {
fresh mem, mem_len, mem_id, mem_id_inv, _env, _visited, _tag in
state == St (_env, mem, mem_len, _visited) &
env_geto state id _tag mem_id &
inv_ido mem_len mem_id mem_id_inv &
list_ntho mem mem_id_inv value'
}
let mem_seto state id value state'=
let open St in
ocanren {
fresh env, mem, mem_len, visited, mem_id, inv_mem_id, mem', _tag in
state == St (env, mem, mem_len, visited) &
env_geto state id _tag mem_id &
inv_ido mem_len mem_id inv_mem_id &
list_replaceo mem inv_mem_id value mem' &
state' == St (env, mem', mem_len, visited)
}
let mem_addo state value state' =
let open St in
ocanren {
fresh env, mem, mem_len, mem_len', visited, mem' in
state == St (env, mem, mem_len, visited) &
mem' == value :: mem &
mem_len' == Nat.s mem_len &
state' == St (env, mem', mem_len', visited)
}
let mem_checko state id =
let open Value in
ocanren {
mem_geto state id Unit
}
(* --- *)
let rec list_foldlo f acc xs acc' = ocanren {
xs == [] & acc' == acc |
{ fresh x', xs', acc_upd in
xs == x' :: xs' &
list_foldlo f acc xs' acc_upd &
f acc_upd x' acc' }
}
let rec list_foldro f acc xs acc' = ocanren {
xs == [] & acc' == acc |
{ fresh x', xs', acc_upd in
xs == x' :: xs' &
f acc x' acc_upd &
list_foldro f acc_upd xs' acc' }
(* TODO: inf search on swap, investigate *)
}
let rec list_foldr2o f acc xs ys acc' = ocanren {
xs == [] & ys == [] & acc' == acc |
{ fresh x', xs', y', ys', acc_upd in
xs == x' :: xs' &
ys == y' :: ys' &
f acc x' y' acc_upd &
list_foldr2o f acc_upd xs' ys' acc' }
}
let rec list_foldl2o f acc xs ys acc' = ocanren {
xs == [] & ys == [] & acc' == acc |
{ fresh x', xs', y', ys', acc_upd in
xs == x' :: xs' &
ys == y' :: ys' &
list_foldl2o f acc xs' ys' acc_upd &
f acc_upd x' y' acc' }
}
let arg_to_valueo state arg value' =
let open Arg in
let open Value in
ocanren {
arg == RValue & value' == Unit |
{ fresh id in
arg == LValue id &
mem_geto state id value' }
}
let arg_to_rvalueo arg value' =
let open Arg in
let open Tag in
ocanren { is_valueo arg & value' == RValue }
let st_mem_leno state mem_len' =
let open St in
ocanren {
fresh _env, _mem, _visited in
state == St (_env, _mem, mem_len', _visited)
}
let tag_correcto tg =
let open Tag in
ocanren {
{is_not_outo tg | { is_outo tg & is_writeo tg } } &
{is_not_reado tg | { is_reado tg & is_ino tg } }
}
let st_add_argo state state_before id arg_tag arg state'' =
(* let open Nat in *)
let open Value in
let open Arg in
let open Tag in
ocanren {
tag_correcto arg_tag & {
{ fresh value', state', mem_len_prev' in
is_valueo arg_tag &
arg_to_valueo state_before arg value' &
mem_addo state value' state' &
st_mem_leno state mem_len_prev' &
env_addo state' id arg_tag mem_len_prev' state'' } |
{ fresh arg', parent_tag, mem_id, state' in
is_refo arg_tag &
(* { arg == RValue } *) (* NOTE: not allowed for now *)
arg == LValue arg' &
env_geto state_before id parent_tag mem_id &
env_addo state id arg_tag mem_id state' &
{ is_not_writeo arg_tag | { is_writeo arg_tag & is_writeo parent_tag } } &
{
{ is_reado arg_tag & state' == state'' } |
{ is_not_reado arg_tag & mem_seto state' id Bot state'' }
}
}
}
}
let st_spoil_foldero state_before state tg id state' =
let open Value in
let open Tag in
let open St in
ocanren {
fresh env, mem, mem_len, _visited, parent_tg, _mem_id in
state == St (env, mem, mem_len, _visited) &
env_geto state id parent_tg _mem_id &
(* NOTE: replaced with later condition (this one needs fix) *)
(* { is_not_writeo tg | { is_writeo tg & is_writeo parent_tg } } & *)
{ is_not_reado tg | { is_reado tg & mem_checko state_before id } } &
{ { is_not_writeo tg & state == state'} |
{ is_writeo tg & {
{ is_outo tg & is_writeo parent_tg & mem_seto state id Unit state' } |
{ is_not_outo tg & is_valueo tg & state == state' } |
{ is_not_outo tg & is_refo tg & is_writeo parent_tg & mem_seto state id Bot state' }
} }
}
}
let st_spoil_by_argso state arg_tags args state' =
ocanren {
fresh state_before in
state == state_before & (* TODO: required ? *)
list_foldl2o (st_spoil_foldero state_before) state arg_tags args state'
}
(* let st_spoil_assignmentso state state' = *)
(* let open St in *)
(* ocanren { *)
(* fresh _env, _mem, _mem_len, visited in *)
(* state == St (_env, _mem, _mem_len, visited) & *)
(* list_foldlo st_spoil_foldero state visited state' *)
(* } *)
(* --- *)
let arg_to_lvalueo arg arg' =
let open Arg in
ocanren { arg' == LValue arg }
let rec list_dropo n xs xs' = ocanren {
xs == [] & xs' == [] |
n == Nat.o & xs == xs' & xs =/= [] |
{ fresh n', _y, ys in
Nat.s n' == n &
xs == _y :: ys &
list_dropo n' ys xs' }
}
let rec list_not_membero xs x = ocanren {
xs == [] |
{ fresh x', xs' in
xs == x' :: xs' &
x' =/= x &
list_not_membero xs' x }
}
let visited_checko state f_id =
let open St in
ocanren {
fresh _env, _mem, _mem_len, visited in
state == St (_env, _mem, _mem_len, visited) &
List.membero visited f_id
}
let not_visited_checko state f_id =
let open St in
ocanren {
fresh _env, _mem, _mem_len, visited in
state == St (_env, _mem, _mem_len, visited) &
list_not_membero visited f_id
}
let visited_addo state f_id state' =
let open St in
ocanren {
fresh env, mem, mem_len, visited, visited' in
state == St (env, mem, mem_len, visited) &
visited' == f_id :: visited &
state' == St (env,mem, mem_len, visited')
}
let rec eval_stmto state prog stmt state' =
let open Stmt in
let open Value in
let open FunDecl in
let open Tag in
ocanren {
{ fresh f_id, args, f, args', state_after_call, arg_tags, _body in
stmt == Call (f_id, args) &
list_ntho prog f_id f &
FunDecl (arg_tags, _body) == f &
List.mapo arg_to_lvalueo args args' &
(* TODO: FIXME: memoisation, do not do calls on check successfull *)
(* NOTE: tmp simplification for less branching (TODO?) *)
{ { fresh state_with_visited in
not_visited_checko state f_id &
visited_addo state f_id state_with_visited &
eval_funo state_with_visited prog f args' state_after_call } |
{ visited_checko state f_id &
state_after_call == state } } &
st_spoil_by_argso state_after_call arg_tags args state' } |
{ fresh id in stmt == Read id & mem_checko state id & state == state' } |
{ fresh id, tag, _mem_id in
stmt == Write id &
env_geto state id tag _mem_id &
is_writeo tag &
mem_seto state id Unit state' }
}
and eval_body_foldero prog state stmt state' =
eval_stmto state prog stmt state'
and eval_bodyo state prog body state' =
list_foldro (eval_body_foldero prog) state body state'
and add_arg_foldero state_before state_c arg_tag arg state_c' =
ocanren {
fresh state, id, state', id' in
state_c == Std.pair state id &
st_add_argo state state_before id arg_tag arg state' &
id' == Nat.s id &
state_c' == Std.pair state' id'
}
and eval_funo state prog decl args state' =
let open FunDecl in
let open St in
ocanren {
fresh arg_tags, body,
env_before, mem_before, len_before, visited_before,
state_clean,
state_with_vars, _counter,
state_evaled,
_env, _mem, _len, visited,
nil_env, nil_visited in
nil_env == [] &
nil_visited == [] &
decl == FunDecl (arg_tags, body) &
state == St (env_before, mem_before, len_before, visited_before) &
state_clean == St (nil_env, mem_before, len_before, nil_visited) &
list_foldr2o (add_arg_foldero state)
(Std.pair state Nat.o) arg_tags args
(Std.pair state_with_vars _counter) & (* TODO: or foldr2o ?? *)
eval_bodyo state_with_vars prog body state_evaled &
state_evaled == St (_env,_mem, _len, visited) &
state' == St (env_before, mem_before, len_before, visited)
}
and eval_fun_empty_argso state prog decl state' =
let open FunDecl in
ocanren {
fresh arg_tags, args, _body in
decl == FunDecl (arg_tags, _body) &
List.mapo arg_to_rvalueo arg_tags args &
eval_funo state prog decl args state'
}
(* --- *)
let empty_stateo state =
let open St in
ocanren {
fresh nil_env, nil_mem, nil_visited in
nil_env == [] &
nil_visited == [] &
nil_mem == [] &
state == St (nil_env, nil_mem, Nat.o, nil_visited)
}
let eval_progo all_prog state' =
let open Prog in
ocanren {
fresh prog, main_decl, state in
all_prog == Prog (prog, main_decl) &
empty_stateo state &
eval_fun_empty_argso state prog main_decl state'
}
end

61
model_with_control_flow/tests.ml Normal file
View file

@ -0,0 +1,61 @@
open Tests_f
open Synthesizer
open Relational
(* type tests *)
let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NWr, Ref, In, NOut)] |}]
let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}]
let%expect_test "Stmt type test (2)" = print_endline (Stmt.Test.test2 ()); [%expect {| [Call (S (O), [S (S (O))])] |}]
let%expect_test "FunDecl type test" = print_endline (FunDecl.Test.test ()); [%expect {| [FunDecl ([Tag (Rd, Wr, Ref, In, NOut); Tag (Rd, Wr, Val, In, NOut)], [Call (S (O), [O]); Write (S (O))])] |}]
let%expect_test "Prog type test" = print_endline (Prog.Test.test ()); [%expect {| [Prog ([], FunDecl ([Tag (Rd, NWr, Val, In, NOut)], [Write (O); Read (O)]))] |}]
let%expect_test "Arg type test" = print_endline (Arg.Test.test ()); [%expect {| [LValue (S (S (S (O))))] |}]
let%expect_test "Value type test" = print_endline (Value.Test.test ()); [%expect {| [Bot; Unit] |}]
let%expect_test "St type test" = print_endline (St.Test.test ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Bot], S (O), [O])] |}]
(* function tests *)
let%expect_test "inv_id test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}]
let%expect_test "inv_id test 2" = print_endline (inv_id_t2 ()); [%expect {| [S (O)] |}]
let%expect_test "inv_id test 3" = print_endline (inv_id_t3 ()); [%expect {| [S (O)] |}]
let%expect_test "list_drop test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}]
let%expect_test "list_replace test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}]
let%expect_test "arG_to_value test 1" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}]
let%expect_test "st_add_arg test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [])] |}]
let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [])] |}]
let%expect_test "multiple writes eval test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit; Unit], S (S (O)), [])] |}]
let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot], S (O), [O])] |}]
let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [O])] |}]
let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [O])] |}]
let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}]
let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), (Tag (NRd, Wr, Ref, In, NOut), S (O))); (O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}]
let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Unit], S (O), [])] |}]
let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), O))], [Bot], S (O), [])] |}]
let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, (Tag (NRd, Wr, Ref, In, NOut), S (O)))], [Bot; Unit], S (S (O)), [])] |}]
let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, Wr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
let%expect_test "rvalue test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}]
let%expect_test "empty_state test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}]
let%expect_test "function eval test 1" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
let%expect_test "function eval test 2" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}]
let%expect_test "function eval test 3" = print_endline (fun_eval_t3 ()); [%expect {| [] |}]
let%expect_test "function eval test 4" = print_endline (fun_eval_t4 ()); [%expect {| [] |}]
let%expect_test "function eval test 5" = print_endline (fun_eval_t5 ()); [%expect {| [] |}]
let%expect_test "function eval test 6" = print_endline (fun_eval_t6 ()); [%expect {| [St ([], [], O, [O])] |}]
let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
let%expect_test "prog eval test 2" = print_endline (prog_eval_t2 ()); [%expect {| [St ([], [], O, [O])] |}]
let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [O])] |}]
let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}]
let%expect_test "prog eval test 5" = print_endline (prog_eval_t5 ()); [%expect {| [St ([], [], O, [O])] |}]
let%expect_test "prog eval test 6" = print_endline (prog_eval_t6 ()); [%expect {| [] |}]
let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Tag (Rd, Wr, Val, In, NOut); Tag (NRd, Wr, Val, In, NOut)] |}]
let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Tag (NRd, Wr, Val, In, NOut); Tag (NRd, Wr, Ref, In, NOut)] |}]
let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Tag (NRd, Wr, Val, In, NOut); Tag (NRd, Wr, Val, In, NOut)]; [Tag (NRd, Wr, Ref, In, NOut); Tag (NRd, Wr, Val, In, NOut)]] |}]
let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Tag (NRd, Wr, Val, In, NOut)]] |}]
let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Val]; [Ref; Ref]] |}]
let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Ref]; [Ref; Val]] |}]
let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Val; Val]; [Ref; Val]] |}]
let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Val]; [Val; Ref]] |}]
let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}]
let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [O])] |}]

509
model_with_control_flow/tests_f.ml Normal file
View file

@ -0,0 +1,509 @@
open Synthesizer
open Relational
open GT
open OCanren
open OCanren.Std
@type answer = St.ground GT.list with show
@type answerArgs = (Arg.ground List.ground) GT.list with show
@type answerValue = Value.ground GT.list with show
@type answerNat = Nat.ground GT.list with show
@type answerNats = (Nat.ground List.ground) GT.list with show
@type answerTag = Tag.ground GT.list with show
@type answerTags = (Tag.ground List.ground) GT.list with show
@type answerCopyCap = CopyCap.ground GT.list with show
@type answerCopyCaps = (CopyCap.ground List.ground) GT.list with show
let inv_id_t _ = show(answerNat) (Stream.take (run q
(fun q -> ocanren { inv_ido 2 1 q })
(fun q -> q#reify Nat.prj_exn)))
let inv_id_t2 _ = show(answerNat) (Stream.take (run q
(fun q -> ocanren { inv_ido 2 0 q })
(fun q -> q#reify Nat.prj_exn)))
let inv_id_t3 _ = show(answerNat) (Stream.take (run q
(fun q -> ocanren { inv_ido 2 q 0 })
(fun q -> q#reify Nat.prj_exn)))
let list_drop_t _ = show(answerNats) (Stream.take (run q
(fun q -> ocanren { list_dropo 2 [1; 2; 3] q })
(fun q -> q#reify (List.prj_exn Nat.prj_exn))))
let list_replace_t _ = show(answerNats) (Stream.take (run q
(fun q -> ocanren { list_replaceo [1; 2; 3; 4] 1 0 q })
(fun q -> q#reify (List.prj_exn Nat.prj_exn))))
let arg_to_value_t _ = show(answerValue) (Stream.take (run q
(fun q -> let open Arg in
ocanren {
fresh s in
empty_stateo s &
arg_to_valueo s RValue q })
(fun q -> q#reify (Value.prj_exn))))
let st_add_arg_t _ = show(answer) (Stream.take (run q
(fun q -> let open Arg in
let open Tag in
ocanren {
fresh s, s', cnt in
empty_stateo s &
empty_stateo s' &
st_add_argo s s' Nat.o rwi_val RValue q })
(fun q -> q#reify (St.prj_exn))))
let write_eval_t1 _ = show(answer) (Stream.take (run q
(fun q -> let open Arg in
let open Tag in
let open Value in
let open St in
let open Stmt in
let open FunDecl in
ocanren {
fresh s, p, stmt in
s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
stmt == Write 0 &
eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn))))
let write_eval_t2 _ = show(answer) (Stream.take (run q
(fun q -> let open Arg in
let open Tag in
let open Value in
let open St in
let open Stmt in
let open FunDecl in
ocanren {
fresh s, p, stmt in
s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
stmt == Write 1 &
eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn))))
let writes_eval_t _ = show(answer) (Stream.take (run q
(fun q -> let open Arg in
let open Tag in
let open Value in
let open St in
let open Stmt in
let open FunDecl in
ocanren {
fresh s, p, stmts in
s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
stmts == [Write 0; Write 1] &
eval_bodyo s p stmts q})
(fun q -> q#reify (St.prj_exn))))
let call_eval_t1 _ = show(answer) (Stream.take (run q
(fun q -> let open Arg in
let open Tag in
let open Value in
let open St in
let open Stmt in
let open FunDecl in
ocanren {
fresh s, p, stmt in
s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) &
p == [FunDecl ([wi_ref], [Write 0])] &
stmt == Call (0, [0]) &
eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn))))
let call_eval_t2 _ = show(answer) (Stream.take (run q
(fun q -> let open Arg in
let open Tag in
let open Value in
let open St in
let open Stmt in
let open FunDecl in
ocanren {
fresh s, p, stmt in
s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
p == [FunDecl ([wi_ref], [Write 0])] &
stmt == Call (0, [0]) &
eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn))))
let call_eval_t3 _ = show(answer) (Stream.take (run q
(fun q -> let open Arg in
let open Tag in
let open Value in
let open St in
let open Stmt in
let open FunDecl in
ocanren {
fresh s, p, stmt in
s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
p == [FunDecl ([wi_ref], [Write 0])] &
stmt == Call (0, [1]) &
eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn))))
let call_eval_t4 _ = show(answer) (Stream.take (run q
(fun q -> let open Arg in
let open Tag in
let open Value in
let open St in
let open Stmt in
let open FunDecl in
ocanren {
fresh s, p, stmt in
s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
stmt == Call (0, [0; 1]) &
eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn))))
let call_eval_t5 _ = show(answer) (Stream.take (run q
(fun q -> let open Arg in
let open Tag in
let open Value in
let open St in
let open Stmt in
let open FunDecl in
ocanren {
fresh s, p, stmt in
s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
stmt == Call (0, [1; 0]) &
eval_stmto s p stmt q})
(fun q -> q#reify (St.prj_exn))))
let mem_set_t1 _ = show(answer) (Stream.take (run q
(fun q -> let open Arg in
let open Tag in
let open Value in
let open St in
ocanren {
fresh s in
s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Bot], 1, []) &
mem_seto s 0 Unit q})
(fun q -> q#reify (St.prj_exn))))
let mem_set_t2 _ = show(answer) (Stream.take (run q
(fun q -> let open Arg in
let open Tag in
let open Value in
let open St in
ocanren {
fresh s in
s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) &
mem_seto s 0 Bot q})
(fun q -> q#reify (St.prj_exn))))
let meem_set_t3 _ = show(answer) (Stream.take (run q
(fun q -> let open Arg in
let open Tag in
let open Value in
let open St in
ocanren {
fresh s in
s == St ([Std.pair 0 (Std.pair wi_ref 1)], [Unit; Unit], 2, []) &
mem_seto s 0 Bot q})
(fun q -> q#reify (St.prj_exn))))
let add_arg_folder_t _ = show(answer) (Stream.take (run q
(fun q -> let open Arg in
let open Tag in
ocanren {
fresh s, s', cnt in
empty_stateo s &
empty_stateo s' &
add_arg_foldero s (Std.pair s' Nat.o) rwi_val RValue (Std.pair q cnt) })
(fun q -> q#reify (St.prj_exn))))
let foldl2_t _ = show(answer) (Stream.take (run q
(fun q -> let open Arg in
let open Tag in
ocanren {
fresh s, s', cnt, arg_tags, args in
arg_tags == [rwi_val] &
args == [RValue] &
empty_stateo s &
empty_stateo s' &
list_foldl2o (add_arg_foldero s) (Std.pair s' Nat.o) arg_tags args (Std.pair q cnt) })
(fun q -> q#reify (St.prj_exn))))
let rvalue_t _ = show(answerArgs) (Stream.take ~n:3 (run q
(fun q -> let open Arg in
ocanren {fresh v in List.mapo arg_to_rvalueo v q})
(fun q -> q#reify (List.prj_exn Arg.prj_exn))))
(* empty state test *)
let empty_state_t _ = show(answer) (Stream.take (run q
(fun q -> ocanren {empty_stateo q})
(fun q -> q#reify (St.prj_exn))))
(* fun eval test *)
let fun_eval_t1 _ = show(answer) (Stream.take (run q
(fun q -> (* let open Prog in *)
let open FunDecl in
let open Tag in
let open Stmt in
ocanren { fresh s, p, d in
empty_stateo s &
p == [] &
d == FunDecl ([], []) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* fun eval test *)
let fun_eval_t2 _ = show(answer) (Stream.take (run q
(fun q -> (* let open Prog in *)
let open FunDecl in
let open Tag in
let open Stmt in
ocanren { fresh s, p, d in
empty_stateo s &
p == [] &
d == FunDecl ([wi_val], [Write 0; Read 0]) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* fun eval test *)
let fun_eval_t3 _ = show(answer) (Stream.take (run q
(fun q -> (* let open Prog in *)
let open FunDecl in
let open Tag in
let open Stmt in
ocanren { fresh s, p, d in
empty_stateo s &
p == [FunDecl ([wi_ref], [Write 0])] &
d == FunDecl ([wi_val], [Call (0, [0]); Read 0]) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* fun eval test *)
let fun_eval_t4 _ = show(answer) (Stream.take (run q
(fun q -> (* let open Prog in *)
let open FunDecl in
let open Tag in
let open Stmt in
ocanren { fresh s, p, d in
empty_stateo s &
p == [FunDecl ([wi_ref], [Write 0])] &
d == FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* fun eval test *)
let fun_eval_t5 _ = show(answer) (Stream.take (run q
(fun q -> (* let open Prog in *)
let open FunDecl in
let open Tag in
let open Stmt in
ocanren { fresh s, p, d in
empty_stateo s &
p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
d == FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* fun eval test *)
let fun_eval_t6 _ = show(answer) (Stream.take (run q
(fun q -> (* let open Prog in *)
let open FunDecl in
let open Tag in
let open Stmt in
ocanren { fresh s, p, d in
empty_stateo s &
p == [FunDecl ([wi_val], [Write 0])] &
d == FunDecl ([wi_val], [Call (0, [0])]) &
eval_fun_empty_argso s p d q })
(fun q -> q#reify (St.prj_exn))))
(* prog eval test *)
let prog_eval_t1 _ = show(answer) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
ocanren {eval_progo (Prog ([], FunDecl ([wi_val], [Write 0; Read 0]))) q})
(fun q -> q#reify (St.prj_exn))))
(* prog with func eval test *)
let prog_eval_t2 _ = show(answer) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0; Read 0])],
FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q})
(fun q -> q#reify (St.prj_exn))))
(* prog with func eval test *)
let prog_eval_t3 _ = show(answer) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Read 0])],
FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q})
(fun q -> q#reify (St.prj_exn))))
(* prog with func eval test *)
let prog_eval_t4 _ = show(answer) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
(fun q -> q#reify (St.prj_exn))))
(* prog with func eval test *)
let prog_eval_t5 _ = show(answer) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
(fun q -> q#reify (St.prj_exn))))
(* prog with func eval test *)
let prog_eval_t6 _ = show(answer) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
ocanren {eval_progo (Prog ([FunDecl ([ri_val], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
(fun q -> q#reify (St.prj_exn))))
(* annotation gen prog test *)
let synt_t1 _ = show(answerTag) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {i_any q &
eval_progo (Prog ([FunDecl ([q], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Read 0]))) (St ([], [], 0, [0]))})
(fun q -> q#reify (Tag.prj_exn))))
(* annotation gen prog test *)
let synt_t2 _ = show(answerTag) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {i_any q & is_not_reado q &
eval_progo (Prog ([FunDecl ([q], [Write 0])],
FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
(fun q -> q#reify (Tag.prj_exn))))
(* annotation gen prog test *)
let synt_t3 _ = show(answerTags) (Stream.take (run qr
(fun q r -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {i_any q & is_not_reado q & i_any r & is_not_reado r &
eval_progo (Prog ([FunDecl ([q], [Write 0])],
FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
(fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
(* annotation gen prog test *)
let synt_t4 _ = show(answerTags) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {i_any q & is_not_reado q &
eval_progo (Prog ([FunDecl ([q], [Write 0])],
FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, [0]))})
(fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *)
(* annotation gen prog test *)
let synt_t5 _ = show(answerCopyCaps) (Stream.take (run qr
(fun q r -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {fresh q', r' in
i_any q' & is_not_reado q' &
i_any r' & is_not_reado r' & is_not_writeo r' &
eq_copyo q' q & eq_copyo r' r &
eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])],
FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
(fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *)
(* annotation gen prog test *)
let synt_t6 _ = show(answerCopyCaps) (Stream.take (run qr
(fun q r -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {fresh q', r' in
i_any q' & is_not_reado q' &
i_any r' & is_not_reado r' & is_not_writeo r' &
eq_copyo q' q & eq_copyo r' r &
eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])],
FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
(fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *)
(* annotation gen prog test *)
let synt_t7 _ = show(answerCopyCaps) (Stream.take (run qr
(fun q r -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {fresh q', r' in
i_any q' & is_not_reado q' & i_any r' & is_not_reado r' &
eq_copyo q' q & eq_copyo r' r &
eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])],
FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))})
(fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
(* annotation gen prog test *)
let synt_t8 _ = show(answerCopyCaps) (Stream.take (run qr
(fun q r -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {fresh q', r' in
i_any q' & is_not_reado q' & i_any r' & is_not_reado r' &
eq_copyo q' q & eq_copyo r' r &
eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])],
FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))})
(fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
(* annotation gen prog test *)
let synt_t9 _ = show(answerCopyCaps) (Stream.take (run qr
(fun q r -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
let open St in
ocanren {fresh q', r' in
i_any q' & is_not_reado q' &
i_any r' & is_reado r' & is_not_writeo r' &
eq_copyo q' q & eq_copyo r' r &
eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Read 1])],
FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, [0]))})
(fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
(* TODO: FIXME: implement memoization cuts *)
(* prog with recursive function call *)
let rec_eval_t _ = show(answer) (Stream.take (run q
(fun q -> let open Prog in
let open FunDecl in
let open Tag in
let open Stmt in
ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Call (0, [0])])],
FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) q})
(fun q -> q#reify (St.prj_exn))))

15
simplest_model_with_mods/model.typ
View file

@ -7,21 +7,6 @@
= Формальная модель используемого языка = Формальная модель используемого языка
*TODO: проблемы с добавлением if в будущем: как записать write and not write ?*
Нужно будет добавить во write-flag модальности: `not write` | `may write` | `always write`
Добавление condition-исполнения - выбор из нескольких блоков. Варианты:
- & of | of & -вложенные блоки ?
- добавить несколько альтернативны тел функциям. Но тогда придётся при трансляции if-блоки выносить в функции
Лямбды - нужно тоже будет как-то находить лямбды и ля них тоже синтезировать атрибуты
вызов лямбд будет нужен в модели?
- lambda-аргумент - вложенные теги?, должна быть одна и та же сигнтура
можно ввести отдельные сигнатуры-определения?
проблема простой семантики: вызов лямбд: могут быть модифицируемые функции
== Синтаксис == Синтаксис
#h(10pt) #h(10pt)