From df26d406696d3ebf352bcda460e85a463d4741cb Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 15 Mar 2026 14:24:43 +0000 Subject: [PATCH] init new separate mode to implement control flow --- model_with_control_flow/.gitignore | 1 + model_with_control_flow/analyzer.ml | 478 ++++++++++++++++++ model_with_control_flow/dune | 64 +++ model_with_control_flow/model.typ | 407 +++++++++++++++ model_with_control_flow/synthesizer.ml | 653 +++++++++++++++++++++++++ model_with_control_flow/tests.ml | 61 +++ model_with_control_flow/tests_f.ml | 509 +++++++++++++++++++ simplest_model_with_mods/model.typ | 15 - 8 files changed, 2173 insertions(+), 15 deletions(-) create mode 100644 model_with_control_flow/.gitignore create mode 100644 model_with_control_flow/analyzer.ml create mode 100644 model_with_control_flow/dune create mode 100644 model_with_control_flow/model.typ create mode 100644 model_with_control_flow/synthesizer.ml create mode 100644 model_with_control_flow/tests.ml create mode 100644 model_with_control_flow/tests_f.ml diff --git a/model_with_control_flow/.gitignore b/model_with_control_flow/.gitignore new file mode 100644 index 0000000..a136337 --- /dev/null +++ b/model_with_control_flow/.gitignore @@ -0,0 +1 @@ +*.pdf diff --git a/model_with_control_flow/analyzer.ml b/model_with_control_flow/analyzer.ml new file mode 100644 index 0000000..84c6623 --- /dev/null +++ b/model_with_control_flow/analyzer.ml @@ -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 diff --git a/model_with_control_flow/dune b/model_with_control_flow/dune new file mode 100644 index 0000000..279ef77 --- /dev/null +++ b/model_with_control_flow/dune @@ -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))) diff --git a/model_with_control_flow/model.typ b/model_with_control_flow/model.typ new file mode 100644 index 0000000..3db4e2c --- /dev/null +++ b/model_with_control_flow/model.typ @@ -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$, + ) +)) + +] diff --git a/model_with_control_flow/synthesizer.ml b/model_with_control_flow/synthesizer.ml new file mode 100644 index 0000000..3c013ec --- /dev/null +++ b/model_with_control_flow/synthesizer.ml @@ -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 diff --git a/model_with_control_flow/tests.ml b/model_with_control_flow/tests.ml new file mode 100644 index 0000000..b12c028 --- /dev/null +++ b/model_with_control_flow/tests.ml @@ -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])] |}] + diff --git a/model_with_control_flow/tests_f.ml b/model_with_control_flow/tests_f.ml new file mode 100644 index 0000000..8960b38 --- /dev/null +++ b/model_with_control_flow/tests_f.ml @@ -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)))) + diff --git a/simplest_model_with_mods/model.typ b/simplest_model_with_mods/model.typ index 8f8167d..9810f9f 100644 --- a/simplest_model_with_mods/model.typ +++ b/simplest_model_with_mods/model.typ @@ -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)