-
Notifications
You must be signed in to change notification settings - Fork 90
Open
Labels
Description
Currently, we have two compiler configs. The original one:
cakeml/compiler/backend/backendScript.sml
Lines 24 to 38 in 8f782f6
| Datatype: | |
| config = | |
| <| source_conf : source_to_flat$config | |
| ; clos_conf : clos_to_bvl$config | |
| ; bvl_conf : bvl_to_bvi$config | |
| ; data_conf : data_to_word$config | |
| ; word_to_word_conf : word_to_word$config | |
| ; word_conf : word_to_stack$config | |
| ; stack_conf : stack_to_lab$config | |
| ; lab_conf : 'a lab_to_target$config | |
| ; symbols : (mlstring # num # num) list | |
| ; tap_conf : tap_config | |
| ; exported : mlstring list (* field for Pancake entry points - empty for CakeML *) | |
| |> | |
| End |
And the version adapted for Eval:
cakeml/compiler/backend/backendScript.sml
Lines 634 to 648 in 8f782f6
| Datatype: | |
| inc_config = | |
| <| inc_source_conf : source_to_flat$config | |
| ; inc_clos_conf : clos_to_bvl$config | |
| ; inc_bvl_conf : bvl_to_bvi$config | |
| ; inc_data_conf : data_to_word$config | |
| ; inc_word_to_word_conf : word_to_word$config | |
| ; inc_word_conf : word_to_stack$config | |
| ; inc_stack_conf : stack_to_lab$config | |
| ; inc_lab_conf : lab_to_target$inc_config | |
| ; inc_symbols : (mlstring # num # num) list | |
| ; inc_tap_conf : tap_config | |
| ; inc_exported : mlstring list | |
| |> | |
| End |
The original is called config and the new version is called inc_config. The only difference between them is that inc_config drops asm_conf from within lab_conf, since it contains function fields in a record type. Function types don't serialise well to text (for Eval) and the cv translator also struggles them.
This issue is about replacing config by inc_config everywhere.