Project

General

Profile

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

    
2
open Lustrec 
3

    
4
let sf_level = 2
5

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

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

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

    
34
(* Action and Condition types and functions. *)
35

    
36
(* Actions are defined by string + the opening and closing of states *)
37

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

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

    
43
type frontier_t =
44
  | Loose
45
  | Strict
46

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

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

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

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

    
74
  val pp_act : Format.formatter -> t -> unit
75
end
76

    
77

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

    
87

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

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

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

    
110
let _ = (module Action : ActionType)
111

    
112

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

    
125
  val pp_cond : Format.formatter -> t -> unit
126
end
127
  
128
module Condition =
129
struct
130
  type t =
131
    | Quote of base_condition_t
132
    | Active of path_t
133
    | Event of event_base_t
134
    | And of t * t
135
    | Neg of t
136
    | True
137

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

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

    
157
end
158

    
159
let _ = (module Condition : ConditionType)
160

    
161
module GlobalVarDef =
162
struct
163
  type t = {variable: Lustre_types.var_decl; init_val: Lustre_types.expr}
164
end
(3-3/4)