uppercase variables

lib/toCert.ml

@@ -198,9 +198,7 @@ let rec tptp_of (vm : Tt.t B.var CVMap.t) (t : term) : Tt.t =
       let b = B.bind_var x (Tt.lift b) in
       cons (B.unbox b)
   (* Generic transformations. *)
-  | Symbol (_, s) ->
-      let x = B.new_var Tt.mkfree s in
-      Tt.Var x
+  | Symbol (_, s) -> Id s
   | Var x -> Tt.Var (CVMap.find x vm)
   | Appl (t, u) -> Tt.App (tptp_of vm t, tptp_of vm u)
   | Lambda (_, b) ->

lib/tptp.ml

+(* TPTP abstract syntax tree and printer. *)
 module B = Bindlib
 
 module Term = struct
   type t =
     | True
     | False
+    | Id of string
     | Var of t B.var
     | App of t * t
     | Not of t
@@ -16,6 +18,7 @@ module Term = struct
     | Lam of (t, t) B.binder
 
   let _Var = B.box_var
+  let _Id s =  B.box (Id s)
   let _App = B.box_apply2 (fun t u -> App (t, u))
   let _Not = B.box_apply (fun t -> Not t)
   let _And = B.box_apply2 (fun t u -> And (t, u))
@@ -35,6 +38,7 @@ module Term = struct
     match t with
     | True -> _True
     | False -> _False
+    | Id s -> _Id s
     | Var x -> _Var x
     | App (t, u) -> _App (l t) (l u)
     | Not t -> _Not (l t)
@@ -46,7 +50,18 @@ module Term = struct
     | Ex b -> lift_bder _Ex b
     | Lam b -> lift_bder _Lam b
 
-  let pp_var ppf (x : t B.var) : unit = Format.fprintf ppf "%s" (B.name_of x)
+  (** [pp_var ppf x] prints variable [x] to formatter [ppf]. Variables
+      are uppercased in TPTP. *)
+  let pp_var ppf (x : t B.var) : unit = 
+    Format.fprintf ppf "%s" (String.capitalize_ascii (B.name_of x))
+
+  (** [pp_id ppf s] prints identifier [s] to formatter [ppf]. Identifiers
+      are lowercased in TPTP. *)
+  let pp_id ppf (s: string): unit =
+    Format.fprintf ppf "%s" (String.lowercase_ascii s)
+
+(* TODO handle name clash if [p] and [P] are both different vars (or
+   different symbols) in some PVS-Cert term. *)
 
   let rec pp (wrap : bool) (ppf : Format.formatter) (t : t) : unit =
     let open Format in
@@ -55,6 +70,7 @@ module Term = struct
     match t with
     | True -> out "$true"
     | False -> out "$false"
+    | Id s -> pp_id ppf s
     | Var x -> pp_var ppf x
     | App (t, u) -> out (wrap "@[%a@ %a@]") (pp false) t (pp true) u
     | Not t -> out (wrap "@[~@ %a@]") (pp false) t

test/lpvs.t

   $ lpvs --lib-root encoding/ false.lp
   symbol false: ∀ prop (\p: prop. p);
   symbol true: ∀ prop (\p: prop. ⇒ p (\_: p. p));
-  fof(false, ! [p] : p).
-  fof(true, ! [p] : p => p).
+  fof(false, ! [P] : P).
+  fof(true, ! [P] : P => P).