Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / parser-json / parser_json.ml @ bbfbc15a

History | View | Annotate | Download (6.06 KB)

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
open Str
11

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

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

    
24
  open Util
25

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

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