cakeml/cv_translator/eval_cake_compileLib.sig at master · CakeML/cakeml · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

signature eval_cake_compileLib =
sig

  include Abbrev

  type arch_thms =
    { default_config_def       : thm
    , to_livesets_def          : thm
    , compile_cake_def         : thm
    , compile_cake_imp         : thm
    , compile_cake_explore_def : thm
    , cv_export_def            : thm }

  type comp_input =
    { prefix               : string
    , conf_def             : thm
    , prog_def             : thm
    , run_as_explorer      : bool
    , output_filename      : string
    , output_conf_filename : string option }

  val eval_cake_compile :
    arch_thms -> string -> thm -> string -> thm

  val eval_cake_compile_explore :
    arch_thms -> string -> thm -> string -> thm

  val eval_cake_compile_with_conf :
    arch_thms -> string -> thm -> thm -> string -> thm

  val eval_cake_compile_explore_with_conf:
    arch_thms -> string -> thm -> thm -> string -> thm

  val eval_cake_compile_general :
    arch_thms -> comp_input -> thm

end