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' && is_false b' then False

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 id vars

83

=

84

let tr =

85

mk_pred_call

86

(Transition

87

( id,

88

inst,

89

i,

90

vals vars,

91

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

92

mems,

93

insts ))

94

in

95

match r, inst with

96

 Some r, Some inst >

97

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

98

 _ >

99

tr

100


101

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

102


103

let mk_state_variable_pack x = StateVarPack (StateVar x)

104


105

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

106


107

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

108


109

let mk_branch_tr x =

110

let open Lustre_types in

111

function

112

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

113

Ternary (Var x, spec1, spec2)

114

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

115

Ternary (Var x, spec2, spec1)

116

 hl >

117

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

118


119

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