CristalCaveGem » LustreC

sf_sem:

	ocamlbuild sf_sem.native

	cp sf_sem.native sf_sem

clean:

	rm -rf _build

	rm sf_sem.native

.PHONY: sf_sem

"models": include

"common": include

"semantics/CPS": include

"semantics/emsoft05": include

open Basetypes 

(* Module to manipulate set of active states.

   It relies on sets of path to represent active ones.

*)

(*******************************)

module Vars =

struct

  include Set.Make (struct type t = path_t let compare = compare end)

  let pp_set fmt rho =

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

      (Utils.fprintf_list ~sep:"@ "

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

      (elements rho)

end

module Env =

struct

  include Map.Make (struct type t = path_t let compare = compare end)

  let from_set s default =

    Vars.fold (fun e m -> add e default m ) s empty

  let find a b =

    try 

      find a b

    with Not_found -> (

      Format.printf "Looking for %a@." pp_path a ;

      raise Not_found

    )

  let keys a =

    fold (fun key _ -> Vars.add key) a Vars.empty

  let pp_env fmt rho =

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

      (Utils.fprintf_list ~sep:"@ "

	 (fun fmt (p,b) -> Format.fprintf fmt "%a -> %b" pp_path p b))

      (bindings rho)

end

(* 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 base_action_t = string

type base_condition_t = string

(* 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_base_act = Format.pp_print_string

let pp_base_cond = Format.pp_print_string

(* Action and Condition types and functions. *)

(* 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. *)

type frontier_t =

  | Loose

  | Strict

let pp_frontier fmt frontier =

  match frontier with

  | Loose  -> 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

let pp_call :

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

  val nil : t

  val aquote : base_action_t -> t

  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

module Action =

struct

  type t =

    | Quote : base_action_t -> t

    | Close : path_t -> t

    | Open  : path_t -> t

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

    | Nil   : t

  let nil = Nil

  let aquote act = Quote act

  let open_path p = Open p

  let close_path p = Close p

  let call c a = Call (c, a)

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

    fun fmt call ->

    match call with

    | Ecall -> (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

    | Call (c, a)      -> 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"

end

let _ = (module Action : ActionType) 

(* 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) *)

module type ConditionType =

sig

  type t

  val cquote : base_condition_t -> t

  val tru : t

  val active : path_t -> t

  val event : event_t -> t

  val ( && ) : t -> t -> t

  val neg : t -> t

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

end

  module Condition =

struct

  type t =

    | 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 tru = True

  let neg cond = Neg cond

  let ( && ) cond1 cond2 = And (cond1, cond2)

  let active path = Active path

  let event evt =

    match evt with

    | None   -> True

    | Some e -> Event e

  let rec pp_cond fmt cond =

    match cond with

    | True               -> 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

end

let _ = (module Condition : ConditionType)

open Basetypes

(* open ActiveEnv *)

(* Type definitions of a model *)

type destination_t =

  | DPath of path_t

  | DJunction of junction_name_t

type trans_t = {

  event: event_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 = {

  entry_act: Action.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;

}

type src_components_t =

  | State of path_t * state_def_t

  | Junction of junction_name_t * transitions_t

type prog_t = state_name_t * src_components_t 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

  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; }

  let states (_, defs) =

    List.fold_left (fun res c -> match c with State (p, _) -> ActiveStates.Vars.add p res | Junction _ -> res) ActiveStates.Vars.empty defs

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

  (* 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

  let pp_trans fmt t =

    Format.fprintf fmt

      "@[<hov 0>(@[<hov 0>%a,@ %a,@ %a,@ %a,@ %a@]@ )@]"

      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

  let pp_transitions fmt l =

    Format.fprintf fmt

      "@[<hov 0>[@[<hov 0>%a@]@ ]@]"

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

  let pp_comp fmt c = match c with

    | Or (_T, _S) ->

       Format.fprintf fmt "Or(%a, {%a})"

	 pp_transitions _T

	 (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 =

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

      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 =

    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

       ))

      src

end

let debug = false

let log ?debug:(dbg=false) f =

  if debug || dbg then

    Format.printf "%t" f

  else

    ()

let rec fprintf_list ~sep:sep f fmt = function

  | []   -> ()

  | [e]  -> f fmt e

  | x::r -> Format.fprintf fmt "%a%(%)%a" f x sep (fprintf_list ~sep f) r

let last l = List.hd (List.rev l)

open Datatype

open SF

let name = "medium"

let model : prog_t =

    let state_main = "main" in

    let state_a = "a" in

    let state_a1 = "a1" in

    let state_b = "b" in

    let actions_main = state_action (action "emain") (action "dmain") (action "xmain") in

    let actions_a = state_action (action "eA") (action "dA") (action "xA") in

    let actions_a1 = state_action (action "eA1") (action "dA1") (action "xA1") in

    let actions_b = state_action (action "eB") (action "dB") (action "xB") in

    let tA = {

      event = no_event;

      condition = condition "cond_tA";

      condition_act = action "condact_tA";

      transition_act = action "transact_tA";

      dest = DPath [state_main;state_a];

    }

    in

    let tJ = {

      event = no_event;

      condition = condition "cond_tJ";

      condition_act = action "condact_tJ";

      transition_act = action "transact_tJ";

      dest = DJunction "jmid";

    }

    in

    let tB = {

      event = no_event;

      condition = condition "cond_tB";

      condition_act = action "condact_tB";

      transition_act = action "transact_tB";

      dest = DPath [state_main;state_b];

    }

    in

    let tA1 = {

      event = no_event;

      condition = condition "cond_tA1";

      condition_act = action "condact_tA1";

      transition_act = action "transact_tA1";

      dest = DPath [state_main;state_a;state_a1];

    }

    in

    let def_a = {

      state_actions = actions_a;

      outer_trans = [tJ];

      inner_trans = [];

      internal_composition = Or ([tA1], [state_a1])

    }

    in

    let def_a1 = {

      state_actions = actions_a1;

      outer_trans = [tB];

      inner_trans = [];

      internal_composition = Or ([], [])

    }

    in

    let def_b = {

      state_actions = actions_b;

      outer_trans = [tA1];

      inner_trans = [];

      internal_composition = Or ([], [])

    }

    in

    let def_main = {

      state_actions = actions_main;

      outer_trans = [];

      inner_trans = [];

      internal_composition = Or ([tA], [state_a; state_b])

    }

    in

    let src = [State([state_main;state_a], def_a);

	       State([state_main;state_a;state_a1], def_a1);

	       State([state_main;state_b], def_b);

	       State([state_main], def_main);

	       Junction("jmid", [tB]);

	      ]

    in

    (state_main, src)

let traces : trace_t list = [[None; None]]

open Datatype

open SF

let name = "simple"

let model : prog_t =

    let state_main = "main" in

    let state_a = "a" in

    let state_a1 = "a1" in

    let state_b = "b" in

    let actions_main = state_action (action "emain") (action "dmain") (action "xmain") in

    let actions_a = state_action (action "eA") (action "dA") (action "xA") in

    let actions_a1 = state_action (action "eA1") (action "dA1") (action "xA1") in

    let actions_b = state_action (action "eB") (action "dB") (action "xB") in

    let tA = {

      event = no_event;

      condition = condition "cond_tA";

      condition_act = action "condact_tA";

      transition_act = action "transact_tA";

      dest = DPath [state_main;state_a];

    }

    in

    let tB = {

      event = no_event;

      condition = condition "cond_tB";

      condition_act = action "condact_tB";

      transition_act = action "transact_tB";

      dest = DPath [state_main;state_b];

    }

    in

    let tA1 = {

      event = no_event;

      condition = condition "cond_tA1";

      condition_act = action "condact_tA1";

      transition_act = action "transact_tA1";

      dest = DPath [state_main;state_a;state_a1];

    }

    in

    let def_a = {

      state_actions = actions_a;

      outer_trans = [tB];

      inner_trans = [];

      internal_composition = Or ([tA1], [state_a1])

    }

    in

    let def_a1 = {

      state_actions = actions_a1;

      outer_trans = [tB];

      inner_trans = [];

      internal_composition = Or ([], [])

    }

    in

    let def_b = {

      state_actions = actions_b;

      outer_trans = [tA1];

      inner_trans = [];

      internal_composition = Or ([], [])

    }

    in

    let def_main = {

      state_actions = actions_main;

      outer_trans = [];

      inner_trans = [];

      internal_composition = Or ([tA], [state_a; state_b])

    }

    in

    let src = [State([state_main;state_a], def_a);

	       State([state_main;state_a;state_a1], def_a1);

	       State([state_main;state_b], def_b);

	       State([state_main], def_main);

	      ]

    in

    (state_main, src)

let traces : trace_t list = [[None; None]]

open Datatype

(* open Transformer2 *)

open SF

let verbose = false

let actionv x = if verbose then action x else no_action

let name = "stopwatch"

let model = 

  let smain    = "main" in

  let sstop    = "stop" in

  let sreset   = "reset" in

  let slapstop = "lap_stop" in

  let srun     = "run" in

  let srunning = "running" in

  let slap     = "lap" in

  let tinitstop = {

    event = no_event;

    condition = no_condition;

    condition_act  = actionv "ac_cond_init_stop";

    transition_act = actionv "ac_trans_init_stop";

    dest = DPath [smain;sstop];

  }

  in

  let tinitreset = {

    event = no_event;

    condition = no_condition;

    condition_act  = actionv "ac_cond_init_reset";

    transition_act = actionv "ac_cond_init_stop";

    dest = DPath [smain;sstop;sreset];

  }

  in

  let treset = {

    event = event "LAP";

    condition = no_condition;

    condition_act  = action "reset counter";

    transition_act = actionv "ac_trans_reset_junction";

    dest = DJunction "jreset" (* [smain;sstop;sreset]; ou bien mettre une junction.  Verifier

				 si il y a des effets de bords non

				 desirés de fermeture/ouverture de

				 noeud *)

  }

  in

  let treset_start  = {

    event = event "START";

    condition = no_condition;

    condition_act  = actionv "ac_cond_reset->running";

    transition_act = actionv "ac_trans_reset->running";

    dest = DPath [smain;srun;srunning];

  }

  in

  let tlapstop_lap  = {

    event = event "LAP";

    condition = no_condition;

    condition_act  = actionv "ac_cond_lap_stop->reset";

    transition_act = actionv "ac_trans_lap_stop->reset";

    dest = DPath [smain;sstop;sreset];

  }

  in

  let tlapstop_start  = {

    event = event "START";

    condition = no_condition;

    condition_act  = actionv "ac_cond_lap_stop->lap";

    transition_act = actionv "ac_trans_lap_stop->lap";

    dest = DPath [smain;srun;slap];

  }

  in

  let ttic   = {

    event = event "TIC";

    condition = no_condition;

    condition_act  = action "cent+=1";

    transition_act = actionv "ac_trans_->J1";

    dest = DJunction "j1";

  }

  in

  let trunning_start  = {

    event = event "START";

    condition = no_condition;

    condition_act  = actionv "ac_cond_running->reset";

    transition_act = actionv "ac_trans_running->reset";

    dest = DPath [smain;sstop;sreset];

  }

  in

  let tlap_start  = {

    event = event "START";

    condition = no_condition;

    condition_act  = actionv "ac_cond_lap->lap_stop";

    transition_act = actionv "ac_trans_lap->lap_stop";

    dest = DPath [smain;sstop;slapstop];

  }

  in

  let tlap_lap  = {

    event = event "LAP";

    condition = no_condition;

    condition_act  = actionv "ac_cond_lap->running";

    transition_act = actionv "ac_trans_lap->running";

    dest = DPath [smain;srun;srunning];

  }

  in

  let trunning_lap  = {

    event = event "LAP";

    condition = no_condition;

    condition_act  = actionv "ac_cond_running->lap";

    transition_act = actionv "ac_trans_running->lap";

    dest = DPath [smain;srun;slap];

  }

  in

  let tj1j2 = {

    event = no_event;

    condition = condition "cent==100";

    condition_act  = action "cont=0;sec+=1";

    transition_act = actionv "ac_trans_J1->J2";

    dest = DJunction "j2";

  }

  in

  let tj1j3 =    {

    event = no_event;

    condition = condition "cent!=100";

    condition_act  = actionv "ac_cond_J1->J3";

    transition_act = actionv "ac_trans_J1->J3";

    dest = DJunction "j3";

  }

  in

  let tj2j3gauche   = {

    event = no_event;

    condition = condition "sec!=60";

    condition_act  = actionv "ac_cond_J2->J3_left";

    transition_act = actionv "ac_trans_J2->J3_left";

    dest = DJunction "j3";

  }

  in

  let tj2j3droite    = {

    event = no_event;

    condition = condition "sec==60";

    condition_act  = action "sec=0; min+=1";

    transition_act = actionv "ac_trans_J2->J3_right";

    dest = (*DPath [smain;srun];*) DJunction "j3";

  }

  in

  let def_main = {

    state_actions = {

      entry_act  = actionv "ac_main_entry";

      during_act = actionv "ac_main_during";

      exit_act   = actionv "ac_main_exit";

    };

    outer_trans = [];

    inner_trans = [];

    internal_composition = Or ([tinitstop], [sstop; srun])

  }

  in

  let def_stop = {

    state_actions = {

      entry_act  = actionv "ac_stop_entry";

      during_act = actionv "ac_stop_during";

      exit_act   = actionv "ac_stop_exit";

    };

    outer_trans = [];

    inner_trans = [];

    internal_composition = Or ([tinitreset], [sreset; slapstop])

  }

  in

  let def_reset = {

    state_actions = {

      entry_act  = actionv "ac_reset_entry";

      during_act = actionv "ac_reset_during";

      exit_act   = actionv "ac_reset_exit";

    };

    outer_trans = [treset_start];

    inner_trans = [treset];

    internal_composition = Or ([treset_start], [])

  }

  in

  let def_lapstop = {

    state_actions = {

      entry_act  = actionv "ac_lapstop_entry";

      during_act = actionv "ac_lapstop_during";

      exit_act   = actionv "ac_lapstop_exit";

    };

    outer_trans = [tlapstop_lap; tlapstop_start];

    inner_trans = [];

    internal_composition = Or ([], [])

  }

  in

  let def_run = {

    state_actions = {

      entry_act  = actionv "ac_run_entry";

      during_act = actionv "ac_run_during";

      exit_act   = actionv "ac_run_exit";

    };

    outer_trans = [];

    inner_trans = [ttic];

    internal_composition = Or ([], [srunning; slap])

  }

  in

  let def_running = {

    state_actions = {

      entry_act  = actionv "ac_running_entry";

      during_act = action "disp=(cent,sec,min)";

      exit_act   = actionv "ac_running_exit";

    };

    outer_trans = [trunning_start; trunning_lap];

    inner_trans = [];

    internal_composition = Or ([], [])

  }

  in

  let def_lap = {

    state_actions = {

      entry_act  = actionv "ac_lap_entry";

      during_act = actionv "ac_lap_during";

      exit_act   = actionv "ac_lap_exit";

    };

    outer_trans = [tlap_start; tlap_lap];

    inner_trans = [];

    internal_composition = Or ([], [])

  }

  in

  let src = [

    State([smain;srun;srunning], def_running);

    State([smain;srun;slap], def_lap);

    State([smain;srun], def_run);

    State([smain;sstop;sreset], def_reset);

    State([smain;sstop;slapstop], def_lapstop);

    State([smain;sstop], def_stop);

    State([smain], def_main);

    Junction("jreset", []);

    Junction("j1", [tj1j2;tj1j3]);

    Junction("j2", [tj2j3droite; tj2j3gauche]);

    Junction("j3", []);

  ]

  in

  (smain, src)

let traces : trace_t list =

  [

    [None; Some "TIC"; Some "START"; Some "TIC"; Some "TIC"];

    [None; Some "START"; Some "START"; Some "START"];

    [None; Some "START"; Some "TIC"; Some "START"; Some "TIC"]

  ]

open Basetypes 

open Datatype

open CPS_transformer

open Theta 

module Semantics = functor (T: TransformerType) (M: MODEL_T) ->

struct

module Prog =

struct

  let init = fst M.model

  let defs = snd M.model

  let vars = SF.states M.model

(*let _ = Format.printf "Model definitions@.%a@.####" Simulink.pp_src defs; () *)

end

module Interp = CPS_interpreter.Interpreter (T)

module KenvTheta = KenvTheta (T)

module Tables = KenvTheta.MemoThetaTables ()

let eval ((modular_entry:bool), (modular_during:bool), (modular_exit:bool)) =

  let module Modularity : KenvTheta.ModularType =

      struct

	let modular : type b. (path_t, b, bool) tag_t -> path_t -> b =

			fun tag ->

			  match tag with

			  | E -> (fun p p' f -> modular_entry)

			  | D -> (fun p      -> modular_during)

			  | X -> (fun p f    -> modular_exit)

      end

  in

  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 

let code_gen fmt modular  =

  let module Eval = (val (eval modular)) in

  let principal, components =  Eval.eval_prog, Eval.eval_components in

  Format.fprintf fmt "%a@." T.pp_principal principal;

  List.iter

    (fun (c, tr) -> Format.fprintf fmt "@.%a@." (fun fmt -> T.pp_component fmt Ecall c) tr)

    (components Ecall);

  List.iter

    (fun (c, tr) -> Format.fprintf fmt "@.%a@." (fun fmt -> T.pp_component fmt Dcall c) tr)

    (components Dcall);

  List.iter

    (fun (c, tr) -> Format.fprintf fmt "@.%a@." (fun fmt -> T.pp_component fmt Xcall c) tr)

    (components Xcall);

  ()

end

open Basetypes 

open Datatype

(* open ActiveEnv *)

open CPS_transformer

(* open Simulink *)

open Theta 

module Interpreter (Transformer : TransformerType) =

struct

  module KT = KenvTheta (Transformer)

  open KT

  let ( >? ) cond tr =

    if cond then tr else Transformer.null

  module type DenotationType =

  sig

    module Theta : MemoThetaType

    val eval_dest : destination_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t

    val eval_tau : trans_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t

    val eval_T : transitions_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t

    val eval_C : (path_t, 'b, Transformer.t) tag_t -> path_t -> composition_t -> Transformer.t

    val eval_open_path : mode_t -> path_t -> path_t -> Transformer.t wrapper_t

    val eval_S : (path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b

  end

  module type AbsDenotationType =

  sig

    val eval_dest : kenv_t -> destination_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t

    val eval_tau : kenv_t -> trans_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t

    val eval_T : kenv_t -> transitions_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t

    val eval_C : kenv_t -> (path_t, 'b, Transformer.t) tag_t -> path_t -> composition_t -> Transformer.t

    val eval_open_path : kenv_t -> mode_t -> path_t -> path_t -> Transformer.t wrapper_t

    val eval_S : kenv_t -> (path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b

  end

  module AbstractKenv (Denot : functor (Kenv : KenvType) -> DenotationType) : AbsDenotationType =

  struct

    let eval_dest kenv =

      let module Kenv =

	  struct

	    let kenv = kenv

	  end in

      let module D = Denot (Kenv) in

      D.eval_dest

    let eval_tau kenv =

      let module Kenv =

	  struct

	    let kenv = kenv

	  end in

      let module D = Denot (Kenv) in

      D.eval_tau

    let eval_T kenv =

      let module Kenv =

	  struct

	    let kenv = kenv

	  end in

      let module D = Denot (Kenv) in

      D.eval_T

    let eval_C kenv =

      let module Kenv =

	  struct

	    let kenv = kenv

	  end in

      let module D = Denot (Kenv) in

      D.eval_C

    let eval_open_path kenv =

      let module Kenv =

	  struct

	    let kenv = kenv

	  end in

      let module D = Denot (Kenv) in

      D.eval_open_path

    let eval_S kenv =

      let module Kenv =

	  struct

	    let kenv = kenv

	  end in

      let module D = Denot (Kenv) in

      D.eval_S

  end

  module Denotation : functor (Thetaify : ThetaifyType) (Kenv : KenvType) -> DenotationType =

  functor (Thetaify : ThetaifyType) (Kenv : KenvType) ->

  struct

    module Theta = Thetaify (Kenv)

    let eval_dest dest wrapper success fail =

      Log.log (fun fmt -> Format.fprintf fmt "@[<v 2>D[[%a]]@ " SF.pp_dest dest);

      match dest with

      | DPath p -> wrapper p (success p)

      | DJunction j -> Theta.theta J j wrapper success fail

    let eval_tau trans wrapper success fail =

      Log.log (fun fmt -> Format.fprintf fmt "@[<v 2>tau[[%a]]@ " SF.pp_trans trans);

      let success' p =

	Transformer.(success p >> eval_act (module Theta) trans.transition_act)

      in

      let cond = Transformer.(event trans.event && trans.condition) in

      Transformer.(eval_cond cond

		     (eval_act (module Theta) trans.condition_act >> eval_dest trans.dest wrapper success' fail)

		     fail.local)

    let rec eval_T tl wrapper success fail =

      Log.log ~debug:false (fun fmt -> Format.fprintf fmt "@[<v 2>T[[%a]]@ " SF.pp_transitions tl);

      match tl with

      | [] -> fail.global

      | t::[] ->  eval_tau t wrapper success fail

      | t::tl ->

	 let fail' = { fail with local = eval_T tl wrapper success fail } in

	 eval_tau t wrapper success fail'

    let frontier path =

      match path with

      | []   -> [], []

      | t::q -> [t], q

    let rec eval_open_path mode p p1 p2 success_p2 =

      Log.log ~debug:false (fun fmt -> Format.fprintf fmt "@[<v 2>open_path_rec[[mode %a, prefix %a, src %a, dst %a]]@ " pp_mode mode pp_path p pp_path p1 pp_path p2);

      match frontier p1, frontier p2 with

      | ([x], ps), ([y], pd) when x = y -> eval_open_path mode (p@[x]) ps pd success_p2

      | (x  , _ ), (y  , pd)            ->

	 match mode with

	 | Outer -> (Transformer.(Theta.theta X (p@x) Loose  >> success_p2 >> Theta.theta E (p@y) pd Loose))

	 | Inner -> (assert (x = []);

		     Transformer.(Theta.theta X (p@x) Strict >> success_p2 >> Theta.theta E (p@y) pd Strict))

	 | Enter -> (assert (x = [] && y <> []);

		     Transformer.(                              success_p2 >> Theta.theta E (p@y) pd Loose))

    let rec eval_C : type a b. (a, b, Transformer.t) tag_t -> path_t -> composition_t -> Transformer.t =

      fun tag prefix comp ->

	match tag with

	| E -> Transformer.(

	  Log.log ~debug:false (fun fmt -> Format.fprintf fmt "@[<v 2>C_%a[[%a, %a]]@ " pp_tag tag pp_path prefix SF.pp_comp comp);

	  match comp with

	  | Or (_T, [])   -> null

	  | Or ([], [s0]) -> eval_open_path Enter prefix [] [s0] null

	  | Or (_T, _S)   -> let wrapper = eval_open_path Enter [] prefix in

			     let success p_d = null in

			     eval_T _T wrapper success { local = bot; global = bot }

	  | And (_S)    -> List.fold_right (fun p -> (>>) (Theta.theta E (prefix@[p]) [] Loose)) _S null

	)

	| D -> Transformer.(

	  match comp with

	  | Or (_T, [])    -> null

	  | Or (_T, p::_S) -> eval_cond (active (prefix@[p])) (Theta.theta D (prefix@[p])) (eval_C D prefix (Or (_T, _S)))

	  | And (_S)       -> List.fold_right (fun p -> (>>) (Theta.theta D (prefix@[p]))) _S null

	)

	| X -> Transformer.(

	  match comp with

	  | Or (_T, [])    -> null

	  | Or (_T, p::_S) -> eval_cond (active (prefix@[p])) (Theta.theta X (prefix@[p]) Loose) (eval_C X prefix (Or (_T, _S)))

	  | And (_S)       -> List.fold_right (fun p -> (>>) (Theta.theta X (prefix@[p]) Loose)) _S null

	)

	| J -> assert false

    let eval_S : type b. (path_t, b, Transformer.t) tag_t -> path_t -> state_def_t -> b =

      fun tag p p_def ->

	match tag with

	| E -> fun path frontier -> Transformer.(

	  Log.log ~debug:false (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))) >> 

	  match path with

	  | []         -> eval_C E p p_def.internal_composition

	  | s::path_tl -> Theta.theta E (p@[s]) path_tl Loose

	)

	| D -> Transformer.(

	  Log.log ~debug:false (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a]]@ " pp_tag tag pp_path p);

	  let wrapper_i = eval_open_path Inner [] p in

	  let wrapper_o = eval_open_path Outer [] p in

	  let success p_d = null in

	  let fail_o =

	    let fail_i =

	      let same_fail_C = eval_C D p p_def.internal_composition in

	      { local = same_fail_C; global = same_fail_C }

	    in

	    let same_fail_i = eval_act (module Theta) p_def.state_actions.during_act >> eval_T p_def.inner_trans wrapper_i success fail_i in

	    { local = same_fail_i; global = same_fail_i }

	  in

	  eval_T p_def.outer_trans wrapper_o success fail_o

	)

	| X -> fun frontier -> Transformer.(

	  Log.log ~debug:false (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a, frontier %a]]@ " pp_tag tag pp_path p pp_frontier frontier);

	  eval_C X p p_def.internal_composition >>

	  ((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.exit_act >> eval_act (module Theta) (close_path p)))

	)

  end

  module type ProgType =

  sig

    val init : state_name_t

    val defs : src_components_t list

  end

  module type EvaluationType =

  sig

    module Theta : ThetaType with type t = Transformer.t

    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)

    module AbsDenotation = AbstractKenv (Denotation)

    include AbsDenotation

    module Kenv : KenvType =

    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

    end

    module AppDenotation = Denotation (Kenv)

    module Theta = AppDenotation.Theta

    let eval_components = Theta.components

    let eval_prog =

      Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] [] Loose))

  end

 (*

  module ThetaFix (Prog : ProgType) (Theta : ThetaType) : ThetaType =

  struct

    include Denotation (Theta)

    let theta =

      let kenv =

	List.fold_left (

	  fun accu d -> match d with

	  | State (p, defp) -> { accu with cont_node = (p, (eval_S E p defp, eval_S D p defp, eval_S X p defp))::accu.cont_node  }

	  | Junction (j, defj) -> { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc  }

	) {cont_node = []; cont_junc = []} Prog.defs

      in Obj.magic (fun tag -> theta_ify kenv tag)

  end

  module Rec (Prog : ProgType) =

  struct

    module rec Theta : ThetaType = ThetaFix (Prog) (Theta)

  end

  module Eval (Prog : ProgType) : EvaluationType =

  struct

    module RecTheta = Rec (Prog)

    module Theta = RecTheta.Theta

    let eval_prog =

	Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] []))

  end

  module Eval (Prog : ProgType) =

  struct

    module ThetaFunctor (Evaluation : EvaluationType) : ThetaType =

    struct

      let theta tag = (theta_ify Evaluation.kenv) tag

    end

    module EvaluationFunctor (Theta : ThetaType) : EvaluationType =

    struct

      include Denotation (Theta)

      let kenv =

	List.fold_left (

	  fun accu d -> match d with

	  | State (p, defp) -> { accu with cont_node = (p, (fun kenv -> eval_S E p defp, eval_S D p defp, eval_S X p defp))::accu.cont_node  }

	  | Junction (j, defj) -> { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc  }

	) {cont_node = []; cont_junc = []} Prog.defs

      let eval_prog =

	Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] []))

    end

    module rec Theta : ThetaType = ThetaFunctor (Evaluation)

    and Evaluation : EvaluationType = EvaluationFunctor (Theta)

