diff --git a/camlp5/dune b/camlp5/dune deleted file mode 100644 index f0a99a9..0000000 --- a/camlp5/dune +++ /dev/null @@ -1,23 +0,0 @@ -(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/dune b/lib/dune new file mode 100644 index 0000000..aa69dad --- /dev/null +++ b/lib/dune @@ -0,0 +1,78 @@ +; (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))) + +(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}))) diff --git a/experiments/simplest_model_init.ml b/lib/lib.ml similarity index 100% rename from experiments/simplest_model_init.ml rename to lib/lib.ml diff --git a/experiments/old_model_init.ml b/lib/lib_next.ml similarity index 100% rename from experiments/old_model_init.ml rename to lib/lib_next.ml diff --git a/simplest_model/tests.ml b/lib/relational_interpreter_oc_tests.ml similarity index 98% rename from simplest_model/tests.ml rename to lib/relational_interpreter_oc_tests.ml index 5da7fe0..c888c92 100644 --- a/simplest_model/tests.ml +++ b/lib/relational_interpreter_oc_tests.ml @@ -1,5 +1,5 @@ -open Tests_f -open Synthesizer +open Relational_interpreter_oc_tests_f +open Relational_semantic_interpreter_oc open Relational let%expect_test "inv id: test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}] diff --git a/simplest_model/tests_f.ml b/lib/relational_interpreter_oc_tests_f.ml similarity index 99% rename from simplest_model/tests_f.ml rename to lib/relational_interpreter_oc_tests_f.ml index 3c1a8a0..f33e1e5 100644 --- a/simplest_model/tests_f.ml +++ b/lib/relational_interpreter_oc_tests_f.ml @@ -1,4 +1,4 @@ -open Synthesizer +open Relational_semantic_interpreter_oc open Relational open GT open OCanren diff --git a/simplest_model/synthesizer.ml b/lib/relational_semantic_interpreter_oc.ml similarity index 100% rename from simplest_model/synthesizer.ml rename to lib/relational_semantic_interpreter_oc.ml diff --git a/simplest_model/analyzer.ml b/lib/semantic_interpreter.ml similarity index 100% rename from simplest_model/analyzer.ml rename to lib/semantic_interpreter.ml diff --git a/lib/test.ml b/lib/test.ml new file mode 100644 index 0000000..97a75c4 --- /dev/null +++ b/lib/test.ml @@ -0,0 +1,29 @@ +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/simplest_model/.gitignore b/simplest_model/.gitignore deleted file mode 100644 index a136337..0000000 --- a/simplest_model/.gitignore +++ /dev/null @@ -1 +0,0 @@ -*.pdf diff --git a/simplest_model/dune b/simplest_model/dune deleted file mode 100644 index a086c48..0000000 --- a/simplest_model/dune +++ /dev/null @@ -1,83 +0,0 @@ -; (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/simplest_model/model.typ b/simplest_model/model.typ deleted file mode 100644 index 556842a..0000000 --- a/simplest_model/model.typ +++ /dev/null @@ -1,203 +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 - -= Формальная модель используемого языка - -== Синтаксис - -#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 -``` - diff --git a/simplest_model/parser.ml b/simplest_model/parser.ml deleted file mode 100644 index dd69b16..0000000 --- a/simplest_model/parser.ml +++ /dev/null @@ -1,262 +0,0 @@ -(* -* 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