heptagon/compiler/minils/ctrln/ctrlNbacGen.ml

(***********************************************************************)
(*                                                                     *)
(*                             Heptagon                                *)
(*                                                                     *)
(* Gwenael Delaval, LIG/INRIA, UJF                                     *)
(* Leonard Gerard, Parkas, ENS                                         *)
(* Adrien Guatto, Parkas, ENS                                          *)
(* Cedric Pasteur, Parkas, ENS                                         *)
(* Marc Pouzet, Parkas, ENS                                            *)
(* Nicolas Berthier, SUMO, INRIA                                       *)
(*                                                                     *)
(* Copyright 2013 ENS, INRIA, UJF                                      *)
(*                                                                     *)
(* This file is part of the Heptagon compiler.                         *)
(*                                                                     *)
(* Heptagon is free software: you can redistribute it and/or modify it *)
(* under the terms of the GNU General Public License as published by   *)
(* the Free Software Foundation, either version 3 of the License, or   *)
(* (at your option) any later version.                                 *)
(*                                                                     *)
(* Heptagon is distributed in the hope that it will be useful,         *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of      *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the       *)
(* GNU General Public License for more details.                        *)
(*                                                                     *)
(* You should have received a copy of the GNU General Public License   *)
(* along with Heptagon.  If not, see <http://www.gnu.org/licenses/>    *)
(*                                                                     *)
(***********************************************************************)

(** Translation from the source language to Controllable-Nbac

    @author Nicolas Berthier *)

(* -------------------------------------------------------------------------- *)

open Ctrln_utils
open Signature
open Types
open Names
open Idents
open Minils
open CtrlNbac
open AST

let (&) f g = f g

exception Untranslatable of string                    (* XXX not catched yet! *)

(* --- *)

let tt = mk_bcst' true
let ff = mk_bcst' false

(* --- *)

(** Private record gathering temporary generation data *)
type 'f gen_data =
    {
      typdefs: 'f typdefs;
      decls: 'f node_decls;
      base: (var_ident * ty) SMap.t;
      local: (var_ident * ty) SMap.t;
      contrs: (var_ident * ty) SMap.t;
      output: IdentSet.t;
      init_cond: 'f bexp;
      init_state: 'f bexp;
      assertion: 'f bexp;
      invariant: 'f bexp;
      (* reachable: bexp; *)
      remaining_contrs: SSet.t;      (* All controllable inputs that has not yet
                                        been assigned to a U/C group. *)
      local_contr_deps: SSet.t SMap.t;         (* All variables that depend on a
                                                  controllable. *)
      extra_inputs: SSet.t;
      uc_groups: (SSet.t * SSet.t) list;
    }

(* --- *)

let mk_gen_data typdefs decls input local output init_cond =
  {
    typdefs;
    decls;
    base = input;
    local;
    contrs = SMap.empty;
    output;
    remaining_contrs = SSet.empty;
    local_contr_deps = SMap.empty;
    extra_inputs = SSet.empty;
    uc_groups = [];
    init_cond;
    init_state = tt;
    assertion = tt;
    invariant = tt;
  }

(* --- *)

let translate_constr { name } = mk_label & mk_symb name (* XXX use qual name? *)
let translate_constrs cl = mk_etyp (List.map translate_constr cl)

(* --- *)

let translate_typ typ = match Modules.unalias_type typ with
  | Tid ({ qual = Pervasives; name = "bool" }) -> `Bool
  | Tid ({ qual = Pervasives; name = "int" }) -> `Int
  | Tid ({ qual = Pervasives; name = "real" }) -> `Real                (* XXX? *)
  | Tid ({ name = tn } as t) -> (match Modules.find_type t with
      | Tenum _ -> `Enum (mk_typname (mk_symb tn))
      | _ -> raise & Untranslatable ("type "^ fullname t))
  | Tprod _ -> raise & Untranslatable ("product type")
  | Tarray _ -> raise & Untranslatable ("array type")
  | Tinvalid -> failwith "Encountered an invalid type!"

