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

Getting RULES to fire before HERMIT starts #177

Open roboguy13 opened 7 years ago

roboguy13 commented 7 years ago

Is there a way to get all rewrite RULES that GHC would normally apply to fire before HERMIT's REPL starts running? Or is there a HERMIT command that would do something along those lines (to fire all RULES that currently apply everywhere)?

xich commented 7 years ago

If you want to do it the 'real' way, you could run HERMIT later in the pipeline, after the first round of simplification and rule application.

If you want to be able to do it on a whim, you can (with the diff I just pushed):

do
  f <- compileRulesT (const True) -- all rules
  repeatR $ anytdR (runFoldR f)

But that is not quite the same as what GHC does, because there can be specialization rules on binders. For that you'd need (I'm speculating, haven't typechecked):

do
  f <- compileRulesT (const True)
  repeatR $ anytdR $ runFoldR f <+ (contextonlyT hermitCoreRules >>= unfoldRulesR)

(essentially, the bit after <+ is getting all the spec rules accumulated in the context at each point in the AST and compiling and running those separately)

You could just repeatR $ anytdR $ (map snd <$> getHermitRulesT) >>= unfoldRulesR, but compiling the top-level stuff beforehand will be a huge perf win.

roboguy13 commented 7 years ago

@xich Thanks! This might be slightly off-topic but if I were to write a GHC plugin, how would I tell the system to run it later in the pipeline (after the RULES have fired)?

xich commented 7 years ago

If you're using hermitPlugin, you can use one of the guards here:

https://github.com/ku-fpg/hermit/blob/d38052f3ec4cdbcc3ed4df308dae5588354c5be7/src/HERMIT/Plugin.hs#L151

xich commented 7 years ago

If you are using the default HERMIT (invoking via hermit command as normal), there is a -pN flag, where N is the desired position in the pipeline. PluginM is much more precise though.

roboguy13 commented 7 years ago

@xich Well, right now I'm trying to develop a small plugin, which is why this is probably slightly off-topic =). Using HERMIT would be tricky at the moment because hermit-shell isn't working on GHC 8 for the time being and compileRulesT isn't exposed (although that second one would be a fairly quick fix). I've tried appending my pass to the end of the list of passes, but that didn't seem to make a difference (not fully sure though). The list of passes provided to the plugin seems to only contain one element too, which is surprising to me.