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
|