1

open Utils

2

open Lustre_types

3


4

type register_t = ResetFlag  StateVar of var_decl

5


6

type left_v

7


8

type right_v

9


10

type ('a, _) expression_t =

11

 Val : 'a > ('a, right_v) expression_t

12

 Tag : ident > ('a, right_v) expression_t

13

 Var : var_decl > ('a, left_v) expression_t

14

 Memory : register_t > ('a, left_v) expression_t

15


16

(** TODO: why moving this elsewhere makes the exhaustiveness check fail? *)

17

let type_of_l_value : type a. (a, left_v) expression_t > Types.t = function

18

 Var v >

19

v.var_type

20

 Memory ResetFlag >

21

Type_predef.type_bool

22

 Memory (StateVar v) >

23

v.var_type

24


25

type 'a predicate_t =

26

 Transition :

27

bool (* stateless *)

28

* ident (* node name *)

29

* ident option

30

(* instance *)

31

* int option

32

(* transition index *)

33

* ('a, 'b) expression_t list

34

(* variables *)

35

* bool (* reset *)

36

* Utils.ISet.t (* memory footprint *)

37

* ident Utils.IMap.t

38

(* memory instances footprint *)

39

> 'a predicate_t

40

 Reset of ident * ident * 'a

41

 MemoryPack of ident * ident option * int option

42

 Initialization

43

 ResetCleared of ident

44


45

type 'a formula_t =

46

 True

47

 False

48

 Equal : ('a, left_v) expression_t * ('a, 'b) expression_t > 'a formula_t

49

 GEqual : ('a, left_v) expression_t * ('a, 'b) expression_t > 'a formula_t

50

 And of 'a formula_t list

51

 Or of 'a formula_t list

52

 Imply of 'a formula_t * 'a formula_t

53

 Exists of var_decl list * 'a formula_t

54

 Forall of var_decl list * 'a formula_t

55

 Ternary :

56

('a, 'b) expression_t * 'a formula_t * 'a formula_t

57

> 'a formula_t

58

 Predicate : 'a predicate_t > 'a formula_t

59

 StateVarPack of register_t

60

 ExistsMem of ident * 'a formula_t * 'a formula_t

61

 Value of 'a

62


63

(* type 'a simulation_t = {

64

* sname: node_desc;

65

* sindex: option int;

66

* sformula: 'a formula_t;

67

* } *)

68


69

type 'a memory_pack_t = {

70

mpname : node_desc;

71

mpindex : int option;

72

mpformula : 'a formula_t;

73

}

74


75

type 'a transition_t = {

76

tname : node_desc;

77

tindex : int option;

78

tvars : var_decl list;

79

tformula : 'a formula_t;

80

tmem_footprint : Utils.ISet.t;

81

tinst_footprint : ident Utils.IMap.t;

82

}
