Use lambdapi packages in qfo

proofs/pipeline/examples/encoding/cpl.lp

 // Constructive propositional calculus
 // TODO: define the connectives
-require open qfo.lhol;
+require open qfo.encoding.lhol;
 
 constant symbol top: Prop;
 constant symbol bot: Prop;

proofs/pipeline/examples/encoding/propositional_connectives.lp

 // Klassische propositional logic
 // TODO: define connectives using constructive ones
-require open qfo.lhol;
-require qfo.cpl as C;
+require open qfo.encoding.lhol;
+require qfo.encoding.cpl as C;
 
 constant symbol top: Prop;
 constant symbol bot: Prop;
@@ -12,9 +12,13 @@ constant symbol not: Prop → Prop;
 constant symbol ex: Set → (Set → Prop) → Prop;
 constant symbol all: Set → (Set → Prop) → Prop;
 
+//builtin "T" ≔ El;
+//builtin "P" ≔ Prf;
 builtin "imp" ≔ imp;
 builtin "bot" ≔ bot;
 builtin "top" ≔ top;
 builtin "and" ≔ conj;
 builtin "or" ≔ disj;
 builtin "not" ≔ not;
+
+opaque symbol ok : Prf (∀ {prop} (λ (x: El prop), imp x x)) ≔ begin assume x; why3; end;

proofs/pipeline/examples/encoding/pvs_cert.lp

 // PVS-Cert
-require open qfo.lhol;
+require open qfo.encoding.lhol;
 
 constant symbol psub {x: Set}: (El x → Prop) → Set;
 protected symbol pair': Π(t: Set) (p: El t → Prop), El t → El (psub p);

proofs/pipeline/examples/encoding/pvs_connectives.lp

 // Definition based on implication
-require open qfo.lhol;
+require open qfo.encoding.lhol;
 
 symbol false ≔ ∀ {prop} (λ x: El prop, x);
 symbol true ≔ false ⇒ (λ _: Prf false, false);

proofs/pipeline/examples/lambdapi.pkg

+root_path = qfo
+package_name = qfo

proofs/pipeline/examples/run.expected

-symbol hello!1 : @Prf (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (imp spec.main.P (imp spec.main.Q (conj spec.main.P spec.main.Q))))) ≔
+symbol hello!1 : @Prf (@imp (disj (not qfo.spec.main.P) (disj (not qfo.spec.main.Q) (conj qfo.spec.main.P qfo.spec.main.Q))) (@imp (disj (not qfo.spec.main.P) (disj (not qfo.spec.main.Q) (conj qfo.spec.main.P qfo.spec.main.Q))) (imp qfo.spec.main.P (imp qfo.spec.main.Q (conj qfo.spec.main.P qfo.spec.main.Q))))) ≔
 begin
   why3;
 end;
-symbol hello!2 : @Prf (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (imp spec.main.P (imp spec.main.Q (conj spec.main.P spec.main.Q))))) ≔
+symbol hello!2 : @Prf (@imp (disj (not qfo.spec.main.P) (disj (not qfo.spec.main.Q) (conj qfo.spec.main.P qfo.spec.main.Q))) (@imp (disj (not qfo.spec.main.P) (disj (not qfo.spec.main.Q) (conj qfo.spec.main.P qfo.spec.main.Q))) (imp qfo.spec.main.P (imp qfo.spec.main.Q (conj qfo.spec.main.P qfo.spec.main.Q))))) ≔
 begin
   why3;
 end;
-symbol hello!3 : @Prf (@imp (disj spec.main.P (disj (not spec.main.P) (not spec.main.Q))) (@imp (disj spec.main.Q (disj (not spec.main.P) (not spec.main.Q))) (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))))) ≔
+symbol hello!3 : @Prf (@imp (disj qfo.spec.main.P (disj (not qfo.spec.main.P) (not qfo.spec.main.Q))) (@imp (disj qfo.spec.main.Q (disj (not qfo.spec.main.P) (not qfo.spec.main.Q))) (disj (not qfo.spec.main.P) (disj (not qfo.spec.main.Q) (conj qfo.spec.main.P qfo.spec.main.Q))))) ≔
 begin
   why3;
 end;
-symbol hello!4 : @Prf (@imp (disj spec.main.P (disj (not spec.main.P) (not spec.main.Q))) (@imp (disj spec.main.Q (disj (not spec.main.P) (not spec.main.Q))) (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))))) ≔
+symbol hello!4 : @Prf (@imp (disj qfo.spec.main.P (disj (not qfo.spec.main.P) (not qfo.spec.main.Q))) (@imp (disj qfo.spec.main.Q (disj (not qfo.spec.main.P) (not qfo.spec.main.Q))) (disj (not qfo.spec.main.P) (disj (not qfo.spec.main.Q) (conj qfo.spec.main.P qfo.spec.main.Q))))) ≔
 begin
   why3;
 end;
