|
1
|
open Utils
|
|
2
|
open Format
|
|
3
|
open Lustre_types
|
|
4
|
open Machine_code_types
|
|
5
|
|
|
6
|
module type MODIFIERS_MAINSRC = sig
|
|
7
|
val pp_declare_ghost_state : formatter -> ident -> unit
|
|
8
|
|
|
9
|
val pp_ghost_state_parameter : formatter -> unit -> unit
|
|
10
|
|
|
11
|
val pp_main_spec : formatter -> unit
|
|
12
|
|
|
13
|
val pp_main_loop_invariants :
|
|
14
|
ident -> machine_t list -> formatter -> machine_t -> unit
|
|
15
|
end
|
|
16
|
|
|
17
|
module EmptyMod : MODIFIERS_MAINSRC
|
|
18
|
|
|
19
|
module Main (Mod : MODIFIERS_MAINSRC) : sig
|
|
20
|
val pp_main_c :
|
|
21
|
formatter ->
|
|
22
|
machine_t ->
|
|
23
|
string ->
|
|
24
|
program_t ->
|
|
25
|
machine_t list ->
|
|
26
|
dep_t list ->
|
|
27
|
unit
|
|
28
|
end
|