Skip to content

How to port a command to the new shell

Andy Gill edited this page May 30, 2015 · 12 revisions

Find the command in the hermit repo

Example: in module HERMIT.Dictionary.Local.Bind, there is nonrec-to-rec, and rec-to-nonrec.

-- | Externals for manipulating binding groups.
externals :: [External]
externals =
    [ external "nonrec-to-rec" (promoteBindR nonrecToRecR :: RewriteH LCore)
        [ "Convert a non-recursive binding into a recursive binding group with a single definition."
        , "NonRec v e ==> Rec [Def v e]" ]                           .+ Shallow
    , external "rec-to-nonrec" (promoteBindR recToNonrecR :: RewriteH LCore)
        [ "Convert a singleton recursive binding into a non-recursive binding group."
        , "Rec [Def v e] ==> NonRec v e,  (v not free in e)" ]
    ]

Transfer the command to the correct place in hermit-shell

Transfer the external definitions, adding an External instance if needed, and camel-case the name.

Example: in HERMIT.Server.Parser.Rewrite, in the hermit-shell repo:

instance External (RewriteH LCore) where
  parseExternals =
    [ external "nonrecToRec" (promoteBindR nonrecToRecR :: RewriteH LCore)
        [ "Convert a non-recursive binding into a recursive binding group with a single definition."
        , "NonRec v e ==> Rec [Def v e]" ]                           .+ Shallow
    , external "recToNonrec" (promoteBindR recToNonrecR :: RewriteH LCore)
        [ "Convert a singleton recursive binding into a non-recursive binding group."
        , "Rec [Def v e] ==> NonRec v e,  (v not free in e)" ]
    ]
  • This has allows the Server to understand the command. For now, we leave the command names as is (the are just Strings)

  • You may need to add some imports, to input promoteBindR nonrecToRecR, etc. Look at the module you copied from to see this.

Add an API entry for the command

Now, add an API entry. Remember to add the haddock comment.

Example: in the module HERMIT.API.Binding, in the hermit-shell repo, add:

-- | Convert a non-recursive binding into a recursive binding group with a single definition.
--   NonRec v e ==> Rec [Def v e]
nonrecToRec :: Rewrite Core
nonrecToRec = Transform $ method "nonrecToRec" []

-- | Convert a singleton recursive binding into a non-recursive binding group.
--   Rec [Def v e] ==> NonRec v e,  (v not free in e)
recToNonrec :: Rewrite Core
recToNonrec = Transform $ method "recToNonrec" []
  • Transform is the generalization of Rewrite, hence the Transform constructor.
  • RewriteH has been simplified to Rewrite, for the API.

Test it

> cabal install
> cd examples/fib
> hermit-shell Fib.hs
[...]
HERMIT> setPath (rhsOf "fib")
HERMIT> rewrite (anyTd recToNonRec)
...

Polymorphism

Sometimes, a command is used a different types. All transmitted command must be monomorphic. We use extra Proxy arguments to enable this. Look for anyCall or focus (not implemented yet) for an example.

Notes

  • Sometimes, you need to add a new type. See module HERMIT.API.Types for examples.

  • Idea - not implemented yet - You should be able to get a complete listing of supported commands direct from the server.

> cd examples/fib
> hermit-shell Fib.hs
[Lots of text]
HERMIT> bnf 
{- Shell () -}
display ::                      Shell ()
rewrite :: Rewrite LCore ->     Shell ()
rewrite :: Rewrite LCoreTC ->   Shell ()
...

{- Rewrite LCore -}
anyCall :: Rewrite LCore ->     Rewrite LCore
... 
...