Project

General

Profile

« Previous | Next » 

Revision 9e277169

Added by Lélio Brun 8 months ago

forgotten file

View differences:

src/spec_common.ml
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 rec red = function
14
  | Equal (a, b) when a = b ->
15
    True
16

  
17
  | And l ->
18
    let l' = List.filter_map (fun a ->
19
        let a' = red a in
20
        if is_true a' then None else Some a') l in
21
    begin match l' with
22
      | [] -> True
23
      | [a] -> a
24
      | l' when List.exists is_false l' -> False
25
      | _ -> And l'
26
    end
27

  
28
  | Or l ->
29
    let l' = List.filter_map (fun a ->
30
        let a' = red a in
31
        if is_false a' then None else Some a') l in
32
    begin match l' with
33
      | [] -> assert false
34
      | [a] -> a
35
      | l' when List.exists is_true l' -> True
36
      | _ -> Or l'
37
    end
38

  
39
  | Imply (a, b) ->
40
    let a' = red a in
41
    let b' = red b in
42
    if a' = b' || is_false a' || is_true b' then True
43
    else if is_true a' && is_false b' then False
44
    else Imply (a', b')
45

  
46
  | Exists (x, p) ->
47
    let p' = red p in
48
    if is_true p' then True else Exists (x, p')
49

  
50
  | Forall (x, p) ->
51
    let p' = red p in
52
    if is_true p' then True else Forall (x, p')
53

  
54
  | Ternary (x, a, b) ->
55
    let a' = red a in
56
    let b' = red b in
57
    Ternary (x, a', b')
58

  
59
  | f -> f
60

  
61
(* 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)
66

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

  
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

Also available in: Unified diff