1

open Lustre_types

2

open Spec_types

3


4

(* a small reduction engine *)

5

let is_true = function

6

 True > true

7

 _ > false

8


9

let is_false = function

10

 False > true

11

 _ > false

12


13

let expr_eq: type a b. (a, left_v) expression_t > (a, b) expression_t > bool =

14

fun a b >

15

match a, b with

16

 Var x, Var y > x = y

17

 Memory r1, Memory r2 > r1 = r2

18

 _ > false

19


20

let rec red: type a. a formula_t > a formula_t = function

21

 Equal (a, b) when expr_eq a b >

22

True

23


24

 And l >

25

let l' = List.filter_map (fun a >

26

let a' = red a in

27

if is_true a' then None else Some a') l in

28

begin match l' with

29

 [] > True

30

 [a] > a

31

 l' when List.exists is_false l' > False

32

 _ > And l'

33

end

34


35

 Or l >

36

let l' = List.filter_map (fun a >

37

let a' = red a in

38

if is_false a' then None else Some a') l in

39

begin match l' with

40

 [] > assert false

41

 [a] > a

42

 l' when List.exists is_true l' > True

43

 _ > Or l'

44

end

45


46

 Imply (a, b) >

47

let a' = red a in

48

let b' = red b in

49

if a' = b'  is_false a'  is_true b' then True

50

else if is_true a' && is_false b' then False

51

else Imply (a', b')

52


53

 Exists (x, p) >

54

let p' = red p in

55

if is_true p' then True else begin match x with

56

 [] > p'

57

 x > Exists (x, p')

58

end

59


60

 Forall (x, p) >

61

let p' = red p in

62

if is_true p' then True else begin match x with

63

 [] > p'

64

 x > Forall (x, p')

65

end

66


67

 Ternary (x, a, b) >

68

let a' = red a in

69

let b' = red b in

70

Ternary (x, a', b')

71


72

 f > f

73


74

(* smart constructors *)

75

(* let mk_condition x l =

76

* if l = tag_true then Ternary (Val x, True, False)

77

* else if l = tag_false then Ternary (Val x, False, True)

78

* else Equal (Val x, Tag l) *)

79


80

let vals vs = List.map (fun v > Val v) vs

81


82

let mk_pred_call pred =

83

Predicate pred

84


85

(* let mk_clocked_on id =

86

* mk_pred_call (Clocked_on id) *)

87


88

let mk_transition ?i ?inst id inputs locals outputs =

89

mk_pred_call

90

(Transition (id, inst, i, vals inputs, vals locals, vals outputs))

91


92

let mk_memory_pack ?i ?inst id =

93

mk_pred_call (MemoryPack (id, inst, i))

94


95

let mk_state_variable_pack x =

96

StateVarPack (StateVar x)

97


98

let mk_state_assign_tr x v =

99

Equal (Memory (StateVar x), Val v)

100


101

let mk_conditional_tr v t f =

102

Ternary (Val v, t, f)

103


104

let mk_branch_tr x hl =

105

And (List.map (fun (t, spec) > Imply (Equal (Var x, Tag t), spec)) hl)

106


107

let mk_assign_tr x v =

108

Equal (Var x, Val v)

109

