Querying/collecting, but with path-dependent contexts

[Malte Schwerhoff]

Dear Tony,

I have a language of logical terms, implemented via Scala case classes, which allows me to, e.g. represent the following term

  A && (B ==> C) && (D && E ==> F && (G ==> H))

where "A, B, ..." are atoms/propositions, "&&" denotes a conjunction and "==>" denotes an implication. The latter could be implemented as follows

  case class Implies(Term left, Term right) extends Term

and similarly for conjunctions.

I now need to collect, e.g. in a Seq[Term], under which conditions an atom can be reached: e.g. atoms A and B under the empty condition sequence [], C under condition sequence [B], F under [D,E] and H under [D,E,G].

It seems that a top-down traversal with an immutable context 'ctx' of type Seq[Term] that is copied upon recursive descent (and thus restored upon ascent), plus a mutable "global" sequence 'res', would do the trick: traversing downwards, the context would be extended by the left-hand side of each encountered conditional, and each time an atom 'a' is reached, the pair '(ctx, a)' would be added to the global sequence 'res'.

I've looked at the functions/strategies that Kiama provides, and 'collect' seems closest to what I have in mind — except that it does not allow me to maintain such a path-dependent context.

How would you implement the traversal I'm looking for with Kiama?

Thank you,

Malte

[Malte Schwerhoff]

Follow-up: Instead of copying an immutable context down the tree, I tried to maintain the condition sequence as a second, mutable global sequence to which values are added when going down the tree, and removed from when going upwards. Here is roughly what I've tried:

    var conditions = List.empty[Term]

    val qdown = query[Term] {
      case term: Implies =>
        println("   [do] implies")
        conditions = term.left :: conditions
      case term: Atom =>
        println(s"   [do] ${conditions.mkString(", ")}  -->  $term")
    }

    val qup = query[Term] {
      case term: Implies =>
        println("   [up] implies")
        conditions = conditions.tail
      case term: Atom =>
        println(s"   [up] ${conditions.mkString(", ")}  -->  $term")
    }

//    val strat = downup(qdown, qup)
    val strat = everywhere(downup(qdown, qup))

    strat(myTermToTraverse)

Unfortunately, neither of my attempts so far worked: with ''downup(qdown, qup)', nothing seems to happen, i.e. no println is hit. With 'everywhere(downup(qdown, qup))', I only see the "[do]" printlns — the upwards query doesn't seem to be executed — and consequently, the conditions are accumulated across the whole tree, not path-wise.

Best regards,

Malte

[Tony Sloane]

Hi Malte,

As you are finding, it’s quite fiddly to propagate extra information through traversals and keep it all straight. Also, Kiama’s query traversals are not as expressive as the rewriting ones. 

I think if it was me I would be looking at using attributes to do this kind of job instead of traversals. If you think of things like “under which conditions can an atom be reached” as a property of the atom node, then it’s clearer to encode as an attribute of that node, I think.

Suppose we have this grammar 

R ::= T

T ::= A | T && T | T ==> T

where A is an atom and R is the root of the tree. We can define an inherited attribute “conds” for the conditions a term depends on with equations something like this (numbering non-terminals to distinguish occurrences)

R ::= T

    T.conds = []

T1 ::= T2 && T3

    T2.conds = T1.conds

    T3.conds = T1.conds 

T1 ::= T2 ==> T3

    T2.conds = T1.conds

    T3.conds = T1.conds ++ [T2]

Encoding this kind of thing using Kiama is fairly easy once you get your head around how we deal with inherited attributes. You could have something like:

val conds : Term => Seq[Term] =

attr {

case tree.parent(t : And) =>

conds(t)

case tree.parent.pair(n, t @ Implies(l, _)) if n eq l =>

conds(t)

case tree.parent.pair(n, t @ Implies(l, r)) if n eq r =>

conds(t) ++ List(l)

case _ =>

List.empty()

}

The tree.parent pattern matching stuff is how Kiama encodes inherited attribute equations where the equation to choose depends on what is higher up in the tree. The pattern tree.parent(p) succeeds if the node being matched has a parent and it binds p to the parent node. Similarly, tree.parent.pair(n, p) succeeds if n matches the current node and p matches the parent. Each of n and p can be nested patterns, so you can craft checks to match further against what is above. The two cases for Implies distinguish between whether the current node is the left or the right child of the Implies. The default case is used when there is no parent, i.e., you’re at the top of the tree, so there is no need for the R ::= T production.

There are plenty of examples in the Kiama repo of using attributes for similar kinds of things, including how to set up the tree stuff. Look for modules like semantic analysis for the sample languages. Of course, I’m happy to help if you get stuck. Also, the following paper might be of interest:

https://link.springer.com/chapter/10.1007/978-3-319-11245-9_11

cheers,

Tony

--
You received this message because you are subscribed to the Google Groups "kiama" group.
To unsubscribe from this group and stop receiving emails from it, send an email to kiama+un...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/kiama/881d7d89-25a8-4df2-8561-8ad4515cc5ea%40googlegroups.com.

[Malte Schwerhoff]

Hi Tony,

Thank you very much for your quick and helpful response. I've implemented the attribute you suggested and then, given a term t, used 'collect' to gather all atoms occurring in t, and the respective path conditions, :

  val conds : Term => Seq[Term] = attr { /* essentially what you suggested */ }

  collect[...] {                                              
    case atom: Atom =>
      (conds(atom), atom)
  }                                                                                  

Works like charm :-)

Best regards,

Malte

Tony

To unsubscribe from this group and stop receiving emails from it, send an email to ki...@googlegroups.com.

[Tony Sloane]

Hi Malte,

Excellent! I’m glad to hear that it worked well.

Yes, using attributes to define properties then collect to bring some of them together is a common approach for us. We usually use something like that to collect semantic errors from a tree. Attributes define the properties such as environments and types. Then a single collect goes over the whole tree checking conditions and collecting any error messages. Kiama’s Messaging module has a collectMessages method that makes this easy.

cheers,

Tony

To unsubscribe from this group and stop receiving emails from it, send an email to kiama+un...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/kiama/367fa08d-5da2-4f61-9325-7991a90decdd%40googlegroups.com.