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_bool
|
134
|
(bool_of_string initial_value))))
|
135
|
| "int" -> (Tydec_int, mkexpr location
|
136
|
(Expr_const (Const_int (int_of_string
|
137
|
initial_value))))
|
138
|
| "real" -> (Tydec_real, mkexpr location
|
139
|
(Expr_const (parse_real_value initial_value)))
|
140
|
| _ -> failwith ("Invalid datatype " ^ datatype
|
141
|
^ " for variable " ^ (json |> member "name"
|
142
|
|> to_string))
|
143
|
and parse_variable json =
|
144
|
(*Format.printf "parse_variable@.";*)
|
145
|
let location = Location.dummy_loc in
|
146
|
let (datatype, initial_value) = lustre_datatype_of_json json location in
|
147
|
mkvar_decl location ~orig:true
|
148
|
( json |> member "name" |> to_string,
|
149
|
{ty_dec_desc = datatype; ty_dec_loc = location},
|
150
|
{ck_dec_desc = Ckdec_any; ck_dec_loc = location},
|
151
|
true,
|
152
|
Some initial_value
|
153
|
)
|
154
|
end
|