varp

(in-package "SATLINK")

(include-book "std/util/define" :dir :system)

(include-book "std/basic/defs" :dir :system)

(include-book "std/basic/arith-equivs" :dir :system)

(include-book "centaur/fty/fixequiv" :dir :system)

(set-tau-auto-mode nil)

(local (add-default-post-define-hook :fix))

(define varp
  (x)
  :parents (cnf)
  :short "Representation of a Boolean variable."
  :long "<p>A variable is now represented as just a natural number, and the
abstract data type wrapper described below is no longer used (we found it too
hard to reason about).  We're preserving the documentation below for reference,
but it's no longer true.</p>

<p>Think of a <b>VARIABLE</b> as an abstract data type that represents
a Boolean variable.  A variable has an <i>index</i> that can be used to
distinguish it from other variables.  The interface for working with variables
is simply:</p>

<dl>
<dt>@(call varp) &rarr; @('bool')</dt>
<dd>Recognize valid identifiers.</dd>

<dt>@('(make-var index)') &rarr; @('id')</dt>
<dd>Construct an identifier with the given given a natural number index.</dd>

<dt>@('(var->index id)') &rarr; @('index')</dt>
<dd>Get the index from an identifier.</dd>
</dl>

<p>In the implementation, variables are nothing more than natural numbers.
That is, @(see varp) is just @(see natp), while @('make-var') and
@('var->index') are logically just @(see nfix) and in the execution are the
identity.</p>

<p>Why, then, bother with a variable type at all?  We use (for efficiency)
integer encodings of related data types like variables and literals. Treating
these as separate types helps us avoid confusing them for one another when we
write programs.</p>

<p>A very nice presentation of this idea is found in <a
href='http://blog.ezyang.com/2010/08/type-kata-newtypes/'>Type Kata:
Distinguishing different data with the same underlying representation</a>, a
blog post by Edward Z. Yang.</p>"
  (natp x)
  :returns (bool booleanp :rule-classes :tau-system)
  ///
  (defthm varp-compound-recognizer
    (equal (varp x)
      (natp x))
    :rule-classes :compound-recognizer))

(local (in-theory (enable varp)))

(defmacro var-fix
  (x)
  `(nfix ,SATLINK::X))

(add-macro-alias var-fix nfix)

(defmacro var-equiv
  (x y)
  `(nat-equiv ,SATLINK::X ,SATLINK::Y))

(add-macro-alias var-equiv
  nat-equiv)

(deffixtype var
  :pred varp
  :fix var-fix
  :equiv var-equiv)

(defsection varp-reasoning
  :parents (varp)
  :short "Basic rules for reasoning about identifiers.")