☰

Assertion processing library

Author(s): Manuel Hermenegildo.

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.

Documentation on exports

PREDICATEget_code_and_related_assertions/5

Usage:get_code_and_related_assertions(I,M,Base,Suffix,Dir)

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.

PREDICATEget_code_and_related_assertions_opts/6

Usage:get_code_and_related_assertions_opts(I,Opts,M,Base,Suffix,Dir)

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.

PREDICATEcleanup_code_and_related_assertions/0

Usage:

Cleans up data asserted by assertion/code reader/normalizer.

    PREDICATEcheck_code_and_assrt_syntax/1

    Usage:check_code_and_assrt_syntax(I)

    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.

    • Call and exit should be compatible with:
      (c_itf_props:filename/1)I is an atom describing the name of a file.
    • The following properties should hold at call time:
      (term_typing:ground/1)I is currently ground (it contains no variables).
    • The following properties should hold upon exit:
      (term_typing:ground/1)I is currently ground (it contains no variables).

    PREDICATEuse_pkg/2

    Usage:use_pkg(Base,Pkg)

    After calling get_assertions_and_code/5 this predicate contains the packages used in the file. The format is the same as that of package/2 in c_itf

    The predicate is of type data.

    PREDICATEclause_read/7

    Usage:clause_read(Base,Head,Body,VarNames,Source,Line0,Line1)

    After calling get_assertions_and_code/5 this predicate contains the clauses in the file. The format is the same as that of clause_of/7 in c_itf

    The predicate is of type data.

    PREDICATEassertion_read/9

    Usage:assertion_read(Goal,M,Status,Type,Body,Dict,Source,LB,LE)

    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.

    The predicate is of type data.

    PREDICATEassertion_body/7
    assertion_body(Pred,Compat,Call,Succ,Comp,Comm,Asst)

    assertion_body(Pred,Compat,Call,Succ,Comp,Comm,Asst)

    PREDICATEgenerate_asr_file/2
    No further documentation available for this predicate.

    PREDICATEread_asr_file/2

    Usage:

    Reads the data in the .asr file. Fails if version is different from current version (so that .asr will be regenerated).

      PREDICATErel_data/1
      No further documentation available for this predicate. The predicate is of type data.

      PREDICATEprint_assertions/1

      Usage:print_assertions(M)

      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.

      PREDICATEprint_unformatted_assertions/1

      Usage:print_unformatted_assertions(M)

      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.

      PREDICATEcomps_to_goal/3

      Usage 1:

      This predicate allows to compound a list of global properties in to sucessive meta-calls

        Usage 2:

        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.

          PREDICATEcomps_to_goal/4
          No further documentation available for this predicate. Meta-predicate with arguments: comps_to_goal(?,pred(3),?,?).

          PREDICATEnormalize_assertion/9

          Usage:normalize_assertion(M,Assrt,PD,AStatus,AType,NABody,S,LB,LE)

          Normalizes one assertion (see normalize_assertions/3).

          PREDICATEnorm_goal_prop/3
          norm_goal_prop(Prop,NProp,NPr)

          Prop is a term describing a global property in an assertion. NProp is its normalized version, where NPr is the extra argument. E.g., norm_goal_prop(regtype,regtype(p(X)),p(X)).

          Usage 1:norm_goal_prop(Prop,NProp,NPr)

          Normalizes a global property.

          Usage 2:norm_goal_prop(Prop,NProp,NPr)

          Denormalizes a global property.

          PREDICATEdenorm_goal_prop/3

          Usage:denorm_goal_prop(NProp,Prop,NPr)

          Denormalizes a global property.

          PREDICATEprop_apply/3
          No further documentation available for this predicate.

          PREDICATEprop_unapply/3
          No further documentation available for this predicate.

          PREDICATEprop_argvar/2
          No further documentation available for this predicate.

          Generated with LPdoc using Ciao