Project

General

Profile

Download (2.45 KB) Statistics
| Branch: | Tag: | Revision:
1
open Lustre_types
2
open Spec_types
3

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

    
9
let is_false = function
10
  | False -> true
11
  | _ -> false
12

    
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 ->
22
    True
23

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

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

    
46
  | Imply (a, b) ->
47
    let a' = red a in
48
    let b' = red b in
49
    if a' = b' || is_false a' || is_true b' then True
50
    else if is_true a' && is_false b' then False
51
    else Imply (a', b')
52

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

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

    
67
  | Ternary (x, a, b) ->
68
    let a' = red a in
69
    let b' = red b in
70
    Ternary (x, a', b')
71

    
72
  | f -> f
73

    
74
(* smart constructors *)
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) *)
79

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

    
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

    
(57-57/66)