From e924e9a3e912a0a466ff0bc3c178fbd5a1e34714 Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Wed, 8 Dec 2021 19:37:00 +0100
Subject: [PATCH] Filter to add proof scripts
---
.github/workflows/proof_tools.yml | 8 +++++
proofs/autosolve/.gitignore | 2 ++
proofs/autosolve/.ocamlformat | 0
proofs/autosolve/Makefile | 5 ++++
proofs/autosolve/autosolve.ml | 47 ++++++++++++++++++++++++++++++
proofs/autosolve/dune | 3 ++
proofs/autosolve/dune-project | 2 ++
proofs/autosolve/tests/autosolve.t | 15 ++++++++++
proofs/autosolve/tests/dune | 2 ++
9 files changed, 84 insertions(+)
create mode 100644 proofs/autosolve/.gitignore
create mode 100644 proofs/autosolve/.ocamlformat
create mode 100644 proofs/autosolve/Makefile
create mode 100644 proofs/autosolve/autosolve.ml
create mode 100644 proofs/autosolve/dune
create mode 100644 proofs/autosolve/dune-project
create mode 100644 proofs/autosolve/tests/autosolve.t
create mode 100644 proofs/autosolve/tests/dune
diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml
index 9621e08..bc19182 100644
--- a/.github/workflows/proof_tools.yml
+++ b/.github/workflows/proof_tools.yml
@@ -54,6 +54,13 @@ jobs:
opam exec -- dune build
opam exec -- dune runtest
+ - name: autosolve
+ run: |
+ cd "${GITHUB_WORKSPACE}"/personoj/proofs/autosolve || exit 1
+ opam install cmdliner --yes
+ opam exec -- dune build
+ opam exec -- dune runtest
+
pipeline:
strategy:
fail-fast: false
@@ -87,6 +94,7 @@ jobs:
(cd qfo && bmake && sudo bmake install)
(cd split && bmake && sudo bmake install)
(cd pipeline && bmake && sudo bmake install)
+ (cd autosolve && bmake && sudo bmake install)
- name: launch pipeline
run: |
diff --git a/proofs/autosolve/.gitignore b/proofs/autosolve/.gitignore
new file mode 100644
index 0000000..6783440
--- /dev/null
+++ b/proofs/autosolve/.gitignore
@@ -0,0 +1,2 @@
+psnj-autosolve
+_build
diff --git a/proofs/autosolve/.ocamlformat b/proofs/autosolve/.ocamlformat
new file mode 100644
index 0000000..e69de29
diff --git a/proofs/autosolve/Makefile b/proofs/autosolve/Makefile
new file mode 100644
index 0000000..429c35b
--- /dev/null
+++ b/proofs/autosolve/Makefile
@@ -0,0 +1,5 @@
+ROOT = autosolve
+CMDLINER = true
+
+.include "../dune-exe.mk"
+.include "../tools.mk"
diff --git a/proofs/autosolve/autosolve.ml b/proofs/autosolve/autosolve.ml
new file mode 100644
index 0000000..c63f569
--- /dev/null
+++ b/proofs/autosolve/autosolve.ml
@@ -0,0 +1,47 @@
+open Cmdliner
+open Common
+open Parsing
+module S = Syntax
+
+let appaxiom fixed =
+ if fixed then Format.set_geometry ~max_indent:16 ~margin:80;
+ let ast = Parser.parse stdin in
+ let process Pos.{ elt = cmd; pos } =
+ match cmd with
+ | S.P_symbol s ->
+ let script =
+ Some ([ Pos.none @@ S.P_tac_why3 None ], Pos.none @@ S.P_proof_end)
+ in
+ let cmd = S.P_symbol { s with p_sym_prf = script; p_sym_def = true } in
+ Format.printf "%a@\n" Pretty.command (Pos.make pos cmd)
+ | _ ->
+ Format.eprintf "Ill-formed input: only axioms allowed@.";
+ exit 1
+ in
+ Stream.iter process ast
+
+let fixed =
+ let doc =
+ "Fix the geometry of the output to have terminal intependant output"
+ in
+ Arg.(value & flag & info [ "fixed" ] ~doc)
+
+let cmd =
+ let doc = "Transform axioms into automatically proved theorems" in
+ let exits = Term.default_exits in
+ let man =
+ [
+ `S Manpage.s_description;
+ `P
+ "$(tname) is a filter that adds a proof script to each axioms passed \
+ on the standard input.";
+ `S Manpage.s_examples;
+ `P "Faced with input";
+ `Pre "symbol foo: TYPE;";
+ `P "$(tname) returns";
+ `Pre "symbol foo: TYPE :=\nbegin\n why3;\nend;";
+ ]
+ in
+ (Term.(const appaxiom $ fixed), Term.info "psnj-autosolve" ~doc ~exits ~man)
+
+let () = Term.(exit @@ eval cmd)
diff --git a/proofs/autosolve/dune b/proofs/autosolve/dune
new file mode 100644
index 0000000..4261f0d
--- /dev/null
+++ b/proofs/autosolve/dune
@@ -0,0 +1,3 @@
+(executable
+ (name autosolve)
+ (libraries cmdliner lambdapi.parsing lambdapi.common))
diff --git a/proofs/autosolve/dune-project b/proofs/autosolve/dune-project
new file mode 100644
index 0000000..ae73029
--- /dev/null
+++ b/proofs/autosolve/dune-project
@@ -0,0 +1,2 @@
+(lang dune 2.9)
+(cram enable)
diff --git a/proofs/autosolve/tests/autosolve.t b/proofs/autosolve/tests/autosolve.t
new file mode 100644
index 0000000..022ed71
--- /dev/null
+++ b/proofs/autosolve/tests/autosolve.t
@@ -0,0 +1,15 @@
+ $ echo 'symbol true: foo bar baz;' | ../autosolve.exe --fixed
+ symbol true : foo bar baz ≔
+ begin
+ why3;
+ end;
+
+ $ echo 'symbol foo: TYPE; symbol bar: TYPE;' | ../autosolve.exe --fixed
+ symbol foo : TYPE ≔
+ begin
+ why3;
+ end;
+ symbol bar : TYPE ≔
+ begin
+ why3;
+ end;
diff --git a/proofs/autosolve/tests/dune b/proofs/autosolve/tests/dune
new file mode 100644
index 0000000..a60e7c5
--- /dev/null
+++ b/proofs/autosolve/tests/dune
@@ -0,0 +1,2 @@
+(cram
+ (deps ../autosolve.exe))
--
GitLab