How to Port a HERMIT test using the eval command - ku-fpg/hermit-shell GitHub Wiki

This is straightforward.

First, use eval everywhere

Consider the hermit test `examples/factorial'. See List of current tests for current tests.

The Fac.hss has:

load-as-rewrite "WWA" "WW-Ass-A.hss"
flatten-module
binding-of 'fac
ww-split [| wrap |] [| unwrap |] (ww-AssA-to-AssC WWA)
bash-extended-with [ case-elim-inline-scrutinee , inline [ 'unwrap, 'wrap, '*, '- ] ]

{ [def-rhs, let-body] ; alpha-lam 'n } -- cosmetic

As a eval version, it would be written, in FacScript.hs:

import HERMIT.API
script :: Shell ()
script = do
  eval "load-as-rewrite \"WWA\" \"WW-Ass-A.hss\""
  eval "flatten-module"
  eval "binding-of 'fac"
  eval "ww-split [| wrap |] [| unwrap |] (ww-AssA-to-AssC WWA)"
  eval "bash-extended-with [ case-elim-inline-scrutinee , inline [ 'unwrap, 'wrap, '*, '- ] ]"

  eval "{ [def-rhs, let-body] ; alpha-lam 'n } -- cosmetic"

Remember to copy the WW-Ass-A.hss file into the same directory. Now you can run the test.

> hermit-shell Fac.hs +Main
...
HERMIT> :l FacScript.hs
...
HERMIT> send script
...
HERMIT> resume

See. Easy!

Second, start replacing the eval with other commands.

import HERMIT.API
script :: Shell ()
script = do
  eval "load-as-rewrite \"WWA\" \"WW-Ass-A.hss\""
  eval "flatten-module"
  bindingOf "fac"  -- <=== THE CHANGED COMMAND
  eval "ww-split [| wrap |] [| unwrap |] (ww-AssA-to-AssC WWA)"
  eval "bash-extended-with [ case-elim-inline-scrutinee , inline [ 'unwrap, 'wrap, '*, '- ] ]"

  eval "{ [def-rhs, let-body] ; alpha-lam 'n } -- cosmetic"