### Profile

« Previous | Next »

## Revision 6d1693b9

#### Added by Lélio Brun 7 months ago

work on spec generation almost done

View differences:

src/spec_common.ml
10 10
```  | False -> true
```
11 11
```  | _ -> false
```
12 12

13
```let rec red = function
```
14
```  | Equal (a, b) when a = b ->
```
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 ->
```
15 22
```    True
```
16 23

17 24
```  | And l ->
```
......
45 52

46 53
```  | Exists (x, p) ->
```
47 54
```    let p' = red p in
```
48
```    if is_true p' then True else Exists (x, p')
```
55
```    if is_true p' then True else begin match x with
```
56
```      | [] -> p'
```
57
```      | x -> Exists (x, p')
```
58
```    end
```
49 59

50 60
```  | Forall (x, p) ->
```
51 61
```    let p' = red p in
```
52
```    if is_true p' then True else Forall (x, p')
```
62
```    if is_true p' then True else begin match x with
```
63
```      | [] -> p'
```
64
```      | x -> Forall (x, p')
```
65
```    end
```
53 66

54 67
```  | Ternary (x, a, b) ->
```
55 68
```    let a' = red a in
```
......
59 72
```  | f -> f
```
60 73

61 74
```(* smart constructors *)
```
62
```let mk_condition x l =
```
63
```  if l = tag_true then Ternary (Val x, True, False)
```
64
```  else if l = tag_false then Ternary (Val x, False, True)
```
65
```  else Equal (Val x, Tag l)
```
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) *)
```
66 79

67 80
```let vals vs = List.map (fun v -> Val v) vs
```
68 81

69
```let mk_pred_call pred vars =
```
70
```  Predicate (pred, vals vars)
```
71

72
```let mk_clocked_on id =
```
73
```  mk_pred_call (Clocked_on id)
```
74

75
```let mk_transition ?i id =
```
76
```  mk_pred_call (Transition (id, i))
```
77

78
```module type SPECVALUE = sig
```
79
```  type t
```
80
```  type ctx
```
81
```  val pp_val: ctx -> Format.formatter -> t -> unit
```
82
```end
```
83

84
```module PrintSpec(SV: SPECVALUE) = struct
```
85

86
```  open Utils.Format
```
87

88
```  let pp_state fmt = function
```
89
```    | In -> pp_print_string fmt "IN"
```
90
```    | Out -> pp_print_string fmt "OUT"
```
91

92
```  let pp_expr ctx fmt = function
```
93
```    | Val v -> SV.pp_val ctx fmt v
```
94
```    | Tag t -> pp_print_string fmt t
```
95
```    | Var v -> pp_print_string fmt v.var_id
```
96
```    | Instance (s, i) -> fprintf fmt "%a:%a" pp_state s pp_print_string i
```
97
```    | Memory (s, i) -> fprintf fmt "%a:%a" pp_state s pp_print_string i
```
98

99
```  let pp_predicate fmt = function
```
100
```    | Clocked_on x -> fprintf fmt "On<%a>" pp_print_string x
```
101
```    | Transition (f, i) ->
```
102
```      fprintf fmt "Transition<%a>%a"
```
103
```        pp_print_string f
```
104
```        (pp_print_option pp_print_int) i
```
105
```    | Initialization -> ()
```
106

107
```  let pp_spec ctx =
```
108
```    let pp_expr = pp_expr ctx in
```
109
```    let rec pp_spec fmt f =
```
110
```      match f with
```
111
```      | True -> pp_print_string fmt "true"
```
112
```      | False -> pp_print_string fmt "false"
```
113
```      | Equal (a, b) ->
```
114
```        fprintf fmt "%a == %a" pp_expr a pp_expr b
```
115
```      | And fs ->
```
116
```        pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "/\\") pp_spec fmt fs
```
117
```      | Or fs ->
```
118
```        pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "\\/") pp_spec fmt fs
```
119
```      | Imply (a, b) ->
```
120
```        fprintf fmt "%a -> %a" pp_spec a pp_spec b
```
121
```      | Exists (xs, a) ->
```
122
```        fprintf fmt "∃%a, %a" (pp_print_list Printers.pp_var) xs pp_spec a
```
123
```      | Forall (xs, a) ->
```
124
```        fprintf fmt "∀%a, %a" (pp_print_list Printers.pp_var) xs pp_spec a
```
125
```      | Ternary (e, a, b) ->
```
126
```        fprintf fmt "If %a Then %a Else %a" pp_expr e pp_spec a pp_spec b
```
127
```      | Predicate (p, es) ->
```
128
```        fprintf fmt "%a%a" pp_predicate p (pp_print_parenthesized pp_expr) es
```
129
```    in
```
130
```    pp_spec
```
131

132
```end
```
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

Also available in: Unified diff