Project

General

Profile

« Previous | Next » 

Revision 04396cc7

Added by Christophe Garion over 4 years ago

parser-json: add variables in parsing

View differences:

src/lustreSpec.ml
43 43

  
44 44
and clock_dec_desc =
45 45
  | Ckdec_any
46
  | Ckdec_bool of (ident * ident) list 
46
  | Ckdec_bool of (ident * ident) list
47 47

  
48 48

  
49 49
type constant =
50
  | Const_bool of bool
50 51
  | Const_int of int
51 52
  | Const_real of Num.num * int * string (* (a, b, c) means a * 10^-b. c is the original string *)
52 53
  | Const_array of constant list
......
56 57

  
57 58
type quantifier_type = Exists | Forall
58 59

  
59
type var_decl = 
60
type var_decl =
60 61
    {var_id: ident;
61 62
     var_orig:bool;
62 63
     var_dec_type: type_dec;
......
100 101
  | Expr_merge of ident * (label * expr) list
101 102
  | Expr_appl of call_t
102 103

  
103
and call_t = ident * expr * expr option 
104
and call_t = ident * expr * expr option
104 105
     (* The third part denotes the boolean condition for resetting *)
105 106

  
106 107
and eq =
......
134 135
| Index of Dimension.dim_expr
135 136
| Field of label
136 137

  
137
type assert_t = 
138
type assert_t =
138 139
    {
139 140
      assert_expr: expr;
140 141
      assert_loc: Location.t;
......
168 169
     node_locals: var_decl list;
169 170
     mutable node_gencalls: expr list;
170 171
     mutable node_checks: Dimension.dim_expr list;
171
     node_asserts: assert_t list; 
172
     node_asserts: assert_t list;
172 173
     node_stmts: statement list;
173 174
     mutable node_dec_stateless: bool;
174 175
     mutable node_stateless: bool option;
......
188 189
     nodei_in_lib: string list;
189 190
    }
190 191

  
191
type const_desc = 
192
    {const_id: ident; 
193
     const_loc: Location.t; 
194
     const_value: constant;      
192
type const_desc =
193
    {const_id: ident;
194
     const_loc: Location.t;
195
     const_value: constant;
195 196
     mutable const_type: Types.type_expr;
196 197
    }
197 198

  
......
199 200
| Node of node_desc
200 201
| Const of const_desc
201 202
| ImportedNode of imported_node_desc
202
| Open of bool * string (* the boolean set to true denotes a local 
203
| Open of bool * string (* the boolean set to true denotes a local
203 204
			   lusi vs a lusi installed at system level *)
204 205
| TypeDef of typedef_desc
205 206

  
......
211 212

  
212 213
type program = top_decl list
213 214

  
214
type dep_t = Dep of 
215
    bool 
215
type dep_t = Dep of
216
    bool
216 217
  * ident
217
  * (top_decl list) 
218
  * (top_decl list)
218 219
  * bool (* is stateful *)
219 220

  
220 221

  
221 222
(************ Machine code types *************)
222 223

  
223
type value_t = 
224
type value_t =
224 225
  {
225 226
    value_desc: value_t_desc;
226 227
    value_type: Types.type_expr;
......
230 231
  | Cst of constant
231 232
  | LocalVar of var_decl
232 233
  | StateVar of var_decl
233
  | Fun of ident * value_t list 
234
  | Fun of ident * value_t list
234 235
  | Array of value_t list
235 236
  | Access of value_t * value_t
236 237
  | Power of value_t * value_t
src/tools/stateflow/main_with_json.ml
23 23
  let json                       = Yojson.Basic.from_file "GPCA_Alarm_Alarm_SFIR_pp.json"
24 24
  let Program (init, defs, vars) = Parse.parse_prog json
25 25
  let prog                       = Parse.parse_prog json
26
  let user_vars                  = Parse.parse_variables json
26
  (* let user_vars                  = Parse.parse_variables json *)
27 27
  (*let _ = Format.printf "Model definitions@.%a@.####" Simulink.pp_src defs; ()*)
28 28
end
29 29

  
......
55 55
let main ()  =
56 56
  begin
57 57
    SF.pp_prog Format.std_formatter (Parse.parse_prog Prog.json);
58
    SF.pp_vars Format.std_formatter (Parse.parse_variables Prog.json);
58
    (* SF.pp_vars Format.std_formatter (Parse.parse_variables Prog.json); *)
59 59
  end
60 60

  
61 61
let _ = main ()
src/tools/stateflow/parser-json/parser_json.ml
1
open Yojson
2
open Datatype
3
(* open Simulink *)
4
(* open Transformer *)
5
open Basetypes
6
open Basic
7
open CPS
8

  
9
module type ParseExt =
10
sig
11
  val parse_condition : json -> Condition.t
12
  val parse_action : json -> Action.t
13
  val parse_event : json -> Basetypes.event_t
14
end
15

  
16
module Parser (Ext : ParseExt) =
17
struct
18
  let path_split = String.split_on_char '/'
19
  let path_concat = String.concat (String.make 1 '/')
20

  
21
  open Util
22

  
23
  let to_list json =
24
    try
25
      json |> to_list
26
    with
27
      Type_error _ -> [ json ]
28

  
29
  let rec parse_prog json : prog_t =
30
     (*Format.printf "parse_prog@.";*)
31
    Program (
32
      json |> member "name"        |> to_string,
33
     (json |> member "states"      |> to_list |> List.map parse_state) @
34
     (json |> member "junctions"   |> to_list |> List.map parse_junction)
35
     @
36
     (json |> member "sffunctions" |> to_list |> List.map
37
        (fun res -> SFFunction (parse_prog res))),
38
      [] (* TODO: to be replaced by variables ! *)
39
    )
40
  and parse_variables json =
41
     (*Format.printf "parse_variables@.";*)
42
    json |> member "data"       |> to_list |> List.map parse_variable
43
  and parse_state json =
44
    (*Format.printf "parse_state@.";*)
45
    State (
46
      json |> member "path" |> parse_path,
47
      json |> parse_state_def
48
    )
49
  and parse_path json =
50
      (*Format.printf "parse_path@.";*)
51
      json |> to_string |> path_split
52
  and parse_state_def json =
53
    (*Format.printf "parse_state_def@.";*)
54
    {
55
      state_actions        = json |> member "state_actions"        |> parse_state_actions;
56
      outer_trans          = json |> member "outer_trans"          |> to_list |> List.map parse_transition;
57
      inner_trans          = json |> member "inner_trans"          |> to_list |> List.map parse_transition;
58
      internal_composition = json |> member "internal_composition" |> parse_internal_composition
59
    }
60
  and parse_state_actions json =
61
    (*Format.printf "parse_state_actions@.";*)
62
    {
63
      entry_act  = json |> member "entry_act"  |> Ext.parse_action;
64
      during_act = json |> member "during_act" |> Ext.parse_action;
65
      exit_act   = json |> member "exit_act"   |> Ext.parse_action;
66
    }
67
  and parse_transition json =
68
    (*Format.printf "parse_transition@.";*)
69
    {
70
      event          = json |> member "event"          |> Ext.parse_event;
71
      condition      = json |> member "condition"      |> Ext.parse_condition;
72
      condition_act  = json |> member "condition_act"  |> Ext.parse_action;
73
      transition_act = json |> member "transition_act" |> Ext.parse_action;
74
      dest           = json |> member "dest"           |> parse_dest
75
    }
76
  and parse_dest json =
77
    (*Format.printf "parse_dest@.";*)
78
    (json |> member "type" |> to_string |>
79
	(function
80
	| "State"    -> (fun p -> DPath p)
81
	| "Junction" -> (fun j -> DJunction (path_concat j))
82
	| _ -> assert false))
83
      (json |> member "name" |> parse_path)
84
  and parse_internal_composition json =
85
    (*Format.printf "parse_internal_composition@.";*)
86
    (json |> member "type" |> to_string |>
87
	(function
88
	| "EXCLUSIVE_OR" -> (fun tinit substates ->                      Or  (tinit, substates))
89
	| "PARALLEL_AND" -> (fun tinit substates -> assert (tinit = []); And (substates))
90
	| _ -> assert false))
91
      (json |> member "tinit"     |> parse_tinit)
92
      (json |> member "substates" |> to_list |> List.map to_string)
93
  and parse_tinit json =
94
    (*Format.printf "parse_tinit@.";*)
95
    json |> to_list |> List.map parse_transition
96
  and parse_junction json =
97
    (*Format.printf "parse_junction@.";*)
98
    Junction (
99
      json |> member "path"        |> to_string,
100
      json |> member "outer_trans" |> to_list |> List.map parse_transition
101
    )
102
  and scope_of_string s =
103
    match s with
104
    | "Constant"  -> Constant
105
    | "Input"     -> Input
106
    | "Local"     -> Local
107
    | "Output"    -> Output
108
    | "Parameter" -> Parameter
109
    | _           -> failwith ("Invalid scope for variable: " ^ s)
110
  and datatype_of_json json =
111
    let datatype = json |> member "datatype" |> to_string in
112
    let init_value = json |> member "initial_value" |> to_string in
113
    match datatype with
114
    | "bool" -> Bool (bool_of_string init_value)
115
    | "int"  -> Int  (int_of_string init_value)
116
    | "real" -> Real (float_of_string init_value)
117
    | _      -> failwith ("Invalid datatype " ^ datatype
118
                          ^ " for variable " ^ (json |> member "name"
119
                                                |> to_string))
120
  and parse_variable json =
121
    (*Format.printf "parse_variables@.";*)
122
    (
123
      json |> member "name"          |> to_string,
124
      json |> member "scope"         |> to_string |> scope_of_string,
125
      json                           |> datatype_of_json
126
    )
127
end
1
open Yojson
2
open Datatype
3
(* open Simulink *)
4
(* open Transformer *)
5
open Basetypes
6
open Basic
7
open Corelang
8
open CPS
9
open LustreSpec
10

  
11
module type ParseExt =
12
sig
13
  val parse_condition : json -> Condition.t
14
  val parse_action : json -> Action.t
15
  val parse_event : json -> Basetypes.event_t
16
end
17

  
18
module Parser (Ext : ParseExt) =
19
struct
20
  let path_split = String.split_on_char '/'
21
  let path_concat = String.concat (String.make 1 '/')
22

  
23
  open Util
24

  
25
  let to_list json =
26
    try
27
      json |> to_list
28
    with
29
      Type_error _ -> [ json ]
30

  
31
  let rec parse_prog json : prog_t =
32
     (*Format.printf "parse_prog@.";*)
33
    Program (
34
      json |> member "name"        |> to_string,
35
     (json |> member "states"      |> to_list |> List.map parse_state) @
36
     (json |> member "junctions"   |> to_list |> List.map parse_junction)
37
     @
38
     (json |> member "sffunctions" |> to_list |> List.map
39
        (fun res -> SFFunction (parse_prog res))),
40
      json |> member "data"        |> to_list |> List.map parse_variable
41
    )
42
  (* and parse_variables json = *)
43
  (*    (\*Format.printf "parse_variables@.";*\) *)
44
  (*   json |> member "data"       |> to_list |> List.map parse_variable *)
45
  and parse_state json =
46
    (*Format.printf "parse_state@.";*)
47
    State (
48
      json |> member "path" |> parse_path,
49
      json |> parse_state_def
50
    )
51
  and parse_path json =
52
      (*Format.printf "parse_path@.";*)
53
      json |> to_string |> path_split
54
  and parse_state_def json =
55
    (*Format.printf "parse_state_def@.";*)
56
    {
57
      state_actions        = json |> member "state_actions"        |> parse_state_actions;
58
      outer_trans          = json |> member "outer_trans"          |> to_list |> List.map parse_transition;
59
      inner_trans          = json |> member "inner_trans"          |> to_list |> List.map parse_transition;
60
      internal_composition = json |> member "internal_composition" |> parse_internal_composition
61
    }
62
  and parse_state_actions json =
63
    (*Format.printf "parse_state_actions@.";*)
64
    {
65
      entry_act  = json |> member "entry_act"  |> Ext.parse_action;
66
      during_act = json |> member "during_act" |> Ext.parse_action;
67
      exit_act   = json |> member "exit_act"   |> Ext.parse_action;
68
    }
69
  and parse_transition json =
70
    (*Format.printf "parse_transition@.";*)
71
    {
72
      event          = json |> member "event"          |> Ext.parse_event;
73
      condition      = json |> member "condition"      |> Ext.parse_condition;
74
      condition_act  = json |> member "condition_act"  |> Ext.parse_action;
75
      transition_act = json |> member "transition_act" |> Ext.parse_action;
76
      dest           = json |> member "dest"           |> parse_dest
77
    }
78
  and parse_dest json =
79
    (*Format.printf "parse_dest@.";*)
80
    (json |> member "type" |> to_string |>
81
	(function
82
	| "State"    -> (fun p -> DPath p)
83
	| "Junction" -> (fun j -> DJunction (path_concat j))
84
	| _ -> assert false))
85
      (json |> member "name" |> parse_path)
86
  and parse_internal_composition json =
87
    (*Format.printf "parse_internal_composition@.";*)
88
    (json |> member "type" |> to_string |>
89
	(function
90
	| "EXCLUSIVE_OR" -> (fun tinit substates ->                      Or  (tinit, substates))
91
	| "PARALLEL_AND" -> (fun tinit substates -> assert (tinit = []); And (substates))
92
	| _ -> assert false))
93
      (json |> member "tinit"     |> parse_tinit)
94
      (json |> member "substates" |> to_list |> List.map to_string)
95
  and parse_tinit json =
96
    (*Format.printf "parse_tinit@.";*)
97
    json |> to_list |> List.map parse_transition
98
  and parse_junction json =
99
    (*Format.printf "parse_junction@.";*)
100
    Junction (
101
      json |> member "path"        |> to_string,
102
      json |> member "outer_trans" |> to_list |> List.map parse_transition
103
    )
104
  and scope_of_string s =
105
    match s with
106
    | "Constant"  -> Constant
107
    | "Input"     -> Input
108
    | "Local"     -> Local
109
    | "Output"    -> Output
110
    | "Parameter" -> Parameter
111
    | _           -> failwith ("Invalid scope for variable: " ^ s)
112
  and datatype_of_json json =
113
    let datatype = json |> member "datatype" |> to_string in
114
    let init_value = json |> member "initial_value" |> to_string in
115
    match datatype with
116
    | "bool" -> Bool (bool_of_string init_value)
117
    | "int"  -> Int  (int_of_string init_value)
118
    | "real" -> Real (float_of_string init_value)
119
    | _      -> failwith ("Invalid datatype " ^ datatype
120
                          ^ " for variable " ^ (json |> member "name"
121
                                                |> to_string))
122
  and lustre_datatype_of_json json location =
123
    let datatype      = json |> member "datatype"      |> to_string in
124
    let initial_value = json |> member "initial_value" |> to_string in
125
    match datatype with
126
    | "bool" -> (Tydec_bool, mkexpr location
127
                   (Expr_const (Const_bool
128
                                  (bool_of_string initial_value))))
129
    | "int"  -> (Tydec_int, mkexpr location
130
                   (Expr_const (Const_int (int_of_string
131
                                             initial_value))))
132
    | "real" -> (Tydec_real, mkexpr location
133
                   (Expr_const (Const_real (Num.num_of_int 0,
134
                                           0,
135
                                           initial_value))))
136
    | _      -> failwith ("Invalid datatype " ^ datatype
137
                          ^ " for variable " ^ (json |> member "name"
138
                                                |> to_string))
139
  and parse_variable json =
140
    (*Format.printf "parse_variable@.";*)
141
    let location                  = Location.dummy_loc in
142
    let (datatype, initial_value) = lustre_datatype_of_json json location in
143
    mkvar_decl location ~orig:true
144
      ( json |> member "name" |> to_string,
145
        {ty_dec_desc = datatype;  ty_dec_loc = location},
146
        {ck_dec_desc = Ckdec_any; ck_dec_loc = location},
147
        false,
148
        Some initial_value
149
      )
150
end

Also available in: Unified diff