parser-json: final version of parser with new types

src/tools/stateflow/common/basetypes.ml

 
 let sf_level = 2
-  
+
 (* Basic datatype for model elements: state and junction name, events ... *)
-type state_name_t    = string
-type junction_name_t = string
-type path_t = state_name_t list
-type event_base_t = string
-type event_t      = event_base_t option
+type state_name_t         = string
+type junction_name_t      = string
+type path_t               = state_name_t list
+type event_base_t         = string
+type event_t              = event_base_t option
+type user_variable_name_t = string
 
 (* Connected to lustrec types *)
-type base_action_t = { defs : LustreSpec.eq list; ident : string }
+type base_action_t    = { defs : LustreSpec.eq list; ident : string }
 type base_condition_t = LustreSpec.expr
-  
+
 (* P(r)etty printers *)
-let pp_state_name = Format.pp_print_string
-let pp_junction_name = Format.pp_print_string
-let pp_path fmt p = Utils.fprintf_list ~sep:"." pp_state_name fmt p
-let pp_event fmt e = match e with None -> Format.fprintf fmt "none" | Some s -> Format.fprintf fmt "%s" s
+let pp_state_name     = Format.pp_print_string
+let pp_junction_name  = Format.pp_print_string
+let pp_path fmt p     = Utils.fprintf_list ~sep:"." pp_state_name fmt p
+let pp_event fmt e    = match e with None -> Format.fprintf fmt "none" | Some s -> Format.fprintf fmt "%s" s
 let pp_base_act fmt a = Utils.fprintf_list ~sep:",@ " Printers.pp_node_eq fmt a.defs
-let pp_base_cond = Printers.pp_expr
-  
+let pp_base_cond      = Printers.pp_expr
+
 (* Action and Condition types and functions. *)
 
 (* Actions are defined by string + the opening and closing of states *)
@@ -44,13 +45,13 @@ type _ call_t =
   | Xcall : (path_t * frontier_t) call_t
 
 let pp_call :
-type a. Format.formatter -> a call_t -> unit = 
+type a. Format.formatter -> a call_t -> unit =
   fun fmt call ->
     match call with
     | Ecall -> Format.fprintf fmt "CallE"
     | Dcall -> Format.fprintf fmt "CallD"
     | Xcall -> Format.fprintf fmt "CallX"
-  
+
 module type ActionType =
 sig
   type t
@@ -59,7 +60,7 @@ sig
   val open_path : path_t -> t
   val close_path : path_t -> t
   val call : 'c call_t -> 'c -> t
-    
+
   val pp_act : Format.formatter -> t -> unit
 end
 
@@ -73,7 +74,7 @@ struct
     | Call  : 'c call_t * 'c -> t
     | Nil   : t
 
-    
+
   let nil = Nil
   let aquote act = Quote act
   let open_path p = Open p
@@ -96,7 +97,7 @@ struct
     | Nil              -> Format.fprintf fmt "Nil"
 end
 
