From 04396cc7fee4e5c5c5154fef675f21bf6622672f Mon Sep 17 00:00:00 2001
From: Christophe Garion <tofgarion@runbox.com>
Date: Mon, 2 Oct 2017 17:55:24 +0200
Subject: [PATCH] parser-json: add variables in parsing
---
src/lustreSpec.ml | 31 +-
src/tools/stateflow/main_with_json.ml | 4 +-
.../stateflow/parser-json/parser_json.ml | 277 ++++++++++--------
3 files changed, 168 insertions(+), 144 deletions(-)
diff --git a/src/lustreSpec.ml b/src/lustreSpec.ml
index 3051b4d0..096fe9fc 100644
--- a/src/lustreSpec.ml
+++ b/src/lustreSpec.ml
@@ -43,10 +43,11 @@ type clock_dec =
and clock_dec_desc =
| Ckdec_any
- | Ckdec_bool of (ident * ident) list
+ | Ckdec_bool of (ident * ident) list
type constant =
+ | Const_bool of bool
| Const_int of int
| Const_real of Num.num * int * string (* (a, b, c) means a * 10^-b. c is the original string *)
| Const_array of constant list
@@ -56,7 +57,7 @@ type constant =
type quantifier_type = Exists | Forall
-type var_decl =
+type var_decl =
{var_id: ident;
var_orig:bool;
var_dec_type: type_dec;
@@ -100,7 +101,7 @@ and expr_desc =
| Expr_merge of ident * (label * expr) list
| Expr_appl of call_t
-and call_t = ident * expr * expr option
+and call_t = ident * expr * expr option
(* The third part denotes the boolean condition for resetting *)
and eq =
@@ -134,7 +135,7 @@ type offset =
| Index of Dimension.dim_expr
| Field of label
-type assert_t =
+type assert_t =
{
assert_expr: expr;
assert_loc: Location.t;
@@ -168,7 +169,7 @@ type node_desc =
node_locals: var_decl list;
mutable node_gencalls: expr list;
mutable node_checks: Dimension.dim_expr list;
- node_asserts: assert_t list;
+ node_asserts: assert_t list;
node_stmts: statement list;
mutable node_dec_stateless: bool;
mutable node_stateless: bool option;
@@ -188,10 +189,10 @@ type imported_node_desc =
nodei_in_lib: string list;
}
-type const_desc =
- {const_id: ident;
- const_loc: Location.t;
- const_value: constant;
+type const_desc =
+ {const_id: ident;
+ const_loc: Location.t;
+ const_value: constant;
mutable const_type: Types.type_expr;
}
@@ -199,7 +200,7 @@ type top_decl_desc =
| Node of node_desc
| Const of const_desc
| ImportedNode of imported_node_desc
-| Open of bool * string (* the boolean set to true denotes a local
+| Open of bool * string (* the boolean set to true denotes a local
lusi vs a lusi installed at system level *)
| TypeDef of typedef_desc
@@ -211,16 +212,16 @@ type top_decl =
type program = top_decl list
-type dep_t = Dep of
- bool
+type dep_t = Dep of
+ bool
* ident
- * (top_decl list)
+ * (top_decl list)
* bool (* is stateful *)
(************ Machine code types *************)
-type value_t =
+type value_t =
{
value_desc: value_t_desc;
value_type: Types.type_expr;
@@ -230,7 +231,7 @@ and value_t_desc =
| Cst of constant
| LocalVar of var_decl
| StateVar of var_decl
- | Fun of ident * value_t list
+ | Fun of ident * value_t list
| Array of value_t list
| Access of value_t * value_t
| Power of value_t * value_t
diff --git a/src/tools/stateflow/main_with_json.ml b/src/tools/stateflow/main_with_json.ml
index 9de4efc9..27c88c9a 100644
--- a/src/tools/stateflow/main_with_json.ml
+++ b/src/tools/stateflow/main_with_json.ml
@@ -23,7 +23,7 @@ struct
let json = Yojson.Basic.from_file "GPCA_Alarm_Alarm_SFIR_pp.json"
let Program (init, defs, vars) = Parse.parse_prog json
let prog = Parse.parse_prog json
- let user_vars = Parse.parse_variables json
+ (* let user_vars = Parse.parse_variables json *)
(*let _ = Format.printf "Model definitions@.%a@.####" Simulink.pp_src defs; ()*)
end
@@ -55,7 +55,7 @@ module EvalProg = Interp.Evaluation (Thetaify) (Prog)
let main () =
begin
SF.pp_prog Format.std_formatter (Parse.parse_prog Prog.json);
- SF.pp_vars Format.std_formatter (Parse.parse_variables Prog.json);
+ (* SF.pp_vars Format.std_formatter (Parse.parse_variables Prog.json); *)
end
let _ = main ()
diff --git a/src/tools/stateflow/parser-json/parser_json.ml b/src/tools/stateflow/parser-json/parser_json.ml
index 75e8d43e..8b580235 100644
--- a/src/tools/stateflow/parser-json/parser_json.ml
+++ b/src/tools/stateflow/parser-json/parser_json.ml
@@ -1,127 +1,150 @@
-open Yojson
-open Datatype
-(* open Simulink *)
-(* open Transformer *)
-open Basetypes
-open Basic
-open CPS
-
-module type ParseExt =
-sig
- val parse_condition : json -> Condition.t
- val parse_action : json -> Action.t
- val parse_event : json -> Basetypes.event_t
-end
-
-module Parser (Ext : ParseExt) =
-struct
- let path_split = String.split_on_char '/'
- let path_concat = String.concat (String.make 1 '/')
-
- open Util
-
- let to_list json =
- try
- json |> to_list
- with
- Type_error _ -> [ json ]
-
- let rec parse_prog json : prog_t =
- (*Format.printf "parse_prog@.";*)
- Program (
- json |> member "name" |> to_string,
- (json |> member "states" |> to_list |> List.map parse_state) @
- (json |> member "junctions" |> to_list |> List.map parse_junction)
- @
- (json |> member "sffunctions" |> to_list |> List.map
- (fun res -> SFFunction (parse_prog res))),
- [] (* TODO: to be replaced by variables ! *)
- )
- and parse_variables json =
- (*Format.printf "parse_variables@.";*)
- json |> member "data" |> to_list |> List.map parse_variable
- and parse_state json =
- (*Format.printf "parse_state@.";*)
- State (
- json |> member "path" |> parse_path,
- json |> parse_state_def
- )
- and parse_path json =
- (*Format.printf "parse_path@.";*)
- json |> to_string |> path_split
- and parse_state_def json =
- (*Format.printf "parse_state_def@.";*)
- {
- state_actions = json |> member "state_actions" |> parse_state_actions;
- outer_trans = json |> member "outer_trans" |> to_list |> List.map parse_transition;
- inner_trans = json |> member "inner_trans" |> to_list |> List.map parse_transition;
- internal_composition = json |> member "internal_composition" |> parse_internal_composition
- }
- and parse_state_actions json =
- (*Format.printf "parse_state_actions@.";*)
- {
- entry_act = json |> member "entry_act" |> Ext.parse_action;
- during_act = json |> member "during_act" |> Ext.parse_action;
- exit_act = json |> member "exit_act" |> Ext.parse_action;
- }
- and parse_transition json =
- (*Format.printf "parse_transition@.";*)
- {
- event = json |> member "event" |> Ext.parse_event;
- condition = json |> member "condition" |> Ext.parse_condition;
- condition_act = json |> member "condition_act" |> Ext.parse_action;
- transition_act = json |> member "transition_act" |> Ext.parse_action;
- dest = json |> member "dest" |> parse_dest
- }
- and parse_dest json =
- (*Format.printf "parse_dest@.";*)
- (json |> member "type" |> to_string |>
- (function
- | "State" -> (fun p -> DPath p)
- | "Junction" -> (fun j -> DJunction (path_concat j))
- | _ -> assert false))
- (json |> member "name" |> parse_path)
- and parse_internal_composition json =
- (*Format.printf "parse_internal_composition@.";*)
- (json |> member "type" |> to_string |>
- (function
- | "EXCLUSIVE_OR" -> (fun tinit substates -> Or (tinit, substates))
- | "PARALLEL_AND" -> (fun tinit substates -> assert (tinit = []); And (substates))
- | _ -> assert false))
- (json |> member "tinit" |> parse_tinit)
- (json |> member "substates" |> to_list |> List.map to_string)
- and parse_tinit json =
- (*Format.printf "parse_tinit@.";*)
- json |> to_list |> List.map parse_transition
- and parse_junction json =
- (*Format.printf "parse_junction@.";*)
- Junction (
- json |> member "path" |> to_string,
- json |> member "outer_trans" |> to_list |> List.map parse_transition
- )
- and scope_of_string s =
- match s with
- | "Constant" -> Constant
- | "Input" -> Input
- | "Local" -> Local
- | "Output" -> Output
- | "Parameter" -> Parameter
- | _ -> failwith ("Invalid scope for variable: " ^ s)
- and datatype_of_json json =
- let datatype = json |> member "datatype" |> to_string in
- let init_value = json |> member "initial_value" |> to_string in
- match datatype with
- | "bool" -> Bool (bool_of_string init_value)
- | "int" -> Int (int_of_string init_value)
- | "real" -> Real (float_of_string init_value)
- | _ -> failwith ("Invalid datatype " ^ datatype
- ^ " for variable " ^ (json |> member "name"
- |> to_string))
- and parse_variable json =
- (*Format.printf "parse_variables@.";*)
- (
- json |> member "name" |> to_string,
- json |> member "scope" |> to_string |> scope_of_string,
- json |> datatype_of_json
- )
-end
+open Yojson
+open Datatype
+(* open Simulink *)
+(* open Transformer *)
+open Basetypes
+open Basic
+open Corelang
+open CPS
+open LustreSpec
+
+module type ParseExt =
+sig
+ val parse_condition : json -> Condition.t
+ val parse_action : json -> Action.t
+ val parse_event : json -> Basetypes.event_t
+end
+
+module Parser (Ext : ParseExt) =
+struct
+ let path_split = String.split_on_char '/'
+ let path_concat = String.concat (String.make 1 '/')
+
+ open Util
+
+ let to_list json =
+ try
+ json |> to_list
+ with
+ Type_error _ -> [ json ]
+
+ let rec parse_prog json : prog_t =
+ (*Format.printf "parse_prog@.";*)
+ Program (
+ json |> member "name" |> to_string,
+ (json |> member "states" |> to_list |> List.map parse_state) @
+ (json |> member "junctions" |> to_list |> List.map parse_junction)
+ @
+ (json |> member "sffunctions" |> to_list |> List.map
+ (fun res -> SFFunction (parse_prog res))),
+ json |> member "data" |> to_list |> List.map parse_variable
+ )
+ (* and parse_variables json = *)
+ (* (\*Format.printf "parse_variables@.";*\) *)
+ (* json |> member "data" |> to_list |> List.map parse_variable *)
+ and parse_state json =
+ (*Format.printf "parse_state@.";*)
+ State (
+ json |> member "path" |> parse_path,
+ json |> parse_state_def
+ )
+ and parse_path json =
+ (*Format.printf "parse_path@.";*)
+ json |> to_string |> path_split
+ and parse_state_def json =
+ (*Format.printf "parse_state_def@.";*)
+ {
+ state_actions = json |> member "state_actions" |> parse_state_actions;
+ outer_trans = json |> member "outer_trans" |> to_list |> List.map parse_transition;
+ inner_trans = json |> member "inner_trans" |> to_list |> List.map parse_transition;
+ internal_composition = json |> member "internal_composition" |> parse_internal_composition
+ }
+ and parse_state_actions json =
+ (*Format.printf "parse_state_actions@.";*)
+ {
+ entry_act = json |> member "entry_act" |> Ext.parse_action;
+ during_act = json |> member "during_act" |> Ext.parse_action;
+ exit_act = json |> member "exit_act" |> Ext.parse_action;
+ }
+ and parse_transition json =
+ (*Format.printf "parse_transition@.";*)
+ {
+ event = json |> member "event" |> Ext.parse_event;
+ condition = json |> member "condition" |> Ext.parse_condition;
+ condition_act = json |> member "condition_act" |> Ext.parse_action;
+ transition_act = json |> member "transition_act" |> Ext.parse_action;
+ dest = json |> member "dest" |> parse_dest
+ }
+ and parse_dest json =
+ (*Format.printf "parse_dest@.";*)
+ (json |> member "type" |> to_string |>
+ (function
+ | "State" -> (fun p -> DPath p)
+ | "Junction" -> (fun j -> DJunction (path_concat j))
+ | _ -> assert false))
+ (json |> member "name" |> parse_path)
+ and parse_internal_composition json =
+ (*Format.printf "parse_internal_composition@.";*)
+ (json |> member "type" |> to_string |>
+ (function
+ | "EXCLUSIVE_OR" -> (fun tinit substates -> Or (tinit, substates))
+ | "PARALLEL_AND" -> (fun tinit substates -> assert (tinit = []); And (substates))
+ | _ -> assert false))
+ (json |> member "tinit" |> parse_tinit)
+ (json |> member "substates" |> to_list |> List.map to_string)
+ and parse_tinit json =
+ (*Format.printf "parse_tinit@.";*)
+ json |> to_list |> List.map parse_transition
+ and parse_junction json =
+ (*Format.printf "parse_junction@.";*)
+ Junction (
+ json |> member "path" |> to_string,
+ json |> member "outer_trans" |> to_list |> List.map parse_transition
+ )
+ and scope_of_string s =
+ match s with
+ | "Constant" -> Constant
+ | "Input" -> Input
+ | "Local" -> Local
+ | "Output" -> Output
+ | "Parameter" -> Parameter
+ | _ -> failwith ("Invalid scope for variable: " ^ s)
+ and datatype_of_json json =
+ let datatype = json |> member "datatype" |> to_string in
+ let init_value = json |> member "initial_value" |> to_string in
+ match datatype with
+ | "bool" -> Bool (bool_of_string init_value)
+ | "int" -> Int (int_of_string init_value)
+ | "real" -> Real (float_of_string init_value)
+ | _ -> failwith ("Invalid datatype " ^ datatype
+ ^ " for variable " ^ (json |> member "name"
+ |> to_string))
+ and lustre_datatype_of_json json location =
+ let datatype = json |> member "datatype" |> to_string in
+ let initial_value = json |> member "initial_value" |> to_string in
+ match datatype with
+ | "bool" -> (Tydec_bool, mkexpr location
+ (Expr_const (Const_bool
+ (bool_of_string initial_value))))
+ | "int" -> (Tydec_int, mkexpr location
+ (Expr_const (Const_int (int_of_string
+ initial_value))))
+ | "real" -> (Tydec_real, mkexpr location
+ (Expr_const (Const_real (Num.num_of_int 0,
+ 0,
+ initial_value))))
+ | _ -> failwith ("Invalid datatype " ^ datatype
+ ^ " for variable " ^ (json |> member "name"
+ |> to_string))
+ and parse_variable json =
+ (*Format.printf "parse_variable@.";*)
+ let location = Location.dummy_loc in
+ let (datatype, initial_value) = lustre_datatype_of_json json location in
+ mkvar_decl location ~orig:true
+ ( json |> member "name" |> to_string,
+ {ty_dec_desc = datatype; ty_dec_loc = location},
+ {ck_dec_desc = Ckdec_any; ck_dec_loc = location},
+ false,
+ Some initial_value
+ )
+end
--
GitLab