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