initial formal model semantics document, etc.

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})))

lib/dune

@@ -1,78 +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)))
-
-(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})))

lib/test.ml

@@ -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

simplest_model/.gitignore

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

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)))

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
+```
+

simplest_model/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 $(<string-expression>) 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   : <x::xs> :!(Util.listBy)[ostap ("+")][mulli]   {List.fold_left (fun x y -> Add (x, y)) x xs}; (* note the use of a pattern for bindings; *)
+    mulli  : <x::xs> :!(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: <s::ss> : !(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

simplest_model/tests.ml

@@ -1,5 +1,5 @@
-open Relational_interpreter_oc_tests_f
+open Tests_f
-open Relational_semantic_interpreter_oc
+open Synthesizer
 open Relational
 
 let%expect_test "inv id: test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}]

simplest_model/tests_f.ml

@@ -1,4 +1,4 @@
-open Relational_semantic_interpreter_oc
+open Synthesizer
 open Relational
 open GT
 open OCanren