end

  *)

end

open Basetypes

open ActiveStates

type mode_t =

  | Outer

  | Inner

  | Enter

type 't success_t = path_t -> 't

type 't fail_t = { local: 't; global: 't }

type 't wrapper_t = path_t -> 't -> 't

type ('a, 'b, 't) tag_t =

  | E : (path_t, path_t -> frontier_t -> 't, 't) tag_t

  | D : (path_t, 't, 't) tag_t

  | X : (path_t, frontier_t -> 't, 't) tag_t

  | J : (junction_name_t, 't wrapper_t -> 't success_t -> 't fail_t -> 't, 't) tag_t

type ('a, 'b, 't) theta_t = ('a, 'b, 't) tag_t -> 'a -> 'b

module type ThetaType =

sig

  type t

  val theta : ('a, 'b, t) theta_t

end

let pp_mode fmt mode =

  match mode with

  | Outer -> Format.fprintf fmt "Outer"

  | Inner -> Format.fprintf fmt "Inner"

  | Enter -> Format.fprintf fmt "Enter"

let pp_tag : type a b t. Format.formatter -> (a, b, t) tag_t -> unit =

  fun fmt tag ->

    match tag with

    | E -> Format.fprintf fmt "e"

    | D -> Format.fprintf fmt "d"

    | X -> Format.fprintf fmt "x"

    | J -> Format.fprintf fmt "j"

(*

module Proj1Theta (T : sig type t1 val bot1 : t1 type t2 val bot2 : t2 end) (Theta : ThetaType with type t = T.t1 * T.t2) : ThetaType with type t = T.t1 =

struct

  type t = T.t1

  let f f1 = (f1, T.bot2)

  let s s1 p = (s1 p, T.bot2)

  let w w1 p (tr1, _) = (w1 p tr1, T.bot2)

  let theta : type a b. (a, b, t) theta_t =

    fun tag ->

    match tag with

    | E -> (fun p p' f     -> fst (Theta.theta E p p' f))

    | D -> (fun p          -> fst (Theta.theta D p))

    | X -> (fun p f        -> fst (Theta.theta X p f))

    | J -> (fun j w1 s1 f1 -> fst (Theta.theta J j (w w1) (s s1) (f f1)))

end

module Proj2Theta (T : sig type t1 val bot1 : t1 type t2 val bot2 : t2 end) (Theta : ThetaType with type t = T.t1 * T.t2) : ThetaType with type t = T.t2 =

struct

  type t = T.t2

  let f f2 = (T.bot1, f2)

  let s s2 p = (T.bot1, s2 p)

  let w w2 p (_, tr2) = (T.bot1, w2 p tr2)

  let theta : type a b. (a, b, t) theta_t =

    fun tag ->

    match tag with

    | E -> (fun p p' f     -> snd (Theta.theta E p p' f))

    | D -> (fun p          -> snd (Theta.theta D p))

    | X -> (fun p f        -> snd (Theta.theta X p f))

    | J -> (fun j w2 s2 f2 -> snd (Theta.theta J j (w w2) (s s2) (f f2)))

end

*)

