CristalCaveGem » LustreC

let sf_level = 2

type junction_name_t = string

type path_t = state_name_t list

type event_base_t = string

type event_t = event_base_t option

(* Connected to lustrec types *)

  defs : Lustre_types.statement list;

  ainputs : Lustre_types.var_decl list;

  aoutputs : Lustre_types.var_decl list;

  avariables : Lustre_types.var_decl list; (* ident: string; *)

}

type base_condition_t = {

  expr : Lustre_types.expr;

  cinputs : Lustre_types.var_decl list;

  coutputs : Lustre_types.var_decl list;

  cvariables : Lustre_types.var_decl list;

}

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_cond fmt c = Printers.pp_expr fmt c.expr

(* Actions are defined by string + the opening and closing of states *)

(* This version is slightly more complex than the one of EMSOFT'05 to enable the

   use of function calls in action.

   TODO: these rich call type could be externalized and a functor introduced. *)

let pp_frontier fmt frontier =

  match frontier with

    Format.fprintf fmt "Loose"

  | Strict ->

    Format.fprintf fmt "Strict"

type _ call_t =

  | Ecall : (path_t * path_t * frontier_t) call_t

  | Dcall : path_t call_t

  | Xcall : (path_t * frontier_t) call_t

 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

end

    | Quote : base_action_t -> t

    | Close : path_t -> t

    | Call : 'c call_t * 'c -> t

    | Nil : t

  let pp_call : type c. Format.formatter -> c call_t -> c -> unit =

      fun (p, p', f) ->

        Format.fprintf fmt "%a(%a, %a, %a)" pp_call call pp_path p pp_path p'

          pp_frontier f

    | Dcall ->

      fun p -> Format.fprintf fmt "%a(%a)" pp_call call pp_path p

    | Xcall ->

      fun (p, f) ->

        Format.fprintf fmt "%a(%a, %a)" pp_call call pp_path p pp_frontier f

  let pp_act fmt act =

    match act with

      pp_call fmt c a

    | Quote a ->

      Format.fprintf fmt "%a" pp_base_act a

    | Close p ->

      Format.fprintf fmt "Close(%a)" pp_path p

    | Open p ->

      Format.fprintf fmt "Open(%a)" pp_path p

    | Nil ->

      Format.fprintf fmt "Nil"

(* Conditions are either (1) simple strings, (2) the active status of a state or

   (3) occurence of an event. They can be combined (conjunction, negation) *)

  val pp_cond : Format.formatter -> t -> unit

end

module Condition = struct

    | Quote of base_condition_t

    | Active of path_t

    | Event of event_base_t

    | And of t * t

    | Neg of t

    | True

  let cquote cond = Quote cond

  let event evt = match evt with None -> True | Some e -> Event e

  let rec pp_cond fmt cond =

    match cond with

      Format.fprintf fmt "true"

    | Active p ->

      Format.fprintf fmt "Active(%a)" pp_path p

    | Event e ->

      Format.fprintf fmt "Event(%s)" e

    | Neg cond ->

      Format.fprintf fmt "(neg %a)" pp_cond cond

    | And (cond1, cond2) ->

      Format.fprintf fmt "%a /\\ %a" pp_cond cond1 pp_cond cond2

    | Quote c ->

      Format.fprintf fmt "%a" pp_base_cond c

let _ = (module Condition : ConditionType)

  type t = { variable : Lustre_types.var_decl; init_val : Lustre_types.expr }