From 221ad26c1f5b47a37516ef7e705d8999f9e0acbf Mon Sep 17 00:00:00 2001 From: William Ball Date: Thu, 29 Aug 2024 22:55:09 -0700 Subject: [PATCH] initial commit --- .gitignore | 1 + bin/dune | 4 ++++ bin/main.ml | 1 + dune-project | 26 ++++++++++++++++++++++++++ lib/dune | 2 ++ lib/formula.ml | 11 +++++++++++ lib/formula.mli | 11 +++++++++++ lib/proof.ml | 0 lib/proof.mli | 0 lib/term.ml | 5 +++++ lib/term.mli | 5 +++++ proof_checker.opam | 31 +++++++++++++++++++++++++++++++ test/dune | 2 ++ test/test_proof_checker.ml | 0 14 files changed, 99 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/formula.ml create mode 100644 lib/formula.mli create mode 100644 lib/proof.ml create mode 100644 lib/proof.mli create mode 100644 lib/term.ml create mode 100644 lib/term.mli create mode 100644 proof_checker.opam create mode 100644 test/dune create mode 100644 test/test_proof_checker.ml diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..69fa449 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +_build/ diff --git a/bin/dune b/bin/dune new file mode 100644 index 0000000..ecf0f55 --- /dev/null +++ b/bin/dune @@ -0,0 +1,4 @@ +(executable + (public_name proof_checker) + (name main) + (libraries proof_checker)) diff --git a/bin/main.ml b/bin/main.ml new file mode 100644 index 0000000..cb31a83 --- /dev/null +++ b/bin/main.ml @@ -0,0 +1 @@ +let () = print_endline "Hi" diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..7e80710 --- /dev/null +++ b/dune-project @@ -0,0 +1,26 @@ +(lang dune 3.16) + +(name proof_checker) + +(generate_opam_files true) + +(source + (github username/reponame)) + +(authors "Author Name") + +(maintainers "Maintainer Name") + +(license LICENSE) + +(documentation https://url/to/documentation) + +(package + (name proof_checker) + (synopsis "A short synopsis") + (description "A longer description") + (depends ocaml dune) + (tags + (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..f3c2831 --- /dev/null +++ b/lib/dune @@ -0,0 +1,2 @@ +(library + (name proof_checker)) diff --git a/lib/formula.ml b/lib/formula.ml new file mode 100644 index 0000000..2daad88 --- /dev/null +++ b/lib/formula.ml @@ -0,0 +1,11 @@ +type t = + | Relation of string * Term.t list + | Equal of Term.t * Term.t + | Bottom + | Neg of t + | Conj of t * t + | Disj of t * t + | Impl of t * t + | Iff of t * t + | Forall of t + | Exists of t diff --git a/lib/formula.mli b/lib/formula.mli new file mode 100644 index 0000000..2daad88 --- /dev/null +++ b/lib/formula.mli @@ -0,0 +1,11 @@ +type t = + | Relation of string * Term.t list + | Equal of Term.t * Term.t + | Bottom + | Neg of t + | Conj of t * t + | Disj of t * t + | Impl of t * t + | Iff of t * t + | Forall of t + | Exists of t diff --git a/lib/proof.ml b/lib/proof.ml new file mode 100644 index 0000000..e69de29 diff --git a/lib/proof.mli b/lib/proof.mli new file mode 100644 index 0000000..e69de29 diff --git a/lib/term.ml b/lib/term.ml new file mode 100644 index 0000000..252d267 --- /dev/null +++ b/lib/term.ml @@ -0,0 +1,5 @@ +type t = + | Var of int + | Const of string + | Free of string + | Function of string * t list diff --git a/lib/term.mli b/lib/term.mli new file mode 100644 index 0000000..252d267 --- /dev/null +++ b/lib/term.mli @@ -0,0 +1,5 @@ +type t = + | Var of int + | Const of string + | Free of string + | Function of string * t list diff --git a/proof_checker.opam b/proof_checker.opam new file mode 100644 index 0000000..b296c11 --- /dev/null +++ b/proof_checker.opam @@ -0,0 +1,31 @@ +# 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: ["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: [ + "ocaml" + "dune" {>= "3.16"} + "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" diff --git a/test/dune b/test/dune new file mode 100644 index 0000000..a2c81b3 --- /dev/null +++ b/test/dune @@ -0,0 +1,2 @@ +(test + (name test_proof_checker)) diff --git a/test/test_proof_checker.ml b/test/test_proof_checker.ml new file mode 100644 index 0000000..e69de29