module TransformerStub =

struct

  type act_t = Action.t

  type cond_t = Condition.t

  let nil = Action.nil

  let aquote = Action.aquote

  let open_path = Action.open_path

  let close_path = Action.close_path

  let call = Action.call

  let pp_act = Action.pp_act

  let cquote = Condition.cquote

  let tru = Condition.tru

  let event = Condition.event

  let active = Condition.active

  let ( && ) = Condition.( && )

  let neg = Condition.neg

  let pp_cond = Condition.pp_cond

end

module type TransformerType =

sig

  type act_t = Action.t

  type cond_t = Condition.t

  type t

  include ActionType with type t := act_t

  include ConditionType with type t := cond_t

  val null : t

  val bot : t

  val ( >> ) : t -> t -> t

  val eval_act : (module ThetaType with type t = t) -> act_t -> t

  val eval_cond : cond_t -> t -> t -> t

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

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

  val pp_component : Format.formatter -> 'c call_t -> 'c -> t -> unit

end

module type ComparableTransformerType =

sig

  include TransformerType

  val ( == ) : t -> t -> bool

end

(*

module Pair (T1 : ComparableTransformerType) (T2 : TransformerType) : ComparableTransformerType with type t = T1.t * T2.t =

struct

  include TransformerStub

  type t = T1.t * T2.t

  module T =

  struct

    type t1 = T1.t

    type t2 = T2.t

    let bot1 = T1.bot

    let bot2 = T2.bot

  end

  let null = T1.null, T2.null

  let bot = T1.bot, T2.bot

  let ( >> ) (tr11, tr12) (tr21, tr22) =

    T1.(tr11 >> tr21), T2.(tr12 >> tr22)

  let eval_act theta action =

    let module Theta = (val theta : ThetaType with type t = T1.t * T2.t) in

    let theta1 = (module Proj1Theta (T) (Theta) : ThetaType with type t = T1.t) in

    let theta2 = (module Proj2Theta (T) (Theta) : ThetaType with type t = T2.t) in

    T1.eval_act theta1 action, T2.eval_act theta2 action

  let eval_cond cond (trt1, trt2) (tre1, tre2) =

    T1.eval_cond cond trt1 tre1, T2.eval_cond cond trt2 tre2

  let ( == ) (tr1, _) (tr2, _) = T1.(tr1 == tr2)

  let pp_transformer fmt (tr1, tr2) =

    Format.fprintf fmt "< %a , %a >" T1.pp_transformer tr1 T2.pp_transformer tr2

  let pp_principal fmt (tr1, tr2) =

    Format.fprintf fmt "< %a , %a >" T1.pp_principal tr1 T2.pp_principal tr2

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

    fun fmt call ->

    match call with

    | Ecall -> (fun c (tr1, tr2) ->

      Format.fprintf fmt "< %t , %t >"

	(fun fmt -> T1.pp_component fmt Ecall c tr1)

	(fun fmt -> T2.pp_component fmt Ecall c tr2))

    | Dcall -> (fun c (tr1, tr2) ->

      Format.fprintf fmt "< %t , %t >"

	(fun fmt -> T1.pp_component fmt Dcall c tr1)

	(fun fmt -> T2.pp_component fmt Dcall c tr2))

    | Xcall -> (fun c (tr1, tr2) ->

      Format.fprintf fmt "< %t , %t >"

	(fun fmt -> T1.pp_component fmt Xcall c tr1)

	(fun fmt -> T2.pp_component fmt Xcall c tr2))

end

*)

