diff --git a/model_with_control_flow/abstract_domain_model.typ b/model_with_control_flow/abstract_domain_model.typ deleted file mode 100644 index 4194f3a..0000000 --- a/model_with_control_flow/abstract_domain_model.typ +++ /dev/null @@ -1,448 +0,0 @@ -// #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 семантику в формат collecting semantics* -i -Нужно будет добавить во write-flag модальности: `not write` | `may write` | `always write` - -Добавление condition-исполнения - выбор из нескольких блоков. Варианты: -- & of | of & -вложенные блоки ? -- добавить несколько альтернативны тел функциям. Но тогда придётся при трансляции if-блоки выносить в функции - -Лямбды - нужно тоже будет как-то находить лямбды и ля них тоже синтезировать атрибуты -вызов лямбд будет нужен в модели? -- lambda-аргумент - вложенные теги?, должна быть одна и та же сигнтура -можно ввести отдельные сигнатуры-определения? - -проблема простой семантики: вызов лямбд: могут быть модифицируемые функции - -== Синтаксис - -#h(10pt) - -#let isCorrect = `isCorrect` - -#let isRead = `isRead` -#let isAlwaysWrite = `isAlwaysWrite` -#let isPossibleWrite = `isPossibleWrite` -#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[$square$ Write][in all cases there is a write to passed variable] // always write, requre at least one write in each flow variant - Or[$diamond$ Write][in some cases there is a write to passed variable] // possible write, no requirements (?) - Or[$not$ Write][] } ), // no write, require n owrites in all flow variants - Prod(`copy`, - { Or[Ref][pass reference to the value] - Or[Value][pass copy of the 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 (always)] - Or[$X$][cell with possible value or $bot$] - Or[$bot$][spoiled cell (always)] - } - ), - // 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] - Or[`CHOICE` #overline(`stmt`) #overline(`stmt`)][control flow operator, xecution of one of the blocks] - // NOTE: var: replaced with arguments (use rvalue as init) (?) - // Or[`VAR`][variables inside functions] // NOTE: no modifiers required, because it is in the new memory ?? // TODO: not required ?? - // NOTE: lambda: compile to call to the funciton with CHOICE between possible lambda bodies <- do this analysis inside synthesizer ? - } - ), - Prod( - `decl`, - { - Or[$overline(stmt)$][function body] - Or[$lambda #[`tag` #h(3pt)] a.$ `decl`][argument 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 -> isAlwaysWrite tag$, // NOTE; strong requirment should write - $isRead tag -> isIn tag$, - $isPossibleWrite tag and (isOut tag or not isCopy tag) -> isAlwaysWrite sigma(x)$, // NOTE: may tag => should sigma(x) - $isRead tag -> mu (sigma(x)) != bot and mu (sigma(x)) != X$, // NOTE: may tag -> ... - // TODO: FIXME: != Bot and != X ??? or just != Bot ??? - - $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$, - - $isPossibleWrite 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$, - - $isAlwaysWrite 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$, - $mu[sigma(x)] != X$, - - $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$], - - $isPossibleWrite sigma(x)$, // TODO: FIXME ?? always or possible ?? - - $cl sigma, mu, l cr - xarrow("WRITE" x) - cl sigma, mu[x <- 0], l union {sigma(x)} cr$, - ) -)) - -#h(10pt) - -#let combine = `combine` - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ CHOICE $overline(s)$ $overline(t)$], - - $cl sigma, mu, l cr - attach(stretch(->)^overline(s), tr: *) - cl sigma_s, mu_s, l_s cr$, - - $cl sigma, mu, l cr - attach(stretch(->)^overline(t), tr: *) - cl sigma_t, mu_t, l_t cr$, - - $l_t = l_s$, - $sigma_s = sigma_t$, - - // TODO changes ?? two ways ?? - $cl sigma, mu, l cr - xarrow("CHOICE" overline(s) space overline(t)) - cl sigma, combine(mu_s, mu_t), l cr$, - ) -)) - -#h(10pt) - -$ combine(mu_1, mu_2)[i] = combine_e (mu_1[i], mu_2[i]) $ -$ combine_e (bot, bot) = bot $ -$ combine_e (0, 0) = 0 $ -$ combine_e (\_, \_) = X $ - -] diff --git a/model_with_control_flow/analyzer.ml b/model_with_control_flow/analyzer.ml index 54b753c..3280f85 100644 --- a/model_with_control_flow/analyzer.ml +++ b/model_with_control_flow/analyzer.ml @@ -60,9 +60,8 @@ struct let state_combine (left : state) (right : state) : state = match left, right with (lenv, lmem, lmem_len, lvisited), (renv, rmem, rmem_len, rvisited) -> - if lenv != renv || lmem_len != rmem_len then raise Incompatible_states - else (lenv, memory_combine lmem rmem, lmem_len, List.append lvisited rvisited) - (* TODO: union visited lists instead ? *) + if lenv != renv || lmem_len != rmem_len || lvisited != rvisited then raise Incompatible_states + else (lenv, memory_combine lmem rmem, lmem_len, List.append lvisited rvisited) (* TODO: union visited lists instead ? *) (* --- *) @@ -518,22 +517,6 @@ struct (* --- *) - (* TODO: more Combine statement tests *) - - let%expect_test "simple function call with value arg and choice, rw" = - eval_prog ([([wi_value], [Choice ([Write 0; Read 0], [Write 0]); Read 0])], ([wi_value], [Write 0; Call (0, [0]) ])); - Printf.printf "done!"; - [%expect {| done! |}] - - let%expect_test "simple function call with ref arg and choice, rw" = - try (eval_prog ([([ri_ref], [Choice ([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 and choice, rr" = - eval_prog ([([ri_ref], [Choice ([Read 0], [Read 0; Read 0])])], ([wi_value], [Write 0; Call (0, [0]) ])); - Printf.printf "done!"; - [%expect {| done! |}] + (* TODO: combine statement tests *) end diff --git a/model_with_control_flow/model.typ b/model_with_control_flow/model.typ index 02e5e7a..d4a8119 100644 --- a/model_with_control_flow/model.typ +++ b/model_with_control_flow/model.typ @@ -94,8 +94,8 @@ Prod( `decl`, { - Or[overline(stmt)][function body] - Or[$lambda #[`tag` #h(3pt)] a.$ `decl`][argument with argument pass strategy annotation] + Or[ovreline(stmt)][function body] + Or[$lambda #[`tag` #h(3pt) `argtype`] a.$ `decl`][argument with argument pass strategy annotation] } ), Prod( @@ -167,8 +167,7 @@ $d space @ space overline(x)$ - запись применения функции $isOut tag -> isAlwaysWrite tag$, // NOTE; strong requirment should write $isRead tag -> isIn tag$, $isPossibleWrite tag and (isOut tag or not isCopy tag) -> isAlwaysWrite sigma(x)$, // NOTE: may tag => should sigma(x) - $isRead tag -> mu (sigma(x)) != bot and mu (sigma(x)) != X$, // NOTE: may tag -> ... - // TODO: FIXME: != Bot and != X ??? or just != Bot ??? + $isRead tag -> mu (sigma(x)) != bot$, // NOTE: may tag -> ... $isCorrect_(cl sigma, mu cr) (tag, x)$, ) @@ -407,7 +406,7 @@ $d space @ space overline(x)$ - запись применения функции $cl sigma, mu, l cr xarrow("WRITE" x) - cl sigma, mu[x <- 0], l cr$, + 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 index 02d5250..a66b74b 100644 --- a/model_with_control_flow/synthesizer.ml +++ b/model_with_control_flow/synthesizer.ml @@ -190,9 +190,9 @@ struct module Stmt = struct [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [%%ocanren_inject - type nonrec ('d, 'dl, 'sl) t = Call of 'd * 'dl | Read of 'd | Write of 'd | Choice of 'sl * 'sl + type nonrec ('d, 'dl) t = Call of 'd * 'dl | Read of 'd | Write of 'd [@@deriving gt ~options:{ show; gmap }] - type ground = (Nat.ground, Nat.ground List.ground, ground List.ground) t + type nonrec ground = (Nat.ground, Nat.ground List.ground) t ] module Test = struct @@ -260,7 +260,7 @@ struct module Value = struct [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] [%%ocanren_inject - type nonrec t = Unit | Undef | Bot + type nonrec t = Unit | Bot [@@deriving gt ~options:{ show; gmap }] type nonrec ground = t ] @@ -290,51 +290,6 @@ struct end end - (* --- *) - - let rec list_zip_witho f xs ys zs = ocanren { - { fresh x, xs', y, ys', z, zs' in - xs == x :: xs' & - ys == y :: ys' & - zs == z :: zs' & - f x y z & - list_zip_witho f xs' ys' zs' } | - { fresh x, xs' in - xs == x :: xs' & - ys == [] & - zs == [] } | - { fresh y, ys' in - xs == [] & - ys == y :: ys' & - zs == [] } | - { xs == [] & ys == [] & zs == [] } - } - - (* --- *) - - let value_combineo left right res = let open Value in ocanren { - { left == Unit & right == Unit & res == Unit } | - { left == Bot & right == Bot & res == Bot } | - { left == Unit & right == Bot & res == Undef } | - { left == Bot & right == Unit & res == Undef } - } - - let memory_combineo left right res = ocanren { - list_zip_witho value_combineo left right res - } - - let state_combineo left right res = let open St in ocanren { - fresh lenv, lmem, lmem_len, lvisited, renv, rmem, rmem_len, rvisited, res_mem in - left == St (lenv, lmem, lmem_len, lvisited) & - right == St (renv, rmem, rmem_len, rvisited) & - lenv == renv & lmem_len == rmem_len & - memory_combineo lmem rmem res_mem & - res == St (lenv, rmem, lmem_len, List.appendo lvisited rvisited) - (* TODO: union visited lists instead ? *) - } - - (* --- *) - let rec list_replaceo xs id value ys = ocanren { (* xs == [] & ys == [] | (* NOTE: error *) *) { fresh x, xs' in @@ -346,7 +301,7 @@ struct 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 @@ -627,10 +582,7 @@ struct stmt == Write id & env_geto state id tag _mem_id & is_may_writeo tag & - mem_seto state id Unit state' } | - { fresh xs, ys in - stmt == Choice (xs, ys) } - (* TODO: FIXME: choice actions *) + mem_seto state id Unit state' } } and eval_body_foldero prog state stmt state' = diff --git a/model_with_structures/.gitignore b/model_with_structures/.gitignore deleted file mode 100644 index a136337..0000000 --- a/model_with_structures/.gitignore +++ /dev/null @@ -1 +0,0 @@ -*.pdf diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml deleted file mode 100644 index 54b753c..0000000 --- a/model_with_structures/analyzer.ml +++ /dev/null @@ -1,539 +0,0 @@ -module Functional = -struct - - (* --- types --- *) - - type data = int - - type read_cap = Rd | NRd - type write_cap = AlwaysWr | MayWr | NeverWr - 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 | Choice of stmt list * stmt list - - 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 - exception Incompatible_states - - (* --- static interpreter (no rec) --- *) - - (* TODO: allow data (rvalue) in calls ?? *) - type arg = RValue | LValue of data - type value = UnitV | UndefV | 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 rec list_zip_with f xs ys = match xs, ys with (* TODO: alternative from stdlib *) - | x :: xs, y :: ys -> f x y :: list_zip_with f xs ys - | _, _ -> [] - - (* --- *) - - let value_combine (left : value) (right : value) : value = match left, right with - | UnitV, UnitV -> UnitV - | BotV, BotV -> BotV - | _, _ -> UndefV (* NOTE: should be expanded in relational interpreter to not use ineq (?) *) - - let memory_combine (left : value list) (right : value list) : value list = - list_zip_with value_combine left right - - let state_combine (left : state) (right : state) : state = match left, right with - (lenv, lmem, lmem_len, lvisited), (renv, rmem, rmem_len, rvisited) -> - if lenv != renv || lmem_len != rmem_len then raise Incompatible_states - else (lenv, memory_combine lmem rmem, lmem_len, List.append lvisited rvisited) - (* TODO: union visited lists instead ? *) - - (* --- *) - - let is_read (tag : tag) : bool = match tag with - | (Rd, _, _, _, _) -> true - | _ -> false - - let is_always_write (tag : tag) : bool = match tag with - | (_, AlwaysWr, _, _, _) -> true - | _ -> false - - let is_may_write (tag : tag) : bool = match tag with - | (_, AlwaysWr, _, _, _) -> true - | (_, MayWr, _, _, _) -> true - | _ -> false - - let is_never_write (tag : tag) : bool = match tag with - | (_, NeverWr, _, _, _) -> true - | _ -> false - - let is_copy (tag : tag) : bool = match tag with - | (_, _, Cp, _, _) -> true - | _ -> false - - let is_in (tag : tag) : bool = match tag with - | (_, _, _, In, _) -> true - | _ -> false - - let is_out (tag : tag) : bool = match tag with - | (_, _, _, _, Out) -> true - | _ -> 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_always_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_may_write arg_tag > is_always_write parent_tag (* TODO: FIXME: not updated semantics ?? *) - 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 is_never_write tag then state (* TODO: FIXME: check *) - else match is_out tag with - | true -> if not @@ is_always_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_may_write parent_tag then raise @@ Incorrect_const_cast id (* TODO: check that may modifier correct *) - 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_may_write @@ fst @@ env_get state id - then mem_set state id UnitV - else raise @@ Incorrect_const_cast id - | Choice (xs, ys) -> let state_x = eval_body state prog xs in - let state_y = eval_body state prog ys in - state_combine state_x state_y - (* TODO: FIXME: additional may write / always write checks ?? *) - - 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, AlwaysWr, Cp, In, NOut) - let rmwi_value : tag = (Rd, MayWr, Cp, In, NOut) - let ri_value : tag = (Rd, NeverWr, Cp, In, NOut) - let wi_value : tag = (NRd, AlwaysWr, Cp, In, NOut) - let mwi_value : tag = (NRd, MayWr, Cp, In, NOut) - let i_value : tag = (NRd, NeverWr, Cp, In, NOut) - let rwi_ref : tag = (Rd, AlwaysWr, NCp, In, NOut) - let rmwi_ref : tag = (Rd, MayWr, NCp, In, NOut) - let ri_ref : tag = (Rd, NeverWr, NCp, In, NOut) - let wi_ref : tag = (NRd, AlwaysWr, NCp, In, NOut) - let mwi_ref : tag = (NRd, MayWr, NCp, In, NOut) - let i_ref : tag = (NRd, NeverWr, 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. *) - - (* --- *) - - (* TODO: more Combine statement tests *) - - let%expect_test "simple function call with value arg and choice, rw" = - eval_prog ([([wi_value], [Choice ([Write 0; Read 0], [Write 0]); Read 0])], ([wi_value], [Write 0; Call (0, [0]) ])); - Printf.printf "done!"; - [%expect {| done! |}] - - let%expect_test "simple function call with ref arg and choice, rw" = - try (eval_prog ([([ri_ref], [Choice ([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 and choice, rr" = - eval_prog ([([ri_ref], [Choice ([Read 0], [Read 0; Read 0])])], ([wi_value], [Write 0; Call (0, [0]) ])); - Printf.printf "done!"; - [%expect {| done! |}] - -end diff --git a/model_with_structures/dune b/model_with_structures/dune deleted file mode 100644 index 4b2faf8..0000000 --- a/model_with_structures/dune +++ /dev/null @@ -1,64 +0,0 @@ -; (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_cf tests_f_cf) - (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_cf) - (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_structures/model.typ b/model_with_structures/model.typ deleted file mode 100644 index 428e355..0000000 --- a/model_with_structures/model.typ +++ /dev/null @@ -1,457 +0,0 @@ -// #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: проверить, что всё нужное добавлено* -*TODO: добавить сложные структуры (типы) и работу с ними* -*TODO: добавить тип лямбд (тип с id сигнатуры)* -*TODO: добавить тип вызова поля структуры* -*TODO: добавить правльную работу со вложенными тегами, path-доступ к полям переменных, корректность пути* - -Нужно будет добавить во write-flag модальности: `not write` | `may write` | `always write` - -Добавление condition-исполнения - выбор из нескольких блоков. Варианты: -- & of | of & -вложенные блоки ? -- добавить несколько альтернативны тел функциям. Но тогда придётся при трансляции if-блоки выносить в функции - -Лямбды - нужно тоже будет как-то находить лямбды и ля них тоже синтезировать атрибуты -вызов лямбд будет нужен в модели? -- lambda-аргумент - вложенные теги?, должна быть одна и та же сигнтура -можно ввести отдельные сигнатуры-определения? - -проблема простой семантики: вызов лямбд: могут быть модифицируемые функции - -== Синтаксис - -#h(10pt) - -#let isCorrect = `isCorrect` - -#let isRead = `isRead` -#let isAlwaysWrite = `isAlwaysWrite` -#let isPossibleWrite = `isPossibleWrite` -#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` -#let path = `path` -#let argtype = `argtype` -#let argmem = `argmem` -#bnf( - Prod(`read`, - { Or[Read][read passed value] - Or[Not Read][] } ), - Prod(`write`, - { Or[$square$ Write][in all cases there is a write to passed variable] // always write, requre at least one write in each flow variant - Or[$diamond$ Write][in some cases there is a write to passed variable] // possible write, no requirements (?) - Or[$not$ Write][] } ), // no write, require n owrites in all flow variants - Prod(`copy`, - { Or[Ref][pass reference to the value] - Or[Value][pass copy of the 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 (always)] - Or[$X$][cell with possible value or $bot$] - Or[$bot$][spoiled cell (always)] - } - ), - Prod( - `path`, - { - Or[$x$][fuction argument or variable itself] - Or[$path . n$][access $n$-th cell of the tuple] - Or[$path : n$][access $n$-th cell of the union] // TODO: another notation ?? - } - ), - Prod( - `argtype`, - { - Or[$()$][simple type representing all primitive types] // `Unit` - Or[\& #h(3pt) `tag` #h(3pt) `argtype`][reference to structure, contains copy / ref choice] // `Ref` - Or[`argtype` $times$ `argtype`][pair type, allows to make tuples] // `Prod` - // Or[`argtype` $+$ `argtype`][union type (important in some way ???)] // `Sum` // TODO ? - Or[$F_x$][type of lambda or function pointer, defined by function declaration id] // `Fun` - } - ), - Prod( - `argmem`, - { - Or[$[m]$][memory id for simple type variable] // `Unit` - Or[\& #h(3pt) `tag` #h(3pt) `argmem`][reference to structure, contains copy / ref choice] // `Ref` - Or[`argmem` $times$ `argmem`][pair type, allows specify memory for tuples] // `Prod` - // Or[`argmem` $+$ `argmem`][union type (important in some way ???)] // `Sum` // TODO ? - Or[$F_m$][memory for lambda or function pointer, defined by function declaration id] // `Fun` // why separated ?? - } - ), - // Prod( - // `arg`, - // { - // Or[$0$][new value, no associated variable] - // Or[$ amp d$][value from some variable] - // } - // ), - Prod( - `stmt`, - { - Or[`CALL` $f space overline(path)$][call function by id] - Or[`CALL_LAM` $path space overline(path)$][call lambda funciton (variable or funcitona argument field)] - Or[`WRITE` $path$][write to variable] - Or[`READ` $path$][read from variable] - // TODO: or introduce block statement ?? // vars definiiton statment ?? - // (for example, for same named vars in nested spaces) - Or[`CHOICE` #overline(`stmt`) #overline(`stmt`)][control flow operator, xecution of one of the blocks] - // NOTE: var: replaced with arguments (use rvalue as init) (?) - // Or[`VAR`][variables inside functions] // NOTE: no modifiers required, because it is in the new memory ?? // TODO: not required ?? - // NOTE: lambda: compile to call to the funciton with CHOICE between possible lambda bodies <- do this analysis inside synthesizer ? - } - ), - Prod( - `decl`, - { - Or[$overline(stmt)$][function body] - Or[$lambda #[`argtype`] a.$ `decl`][argument 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 -> argmem$ - #[ позиции памяти, соответстующие переменным контекста, - частично определённая функция ] - -$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 ?? - -// TODO: FIXME: define typeof operation -#let typeof = `typeof` - -// TODO: FIXME: define access operation -// TODO: two versions: write with change & read -#let access = `access` - -// TODO: FIXME: define argtag operation -#let argtag = `argtag` - -// TODO: FIXME: define addpaths operation: ~> - -// FIXME -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ is correct], - $isOut tag -> isAlwaysWrite tag$, // NOTE; strong requirment should write - $isRead tag -> isIn tag$, - $isPossibleWrite tag and (isOut tag or not isCopy tag) -> isAlwaysWrite argtag(sigma, x)$, // NOTE: may tag => should sigma(x) - $isRead tag -> access(mu, sigma, x) != bot and access(mu, sigma, x) != X$, - - $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$, - - $isPossibleWrite tag$, // NOTE: weak requirement: may write - $not isCopy tag$, - $not isOut tag$, - - $isCorrect_(cl sigma, mu cr) (tag, x)$, - - // gamma - memory (as mu) - $gamma stretch(=>)^((tag, x) : args)_sigma access(gamma, sigma, x) <- bot]$ - ) -)) - -#h(10pt) - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ fix step], - - $mu stretch(=>)^args_sigma gamma$, - - $isAlwaysWrite tag$, // NOTE: strong requirement: should write - $isOut tag$, - - $isCorrect_(cl sigma, mu cr) (tag, x)$, - - // gamma - memory (as mu) - $gamma stretch(=>)^((tag, x) : args)_sigma access(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) - -// TODO: special operation to add all paths one by one ?? - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ $(lambda a. d) x$], - - $cl sigma, mu, l cr - stretch(~>)^a - cl sigma, mu', l' cr$, - - $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 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: [ CALL_LAM $y space overline(x)$], - - $typeof(y) = F_f$, - - $cl sigma, mu, l cr - xarrow("CALL" f space overline(x)) - cl sigma, gamma, l cr$, - - $cl sigma, mu, l cr - xarrow("CALL_LAM" y space overline(x)) - cl sigma, gamma, l cr$, - ) -)) - -#h(10pt) - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ READ $x$], - - $access(mu, sigma, x) != bot$, - $access(mu, sigma, x) != X$, - - $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$], - - $isPossibleWrite sigma(x)$, // TODO: FIXME ?? always or possible ?? - - $cl sigma, mu, l cr - xarrow("WRITE" x) - cl sigma, access(mu, sigma, x) <- 0, l cr$, - ) -)) - -#h(10pt) - -#let combine = `combine` - -#align(center, prooftree( - vertical-spacing: 4pt, - rule( - name: [ CHOICE $overline(s)$ $overline(t)$], - - $cl sigma, mu, l cr - attach(stretch(->)^overline(s), tr: *) - cl sigma_s, mu_s, l_s cr$, - - $cl sigma, mu, l cr - attach(stretch(->)^overline(t), tr: *) - cl sigma_t, mu_t, l_t cr$, - - $l_t = l_s$, - $sigma_s = sigma_t$, - - // TODO changes ?? two ways ?? - $cl sigma, mu, l cr - xarrow("CHOICE" overline(s) space overline(t)) - cl sigma, combine(mu_s, mu_t), l cr$, - ) -)) - -#h(10pt) - -$ combine(mu_1, mu_2)[i] = combine_e (mu_1[i], mu_2[i]) $ -$ combine_e (bot, bot) = bot $ -$ combine_e (0, 0) = 0 $ -$ combine_e (\_, \_) = X $ - -] diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml deleted file mode 100644 index 02d5250..0000000 --- a/model_with_structures/synthesizer.ml +++ /dev/null @@ -1,704 +0,0 @@ -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 = AlwaysWr | MayWr | NeverWr - [@@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, AlwaysWr, 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, NeverWr, 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, AlwaysWr, 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, NeverWr, 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, AlwaysWr, 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, NeverWr, 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, AlwaysWr, 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, NeverWr, 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_always_writeo tag = let open WriteCap in ocanren { - fresh r_, c_, i_, o_ in - tag == Tag (r_, AlwaysWr, c_, i_, o_) } - let is_may_writeo tag = let open WriteCap in ocanren { - fresh r_, c_, i_, o_ in - { tag == Tag (r_, AlwaysWr, c_, i_, o_) | - tag == Tag (r_, MayWr, c_, i_, o_) } } - let is_never_writeo tag = let open WriteCap in ocanren { - fresh r_, c_, i_, o_ in - tag == Tag (r_, NeverWr, 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, NeverWr, 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, 'sl) t = Call of 'd * 'dl | Read of 'd | Write of 'd | Choice of 'sl * 'sl - [@@deriving gt ~options:{ show; gmap }] - type ground = (Nat.ground, Nat.ground List.ground, 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 | Undef | 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_zip_witho f xs ys zs = ocanren { - { fresh x, xs', y, ys', z, zs' in - xs == x :: xs' & - ys == y :: ys' & - zs == z :: zs' & - f x y z & - list_zip_witho f xs' ys' zs' } | - { fresh x, xs' in - xs == x :: xs' & - ys == [] & - zs == [] } | - { fresh y, ys' in - xs == [] & - ys == y :: ys' & - zs == [] } | - { xs == [] & ys == [] & zs == [] } - } - - (* --- *) - - let value_combineo left right res = let open Value in ocanren { - { left == Unit & right == Unit & res == Unit } | - { left == Bot & right == Bot & res == Bot } | - { left == Unit & right == Bot & res == Undef } | - { left == Bot & right == Unit & res == Undef } - } - - let memory_combineo left right res = ocanren { - list_zip_witho value_combineo left right res - } - - let state_combineo left right res = let open St in ocanren { - fresh lenv, lmem, lmem_len, lvisited, renv, rmem, rmem_len, rvisited, res_mem in - left == St (lenv, lmem, lmem_len, lvisited) & - right == St (renv, rmem, rmem_len, rvisited) & - lenv == renv & lmem_len == rmem_len & - memory_combineo lmem rmem res_mem & - res == St (lenv, rmem, lmem_len, List.appendo lvisited rvisited) - (* TODO: union visited lists instead ? *) - } - - (* --- *) - - 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_always_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_never_writeo arg_tag | { is_may_writeo arg_tag & is_may_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 & - { is_not_reado tg | { is_reado tg & mem_checko state_before id } } & - { { is_never_writeo tg & state == state'} | - { is_always_writeo tg & - is_outo tg & is_may_writeo parent_tg & mem_seto state id Unit state' } | - { is_may_writeo tg & { - { is_not_outo tg & is_valueo tg & state == state' } | - { is_not_outo tg & is_refo tg & is_may_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_may_writeo tag & - mem_seto state id Unit state' } | - { fresh xs, ys in - stmt == Choice (xs, ys) } - (* TODO: FIXME: choice actions *) - } - - 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_structures/tests.ml b/model_with_structures/tests.ml deleted file mode 100644 index 8017884..0000000 --- a/model_with_structures/tests.ml +++ /dev/null @@ -1,61 +0,0 @@ -open Tests_f -open Synthesizer -open Relational - -(* type tests *) -let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, 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, AlwaysWr, Ref, In, NOut); Tag (Rd, AlwaysWr, 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, NeverWr, 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, AlwaysWr, 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, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, 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, AlwaysWr, Ref, In, NOut), O))], [Unit], S (O), [])] |}] -let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [])] |}] -let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, 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, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] -let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, 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, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)] |}] -let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Ref, In, NOut)] |}] -let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]; [Tag (NRd, AlwaysWr, Ref, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]] |}] -let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Tag (NRd, AlwaysWr, 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_structures/tests_f.ml b/model_with_structures/tests_f.ml deleted file mode 100644 index 5427966..0000000 --- a/model_with_structures/tests_f.ml +++ /dev/null @@ -1,509 +0,0 @@ -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_never_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_never_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_never_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 3476d96..9810f9f 100644 --- a/simplest_model_with_mods/model.typ +++ b/simplest_model_with_mods/model.typ @@ -383,7 +383,7 @@ $d space @ space overline(x)$ - запись применения функции $cl sigma, mu, l cr xarrow("WRITE" x) - cl sigma, mu[x <- 0], l cr$, + cl sigma, mu[x <- 0], l union {sigma(x)} cr$, ) ))