let ref_of_ty ty = match translate_typ ty with
  | `Bool -> mk_bref
  | `Enum _ -> mk_eref
  | `Int | `Real -> mk_nref

(* --- *)

let simplify_static_exp se = (Static.simplify QualEnv.empty se).se_desc

let translate_static_bexp se = match simplify_static_exp se with
  | Sbool true | Sconstructor { qual = Pervasives; name = "true" } -> tt
  | Sbool false | Sconstructor { qual = Pervasives; name = "false" } -> ff
  | _ -> failwith ("Boolean static expression expected!")

let translate_static_eexp se = match simplify_static_exp se with
  | Sconstructor { qual = Pervasives; name = "true" as n }
  | Sconstructor { qual = Pervasives; name = "false" as n } ->
      failwith ("Enum static expression expected! (found `"^n^"')")
  | Sconstructor c -> `Enum (translate_constr c)
  | _ -> failwith ("Enum static expression expected!")

let translate_static_nexp se = match simplify_static_exp se with
  | Sint v -> `Int v
  | Sfloat v -> `Real v
  | Sop ({ qual = Pervasives; name="~-" },[{ se_desc = Sint v }]) -> `Int (-v)
  | Sop ({ qual = Pervasives; name="~-." },[{ se_desc=Sfloat v }]) -> `Real (-.v)
  | _ -> failwith ("Numerical static expression expected!")

(* --- *)

let rec translate_ext_bexp ~pref : _ -> 'f bexp = function
  | Wconst se -> translate_static_bexp se
  | Wvar id -> mk_bref' (pref & mk_symb & name id)
  | Wfield _ -> failwith "TODO Unsupported Boolean `field' expression!"
  | Wwhen (ev, _, _) -> translate_ext_bexp ~pref ev.w_desc
  | Wreinit _ -> failwith "TODO Unsupported Boolean `reinit' expression!"

and translate_ext_eexp ~pref : _ -> 'f eexp = function
  | Wconst se -> translate_static_eexp se
  | Wvar id -> mk_eref' (pref & mk_symb & name id)
  | Wwhen (ev, _, _) -> translate_ext_eexp ~pref ev.w_desc
  | _ -> failwith "TODO Unsupported Enum expression!"

and translate_ext_nexp ~pref : _ -> 'f nexp = function
  | Wconst se -> translate_static_nexp se
  | Wvar id -> mk_nref' (pref & mk_symb & name id)
  | Wwhen (ev, _, _) -> translate_ext_nexp ~pref ev.w_desc
  | _ -> failwith "TODO Unsupported Numerical expression!"

