Spurious `()` function arguments in ML terms extracted from Pulse

[tahina-pro]

Context: I am trying to extract DPE to C via krml and I am hitting some ML extraction roadblocks: some ML code extracted from Pulse fails to trigger the expected Karamel extraction rules.

On branch taramana_pulse_krml_20240308, I added two Karamel extraction tests:

A failing extraction test

I have a failing extraction test trying to extract Pulse.Lib.Reference.replace (this function would extract to a Rust primitive, but has no C primitive equivalent, so I need to extract its implementation Pulse.Lib.Reference.replace' to C and let Karamel monomorphize it.)

When running make -C share/pulse/examples -f Example.KrmlExtractionTest.Failure.Makefile, a .krml file is produced, but then Karamel tries to extract the implementation of Pulse.Lib.Reference,op_Bang, and of course fails. This means that the corresponding rule for op_Bang in src/extraction/ExtractPulse.fst is not triggered.

I instrumented ExtractPulse.fst to print all ML expressions before they are extracted to Krml. I found out that, when trying to extract Pulse.Lib.Reference.replace', Pulse extraction produced the following ML expression (after flattening):

(MLE_App ((MLE_TApp ((MLE_Name (Pulse.Lib.Reference, op_Bang)), ['a])),
  [(MLE_Const MLC_Unit); (MLE_Var r); (MLE_Const MLC_Unit); (MLE_Const MLC_Unit)]))

(excerpt from the output of this command: make -C share/pulse/examples -f Example.KrmlExtractionTest.Failure.Makefile _output/Example.KrmlExtractionTest.Failure/Pulse_Lib_Reference.krml)

Notice that there is a spurious Unit between op_Bang and its non-ghost argument r. I don't know where this spurious Unit comes from, but because of it, the ML-to-krml extraction rules for op_Bang do not trigger.

A successful extraction test

By contrast, I also have a successful extraction test where I copy and paste the implementation of Pulse.Lib.Reference.replace' and call that copy. Curiously, ML extraction adds no spurious () there, and so Krml extraction rule for op_Bang successfully triggers, and Karamel successfully produces a meaningful C file in share/pulse/examples/_output/Example.KrmlExtractionTest.Success

Can anyone please help me? Thanks in advance!

[aseemr]

Hi @tahina-pro, thanks for the setup to reproduce the issue. I pushed a fix in main to eta expand op_Bang ... this should unblock you.

[tahina-pro]

Yes, your fix works well, cf. https://github.com/FStarLang/pulse/actions/runs/8239395914 Thank you Aseem!