Project

General

Profile

Download (2.75 KB) Statistics
| Branch: | Tag: | Revision:
1
open Spec_types
2

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

    
6
let is_false = function False -> true | _ -> false
7

    
8
let expr_eq : type a b. (a, left_v) expression_t -> (a, b) expression_t -> bool
9
    =
10
 fun a b ->
11
  match a, b with
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
  | Equal (a, b) when expr_eq a b ->
21
    True
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')
56
  | Imply (a, b) ->
57
    let a' = red a in
58
    let b' = red b in
59
    if a' = b' || is_false a' || is_true b' then True
60
    else if is_true a' && is_false b' then False
61
    else Imply (a', b')
62
  | Exists (x, p) -> (
63
    let p' = red p in
64
    if is_true p' then True else match x with [] -> p' | x -> Exists (x, p'))
65
  | Forall (x, p) -> (
66
    let p' = red p in
67
    if is_true p' then True else match x with [] -> p' | x -> Forall (x, p'))
68
  | Ternary (x, a, b) ->
69
    let a' = red a in
70
    let b' = red b in
71
    Ternary (x, a', b')
72
  | f ->
73
    f
74

    
75
(* smart constructors *)
76
(* let mk_condition x l =
77
 *   if l = tag_true then Ternary (Val x, True, False)
78
 *   else if l = tag_false then Ternary (Val x, False, True)
79
 *   else Equal (Val x, Tag l) *)
80

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

    
83
let mk_pred_call pred = Predicate pred
84

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

    
88
let mk_transition ?(mems = Utils.ISet.empty) ?r ?i ?inst id inputs locals
89
    outputs =
90
  let tr =
91
    mk_pred_call
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)
115

    
116
let mk_branch_tr x 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)
(57-57/66)