let translate_ext ~pref ext = match translate_typ ext.w_ty with
    | `Bool -> `Bexp (translate_ext_bexp ~pref ext.w_desc)
    | `Enum _ -> `Eexp (translate_ext_eexp ~pref ext.w_desc)
    | `Int | `Real -> `Nexp (translate_ext_nexp ~pref ext.w_desc)

(* --- *)

let translate_app ~pref op el =
  let pervasives = function
    | "not",          [e]   -> mk_neg e
    | "or",           e::l  -> mk_disj e l
    | "&",            e::l  -> mk_conj e l
    | "xor",         [e;f]  -> mk_xor e f
    | "=",           [e;f]  -> mk_eq e f
    | "<>",          [e;f]  -> mk_ne e f
    |("<"  | "<."),  [e;f]  -> mk_lt e f
    |("<=" | "<=."), [e;f]  -> mk_le e f
    |(">"  | ">."),  [e;f]  -> mk_gt e f
    |(">=" | ">=."), [e;f]  -> mk_ge e f
    |("+"  | "+."), e::f::l -> mk_sum e f l
    |("-"  | "-."), e::f::l -> mk_sub e f l
    |("*"  | "*."), e::f::l -> mk_mul e f l
    |("/"  | "/."), e::f::l -> mk_div e f l
    | name, _ -> raise (Untranslatable name)
  in
  match op, List.map (translate_ext ~pref) el with
    | Eequal, [e;f] -> mk_eq e f
    | Efun { qual = Pervasives; name }, el -> pervasives (name, el)
    | Eifthenelse, [c;t;e] -> mk_cond c t e
    | _ -> failwith "Unsupported application!"

(** [translate_exp gd e] translates the {e memoryless} expression [e] into its
    Controllable Nbac representation.  *)
let rec translate_exp ~pref ({ e_desc = desc }) =               (* XXX clock? *)
  match desc with
    | Eextvalue ext -> translate_ext ~pref ext
    | Eapp ({ a_op }, el, _) -> translate_app ~pref a_op el
    | Emerge (v, (_c, e) :: l) ->
        let v = pref & mk_symb & name v in
        List.fold_left
          (fun x (c, e) -> mk_cond
            (mk_eq (mk_eref v) (mk_ecst (translate_constr c)))
            (translate_ext ~pref e) x)
          (translate_ext ~pref e)
          l
    | Ewhen (exp, _, _) -> translate_exp ~pref exp
    | Efby _ -> failwith "TODO: translate_exp (fby)"
    | Estruct _ -> failwith "TODO: translate_exp (struct)"
    | _ -> failwith "TODO: translate_exp"

(* --- *)

let rec translate_clk ~pref on off = function
  | Clocks.Cbase | Clocks.Cvar { contents = Clocks.Cindex _ } -> on
  | Clocks.Cvar { contents = Clocks.Clink ck } -> translate_clk ~pref on off ck
  | Clocks.Con (ck, {name = cstr}, v) ->
      let v = pref & mk_symb & name v in
      let c = mk_eq (mk_eref v) (mk_ecst (mk_label (mk_symb cstr))) in
      translate_clk ~pref (mk_cond c on off) off ck

(* --- *)

let acc_dependencies_on vars deps_on_vars i e = fold_exp_dependencies
  (fun v s ->
    if SSet.mem v vars then SSet.add v s
    else try SSet.union s (SMap.find v deps_on_vars) with
      | Not_found -> s)
  e i

(* --- *)

let add_state_var' ~pref gd id ty exp init =
  let v = pref & mk_symb & name id in
  let typ = translate_typ ty in
  let mk_init = match typ, init with
    | _,       None   -> (fun b -> b)
    | `Bool,   Some i -> mk_and' (mk_beq' (mk_bref' v) (translate_static_bexp i))
    | `Enum _, Some i -> mk_and' (mk_eeq' (mk_eref' v) (translate_static_eexp i))
    | #ntyp,   Some i -> mk_and' (mk_neq' (mk_nref' v) (translate_static_nexp i))
  in
  { gd with
    decls = SMap.add v (typ, `State (exp, None), None) gd.decls;
    init_state = mk_init gd.init_state; }, v

let add_state_var ~pref gd id ty exp init =
  let gd, v = add_state_var' ~pref gd id ty exp init in
  { gd with base = SMap.add v (id, ty) gd.base; }

let add_output_var ~pref gd id ty exp =
  add_state_var' ~pref gd id ty exp None |> fst


let add_local_var ~pref gd id ty exp =
  let v = pref & mk_symb & name id in
  let typ = translate_typ ty in
  let ldeps = fold_exp_dependencies (fun v acc ->
    if SSet.mem v gd.remaining_contrs then SSet.add v acc
    else try SSet.union acc (SMap.find v gd.local_contr_deps) with
      | Not_found -> acc)
    exp
    SSet.empty
  in
  let local_contr_deps = SMap.add v ldeps gd.local_contr_deps in
  { gd with
    decls = SMap.add v (typ, `Local (exp, None), None) gd.decls;
    local_contr_deps; }

let declare_additional_input ~pref gd id =
  let l = mk_symb & name id in
  try
    let v = pref l in
    let t = SMap.find l gd.local |> snd |> translate_typ in
    { gd with
      decls = SMap.add v (t, `Input one, None) gd.decls;
      extra_inputs = SSet.add v gd.extra_inputs; }
  with
    | Not_found ->                                 (* output of the main node. *)
        assert (IdentSet.mem id gd.output);
        gd

