From 19b9d3aa566b8d9903e190f7fbf52db63382fefc Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 30 Nov 2025 00:42:04 +0300 Subject: [PATCH] start with template code https://github.com/Kakadu/OCanren-basic-template --- .gitignore | 2 + bin/dune | 13 +++++ bin/main.ml | 77 ++++++++++++++++++++++++++++ dune-project | 33 ++++++++++++ lib/dune | 20 ++++++++ lib/lib.ml | 17 ++++++ pass_strategy_synthesis.opam | 35 +++++++++++++ test/dune | 2 + test/test_pass_strategy_synthesis.ml | 0 9 files changed, 199 insertions(+) create mode 100644 .gitignore create mode 100644 bin/dune create mode 100644 bin/main.ml create mode 100644 dune-project create mode 100644 lib/dune create mode 100644 lib/lib.ml create mode 100644 pass_strategy_synthesis.opam create mode 100644 test/dune create mode 100644 test/test_pass_strategy_synthesis.ml diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..37383b1 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +_build +dune.lock diff --git a/bin/dune b/bin/dune new file mode 100644 index 0000000..b712391 --- /dev/null +++ b/bin/dune @@ -0,0 +1,13 @@ +(env + (_ + (flags + (:standard -warn-error +5)))) + +(executable + (public_name main) + (modules main) + (flags + (:standard -rectypes)) + (libraries lib1) + (preprocess + (pps OCanren-ppx.ppx_repr OCanren-ppx.ppx_fresh GT.ppx GT.ppx_all))) diff --git a/bin/main.ml b/bin/main.ml new file mode 100644 index 0000000..ab20072 --- /dev/null +++ b/bin/main.ml @@ -0,0 +1,77 @@ +(* let () = print_endline "Hello, World!" *) +open OCanren +open Lib +open Lam + +let rec substo l x a l' = + let open Lam in + conde + [ fresh y (l === v y) (y === x) (l' === a) + ; fresh + (m n m' n') + (l === app m n) + (l' === app m' n') + (substo m x a m') + (substo n x a n') + ; fresh + (v b) + (l === abs v b) + (conde [ x === v &&& (l' === l); fresh b' (l' === abs v b') (substo b x a b') ]) + ] +;; + +let rec evalo m n = + conde + [ fresh x (m === v x) (n === m) + ; fresh (x l) (m === abs x l) (n === m) + ; fresh + (f a f' a') + (m === app f a) + (evalo f f') + (evalo a a') + (conde + [ fresh (x l l') (f' === abs x l) (substo l x a' l') (evalo l' n) + ; fresh (p q) (f' === app p q) (n === app f' a') + ; fresh x (f' === v x) (n === app f' a') + ]) + ] +;; + +let a_la_quine q r s = ?&[ evalo (app q r) s; evalo (app r s) q; evalo (app s q) r ] + +open Tester + +let runL n = run_r Lam.reify (GT.show Lam.logic) n +let run_exn eta = run_r Lam.prj_exn eta + +let _ = + run_exn (GT.show Lam.ground) 1 q qh (REPR (fun q -> substo (v varX) varX (v varY) q)); + run_exn (GT.show Lam.ground) 1 q qh (REPR (fun q -> evalo (abs varX (v varX)) q)); + run_exn (GT.show Lam.ground) 2 q qh (REPR (fun q -> evalo (abs varX (v varX)) q)); + run_exn + (GT.show Lam.ground) + 1 + q + qh + (REPR (fun q -> evalo (app (abs varX (v varX)) (v varY)) q)); + run_exn + (GT.show Lam.ground) + 1 + q + qh + (REPR (fun q -> evalo (app (abs varX (v varX)) q) (v varY))); + run_exn + (GT.show Lam.ground) + 1 + q + qh + (REPR (fun q -> evalo (app (abs varX q) (v varY)) (v varY))); + run_exn (GT.show Lam.ground) 1 q qh (REPR (fun q -> evalo (app (v varX) (v varX)) q)); + run_exn (GT.show Lam.ground) 1 q qh (REPR (fun q -> evalo (v varX) q)) +;; + +let _withFree = + runL 1 q qh (REPR (fun q -> evalo (app q (v varX)) (v varX))); + runL 1 qr qrh (REPR (fun q r -> evalo (app r q) (v varX))); + runL 2 qrs qrsh (REPR (fun q r s -> a_la_quine q r s)) +;; diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..21d5a54 --- /dev/null +++ b/dune-project @@ -0,0 +1,33 @@ +(lang dune 3.20) + +(name pass_strategy_synthesis) + +(generate_opam_files true) + +(source + (github username/reponame)) + +(authors "Author Name ") + +(maintainers "Maintainer Name ") + +(license LICENSE) + +(documentation https://url/to/documentation) + +(package + (name pass_strategy_synthesis) + (synopsis "A short synopsis") + (description "A longer description") + (depends + (ocaml + (= 4.14.2)) + GT + (OCanren + (>= 0.3.0~)) + (OCanren-ppx + (>= 0.3.0~))) + (tags + ("add topics" "to describe" your project))) + +; See the complete stanza docs at https://dune.readthedocs.io/en/stable/reference/dune-project/index.html diff --git a/lib/dune b/lib/dune new file mode 100644 index 0000000..9eb006f --- /dev/null +++ b/lib/dune @@ -0,0 +1,20 @@ +(env + (_ + (flags + (:standard -warn-error +5)))) + +(library + (name lib1) + (modules lib) + (flags (-rectypes)) + (libraries OCanren OCanren.tester) + (inline_tests) + (wrapped false) + (preprocess + (pps + OCanren-ppx.ppx_repr + OCanren-ppx.ppx_fresh + OCanren-ppx.ppx_distrib + GT.ppx + GT.ppx_all + ppx_inline_test))) diff --git a/lib/lib.ml b/lib/lib.ml new file mode 100644 index 0000000..2025d58 --- /dev/null +++ b/lib/lib.ml @@ -0,0 +1,17 @@ +open OCanren + +module Lam = struct + [%%distrib + type nonrec ('varname, 'self) t = + | V of 'varname + | App of 'self * 'self + | Abs of 'varname * 'self + [@@deriving gt ~options:{ show; fmt; gmap }] + + type ground = (GT.string, ground) t] + + let varX = !!"x" + let varY = !!"y" + let varF = !!"f" +end + diff --git a/pass_strategy_synthesis.opam b/pass_strategy_synthesis.opam new file mode 100644 index 0000000..03368cf --- /dev/null +++ b/pass_strategy_synthesis.opam @@ -0,0 +1,35 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "A short synopsis" +description: "A longer description" +maintainer: ["Maintainer Name "] +authors: ["Author Name "] +license: "LICENSE" +tags: ["add topics" "to describe" "your" "project"] +homepage: "https://github.com/username/reponame" +doc: "https://url/to/documentation" +bug-reports: "https://github.com/username/reponame/issues" +depends: [ + "dune" {>= "3.20"} + "ocaml" {= "4.14.2"} + "GT" + "OCanren" {>= "0.3.0~"} + "OCanren-ppx" {>= "0.3.0~"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/username/reponame.git" +x-maintenance-intent: ["(latest)"] diff --git a/test/dune b/test/dune new file mode 100644 index 0000000..abea2c4 --- /dev/null +++ b/test/dune @@ -0,0 +1,2 @@ +(test + (name test_pass_strategy_synthesis)) diff --git a/test/test_pass_strategy_synthesis.ml b/test/test_pass_strategy_synthesis.ml new file mode 100644 index 0000000..e69de29