-let _ = (module Action : ActionType) 
+let _ = (module Action : ActionType)
 
 
 (* Conditions are either (1) simple strings, (2) the active status of a state or

src/tools/stateflow/common/datatype.ml

@@ -34,27 +34,34 @@ type state_def_t = {
   internal_composition : composition_t;
 }
 
-type src_components_t =
+type 'prog_t src_components_t =
   | State of path_t * state_def_t
   | Junction of junction_name_t * transitions_t
+  | SFFunction of 'prog_t
+
+type prog_t = Program of state_name_t * prog_t src_components_t list * LustreSpec.var_decl list
+
+type scope_t = Constant | Input | Local | Output | Parameter
+
+type datatype_var_init_t = Bool of bool | Real of float | Int of int
+
+type user_variable_t = user_variable_name_t * scope_t * datatype_var_init_t
 
-type prog_t = state_name_t * src_components_t list * LustreSpec.var_decl list 
-  
 type trace_t = event_t list
-    
+
 module type MODEL_T = sig
   val name : string
   val model : prog_t
   val traces: trace_t list
 end
-  
+
 (* Module (S)tate(F)low provides basic constructors for action, condition,
    events, as well as printer functions *)
 module SF =
 struct
 
   (* Basic constructors *)
-  
+
   let no_action    = Action.nil
   let no_condition = Condition.tru
   let no_event     = None
@@ -64,26 +71,27 @@ struct
   let no_state_action    = {entry_act = no_action; during_act = no_action; exit_act = no_action; }
   let state_action a b c = {entry_act = a; during_act = b; exit_act = c; }
 
-  let states (_, defs, _) =
+  let states (Program (_, defs, _)) =
     List.fold_left
       (fun res c ->
 	match c with
 	| State (p, _) -> ActiveStates.Vars.add p res
-	| Junction _ -> res
+	| Junction _  -> res
+        | SFFunction _ -> res
       )
       ActiveStates.Vars.empty defs
 
   let init_env model = ActiveStates.Env.from_set (states model) false
 
   let global_vars (_, _, env) = env
-    
+
   (* Printers *)
-      
+
   let pp_event fmt e =
     match e with
     | Some e -> Format.fprintf fmt "%s" e
     | None -> Format.fprintf fmt "noevent"
-    
+
   let pp_dest fmt d = match d with
     | DPath p -> Format.fprintf fmt "Path %a" pp_path p
     | DJunction j -> Format.fprintf fmt "Junction %a" pp_junction_name j
@@ -94,9 +102,9 @@ struct
       pp_event t.event
       Condition.pp_cond t.condition
       Action.pp_act t.condition_act
-      Action.pp_act t.transition_act    
+      Action.pp_act t.transition_act
       pp_dest t.dest
-      
+
   let pp_transitions fmt l =
     Format.fprintf fmt
       "@[<hov 0>[@[<hov 0>%a@]@ ]@]"
@@ -116,26 +124,61 @@ struct
       Action.pp_act sa.entry_act
       Action.pp_act sa.during_act
       Action.pp_act sa.exit_act
-      
+
   let pp_state fmt s =
     Format.fprintf fmt "@[<v 0>(@[<v 0>%a,@ %a,@ %a,@ %a@]@ @])"
       pp_state_actions s.state_actions
       pp_transitions s.outer_trans
       pp_transitions s.inner_trans
       pp_comp s.internal_composition
-      
-  let pp_src fmt src =
+
+  let pp_src pp_sffunction fmt src =
     Format.fprintf fmt "@[<v>%a@ @]"
-      (Utils.fprintf_list ~sep:"@ @ " (fun fmt src -> match src with
-	State (p, def) ->
-	  Format.fprintf fmt "%a: %a"
-	    pp_path p
-	    pp_state def
-      | Junction (s, tl) ->
-	 Format.fprintf fmt "%a: %a"
-	   pp_state_name s
-	   pp_transitions tl
-       ))
+      (Utils.fprintf_list ~sep:"@ @ "
+         (fun fmt src -> match src with
+	    | State (p, def)   -> Format.fprintf fmt "%a: %a"
+                                  pp_path p pp_state def
+            | Junction (s, tl) -> Format.fprintf fmt "%a: %a"
+	                            pp_state_name s
+	                            pp_transitions tl
+            | SFFunction p     -> pp_sffunction fmt p
+         ))
       src
+
+  let rec pp_sffunction fmt (Program (name, component_list, _)) =
+    Format.fprintf fmt "SFFunction name: %s@ %a@ "
+      name
+      (pp_src pp_sffunction) component_list
+
+  let pp_prog fmt (Program (name, component_list, _)) =
+    Format.fprintf fmt "Main node name: %s@ %a@ "
+      name
+      (pp_src pp_sffunction) component_list
+
+  let pp_scope fmt src =
+    Format.fprintf fmt (match src with
+        | Constant  -> "Constant"
+        | Input     -> "Input"
+        | Local     -> "Local"
+        | Output    -> "Output"
+        | Parameter -> "Parameter")
+
+  let pp_vars fmt src =
+    Format.fprintf fmt "@[<v>%a@ @]"
+      (Utils.fprintf_list ~sep:"@ "
+         (fun fmt src -> match src with
+	    | (name, scope, Bool b) -> Format.fprintf fmt "%s: %a %s := %s"
+                                  name
+                                  pp_scope scope
+                                  "Bool" (string_of_bool b)
+	    | (name, scope, Real f) -> Format.fprintf fmt "%s: %a %s := %s"
+                                  name
+                                  pp_scope scope
+                                  "Real" (string_of_float f)
+	    | (name, scope, Int i)  -> Format.fprintf fmt "%s: %a %s := %s"
+                                  name
+                                  pp_scope scope
+                                  "Int" (string_of_int i)
+         ))
+    src
 end
-   

src/tools/stateflow/main_with_json.ml

@@ -3,13 +3,16 @@ open Basetypes
 open Datatype
 (* open Interpreter *)
 open Parser_json
-open Transformer
+(* open Transformer *)
 open Theta
+open CPS_ccode_generator
+open CPS_interpreter
+open CPS_transformer
 
 module ParseExt =
 struct
-  let parse_condition _ = Transformer.Condition.tru
-  let parse_action    _ = Transformer.Action.nil
+  let parse_condition _ = Condition.tru
+  let parse_action    _ = Action.nil
   let parse_event json  = Some Yojson.Basic.(json |> to_string)
 end
 
@@ -18,17 +21,16 @@ module Parse = Parser (ParseExt)
 module Prog =
 struct
   let json                       = Yojson.Basic.from_file "GPCA_Alarm_Alarm_SFIR_pp.json"
-  let Simulink.Prog (init, defs) = Parse.parse_prog json
+  let Program (init, defs, vars) = Parse.parse_prog json
   let prog                       = Parse.parse_prog json
   let user_vars                  = Parse.parse_variables json
-  let vars                       = Simulink.states (Simulink.Prog (init, defs))
   (*let _ = Format.printf "Model definitions@.%a@.####" Simulink.pp_src defs; ()*)
 end
 
 module Transformer =
-  (* Transformer.LustrePrinter (Prog) *)
-  Transformer.CodeGenerator
-  (* Transformer.Evaluator *)
+  (* CPS_ccode_generator.LustrePrinter (Program) *)
+  CodeGenerator
+  (* CPS_ccode_generator.Evaluator *)
 
 module Interp = Interpreter (Transformer)
 
@@ -51,21 +53,9 @@ module Thetaify = KenvTheta.ModularThetaify (Tables) (Modularity)
 module EvalProg = Interp.Evaluation (Thetaify) (Prog)
 
 let main ()  =
-  let principal = EvalProg.eval_prog in
-  let components = EvalProg.eval_components in
   begin
-    Format.printf "%a@." Transformer.pp_principal principal;
-    List.iter
-      (fun (c, tr) -> Format.printf "@.%a@." (fun fmt -> Transformer.pp_component fmt Ecall c) tr)
-      (components Ecall);
-    List.iter
-      (fun (c, tr) -> Format.printf "@.%a@." (fun fmt -> Transformer.pp_component fmt Dcall c) tr)
-      (components Dcall);
-    List.iter
-      (fun (c, tr) -> Format.printf "@.%a@." (fun fmt -> Transformer.pp_component fmt Xcall c) tr)
-      (components Xcall);
-    Simulink.pp_prog Format.std_formatter (Parse.parse_prog Prog.json);
-    Simulink.pp_vars Format.std_formatter (Parse.parse_variables Prog.json);
+    SF.pp_prog Format.std_formatter (Parse.parse_prog Prog.json);
+    SF.pp_vars Format.std_formatter (Parse.parse_variables Prog.json);
   end
 
 let _ = main ()

src/tools/stateflow/parser-json/parser_json.ml

@@ -26,15 +26,16 @@ struct
     with
       Type_error _ -> [ json ]
 
-  let rec parse_prog json =
+  let rec parse_prog json : prog_t =
      (*Format.printf "parse_prog@.";*)
-    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)))
+        (fun res -> SFFunction (parse_prog res))),
+      [] (* TODO: to be replaced by variables ! *)
     )
   and parse_variables json =
      (*Format.printf "parse_variables@.";*)

