3.9 termlint.pl -- Term type checker

author

Gergo Barany <gergo@complang.tuwien.ac.at>

version

0.8.6-rc4

copyright

Copyright (C) 2009 Gergo Barany

license

See COPYING in the root folder of the SATIrE project

This is term_lint.pl, a small tool for checking terms against a tree grammar (abstract syntax).

term_match(+Term, +NonterminalSymbol)

OK. Here is the semantics to the structures defined above:

The grammar is a sequence of grammar rules. Each rule is of the form Nonterminal ::= Body. There should be no two rules for the same nonterminal (use | instead), but this is not checked.

Body has the following meaning:

atom

a nonterminal, references another rule to be used

A | B

match A; if that fails, match B

A where C

match A; if that succeeds, call Prolog goal C

{}(A)

unify with term A; {_} means "any term", {foo} is terminal foo atomsAs match one of the atoms in As functorsFswithA1,...(),An match term F(A1,...,An) where F is a functor in Fs

f(A1, ..., An)

match a term with functor f, where arguments match A1,...,An

Argument expressions (in argument tuples) can be:

atom

a nonterminal ?A term is "missing" (see below) or matches argument expression A

{}(A)

unify with term A

.(A,)

list of terms matching argument expression A

As a special case, [_] means "list of any type".

Options (A?) are resolved as follows: If the term under consideration is a solution of predicate missing/1 (to be defined along with the grammar rules), there is a match; otherwise a term of type A must be matched.

Predicates to be defined along with the grammar rules are:

missing() / 1

defines what A? can match except for A

start_symbol() / 1

single solution is the start symbol of the grammar

Here are a few example grammars to illustrate the explanations above.

Arithmetic expressions, simple verbose version:

var ::= {VarName} where atom(VarName).
num ::= {Number} where number(Number).
expr ::=
  var
| num
| expr + expr
| expr - expr
| expr * expr
| expr / expr.

Arithmetic expressions, more condensed version:

expr ::=
  {Leaf} where (atom(Leaf) ; number(Leaf))
| functors [+, -, *, /] with (expr, expr).

*Simple type system*:

type ::=
  atoms [number, character, string]
| function_type([type] /* argument types */, type? /* return type if any */).

missing(none).    /* what to match if no return type is given */

Partial specification (some parts are not constrained):

allowed ::=
  lst([_])        /* argument is list of some unknown things */
| opt(allowed?)   /* argument is missing, or of type allowed */
| any({_}).       /* argument is any term (anything unifies with _) */

missing(nothing).

In this last example, some allowed terms are:

  lst([]), lst([f(f)]), lst([x,y]), ...
  opt(nothing), opt(lst([])), opt(opt(nothing)), ...
  any(foo), any(g(f(x))), ...

One more thing, which might not be explicit from the stuff above: The anonymous variable _ (free variables in general) may appear in the grammar, but only inside[]or {}:

.(Arg1,)

(list of any type) or

{}(Arg1)

(any term) or

{}(foo(_G1453))

(any term with functor foo)

but:

foo() ::= foo(Arg1)

is not allowed; use foo ::= foo({_})

foo() ::= Xwherecond(X)

is not allowed; use foo ::= {X} where cond(X)

The interpreter does not check these things at the moment. Which means that grammars containing variables in weird places will misbehave in weird ways.