1

open Spec_types

2

open Utils

3


4

(* a small reduction engine *)

5

let is_true = function True > true  _ > false

6


7

let is_false = function False > true  _ > false

8


9

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

10

=

11

fun a b >

12

match a, b with

13

 Var x, Var y >

14

x = y

15

 Memory r1, Memory r2 >

16

r1 = r2

17

 _ >

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

 And l > (

24

let l' =

25

List.filter_map

26

(fun a >

27

let a' = red a in

28

if is_true a' then None else Some a')

29

l

30

in

31

match l' with

32

 [] >

33

True

34

 [ a ] >

35

a

36

 l' when List.exists is_false l' >

37

False

38

 _ >

39

And l')

40

 Or l > (

41

let l' =

42

List.filter_map

43

(fun a >

44

let a' = red a in

45

if is_false a' then None else Some a')

46

l

47

in

48

match l' with

49

 [] >

50

assert false

51

 [ a ] >

52

a

53

 l' when List.exists is_true l' >

54

True

55

 _ >

56

Or l')

57

 Imply (a, b) >

58

let a' = red a in

59

let b' = red b in

60

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

61

else if is_true a' then b'

62

else Imply (a', b')

63

 Exists (x, p) > (

64

let p' = red p in

65

if is_true p' then True else match x with [] > p'  x > Exists (x, p'))

66

 Forall (x, p) > (

67

let p' = red p in

68

if is_true p' then True else match x with [] > p'  x > Forall (x, p'))

69

 Ternary (x, a, b) >

70

let a' = red a in

71

let b' = red b in

72

Ternary (x, a', b')

73

 f >

74

f

75


76

(* smart constructors *)

77


78

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

79


80

let mk_pred_call pred = Predicate pred

81


82

let mk_transition ?(mems = ISet.empty) ?(insts = IMap.empty) ?r ?i ?inst

83

stateless id vars =

84

let tr =

85

mk_pred_call

86

(Transition

87

( stateless,

88

id,

89

inst,

90

i,

91

vals vars,

92

(match r with Some _ > true  None > false),

93

mems,

94

insts ))

95

in

96

match r, inst with

97

 Some r, Some inst >

98

ExistsMem (id, mk_pred_call (Reset (id, inst, r)), tr)

99

 _ >

100

tr

101


102

let mk_memory_pack ?i ?inst id = mk_pred_call (MemoryPack (id, inst, i))

103


104

let mk_state_variable_pack x = StateVarPack (StateVar x)

105


106

let mk_state_assign_tr x v = Equal (Memory (StateVar x), Val v)

107


108

let mk_conditional_tr v t f = Ternary (Val v, t, f)

109


110

let mk_branch_tr x =

111

let open Lustre_types in

112

function

113

 [ (h1, spec1); (h2, spec2) ] when h1 = tag_true && h2 = tag_false >

114

Ternary (Var x, spec1, spec2)

115

 [ (h1, spec1); (h2, spec2) ] when h1 = tag_false && h2 = tag_true >

116

Ternary (Var x, spec2, spec1)

117

 hl >

118

let n = List.length hl in

119

And (List.mapi (fun k (t, spec) >

120

let c = if k = n  1 then GEqual (Var x, Tag t) else Equal (Var x, Tag t) in

121

Imply (c, spec)) hl)

122


123

let mk_assign_tr x v = Equal (Var x, Val v)