(* --- *)

let close_uc_group gd defined_contrs =
  let rem = SSet.diff gd.remaining_contrs defined_contrs in
  let lcd = SMap.map (SSet.inter rem) gd.local_contr_deps in
  let lcd = SMap.filter (fun _ d -> not (SSet.is_empty d)) lcd in
  { gd with
    remaining_contrs = rem;
    extra_inputs = SSet.empty;
    local_contr_deps = lcd;
    uc_groups = (gd.extra_inputs, defined_contrs) :: gd.uc_groups; }

(* --- *)

let pat_ids pat =
  let rec acc_pat acc = function
    | Evarpat id -> ((* pref &  *)(* mk_symb & name  *)id) :: acc
    | Etuplepat pats -> List.fold_left acc_pat acc pats
  in
  acc_pat [] pat |> List.rev

let translate_abstract_app ~pref gd pat _f args =
  let results = pat_ids (* ~pref *) pat in
  let args = List.map (translate_ext ~pref) args in
  let gd =
    (* in case of dependencies on remainging controllable variables, switch to
       next U/C group. *)
    let depc = List.fold_left
      (acc_dependencies_on gd.remaining_contrs gd.local_contr_deps)
      SSet.empty args
    in
    if SSet.is_empty depc then gd else close_uc_group gd depc
  in
  (* declare extra inputs. *)
  (List.fold_left (declare_additional_input ~pref) gd results, [])

(* --- *)

