Project

General

Profile

Download (6.27 KB) Statistics
| Branch: | Tag: | Revision:
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
(1-1/2)