diff --git a/proofs/qfo/bin/dune b/proofs/qfo/bin/dune
index 9a1555974fcb534ea0bbb3d0247552a655be64eb..7cef94817a1755dd9a88f62fc16e20275a02cafb 100644
--- a/proofs/qfo/bin/dune
+++ b/proofs/qfo/bin/dune
@@ -1,4 +1,4 @@
(executable
(public_name psnj-qfo)
(name main)
- (libraries cmdliner lambdapi.common lambdapi.handle pvsLp))
+ (libraries cmdliner lambdapi.common lambdapi.handle qfo))
diff --git a/proofs/qfo/bin/main.ml b/proofs/qfo/bin/main.ml
index ae61cdc50fa70fe48ce17bcc99b7a80d188c00e8..b6c156cbcdb3bdf41612b0b576b06f41319c136f 100644
--- a/proofs/qfo/bin/main.ml
+++ b/proofs/qfo/bin/main.ml
@@ -56,7 +56,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 = PvsLp.Mappings.of_file mapfile in
+ let mapping = Qfo.Mappings.of_file mapfile in
let pvs_cert, pvs_connectives, propositional_connectives =
let f s =
try StrMap.find s mapping
@@ -95,23 +95,23 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
print_err pos msg;
exit 1
in
- let module Pcert = (val PvsLp.Encodings.mkpcert pvs_cert pvs_cert_ss) in
+ let ps = Qfo.Encodings.mkpredicate_subtyping pvs_cert pvs_cert_ss in
Console.out 1 "Loaded PVS-Cert encoding";
- let module DepConn =
- (val let pvs_connectives_ss =
- try
- let ss = new_sig_state mp in
- let ast =
- Parser.parse_string "<qfo>"
- "require open qfo.encoding.lhol qfo.encoding.pvs_connectives;"
- in
- compile_ast ss ast
- with Error.Fatal (p, m) ->
- Format.eprintf "Couldn't initalise PVS connectives signature@\n";
- print_err p m;
- exit 2
- in
- PvsLp.Encodings.mkconnectors pvs_connectives pvs_connectives_ss)
+ let pvs_c =
+ let pvs_connectives_ss =
+ try
+ let ss = new_sig_state mp in
+ let ast =
+ Parser.parse_string "<qfo>"
+ "require open qfo.encoding.lhol qfo.encoding.pvs_connectives;"
+ in
+ compile_ast ss ast
+ with Error.Fatal (p, m) ->
+ Format.eprintf "Couldn't initalise PVS connectives signature@\n";
+ print_err p m;
+ exit 2
+ in
+ Qfo.Encodings.mkconnectives pvs_connectives pvs_connectives_ss
in
let prop_calc_ss =
let ss = new_sig_state mp in
@@ -121,11 +121,10 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
in
compile_ast ss ast
in
- let module Propc =
- (val PvsLp.Encodings.mkconnectors propositional_connectives prop_calc_ss)
+ let prop_c =
+ Qfo.Encodings.mkconnectives propositional_connectives prop_calc_ss
in
Console.out 1 "Loaded classical propositional calculus";
- let module Tran = PvsLp.LpCert.PropOfPcert (Pcert) (DepConn) (Propc) in
let qfo_ss =
(* Create a sig state with PVS-Cert and the specification*)
try
@@ -149,11 +148,12 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
in
(* Load propositions from stdin in [qfo_ss] *)
let props = compile_props qfo_ss (Parser.parse stdin) in
- let tr_pp (name, ty) =
+ let transpile_print (name, ty) =
+ let open Qfo.Transpile in
try
- let propty = Tran.f ty in
+ let propty = translate_term ~ps ~prop_c ~pvs_c ty in
Format.printf "@[symbol %s:@ %a;@]@." name Print.pp_term propty
- with Tran.CannotTranslate t ->
+ with CannotTranslate t ->
Format.eprintf "Cannot translate %a@." Print.pp_term t
in
(* Prepare for printing *)
@@ -175,7 +175,7 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
Print.sig_state := printing_ss;
Print.print_implicits := true;
Print.print_domains := true);
- List.iter tr_pp props
+ List.iter transpile_print props
open Cmdliner
@@ -225,13 +225,7 @@ let cmd =
; `P
"where the value associated to \"pvs_cert\" is an object that define \
the following form"
- ; `Pre
- "{ \"Set\": STRING, \"Element\": STRING,\n\
- \ \"Propositions\": STRING, \"Proof\": STRING,\n\
- \ \"forall\": STRING, \"arrow\": STRING, \"implication\": STRING,\n\
- \ \"o\": STRING,\n\
- \ \"subset\": STRING, \"pair\": STRING, \"value\": STRING, \"proof\": \
- STRING }"
+ ; `Pre "{ \"subset\": STRING }"
; `P
"and the values associated to both \"pvs_connectives\" and \
\"propositional_connectives\" must be of the form"
@@ -261,18 +255,7 @@ let cmd =
; `Pre
{|{
"pvs_cert": {
- "Set": "Set",
- "Element": "El",
- "Propositions": "Prop",
- "Proof": "Prf",
- "forall": "∀",
- "arrow": "arrd",
- "implication": "⇒",
- "o": "prop",
- "subset": "psub",
- "pair": "pair",
- "value": "fst",
- "proof": "snd"
+ "subset": "psub"
},
"pvs_connectives": {
"truth": "true",
diff --git a/proofs/qfo/lib/dune b/proofs/qfo/lib/dune
index a36a017e10eee2971b3e00f70b27f30c57aa76ee..c767a7329edef43bcdee9fa9143f9a31af30bc71 100644
--- a/proofs/qfo/lib/dune
+++ b/proofs/qfo/lib/dune
@@ -5,4 +5,4 @@
lambdapi.lplib
lambdapi.parsing
lambdapi.core)
- (name pvsLp))
+ (name qfo))
diff --git a/proofs/qfo/lib/encodings.ml b/proofs/qfo/lib/encodings.ml
index 10756ee01c57fc3758d71c154dd0b60b39eb0ae8..f05ec3cbb8d9871d451bda0451c90ce36192ae8d 100644
--- a/proofs/qfo/lib/encodings.ml
+++ b/proofs/qfo/lib/encodings.ml
@@ -1,12 +1,3 @@
-(** Define several encodings and functions to load them from signature
- states.
-
- An encoding is represented by a module made of symbols. Having these
- symbols is required when we want to create terms in this encoding. To
- destruct on an encoding, having the name is enough. For each fragment
- [F], there is a function [mkf] that takes a signature state and
- extracts the symbol that are part of [F]. *)
-
open Common
open Core
module T = Term
@@ -23,94 +14,44 @@ let fsym (sig_st : Sig_state.t) (sym : string) : T.sym =
type mapping = (string * string) list
-(** Lambda HOL *)
-module type LHOL = sig
- val element : T.sym
- val set : T.sym
- val proof : T.sym
- val forall : T.sym
- val propositions : T.sym
- val o : T.sym
- val implication : T.sym
- val arrow : T.sym
-end
-
-let mklhol (map : mapping) (sig_st : Sig_state.t) : (module LHOL) =
- let s (name : string) : T.sym =
- try fsym sig_st (List.assoc name map)
- with Not_found ->
- failwith (Format.sprintf "Symbol \"%s\" not found in mapping" name)
- in
- (module struct
- let set = s "Set"
- let element = s "Element"
- let propositions = s "Propositions"
- let proof = s "Proof"
- let forall = s "forall"
- let o = s "o"
- let implication = s "implication"
- let arrow = s "arrow"
- end)
-
+type predicate_subtyping = { subset : T.sym }
(** PVS-Cert *)
-module type PREDICATE_SUBTYPING = sig
- val subset : T.sym
- val pair : T.sym
- val value : T.sym
- val proof : T.sym
- val symbols : T.sym list
-end
let mkpredicate_subtyping (map : mapping) (sig_st : Sig_state.t) :
- (module PREDICATE_SUBTYPING) =
+ predicate_subtyping =
let s (name : string) : T.sym =
try fsym sig_st (List.assoc name map)
with Not_found ->
failwith (Format.sprintf "Symbol \"%s\" not found in mapping" name)
in
- (module struct
- let subset = s "subset"
- let pair = s "pair"
- let value = s "value"
- let proof = s "proof"
- let symbols = [ subset; pair; value; proof ]
- end)
-
-module type PCERT = sig
- include LHOL include PREDICATE_SUBTYPING
-end
-
-let mkpcert (pcertmap : mapping) (sig_st : Sig_state.t) : (module PCERT) =
- let (module Lhol) = mklhol pcertmap sig_st
- and (module Prst) = mkpredicate_subtyping pcertmap sig_st in
- (module struct include Lhol include Prst end)
-
+ { 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
+}
(** Logical connectives *)
-module type CONNECTORS = sig
- val truth : T.sym
- val falsity : T.sym
- val implication : T.sym
- val negation : T.sym
- val conjunction : T.sym
- val disjunction : T.sym
- val existential : T.sym
- val universal : T.sym
-end
-let mkconnectors (map : (string * string) list) (sig_st : Sig_state.t) :
- (module CONNECTORS) =
+let mkconnectives (map : (string * string) list) (sig_st : Sig_state.t) :
+ connectives =
let s (name : string) : T.sym =
try fsym sig_st (List.assoc name map)
with Not_found ->
failwith (Format.sprintf "Symbol \"%s\" not found in mapping" name)
in
- (module struct
- let truth = s "truth"
- let falsity = s "falsity"
- let negation = s "negation"
- let implication = s "implication"
- let conjunction = s "conjunction"
- let disjunction = s "disjunction"
- let existential = s "existential"
- let universal = s "universal"
- end)
+ {
+ 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/qfo/lib/encodings.mli
new file mode 100644
index 0000000000000000000000000000000000000000..5598bbdfe944e3e0ea631a830146c1ad64403c1f
--- /dev/null
+++ b/proofs/qfo/lib/encodings.mli
@@ -0,0 +1,33 @@
+(** Define several encodings and functions to load them from signature
+ states.
+
+ An encoding is represented by a record of symbols. Having these
+ symbols is required when we want to create terms in this encoding. To
+ destruct on an encoding, having the name is enough. For each fragment
+ [F], there is a function [mkf] that takes a signature state and
+ extracts the symbol that are part of [F]. *)
+
+open Core
+
+type mapping = (string * string) list
+(** A mapping [(name,sym)] indicates that record element [name] is to
+ be mapped to symbol [sym] that will be found in a signature.*)
+
+type predicate_subtyping = { subset : Term.sym }
+(** The symbols used to encode predicate subtyping. *)
+
+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
+}
+(** Logical connectives. They may be dependent or non-dependent. *)
+
+val mkconnectives : mapping -> Sig_state.t -> connectives
diff --git a/proofs/qfo/lib/lpCert.ml b/proofs/qfo/lib/transpile.ml
similarity index 58%
rename from proofs/qfo/lib/lpCert.ml
rename to proofs/qfo/lib/transpile.ml
index 7efca934153ab49e4bbb5f4598efe85eb23c3272..932eb6a77d33ee717630abf0e3e1258659620959 100644
--- a/proofs/qfo/lib/lpCert.ml
+++ b/proofs/qfo/lib/transpile.ml
@@ -1,4 +1,4 @@
-(** Manipulating PVS-Cert encoded in Lambdapi. *)
+(** Transpile terms from PVS-Cert to STT. Connectives are also transformed. *)
open Core
module T = Term
@@ -6,37 +6,31 @@ module LibT = LibTerm
module B = Bindlib
module E = Encodings
-(** [PropOfPcert(Pc)(DepConn)(Prop)] takes the encoding of PVS-Cert
- [Pc], the dependent logical connectives [DepConn] and non dependent
- ones [Prop] and provide a translation function from PVS-Cert to kind
- of first order (substitute dependent connectors when they can be,
- remove predicate subtyping). *)
-module PropOfPcert (Pc : E.PCERT) (DepConn : E.CONNECTORS) (Prop : E.CONNECTORS) : sig
- exception CannotTranslate of T.term
+exception CannotTranslate of T.term
+(** Raised when a non translatable symbol is found. *)
- val f : T.term -> T.term
-end = struct
- exception CannotTranslate of T.term
-
- (** Map dependent binary connectives to non dependent ones. *)
+(** [translate_term ~ps ~pvs_c ~prop_c t] translates term [t]. Term
+ [t] may contain symbols from [ps] and [pvs_c]. Connectives from
+ [pvs_c] are translated by connectives of [prop_c]. *)
+let translate_term ~(ps : E.predicate_subtyping) ~(pvs_c : E.connectives)
+ ~(prop_c : E.connectives) (t : T.term) : T.term =
let binary =
[
- (Pc.implication, Prop.implication)
- ; (DepConn.implication, Prop.implication)
- ; (DepConn.conjunction, Prop.conjunction)
- ; (DepConn.disjunction, Prop.disjunction)
+ (pvs_c.implication, prop_c.implication)
+ ; (pvs_c.conjunction, prop_c.conjunction)
+ ; (pvs_c.disjunction, prop_c.disjunction)
]
-
- let rec f (t : T.term) : T.term =
+ in
+ let rec f (t : T.term) =
match T.get_args t with
| (Wild | TRef _ | Meta _ | TEnv _ | Plac _ | Patt _), _ ->
assert false (* should not appear in typechecked terms *)
(* Mapping constants *)
- | Symb i, [] when i == DepConn.truth -> T.mk_Symb Prop.truth
- | Symb i, [] when i == DepConn.falsity -> T.mk_Symb Prop.falsity
+ | Symb i, [] when i == pvs_c.truth -> T.mk_Symb prop_c.truth
+ | Symb i, [] when i == pvs_c.falsity -> T.mk_Symb prop_c.falsity
(* Mapping unary operators *)
- | Symb i, [ e ] when i == DepConn.negation ->
- T.add_args (T.mk_Symb Prop.negation) [ f e ]
+ | Symb i, [ e ] when i == pvs_c.negation ->
+ T.add_args (T.mk_Symb prop_c.negation) [ f e ]
(* Mapping binary operators *)
| Symb i, [ l; r ] when List.(memq i (map fst binary)) ->
let r =
@@ -51,7 +45,7 @@ end = struct
let new_sym = List.assq i binary in
T.add_args (T.mk_Symb new_sym) [ f l; f r ]
(* Mapping quantifiers *)
- | Symb s, _ when List.memq s Pc.symbols ->
+ | Symb s, _ when s == ps.subset ->
Format.eprintf
"PVS-Cert pair, fst and snd cannot be translated to propositional \
logic@.";
@@ -74,4 +68,5 @@ end = struct
| _ -> assert false
in
T.add_args hd args
-end
+ in
+ f t
diff --git a/proofs/qfo/test/qfo.json b/proofs/qfo/test/qfo.json
index 2d3e4c3ecba9fff9c1cb2d767665461e54118259..ba87425e23abccc636ebc5a52e71bf3cbd1aed8f 100644
--- a/proofs/qfo/test/qfo.json
+++ b/proofs/qfo/test/qfo.json
@@ -1,17 +1,6 @@
{
"pvs_cert": {
- "Set": "Set",
- "Element": "El",
- "Propositions": "Prop",
- "Proof": "Prf",
- "forall": "∀",
- "arrow": "arrd",
- "implication": "⇒",
- "o": "prop",
- "subset": "psub",
- "pair": "pair",
- "value": "fst",
- "proof": "snd"
+ "subset": "psub"
},
"pvs_connectives": {
"truth": "true",
diff --git a/proofs/qfo/test/qfo.t b/proofs/qfo/test/qfo.t
index 3c5d63c21a3048f9a0f602a3dcb59da786ee266e..1e69fd2c698f65ff7b33d08bb6be5fd9226bbd98 100644
--- a/proofs/qfo/test/qfo.t
+++ b/proofs/qfo/test/qfo.t
@@ -1,9 +1,12 @@
- $ psnj-qfo qfo.json < false.lp 2>'/dev/null'
+ $ psnj-qfo qfo.json < false.lp
+ Loaded package file from "$TESTCASE_ROOT"
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 qfo.json 2>'/dev/null'
+ $ echo 'symbol tt: ∀ {prop} (λ p: El prop, p ∧ (λ _, p));' | psnj-qfo qfo.json
+ Loaded package file from "$TESTCASE_ROOT"
symbol tt: @∀ prop (λ p: El prop, conj p p);
- $ psnj-qfo -e 'require open qfo.spec.withsymb;' qfo.json < withsymb_thms.lp 2>'/dev/null'
+ $ 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;