This module defines some predicates which are useful for writing programs which process assertions (as defined in the assertions library). The exported predicates allow reading assertions in all acceptable syntactic forms and converting them to a normalized format.
If you want to have access to some of the declarations read by the predicates exported by this file it is also necessary to include the library compiler/c_itf.
This is the main entry point to the assertion reader/normalizer. Reads all declarations and code in I and leaves it asserted in the database, in the format defined in 'compiler/c_itf'. Clauses are stored in clause_read/7. Used packages are stored in use_pkg/2.
Also, it reads and normalizes all assertions in this file and all related files, leaving them asserted in assertion_read/9 facts. If up to date .asr files exist for this or any of the related files, the assertion information is read directly from such .asr files. Otherwise, the .pl file is read and an up to date .asr file is generated containing all assertions in the .pl file, normalized and stored as assertion_read/9 facts.
M is the name of the module defined by the file. Base is the absolute name of the file I but with no suffix. Suffix is the file suffix (e.g., '.pl'). Dir is the directory part of the filename (with no / at the end).
Since this predicate is intended for gathering file information for purposes which can be other than compilation to executable code (e.g., generating documentation or in the preprocessor) this predicate catches errors and proceeds in cases where file processing (e.g., during actual compilation) might normally abort.
Version which accepts some options in Opts. In particular, '-v' produces verbose output for debugging. Also passes on the options in Opts to pass two of the assertion normalizer.
Cleans up data asserted by assertion/code reader/normalizer.
This predicate is useful for checking the syntax of the code and assertions in a file, as well as imports and exports. Full (semantic) assertion checking must be done with the preprocessor.
Each fact represents that an assertion for Goal has been read in module M, which has status Status and is of type Type. Body is the actual body of the assertion. Dict contains the names of the variables which appear in the assertion. Source is the file in which the assertion appears (treats included files correctly). LB and LE are the first and last line numbers in this source file in which the assertion appears (if the source is not available or has not been read LB=LE=0). Goal may be normalized or not, i.e., it may contain modes or properties, but it is always a term of the same functor and arity as the predicate it represents (i.e., it is not in Functor/Arity format). Body is always normalized (but the properties or property conjunctions inside may not -- see normalize_assertions_pass_one/1 and normalize_assertions_pass_two/1.
Reads the data in the .asr file. Fails if version is different from current version (so that .asr will be regenerated).
Prints the assertions stored in the database as assertion_read/9 facts, performing some pretty-printing and simplification (e.g., eliminating empty fields). If M is instantiated, only information on module M is printed. Otherwise information for all modules is printed.
Prints the assertions stored in the database as assertion_read/9 facts, in a raw format (no attempt is made to simplify the assertions). If M is instantiated, only information on module M is printed. Otherwise information for all modules is printed.
This predicate allows to compound a list of global properties in to sucessive meta-calls
This predicate allows to compound a list of global properties in to successive meta-calls, but in the third argument you can use your own selector.
:- true pred compare(?atm,@term,@term) => member([(=),(>),(<)]) * term * term.