• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
      • Gl
      • Witness-cp
      • Ccg
      • Install-not-normalized
      • Rewrite$
      • Removable-runes
      • Efficiency
      • Rewrite-bounds
      • Bash
      • Def-dag-measure
      • Fgl
        • Fgl-rewrite-rules
        • Fgl-function-mode
        • Fgl-object
          • Fgl-object-eval
          • Fgl-object-p
          • G-map
          • G-ite
          • G-cons
          • G-concrete
          • G-apply
          • G-integer
          • Fgl-object-equiv
          • G-boolean
          • G-var
          • Fgl-bitvector
          • Fgl-object-kind
          • Summarize-fgl-object
          • Fgl-object-alist
          • Fgl-objectlist
          • Fgl-object-fix
          • Fgl-object-count
        • Fgl-solving
        • Fgl-handling-if-then-elses
        • Fgl-getting-bits-from-objects
        • Fgl-primitive-and-meta-rules
        • Fgl-interpreter-overview
        • Fgl-counterexamples
        • Fgl-correctness-of-binding-free-variables
        • Fgl-debugging
        • Fgl-testbenches
        • Def-fgl-boolean-constraint
        • Fgl-stack
        • Fgl-rewrite-tracing
        • Def-fgl-param-thm
        • Def-fgl-thm
        • Fgl-fast-alist-support
        • Advanced-equivalence-checking-with-fgl
        • Fgl-array-support
        • Fgl-internals
      • Bdd
      • Remove-hyps
      • Contextual-rewriting
      • Simp
      • Rewrite$-hyps
      • Bash-term-to-dnf
      • Use-trivial-ancestors-check
      • Minimal-runes
      • Clause-processor-tools
      • Fn-is-body
      • Without-subsumption
      • Rewrite-equiv-hint
      • Def-bounds
      • Rewrite$-context
      • Try-gl-concls
      • Hint-utils
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • Fgl

Fgl-object

FGL symbolic object type

This is a sum-of-products (i.e., union) type, introduced by defflexsum.

Members
:g-concrete → g-concrete
FGL-object constructor for constant (quoted) objects.
:g-boolean → g-boolean
FGL object constructor for symbolic Boolean objects.
:g-integer → g-integer
FGL object constructor for symbolic integers, with Boolean functions representing the bits.
:g-ite → g-ite
FGL object constructor for if-then-else objects.
:g-apply → g-apply
FGL object constructor for function calls.
:g-var → g-var
FGL object constructor for free variables.
:g-map → g-map
FGL object constructor for fast alists and arrays.
:g-cons → g-cons
FGL object constructor for conses.

An FGL symbolic object is the representation for symbolic data inside the FGL interpreter. There are several kinds of objects, including concrete objects that simply represent a particular explicit value, bit-level objects that represent some function resulting in a Boolean or bitvector (integer), and termlike objects that represent free variables and calls of arbitrary functions on symbolic objects.

Symbolic objects are evaluated using fgl-object-eval. This takes an environment object of type fgl-env consisting of an alist mapping free variables to their values, for evaluating g-var objects, and a Boolean function environment for evaluating g-boolean and g-integer objects.

The FGL object type is an FTY-style sum-of-products type. That means any of the sum members listed above may be used to construct an object of this type. Functions that access FGL objects must check which kind of object they have been passed. The kind of a FGL object may be accessed using the fgl-object-kind function, but usually it is easier to use the fgl-object-case macro, which we illustrate using the following examples:

;; If x is a g-concrete representing an integer, return its integer-length plus
;; one, else if it's a g-integer return the length of its bitlist, else NIL:
 (fgl-object-case x
    :g-concrete (and (integerp x.val) (+ 1 (integer-length x.val)))
    :g-integer (len x.bits)
    :otherwise nil)

;; Check whether x can be syntactically determined to be always non-NIL.
 (defun gobj-syntactically-nonnil (x)
   (fgl-object-case x
      :g-concrete (and x.val t)
      :g-integer  t
      :g-boolean  (eq x.bool t)
      :g-ite      (if (gobj-syntactically-nonnil x.test)
                      (gobj-syntactically-nonnil x.then)
                    (and (gobj-syntactically-nonnil x.then)
                         (gobj-syntactically-nonnil x.else)))
      :g-apply    nil
      :g-var      nil
      :g-cons     t
      :g-map      (and x.alist t)))

;; Check whether x is a g-concrete object.
  (fgl-object-case x :g-concrete)

;; Check whether x is either a g-concrete or g-boolean object.
  (fgl-object-case x '(:g-concrete :g-boolean))

The first two examples above show fgl-object-case both case-splitting between different kinds and also binding fields of x using dotted notation, e.g. x.bits above is bound to (g-integer->bits x). The latter two show a special syntax that is a shortcut for checking the kind of x. Note that it is likely preferable to use (fgl-object-case x :g-concrete) rather than (eq (fgl-object-kind x) :g-concrete), even though they have the same meaning, because the former will produce an error in case you misspell :g-concrete.

Subtopics

Fgl-object-eval
Evaluator for FGL symbolic objects.
Fgl-object-p
Recognizer for fgl-object structures.
G-map
FGL object constructor for fast alists and arrays.
G-ite
FGL object constructor for if-then-else objects.
G-cons
FGL object constructor for conses.
G-concrete
FGL-object constructor for constant (quoted) objects.
G-apply
FGL object constructor for function calls.
G-integer
FGL object constructor for symbolic integers, with Boolean functions representing the bits.
Fgl-object-equiv
Basic equivalence relation for fgl-object structures.
G-boolean
FGL object constructor for symbolic Boolean objects.
G-var
FGL object constructor for free variables.
Fgl-bitvector
Bitvector representation in FGL
Fgl-object-kind
Get the kind (tag) of a fgl-object structure.
Summarize-fgl-object
Remove repeated unary function calls in an FGL object to create an object that might be smaller to print.
Fgl-object-alist
An alist mapping anything to fgl-object-p.
Fgl-objectlist
A list of fgl-object-p objects.
Fgl-object-fix
Fixing function for fgl-object structures.
Fgl-object-count
Measure for recurring over fgl-object structures.