1

open Lustre_types

2


3

type register_t =

4

 ResetFlag

5

 StateVar of var_decl

6


7

type left_v

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.type_expr =

18

function

19

 Var v > v.var_type

20

 Memory ResetFlag > Type_predef.type_bool

21

 Memory (StateVar v) > v.var_type

22


23

type ('a, 'b) expressions_t = ('a, 'b) expression_t list

24


25

type 'a predicate_t =

26

 Transition: ident (* node name *)

27

* ident option (* instance *)

28

* int option (* transition index *)

29

* ('a, 'b) expressions_t (* inputs *)

30

* ('a, 'b) expressions_t (* locals *)

31

* ('a, 'b) expressions_t (* outputs *)

32

* bool (* reset *)

33

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

34

> 'a predicate_t

35

 Reset of ident * ident * 'a

36

 MemoryPack of ident * ident option * int option

37

 Initialization

38

 ResetCleared of ident

39


40

type 'a formula_t =

41

 True

42

 False

43

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

44

 And of 'a formula_t list

45

 Or of 'a formula_t list

46

 Imply of 'a formula_t * 'a formula_t

47

 Exists of var_decl list * 'a formula_t

48

 Forall of var_decl list * 'a formula_t

49

 Ternary: ('a, 'b) expression_t * 'a formula_t * 'a formula_t > 'a formula_t

50

 Predicate: 'a predicate_t > 'a formula_t

51

 StateVarPack of register_t

52

 ExistsMem of ident * 'a formula_t * 'a formula_t

53


54

(* type 'a simulation_t = {

55

* sname: node_desc;

56

* sindex: option int;

57

* sformula: 'a formula_t;

58

* } *)

59


60

type 'a memory_pack_t = {

61

mpname: node_desc;

62

mpindex: int option;

63

mpformula: 'a formula_t;

64

}

65


66

type 'a transition_t = {

67

tname: node_desc;

68

tindex: int option;

69

tinputs: var_decl list;

70

tlocals: var_decl list;

71

toutputs: var_decl list;

72

tformula: 'a formula_t;

73

tfootprint: Utils.ISet.t;

74

}

75

