Skip to content

Latest commit

 

History

History

translation

Translation scripts for the Dafny compiler.

cakeml_and_dafny_astProgScript.sml:

  • Translates CakeML's and Dafny's AST types.

dafny_astProgScript.sml:

  • Translates functions for Dafny's AST.

dafny_compilerProgScript.sml:

  • Translates the Dafny to CakeML compiler.

dafny_sexpProgScript.sml:

  • Translates definitions to lex and parse S-expressions generated by Dafny.

dafny_to_cakemlProgScript.sml:

  • Translates definitions to convert Dafny's AST into CakeML's AST.

result_monadProgScript.sml:

  • Translates the definitions for Result monad.

sexp_to_dafnyProgScript.sml:

  • Translates definitions to generate Dafny's AST from S-expressions.