search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

Support for printing arbitrary K terms #280

Open denis-bogdanas opened 10 years ago

denis-bogdanas commented 10 years ago

It would be nice to print arbitrary K terms at the console, like:

... . => ListItem(elab(K) ~> elabInstanceInit)

This would greatly help debugging infinite loops. When computation just get stuck we can perform debugging by analyzing the content of with some unprinted K terms. Even if they are not printed. But when computation don't terminate there is no way to retrieve the content of unless it is properly printed during execution.

denis-bogdanas commented 10 years ago

More generally, a function K2String(K) would be great.

grosu commented 10 years ago

I thought we already have that. The same way we have #parse we should also have #print. The former parses a string into a K term, while the latter does the inverse. Both of these can/should take different options.

denis-bogdanas commented 10 years ago

No we don't. Searching #print over K repository returns nothing.

traiansf commented 10 years ago

We definitely have some which Dwight implemented using the Maude meta-level. Not sure how useful it is in this context, though

2014-03-11 12:55 GMT+02:00 Denis Bogdanas notifications@github.com:

No we don't. Searching #print over K repository returns nothing.

— Reply to this email directly or view it on GitHubhttps://github.com/kframework/k/issues/280#issuecomment-37283451 .