vampire-sys 0.5.2

Low-level FFI bindings to the Vampire theorem prover (use the 'vampire' crate instead)
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120

/*
 * This file is part of the source code of the software program
 * Vampire. It is protected by applicable
 * copyright laws.
 *
 * This source code is distributed under the licence found here
 * https://vprover.github.io/license.html
 * and in the source directory
 */

#include "Shell/Options.hpp"
#include "Kernel/HOL/HOL.hpp"
#include "Test/UnitTesting.hpp"
#include "Test/HOLUtils.hpp"

#include <map>

constexpr auto RAW = Options::HPrinting::RAW;
constexpr auto DB_INDICES = Options::HPrinting::DB_INDICES;
constexpr auto PRETTY = Options::HPrinting::PRETTY;
constexpr auto TPTP = Options::HPrinting::TPTP;

using namespace Test::HOL;

void runTest(TermList term, const std::map<Options::HPrinting, std::string>& reps) {
  for (const auto& [printOpt, expected] : reps)
    ASS_EQ(termListToString(term, printOpt), expected)
}

HOL_TEST_FUN(hol_print_1) {
  const auto x0F = x(0, Defs::instance()->fSrt);
  const auto x1F = x(1, Defs::instance()->fSrt);

  runTest(
    lam({x0F, x(1)}, x(1)),
    { {RAW,        "(^[X0 : (srt > srt), X1 : srt] : (X1))"},
      {DB_INDICES, "(^[X0 : (srt > srt), X1 : srt] : (X1))"},
      {PRETTY,     "(λX0 : (srt → srt), X1 : srt : (X1))"},
      {TPTP,       "(^[X0 : (srt > srt), X1 : srt] : (X1))"} }
  );
  
  runTest(
    lam({x0F, x(1)}, app(x0F, x(1))),
    { {RAW,        "(^[X0 : (srt > srt), X1 : srt] : (vAPP(srt,srt,X0,X1)))"},
      {DB_INDICES, "(^[X0 : (srt > srt), X1 : srt] : ((X0 @ X1)))"},
      {PRETTY,     "(λX0 : (srt → srt), X1 : srt : ((X0 X1)))"},
      {TPTP,       "(^[X0 : (srt > srt), X1 : srt] : ((X0 @ X1)))"} }
  );

  runTest(
    app(D.f, x(1)),
    { {RAW,        "vAPP(srt,srt,f,X1)"},
      {DB_INDICES, "(f @ X1)"},
      {PRETTY,     "(f X1)"},
      {TPTP,       "(f @ X1)"} }
  );

  runTest(
    lam(x(1), app(D.f, x(1))),
    { {RAW,        "(^[X1 : srt] : (vAPP(srt,srt,f,X1)))"},
      {DB_INDICES, "(^[X1 : srt] : ((f @ X1)))"},
      {PRETTY,     "(λX1 : srt : ((f X1)))"},
      {TPTP,       "(^[X1 : srt] : ((f @ X1)))"} }
  );

  runTest(
    lam(x1F, lam(x(1), x(1))),
    { {RAW,        "(^[X1 : (srt > srt)] : ((^[X1 : srt] : (X1))))" }, 
      {DB_INDICES, "(^[X1 : (srt > srt)] : ((^[X1 : srt] : (X1))))" }, 
      {PRETTY,     "(λX1 : (srt → srt) : ((λX1 : srt : (X1))))" }, 
      {TPTP,       "(^[X1 : (srt > srt)] : ((^[X1 : srt] : (X1))))" } }
  );
}

HOL_TEST_FUN(hol_print_2) {
  using HOL::convert::toNameless;

  const auto x0F = x(0, Defs::instance()->fSrt);
  const auto x1F = x(1, Defs::instance()->fSrt);

  runTest(
    toNameless(lam({x0F, x(1)}, x(1))),
    { {RAW,        "vLAM(srt > srt,srt > srt,vLAM(srt,srt,db0(srt)))" },
      {DB_INDICES, "(^db0 : srt > srt. ((^db1 : srt. (db0_0))))" },
      {PRETTY,     "(λy0 : srt → srt. (λy1 : srt. y1))" },
      {TPTP,       "(^[Y0 : srt > srt]: ((^[Y1 : srt]: (Y1))))" } }
  );

  runTest(
    toNameless(lam({x0F, x(1)}, app(x0F, x(1)))),
    { {RAW,        "vLAM(srt > srt,srt > srt,vLAM(srt,srt,vAPP(srt,srt,db1(srt > srt),db0(srt))))" },
      {DB_INDICES, "(^db0 : srt > srt. ((^db1 : srt. (db1_1 @ db0_0))))" },
      {PRETTY,     "(λy0 : srt → srt. (λy1 : srt. (y0 y1)))" },
      {TPTP,       "(^[Y0 : srt > srt]: ((^[Y1 : srt]: (Y0 @ Y1))))" } }
  );

  runTest(
    toNameless(app(D.f, x(1))),
    { {RAW,        "vAPP(srt,srt,f,X1)"},
      {DB_INDICES, "(f @ X1)"},
      {PRETTY,     "(f X1)"},
      {TPTP,       "(f @ X1)"} }
  );

  runTest(
    toNameless(lam(x(1), app(D.f, x(1)))),
    { {RAW,        "vLAM(srt,srt,vAPP(srt,srt,f,db0(srt)))"},
      {DB_INDICES, "(^db0 : srt. (f @ db0_0))"},
      {PRETTY,     "(λy0 : srt. (f y0))"},
      {TPTP,       "(^[Y0 : srt]: (f @ Y0))"} }
  );

  runTest(
    toNameless(lam(x1F, lam(x(1), x(1)))),
    { {RAW,        "vLAM(srt > srt,srt > srt,vLAM(srt,srt,db0(srt)))" },
      {DB_INDICES, "(^db0 : srt > srt. ((^db1 : srt. (db0_0))))" },
      {PRETTY,     "(λy0 : srt → srt. (λy1 : srt. y1))" },
      {TPTP,       "(^[Y0 : srt > srt]: ((^[Y1 : srt]: (Y1))))" }}
  );
}