Some feature requests from Oege de Moor:

Hi Oege,

Regarding properties:

> does it always produce a well-formed term,

When using concrete syntax for term patterns and only using
simple rewrite rules, and a simple strategy that only applies rules, it
is sufficient to check that the syntactic sort of the lhs and rhs of a
rule is the same to guarantee well-formedness of the result.

This could also be checked for plain terms against a signature. We
should probably add such a check to the compiler.

> Ah, I see. Using concrete syntax implies that you cannot plug a
> variable into the wrong position on the rhs.

Yes, if you are using the meta-variables of SDF. For example,
in the following rule

DefSum :
|[ sum x = e1 to e2 ( e3 ) ]| ->
|[ let var y := 0
in (for x := e1 to e2 do y := y + e3); y
end ]|
where y := “sum”

x and y are meta-variables of type Id, and e1, e2, and e3 are meta-
variables of type Exp. Thus, it would be syntactically incorrect
to write

for e1 := …

On the other hand if you would be using anti-quotation as in

DefSum :
|[ sum #id[x] = #[e1] to #e2 ]| ->
|[ let var #id[y] := 0
in (for #id[x] := #[e1] to #[e2] do #id[y] := #id[y] + #[e3]); #id[y]
end ]|
where y := “sum”

then you could still mess up by writing

for #id[e1] := …

The parser would check that the anti-quotations are correct, but not the
Stratego terms inserted in them. A well-formedness checker for terms
could of course catch this.

> does it cover all cases

In what sense? If you are doing simplifications then you simplify what
you can. But I guess that you are eliminating a construct completely
using rewrite rules. In that case it would make sense to check the left-
hand sides against the signature to see if the patterns for
that construct as top-level constructor are complete.

> does it terminate, is it confluent?

For most of the things we usually do (involving more complex strategies)
these questions are probably undecidable. For simpler things they are
usually obvious. It might be interesting to try to use existing
termination/confluence checkers. (You can get the AST for your Stratego
program from the compiler; it should be a piece of cake to transform
that to input for such a checker; I’d be interested in the result;-)

Submitted on 15 May 2006 at 16:41