Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/spec_common.ml
1 1
open Spec_types
2 2

  
3 3
(* a small reduction engine *)
4
let is_true = function
5
  | True -> true
6
  | _ -> false
4
let is_true = function True -> true | _ -> false
7 5

  
8
let is_false = function
9
  | False -> true
10
  | _ -> false
6
let is_false = function False -> true | _ -> false
11 7

  
12
let expr_eq: type a b. (a, left_v) expression_t -> (a, b) expression_t -> bool =
13
  fun a b ->
8
let expr_eq : type a b. (a, left_v) expression_t -> (a, b) expression_t -> bool
9
    =
10
 fun a b ->
14 11
  match a, b with
15
  | Var x, Var y -> x = y
16
  | Memory r1, Memory r2 -> r1 = r2
17
  | _ -> false
18

  
19
let rec red: type a. a formula_t -> a formula_t = function
12
  | Var x, Var y ->
13
    x = y
14
  | Memory r1, Memory r2 ->
15
    r1 = r2
16
  | _ ->
17
    false
18

  
19
let rec red : type a. a formula_t -> a formula_t = function
20 20
  | Equal (a, b) when expr_eq a b ->
21 21
    True
22

  
23
  | And l ->
24
    let l' = List.filter_map (fun a ->
25
        let a' = red a in
26
        if is_true a' then None else Some a') l in
27
    begin match l' with
28
      | [] -> True
29
      | [a] -> a
30
      | l' when List.exists is_false l' -> False
31
      | _ -> And l'
32
    end
33

  
34
  | Or l ->
35
    let l' = List.filter_map (fun a ->
36
        let a' = red a in
37
        if is_false a' then None else Some a') l in
38
    begin match l' with
39
      | [] -> assert false
40
      | [a] -> a
41
      | l' when List.exists is_true l' -> True
42
      | _ -> Or l'
43
    end
44

  
22
  | And l -> (
23
    let l' =
24
      List.filter_map
25
        (fun a ->
26
          let a' = red a in
27
          if is_true a' then None else Some a')
28
        l
29
    in
30
    match l' with
31
    | [] ->
32
      True
33
    | [ a ] ->
34
      a
35
    | l' when List.exists is_false l' ->
36
      False
37
    | _ ->
38
      And l')
39
  | Or l -> (
40
    let l' =
41
      List.filter_map
42
        (fun a ->
43
          let a' = red a in
44
          if is_false a' then None else Some a')
45
        l
46
    in
47
    match l' with
48
    | [] ->
49
      assert false
50
    | [ a ] ->
51
      a
52
    | l' when List.exists is_true l' ->
53
      True
54
    | _ ->
55
      Or l')
45 56
  | Imply (a, b) ->
46 57
    let a' = red a in
47 58
    let b' = red b in
48 59
    if a' = b' || is_false a' || is_true b' then True
49 60
    else if is_true a' && is_false b' then False
50 61
    else Imply (a', b')
51

  
52
  | Exists (x, p) ->
62
  | Exists (x, p) -> (
53 63
    let p' = red p in
54
    if is_true p' then True else begin match x with
55
      | [] -> p'
56
      | x -> Exists (x, p')
57
    end
58

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

  
67
    if is_true p' then True else match x with [] -> p' | x -> Forall (x, p'))
66 68
  | Ternary (x, a, b) ->
67 69
    let a' = red a in
68 70
    let b' = red b in
69 71
    Ternary (x, a', b')
70

  
71
  | f -> f
72
  | f ->
73
    f
72 74

  
73 75
(* smart constructors *)
74 76
(* let mk_condition x l =
......
78 80

  
79 81
let vals vs = List.map (fun v -> Val v) vs
80 82

  
81
let mk_pred_call pred =
82
  Predicate pred
83
let mk_pred_call pred = Predicate pred
83 84

  
84 85
(* let mk_clocked_on id =
85 86
 *   mk_pred_call (Clocked_on id) *)
86 87

  
87
let mk_transition ?(mems=Utils.ISet.empty) ?r ?i ?inst id inputs locals outputs =
88
let mk_transition ?(mems = Utils.ISet.empty) ?r ?i ?inst id inputs locals
89
    outputs =
88 90
  let tr =
89 91
    mk_pred_call
90
      (Transition (id, inst, i, vals inputs, vals locals, vals outputs,
91
                  (match r with Some _ -> true | None -> false), mems)) in
92
    (match r, inst with
93
     | Some r, Some inst ->
94
       ExistsMem (id, mk_pred_call (Reset (id, inst, r)), tr)
95
     | _ ->
96
       tr)
97

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

  
101
let mk_state_variable_pack x =
102
  StateVarPack (StateVar x)
103

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

  
107
let mk_conditional_tr v t f =
108
  Ternary (Val v, t, f)
92
      (Transition
93
         ( id,
94
           inst,
95
           i,
96
           vals inputs,
97
           vals locals,
98
           vals outputs,
99
           (match r with Some _ -> true | None -> false),
100
           mems ))
101
  in
102
  match r, inst with
103
  | Some r, Some inst ->
104
    ExistsMem (id, mk_pred_call (Reset (id, inst, r)), tr)
105
  | _ ->
106
    tr
107

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

  
110
let mk_state_variable_pack x = StateVarPack (StateVar x)
111

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

  
114
let mk_conditional_tr v t f = Ternary (Val v, t, f)
109 115

  
110 116
let mk_branch_tr x hl =
111 117
  And (List.map (fun (t, spec) -> Imply (Equal (Var x, Tag t), spec)) hl)
112 118

  
113
let mk_assign_tr x v =
114
  Equal (Var x, Val v)
115

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

Also available in: Unified diff