commit 221ad26c1f5b47a37516ef7e705d8999f9e0acbf Author: William Ball Date: Thu Aug 29 22:55:09 2024 -0700 initial commit 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