search

ku-fpg / hermit

Haskell Equational Reasoning Model-to-Implementation Tunnel
http://www.ittc.ku.edu/csdl/fpg/Tools/HERMIT
BSD 2-Clause "Simplified" License
49 stars 8 forks source link

Navigation? #154

Open conal opened 8 years ago

conal commented 8 years ago

Does navigation work in the latest HERMIT? The commands down, left, and right aren't recognized. I found navigate, but when I use the down, left, or right keys in navigation mode, I get error messages like the following.

User error, unrecognized HERMIT command: "down"

Moreover, I like to run Hermit (and most things I do) inside Emacs, where those keys don't make it to the HERMIT process.

andygill commented 8 years ago

I believe that they are replaced by named commands, specific to the node at hand. One thing I will be working on as a matter of priority is documenting things (like this). I'll file a ticket about documentation.

conal commented 8 years ago

Great. Thanks. Meanwhile, I'm perusing the results of help Navigation.

ecaustin commented 8 years ago

I've been out of the loop for a bit, but last I recall the only navigation commands that we still supported were up and top.

I believe even those were under discussion for removal, or at least reimplementation.

xich commented 8 years ago

Yep, help Navigation should list things.

The directions have all been replaced by "crumbs". A crumb is a pair of parent and child (app-fun is the crumb which moves from an application node to it's function child. app-arg is the crumb that moves from application node to it's argument child.) A path is a list of crumbs. You can type in paths with Haskell list syntax. For instance, [lam-body, app-fun] should move you from (\y -> f y) to f.

There are other more powerful navigation commands like lams-body which just repeats lam-body until failure. Also binding-of, rhs-of, occurrence-of, and top.

xich commented 8 years ago

(The justification for crumbs is in section 4.2.2 of my dissertation.)

conal commented 8 years ago

Thanks. I just grabbed a copy.

On Sun, Jan 3, 2016 at 9:16 PM, Andrew Farmer notifications@github.com wrote:

(The justification for crumbs is in section 4.2.2 of my dissertation.)

— Reply to this email directly or view it on GitHub https://github.com/ku-fpg/hermit/issues/154#issuecomment-168583816.

conal commented 8 years ago

Is the "navigation" command/mode obsolete?

On Sun, Jan 3, 2016 at 9:13 PM, Evan Austin notifications@github.com wrote:

I've been out of the loop for a bit, but last I recall the only navigation commands that we still supported were up and top.

I believe even those were under discussion for removal, or at least reimplementation.

— Reply to this email directly or view it on GitHub https://github.com/ku-fpg/hermit/issues/154#issuecomment-168582703.

conal commented 8 years ago

Nice! Thanks for the tips.

On Sun, Jan 3, 2016 at 9:15 PM, Andrew Farmer notifications@github.com wrote:

Yep, help Navigation should list things.

The directions have all been replaced by "crumbs". A crumb is a pair of parent and child (app-fun is the crumb which moves from an application node to it's function child. app-arg is the crumb that moves from application node to it's argument child.) A path is a list of crumbs. You can type in paths with Haskell list syntax. For instance, [lam-body, app-fun] should move you from (\y -> f y) to f.

There are other more powerful navigation commands like lams-body which just repeats lam-body until failure. Also 'binding-of', rhs-of, occurrence-of, and top.

— Reply to this email directly or view it on GitHub https://github.com/ku-fpg/hermit/issues/154#issuecomment-168583423.