Skip to content

Latest commit

 

History

History

cv_translator

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Translator to cv type used by cv_compute

backend_32_cvScript.sml: Translate arch-size-specific functions to cv equations.

backend_64_cvScript.sml: Translate arch-size-specific functions to cv equations.

backend_ag32_cvScript.sml: Translate ag32-specialised functions to cv equations.

backend_arm8_cvScript.sml: Translate arm8-specialised functions to cv equations.

backend_cvScript.sml: Translate non-target-specific backend functions to cv equations.

backend_x64_cvScript.sml: Translate x64-specialised functions to cv equations.

backend_x64_evalScript.sml: Experiments with evaluating the compiler using cv_compute

eval_cake_compileLib.sml: Functions for in-logic evaluation of the CakeML compiler. These use HOL's cv_compute facility.

eval_cake_compile_ag32Lib.sml: Functions for in-logic evaluation of the CakeML compiler for ag32.

eval_cake_compile_arm8Lib.sml: Functions for in-logic evaluation of the CakeML compiler for arm8.

eval_cake_compile_x64Lib.sml: Functions for in-logic evaluation of the CakeML compiler for x64.

to_data_cvScript.sml: Translation of the to_data compiler function.