let translate_eq ~pref (gd, equs)
    ({ eq_lhs = pat;
       eq_rhs = { e_desc = exp; e_ty = ty } as rhs;
       eq_base_ck = clk } as eq)
    =
  match pat with
    | Evarpat id ->
        begin match exp with
          | Efby (init, ev) ->
              let v = pref & mk_symb & name id in
              let ev = translate_ext ~pref ev in
              let ev = translate_clk ~pref ev (ref_of_ty ty v) clk in
              (add_state_var ~pref gd id ty ev init, eq :: equs)
          | Eapp ({ a_op = (Enode f | Efun f) }, args, None)
                when f.qual <> Pervasives ->
              let gd, equs' = translate_abstract_app ~pref gd pat f args in
              (gd, eq :: equs' @ equs)
          | _ when IdentSet.mem id gd.output ->
              (add_output_var ~pref gd id ty (translate_exp ~pref rhs),
               eq :: equs)
          | _ ->
              (add_local_var ~pref gd id ty (translate_exp ~pref rhs),
               eq :: equs)
        end
    | Etuplepat _ ->
        begin match exp with
          | Eapp ({ a_op = (Enode f | Efun f) }, args, None)
                when f.qual <> Pervasives ->
              let gd, equs' = translate_abstract_app ~pref gd pat f args in
              (gd, eq :: equs' @ equs)
          | _ -> failwith "TODO: Minils.Etuplepat construct!"
        end

let translate_eqs ~pref acc equs =
  let gd, equs = List.fold_left (translate_eq ~pref) acc equs in
  gd, List.rev equs

(* --- *)

let prefix_vars ~pref vars : symb -> symb =
  let vars = List.fold_left begin fun acc { v_ident = id } ->
    let v = mk_symb & name id in
    SMap.add v (mk_symb ("c_" ^ Symb.to_string v)) acc
  end (SMap.empty) vars in
  fun p -> pref (try SMap.find p vars with Not_found -> p)

let declare_contr (decls, contrs, vds)
    ({ v_ident = id; v_type = ty } as vd) rank =
  let v = mk_symb & name id in
  SMap.add v (translate_typ ty, `Contr (one, rank, None), None) decls,
  SMap.add v (id, ty) contrs,
  vd :: vds

(** Contract translation *)
let translate_contract ~pref gd
    ({ c_local;           c_eq = equs;
       c_assume = a;      c_enforce = g;
       c_assume_loc = a'; c_enforce_loc = g';
       c_controllables = cl } as contract) =
  let declare_contrs acc cl =
    fst & List.fold_left
      (fun (acc, rank) c -> (declare_contr acc c rank, AST.succ rank))
      (acc, one) cl
  in

  let pref = prefix_vars ~pref c_local in
  let decls, contrs, locals = declare_contrs (gd.decls, SMap.empty, []) cl in
  let c = SMap.fold (fun v _ -> SSet.add v) contrs SSet.empty in
  let gd = { gd with decls; contrs; remaining_contrs = c; } in
  let gd, equs' = translate_eqs ~pref (gd, []) equs in
  let ak = as_bexp & mk_and (translate_ext ~pref a) (translate_ext ~pref a')
  and ok = as_bexp & mk_and (translate_ext ~pref g) (translate_ext ~pref g') in

  let gd, ok =
    if !Compiler_options.nosink
    then (gd, ok)
    else let sink = gen_var "" sink_state_str in
         let sink_expr = mk_bref' & pref & mk_symb & name sink in
         let ok = `Bexp ((* mk_bcond' gd.init_cond tt *) ok) in
         (add_state_var ~pref gd sink Initial.tbool ok None, sink_expr)
  in
  let assertion = mk_and' gd.assertion ak
  and invariant = mk_and' gd.invariant ok in
  ({ gd with assertion; invariant; }, { contract with c_eq = equs'; }, locals)

(* --- *)

let declare_output s { v_ident = id } =
  IdentSet.add id s

let declare_input m { v_ident = id; v_type = typ } =
  SMap.add (mk_symb & name id) (translate_typ typ, `Input one, None) m

let register_var_typ m { v_ident = id; v_type = typ } =
  SMap.add (mk_symb & name id) (id, typ) m

(* --- *)

let finalize_uc_groups gd =
  let gd = if SSet.is_empty gd.remaining_contrs then gd else
      (* switch to last U/C group here, and declare controller call. *)
      close_uc_group gd gd.remaining_contrs
  in
  if SSet.is_empty gd.extra_inputs then gd else
    { gd with
      extra_inputs = SSet.empty;
      uc_groups = (gd.extra_inputs, SSet.empty) :: gd.uc_groups; }

(* Note uc_groups are reversed in gd BEFORE the call to this function. *)
let assign_uc_groups gd =
  let gd = finalize_uc_groups gd in
  let uc_groups = List.rev gd.uc_groups in      (* start from the first group *)
  let decls, _ = List.fold_left begin fun (decls, group) (u, c) ->
    let decls = SSet.fold (fun u decls -> match SMap.find u decls with
      | (t, `Input _, l) ->
          SMap.add u (t, `Input group, l) decls
      | _ -> decls) u decls
    in
    let decls = SSet.fold (fun c decls -> match SMap.find c decls with
      | (t, `Contr (_, r, l'), l) ->
          SMap.add c (t, `Contr (group, r, l'), l) decls
      | _ -> decls) c decls
    in
    decls, AST.succ group
  end (gd.decls, AST.succ one) (List.tl uc_groups) in
  { gd with decls; uc_groups }

(* --- *)

let scmp a b = String.compare (Symb.to_string a) (Symb.to_string b)

let var_exp v ty =
  mk_extvalue ~ty ~clock:Clocks.Cbase ~linearity:Linearity.Ltop (Wvar v)

let decl_arg (v, t) =
  mk_arg (Some (name v)) t Linearity.Ltop Signature.Cbase

let gen_ctrlf_calls ~requal_types gd node_name equs =

  let equs, _, _ = List.fold_left begin fun (equs, ubase, num) (u, c) ->

    (* Controllable inputs of the current U/C group *)
    let c = SSet.elements c in
    let c = List.sort scmp c in                       (* XXX now optional (x) *)
    let o = List.map (fun v -> SMap.find v gd.contrs) c in
    let os = List.map decl_arg o in
    let ov, ot = List.split o in
    let ov = Etuplepat (List.map (fun v -> Evarpat v) ov) in

    (* Accumulate state variables and all non-controllable inputs from the
       beginning, plus all controllables from previous U/C groups *)
    let u = SSet.fold (fun v -> SMap.add v (SMap.find v gd.local)) u ubase in
    let i = SMap.bindings u in
    let i = List.sort (fun (a, _) (b, _) -> scmp b a) i in  (* rev. i + ibid (x) *)
    let is = List.rev_map (fun (_, p) -> decl_arg p) i in
    let i = List.rev_map (fun (_, (v, t)) -> var_exp v t) i in

    (* Build controller call *)
    let func_name = controller_node ~num node_name in
    let app = Eapp (mk_app (Efun func_name), i, None) in
    let exp = mk_exp ~linearity:Linearity.Ltop Clocks.Cbase (Tprod ot) app in
    let equ = mk_equation false ov exp in

    let is, os = if requal_types then
        (* Optional requalification of types declared in the exported module: *)
        let requal_arg = function
          | { a_type = Tid { qual; name } } as arg when qual = node_name.qual ->
              { arg with a_type = Tid { qual = func_name.qual; name } }
          | a -> a
        in
        List.map requal_arg is, List.map requal_arg os
      else
        is, os
    in

    (* Declare new node *)
    let node_sig = Signature.mk_node Location.no_location ~extern:false is os
      false false [] in
    Modules.add_value func_name node_sig;

    (* Augment base non-controllble inputs with current controllables *)
    let u = List.fold_left (fun u v -> SMap.add v (SMap.find v gd.contrs) u) u c in

    (equ :: equs, u, num + 1)
  end (equs, gd.base, 0) gd.uc_groups in

  equs

(* --- *)

(** Node translation. Note the given node is not expored if it does not comprize a
    contract. *)
let translate_node ~requal_types typdefs = function
  | ({ n_contract = None } as node) -> node, None
  | ({ n_name; n_input; n_output; n_local; n_equs;
       n_contract = Some contr } as node) ->
      let pref p = p in
      let local = List.fold_left register_var_typ SMap.empty n_local in
      let input = List.fold_left register_var_typ SMap.empty n_input in
      let output = List.fold_left declare_output IdentSet.empty n_output in
      let decls = List.fold_left declare_input SMap.empty n_input in

      let init_cond_var = mk_symb init_cond_str in
      let init_cond = mk_bref' init_cond_var in    (* XXX what about gd.base? *)
      let init_cond_spec = (`Bool, `State (`Bexp ff, None), None) in
      let decls = SMap.add init_cond_var init_cond_spec decls in

      let gd = mk_gen_data typdefs decls input local output init_cond in
      let gd, contract, locals' = translate_contract ~pref gd contr in
      let gd, equs' = translate_eqs ~pref (gd, []) n_equs in
      let gd = assign_uc_groups gd in
      let equs' = gen_ctrlf_calls ~requal_types gd n_name equs' in

      let ctrln_node_desc =
        { cn_typs = typdefs;
          cn_decls = gd.decls;
          cn_init = mk_and' gd.init_state init_cond;
          cn_assertion = (* mk_or' init_cond  *)gd.assertion;
          cn_invariant = Some (mk_or' init_cond gd.invariant);
          cn_reachable = None;
          cn_attractive = None; }
      and node =
        { node with
          n_equs = equs';
          n_local = List.rev_append locals' n_local;
          n_contract = Some contract; }
      in

      (node, Some (n_name, (`Desc ctrln_node_desc : 'f AST.node)))

(* --- *)

(** Moves all type declarations into the given module, declare aliases for them
    (in cases). Also requalifies constructor names in the program, FIXME: as
    well as types of expressions to avoid some errors in code generation later
    on. *)
let requal_declared_types prog =

  let cmodul = controller_modul prog.p_modname in
  let requal m = m = prog.p_modname in

  let requal_it ({ qual; name } as cstr) =
    if requal qual then { qual = cmodul; name } else cstr in

  let requal_type = function
    | Tid { qual; name } when requal qual -> Tid { qual = cmodul; name }
    | t -> t
  in

  let open Mls_mapfold in
  let open Global_mapfold in
  let funcs = { Mls_mapfold.defaults with

    type_dec = (fun _ () -> function
      | { t_name = tn; t_desc = Type_enum cl } as t when requal tn.qual ->
          let tn' = requal_it tn in
          let t = { t with
            t_name = tn';
            t_desc = Type_alias (Tid { qual = cmodul; name = tn.name});
          } in
          Modules.replace_type tn (Signature.Talias (Tid tn));
          Modules.add_type tn' (Signature.Tenum (List.map requal_it cl));
          t, ()
      | _ -> raise Errors.Fallback);

    edesc = (fun funs () -> function
      | Ewhen (e, c, x) ->
          Ewhen (exp_it funs () e |> fst, requal_it c,
                 var_ident_it funs.global_funs () x |> fst), ()
      | Emerge (i, l) ->
          Emerge (var_ident_it funs.global_funs () i |> fst,
                  List.map (fun (c, x) -> requal_it c,
                    extvalue_it funs () x |> fst) l), ()
      | _ -> raise Errors.Fallback);

    extvalue_desc = (fun funs () -> function
      | Wwhen (w, c, v) ->
          Wwhen (extvalue_it funs () w |> fst, requal_it c,
                 var_ident_it funs.global_funs () v |> fst), ()
      | _ -> raise Errors.Fallback);

    global_funs = { Global_mapfold.defaults with

      ty = (fun _ () ty -> requal_type ty, ());

      ck = (fun funs () -> function
        | Clocks.Con (ck, c, i) ->
            Clocks.Con (ck_it funs () ck |> fst, requal_it c,
                        var_ident_it funs () i |> fst), ()
        | _ -> raise Errors.Fallback);

      static_exp_desc = (fun _ () -> function
        | Sconstructor c -> Sconstructor (requal_it c), ()
        | _ -> raise Errors.Fallback);

    };
  } in

  program funcs () prog |> fst

(* --- *)

(** [gen p] translates all type definitions, plus the nodes comprizing a
    contract, into Controllable-Nbac.

    @return a Controllable-Nbac program comprizing one process for each node
    necessitating controller synthesis), and a new Minils program, in which
    those nodes have been transformed so that they "call" their respective
    controller.

    XXX The [requalify_declared_types] argument is here to avoid cyclic
    dependencies between modules due to type declarations. Yet, a better idea
    might be to integrate the generated controllers into the original program
    later on.  *)
let gen ?(requalify_declared_types = true) ({ p_desc } as p) =

  let requal_types = requalify_declared_types in

  let _cnp_typs, nodes, descs =
    List.fold_left begin fun (typdefs, nodes, descs) -> function
      | Pnode n ->
          begin match translate_node ~requal_types typdefs n with
            | node, Some n -> (typdefs, n :: nodes, Pnode node :: descs)
            | node, None -> (typdefs, nodes, Pnode node :: descs)
          end
      | Ptype { t_name = ({ name }); t_desc = Type_enum cl } as ty ->
          let tn = mk_typname & mk_symb name and typ = translate_constrs cl in
          let typdefs = declare_typ tn typ typdefs in
          (typdefs, nodes, ty :: descs)
      | p -> (typdefs, nodes, p :: descs)
    end (empty_typdefs, [], []) p_desc
  in

  let cnp_nodes = List.rev nodes and p_desc = List.rev descs in
  let prog = { p with p_desc } in
  let prog =                            (* moving types to controller module? *)
    if requalify_declared_types
    then requal_declared_types prog
    else prog
  in
  cnp_nodes, prog