Subject: Fragments

Keywords: ::tactic
          ::tnf
          ::hpf
          ::dekreitz

Title: Tactic Data

--------------------------------------------------

Each tactic function occuring in a Tactic Expression of an
INF step, may have an associated description object.

The tactic function object contains information about the 
semantics of the arguments as well as their syntactic types.
The object also contains a (token # term) property list.
The property list is primarily used to store data to assist
in constructing fragments from an INF step.

Such tactic data object are constructed when dekreitzing fragments. 
If a tactic function occurs in the source fragment that does not
have a tactic data object, then that source fragment fails to be
dekreitzed Once the tactic data object is added then the source 
fragment can be dekreitzed.

The argument semantic types themselves are described in data objects
as well.

The intent is that all data in the Tactic Expressionof a fragment
will be well described by these data objects so as to facilitate
programmatic manipulation of the fragment data. In this way fragments
can be made more abstract to allow greater reuse.    

There are similar tactic data objects for tacticals, conversionals, and
conversions.

⋅
--------------------------------------------------

Authors: 

Contributors: RICH:t
              NUPRL:t

⋅

Home