src/tools/stateflow/semantics/cPS.ml

-open Basetypes 
+open Basetypes
 open Datatype
 open CPS_transformer
-open Theta 
+open Theta
 
 module Semantics = functor (T: TransformerType) (M: MODEL_T) ->
 struct
-  
+
 module Prog =
 struct
-  let init, defs, state_vars = 
-    let (init, defs, globals) = M.model in
+  let init, defs, state_vars =
+    let Program (init, defs, globals) = M.model in
     let state_vars = SF.states M.model in
     init, defs, state_vars
-    
+
 (*let _ = Format.printf "Model definitions@.%a@.####" Simulink.pp_src defs; () *)
 end
 
@@ -35,11 +35,11 @@ let eval ((modular_entry:bool), (modular_during:bool), (modular_exit:bool)) =
   let module Thetaify = KenvTheta.ModularThetaify (Tables) (Modularity) in
   let module EvalProg = Interp.Evaluation (Thetaify) (Prog) in
   (module EvalProg: Interp.EvaluationType)
-  
+
 let compute modular  =
   let module Eval = (val (eval modular)) in
-  Eval.eval_prog 
-    
+  Eval.eval_prog
+
 let code_gen modular  =
   let module Eval = (val (eval modular)) in
   let principal, components =  Eval.eval_prog, Eval.eval_components in

