diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml
index bc19182210d7f3062801531cf0fe4ffa6747854c..9b94bccb0cd3d29e6fcfa2b1cf84dc5ef1bdcc41 100644
--- a/.github/workflows/proof_tools.yml
+++ b/.github/workflows/proof_tools.yml
@@ -26,40 +26,12 @@ jobs:
- name: Pin lambdapi
run: opam pin add 'git://github.com/gabrielhdt/lambdapi#refiner'
- - name: dopth
+ - name: toolbox
run: |
- cd "${GITHUB_WORKSPACE}"/personoj/proofs/dopth || exit 1
- opam install dune --yes
- opam exec -- dune build
- opam exec -- dune runtest
-
- - name: chainprops
- run: |
- cd "${GITHUB_WORKSPACE}"/personoj/proofs/chainprops || exit 1
- opam install . --deps-only --yes
- opam exec -- dune build
- opam exec -- dune runtest
-
- - name: appaxiom
- run: |
- cd "${GITHUB_WORKSPACE}"/personoj/proofs/appaxiom || exit 1
+ cd "${GITHUB_WORKSPACE}"/personoj/proofs/psnj_toolbox || exit 1
opam install . --deps-only --yes
opam exec -- dune build
- opam exec -- dune runtest
-
- - name: qfo
- run: |
- cd "${GITHUB_WORKSPACE}"/personoj/proofs/qfo || exit 1
- opam install . --deps-only --yes
- 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
+ opam exe -- dune runtest
pipeline:
strategy:
@@ -88,13 +60,9 @@ jobs:
run: |
opam install yojson angstrom feather cmdliner
cd "${GITHUB_WORKSPACE}"/personoj/proofs || exit 1
- (cd appaxiom && bmake && sudo bmake install)
- (cd chainprops && bmake && sudo bmake install)
- (cd dopth && bmake && sudo bmake install)
- (cd qfo && bmake && sudo bmake install)
(cd split && bmake && sudo bmake install)
(cd pipeline && bmake && sudo bmake install)
- (cd autosolve && bmake && sudo bmake install)
+ (cd psnj_toolbox && make && sudo make install)
- name: launch pipeline
run: |
diff --git a/proofs/appaxiom/.gitignore b/proofs/appaxiom/.gitignore
deleted file mode 100644
index 27d8084067096606ee10d0d194aa793ef4374c72..0000000000000000000000000000000000000000
--- a/proofs/appaxiom/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-psnj-appaxiom
diff --git a/proofs/appaxiom/Makefile b/proofs/appaxiom/Makefile
deleted file mode 100644
index a5a2240b148097faa2ed3785f3688481cc92a8d1..0000000000000000000000000000000000000000
--- a/proofs/appaxiom/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-ROOT = appaxiom
-CMDLINER = true
-
-.include "../dune-exe.mk"
-.include "../tools.mk"
diff --git a/proofs/appaxiom/dune b/proofs/appaxiom/dune
deleted file mode 100644
index c9f00bc7400fb3f4442a71864e2a935b40e45639..0000000000000000000000000000000000000000
--- a/proofs/appaxiom/dune
+++ /dev/null
@@ -1,3 +0,0 @@
-(executable
- (name appaxiom)
- (libraries cmdliner lambdapi.parsing lambdapi.common))
diff --git a/proofs/appaxiom/dune-project b/proofs/appaxiom/dune-project
deleted file mode 100644
index 1c9b5d940764918fa8f3120ce39b2febde671f4f..0000000000000000000000000000000000000000
--- a/proofs/appaxiom/dune-project
+++ /dev/null
@@ -1,10 +0,0 @@
-(lang dune 2.9)
-(cram enable)
-(generate_opam_files true)
-
-(maintainers "dedukti-dev@inria.fr")
-
-(package
- (name appaxiom)
- (synopsis "Apply something on Dedukti axioms")
- (depends cmdliner lambdapi))
diff --git a/proofs/appaxiom/tests/appaxiom.t b/proofs/appaxiom/tests/appaxiom.t
deleted file mode 100644
index d5f441d2ade8140b179566758cef9fa6ae267343..0000000000000000000000000000000000000000
--- a/proofs/appaxiom/tests/appaxiom.t
+++ /dev/null
@@ -1,2 +0,0 @@
- $ echo 'symbol true : imp P P;' | ../appaxiom.exe
- symbol true : @Prf (imp P P);
diff --git a/proofs/appaxiom/tests/dune b/proofs/appaxiom/tests/dune
deleted file mode 100644
index 3ffdfab4131b5a0fdd1fda0a9334813cee73042d..0000000000000000000000000000000000000000
--- a/proofs/appaxiom/tests/dune
+++ /dev/null
@@ -1,2 +0,0 @@
-(cram
- (deps ../appaxiom.exe))
diff --git a/proofs/autosolve/.gitignore b/proofs/autosolve/.gitignore
deleted file mode 100644
index 6783440b6e83301a4009c0854c2492efe3491971..0000000000000000000000000000000000000000
--- a/proofs/autosolve/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-psnj-autosolve
-_build
diff --git a/proofs/autosolve/Makefile b/proofs/autosolve/Makefile
deleted file mode 100644
index 429c35befbc9bc944826ebe17a71f4720e58defc..0000000000000000000000000000000000000000
--- a/proofs/autosolve/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-ROOT = autosolve
-CMDLINER = true
-
-.include "../dune-exe.mk"
-.include "../tools.mk"
diff --git a/proofs/autosolve/dune b/proofs/autosolve/dune
deleted file mode 100644
index 4261f0dd6fe629c4a197535c8d6dd84e65a30660..0000000000000000000000000000000000000000
--- a/proofs/autosolve/dune
+++ /dev/null
@@ -1,3 +0,0 @@
-(executable
- (name autosolve)
- (libraries cmdliner lambdapi.parsing lambdapi.common))
diff --git a/proofs/autosolve/dune-project b/proofs/autosolve/dune-project
deleted file mode 100644
index ae730292676bfc91a5a5e576cfbc1f333eb7df2d..0000000000000000000000000000000000000000
--- a/proofs/autosolve/dune-project
+++ /dev/null
@@ -1,2 +0,0 @@
-(lang dune 2.9)
-(cram enable)
diff --git a/proofs/autosolve/tests/dune b/proofs/autosolve/tests/dune
deleted file mode 100644
index a60e7c548b9842e4dc82503a3975c13417f75553..0000000000000000000000000000000000000000
--- a/proofs/autosolve/tests/dune
+++ /dev/null
@@ -1,2 +0,0 @@
-(cram
- (deps ../autosolve.exe))
diff --git a/proofs/chainprops/.gitignore b/proofs/chainprops/.gitignore
deleted file mode 100644
index b91579a7da3e04c3522afb85b7ffc8bfdf8d25d8..0000000000000000000000000000000000000000
--- a/proofs/chainprops/.gitignore
+++ /dev/null
@@ -1,4 +0,0 @@
-_opam
-_build
-psnj-chainprops
-*.1
diff --git a/proofs/chainprops/.ocamlformat b/proofs/chainprops/.ocamlformat
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/proofs/chainprops/Makefile b/proofs/chainprops/Makefile
deleted file mode 100644
index e9f658ea32cdfaec1a3fdd8db35bc90412024905..0000000000000000000000000000000000000000
--- a/proofs/chainprops/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-ROOT = chainprops
-CMDLINER = true
-
-.include "../dune-exe.mk"
-.include "../tools.mk"
diff --git a/proofs/chainprops/chainprops.ml b/proofs/chainprops/chainprops.ml
deleted file mode 100644
index 94ebc344ff77865fdc3a4a63a25bf06ec1f21ce7..0000000000000000000000000000000000000000
--- a/proofs/chainprops/chainprops.ml
+++ /dev/null
@@ -1,151 +0,0 @@
-(** Parse dependencies file *)
-module Deps : sig
- type t = string * string list
-
- val pp : Format.formatter -> t -> unit
-
- val parse : in_channel -> t list
-end = struct
- open Angstrom
-
- type t = string * string list
-
- let is_space = function ' ' | '\t' -> true | _ -> false
-
- let blank = skip_while is_space
-
- let blank1 = satisfy is_space *> blank
-
- let eol = string "\n\r" <|> string "\n"
-
- let colon = blank *> char ':' <* blank
-
- (* Word characters taken from the parser of lambdapi. *)
- let is_wordchar = function
- | ' ' | '\r' | '\t' | '\n' | '(' | ')' | '{' | '}' | '[' | ']' | ':' | '.'
- | '`' | '"' ->
- false
- | _ -> true
-
- let word = take_while1 is_wordchar
-
- let line = both (word <* colon) (sep_by blank1 word)
-
- let deps = many (line <* many1 eol)
-
- let pp ppf ((s, deps) : t) =
- let open Format in
- let pp_sep = pp_print_space in
- fprintf ppf "@[<h>%s:@ %a@]" s (pp_print_list ~pp_sep pp_print_string) deps
-
- let parse (ic : in_channel) : t list =
- let file = really_input_string ic (in_channel_length ic) in
- match parse_string ~consume:All deps file with
- | Ok v -> v
- | Error msg -> failwith msg
-end
-
-(** Transform a list of propositions into inference steps. *)
-
-open Common
-open Parsing
-module S = Syntax
-
-type decl = string * S.p_term
-(** A proposition declaration with a name and a type. *)
-
-(** [pp ppf decl] pretty prints declaration [decl] to formatter [ppf]. *)
-let pp (ppf : Format.formatter) ((n, ty) : decl) : unit =
- Format.fprintf ppf "@[symbol %s:@ %a;@]" n Pretty.term ty
-
-(** [propositions ast] returns the list of propositions as pairs
- [(name,ty)] where [name] is the name of the proposition and [ty]
- is its type. *)
-let propositions (ast : S.ast) : decl list =
- let props : decl list ref = ref [] in
- let match_decl = function
- | S.P_symbol { p_sym_nam; p_sym_typ = Some ty; _ } -> (p_sym_nam.elt, ty)
- | _ ->
- failwith
- "Invalid Dedukti source file: only symbol declarations are supported"
- in
- Stream.iter (fun c -> props := match_decl c.Pos.elt :: !props) ast;
- List.rev !props
-
-(** [merge imp deps props] transform each proposition of [props] into
- implications (the implication is defined by [imp]) from its
- dependencies specified in [deps] to itself. *)
-let merge (imp : S.p_term) (deps : Deps.t list) (props : decl list) : decl list
- =
- let fn ((name, ty) : decl) : decl =
- let deps = try List.assoc name deps with Not_found -> [] in
- let f dep acc =
- let d_ty = List.assoc dep props in
- Syntax.P.(appl (appl imp d_ty) acc)
- in
- let ty = List.fold_right f deps ty in
- (name, ty)
- in
- List.map fn props
-
-let chainprops deps imply pp_deps =
- let ic = open_in deps in
- let deps = Deps.parse ic in
- close_in ic;
- if pp_deps then (
- Format.(
- eprintf "=== Dependencies ===@\n";
- pp_print_list ~pp_sep:pp_print_newline Deps.pp err_formatter deps;
- eprintf "@\n====================@."));
- let imply = Syntax.P.iden imply in
- let props = propositions (Parser.parse stdin) in
- let inferences = merge imply deps props in
- let open Format in
- pp_print_list ~pp_sep:pp_print_newline pp std_formatter inferences;
- pp_print_newline std_formatter ()
-
-(** CLI *)
-
-open Cmdliner
-
-let deps =
- let doc =
- "Dependencies of propositions inside Dedukti file. A line $(b,tgt: hyp0 \
- hyp1) specifies that proposition $(b,tgt) is deduced from $(b,hyp0) and \
- $(b,hyp1)."
- in
- Arg.(required & pos 0 (some non_dir_file) None & info [] ~doc ~docv:"DEPS")
-
-let imply =
- let doc = "Use symbol $(docv) for implication" in
- Arg.(value & opt string "imp" & info [ "imp" ] ~doc ~docv:"IMP")
-
-let pp_deps =
- let doc = "Print parsed dependencies to stderr (for debugging purposes)" in
- Arg.(value & flag & info [ "pp-deps" ] ~doc)
-
-let cmd =
- let doc = "Build a proof tree from propositions and dependencies" in
- let exits = Term.default_exits in
- let man =
- [
- `S Manpage.s_description;
- `P
- "psnj-chainprops tranform a list of propositions given on its standard \
- input into a list of inferences represented as implications. The \
- hypothesese and conclusions of inferences are specified in a \
- dependency file which follows a Makefile syntax.";
- `S Manpage.s_examples;
- `P "Given a file foo.dep";
- `Pre "tgt: hyp0 hyp1";
- `P "and the input";
- `Pre "symbol tgt: P;\nsymbol hyp0: H0;\nsymbol hyp1: H1;";
- `P "$(b,psnj-chainprops foo.dep) outputs";
- `Pre
- "symbol hyp0: H0;\nsymbol hyp1: H1;\nsymbol tgt: @imp H0 (@imp H1 P);";
- ]
- in
- ( Term.(const chainprops $ deps $ imply $ pp_deps),
- Term.info "psnj-chainprops" ~doc ~exits ~man )
-
-let () = Term.(exit @@ eval cmd)
diff --git a/proofs/chainprops/chainprops.opam b/proofs/chainprops/chainprops.opam
deleted file mode 100644
index d3041df5a01cf186aef8a6e2628e5b987f63762d..0000000000000000000000000000000000000000
--- a/proofs/chainprops/chainprops.opam
+++ /dev/null
@@ -1,27 +0,0 @@
-# This file is generated by dune, edit dune-project instead
-opam-version: "2.0"
-synopsis: "Make inference steps out of Dedukti propositions"
-maintainer: ["dedukti-dev@inria.fr"]
-depends: [
- "dune" {>= "2.9"}
- "cmdliner"
- "angstrom"
- "lambdapi"
- "odoc" {with-doc}
-]
-build: [
- ["dune" "subst"] {dev}
- [
- "dune"
- "build"
- "-p"
- name
- "-j"
- jobs
- "--promote-install-files=false"
- "@install"
- "@runtest" {with-test}
- "@doc" {with-doc}
- ]
- ["dune" "install" "-p" name "--create-install-files" name]
-]
diff --git a/proofs/chainprops/dune b/proofs/chainprops/dune
deleted file mode 100644
index fc6bf90c2a7f0348c4cab9a31e7ef89cf223b2fd..0000000000000000000000000000000000000000
--- a/proofs/chainprops/dune
+++ /dev/null
@@ -1,3 +0,0 @@
-(executable
- (name chainprops)
- (libraries angstrom cmdliner lambdapi.common lambdapi.parsing))
diff --git a/proofs/chainprops/dune-project b/proofs/chainprops/dune-project
deleted file mode 100644
index fb65ab4c61d7c10fa59133a3f3ddf85e0e2ee837..0000000000000000000000000000000000000000
--- a/proofs/chainprops/dune-project
+++ /dev/null
@@ -1,12 +0,0 @@
-(lang dune 2.9)
-(name chainprops)
-(cram enable)
-
-(generate_opam_files true)
-(maintainers "dedukti-dev@inria.fr")
-
-(package
- (name chainprops)
- (synopsis "Make inference steps out of Dedukti propositions")
- (depends
- cmdliner angstrom lambdapi))
diff --git a/proofs/chainprops/test/dune b/proofs/chainprops/test/dune
deleted file mode 100644
index dfa5154a06c2b555b45c9fe51fc6e26be62dc298..0000000000000000000000000000000000000000
--- a/proofs/chainprops/test/dune
+++ /dev/null
@@ -1,2 +0,0 @@
-(cram
- (deps ../chainprops.exe example.lp example.dep foo.lp foo.dep))
diff --git a/proofs/dopth/.gitignore b/proofs/dopth/.gitignore
deleted file mode 100644
index a61f5c2a8ea98fcb76530d46e8283c119635ca43..0000000000000000000000000000000000000000
--- a/proofs/dopth/.gitignore
+++ /dev/null
@@ -1,5 +0,0 @@
-psnj-dopth.1
-psnj-dopth
-_build/
-_opam/
-
diff --git a/proofs/dopth/.ocamlformat b/proofs/dopth/.ocamlformat
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/proofs/dopth/Makefile b/proofs/dopth/Makefile
deleted file mode 100644
index 272bda42c44fa7d7a4bba1f98fc371767c0dd47b..0000000000000000000000000000000000000000
--- a/proofs/dopth/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-ROOT = dopth
-
-.include "../dune-exe.mk"
-.include "../tools.mk"
diff --git a/proofs/dopth/dopth.ml b/proofs/dopth/dopth.ml
deleted file mode 100644
index ee36181c2ff4994b67b52548c0ec136bd391c5e1..0000000000000000000000000000000000000000
--- a/proofs/dopth/dopth.ml
+++ /dev/null
@@ -1,90 +0,0 @@
-module Path = struct
- type t = int list
-
- (** [is_predecessor p q] is true if [q = p.i] ([p] is closer to the root). *)
- let is_predecessor (p : t) (q : t) : bool =
- match q with [] -> false | _ :: q_tl -> q_tl = p
-
- let of_string (s : string) : t =
- if s = "root" then []
- else
- try String.split_on_char '.' s |> List.rev_map int_of_string
- with Failure err ->
- Format.eprintf "Invalid path: %s@." s;
- invalid_arg err
-end
-
-module Id = struct
- type t = string
-
- let make (name : string) = name
-
- let hash : t -> int = Hashtbl.hash
-
- let pp = Format.pp_print_string
-
- let compare = String.compare
-end
-
-let id2path : (Id.t * Path.t) list ref = ref []
-
-module Deps = struct
- module IdMap = Map.Make (struct
- type t = Id.t
-
- let compare = Id.compare
- end)
-
- type t = Id.t list IdMap.t
-
- let empty = IdMap.empty
-
- (** [add id d t] adds dependency [d] to [id] in table [t]. If [id]
- is not bound, it is added to the table. *)
- let add (id : Id.t) (d : Id.t) (t : t) : t =
- let deps =
- match IdMap.find_opt id t with None -> [] | Some deps -> d :: deps
- in
- IdMap.add id (d :: deps) t
-
- let find (id : Id.t) (t : t) : Id.t list = IdMap.find id t
-
- (** [update x x_pth tbl] updates the entries of the table [tbl] adding [id]: if
- [(e,q)] is an element of [id2path], [p] is the successor of [q] then
- [id] is added to the dependencies of [e] element [e] of the table *)
- let update (x : Id.t) (x_pth : Path.t) (tbl : t) : t =
- let f (t : t) ((y, y_pth) : Id.t * Path.t) : t =
- if Path.is_predecessor y_pth x_pth then add y x t else t
- in
- List.fold_left f tbl !id2path
-
- let pp (ppf : Format.formatter) (tbl : t) : unit =
- let open Format in
- let pp_deplist ppf (l : Id.t list) : unit =
- let pp_sep ppf () = pp_print_space ppf () in
- let l = List.sort_uniq Id.compare l in
- pp_print_list ~pp_sep Id.pp ppf l
- in
- let pprint_d (id : Id.t) (d : Id.t list) : unit =
- fprintf ppf "%a: @[<h>%a@]@\n" Id.pp id pp_deplist d
- in
- IdMap.iter pprint_d tbl
-end
-
-let () =
- (try
- while true do
- let id = input_line stdin in
- let pth = input_line stdin in
- id2path := (Id.make id, Path.of_string pth) :: !id2path
- done
- with End_of_file -> ());
- let tbl = Deps.empty in
- try
- let tbl =
- List.fold_left (fun acc (x, pth) -> Deps.update x pth acc) tbl !id2path
- in
- Deps.pp Format.std_formatter tbl
- with Invalid_argument err ->
- Format.eprintf "Invalid input (%s)@." err;
- exit 1
diff --git a/proofs/dopth/dune b/proofs/dopth/dune
deleted file mode 100644
index aad211b63cb2a2dda24bf1dfcf2575a92cc76ddc..0000000000000000000000000000000000000000
--- a/proofs/dopth/dune
+++ /dev/null
@@ -1,2 +0,0 @@
-(executable
- (name dopth))
diff --git a/proofs/dopth/dune-project b/proofs/dopth/dune-project
deleted file mode 100644
index ae730292676bfc91a5a5e576cfbc1f333eb7df2d..0000000000000000000000000000000000000000
--- a/proofs/dopth/dune-project
+++ /dev/null
@@ -1,2 +0,0 @@
-(lang dune 2.9)
-(cram enable)
diff --git a/proofs/dopth/psnj-dopth.asciidoc b/proofs/dopth/psnj-dopth.asciidoc
deleted file mode 100644
index 3b59219fd4f337c635de78f6b3f858b6a917481e..0000000000000000000000000000000000000000
--- a/proofs/dopth/psnj-dopth.asciidoc
+++ /dev/null
@@ -1,45 +0,0 @@
-= PSNJ-DOPTH(1)
-:Date: 2021-11-17
-
-== NAME
-
-psnj-dopth - Build a Makefile dependency list from paths
-
-== SYNOPSIS
-
-psnj-dopth
-
-== DESCRIPTION
-
-*psnj-dopth* is a filter that transform a newline-separated list
-of strings and paths into a Makefile dependency list. A path is a
-dot-separated list of integers (such as 0.1.1) or the word *root*. A
-string _s1_ depends on a string _s2_ if the path of _s1_ is a successor
-of the path of _s2_. A path _p_ is a successor of _q_ if _p_ = _q_.i
-where _i_ is an integer.
-
-== EXIT STATUS
-
-*psnj-dopth* exits with 0 on success, and something else on failure.
-
-== EXAMPLE
-
-With input
-
-----
-foo
-root
-bar
-0
-baz
-0.1
-frob
-1
-----
-
-dopth returns (the order is not specified)
-
-----
-foo: bar frob
-bar: baz
-----
diff --git a/proofs/dopth/tests/dopth.t b/proofs/dopth/tests/dopth.t
deleted file mode 100644
index d4d4b0aa5ef1b86e017640ab342770f371d2cdc6..0000000000000000000000000000000000000000
--- a/proofs/dopth/tests/dopth.t
+++ /dev/null
@@ -1,3 +0,0 @@
- $ ../dopth.exe < example.plain
- bar: baz
- foo: bar frob
diff --git a/proofs/dopth/tests/dune b/proofs/dopth/tests/dune
deleted file mode 100644
index 4188c17b72c4842cdeeb4767ab73fdfc0c23a1f1..0000000000000000000000000000000000000000
--- a/proofs/dopth/tests/dune
+++ /dev/null
@@ -1,2 +0,0 @@
-(cram
- (deps ../dopth.exe example.plain))
diff --git a/proofs/pipeline/examples/encoding/propositional_connectives.lp b/proofs/pipeline/examples/encoding/propositional_connectives.lp
index 243a6dea3971b7e95ec3f65638cfd499676f9339..b6afc53218c7a8ba6ba811a6c83e63fccc1661e6 100644
--- a/proofs/pipeline/examples/encoding/propositional_connectives.lp
+++ b/proofs/pipeline/examples/encoding/propositional_connectives.lp
@@ -1,7 +1,5 @@
// Klassische propositional logic
-// TODO: define connectives using constructive ones
require open qfo.encoding.lhol;
-require qfo.encoding.cpl as C;
constant symbol top: Prop;
constant symbol bot: Prop;
@@ -9,8 +7,11 @@ constant symbol imp: Prop → Prop → Prop;
constant symbol conj: Prop → Prop → Prop;
constant symbol disj: Prop → Prop → Prop;
constant symbol not: Prop → Prop;
-constant symbol ex: Set → (Set → Prop) → Prop;
-constant symbol all: Set → (Set → Prop) → Prop;
+constant symbol ex (a: Set): (El a → Prop) → Prop;
+symbol all (a: Set): (El a → Prop) → Prop;
+
+rule Prf (all $a $p) ↪ Πx: El $a, Prf ($p x);
+// Allow to assume over prenex quantifications
//builtin "T" ≔ El;
//builtin "P" ≔ Prf;
diff --git a/proofs/pipeline/pipe.ml b/proofs/pipeline/pipe.ml
index 8ac1ce5fbd3627863a17013ae62c02d0b2393065..92fbdde7eb11919291fcf53cfcd78962c06c94f2 100644
--- a/proofs/pipeline/pipe.ml
+++ b/proofs/pipeline/pipe.ml
@@ -14,17 +14,12 @@ let process proveit src qfo_conf =
]
and mkdeps =
process "jq" [ "-r"; {|(.name + "!" + (.incr | tostring)), .path|} ]
- and dopth = process "psnj-dopth" []
+ and dopth = process "psnj" [ "dopth" ]
and foise =
- process "psnj-qfo"
- [
- qfo_conf;
- "-e";
- "require open qfo.spec.main;";
- ]
- and chainprops depfile = process "psnj-chainprops" [ depfile ]
- and appaxiom = process "psnj-appaxiom" [ "-a"; "Prf" ]
- and solve = process "psnj-autosolve" [ "--fixed" ] in
+ process "psnj" [ "qfo"; qfo_conf; "-e"; "require open qfo.spec.main;" ]
+ and chainprops depfile = process "psnj" [ "chainprops"; depfile ]
+ and appaxiom = process "psnj" [ "appaxiom"; "-a"; "Prf" ]
+ and solve = process "psnj" [ "autosolve"; "--fixed" ] in
(* Set some file names *)
let logfile =
(* File produced by proveit if proveit is provided, src otherwise *)
diff --git a/proofs/psnj_toolbox/.gitignore b/proofs/psnj_toolbox/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..0edf27191e5b698f302fbd22adb51798864ca205
--- /dev/null
+++ b/proofs/psnj_toolbox/.gitignore
@@ -0,0 +1 @@
+psnj
diff --git a/proofs/appaxiom/.ocamlformat b/proofs/psnj_toolbox/.ocamlformat
similarity index 100%
rename from proofs/appaxiom/.ocamlformat
rename to proofs/psnj_toolbox/.ocamlformat
diff --git a/proofs/psnj_toolbox/Makefile b/proofs/psnj_toolbox/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..3d7d3904133b81c59cadf277b8af0611b8800369
--- /dev/null
+++ b/proofs/psnj_toolbox/Makefile
@@ -0,0 +1,14 @@
+PREFIX = /usr/local/
+
+bin: psnj
+
+_build/install/default/bin/psnj:
+ opam exec -- dune build
+
+psnj: _build/install/default/bin/psnj
+ ln -sf _build/install/default/bin/psnj .
+
+install:
+ cp -fL psnj ${PREFIX}/bin/psnj
+
+.PHONY: bin install
diff --git a/proofs/appaxiom/appaxiom.ml b/proofs/psnj_toolbox/bin/appaxiom.ml
similarity index 84%
rename from proofs/appaxiom/appaxiom.ml
rename to proofs/psnj_toolbox/bin/appaxiom.ml
index 70951f2d42b069d09f33d205d8141dcc3e4ef5ea..757ad332737c81fe0e4c6e100f08e1135e3e5dca 100644
--- a/proofs/appaxiom/appaxiom.ml
+++ b/proofs/psnj_toolbox/bin/appaxiom.ml
@@ -36,17 +36,15 @@ let cmd =
"$(tname) is a filter that apply some symbol on top of the type of \
symbol declarations.";
`S Manpage.s_examples;
- `Pre "echo 'symbol true : imp P P;' | psnj-appaxiom --add 'Prf'";
+ `Pre "echo 'symbol true : imp P P;' | psnj-appaxiom --app 'Prf'";
`P "outputs";
`Pre "symbol true : @Prf (=> P P);";
`S Manpage.s_bugs;
`P
"$(tname) operates a syntactic transformation. If a symbol has a \
definition, it won't be changed, so the type of the definition will \
- surely not match the declared type. To change definitions based on \
+ probably not match the declared type. To change definitions based on \
their type, coercions are needed.";
]
in
- (Term.(const appaxiom $ sym), Term.info "psnj-appaxiom" ~doc ~exits ~man)
-
-let () = Term.(exit @@ eval cmd)
+ (Term.(const appaxiom $ sym), Term.info "appaxiom" ~doc ~exits ~man)
diff --git a/proofs/autosolve/autosolve.ml b/proofs/psnj_toolbox/bin/autosolve.ml
similarity index 70%
rename from proofs/autosolve/autosolve.ml
rename to proofs/psnj_toolbox/bin/autosolve.ml
index c63f56934b0448e469efe268d72589d10575ce32..04814ea66006b325ddee11ffc078febef52dce45 100644
--- a/proofs/autosolve/autosolve.ml
+++ b/proofs/psnj_toolbox/bin/autosolve.ml
@@ -9,10 +9,18 @@ let appaxiom fixed =
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)
+ (* Lambdapi 1.0 *)
+ let script = [ Pos.none (S.P_tac_why3 None) ] in
+ (* Lambdapi 2.0 *)
+ (* let script = [ [ S.Tactic (Pos.none (S.P_tac_why3 None), []) ] ] in *)
+ let cmd =
+ S.P_symbol
+ {
+ s with
+ p_sym_prf = Some (script, Pos.none S.P_proof_end);
+ p_sym_def = true;
+ }
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@.";
@@ -42,6 +50,4 @@ let cmd =
`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)
+ (Term.(const appaxiom $ fixed), Term.info "autosolve" ~doc ~exits ~man)
diff --git a/proofs/psnj_toolbox/bin/chainprops.ml b/proofs/psnj_toolbox/bin/chainprops.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e6feb3c179e19165e93e3c0a29e1f036b6aba0df
--- /dev/null
+++ b/proofs/psnj_toolbox/bin/chainprops.ml
@@ -0,0 +1,61 @@
+open Psnj
+open Parsing
+module C = Chainprops
+
+let chainprops deps imply pp_deps =
+ let ic = open_in deps in
+ let deps = Deps.of_makefile ic in
+ close_in ic;
+ if pp_deps then (
+ Format.(
+ eprintf "=== Dependencies ===@\n";
+ Deps.pp_makefile Format.err_formatter deps;
+ eprintf "@\n====================@."));
+ let imply = Syntax.P.iden imply in
+ let props = Chainprops.propositions (Parser.parse stdin) in
+ let inferences = Chainprops.merge imply deps props in
+ let open Format in
+ pp_print_list ~pp_sep:pp_print_newline C.pp std_formatter inferences;
+ pp_print_newline std_formatter ()
+
+open Cmdliner
+
+let deps =
+ let doc =
+ "Dependencies of propositions inside Dedukti file. A line $(b,tgt: hyp0 \
+ hyp1) specifies that proposition $(b,tgt) is deduced from $(b,hyp0) and \
+ $(b,hyp1)."
+ in
+ Arg.(required & pos 0 (some non_dir_file) None & info [] ~doc ~docv:"DEPS")
+
+let imply =
+ let doc = "Use symbol $(docv) for implication" in
+ Arg.(value & opt string "imp" & info [ "imp" ] ~doc ~docv:"IMP")
+
+let pp_deps =
+ let doc = "Print parsed dependencies to stderr (for debugging purposes)" in
+ Arg.(value & flag & info [ "pp-deps" ] ~doc)
+
+let cmd =
+ let doc = "Build a proof tree from propositions and dependencies" in
+ let exits = Term.default_exits in
+ let man =
+ [
+ `S Manpage.s_description;
+ `P
+ "psnj-chainprops tranform a list of propositions given on its standard \
+ input into a list of inferences represented as implications. The \
+ hypothesese and conclusions of inferences are specified in a \
+ dependency file which follows a Makefile syntax.";
+ `S Manpage.s_examples;
+ `P "Given a file foo.dep";
+ `Pre "tgt: hyp0 hyp1";
+ `P "and the input";
+ `Pre "symbol tgt: P;\nsymbol hyp0: H0;\nsymbol hyp1: H1;";
+ `P "$(b,psnj-chainprops foo.dep) outputs";
+ `Pre
+ "symbol hyp0: H0;\nsymbol hyp1: H1;\nsymbol tgt: @imp H0 (@imp H1 P);";
+ ]
+ in
+ ( Term.(const chainprops $ deps $ imply $ pp_deps),
+ Term.info "chainprops" ~doc ~exits ~man )
diff --git a/proofs/psnj_toolbox/bin/dopth.ml b/proofs/psnj_toolbox/bin/dopth.ml
new file mode 100644
index 0000000000000000000000000000000000000000..6e9df16e711ba64e10489f0c3a88e9e8032d0369
--- /dev/null
+++ b/proofs/psnj_toolbox/bin/dopth.ml
@@ -0,0 +1,59 @@
+open Psnj
+module D = Deps
+
+let dopth fixed =
+ if fixed then Format.set_geometry ~max_indent:16 ~margin:80;
+ let id2path =
+ (* Read ids and paths from stdin *)
+ let id2path = ref D.IdMap.empty in
+ (try
+ while true do
+ let id = input_line stdin in
+ let pth = input_line stdin in
+ id2path := D.(IdMap.add (Id.make id) (Path.of_string pth) !id2path)
+ done
+ with End_of_file -> ());
+ !id2path
+ in
+ try
+ let tbl = D.of_paths id2path in
+ D.pp_makefile Format.std_formatter tbl
+ with Invalid_argument err ->
+ Format.eprintf "Invalid input (%s)@." err;
+ exit 1
+
+open Cmdliner
+
+let fixed =
+ let doc = "Fix terminal geometry to avoid depending on environment" in
+ Arg.(value & flag & info [ "fixed" ] ~doc)
+
+let cmd =
+ let exits = Term.default_exits in
+ let doc = "Build a Makefile dependency list from paths" in
+ let man =
+ [
+ `S Manpage.s_description;
+ `P
+ "$(tname) is a filter that transform newline-separated list of strings \
+ and paths into a Makefile dependency list. A path is a dot-separated \
+ list of integers (such as 0.1.1) or the word $(b,root). A string \
+ $(i,s1) depends on a string $(i,s2) if the path of $(i,s1) is a \
+ successor of the path of $(i,s2). A path $(i,p) is a successor of \
+ $(i,q) if $(i,p) = $(i,q).$(i,i) where $(i,i) is a natural number.";
+ `S Manpage.s_examples;
+ `P "With input";
+ `Pre {|foo
+root
+bar
+0
+baz
+0.1
+frob
+1|};
+ `P "$(tname) outputs (the order is not specified";
+ `Pre {|foo: bar frob
+bar: baz|};
+ ]
+ in
+ (Term.(const dopth $ fixed), Term.info "dopth" ~exits ~man ~doc)
diff --git a/proofs/psnj_toolbox/bin/dune b/proofs/psnj_toolbox/bin/dune
new file mode 100644
index 0000000000000000000000000000000000000000..d28c3fabbdbd436bb617516fcec012506d1584d7
--- /dev/null
+++ b/proofs/psnj_toolbox/bin/dune
@@ -0,0 +1,12 @@
+(executable
+ (public_name psnj)
+ (name main)
+ (modules main dopth chainprops appaxiom autosolve qfo)
+ (libraries
+ personoj
+ personoj.qfo
+ cmdliner
+ lambdapi.common
+ lambdapi.handle
+ lambdapi.parsing
+ lambdapi.lplib))
diff --git a/proofs/psnj_toolbox/bin/main.ml b/proofs/psnj_toolbox/bin/main.ml
new file mode 100644
index 0000000000000000000000000000000000000000..7287e787c3fc21a21be02fa90b681e4ef0ea8977
--- /dev/null
+++ b/proofs/psnj_toolbox/bin/main.ml
@@ -0,0 +1,9 @@
+open Cmdliner
+
+let default_cmd =
+ let doc = "A set of tools to manipulate propositions as inference steps" in
+ let exits = Term.default_exits in
+ (Term.(ret @@ const @@ `Help (`Pager, None)), Term.info "psnj" ~doc ~exits)
+
+let cmds = [ Dopth.cmd; Chainprops.cmd; Appaxiom.cmd; Autosolve.cmd; Qfo.cmd ]
+let () = Term.(exit @@ eval_choice default_cmd cmds)
diff --git a/proofs/qfo/bin/main.ml b/proofs/psnj_toolbox/bin/qfo.ml
similarity index 85%
rename from proofs/qfo/bin/main.ml
rename to proofs/psnj_toolbox/bin/qfo.ml
index b6c156cbcdb3bdf41612b0b576b06f41319c136f..ec31b58f765366b83b07b365fb929364b12f081a 100644
--- a/proofs/qfo/bin/main.ml
+++ b/proofs/psnj_toolbox/bin/qfo.ml
@@ -16,7 +16,8 @@ let compile_ast (sig_st : Sig_state.t) (ast : Syntax.ast) : Sig_state.t =
let ss = ref sig_st in
let compile = Compile.Pure.compile false in
let consume cmd = ss := Command.handle compile !ss cmd in
- Stream.iter consume ast; !ss
+ Stream.iter consume ast;
+ !ss
(** [compile_props sig_st ast] compiles an AST made of symbol declarations
of the form [symbol foo: bar;]. Term [bar] need not be of type [TYPE]. *)
@@ -39,14 +40,17 @@ let compile_props (sig_st : Sig_state.t) (ast : Syntax.ast) :
try
let te = Scope.scope_term false !ss [] pty in
fst (Unif.Infer.infer [] (Pos.none te))
- with Error.Fatal (p, msg) -> print_err p msg; exit 1
+ with Error.Fatal (p, msg) ->
+ print_err p msg;
+ exit 1
in
out := (p_sym_nam.elt, ty) :: !out
| _ ->
Format.eprintf "Invalid input: only symbol declarations allowed@.";
exit 1
in
- Stream.iter consume ast; List.rev !out
+ Stream.iter consume ast;
+ List.rev !out
let new_sig_state (mp : Path.t) : Sig_state.t =
Sig_state.(of_sign (create_sign mp))
@@ -56,7 +60,7 @@ let new_sig_state (mp : Path.t) : Sig_state.t =
let translate (lib_root : string option) (map_dir : (string * string) list)
(mapfile : string) (eval : string list) : unit =
(* Get symbol mappings *)
- let mapping = Qfo.Mappings.of_file mapfile in
+ let mapping = PsnjQfo.Mappings.of_file mapfile in
let pvs_cert, pvs_connectives, propositional_connectives =
let f s =
try StrMap.find s mapping
@@ -73,7 +77,9 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
Library.set_lib_root lib_root;
List.iter Library.add_mapping map_dir;
Console.State.push ()
- with Error.Fatal (pos, msg) -> print_err pos msg; exit 1);
+ with Error.Fatal (pos, msg) ->
+ print_err pos msg;
+ exit 1);
(* Try to find lambdapi pkgs from current working directory, and do
nothing if it fails *)
(try
@@ -95,7 +101,7 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
print_err pos msg;
exit 1
in
- let ps = Qfo.Encodings.mkpredicate_subtyping pvs_cert pvs_cert_ss in
+ let ps = PsnjQfo.Encodings.mkpredicate_subtyping pvs_cert pvs_cert_ss in
Console.out 1 "Loaded PVS-Cert encoding";
let pvs_c =
let pvs_connectives_ss =
@@ -111,7 +117,7 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
print_err p m;
exit 2
in
- Qfo.Encodings.mkconnectives pvs_connectives pvs_connectives_ss
+ PsnjQfo.Encodings.mkconnectives pvs_connectives pvs_connectives_ss
in
let prop_calc_ss =
let ss = new_sig_state mp in
@@ -122,7 +128,7 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
compile_ast ss ast
in
let prop_c =
- Qfo.Encodings.mkconnectives propositional_connectives prop_calc_ss
+ PsnjQfo.Encodings.mkconnectives propositional_connectives prop_calc_ss
in
Console.out 1 "Loaded classical propositional calculus";
let qfo_ss =
@@ -149,7 +155,7 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
(* Load propositions from stdin in [qfo_ss] *)
let props = compile_props qfo_ss (Parser.parse stdin) in
let transpile_print (name, ty) =
- let open Qfo.Transpile in
+ let open PsnjQfo.Transpile in
try
let propty = translate_term ~ps ~prop_c ~pvs_c ty in
Format.printf "@[symbol %s:@ %a;@]@." name Print.pp_term propty
@@ -203,56 +209,56 @@ let cmd =
let doc = "Convert PVS-Cert encoded file quasi first order encoded files" in
let man =
[
- `S Manpage.s_description
- ; `P
+ `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 simple type theory with non dependent \
- logical connectives."
- ; `P
+ logical connectives.";
+ `P
"The program requires all its source files to be in the package \
$(b,qfo). The easiest way to do that is to place the source files in \
a directory where there is a $(b,lambdapi.pkg) file with the line \
- $(b,root_path=qfo)."
- ; `P
+ $(b,root_path=qfo).";
+ `P
"To convert files, the program needs identify the symbols of the \
encoding. The mapping allows to indicate the name of such symbols. \
- This mapping is a JSON object with the following structure"
- ; `Pre
+ This mapping is a JSON object with the following structure";
+ `Pre
"{ \"pvs_cert\": ...,\n\
\ \"pvs_connectives\": ...,\n\
- \ \"propositional_connectives\": ... }"
- ; `P
+ \ \"propositional_connectives\": ... }";
+ `P
"where the value associated to \"pvs_cert\" is an object that define \
- the following form"
- ; `Pre "{ \"subset\": STRING }"
- ; `P
+ the following form";
+ `Pre "{ \"subset\": STRING }";
+ `P
"and the values associated to both \"pvs_connectives\" and \
- \"propositional_connectives\" must be of the form"
- ; `Pre
+ \"propositional_connectives\" must be of the form";
+ `Pre
"{ \"truth\": STRING; \"falsity\": STRING;\n\
\ \"implication\": STRING;\n\
\ \"negation\": STRING; \n\
\ \"conjunction\": STRING; \"disjunction\": STRING;\n\
- \ \"existential\": STRING; \"universal\": STRING }"
- ; `P
+ \ \"existential\": STRING; \"universal\": STRING }";
+ `P
"The object \"pvs_cert\" define symbols used to encode PVS-Cert while \
\"pvs_connectives\" and \"propositional_connectives\" define logical \
connectors: connectors from \"pvs_connectives\" are replaced by \
- connectors from \"propositional_connectives\"."
- ; `P
+ connectors from \"propositional_connectives\".";
+ `P
"Symbols mentioned in $(b,\"pvs_cert\") are expected to be found in \
modules $(b,qfo.encoding.pvs_cert) and $(b,qfo.encoding.lhol), \
symbols mentioned in $(b,\"pvs_connectives\") are expected to be \
found in module $(b,qfo.encoding.pvs_connectives) and symbols \
mentioned in $(b,\"propositional_connectives\") are expected to be \
- found in module $(b,qfo.encoding.proposisitional_connectives)."
- ; `P
+ found in module $(b,qfo.encoding.proposisitional_connectives).";
+ `P
"Furthermore, if the standard input uses symbols from some other \
- module \"mod\", it can be opened using $(b,-e 'require open mod;')."
- ; `S Manpage.s_examples
- ; `P "Let qfo.json be the following json file"
- ; `Pre
+ module \"mod\", it can be opened using $(b,-e 'require open mod;').";
+ `S Manpage.s_examples;
+ `P "Let qfo.json be the following json file";
+ `Pre
{|{
"pvs_cert": {
"subset": "psub"
@@ -277,19 +283,17 @@ let cmd =
"existential": "ex",
"universal": "all"
}
-}|}
- ; `P "and with the following input,"
- ; `Pre "symbol true : ∀ {prop} (λ p: El prop, p ⇒ (λ _: Prf p, p));"
- ; `P "The program outputs"
- ; `Pre "symbol true: @∀ prop (λ p: El prop, imp p p);"
- ; `S Manpage.s_bugs
- ; `P
+}|};
+ `P "and with the following input,";
+ `Pre "symbol true : ∀ {prop} (λ p: El prop, p ⇒ (λ _: Prf p, p));";
+ `P "The program outputs";
+ `Pre "symbol true: @∀ prop (λ p: El prop, imp p p);";
+ `S Manpage.s_bugs;
+ `P
"If the input opens some module (using \"open mod\"), then symbols \
- from this module will appear fully qualified."
+ from this module will appear fully qualified.";
]
in
let exits = Term.default_exits in
- ( Term.(const translate $ lib_root $ map_dir $ mapfile $ lp_eval)
- , Term.info "psnj-qfo" ~doc ~man ~exits )
-
-let () = Term.(exit @@ eval cmd)
+ ( Term.(const translate $ lib_root $ map_dir $ mapfile $ lp_eval),
+ Term.info "qfo" ~doc ~man ~exits )
diff --git a/proofs/psnj_toolbox/dune-project b/proofs/psnj_toolbox/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..bef01ac58fb9acd8879340ac34ef4d1a1ad9ef99
--- /dev/null
+++ b/proofs/psnj_toolbox/dune-project
@@ -0,0 +1,10 @@
+(lang dune 2.9)
+(name personoj)
+
+(generate_opam_files true)
+(cram enable)
+
+(package
+ (name personoj)
+ (synopsis "todo")
+ (depends cmdliner angstrom lambdapi))
diff --git a/proofs/psnj_toolbox/lib/chainprops.ml b/proofs/psnj_toolbox/lib/chainprops.ml
new file mode 100644
index 0000000000000000000000000000000000000000..c4d991e13242ba870b5e4aacf8f8abeab5a308e1
--- /dev/null
+++ b/proofs/psnj_toolbox/lib/chainprops.ml
@@ -0,0 +1,40 @@
+open Common
+open Parsing
+module S = Syntax
+
+type decl = Deps.Id.t * S.p_term
+(** A proposition declaration with a name and a type. *)
+
+(** [pp ppf decl] pretty prints declaration [decl] to formatter [ppf]. *)
+let pp (ppf : Format.formatter) ((n, ty) : decl) : unit =
+ Format.fprintf ppf "@[symbol %a:@ %a;@]" Deps.Id.pp n Pretty.term ty
+
+(** [propositions ast] returns the list of propositions as pairs
+ [(name,ty)] where [name] is the name of the proposition and [ty]
+ is its type. *)
+let propositions (ast : S.ast) : decl list =
+ let props : decl list ref = ref [] in
+ let match_decl = function
+ | S.P_symbol { p_sym_nam; p_sym_typ = Some ty; _ } ->
+ (Deps.Id.make p_sym_nam.elt, ty)
+ | _ ->
+ failwith
+ "Invalid Dedukti source file: only symbol declarations are supported"
+ in
+ Stream.iter (fun c -> props := match_decl c.Pos.elt :: !props) ast;
+ List.rev !props
+
+(** [merge imp deps props] transform each proposition of [props] into
+ implications (the implication is defined by [imp]) from its
+ dependencies specified in [deps] to itself. *)
+let merge (imp : S.p_term) (deps : Deps.t) (props : decl list) : decl list =
+ let fn ((name, ty) : decl) : decl =
+ let deps = try Deps.get name deps with Not_found -> [] in
+ let f dep acc =
+ let d_ty = List.assoc dep props in
+ Syntax.P.(appl (appl imp d_ty) acc)
+ in
+ let ty = List.fold_right f deps ty in
+ (name, ty)
+ in
+ List.map fn props
diff --git a/proofs/psnj_toolbox/lib/deps.ml b/proofs/psnj_toolbox/lib/deps.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3ca525a5e0e2446945c746b6d57cca963e5d655c
--- /dev/null
+++ b/proofs/psnj_toolbox/lib/deps.ml
@@ -0,0 +1,100 @@
+(** Paths are (possibly) empty lists of natural numbers. *)
+module Path = struct
+ type t = int list
+
+ let is_predecessor (p : t) (q : t) : bool =
+ match q with [] -> false | _ :: q_tl -> q_tl = p
+
+ let of_string (s : string) : t =
+ if s = "root" then []
+ else
+ try String.split_on_char '.' s |> List.rev_map int_of_string
+ with Failure err ->
+ Format.eprintf "Invalid path: %s@." s;
+ invalid_arg err
+end
+
+module Id = struct
+ type t = string
+
+ let make (name : string) : t = name
+ let pp = Format.pp_print_string
+ let compare = String.compare
+end
+
+module IdMap = Map.Make (struct
+ type t = Id.t
+
+ let compare = Id.compare
+end)
+
+type t = Id.t list IdMap.t
+
+(** [add id d t] adds dependency [d] to [id] in table [t]. If [id]
+ is not bound, it is added to the table. *)
+let add (id : Id.t) (d : Id.t) (t : t) : t =
+ let deps =
+ match IdMap.find_opt id t with None -> [] | Some deps -> d :: deps
+ in
+ IdMap.add id (d :: deps) t
+
+let get (id : Id.t) (m : t) : Id.t list = IdMap.find id m
+
+(** [update x x_pth tbl id_paths] updates the entries of the table
+ [tbl] adding [id]: if [(e,q)] is an element of [id_paths], [x_th]
+ is the successor of [q] then [x] is added to the dependencies of
+ element [e] of the table *)
+let update (x : Id.t) (x_pth : Path.t) (tbl : t) (id_paths : Path.t IdMap.t) : t
+ =
+ let f (y : Id.t) (y_pth : Path.t) (t : t) : t =
+ if Path.is_predecessor y_pth x_pth then add y x t else t
+ in
+ IdMap.fold f id_paths tbl
+
+let of_paths (m : Path.t IdMap.t) : t =
+ IdMap.fold (fun x pth acc -> update x pth acc m) m IdMap.empty
+
+let pp_makefile (ppf : Format.formatter) (tbl : t) : unit =
+ let open Format in
+ let pp_deplist ppf (l : Id.t list) : unit =
+ let pp_sep ppf () = pp_print_space ppf () in
+ let l = List.sort_uniq Id.compare l in
+ pp_print_list ~pp_sep Id.pp ppf l
+ in
+ let pprint_d (id : Id.t) (d : Id.t list) : unit =
+ fprintf ppf "@[<h>%a:@ %a@]@\n" Id.pp id pp_deplist d
+ in
+ IdMap.iter pprint_d tbl
+
+module P = struct
+ open Angstrom
+
+ let is_space = function ' ' | '\t' -> true | _ -> false
+ let blank = skip_while is_space
+ let blank1 = satisfy is_space *> blank
+ let eol = string "\n\r" <|> string "\n"
+ let colon = blank *> char ':' <* blank
+
+ (* Word characters taken from the parser of lambdapi. *)
+ let is_wordchar = function
+ | ' ' | '\r' | '\t' | '\n' | '(' | ')' | '{' | '}' | '[' | ']' | ':' | '.'
+ | '`' | '"' ->
+ false
+ | _ -> true
+
+ let word = take_while1 is_wordchar
+ let line = both (word <* colon) (sep_by blank1 word)
+ let deps = many (line <* many1 eol)
+
+ let parse (ic : in_channel) : (string * string list) list =
+ let file = really_input_string ic (in_channel_length ic) in
+ match parse_string ~consume:All deps file with
+ | Ok v -> v
+ | Error msg -> failwith msg
+end
+
+let of_makefile (ic : in_channel) : t =
+ let elts = P.parse ic in
+ List.fold_right
+ (fun (src, tgts) acc -> IdMap.add src tgts acc)
+ elts IdMap.empty
diff --git a/proofs/psnj_toolbox/lib/deps.mli b/proofs/psnj_toolbox/lib/deps.mli
new file mode 100644
index 0000000000000000000000000000000000000000..c0a3f7d1fd26b4cc4115e07bebf9e5d443489913
--- /dev/null
+++ b/proofs/psnj_toolbox/lib/deps.mli
@@ -0,0 +1,40 @@
+module Path : sig
+ type t
+
+ val is_predecessor : t -> t -> bool
+ (** [is_predecessor p q] is true if [q = p.i] ([p] is closer to the
+ root). *)
+
+ val of_string : string -> t
+ (** [of_string s] parses a string [s] into a path. The string [s]
+ may be ["root"] or a dot-separated list of integers.
+ @raise Invalid_argument when [s] is ill-formed *)
+end
+
+module Id : sig
+ type t
+
+ val make : string -> t
+ val pp : Format.formatter -> t -> unit
+ val compare : t -> t -> int
+end
+
+module IdMap : Map.S with type key = Id.t
+
+type t
+(** The type of dependencies collections *)
+
+val get : Id.t -> t -> Id.t list
+(** [get id c] returns the dependencies of identifier [id] in collection
+ [c]. *)
+
+val of_paths : Path.t IdMap.t -> t
+(** [of_paths ps] creates a dependencies collection out of a mapping
+ [ps] from identifiers to paths. *)
+
+val pp_makefile : Format.formatter -> t -> unit
+(** [pp_makefile ppf c] prints dependencies of [c] in makefile syntax
+ on formatter [ppf]. *)
+
+val of_makefile : in_channel -> t
+(** [of_makefile ic] parses a makefile dependency list from channel [ic]. *)
diff --git a/proofs/psnj_toolbox/lib/dune b/proofs/psnj_toolbox/lib/dune
new file mode 100644
index 0000000000000000000000000000000000000000..e3291041a24bb94918e601c2a29d7f1ca4d18c2f
--- /dev/null
+++ b/proofs/psnj_toolbox/lib/dune
@@ -0,0 +1,4 @@
+(library
+ (name psnj)
+ (public_name personoj)
+ (libraries angstrom lambdapi.common lambdapi.parsing lambdapi.core))
diff --git a/proofs/qfo/lib/dune b/proofs/psnj_toolbox/lib/qfo/dune
similarity index 69%
rename from proofs/qfo/lib/dune
rename to proofs/psnj_toolbox/lib/qfo/dune
index c767a7329edef43bcdee9fa9143f9a31af30bc71..9a493de4446f5c8e4e7b36c589d9d1bd517d2585 100644
--- a/proofs/qfo/lib/dune
+++ b/proofs/psnj_toolbox/lib/qfo/dune
@@ -1,8 +1,9 @@
(library
+ (public_name personoj.qfo)
(libraries
yojson
lambdapi.common
lambdapi.lplib
lambdapi.parsing
lambdapi.core)
- (name qfo))
+ (name PsnjQfo))
diff --git a/proofs/qfo/lib/encodings.ml b/proofs/psnj_toolbox/lib/qfo/encodings.ml
similarity index 73%
rename from proofs/qfo/lib/encodings.ml
rename to proofs/psnj_toolbox/lib/qfo/encodings.ml
index f05ec3cbb8d9871d451bda0451c90ce36192ae8d..05cb31ac9e2462c8e3809a0fe8f00ff0be8a440b 100644
--- a/proofs/qfo/lib/encodings.ml
+++ b/proofs/psnj_toolbox/lib/qfo/encodings.ml
@@ -27,14 +27,14 @@ let mkpredicate_subtyping (map : mapping) (sig_st : Sig_state.t) :
{ subset = s "subset" }
type connectives = {
- truth : T.sym
- ; falsity : T.sym
- ; implication : T.sym
- ; negation : T.sym
- ; conjunction : T.sym
- ; disjunction : T.sym
- ; existential : T.sym
- ; universal : T.sym
+ truth : T.sym;
+ falsity : T.sym;
+ implication : T.sym;
+ negation : T.sym;
+ conjunction : T.sym;
+ disjunction : T.sym;
+ existential : T.sym;
+ universal : T.sym;
}
(** Logical connectives *)
@@ -46,12 +46,12 @@ let mkconnectives (map : (string * string) list) (sig_st : Sig_state.t) :
failwith (Format.sprintf "Symbol \"%s\" not found in mapping" name)
in
{
- truth = s "truth"
- ; falsity = s "falsity"
- ; negation = s "negation"
- ; implication = s "implication"
- ; conjunction = s "conjunction"
- ; disjunction = s "disjunction"
- ; existential = s "existential"
- ; universal = s "universal"
+ truth = s "truth";
+ falsity = s "falsity";
+ negation = s "negation";
+ implication = s "implication";
+ conjunction = s "conjunction";
+ disjunction = s "disjunction";
+ existential = s "existential";
+ universal = s "universal";
}
diff --git a/proofs/qfo/lib/encodings.mli b/proofs/psnj_toolbox/lib/qfo/encodings.mli
similarity index 82%
rename from proofs/qfo/lib/encodings.mli
rename to proofs/psnj_toolbox/lib/qfo/encodings.mli
index 5598bbdfe944e3e0ea631a830146c1ad64403c1f..edfb8262b926afb719b2cfc3343ca15280af1dae 100644
--- a/proofs/qfo/lib/encodings.mli
+++ b/proofs/psnj_toolbox/lib/qfo/encodings.mli
@@ -19,14 +19,14 @@ type predicate_subtyping = { subset : Term.sym }
val mkpredicate_subtyping : mapping -> Sig_state.t -> predicate_subtyping
type connectives = {
- truth : Term.sym
- ; falsity : Term.sym
- ; implication : Term.sym
- ; negation : Term.sym
- ; conjunction : Term.sym
- ; disjunction : Term.sym
- ; existential : Term.sym
- ; universal : Term.sym
+ truth : Term.sym;
+ falsity : Term.sym;
+ implication : Term.sym;
+ negation : Term.sym;
+ conjunction : Term.sym;
+ disjunction : Term.sym;
+ existential : Term.sym;
+ universal : Term.sym;
}
(** Logical connectives. They may be dependent or non-dependent. *)
diff --git a/proofs/qfo/lib/mappings.ml b/proofs/psnj_toolbox/lib/qfo/mappings.ml
similarity index 100%
rename from proofs/qfo/lib/mappings.ml
rename to proofs/psnj_toolbox/lib/qfo/mappings.ml
diff --git a/proofs/qfo/lib/mappings.mli b/proofs/psnj_toolbox/lib/qfo/mappings.mli
similarity index 100%
rename from proofs/qfo/lib/mappings.mli
rename to proofs/psnj_toolbox/lib/qfo/mappings.mli
diff --git a/proofs/qfo/lib/transpile.ml b/proofs/psnj_toolbox/lib/qfo/transpile.ml
similarity index 94%
rename from proofs/qfo/lib/transpile.ml
rename to proofs/psnj_toolbox/lib/qfo/transpile.ml
index 37bf94c6b002b405fa2bd7356047431a650b44a8..17e0d5f7fbf9d77e91d2b58684ea91cb8413bf7e 100644
--- a/proofs/qfo/lib/transpile.ml
+++ b/proofs/psnj_toolbox/lib/qfo/transpile.ml
@@ -16,9 +16,9 @@ let translate_term ~(ps : E.predicate_subtyping) ~(pvs_c : E.connectives)
~(prop_c : E.connectives) (t : T.term) : T.term =
let binary =
[
- (pvs_c.implication, prop_c.implication)
- ; (pvs_c.conjunction, prop_c.conjunction)
- ; (pvs_c.disjunction, prop_c.disjunction)
+ (pvs_c.implication, prop_c.implication);
+ (pvs_c.conjunction, prop_c.conjunction);
+ (pvs_c.disjunction, prop_c.disjunction);
]
in
let rec f (t : T.term) =
diff --git a/proofs/appaxiom/appaxiom.opam b/proofs/psnj_toolbox/personoj.opam
similarity index 83%
rename from proofs/appaxiom/appaxiom.opam
rename to proofs/psnj_toolbox/personoj.opam
index b0418660e6cef4158b109a22dd9fb4d5ecf58c08..ddcfb66995694475013bf1b4efa62ab02805875c 100644
--- a/proofs/appaxiom/appaxiom.opam
+++ b/proofs/psnj_toolbox/personoj.opam
@@ -1,10 +1,10 @@
# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
-synopsis: "Apply something on Dedukti axioms"
-maintainer: ["dedukti-dev@inria.fr"]
+synopsis: "todo"
depends: [
"dune" {>= "2.9"}
"cmdliner"
+ "angstrom"
"lambdapi"
"odoc" {with-doc}
]
diff --git a/proofs/psnj_toolbox/test/appaxiom.t b/proofs/psnj_toolbox/test/appaxiom.t
new file mode 100644
index 0000000000000000000000000000000000000000..389d2a836816b0a14831904bcbbb510aba364228
--- /dev/null
+++ b/proofs/psnj_toolbox/test/appaxiom.t
@@ -0,0 +1,5 @@
+ $ echo 'symbol true : imp P P;' | psnj appaxiom
+ symbol true : @Prf (imp P P);
+
+ $ echo 'symbol x : nat;' | psnj appaxiom --app 'El'
+ symbol x : @El nat;
diff --git a/proofs/autosolve/tests/autosolve.t b/proofs/psnj_toolbox/test/autosolve.t
similarity index 53%
rename from proofs/autosolve/tests/autosolve.t
rename to proofs/psnj_toolbox/test/autosolve.t
index 022ed716738ec4c0c94c4a3c8cefbbf7b19684dd..b2861f5d21cdb0286a88ee40d27d5d4d3005314b 100644
--- a/proofs/autosolve/tests/autosolve.t
+++ b/proofs/psnj_toolbox/test/autosolve.t
@@ -1,10 +1,10 @@
- $ echo 'symbol true: foo bar baz;' | ../autosolve.exe --fixed
+ $ echo 'symbol true : foo bar baz;' | psnj autosolve --fixed
symbol true : foo bar baz ≔
begin
why3;
end;
- $ echo 'symbol foo: TYPE; symbol bar: TYPE;' | ../autosolve.exe --fixed
+ $ echo 'symbol foo: TYPE; symbol bar: TYPE;' | psnj autosolve --fixed
symbol foo : TYPE ≔
begin
why3;
@@ -13,3 +13,4 @@
begin
why3;
end;
+
diff --git a/proofs/chainprops/test/example.dep b/proofs/psnj_toolbox/test/ch_example.dep
similarity index 100%
rename from proofs/chainprops/test/example.dep
rename to proofs/psnj_toolbox/test/ch_example.dep
diff --git a/proofs/chainprops/test/example.lp b/proofs/psnj_toolbox/test/ch_example.lp
similarity index 100%
rename from proofs/chainprops/test/example.lp
rename to proofs/psnj_toolbox/test/ch_example.lp
diff --git a/proofs/chainprops/test/foo.dep b/proofs/psnj_toolbox/test/ch_foo.dep
similarity index 100%
rename from proofs/chainprops/test/foo.dep
rename to proofs/psnj_toolbox/test/ch_foo.dep
diff --git a/proofs/chainprops/test/foo.lp b/proofs/psnj_toolbox/test/ch_foo.lp
similarity index 100%
rename from proofs/chainprops/test/foo.lp
rename to proofs/psnj_toolbox/test/ch_foo.lp
diff --git a/proofs/chainprops/test/run.t b/proofs/psnj_toolbox/test/chainprops.t
similarity index 70%
rename from proofs/chainprops/test/run.t
rename to proofs/psnj_toolbox/test/chainprops.t
index c253b0459675dd7f2a6276151735ec813947f452..ca7eddeaa19c9d7e66b177e5cb9b740f477e1016 100644
--- a/proofs/chainprops/test/run.t
+++ b/proofs/psnj_toolbox/test/chainprops.t
@@ -1,10 +1,10 @@
- $ ../chainprops.exe example.dep < example.lp
+ $ psnj chainprops ch_example.dep < ch_example.lp
symbol tgt: @imp H0 (@imp H1 P);
symbol hyp0: H0;
symbol hyp1: H1;
- $ ../chainprops.exe foo.dep < foo.lp
+ $ psnj chainprops ch_foo.dep < ch_foo.lp
symbol foo: @imp Bar (@imp Baz Foo);
symbol bar: @imp Frob (@imp Nitz (@imp Baz Bar));
symbol baz: Baz;
diff --git a/proofs/psnj_toolbox/test/dopth.t b/proofs/psnj_toolbox/test/dopth.t
new file mode 100644
index 0000000000000000000000000000000000000000..12af2d4310d25fc33b35ae9cfc9768a36450b8a2
--- /dev/null
+++ b/proofs/psnj_toolbox/test/dopth.t
@@ -0,0 +1,3 @@
+ $ psnj dopth < example.plain
+ bar: baz
+ foo: bar frob
diff --git a/proofs/psnj_toolbox/test/dune b/proofs/psnj_toolbox/test/dune
new file mode 100644
index 0000000000000000000000000000000000000000..177990a1e114abc01c64ff830641bbb0546c16e9
--- /dev/null
+++ b/proofs/psnj_toolbox/test/dune
@@ -0,0 +1,5 @@
+(test
+ (name psnj_toolbox))
+
+(cram
+ (deps example.plain ch_foo.dep ch_foo.lp ch_example.dep ch_example.lp))
diff --git a/proofs/dopth/tests/example.plain b/proofs/psnj_toolbox/test/example.plain
similarity index 100%
rename from proofs/dopth/tests/example.plain
rename to proofs/psnj_toolbox/test/example.plain
diff --git a/proofs/autosolve/.ocamlformat b/proofs/psnj_toolbox/test/psnj_toolbox.ml
similarity index 100%
rename from proofs/autosolve/.ocamlformat
rename to proofs/psnj_toolbox/test/psnj_toolbox.ml
diff --git a/proofs/psnj_toolbox/test/qfo/dune b/proofs/psnj_toolbox/test/qfo/dune
new file mode 100644
index 0000000000000000000000000000000000000000..1333a843e4e24fb0388d0a8f66c56f5fd90406de
--- /dev/null
+++ b/proofs/psnj_toolbox/test/qfo/dune
@@ -0,0 +1,8 @@
+(cram
+ (deps
+ lambdapi.pkg
+ withsymb_thms.lp
+ false.lp
+ qfo.json
+ (glob_files encoding/*)
+ (glob_files spec/*)))
diff --git a/proofs/qfo/test/encoding/cpl.lp b/proofs/psnj_toolbox/test/qfo/encoding/cpl.lp
similarity index 100%
rename from proofs/qfo/test/encoding/cpl.lp
rename to proofs/psnj_toolbox/test/qfo/encoding/cpl.lp
diff --git a/proofs/qfo/test/encoding/lhol.lp b/proofs/psnj_toolbox/test/qfo/encoding/lhol.lp
similarity index 100%
rename from proofs/qfo/test/encoding/lhol.lp
rename to proofs/psnj_toolbox/test/qfo/encoding/lhol.lp
diff --git a/proofs/qfo/test/encoding/propositional_connectives.lp b/proofs/psnj_toolbox/test/qfo/encoding/propositional_connectives.lp
similarity index 100%
rename from proofs/qfo/test/encoding/propositional_connectives.lp
rename to proofs/psnj_toolbox/test/qfo/encoding/propositional_connectives.lp
diff --git a/proofs/qfo/test/encoding/pvs_cert.lp b/proofs/psnj_toolbox/test/qfo/encoding/pvs_cert.lp
similarity index 100%
rename from proofs/qfo/test/encoding/pvs_cert.lp
rename to proofs/psnj_toolbox/test/qfo/encoding/pvs_cert.lp
diff --git a/proofs/qfo/test/encoding/pvs_connectives.lp b/proofs/psnj_toolbox/test/qfo/encoding/pvs_connectives.lp
similarity index 100%
rename from proofs/qfo/test/encoding/pvs_connectives.lp
rename to proofs/psnj_toolbox/test/qfo/encoding/pvs_connectives.lp
diff --git a/proofs/qfo/test/false.lp b/proofs/psnj_toolbox/test/qfo/false.lp
similarity index 100%
rename from proofs/qfo/test/false.lp
rename to proofs/psnj_toolbox/test/qfo/false.lp
diff --git a/proofs/qfo/test/lambdapi.pkg b/proofs/psnj_toolbox/test/qfo/lambdapi.pkg
similarity index 100%
rename from proofs/qfo/test/lambdapi.pkg
rename to proofs/psnj_toolbox/test/qfo/lambdapi.pkg
diff --git a/proofs/qfo/test/qfo.json b/proofs/psnj_toolbox/test/qfo/qfo.json
similarity index 100%
rename from proofs/qfo/test/qfo.json
rename to proofs/psnj_toolbox/test/qfo/qfo.json
diff --git a/proofs/qfo/test/qfo.t b/proofs/psnj_toolbox/test/qfo/qfo.t
similarity index 73%
rename from proofs/qfo/test/qfo.t
rename to proofs/psnj_toolbox/test/qfo/qfo.t
index f437d2ebcc01575c2605a5293857d500513bdcee..9abbedebb7bb60b623669addff0c0a38260f73a4 100644
--- a/proofs/qfo/test/qfo.t
+++ b/proofs/psnj_toolbox/test/qfo/qfo.t
@@ -1,16 +1,16 @@
- $ psnj-qfo qfo.json < false.lp
+ $ psnj qfo qfo.json < false.lp
Loaded package file from "$TESTCASE_ROOT"
symbol false: all prop (λ p: El prop, p);
symbol true: all prop (λ p: El prop, imp p p);
- $ echo 'symbol tt: ∀ {prop} (λ p: El prop, p ∧ (λ _, p));' | psnj-qfo qfo.json
+ $ echo 'symbol tt: ∀ {prop} (λ p: El prop, p ∧ (λ _, p));' | psnj qfo qfo.json
Loaded package file from "$TESTCASE_ROOT"
symbol tt: all prop (λ p: El prop, conj p p);
- $ echo 'symbol tt: ∃ {prop} (λ p: El prop, p);' | psnj-qfo qfo.json
+ $ echo 'symbol tt: ∃ {prop} (λ p: El prop, p);' | psnj qfo qfo.json
Loaded package file from "$TESTCASE_ROOT"
symbol tt: ex prop (λ p: El prop, p);
- $ psnj-qfo -e 'require open qfo.spec.withsymb;' qfo.json < withsymb_thms.lp
+ $ psnj qfo -e 'require open qfo.spec.withsymb;' qfo.json < withsymb_thms.lp
Loaded package file from "$TESTCASE_ROOT"
symbol trivial: imp qfo.spec.withsymb.P qfo.spec.withsymb.P;
diff --git a/proofs/qfo/test/spec/withsymb.lp b/proofs/psnj_toolbox/test/qfo/spec/withsymb.lp
similarity index 100%
rename from proofs/qfo/test/spec/withsymb.lp
rename to proofs/psnj_toolbox/test/qfo/spec/withsymb.lp
diff --git a/proofs/qfo/test/withsymb_thms.lp b/proofs/psnj_toolbox/test/qfo/withsymb_thms.lp
similarity index 100%
rename from proofs/qfo/test/withsymb_thms.lp
rename to proofs/psnj_toolbox/test/qfo/withsymb_thms.lp
diff --git a/proofs/qfo/.gitignore b/proofs/qfo/.gitignore
deleted file mode 100644
index 93b95a23816f1aacc5e0b8e98be1cc23bae41ce5..0000000000000000000000000000000000000000
--- a/proofs/qfo/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-psnj-qfo
-_build
diff --git a/proofs/qfo/.ocamlformat b/proofs/qfo/.ocamlformat
deleted file mode 100644
index 42e44b125e415b03c85ff79fe6f79b950e3b022f..0000000000000000000000000000000000000000
--- a/proofs/qfo/.ocamlformat
+++ /dev/null
@@ -1,5 +0,0 @@
-break-separators=before
-break-sequences=false
-break-struct=natural
-module-item-spacing=compact
-
diff --git a/proofs/qfo/Makefile b/proofs/qfo/Makefile
deleted file mode 100644
index af6b6f01a10a63c1482c746e140275b622f8ffd1..0000000000000000000000000000000000000000
--- a/proofs/qfo/Makefile
+++ /dev/null
@@ -1,32 +0,0 @@
-PREFIX ?= /usr/local
-
-_EXE = _build/default/bin/main.exe
-
-all: psnj-qfo psnj-qfo.1
-
-${_EXE}:
- @opam exec -- dune build
-
-psnj-qfo: ${_EXE}
- @ln -sf ${_EXE} $@
-
-psnj-qfo.1: psnj-qfo
- @./psnj-qfo --help=groff > $@
-
-install: psnj-qfo psnj-qfo.1
- cp -Lf psnj-qfo ${PREFIX}/bin/
- cp -Lf psnj-qfo.1 ${PREFIX}/man/man1/
-
-uninstall:
- rm -f ${PREFIX}/bin/psnj-qfo
- rm -f ${PREFIX}/man/man1/psnj-qfo.1
-
-clean:
- rm -f psnj-qfo psnj-qfo.1
- opam exec -- dune clean
-
-tests:
- @opam exec -- dune runtest
- @echo 'Success'
-
-.PHONY: install uninstall clean tests
diff --git a/proofs/qfo/bin/dune b/proofs/qfo/bin/dune
deleted file mode 100644
index 7cef94817a1755dd9a88f62fc16e20275a02cafb..0000000000000000000000000000000000000000
--- a/proofs/qfo/bin/dune
+++ /dev/null
@@ -1,4 +0,0 @@
-(executable
- (public_name psnj-qfo)
- (name main)
- (libraries cmdliner lambdapi.common lambdapi.handle qfo))
diff --git a/proofs/qfo/dune-project b/proofs/qfo/dune-project
deleted file mode 100644
index ee333d85f77e2b6556ced36840c01237bb722e2b..0000000000000000000000000000000000000000
--- a/proofs/qfo/dune-project
+++ /dev/null
@@ -1,11 +0,0 @@
-(lang dune 2.9)
-(name psnj_qfo)
-(cram enable)
-
-(generate_opam_files true)
-(maintainers "dedukti-dev@inria.fr")
-
-(package
- (name psnj_qfo)
- (synopsis "Transform PVS-Cert encoded lambdapi to solver friendly encodings")
- (depends cmdliner yojson lambdapi))
diff --git a/proofs/qfo/psnj_qfo.opam b/proofs/qfo/psnj_qfo.opam
deleted file mode 100644
index 9e3543700b277f08ddb5af3dc9609786300c6a79..0000000000000000000000000000000000000000
--- a/proofs/qfo/psnj_qfo.opam
+++ /dev/null
@@ -1,27 +0,0 @@
-# This file is generated by dune, edit dune-project instead
-opam-version: "2.0"
-synopsis: "Transform PVS-Cert encoded lambdapi to solver friendly encodings"
-maintainer: ["dedukti-dev@inria.fr"]
-depends: [
- "dune" {>= "2.9"}
- "cmdliner"
- "yojson"
- "lambdapi"
- "odoc" {with-doc}
-]
-build: [
- ["dune" "subst"] {dev}
- [
- "dune"
- "build"
- "-p"
- name
- "-j"
- jobs
- "--promote-install-files=false"
- "@install"
- "@runtest" {with-test}
- "@doc" {with-doc}
- ]
- ["dune" "install" "-p" name "--create-install-files" name]
-]
diff --git a/proofs/qfo/test/dune b/proofs/qfo/test/dune
deleted file mode 100644
index dc6f72f318b6f391d732e1a1d71a9298df040364..0000000000000000000000000000000000000000
--- a/proofs/qfo/test/dune
+++ /dev/null
@@ -1,15 +0,0 @@
-(test
- (name lpvs))
-
-(cram
- (deps
- lambdapi.pkg
- encoding/lhol.lp
- encoding/pvs_cert.lp
- encoding/propositional_connectives.lp
- encoding/pvs_connectives.lp
- encoding/cpl.lp
- qfo.json
- false.lp
- spec/withsymb.lp
- withsymb_thms.lp))
diff --git a/proofs/qfo/test/lpvs.ml b/proofs/qfo/test/lpvs.ml
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000