Outline of the way the FGL interpreter works.

The FGL interpreter is called by the FGL clause processor in order to try and turn the theorem term into an equivalent Boolean formula, which then can perhaps be solved by SAT. In order to do this, it recursively interprets terms turning them into symbolic objects (see fgl-object) containing Boolean formula objects. In this doc topic we outline the operation of the interpreter.

The interpreter consists of a 31-way mutual recursion. We won't detail each of the functions in the mutual recursion, but we will try to cover in general terms all of the things that happen in them.

The highest-level entry point into the interpreter when trying to compute a
Boolean formula from a term is

- When it is a constant (quote), it returns the quoted value, coerced to a g-concrete symbolic object.
- When it is a variable, it looks up the variable in the current bindings (alist). There are actually two sets of bindings for our interpreter: "minor" bindings, which come from lambdas, and "major" bindings, which come from outermost contexts not inside any lambdas; these are checked in that order.
- When it is a lambda application, it processes the term into an equivalent
pair
(bindinglist body) . The bindinglist is a list of pairs(formals actuals) from the nest of lambdas, omitting formal/actual pairs that are the same. This may include the bindings of more than one lambda: if the body of a lambda is itself a lambda application, it recursively adds that to the bindinglist, stopping when it finds a lambda body that is not itself a lambda. The interpreter interprets the bindinglist by recurring through the list, recursively interpreting each of the actuals of each pair withfgl-interp-term-equivs . When a pair is done it adds the bindings formed by pairing the formals with the symbolic object results from the actuals to the minor bindings of the interpreter. When done with all the(formals actuals) pairs, it then recursively interprets the body, then pops off the bindings produced by the bindinglist, returning the symbolic object resulting from interpreting the body. - When it is a function call, it deals with a few special cases, described
next, and then the generic function call case. In the generic case, it first
recursively interprets the arguments of the function, then calls
fgl-interp-fncall , described below, on the function and symbolic objects resulting from the arguments.

The special cases of function calls include

- For
if terms, the test is recursively interpreted and coerced to a Boolean function usingfgl-interp-test . Then, unless a syntactic analysis shows that the path condition implies the test's negation, we recursively interpret the "then" branch withfgl-interp-term-equivs and with the test conjoined to the path condition, and unless the syntactic analysis shows the path condition implies the test, we recursively interpret the "else" branch with the negated test conjoined to the path condition. If both branches were interpreted, we then attempt to merge the results from the two branches into a single symbolic object usingfgl-interp-merge-branches , described below. - For
return-last , we provide special support fortime$ , allowing it to time the symbolic interpretation of the enclosed term. Otherwise, we simply interpret the last argument. Note this means thatprog2$ might not function as expected -- if you intend the first argument toprog2$ to be interpreted in FGL for side effects, you should instead bind it to an ignored variable or else use an equivalent two-argument function instead. - For
bind-var , we bind the first argument, which must be a variable that is not yet bound in the current major or minor frame, to the result of interpreting the second argument under theunequiv equivalence relation. Under this equivalence relation, every object is equivalent to every other object; this is sort of an "anything goes" mode which allows certain behavior that would normally be unsound. This is allowable in this context becausebind-var logically just returns its first argument (the variable), so the second argument is irrelevant. It is allowable to bind anything to the variable if it is not yet bound **** - For
binder , the argument must be a function call whose first argument is a variable, and that variable must be free in the current stack frame. The rest of that function's arguments are recursively interpreted, and then binder rewrite/meta rules are applied to choose a binding for the free variable based on the rest of the arguments. - For
abort-rewrite , the interpreter returnsnil and inserts a special error keyword in the interpreter state'serrmsg field, which will get caught when returning from the current major stack frame. - For
fgl-sat-check , we usefgl-interp-test to coerce the second argument (the condition to be tested) to a Boolean function, andfgl-interp-term-equivs to interpret the first argument (params). We then callinterp-st-sat-check , an attachable function which calls SAT and returns NIL if the input Boolean formula is unsat. - For
syntax-interp-fn , we check that the second argument is a quoted term (this is true for calls generated by thesyntax-interp andsyntax-bind macros) and that we're in anunequiv equivalence context. If so, we evaluate the first argument usingfancy-ev , with the current variable bindings from the symbolic interpreter passed in as the evaluation environment. For example, if a variablex is bound to a symbolic integer in our current interpreter frame, thenx will be bound to the fgl-object representation of that symbolic integer when evaluating thesyntax-interp term. This is similar to ACL2's syntaxp behavior, but the syntaxp term operates on FGL object syntax rather than ACL2 term syntax. - For
assume , we first check that we're in anunequiv equivalence context. Then we interpret the first and second arguments as if they were thetest andthen branches of anif ; in particular, the Boolean formula resulting from thetest is conjoined onto the path condition (that is, assumed) when symbolically executing thethen branch. We then simply return the result from thethen branch. - For
narrow-equiv , we interpret the first argument. If its result is a concrete object whose value satisfiesequiv-contexts-p and those equivalence contexts are a refinement (narrowing) of the interpreter state's current equiv-contexts, then we set the interpreter state's equiv-contexts field to that object while interpreting the second argument. This can be used to (conditionally) exit anunequiv context. - For
fgl-time-fn , we interpret the first argument and use that as atime$ format specifier for timing the interpretation of the second argument, returning the result from the second argument. - For
fgl-prog2 , we interpret the first argument under theunequiv equivalence context, discarding the result; then interpret the second argument under the current equivalence context and return its result. - For
fgl-interp-obj , we first check that we're in anunequiv equivalence context. Then we interpret the first argument. If its result is a concrete object whose value satisfiespseudo-term-p , then we interpret that term and return its result.

Generic function calls are run by

- If all the arguments are explicit, i.e. symbolic objects of the g-concrete kind, then try to execute the function using magic-ev-fncall. If it runs successfuly, return the result as a
g-concrete object. - Otherwise try applying each of the rules enabled for that function in the
fgl-rewrite-rules table usingfgl-rewrite-try-rule . These may be rewrite, meta, or primitive rules. If any of those rules succeeds, return the symbolic object produced by recursively interpreting the RHS of the rule under the unifying substitution. - Otherwise try executing a primitive associated with that function; see fgl-primitive-and-meta-rules. If successful, return the value from that primitive.
- Otherwise, if there exists a rule with rune
(:definition fnname) , or if there are rewrite/definition rules for that function listed in thefgl-definition-rules table, then try rewriting the call using those rules. - Finally, if none of the above were successful, produce the object
(g-apply fnname args) .

This completes the overview of how a term is interpreted and turned into
either a symbolic object (fgl-object) or Boolean formula. Next we
describe three subroutines that we skipped describing above:

If the hypotheses are all relieved, then we recurs on the conclusion using

During this process, various helper functions are also called to support tracing (see fgl-rewrite-tracing) and accumulated-persistence-style profiling, but none of these are logically relevant.

Application of binder rules is similar, but with slightly different logical contracts for the rules and very slightly different behavior. For binder rules, we unify the argument list with the argument list of the LHS of the rule, omitting the initial argument of the LHS which must be the variable to be bound. Binder rules also specify the equivalence context under which the RHS must be rewritten.

For

For

For

It first checks for trivial cases -- test constant true, test constant false,
or branches equal -- and returns the obvious results in those cases.
Otherwise, if either branch is a function call (g-apply) object, then it
tries applying branch merge rules for those functions using

Otherwise, if both branches are calls of the same function, it recursively
merges the argument lists and returns the function applied to the merged
arguments. Otherwise, it calls helper function

To do.