demos/logic3.h

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //  This file is generated automatically using Prop (version 2.3.6),
   3 //  last updated on Nov 2, 1999.
   4 //  The original source file is "logic3.ph".
   5 ///////////////////////////////////////////////////////////////////////////////
   6
   7 #define PROP_REWRITING_USED
   8 #define PROP_PRINTER_USED
   9 #define PROP_QUARK_USED
  10 #include <propdefs.h>
  11 ///////////////////////////////////////////////////////////////////////////////
  12 //  Quark literals
  13 ///////////////////////////////////////////////////////////////////////////////
  14 static const Quark _l_o_g_i_c_3co_h_Q3("->");
  15 static const Quark _l_o_g_i_c_3co_h_Q4("xor");
  16 static const Quark _l_o_g_i_c_3co_h_Q1("and");
  17 static const Quark _l_o_g_i_c_3co_h_Q2("or");
  18 static const Quark _l_o_g_i_c_3co_h_Q5("<->");
  19 #line 1 "logic3.ph"
  20 #ifndef logic3_demo_h
  21 #define logic3_demo_h
  22
  23 #include <stdlib.h>
  24 #include <AD/strings/quark.h>
  25
  26 #line 7 "logic3.ph"
  27 #line 20 "logic3.ph"
  28 ///////////////////////////////////////////////////////////////////////////////
  29 //
  30 // Forward class definition for Wff
  31 //
  32 ///////////////////////////////////////////////////////////////////////////////
  33 #ifndef datatype_Wff_defined
  34 #define datatype_Wff_defined
  35    class a_Wff;
  36    typedef a_Wff * Wff;
  37 #endif
  38
  39 #  define True (Wff)0
  40 #  define False (Wff)1
  41
  42 ///////////////////////////////////////////////////////////////////////////////
  43 //
  44 // Base class for datatype Wff
  45 //
  46 ///////////////////////////////////////////////////////////////////////////////
  47 class a_Wff : public TermObj {
  48 public:
  49    enum Tag_Wff {
  50       tag_Var = 0, tag_Op = 1, tag_Not = 2
  51    };
  52
  53 public:
  54    const Tag_Wff tag__; // variant tag
  55 protected:
  56    inline a_Wff(Tag_Wff t__) : tag__(t__) {}
  57 public:
  58 };
  59 inline int boxed(const a_Wff * x) { return (unsigned long)x >= 2; }
  60 inline int untag(const a_Wff * x) { return boxed(x) ? x->tag__ + 2 : (int)x; }
  61 ///////////////////////////////////////////////////////////////////////////////
  62 //
  63 //  Pretty printing methods for Wff
  64 //
  65 ///////////////////////////////////////////////////////////////////////////////
  66 class PrettyOStream;
  67 extern ostream& operator<<(ostream&, Wff);
  68 extern PrettyOStream& operator<<(PrettyOStream&, Wff);
  69 ///////////////////////////////////////////////////////////////////////////////
  70 //
  71 // Class for datatype constructor Wff::Var
  72 //
  73 ///////////////////////////////////////////////////////////////////////////////
  74 class Wff_Var : public a_Wff {
  75 public:
  76 #line 10 "logic3.ph"
  77    Quark Var;
  78    inline Wff_Var (Quark const & x_Var)
  79     : a_Wff(tag_Var), Var(x_Var)
  80    {
  81    }
  82 };
  83
  84 ///////////////////////////////////////////////////////////////////////////////
  85 //
  86 // Class for datatype constructor Wff::Op
  87 //
  88 ///////////////////////////////////////////////////////////////////////////////
  89 class Wff_Op : public a_Wff {
  90 public:
  91 #line 10 "logic3.ph"
  92    Quark _1; Wff _2; Wff _3;
  93    inline Wff_Op (Quark const & x_1, Wff x_2, Wff x_3)
  94     : a_Wff(tag_Op), _1(x_1), _2(x_2), _3(x_3)
  95    {
  96    }
  97 };
  98
  99 ///////////////////////////////////////////////////////////////////////////////
 100 //
 101 // Class for datatype constructor Wff::Not
 102 //
 103 ///////////////////////////////////////////////////////////////////////////////
 104 class Wff_Not : public a_Wff {
 105 public:
 106 #line 11 "logic3.ph"
 107    Wff Not;
 108    inline Wff_Not (Wff x_Not)
 109     : a_Wff(tag_Not), Not(x_Not)
 110    {
 111    }
 112 };
 113
 114 ///////////////////////////////////////////////////////////////////////////////
 115 //
 116 // Datatype constructor functions for Wff
 117 //
 118 ///////////////////////////////////////////////////////////////////////////////
 119 inline a_Wff * Var (Quark const & x_Var)
 120 {
 121    return new Wff_Var (x_Var);
 122 }
 123 inline a_Wff * Op (Quark const & x_1, Wff x_2, Wff x_3)
 124 {
 125    return new Wff_Op (x_1, x_2, x_3);
 126 }
 127 inline a_Wff * Not (Wff x_Not)
 128 {
 129    return new Wff_Not (x_Not);
 130 }
 131 ///////////////////////////////////////////////////////////////////////////////
 132 //
 133 // Downcasting functions for Wff
 134 //
 135 ///////////////////////////////////////////////////////////////////////////////
 136 inline Wff_Var * _Var(const a_Wff * _x_) { return (Wff_Var *)_x_; }
 137 inline Wff_Op * _Op(const a_Wff * _x_) { return (Wff_Op *)_x_; }
 138 inline Wff_Not * _Not(const a_Wff * _x_) { return (Wff_Not *)_x_; }
 139
 140 ///////////////////////////////////////////////////////////////////////////////
 141 // Definition of law And
 142 ///////////////////////////////////////////////////////////////////////////////
 143 #line 14 "logic3.ph"
 144 inline Wff And(Wff a, Wff b)
 145 { return Op(_l_o_g_i_c_3co_h_Q1,a,b); }
 146
 147 ///////////////////////////////////////////////////////////////////////////////
 148 // Definition of law Or
 149 ///////////////////////////////////////////////////////////////////////////////
 150 #line 16 "logic3.ph"
 151 inline Wff Or(Wff a, Wff b)
 152 { return Op(_l_o_g_i_c_3co_h_Q2,a,b); }
 153
 154 ///////////////////////////////////////////////////////////////////////////////
 155 // Definition of law Implies
 156 ///////////////////////////////////////////////////////////////////////////////
 157 #line 17 "logic3.ph"
 158 inline Wff Implies(Wff a, Wff b)
 159 { return Op(_l_o_g_i_c_3co_h_Q3,a,b); }
 160
 161 ///////////////////////////////////////////////////////////////////////////////
 162 // Definition of law Xor
 163 ///////////////////////////////////////////////////////////////////////////////
 164 #line 18 "logic3.ph"
 165 inline Wff Xor(Wff a, Wff b)
 166 { return Op(_l_o_g_i_c_3co_h_Q4,a,b); }
 167
 168 ///////////////////////////////////////////////////////////////////////////////
 169 // Definition of law Equiv
 170 ///////////////////////////////////////////////////////////////////////////////
 171 #line 19 "logic3.ph"
 172 inline Wff Equiv(Wff a, Wff b)
 173 { return Op(_l_o_g_i_c_3co_h_Q5,a,b); }
 174
 175 #line 20 "logic3.ph"
 176 #line 20 "logic3.ph"
 177
 178
 179 #endif
 180 #line 23 "logic3.ph"
 181 /*
 182 ------------------------------- Statistics -------------------------------
 183 Merge matching rules         = yes
 184 Number of DFA nodes merged   = 0
 185 Number of ifs generated      = 0
 186 Number of switches generated = 0
 187 Number of labels             = 0
 188 Number of gotos              = 0
 189 Adaptive matching            = disabled
 190 Fast string matching         = disabled
 191 Inline downcasts             = disabled
 192 --------------------------------------------------------------------------
 193 */