Project

General

Profile

Download (4.56 KB) Statistics
| Branch: | Tag: | Revision:
1

    
2
let sf_level = 2
3

    
4
(* Basic datatype for model elements: state and junction name, events ... *)
5
type state_name_t         = string
6
type junction_name_t      = string
7
type path_t               = state_name_t list
8
type event_base_t         = string
9
type event_t              = event_base_t option
10
type user_variable_name_t = string
11

    
12
(* Connected to lustrec types *)
13
type base_action_t    = { defs : LustreSpec.statement list;
14
			  ainputs: LustreSpec.var_decl list;
15
			  aoutputs: LustreSpec.var_decl list;
16
			  avariables: LustreSpec.var_decl list;
17
			  (* ident: string; *)
18
			}
19
type base_condition_t = { expr: LustreSpec.expr;
20
			  cinputs: LustreSpec.var_decl list;
21
			  coutputs: LustreSpec.var_decl list;
22
			  cvariables: LustreSpec.var_decl list }
23

    
24
(* P(r)etty printers *)
25
let pp_state_name     = Format.pp_print_string
26
let pp_junction_name  = Format.pp_print_string
27
let pp_path fmt p     = Utils.fprintf_list ~sep:"." pp_state_name fmt p
28
let pp_event fmt e    = match e with None -> Format.fprintf fmt "none" | Some s -> Format.fprintf fmt "%s" s
29
let pp_base_act fmt a = Printers.pp_node_stmts fmt a.defs
30
let pp_base_cond fmt c= Printers.pp_expr fmt c.expr
31

    
32
(* Action and Condition types and functions. *)
33

    
34
(* Actions are defined by string + the opening and closing of states *)
35

    
36
(* This version is slightly more complex than the one of EMSOFT'05 to enable the
37
   use of function calls in action.
38

    
39
   TODO: these rich call type could be externalized and a functor introduced. *)
40

    
41
type frontier_t =
42
  | Loose
43
  | Strict
44

    
45
let pp_frontier fmt frontier =
46
  match frontier with
47
  | Loose  -> Format.fprintf fmt "Loose"
48
  | Strict -> Format.fprintf fmt "Strict"
49

    
50
type _ call_t =
51
  | Ecall : (path_t * path_t * frontier_t) call_t
52
  | Dcall : path_t call_t
53
  | Xcall : (path_t * frontier_t) call_t
54

    
55
let pp_call :
56
type a. Format.formatter -> a call_t -> unit =
57
  fun fmt call ->
58
    match call with
59
    | Ecall -> Format.fprintf fmt "CallE"
60
    | Dcall -> Format.fprintf fmt "CallD"
61
    | Xcall -> Format.fprintf fmt "CallX"
62

    
63
module type ActionType =
64
sig
65
  type t
66
  val nil : t
67
  val aquote : base_action_t -> t
68
  val open_path : path_t -> t
69
  val close_path : path_t -> t
70
  val call : 'c call_t -> 'c -> t
71

    
72
  val pp_act : Format.formatter -> t -> unit
73
end
74

    
75

    
76
module Action =
77
struct
78
  type t =
79
    | Quote : base_action_t -> t
80
    | Close : path_t -> t
81
    | Open  : path_t -> t
82
    | Call  : 'c call_t * 'c -> t
83
    | Nil   : t
84

    
85

    
86
  let nil = Nil
87
  let aquote act = Quote act
88
  let open_path p = Open p
89
  let close_path p = Close p
90
  let call c a = Call (c, a)
91

    
92
  let pp_call : type c. Format.formatter -> c call_t -> c -> unit =
93
    fun fmt call ->
94
    match call with
95
    | Ecall -> (fun (p, p', f) -> Format.fprintf fmt "%a(%a, %a, %a)" pp_call call pp_path p pp_path p' pp_frontier f)
96
    | Dcall -> (fun p          -> Format.fprintf fmt "%a(%a)" pp_call call pp_path p)
97
    | Xcall -> (fun (p, f)     -> Format.fprintf fmt "%a(%a, %a)" pp_call call pp_path p pp_frontier f)
98

    
99
  let pp_act fmt act =
100
    match act with
101
    | Call (c, a)      -> pp_call fmt c a
102
    | Quote a          -> Format.fprintf fmt "%a" pp_base_act a
103
    | Close p          -> Format.fprintf fmt "Close(%a)" pp_path p
104
    | Open p           -> Format.fprintf fmt "Open(%a)" pp_path p
105
    | Nil              -> Format.fprintf fmt "Nil"
106
end
107

    
108
let _ = (module Action : ActionType)
109

    
110

    
111
(* Conditions are either (1) simple strings, (2) the active status of a state or
112
   (3) occurence of an event. They can be combined (conjunction, negation) *)
113
module type ConditionType =
114
sig
115
  type t
116
  val cquote : base_condition_t -> t
117
  val tru : t
118
  val active : path_t -> t
119
  val event : event_t -> t
120
  val ( && ) : t -> t -> t
121
  val neg : t -> t
122

    
123
  val pp_cond : Format.formatter -> t -> unit
124
end
125

    
126
  module Condition =
127
struct
128
  type t =
129
    | Quote of base_condition_t
130
    | Active of path_t
131
    | Event of event_base_t
132
    | And of t * t
133
    | Neg of t
134
    | True
135

    
136
  let cquote cond = Quote cond
137
  let tru = True
138
  let neg cond = Neg cond
139
  let ( && ) cond1 cond2 = And (cond1, cond2)
140
  let active path = Active path
141
  let event evt =
142
    match evt with
143
    | None   -> True
144
    | Some e -> Event e
145

    
146
  let rec pp_cond fmt cond =
147
    match cond with
148
    | True               -> Format.fprintf fmt "true"
149
    | Active p           -> Format.fprintf fmt "Active(%a)" pp_path p
150
    | Event e            -> Format.fprintf fmt "Event(%s)" e
151
    | Neg cond           -> Format.fprintf fmt "(neg %a)" pp_cond cond
152
    | And (cond1, cond2) -> Format.fprintf fmt "%a /\\ %a" pp_cond cond1 pp_cond cond2
153
    | Quote c            -> Format.fprintf fmt "%a" pp_base_cond c
154

    
155
end
156

    
157
let _ = (module Condition : ConditionType)
(2-2/3)