-symbol hello!5 : @Prf (disj spec.main.P (disj (not spec.main.P) (not spec.main.Q))) ≔
+symbol hello!5 : @Prf (disj qfo.spec.main.P (disj (not qfo.spec.main.P) (not qfo.spec.main.Q))) ≔
 begin
   why3;
 end;
-symbol hello!6 : @Prf (disj spec.main.Q (disj (not spec.main.P) (not spec.main.Q))) ≔
+symbol hello!6 : @Prf (disj qfo.spec.main.Q (disj (not qfo.spec.main.P) (not qfo.spec.main.Q))) ≔
 begin
   why3;
 end;
\ No newline at end of file

proofs/pipeline/examples/run.sh

 #!/bin/sh
 set -euf
-opam exec -- psnj-pipe --qfo=encoding/qfo.json hello.log encoding/ spec/
+opam exec -- psnj-pipe --qfo=encoding/qfo.json hello.log

proofs/pipeline/examples/spec/main.lp

-require open qfo.lhol qfo.pvs_cert;
+require open qfo.encoding.lhol qfo.encoding.pvs_cert;
 symbol P: Prop;
 symbol Q: Prop;

proofs/pipeline/pipe.ml

 open Feather
 open Feather.Infix
 
-let process proveit src qfo_conf encoding specification =
+let process proveit src qfo_conf =
   (* Define commands *)
   let proveit =
     Option.map (fun p -> process p [ "--traces"; "-l"; src ]) proveit
@@ -19,12 +19,8 @@ let process proveit src qfo_conf encoding specification =
     process "psnj-qfo"
       [
         qfo_conf;
-        "--map-dir";
-        "qfo:" ^ encoding;
-        "--map-dir";
-        "spec:" ^ specification;
         "-e";
-        "require open spec.main;";
+        "require open qfo.spec.main;";
       ]
   and chainprops depfile = process "psnj-chainprops" [ depfile ]
   and appaxiom = process "psnj-appaxiom" [ "-a"; "Prf" ] 
@@ -59,16 +55,6 @@ let qfo_conf =
   let doc = "Configuration for QFO" in
   Arg.(value & opt string "qfo.json" & info [ "qfo" ] ~doc)
 
-let encoding =
-  let doc =
-    "Use encoding $(docv) to translate files from full blown PVS-Cert to STT."
-  in
-  Arg.(required & pos 1 (some dir) None & info [] ~doc ~docv:"ENC")
-
-let specification =
-  let doc = "Open module $(docv).main to translate propositions" in
-  Arg.(required & pos 2 (some dir) None & info [] ~doc ~docv:"MOD")
-
 let proveit =
   let doc = "Execute $(docv) to obtain a log file with proof information" in
   Arg.(value & opt (some string) None & info [ "proveit" ] ~doc ~docv:"FILE")
@@ -77,7 +63,7 @@ let cmd =
   let exits = Term.default_exits in
   let doc = "Pipeline for personoj" in
   let man = [] in
