List of keywords
See list of declarations. These keywords are used in the :- ... declaration syntax ... a Dyna programmer is free to reuse them for type or field names without fear of conflict. In fact, many of them coincide with the names of automatically declared union types.
true, false, inf, neg_inf
These compile into C++ classes, which means that they may not be used as C++ variable or names in the same C++ namespace. Also, they may not be used as Dyna field names.
int, double, etc.
+, *, etc.
C++ names for infix operators
Give a translation table: + translates to plus, * translates to times, / to slash, : to colon, += to logplus, == to doubleequals, etc. None of these are reserved words, it's just that you have to know the correspondence.
Automatically declared union types
Dyna automatically creates some union types for your convenience.
- Not all of these are implemented yet (easy to do, though).
- Should probably move this section onto its own page, or to the declaration inference page.
Some automatic union types describe different classes of terms:
Other automatic union types describe different kinds of expressions. An expression is a term with a value:
primitive(the value of a primitive is itself)
computed(not sure if we need this name, but it means that the top level functor is an operator)
item(all expressions that are not primitive or computed)
theorem(appears on the left-hand side of a rule)
axiom(all items that are not theorems)
assertable(maybe we should also allow assertable theorems, if declared as such? there is potential overhead because it requires special backpointers and prevents the item from being transient; best to handle as a program transformation, and perhaps not even worth it)
foreign_axiom(what we used to call user items)
trainable(axiom types that are explicitly declared as trainable; may include both asserted and foreign axioms)
For each theorem type,
foo, we also have a type
foo_antecedent which is a union over all the
expr types that appear on the right-hand side of rules producing
foo. We also have a type
foo_consequent which is a union over all the item types that appear on the left-hand side of rules using
foo. It is possible to construct iterators over all the antecedents or consequents of a given
We also have expression subtypes according to their value type:
expr_double and so forth. For example, a
log term is an
expr_double whose argument is an
expr_double (this results in some type checking), and on the C++ side,
c[i] returns a
i is an
expr_double. In the same way we have subtypes such as
axiom_double; on the C++ side, you can assign a double to
i is an
- We need to check carefully that this works with respect to overloading: there may be several subtypes of
*with different valtypes and storage disciplines, only some of which are subtypes of foo_antecedents.
Another automatically declared union type is
list, whose subtypes are
A union type is not automatically declared if it would be empty. For example, a program with no inference rules has no
theorem type, and a program that uses neither
nil has no