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 * ident option * int option

27

* ('a, 'b) expressions_t

28

* ('a, 'b) expressions_t

29

* ('a, 'b) expressions_t > 'a predicate_t

30

 MemoryPack of ident * ident option * int option

31

 Initialization

32

 ResetCleared of ident

33


34

type 'a formula_t =

35

 True

36

 False

37

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

38

 And of 'a formula_t list

39

 Or of 'a formula_t list

40

 Imply of 'a formula_t * 'a formula_t

41

 Exists of var_decl list * 'a formula_t

42

 Forall of var_decl list * 'a formula_t

43

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

44

 Predicate: 'a predicate_t > 'a formula_t

45

 StateVarPack of register_t

46

 ExistsMem of 'a formula_t * 'a formula_t

47


48

(* type 'a simulation_t = {

49

* sname: node_desc;

50

* sindex: option int;

51

* sformula: 'a formula_t;

52

* } *)

53


54

type 'a memory_pack_t = {

55

mpname: node_desc;

56

mpindex: int option;

57

mpformula: 'a formula_t;

58

}

59


60

type 'a transition_t = {

61

tname: node_desc;

62

tindex: int option;

63

tinputs: var_decl list;

64

tlocals: var_decl list;

65

toutputs: var_decl list;

66

tformula: 'a formula_t;

67

}

68

