Project

General

Profile

Download (2.82 KB) Statistics
| Branch: | Tag: | Revision:
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
83
    inputs locals outputs =
84
  let tr =
85
    mk_pred_call
86
      (Transition
87
         ( id,
88
           inst,
89
           i,
90
           vals inputs,
91
           vals locals,
92
           vals outputs,
93
           (match r with Some _ -> true | None -> false),
94
           mems,
95
           insts ))
96
  in
97
  match r, inst with
98
  | Some r, Some inst ->
99
    ExistsMem (id, mk_pred_call (Reset (id, inst, r)), tr)
100
  | _ ->
101
    tr
102

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

    
105
let mk_state_variable_pack x = StateVarPack (StateVar x)
106

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

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

    
111
let mk_branch_tr x =
112
  let open Lustre_types in
113
  function
114
  | [ (h1, spec1); (h2, spec2) ] when h1 = tag_true && h2 = tag_false ->
115
    Ternary (Var x, spec1, spec2)
116
  | [ (h1, spec1); (h2, spec2) ] when h1 = tag_false && h2 = tag_true ->
117
    Ternary (Var x, spec2, spec1)
118
  | hl ->
119
    And (List.map (fun (t, spec) -> Imply (Equal (Var x, Tag t), spec)) hl)
120

    
121
let mk_assign_tr x v = Equal (Var x, Val v)
(57-57/66)