src/tools/stateflow/semantics/cPS_interpreter.ml

-open Basetypes 
+open Basetypes
 open Datatype
 (* open ActiveEnv *)
 open CPS_transformer
 (* open Simulink *)
-open Theta 
+open Theta
 
 module Interpreter (Transformer : TransformerType) =
 struct
@@ -165,7 +165,7 @@ struct
 	match tag with
 	| E -> fun path frontier -> Transformer.(
 	  Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a, dest %a, frontier %a]]@ " pp_tag tag pp_path p pp_path path pp_frontier frontier);
-	  ((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.entry_act >> eval_act (module Theta) (open_path p))) >> 
+	  ((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.entry_act >> eval_act (module Theta) (open_path p))) >>
 	  match path with
 	  | []         -> eval_C E p p_def.internal_composition
 	  | s::path_tl -> Theta.theta E (p@[s]) path_tl Loose
@@ -195,7 +195,7 @@ struct
   module type ProgType =
   sig
     val init : state_name_t
-    val defs : src_components_t list
+    val defs : prog_t src_components_t list
   end
 
   module type EvaluationType =
@@ -204,7 +204,7 @@ struct
     val eval_prog : Transformer.t
     val eval_components : 'c call_t -> ('c * Transformer.t) list
   end
-    
+
   module Evaluation (Thetaify : ThetaifyType) (Prog : ProgType) : EvaluationType =
   struct
     module Denotation = Denotation (Thetaify)
@@ -216,9 +216,12 @@ struct
       let kenv =
 	List.fold_left (
 	  fun accu d -> match d with
-   | State (p, defp) -> { accu with cont_node = (p, ((fun kenv -> eval_S kenv E p defp), (fun kenv -> eval_S kenv D p defp), (fun kenv -> eval_S kenv X p defp)))::accu.cont_node  }
-	  | Junction (j, defj) -> { accu with cont_junc = (j, (fun kenv -> eval_T kenv defj))::accu.cont_junc  }
-	) {cont_node = []; cont_junc = []} Prog.defs
+          | State (p, defp)    -> { accu with cont_node = (p, ((fun kenv -> eval_S kenv E p defp),
+                                                               (fun kenv -> eval_S kenv D p defp),
+                                                               (fun kenv -> eval_S kenv X p defp)))::accu.cont_node }
+	  | Junction (j, defj) -> { accu with cont_junc = (j, (fun kenv -> eval_T kenv defj))::accu.cont_junc }
+          | SFFunction _       -> accu
+        ) {cont_node = []; cont_junc = []} Prog.defs
     end
 
     module AppDenotation = Denotation (Kenv)

src/tools/stateflow/semantics/cPS_transformer.ml

@@ -80,6 +80,8 @@ sig
   (* val mktransformer : t -> unit *)
   val mkprincipal : t -> LustreSpec.program
   val mkcomponent : 'c call_t -> 'c -> t -> LustreSpec.program
+  val pp_principal : Format.formatter -> t -> unit
+  val pp_component : Format.formatter -> 'c call_t -> 'c -> t -> unit
 end
 
 module type ComparableTransformerType =
@@ -88,7 +90,3 @@ sig
 
   val ( == ) : t -> t -> bool
 end
-
-
-  
-