Project

General

Profile

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