parsing with narrowing

[grosu]

In a meeting with Ben yesterday, it came out that we can use narrowing for parsing. This morning I did some experiments using Maude's narrowing support to flush out the idea, and it seems to work:

in full-maude .

mod TOKENS is
  sorts Token TokenList .
  op nil : -> TokenList .
  op __ : Token TokenList -> TokenList .
  ops a b c d e f g h i j k l m n o p q r s t u v x y z w  0 1 2 3 4 5 6 7 8 9 : -> Token .
  op append : TokenList TokenList -> TokenList .
  var T : Token .  vars Ts Ts' : TokenList .
  rl append(nil,Ts') => Ts' .
  rl append(T Ts, Ts') => T append(Ts,Ts') .
endm

mod KAST is
  sorts KItem K KLabel KList .
  subsorts KItem < K < KList .
  op .KList : -> KList .
  op _,_ : KItem KList -> KList .
  op _`(_`) : KLabel KList -> KItem .
endm

mod GRAMMAR is
  including TOKENS .
  including KAST .

  op [_,_] : K KItem -> TokenList .

***(
  syntax S ::= S A | epsilon
  syntax A ::= a | b
***)

  sorts S A .
  subsorts S A < K .

  ops 'a:->A' 'b:->A' '__:S*A->S' 'epsilon:->S' : -> KLabel .

  vars S1 S2 : S .  vars A1 A2 : A .  vars K1 K2 : KItem .
  rl [S1, '__:S*A->S'(K1,K2)] => append([S2, K1], [A1, K2]) .
  rl [S1, 'epsilon:->S'(.KList)] => nil .

  rl [A1, 'a:->A'(.KList)] => a nil .
  rl [A1, 'b:->A'(.KList)] => b nil .

endm

select FULL-MAUDE .
loop init .

(search [1,5] in TOKENS :  append(Ts:TokenList, c d nil) ~>* a b c d nil .)

(search [1,7] in GRAMMAR :  [S1:S, AST:K] ~>* nil .)

(search [1,7] in GRAMMAR :  [S1:S, AST:K] ~>* a nil .)

(search [1,8] in GRAMMAR :  [S1:S, AST:K] ~>* a b nil .)

The above outputs:

search [1,5] in TOKENS : append(Ts:TokenList,c d nil) ~>* a b c d nil .

Solution 1
Ts:TokenList --> a b nil

No more solutions.

search [1,7] in GRAMMAR :[S1:S,AST:K] ~>* nil .

Solution 1
AST:K --> 'epsilon:->S'(.KList)

No more solutions.

search [1,7] in GRAMMAR :[S1:S,AST:K] ~>* a nil .

Solution 1
AST:K --> '__:S*A->S'(('epsilon:->S'(.KList)),'a:->A'(.KList))

No more solutions.

search [1,8] in GRAMMAR :[S1:S,AST:K] ~>* a b nil .

Solution 1
AST:K --> '__:S*A->S'(('__:S*A->S'(('epsilon:->S'(.KList)),'a:->A'(.KList))),'b:->A'(.KList))

No more solutions.

Bye.

Unfortunately, it looks like narrowing in Maude only works with full maude, and does not have support for associativity, so I had to cripple the definition to use append instead of associative lists. And in the end it is still slow. It takes about 1min for the above to terminate.

So here is my question. We want a powerful narrowing engine for test-case generation and many other reasons anyway in the K framework, which should interact well with strategies and associative lists. Then why not use that for parsing as well? Of course, you will say "performance", but can't we improve the performance to an extent that it will not be a bottleneck? We want narrowing to be fast anyway.

[laurayuwen]

Looks nice! If we have a mechanism to produce AST from narrowing path (maude can already show the path), mod GRAMMAR can be further simplified to have rules look like rl [A1] => a nil ., but this module will be automatically generated by parsing mechanism anyway. But this reminds me of how we used spoofax to create Java parser from SDF syntax, what is the technique there and how is narrowing approach going to beat them?

[grosu]

can be further simplified to have rules look like rl [A1] => a nil .

That's how it was initially, but I wanted to also see the AST. And the difference in performance is not that big. They are both equally slow.

But this reminds me of how we used spoofax to create Java parser from SDF syntax,

Why do you think there is any relationship here? SDF is specialized for parsing and that's what it does, it generates parsers from grammars, no narrowing, just a very specialized parser generator.

what is the technique there

Go ahead and read :) Both the SDF approach and our code to generate SDF from K and then parsers from SDF.

and how is narrowing approach going to beat them

Elegance and ease of implementation, provided to can bring the performance within bounds asymptotically similar.