|
1
|
open Utils
|
|
2
|
open Lustre_types
|
|
3
|
open Spec_types
|
|
4
|
|
|
5
|
val type_of_value : Machine_code_types.value_t expression_t -> Types.t
|
|
6
|
|
|
7
|
val mk_conditional_tr : 'a -> 'a formula_t -> 'a formula_t -> 'a formula_t
|
|
8
|
|
|
9
|
val mk_branch_tr : var_decl -> (ident * 'a formula_t) list -> 'a formula_t
|
|
10
|
|
|
11
|
val mk_assign_tr : var_decl -> 'a -> 'a formula_t
|
|
12
|
|
|
13
|
val mk_memory_pack : ?i:int -> ?inst:ident -> ident -> 'a formula_t
|
|
14
|
|
|
15
|
val mk_transition :
|
|
16
|
?mems:ISet.t ->
|
|
17
|
?insts:ident IMap.t ->
|
|
18
|
?r:'a ->
|
|
19
|
?i:int ->
|
|
20
|
?inst:ident ->
|
|
21
|
bool ->
|
|
22
|
ident ->
|
|
23
|
'a list ->
|
|
24
|
'a formula_t
|
|
25
|
|
|
26
|
val mk_state_variable_pack : var_decl -> 'a formula_t
|
|
27
|
|
|
28
|
val mk_state_assign_tr : var_decl -> 'a -> 'a formula_t
|
|
29
|
|
|
30
|
val red : 'a formula_t -> 'a formula_t
|