From 3f6844835c179090bdeffccc74e9d781d7570e48 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 22 Feb 2026 12:58:04 +0000 Subject: [PATCH 1/3] parser: init as ostap sample, modify dune file --- lib/dune | 31 ++++++ lib/parser.ml | 262 ++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 293 insertions(+) create mode 100644 lib/parser.ml diff --git a/lib/dune b/lib/dune index aa69dad..3178596 100644 --- a/lib/dune +++ b/lib/dune @@ -65,6 +65,25 @@ -pp lib/pp5+gt+plugins+ocanren+dump.exe))) +(library + (name parser) + (modules parser) + (flags + ; (-dsource) + (:standard -rectypes)) + (libraries ostap GT) + (preprocessor_deps ./pp5+gt+plugins+ostap+dump.exe) + (wrapped false) + (preprocess + (pps + ppx_expect + ppx_inline_test + GT.ppx + GT.ppx_all + -- + -pp + lib/pp5+gt+plugins+ostap+dump.exe))) + (rule (targets pp5+gt+plugins+ocanren+dump.exe) (action @@ -76,3 +95,15 @@ logger.syntax,GT.syntax,GT.syntax.all,OCanren.syntax -o %{targets}))) + +(rule + (targets pp5+gt+plugins+ostap+dump.exe) + (action + (run + mkcamlp5.opt + -package + camlp5,camlp5.pa_o,camlp5.macro,camlp5.pr_dump,logger.syntax + -package + logger.syntax,GT.syntax,GT.syntax.all,ostap.syntax + -o + %{targets}))) diff --git a/lib/parser.ml b/lib/parser.ml new file mode 100644 index 0000000..dd69b16 --- /dev/null +++ b/lib/parser.ml @@ -0,0 +1,262 @@ +(* +* Samlpe: Ostap sample. +* Copyright (C) 2006-2009 +* Dmitri Boulytchev, St.Petersburg State University +* +* This software is free software; you can redistribute it and/or +* modify it under the terms of the GNU Library General Public +* License version 2, as published by the Free Software Foundation. +* +* This software is distributed in the hope that it will be useful, +* but WITHOUT ANY WARRANTY; without even the implied warranty of +* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. +* +* See the GNU Library General Public License version 2 for more details +* (enclosed in the file COPYING). +*) + +(* This module serves as Ostap tutorial. The important part is expression in the + form ostap (...) (see below), which specified the parsers using a certain + syntax extension +*) +open Ostap +open Matcher + +[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] + +(* Supplementary wrapper: takes a parser, a printer, a string, parses the + string with the parser, and prints the result (if any) with the printer +*) +let parse p pr s = +match Util.parse + (* Makes some default stream with minimal entries *) + (object + inherit Matcher.t s + inherit Util.Lexers.decimal s + inherit Util.Lexers.ident [] s + inherit! Util.Lexers.skip [ + Matcher.Skip.whitespaces " \t\n"; + Matcher.Skip.lineComment "--"; + Matcher.Skip.nestedComment "(*" "*)" + ] s + end) + (ostap (p -EOF)) +with +| `Ok p -> Printf.printf "Parsed : %s\n" @@ pr p +| `Fail er -> Printf.printf "Syntax error: %s\n" er + +(* Supplementary printer combinators *) +let id x = x +let pair f g (x, y) = f x ^ g y +let triple f g h (x, y, z) = f x ^ g y ^ h z +let list f x = List.fold_left (^) "" @@ List.map f x +let option f = function None -> "None" | Some x -> "Some " ^ f x + +(* An overview of the basic combinators: + - sequencing + - attaching semantics + - alternation + - optionality + - iteration +*) +let _ = +(* Sequencing *) +parse (ostap ("a" "b" "c")) (* several items in a row return a tuple of parse values *) + (triple Token.repr Token.repr Token.repr) + "abc"; +parse (ostap ("a" "b" "d")) (* should be parsing error --- "d" is expected, but "c" specified *) + (triple Token.repr Token.repr Token.repr) + "abc"; +parse (ostap ("a" -"b" "c")) (* an item can be skipped from the result by preceding it with "-" *) + (pair Token.repr Token.repr) + "abc"; +parse (ostap ("a" -"b" "c")) (* but the skipped item nevertheless important for parsing *) + (pair Token.repr Token.repr) + "adc"; +parse (ostap (-"(" "a" -")")) (* it is quite usefule to omit a non-important symbols from *) + (* being returned as a result *) + Token.repr + "(a)"; +parse (ostap (-"(" "a" -"b" -")")) (* by the way, whitespaces are allowed anywhere (due to a proper *) + (* stream definition, see object ... end expression above *) + Token.repr + " ( a (* comment *) b (* comment again *) ) "; +parse (ostap ("a" "b" "c" {"nothing"})) (* now, a semantics can be specified; it replaces the default *) + (* return value *) + id + "a b c"; +parse (ostap (x:"a" y:"b" z:"c" {"Something: " ^ (Token.repr x) ^ (Token.repr y) ^ (Token.repr z)})) (* the semantics can make use of a bindings *) + id + "a b c"; +parse (ostap ("a" | "b")) (* besides sequencing, there is an alternation *) + Token.repr + "a"; +parse (ostap ("a" | "b")) (* both branches are matched *) + Token.repr + "b"; +parse (ostap (x:("a" | "b") {"Something: " ^ Token.repr x})) (* grouping is allowed *) + id + "a"; +parse (ostap ("a"?)) (* optional parsing *) + (option Token.repr) + "a"; +parse (ostap ("a"?)) (* optional parsing *) + (option Token.repr) + ""; +parse (ostap (x:"a"? {match x with None -> "None" | Some s -> "Some " ^ Token.repr s})) (* bindings for optional return option type *) + id + "a"; +parse (ostap ("a"*)) (* greedy iteration (zero-or-more) *) + (list Token.repr) + "aaa"; +parse (ostap ("a"+)) (* greedy iteration (one-or-more) *) + (list Token.repr) + "aaa"; +parse (ostap (("a" | "b" | "c")+)) (* of course any parser can be specified as an argument *) + (list Token.repr) + "aa"; +parse (ostap (!(Util.list)[ostap ("a" | "b" | "c")])) (* parsers can be parameterized; ostap expressions can be nested; arbitrary expression can be emdedded *) + (* via the !(...) construct; there are some useful combinators in the Util module --- this one for *) + (* non-empty lists *) + (list Token.repr) + "a, a, b, c, a, b"; +parse (ostap (!(Util.listBy)[ostap (";")][ostap ("a" | "b" | "c")])) (* another useful one: a list with explicitly specified delimiter *) + (list Token.repr) + "a; a; b; c; a; b"; +parse (ostap (x:("a" | "b" | "c") - $(Token.repr x) {"two " ^ Token.repr x ^ "'s"})) (* a $() can be used to parse a dynamically-evaluated *) + (* string; we used "-" to omit the second occurrence of x from being *) + (* returned; note a space between the "-" and the "$(...)" *) + id + "aa";; + +(* This completes the basic combinators overview *) + +(* Among the expression ostap (...) there is a structure item ostap (...) *) +(* to specify a set of mutally-recirsive definitions: *) + +ostap ( +animal : "zeboro" | "cat" | "rabbit" | "giraffe"; +location: "pool" | "bank" | "cafe" | "theater"; +action : "playing" | "eating" | "swimming" | "working"; +phrase : "A" animal "is" action "in" "a" location {"parsed"} +) + +let _ = List.iter (parse phrase id) ["A zeboro is playing in a theater"; + "A cat is eating in a cafe"; + "A rabbit is eating a cat"];; + +(* Now some "real" parsers *) +type expr = Mul of expr * expr | Add of expr * expr | Var of string + +let rec expr_to_string = function +| Var s -> s +| Mul (x, y) -> "(" ^ expr_to_string x ^ " * " ^ expr_to_string y ^ ")" +| Add (x, y) -> "(" ^ expr_to_string x ^ " + " ^ expr_to_string y ^ ")" + +(* Expressions with right-associative binaries *) +module RightAssoc = +struct + + ostap ( + expr : addi; + addi : x:mulli "+" y:addi {Add (x, y)} | mulli; + mulli : x:primary "*" y:mulli {Mul (x, y)} | primary; + primary: x:IDENT {Var x} | -"(" expr -")" + ) + + let _ = List.iter (parse expr expr_to_string) ["a"; "a+b"; "a+b+c"; "a+b*c"; "a+b*c+d"; "(a+b)*c"] + +end + +(* Expressions with left-associative binaries *) +module LeftAssoc = +struct + + [@@@ocaml.warning "-8"] + ostap ( + expr : addi; + addi : :!(Util.listBy)[ostap ("+")][mulli] {List.fold_left (fun x y -> Add (x, y)) x xs}; (* note the use of a pattern for bindings; *) + mulli : :!(Util.listBy)[ostap ("*")][primary] {List.fold_left (fun x y -> Mul (x, y)) x xs}; (* note a space between the "<...>" and the ":" *) + primary: x:IDENT {Var x} | -"(" expr -")" + ) + + let _ = List.iter (parse expr expr_to_string) ["a"; "a+b"; "a+b+c"; "a+b*c"; "a+b*c+d"; "(a+b)*c"] + +end + +(* But better use a custom combinator Util.expr: *) +module ExprExample = +struct + + ostap ( + expr: + !(Util.expr (* The combinator Util.expr takes three arguments: *) + (fun x -> x) (* --- a function, used to transform each parsed subexpression into something; often just an id *) + [| (* --- an array of binary operator specifiers, ordered by the priority in increasing order *) + `Lefta , [ostap ("+"), fun x y -> Add (x, y)]; (* --- each specifier describes the associativity at given priority (one of `Lefta, `Righta, `Nona) *) + `Righta, [ostap ("*"), fun x y -> Mul (x, y)]; (* --- and the list of pairs: *) + |] (* --- the parser for the operator's infix and two-argument function to construct AST node *) + primary (* --- a parser for the primary (simplest form of the expression) *) + ); + + primary: x:IDENT {Var x} | -"(" expr -")" + ) + + let _ = List.iter (parse expr expr_to_string) ["a"; "a+b"; "a+b+c"; "a+b*c"; "a+b*c*e+d"; "(a+b)*c"] + +end + +(* And now some "real-world" example *) +module ShallowLanguageImplemenation = +struct + + let empty x = failwith @@ "Undefined variable " ^ x + let update x v s y = if x = y then v else s y + + let runParser p s = + match Util.parse + (object + inherit Matcher.t s + inherit Util.Lexers.decimal s + inherit Util.Lexers.ident ["if"; "then"; "else"; "fi"; "while"; "do"; "done"] s + inherit! Util.Lexers.skip [ + Matcher.Skip.whitespaces " \t\n"; + Matcher.Skip.lineComment "--"; + Matcher.Skip.nestedComment "(*" "*)" + ] s + end) + (ostap (p -EOF)) + with + | `Ok p -> p + | `Fail er -> failwith @@ Printf.sprintf "Syntax error: %s\n" er + + [@@@ocaml.warning "-8"] + ostap ( + expr: + !(Util.expr + (fun x -> x) + [| + `Nona , [ostap ("=="), (fun x y s -> if x s = y s then 1 else 0)]; + `Lefta , [ostap ("+" ), (fun x y s -> x s + y s); ostap ("-"), (fun x y s -> x s - y s)]; + `Lefta , [ostap ("*" ), (fun x y s -> x s * y s); ostap ("/"), (fun x y s -> x s / y s)] + |] + primary + ); + + primary: x:IDENT {fun s -> s x} | n:DECIMAL {fun s -> n} | -"(" expr -")"; + + simpleStmt: + x:IDENT ":=" e:expr {fun s -> update x (e s) s} + | "if" c:expr "then" s1:stmt "else" s2:stmt "fi" {fun s -> (if c s = 0 then s2 else s1) s} + | "while" c:expr "do" s1:stmt "done" {fun s -> let rec w s = if c s = 0 then s else w (s1 s) in w s}; + + stmt: : !(Util.listBy)[ostap (";")][simpleStmt] {List.fold_left (fun s ss d -> ss @@ s d) s ss} + ) + + let fact = + let f = runParser stmt "result := 1; while 1 - (n == 0) do result := result * n; n := n - 1 done" in + fun n -> (f @@ update "n" n empty) "result" + + let _ = List.iter (fun n -> Printf.printf "fact %d = %d\n" n (fact n)) [1; 2; 3; 4; 5; 6; 7] + +end From 8885c4891c8bf31094a11ca9f1dd1fe728c32843 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 22 Feb 2026 13:17:41 +0000 Subject: [PATCH 2/3] projct structure refactoring --- camlp5/dune | 23 ++++ .../old_model_init.ml | 0 .../simplest_model_init.ml | 0 lib/dune | 109 ------------------ lib/test.ml | 29 ----- .../analyzer.ml | 0 simplest_model/dune | 83 +++++++++++++ {lib => simplest_model}/parser.ml | 0 .../synthesizer.ml | 0 .../tests.ml | 4 +- .../tests_f.ml | 2 +- 11 files changed, 109 insertions(+), 141 deletions(-) create mode 100644 camlp5/dune rename lib/lib_next.ml => experiments/old_model_init.ml (100%) rename lib/lib.ml => experiments/simplest_model_init.ml (100%) delete mode 100644 lib/dune delete mode 100644 lib/test.ml rename lib/semantic_interpreter.ml => simplest_model/analyzer.ml (100%) create mode 100644 simplest_model/dune rename {lib => simplest_model}/parser.ml (100%) rename lib/relational_semantic_interpreter_oc.ml => simplest_model/synthesizer.ml (100%) rename lib/relational_interpreter_oc_tests.ml => simplest_model/tests.ml (98%) rename lib/relational_interpreter_oc_tests_f.ml => simplest_model/tests_f.ml (99%) diff --git a/camlp5/dune b/camlp5/dune new file mode 100644 index 0000000..f0a99a9 --- /dev/null +++ b/camlp5/dune @@ -0,0 +1,23 @@ +(rule + (targets pp5+gt+plugins+ocanren+dump.exe) + (action + (run + mkcamlp5.opt + -package + camlp5,camlp5.pa_o,camlp5.macro,camlp5.pr_dump,logger.syntax + -package + logger.syntax,GT.syntax,GT.syntax.all,OCanren.syntax + -o + %{targets}))) + +(rule + (targets pp5+gt+plugins+ostap+dump.exe) + (action + (run + mkcamlp5.opt + -package + camlp5,camlp5.pa_o,camlp5.macro,camlp5.pr_dump,logger.syntax + -package + logger.syntax,GT.syntax,GT.syntax.all,ostap.syntax + -o + %{targets}))) diff --git a/lib/lib_next.ml b/experiments/old_model_init.ml similarity index 100% rename from lib/lib_next.ml rename to experiments/old_model_init.ml diff --git a/lib/lib.ml b/experiments/simplest_model_init.ml similarity index 100% rename from lib/lib.ml rename to experiments/simplest_model_init.ml diff --git a/lib/dune b/lib/dune deleted file mode 100644 index 3178596..0000000 --- a/lib/dune +++ /dev/null @@ -1,109 +0,0 @@ -; (env -; (_ -; (flags -; (:standard -warn-error +5)))) - -(library - (name semantic_interpreter) - (modules semantic_interpreter) - (flags (-rectypes)) - (libraries OCanren OCanren.tester) - (inline_tests) - (wrapped false) - (preprocess - (pps GT.ppx GT.ppx_all ppx_expect ppx_inline_test))) - -(library - (name relational_interpreter_oc_tests) - (modules relational_interpreter_oc_tests) - (flags (-rectypes)) - (libraries - relational_semantic_interpreter_oc - relational_interpreter_oc_tests_f) - (inline_tests) - (wrapped false) - (preprocess - (pps ppx_expect ppx_inline_test))) - -(library - (name relational_interpreter_oc_tests_f) - (modules relational_interpreter_oc_tests_f) - (flags (-rectypes)) - (libraries OCanren OCanren.tester relational_semantic_interpreter_oc) - (preprocessor_deps ./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 - lib/pp5+gt+plugins+ocanren+dump.exe))) - -(library - (name relational_semantic_interpreter_oc) - (modules relational_semantic_interpreter_oc) - (flags - ; (-dsource) - (:standard -rectypes)) - (libraries OCanren OCanren.tester) - (preprocessor_deps ./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 - lib/pp5+gt+plugins+ocanren+dump.exe))) - -(library - (name parser) - (modules parser) - (flags - ; (-dsource) - (:standard -rectypes)) - (libraries ostap GT) - (preprocessor_deps ./pp5+gt+plugins+ostap+dump.exe) - (wrapped false) - (preprocess - (pps - ppx_expect - ppx_inline_test - GT.ppx - GT.ppx_all - -- - -pp - lib/pp5+gt+plugins+ostap+dump.exe))) - -(rule - (targets pp5+gt+plugins+ocanren+dump.exe) - (action - (run - mkcamlp5.opt - -package - camlp5,camlp5.pa_o,camlp5.macro,camlp5.pr_dump,logger.syntax - -package - logger.syntax,GT.syntax,GT.syntax.all,OCanren.syntax - -o - %{targets}))) - -(rule - (targets pp5+gt+plugins+ostap+dump.exe) - (action - (run - mkcamlp5.opt - -package - camlp5,camlp5.pa_o,camlp5.macro,camlp5.pr_dump,logger.syntax - -package - logger.syntax,GT.syntax,GT.syntax.all,ostap.syntax - -o - %{targets}))) diff --git a/lib/test.ml b/lib/test.ml deleted file mode 100644 index 97a75c4..0000000 --- a/lib/test.ml +++ /dev/null @@ -1,29 +0,0 @@ -open GT -open OCanren - -module Tag = struct - [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] - ocanren type tag = Ref | Value - - module Test = struct - @type answer = logic GT.list with show - - let _ = - Printf.printf "%s" @@ show(answer) (Stream.take (run q (fun q -> ocanren {q === Ref}) - (fun q -> q#reify reify))) - end -end - -module Stmt = struct - ocanren type ('d, 'dl) stmt = Call of 'd * 'dl | Read of 'd | Write of 'd - - module Test = struct - @type answer1 = Nat.ground List.ground GT.list with show - @type answer = (Nat.ground, Nat.ground List.ground) ground GT.list with show - let _ = Printf.printf "%s\n" @@ show(answer1) (Stream.take (run q (fun q -> ocanren {Call (1, [2]) === Call (1, q)}) - (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) - - let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> ocanren {Call (1, [2]) === q}) - (fun q -> q#reify (prj_exn Nat.prj_exn (List.prj_exn Nat.prj_exn))))) - end -end diff --git a/lib/semantic_interpreter.ml b/simplest_model/analyzer.ml similarity index 100% rename from lib/semantic_interpreter.ml rename to simplest_model/analyzer.ml diff --git a/simplest_model/dune b/simplest_model/dune new file mode 100644 index 0000000..a086c48 --- /dev/null +++ b/simplest_model/dune @@ -0,0 +1,83 @@ +; (env +; (_ +; (flags +; (:standard -warn-error +5)))) + +(library + (name analyzer) + (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) + (modules tests) + (flags (-rectypes)) + (libraries synthesizer tests_f) + (inline_tests) + (wrapped false) + (preprocess + (pps ppx_expect ppx_inline_test))) + +(library + (name tests_f) + (modules tests_f) + (flags (-rectypes)) + (libraries OCanren OCanren.tester synthesizer) + (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) + (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))) + +(library + (name parser) + (modules parser) + (flags + ; (-dsource) + (:standard -rectypes)) + (libraries ostap GT) + (preprocessor_deps ../camlp5/pp5+gt+plugins+ostap+dump.exe) + (wrapped false) + (preprocess + (pps + ppx_expect + ppx_inline_test + GT.ppx + GT.ppx_all + -- + -pp + camlp5/pp5+gt+plugins+ostap+dump.exe))) diff --git a/lib/parser.ml b/simplest_model/parser.ml similarity index 100% rename from lib/parser.ml rename to simplest_model/parser.ml diff --git a/lib/relational_semantic_interpreter_oc.ml b/simplest_model/synthesizer.ml similarity index 100% rename from lib/relational_semantic_interpreter_oc.ml rename to simplest_model/synthesizer.ml diff --git a/lib/relational_interpreter_oc_tests.ml b/simplest_model/tests.ml similarity index 98% rename from lib/relational_interpreter_oc_tests.ml rename to simplest_model/tests.ml index c888c92..5da7fe0 100644 --- a/lib/relational_interpreter_oc_tests.ml +++ b/simplest_model/tests.ml @@ -1,5 +1,5 @@ -open Relational_interpreter_oc_tests_f -open Relational_semantic_interpreter_oc +open Tests_f +open Synthesizer open Relational let%expect_test "inv id: test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}] diff --git a/lib/relational_interpreter_oc_tests_f.ml b/simplest_model/tests_f.ml similarity index 99% rename from lib/relational_interpreter_oc_tests_f.ml rename to simplest_model/tests_f.ml index f33e1e5..3c1a8a0 100644 --- a/lib/relational_interpreter_oc_tests_f.ml +++ b/simplest_model/tests_f.ml @@ -1,4 +1,4 @@ -open Relational_semantic_interpreter_oc +open Synthesizer open Relational open GT open OCanren From 00d13ddbbed2b5ba7007804ced437c52764c9e44 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 22 Feb 2026 15:53:15 +0000 Subject: [PATCH 3/3] initial formal model semantics document, etc. --- simplest_model/.gitignore | 1 + simplest_model/model.typ | 203 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 204 insertions(+) create mode 100644 simplest_model/.gitignore create mode 100644 simplest_model/model.typ diff --git a/simplest_model/.gitignore b/simplest_model/.gitignore new file mode 100644 index 0000000..a136337 --- /dev/null +++ b/simplest_model/.gitignore @@ -0,0 +1 @@ +*.pdf diff --git a/simplest_model/model.typ b/simplest_model/model.typ new file mode 100644 index 0000000..556842a --- /dev/null +++ b/simplest_model/model.typ @@ -0,0 +1,203 @@ +// #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 + += Формальная модель используемого языка + +== Синтаксис + +#h(10pt) + +#bnf( + Prod( + `tag`, + { + Or[`Ref`][pass by reference] + Or[`Value`][copy] + } + ), + Prod( + `value`, + { + Or[`Unit`][cell with some value] + Or[`Bot`][spoiled cell] + } + ), + Prod( + `arg`, + { + Or[`RValue`][new value, no associated variable] + Or[`LValue` $d$][value from some variable] + } + ), + Prod( + `stmt`, + { + Or[$f($`args`$)$][call function by id] + Or[`write` $d$][write to variable] + Or[`read` $d$][read from variable] + } + ), + Prod( + `body`, + { + Or[`body` `stmt`][with statement] + Or[$epsilon$][empty body] + } + ), + Prod( + `fun_decl`, + { + Or[`body`][function body] + Or[`tag` `fun_decl`][with argument pass strategy annotation] + } + ), + Prod( + `prog`, + { + Or[`fun_decl`][main function] + Or[`fun_decl` `prog`][with supplimentary funcitons] + } + ), +) +#align(center, [$d, f in NN,$ `args` $in NN ast.basic$]) + +== Семантика статического интерпретатора + +#h(10pt) + +$V := {0, bot}$ - значения памяти + +$L := NN$ - позиции в памяти + +$X$ - можество переменных + +$sigma : X -> L$ - позиции памяти, соответстующие переменным контекста + +$mu : NN -> V$ - память + +$l in NN$ - длина используемого фрагмента памяти + +$M subset NN$ - множество испорченных ячеек памяти + +#[ + +#let cl = $chevron.l$ +#let cr = $chevron.r$ + +#align(center, grid( + columns: 2, + gutter: 5%, + align(bottom, prooftree( + vertical-spacing: 4pt, + rule( + name: [ spoil init], + $mu =>^nothing mu$, + ) + )), + prooftree( + vertical-spacing: 4pt, + rule( + name: [ spoil step], + + $mu =>^M gamma$, + $mu =>^(M union {n}) gamma[n <- bot]$ + ) + ), +)) + +#h(10pt) + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ $f(x), space f := lambda a. e$], + + $cl [a -> sigma(x)], mu, l, nothing cr + xarrow(e) + cl sigma, mu', l', M' cr$, + + $mu' =>^M' gamma$, + + $cl sigma, mu, l, M cr + xarrow(f(*x)) + cl sigma, gamma|_[0, l), l, M cr$, + ) +)) + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ READ $x$], + + $mu(sigma(x)) != bot$, + + $cl sigma, mu, l, M cr + xarrow("READ" x) + cl sigma, mu, l, M cr$, + ) +)) + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ WRITE $x$], + + $cl sigma, mu, l, M cr + xarrow("WRITE" x) + cl sigma, mu[x <- 0], l, M union {sigma(x)} cr$, + ) +)) + +] + +== Пример аннтаций аргументов + +#h(10pt) + +#align(center, grid( +columns: 3, +gutter: 5%, + ``` + def f(?fx x, ?fy y) { + read(x); + write(x); + read(y); + } + def w(?wx x) { + write(x); + } + ```, + ``` + def g(?gx x, ?gy y) { + write(x); + write(y); + read(x); + read(y); + } + def r(?rx x) { + read(x); + } + ```, + ``` + def main(x, y, z, k) { + w(x); + r(x); // -> ?wx != ref + f(x, y); + r(y); + g(z, k); + w(z); + f(y, z); + r(k); // -> ?gy != ref + } + ``` +)) +``` +-> ?fx = ref, ?fy = ref, ?wx = copy, ?gx = ref, ?gy = copy, ?rx = ref +... +-> ?fx = copy, ?fy = copy, ?wx = copy, ?gx = copy, ?gy = copy, ?rx = copy +``` +