List of keywords

From Dyna
Jump to: navigation, search


Declaration names

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.

Literal constants

true, false, inf, neg_inf

Type names

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.

Primitive types

int, double, etc.

Computed types

+, *, 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:

  • term (all terms)
    • primitive
    • structure
      • atom
      • compound

Other automatic union types describe different kinds of expressions. An expression is a term with a value:

  • expr (all expressions)
    • 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 foo item.

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 double if i is an expr_double. In the same way we have subtypes such as item_double and axiom_double; on the C++ side, you can assign a double to c[i] if i is an axiom_double.

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 cons and nil.

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 cons nor nil has no list type.

Personal tools