CristalCaveGem » LustreC

open Basetypes

(* open ActiveEnv *)

(* Type definitions of a model *)

type trans_t = {

  condition : Condition.t;

  condition_act : Action.t;

  transition_act : Action.t;

  dest : destination_t;

type transitions_t = trans_t list

type composition_t =

  | Or of transitions_t * state_name_t list

  | And of state_name_t list

type state_actions_t = {

  during_act : Action.t;

  exit_act : Action.t;

type state_def_t = {

  state_actions : state_actions_t;

  outer_trans : transitions_t;

  inner_trans : transitions_t;

  internal_composition : composition_t;

}

  | Junction of junction_name_t * transitions_t

  | Program of

      state_name_t

      * prog_t src_components_t list

      * (Lustre_types.var_decl * Lustre_types.expr) 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 trace_t = event_t list

  val name : string

  val traces : trace_t list

   events, as well as printer functions *)

  let no_event = None

  let event s = Some s

  let action s = Action.aquote s

  let condition s = Condition.cquote s

  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 }

      (fun res c ->

        | State (p, _) ->

          ActiveStates.Vars.add p res

        | Junction _ ->

          res

        | SFFunction _ ->

          res)

  let init_env model = ActiveStates.Env.from_set (states model) false

    match e with

      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

  let pp_trans fmt t =

      pp_event t.event Condition.pp_cond t.condition Action.pp_act

      t.condition_act Action.pp_act t.transition_act pp_dest t.dest

      (Utils.fprintf_list ~sep:";@ " pp_trans)

      l

    match c with

        (Utils.fprintf_list ~sep:"; " pp_state_name)

        _S

    | And _S ->

      Format.fprintf fmt "And({%a})"

        (Utils.fprintf_list ~sep:"; " pp_state_name)

        _S

  let pp_state_actions fmt sa =

      Action.pp_act sa.during_act Action.pp_act sa.exit_act

    Format.fprintf fmt "@[<v 0>(@[<v 0>%a,@ %a,@ %a,@ %a@]@ @])"

      pp_transitions s.inner_trans pp_comp s.internal_composition

  let pp_src pp_sffunction 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))

  let rec pp_sffunction fmt (Program (name, component_list, _)) =

      component_list

    Format.fprintf fmt "@[<v>%a@ @]"

      (Utils.fprintf_list ~sep:"@ " Printers.pp_var)

  let pp_prog fmt (Program (name, component_list, vars)) =

      component_list pp_vars (List.map fst vars)

  let pp_scope fmt src =

      (match src with

      | Constant ->

        "Constant"

      | Input ->

        "Input"

      | Local ->

        "Local"

      | Output ->

        "Output"

      | Parameter ->

        "Parameter")