prop-src/wam.ph

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //
   3 //  This file describes the internal abstract machine of the
   4 //  constraint compiler, which is based (very) loosely on the Warren
   5 //  Abstract Machine (WAM).   It also describes various other semantic
   6 //  objects used in the analysis of the logic clauses.
   7 //
   8 ///////////////////////////////////////////////////////////////////////////////
   9 #ifndef WAM_definitions_h
  10 #define WAM_definitions_h
  11
  12 #include "basics.ph"
  13
  14 ///////////////////////////////////////////////////////////////////////////////
  15 //
  16 //  Forward type definitions.
  17 //
  18 ///////////////////////////////////////////////////////////////////////////////
  19 datatype Ty      // type expressions
  20      and Cons    // constructor descriptor
  21      and Exp     // expressions
  22      and Stmt    // statements
  23      and Def     // definitions
  24      and Decl    // declarations
  25 ;
  26
  27 ///////////////////////////////////////////////////////////////////////////////
  28 //
  29 //  Kind of variables.  These are characterized as follows, in order
  30 //  of priority:
  31 //  (a) Global variables are variables that occur as argument
  32 //      in a structural pattern.  These may escape the life-time of
  33 //      the clause.
  34 //  (b) Local variables are variables that occur multiple times in a clause
  35 //      (if they don't satisfy condition (a)).
  36 //  (c) Void variables are variables with only one occurrence.  These
  37 //      can be elided since they are always unifiable and never accessed.
  38 //
  39 ///////////////////////////////////////////////////////////////////////////////
  40 datatype VarKind : MEM
  41     = VOIDvar   (Ty)
  42     | LOCALvar  (Ty)
  43     | TEMPvar   (Ty)
  44     | GLOBALvar (Ty)
  45
  46 ///////////////////////////////////////////////////////////////////////////////
  47 //
  48 //  Instantiateness of a clause parameter.
  49 //
  50 ///////////////////////////////////////////////////////////////////////////////
  51 and Instness : MEM
  52     = NOinst                            // unknown
  53     | IDinst     (Id)                   // named instness
  54     | FREEinst   (Ty)                   // free term
  55     | GROUNDinst (Ty)                   // ground term
  56     | BOUNDinst  (Ty,List<Instness>)    // bound term (disjunction)
  57     | APPinst    (Cons,List<Instness>)  // functor application
  58     | FUNinst    (Instness, Instness)   // instness mapping
  59     | VARinst    (Instness)             // instness variable
  60
  61 ///////////////////////////////////////////////////////////////////////////////
  62 //
  63 //  Determinism of a clause.
  64 //
  65 ///////////////////////////////////////////////////////////////////////////////
  66 and Determinism : MEM
  67     = UNKNOWN_DET
  68     | DET                   // deterministic
  69     | SEMI_DET              // may succeed or fail once
  70     | MULTI_DET             // may succeed many times but only fail once
  71     | NON_DET               // non-deterministic
  72     | FAIL_DET              // always fail
  73     | ERROR_DET             // neither fail nor succeed
  74     | VAR_DET (Determinism) // determinstic variable
  75
  76 ///////////////////////////////////////////////////////////////////////////////
  77 //
  78 //  Unification mode
  79 //
  80 ///////////////////////////////////////////////////////////////////////////////
  81 and UnificationMode = READ_MODE | WRITE_MODE
  82
  83 ///////////////////////////////////////////////////////////////////////////////
  84 //
  85 //  The WAM instruction set.
  86 //
  87 //  Notice that our term representation is substantially different that
  88 //  the traditional WAM.  This is mostly due to C++ interoperability
  89 //  constraints (for example, it is not too nice to have tagged integers
  90 //  if the user has to tag/untag them manually).  In general, we make
  91 //  no distinction between structures or constants in the WAM level, since
  92 //  we'll be re-using the pattern matching compiler to perform indexing
  93 //  and semi-unification.  Also notice that terms in Prop are statically
  94 //  typed in the style of ML.
  95 //
  96 ///////////////////////////////////////////////////////////////////////////////
  97 and WAM : MEM =
  98         "get_x"
  99     |   "get_y"
 100     |   "proceed"                    // WAM return
 101     |   "fail"                       // WAM failure
 102     |   "deref"
 103     |   "unify"
 104     |   "unify_variable"
 105     |   "unify_term"         (Ty, Cons)
 106     |   "try"                (Label)
 107     |   "retry"              (Label)
 108     |   "trust"              (Label)
 109     |   "try_me_else"        (Label)
 110     |   "retry_me_else"      (Label)
 111     |   "trust_me_else_fail"
 112     |   "label"              (Label)  // label in the code
 113
 114 ///////////////////////////////////////////////////////////////////////////////
 115 //
 116 //  A program label.
 117 //
 118 ///////////////////////////////////////////////////////////////////////////////
 119 and Label : MEM = LABEL (Id) => _
 120
 121 ///////////////////////////////////////////////////////////////////////////////
 122 //
 123 //  Miscellaneous types
 124 //
 125 ///////////////////////////////////////////////////////////////////////////////
 126 where type WAMs   = List<WAM>    // a list of wam instructions.
 127        and Labels = List<Label>  // a list of labels.
 128 ;
 129
 130 ///////////////////////////////////////////////////////////////////////////////
 131 //
 132 //  Optimization and manipulation of WAM code.
 133 //
 134 ///////////////////////////////////////////////////////////////////////////////
 135 extern WAMs peep_hole (WAMs); // peep hole optimizer.
 136
 137 ///////////////////////////////////////////////////////////////////////////////
 138 //
 139 //  Manipulation routines.
 140 //
 141 ///////////////////////////////////////////////////////////////////////////////
 142 extern Instness    deref (Instness);
 143 extern Determinism deref (Determinism);
 144
 145 ///////////////////////////////////////////////////////////////////////////////
 146 //
 147 //  Pretty printers.
 148 //
 149 ///////////////////////////////////////////////////////////////////////////////
 150 extern std::ostream& operator << (std::ostream&, WAM);
 151 extern std::ostream& operator << (std::ostream&, WAMs);
 152 extern std::ostream& operator << (std::ostream&, Label);
 153 extern std::ostream& operator << (std::ostream&, Labels);
 154 extern std::ostream& operator << (std::ostream&, Instness);
 155 extern std::ostream& operator << (std::ostream&, Determinism);
 156
 157 #endif