From 8fdc350b1160424fc73944f808ef0c914e382f7b Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Wed, 1 Dec 2021 13:07:08 +0100
Subject: [PATCH] formatting
---
.github/workflows/proof_tools.yml | 8 +++
proofs/appaxiom/tests/dune | 3 +-
proofs/chainprops/dune | 3 +-
proofs/chainprops/test/dune | 7 +-
proofs/dopth/tests/dune | 4 +-
proofs/qfo/.ocamlformat | 5 ++
proofs/qfo/bin/qfo.ml | 105 +++++++++++++++---------------
7 files changed, 70 insertions(+), 65 deletions(-)
create mode 100644 proofs/qfo/.ocamlformat
diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml
index 2ac6f49..3e39502 100644
--- a/.github/workflows/proof_tools.yml
+++ b/.github/workflows/proof_tools.yml
@@ -31,6 +31,8 @@ jobs:
cd "${GITHUB_WORKSPACE}"/personoj/proofs/dopth || exit 1
opam install dune --yes
opam exec -- dune build
+ opam install ocamlformat
+ opam exec -- dune build @fmt
opam exec -- dune runtest
- name: chainprops
@@ -38,6 +40,8 @@ jobs:
cd "${GITHUB_WORKSPACE}"/personoj/proofs/chainprops || exit 1
opam install . --deps-only --yes
opam exec -- dune build
+ opam install ocamlformat
+ opam exec -- dune build @fmt
opam exec -- dune runtest
- name: appaxiom
@@ -45,6 +49,8 @@ jobs:
cd "${GITHUB_WORKSPACE}"/personoj/proofs/appaxiom || exit 1
opam install . --deps-only --yes
opam exec -- dune build
+ opam install ocamlformat
+ opam exec -- dune build @fmt
opam exec -- dune runtest
- name: qfo
@@ -52,4 +58,6 @@ jobs:
cd "${GITHUB_WORKSPACE}"/personoj/proofs/qfo || exit 1
opam install . --deps-only --yes
opam exec -- dune build
+ opam install ocamlformat
+ opam exec -- dune build @fmt
opam exec -- dune runtest
diff --git a/proofs/appaxiom/tests/dune b/proofs/appaxiom/tests/dune
index 3dc07d1..3ffdfab 100644
--- a/proofs/appaxiom/tests/dune
+++ b/proofs/appaxiom/tests/dune
@@ -1,3 +1,2 @@
(cram
- (deps
- ../appaxiom.exe))
+ (deps ../appaxiom.exe))
diff --git a/proofs/chainprops/dune b/proofs/chainprops/dune
index beb7fb1..fc6bf90 100644
--- a/proofs/chainprops/dune
+++ b/proofs/chainprops/dune
@@ -1,4 +1,3 @@
(executable
(name chainprops)
- (libraries angstrom cmdliner
- lambdapi.common lambdapi.parsing))
+ (libraries angstrom cmdliner lambdapi.common lambdapi.parsing))
diff --git a/proofs/chainprops/test/dune b/proofs/chainprops/test/dune
index 4b0acc7..dfa5154 100644
--- a/proofs/chainprops/test/dune
+++ b/proofs/chainprops/test/dune
@@ -1,7 +1,2 @@
(cram
- (deps
- ../chainprops.exe
- example.lp
- example.dep
- foo.lp
- foo.dep))
+ (deps ../chainprops.exe example.lp example.dep foo.lp foo.dep))
diff --git a/proofs/dopth/tests/dune b/proofs/dopth/tests/dune
index 792f222..4188c17 100644
--- a/proofs/dopth/tests/dune
+++ b/proofs/dopth/tests/dune
@@ -1,4 +1,2 @@
(cram
- (deps
- ../dopth.exe
- example.plain))
+ (deps ../dopth.exe example.plain))
diff --git a/proofs/qfo/.ocamlformat b/proofs/qfo/.ocamlformat
new file mode 100644
index 0000000..42e44b1
--- /dev/null
+++ b/proofs/qfo/.ocamlformat
@@ -0,0 +1,5 @@
+break-separators=before
+break-sequences=false
+break-struct=natural
+module-item-spacing=compact
+
diff --git a/proofs/qfo/bin/qfo.ml b/proofs/qfo/bin/qfo.ml
index 625cb4b..7c2a941 100644
--- a/proofs/qfo/bin/qfo.ml
+++ b/proofs/qfo/bin/qfo.ml
@@ -53,59 +53,60 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
Console.State.push ();
(* Try to find lambdapi pkgs from current working directory, and do
nothing if it fails *)
- try
+ try
Package.apply_config (Sys.getcwd ());
- Format.eprintf "Loaded package file from \"%s\"@." (Sys.getcwd ());
- with Error.Fatal _ -> ();
- let mp = [ "<stdin>" ] in
- let sign = Sig_state.create_sign mp in
- let ss = Sig_state.of_sign sign in
- let pcert_ss =
- let ast =
- Parser.parse_string "lpvs"
- "require open lpvs.encoding.lhol lpvs.encoding.pcert \
- lpvs.encoding.depconnectives;"
+ Format.eprintf "Loaded package file from \"%s\"@." (Sys.getcwd ())
+ with Error.Fatal _ ->
+ ();
+ let mp = [ "<stdin>" ] in
+ let sign = Sig_state.create_sign mp in
+ let ss = Sig_state.of_sign sign in
+ let pcert_ss =
+ let ast =
+ Parser.parse_string "lpvs"
+ "require open lpvs.encoding.lhol lpvs.encoding.pcert \
+ lpvs.encoding.depconnectives;"
+ in
+ compile_ast ss ast
in
- compile_ast ss ast
- in
- let module Pcert = (val PvsLp.Encodings.mkpcert pcertmap pcert_ss) in
- Console.out 1 "Loaded PVS-Cert encoding";
- let module DepConn =
- (val let dep_conn_ss =
- let ast =
- (* WARNING: [open] is used because the [require open] of the
- previous command has some side effects which records that it
- has been required. *)
- Parser.parse_string "lpvs"
- "open lpvs.encoding.lhol; open lpvs.encoding.depconnectives;"
+ let module Pcert = (val PvsLp.Encodings.mkpcert pcertmap pcert_ss) in
+ Console.out 1 "Loaded PVS-Cert encoding";
+ let module DepConn =
+ (val let dep_conn_ss =
+ let ast =
+ (* WARNING: [open] is used because the [require open] of the
+ previous command has some side effects which records that it
+ has been required. *)
+ Parser.parse_string "lpvs"
+ "open lpvs.encoding.lhol; open lpvs.encoding.depconnectives;"
+ in
+ compile_ast ss ast
in
- compile_ast ss ast
- in
- PvsLp.Encodings.mkconnectors depconnectives dep_conn_ss)
- in
- let prop_calc_ss =
- let ast =
- Parser.parse_string "lpvs"
- "open lpvs.encoding.lhol;require open lpvs.encoding.connectives;"
+ PvsLp.Encodings.mkconnectors depconnectives dep_conn_ss)
in
- compile_ast ss ast
- in
- let module Propc =
- (val PvsLp.Encodings.mkconnectors connectives prop_calc_ss)
- in
- Console.out 1 "Loaded classical propositional calculus";
- let module Tran = PvsLp.LpCert.PropOfPcert (Pcert) (DepConn) (Propc) in
- let ast = Parser.parse stdin in
- let _ss = compile_ast pcert_ss ast in
- let syms = get_symbols sign in
- let tr_pp name (ty, _) =
- try
- let propty = Tran.f ty in
- Format.printf "@[symbol %s:@ %a;@]@." name Print.pp_term propty
- with Tran.CannotTranslate t ->
- Format.eprintf "Cannot translate %a@." Print.pp_term t
- in
- StrMap.iter tr_pp syms
+ let prop_calc_ss =
+ let ast =
+ Parser.parse_string "lpvs"
+ "open lpvs.encoding.lhol;require open lpvs.encoding.connectives;"
+ in
+ compile_ast ss ast
+ in
+ let module Propc =
+ (val PvsLp.Encodings.mkconnectors connectives prop_calc_ss)
+ in
+ Console.out 1 "Loaded classical propositional calculus";
+ let module Tran = PvsLp.LpCert.PropOfPcert (Pcert) (DepConn) (Propc) in
+ let ast = Parser.parse stdin in
+ let _ss = compile_ast pcert_ss ast in
+ let syms = get_symbols sign in
+ let tr_pp name (ty, _) =
+ try
+ let propty = Tran.f ty in
+ Format.printf "@[symbol %s:@ %a;@]@." name Print.pp_term propty
+ with Tran.CannotTranslate t ->
+ Format.eprintf "Cannot translate %a@." Print.pp_term t
+ in
+ StrMap.iter tr_pp syms
open Cmdliner
@@ -137,9 +138,9 @@ let cmd =
[
`S Manpage.s_description
; `P
- "$(tname) is a filter that transforms a list of Dedukti axioms \
- encoded in PVS-Cert with dependent logical connectives into a list of axioms expressed in \
- something close to first order logic."
+ "$(tname) is a filter that transforms a list of Dedukti axioms encoded \
+ in PVS-Cert with dependent logical connectives into a list of axioms \
+ expressed in something close to first order logic."
; `P
"To convert files, the program needs identify the symbols of the \
encoding. The mapping allows to indicate the name of such symbols. \
--
GitLab