-  ( Term.(const process $ proveit $ src $ qfo_conf $ encoding $ specification),
+  ( Term.(const process $ proveit $ src $ qfo_conf),
     Term.(info "psnj-pipe" ~exits ~doc ~man) )
 
 let () = Term.(exit @@ eval cmd)

proofs/qfo/bin/main.ml

@@ -86,7 +86,8 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
       let ss = new_sig_state mp in
       let ast =
         Parser.parse_string "<qfo>"
-          "require open qfo.lhol qfo.pvs_cert qfo.pvs_connectives;"
+          "require open qfo.encoding.lhol qfo.encoding.pvs_cert \
+           qfo.encoding.pvs_connectives;"
       in
       compile_ast ss ast
     with Error.Fatal (pos, msg) ->
@@ -102,7 +103,7 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
            let ss = new_sig_state mp in
            let ast =
              Parser.parse_string "<qfo>"
-               "require open qfo.lhol qfo.pvs_connectives;"
+               "require open qfo.encoding.lhol qfo.encoding.pvs_connectives;"
            in
            compile_ast ss ast
          with Error.Fatal (p, m) ->
@@ -116,7 +117,7 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
     let ss = new_sig_state mp in
     let ast =
       Parser.parse_string "<qfo>"
-        "require open qfo.lhol qfo.propositional_connectives;"
+        "require open qfo.encoding.lhol qfo.encoding.propositional_connectives;"
     in
     compile_ast ss ast
   in
@@ -131,7 +132,8 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
       let ss = new_sig_state [ "<qfo>" ] in
       let ast =
         Parser.parse_string "<qfo>"
-          "require open qfo.lhol qfo.pvs_cert qfo.pvs_connectives;"
+          "require open qfo.encoding.lhol qfo.encoding.pvs_cert \
+           qfo.encoding.pvs_connectives;"
       in
       compile_ast ss ast
     with Error.Fatal (p, m) ->
@@ -160,7 +162,8 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
     try
       let ss = new_sig_state [ "<qfo.print>" ] in
       let open_cmd =
-        "require open qfo.lhol qfo.pvs_cert qfo.propositional_connectives;"
+        "require open qfo.encoding.lhol qfo.encoding.pvs_cert \
+         qfo.encoding.propositional_connectives;"
       in
       compile_ast ss (Parser.parse_string "<qfo.print>" open_cmd)
     with Error.Fatal (p, msg) ->
@@ -206,6 +209,11 @@ let cmd =
          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
+        "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
         "To convert files, the program needs identify the symbols of the \
          encoding. The mapping allows to indicate the name of such symbols. \
@@ -238,9 +246,16 @@ let cmd =
          \"pvs_connectives\" and \"propositional_connectives\" define logical \
          connectors: connectors from \"pvs_connectives\" are replaced by \
          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
         "Furthermore, if the standard input uses symbols from some other \
-         module \"mod\", it can be opened using $(b,-e mod)."
+         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
@@ -285,9 +300,6 @@ let cmd =
     ; `P "The program outputs"
     ; `Pre "symbol true: @∀ prop (λ p: El prop, imp p p);"
     ; `S Manpage.s_bugs
-    ; `P
-        "Unlike in lambdapi, because standard input is parsed, the option \
-         $(b,--map-dir) should in general be used."
     ; `P
         "If the input opens some module (using \"open mod\"), then symbols \
          from this module will appear fully qualified."

proofs/qfo/test/encoding/cpl.lp

 // Constructive propositional calculus
 // TODO: define the connectives
-require open qfo.lhol;
+require open qfo.encoding.lhol;
 
 constant symbol top: Prop;
 constant symbol bot: Prop;

proofs/qfo/test/encoding/propositional_connectives.lp

 // Klassische propositional logic
 // TODO: define connectives using constructive ones
-require open qfo.lhol;
-require qfo.cpl as C;
+require open qfo.encoding.lhol;
+require qfo.encoding.cpl as C;
 
 constant symbol top: Prop;
 constant symbol bot: Prop;

proofs/qfo/test/encoding/pvs_cert.lp

 // PVS-Cert
-require open qfo.lhol;
+require open qfo.encoding.lhol;
 
 constant symbol psub {x: Set}: (El x → Prop) → Set;
 protected constant symbol pair': Π(t: Set) (p: El t → Prop), El t → El (psub p);

proofs/qfo/test/encoding/pvs_connectives.lp

 // Definition based on implication
-require open qfo.lhol;
+require open qfo.encoding.lhol;
 
 symbol false ≔ ∀ {prop} (λ x: El prop, x);
 symbol true ≔ false ⇒ (λ _: Prf false, false);

proofs/qfo/test/qfo.t

-  $ psnj-qfo --map-dir=qfo:encoding qfo.json < false.lp
+  $ psnj-qfo qfo.json < false.lp 2>'/dev/null'
   symbol false: @∀ prop (λ p: El prop, p);
   symbol true: @∀ prop (λ p: El prop, imp p p);
 
-  $ echo 'symbol tt: ∀ {prop} (λ p: El prop, p ∧ (λ _, p));' | psnj-qfo --map-dir=qfo:encoding qfo.json
+  $ echo 'symbol tt: ∀ {prop} (λ p: El prop, p ∧ (λ _, p));' | psnj-qfo qfo.json 2>'/dev/null'
   symbol tt: @∀ prop (λ p: El prop, conj p p);
 
-  $ psnj-qfo --map-dir=qfo:encoding --map-dir=spec:spec -e 'require open spec.withsymb;' qfo.json < withsymb_thms.lp
-  symbol trivial: imp spec.withsymb.P spec.withsymb.P;
+  $ psnj-qfo -e 'require open qfo.spec.withsymb;' qfo.json < withsymb_thms.lp 2>'/dev/null'
+  symbol trivial: imp qfo.spec.withsymb.P qfo.spec.withsymb.P;

proofs/qfo/test/spec/withsymb.lp

-require open qfo.lhol;
+require open qfo.encoding.lhol;
 symbol P: Prop;
 symbol trivial: Prf (P ⇒ (λ _: Prf P, P));