module Evaluator : TransformerType with type t = (event_t * bool ActiveStates.Env.t * base_action_t list -> event_t * bool ActiveStates.Env.t * base_action_t list ) =

struct

  include TransformerStub

  type env_t = event_t * bool ActiveStates.Env.t * base_action_t list (* Don't care for values yet *)

  type t = env_t -> env_t

  let null rho = rho

  let add_action a (evt, rho, al) = (evt, rho, al@[a]) (* not very efficient but

							  avoid to keep track of

							  action order *)

  let bot _ = assert false

  let ( >> ) tr1 tr2 = fun rho -> rho |> tr1 |> tr2

  let ( ?? ) b tr = if b then tr else null

  let eval_open p (evt, rho, al)  = (evt, ActiveStates.Env.add p true rho, al)

  let eval_close p (evt, rho, al) = (evt, ActiveStates.Env.add p false rho, al)

  let eval_call : type c. (module ThetaType with type t = t) -> c call_t -> c -> t =

    fun kenv ->

    let module Theta = (val kenv : ThetaType with type t = t) in	      

    fun call -> match call with

    | Ecall -> (fun (p, p', f) -> Theta.theta E p p' f)

    | Dcall -> (fun p          -> Theta.theta D p)

    | Xcall -> (fun (p, f)     -> Theta.theta X p f)

  let eval_act kenv action =

    (* Format.printf "----- action = %a@." Action.pp_act action; *)

    match action with

    | Action.Call (c, a)      -> eval_call kenv c a

    | Action.Quote a          -> add_action a

    | Action.Open p           -> eval_open p

    | Action.Close p          -> eval_close p

    | Action.Nil              -> null

  (*if (match trans.event with None -> true | _ -> e = trans.event) && trans.condition rho*)

  let rec eval_cond condition ok ko =

    (* Format.printf "----- cond = %a@." Condition.pp_cond condition; *)

    match condition with

    | Condition.True               -> ok

    | Condition.Active p           -> (fun ((evt, env, al) as rho) -> if ActiveStates.Env.find p env then ok rho else ko rho)

    | Condition.Event e            -> (fun ((evt, env, al) as rho) -> match evt with None -> ko rho | Some e' -> if e=e' then ok rho else ko rho)

    | Condition.Neg cond           -> eval_cond cond ko ok

    | Condition.And (cond1, cond2) -> eval_cond cond1 (eval_cond cond2 ok ko) ko

    | Condition.Quote c            -> add_action c >> ok (* invalid behavior but similar to the other: should evaluate condition *)

  let pp_transformer fmt tr =

    Format.fprintf fmt "<transformer>"

  let pp_principal fmt tr =

    Format.fprintf fmt "principal =@.%a" pp_transformer tr

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

    fun fmt call -> match call with

    | Ecall -> (fun (p, p', f) tr ->

      Format.fprintf fmt "component %a(%a, %a, %a) =@.%a" pp_call call pp_path p pp_path p' pp_frontier f pp_transformer tr)

    | Dcall -> (fun p tr ->

      Format.fprintf fmt "component %a(%a) =@.%a" pp_call call pp_path p pp_transformer tr)

    | Xcall -> (fun (p, f) tr ->

      Format.fprintf fmt "component %a(%a, %a) =@.%a" pp_call call pp_path p pp_frontier f pp_transformer tr)

end

module CodeGenerator : ComparableTransformerType =

struct

  include TransformerStub

  type t =

  | Bot

  | Act of act_t

  | Seq of t list

  | Ite of cond_t * t * t

  let null = Seq []

  let bot = Bot

  let ( >> ) tr1 tr2 =

    match tr1, tr2 with

    | Seq trl1, Seq trl2 -> Seq (trl1@trl2)

    | Seq trl1, _        -> Seq (trl1@[tr2])

    | _       , Seq trl2 -> Seq (tr1::trl2)

    | _                  -> Seq ([tr1;tr2])

  let rec ( == ) tr1 tr2 = tr1 = tr2

  let eval_act kenv (action : act_t) =

    (*Format.printf "----- action = %a@." Action.pp_act action;*)

    Act action

  (*if (match trans.event with None -> true | _ -> e = trans.event) && trans.condition rho*)

  let rec eval_cond condition ok ko =

    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)

    Ite (condition, ok, ko)

  let rec pp_transformer fmt tr =

    match tr with

    | Bot           -> Format.fprintf fmt "bot"

    | Act a         ->

       Format.fprintf fmt "<%a>" pp_act a

    | Seq trl       ->

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

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

	 trl

    | Ite (c, t, e) ->

       Format.fprintf fmt "@[<v 0>if %a@ @[<v 2>then@ %a@]@ @[<v 2>else@ %a@]@ endif@]" pp_cond c pp_transformer t pp_transformer e

  let pp_principal fmt tr =

    Format.fprintf fmt "principal =@.%a" pp_transformer tr

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

    fun fmt call -> match call with

    | Ecall -> (fun (p, p', f) tr ->

      Format.fprintf fmt "component %a(%a, %a, %a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_path p' pp_frontier f pp_transformer tr)

    | Dcall -> (fun p tr ->

      Format.fprintf fmt "component %a(%a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_transformer tr)

    | Xcall -> (fun (p, f) tr ->

      Format.fprintf fmt "component %a(%a, %a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_frontier f pp_transformer tr)

end

module LustrePrinter (Vars : sig val vars : ActiveStates.Vars.t end) : TransformerType =

struct

  include TransformerStub

  type name_t = string

  type t = name_t -> name_t -> (ActiveStates.Vars.t * (Format.formatter -> unit))

  let new_loc, reset_loc =