{"action":"created","issue":{"url":"https://api.github.com/repos/kframework/k/issues/2150","repository_url":"https://api.github.com/repos/kframework/k","labels_url":"https://api.github.com/repos/kframework/k/issues/2150/labels{/name}","comments_url":"https://api.github.com/repos/kframework/k/issues/2150/comments","events_url":"https://api.github.com/repos/kframework/k/issues/2150/events","html_url":"https://github.com/kframework/k/issues/2150","id":133447620,"number":2150,"title":"parsing with narrowing","user":{"login":"grosu","id":3733729,"avatar_url":"https://avatars.githubusercontent.com/u/3733729?v=3","gravatar_id":"","url":"https://api.github.com/users/grosu","html_url":"https://github.com/grosu","followers_url":"https://api.github.com/users/grosu/followers","following_url":"https://api.github.com/users/grosu/following{/other_user}","gists_url":"https://api.github.com/users/grosu/gists{/gist_id}","starred_url":"https://api.github.com/users/grosu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/grosu/subscriptions","organizations_url":"https://api.github.com/users/grosu/orgs","repos_url":"https://api.github.com/users/grosu/repos","events_url":"https://api.github.com/users/grosu/events{/privacy}","received_events_url":"https://api.github.com/users/grosu/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2016-02-13T16:45:21Z","updated_at":"2016-02-14T15:12:43Z","closed_at":null,"body":"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:\r\n\r\n```\r\nin full-maude .\r\n\r\nmod TOKENS is\r\n  sorts Token TokenList .\r\n  op nil : -> TokenList .\r\n  op __ : Token TokenList -> TokenList .\r\n  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 .\r\n  op append : TokenList TokenList -> TokenList .\r\n  var T : Token .  vars Ts Ts' : TokenList .\r\n  rl append(nil,Ts') => Ts' .\r\n  rl append(T Ts, Ts') => T append(Ts,Ts') .\r\nendm\r\n\r\nmod KAST is\r\n  sorts KItem K KLabel KList .\r\n  subsorts KItem < K < KList .\r\n  op .KList : -> KList .\r\n  op _,_ : KItem KList -> KList .\r\n  op _`(_`) : KLabel KList -> KItem .\r\nendm\r\n\r\nmod GRAMMAR is\r\n  including TOKENS .\r\n  including KAST .\r\n\r\n  op [_,_] : K KItem -> TokenList .\r\n\r\n***(\r\n  syntax S ::= S A | epsilon\r\n  syntax A ::= a | b\r\n***)\r\n\r\n  sorts S A .\r\n  subsorts S A < K .\r\n\r\n  ops 'a:->A' 'b:->A' '__:S*A->S' 'epsilon:->S' : -> KLabel .\r\n\r\n  vars S1 S2 : S .  vars A1 A2 : A .  vars K1 K2 : KItem .\r\n  rl [S1, '__:S*A->S'(K1,K2)] => append([S2, K1], [A1, K2]) .\r\n  rl [S1, 'epsilon:->S'(.KList)] => nil .\r\n\r\n  rl [A1, 'a:->A'(.KList)] => a nil .\r\n  rl [A1, 'b:->A'(.KList)] => b nil .\r\n\r\nendm\r\n\r\nselect FULL-MAUDE .\r\nloop init .\r\n\r\n(search [1,5] in TOKENS :  append(Ts:TokenList, c d nil) ~>* a b c d nil .)\r\n\r\n(search [1,7] in GRAMMAR :  [S1:S, AST:K] ~>* nil .)\r\n\r\n(search [1,7] in GRAMMAR :  [S1:S, AST:K] ~>* a nil .)\r\n\r\n(search [1,8] in GRAMMAR :  [S1:S, AST:K] ~>* a b nil .)\r\n```\r\nThe above outputs:\r\n```\r\nsearch [1,5] in TOKENS : append(Ts:TokenList,c d nil) ~>* a b c d nil .\r\n\r\nSolution 1\r\nTs:TokenList --> a b nil\r\n\r\nNo more solutions.\r\n\r\nsearch [1,7] in GRAMMAR :[S1:S,AST:K] ~>* nil .\r\n\r\nSolution 1\r\nAST:K --> 'epsilon:->S'(.KList)\r\n\r\nNo more solutions.\r\n\r\nsearch [1,7] in GRAMMAR :[S1:S,AST:K] ~>* a nil .\r\n\r\nSolution 1\r\nAST:K --> '__:S*A->S'(('epsilon:->S'(.KList)),'a:->A'(.KList))\r\n\r\nNo more solutions.\r\n\r\nsearch [1,8] in GRAMMAR :[S1:S,AST:K] ~>* a b nil .\r\n\r\nSolution 1\r\nAST:K --> '__:S*A->S'(('__:S*A->S'(('epsilon:->S'(.KList)),'a:->A'(.KList))),'b:->A'(.KList))\r\n\r\nNo more solutions.\r\n\r\nBye.\r\n```\r\nUnfortunately, 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.\r\n\r\nSo 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.\r\n"},"comment":{"url":"https://api.github.com/repos/kframework/k/issues/comments/183904221","html_url":"https://github.com/kframework/k/issues/2150#issuecomment-183904221","issue_url":"https://api.github.com/repos/kframework/k/issues/2150","id":183904221,"user":{"login":"laurayuwen","id":3274406,"avatar_url":"https://avatars.githubusercontent.com/u/3274406?v=3","gravatar_id":"","url":"https://api.github.com/users/laurayuwen","html_url":"https://github.com/laurayuwen","followers_url":"https://api.github.com/users/laurayuwen/followers","following_url":"https://api.github.com/users/laurayuwen/following{/other_user}","gists_url":"https://api.github.com/users/laurayuwen/gists{/gist_id}","starred_url":"https://api.github.com/users/laurayuwen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/laurayuwen/subscriptions","organizations_url":"https://api.github.com/users/laurayuwen/orgs","repos_url":"https://api.github.com/users/laurayuwen/repos","events_url":"https://api.github.com/users/laurayuwen/events{/privacy}","received_events_url":"https://api.github.com/users/laurayuwen/received_events","type":"User","site_admin":false},"created_at":"2016-02-14T15:12:43Z","updated_at":"2016-02-14T15:12:43Z","body":"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. \r\nBut 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?"}}