|
|
|---|
|
|
|
|---|
Check correct compilation.
As explained in compilation, this is a relation among the code, input, and output files, each of which is represented as a list of Unicode characters. This is a non-executable predicate, which makes use of an existential quantifier to introduce the code, input, and output CSTs, the code, input, and output ASTs, the static environment for the program a limit that suffuces to execute the program, the type of the output, and the value of the output.
Theorem:
(defthm compilep-suff (implies (and (abnf::treep code-cst) (abnf::treep input-cst) (abnf::treep output-cst) (filep code-ast) (input-filep input-ast) (output-filep output-ast) (senvp env) (natp limit) (typep output-type) (valuep output-value) (b* ((pkg (make-package :file code-ast)) (prg (make-program :package pkg))) (and (file-lex-parse-p code code-cst) (input-file-lex-parse-p input input-cst) (output-file-lex-parse-p output output-cst) (equal code-ast (abs-file code-cst)) (equal input-ast (abs-input-file input-cst)) (equal output-ast (abs-output-file output-cst)) (equal (check-program-and-input prg input-ast) env) (equal (check-output-file output-ast env) output-type) (equal (exec-program prg input-ast curve limit) (value-result-ok output-value)) (equal (eval-output-file output-ast curve) (value-result-ok output-value)) (equal (type-of-value output-value) output-type)))) (compilep code input output curve)))
Theorem:
(defthm booleanp-of-compilep (b* ((yes/no (compilep code input output curve))) (booleanp yes/no)) :rule-classes :rewrite)