l2lExpandMetaOp.ml

(** Time-stamp: <modified the 05/05/2022 (at 08:40) by Erwan Jahier> *)

open Lxm
open Lic

let dbg = (Lv6Verbose.get_flag "ei")

(* pack useful info into a single struct *)
type local_ctx = { 
  node : Lic.node_exp;
  prg : LicPrg.t;
}

(********************************************************************************)
(* stuff to create fresh var names. *)
let new_var str _lctx type_eff clock_eff = 
  let id = Lv6Id.of_string (FreshName.local_var (str)) in 
  let var =
    { 
      var_name_eff   = id;
      var_nature_eff = AstCore.VarLocal;
      var_number_eff = -1; (* this field is used only for i/o. 
                              Should i rather put something sensible there ? *)
      var_type_eff   = type_eff;
      var_clock_eff  = id, clock_eff;
    }
  in
    var

(********************************************************************************)
(* A small util function followed by a quick unit test. *)
let rec fill i size = if i >= size then [] else (i)::(fill (i+1) size) 
let _ = assert (fill 0 5 = [0;1;2;3;4])
      
let rec (list_map3: 
           ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list) =
  fun f l1 l2 l3 ->
    match (l1, l2, l3) with
      |	([], [], []) -> []
      | (e1::t1, e2::t2, e3::t3) -> (f e1 e2 e3)::(list_map3 f t1 t2 t3)
      | _ -> (* should not occur *) 
          print_string "*** list_map3 called with lists of different size.\n";
          flush stdout;
          assert false
(********************************************************************************)
(* Some utililities to build Lic expressions *)

(* We generate code that does not correspond to any source *)
let lxm = Lxm.dummy "no_source"

let (val_exp_of_var_info : Lxm.t -> Lic.var_info -> Lic.val_exp) =
  fun lxm vi -> 
    { 
      ve_core = CallByPosLic({src=lxm;it=Lic.VAR_REF vi.var_name_eff}, []); 
      ve_typ  = [vi.var_type_eff];
      ve_clk  = [snd vi.var_clock_eff];
      ve_src  =  lxm
    }

let (val_exp_of_ident : Lxm.t -> string -> Lic.type_ -> Lic.clock -> Lic.val_exp) =
  fun lxm id t clk -> 
    { 
      ve_clk = [clk]; 
      ve_typ = [t]; 
      ve_core = CallByPosLic({it=Lic.VAR_REF id;src=lxm},[]);
      ve_src = lxm
    }

let (val_exp_of_int : Lxm.t -> string -> Lic.clock -> Lic.val_exp) =
  fun lxm i clk -> 
    { 
      ve_clk = [clk]; 
      ve_typ = [Int_type_eff]; 
      ve_core = CallByPosLic({it= CONST(Int_const_eff i);src=lxm},[]);
      ve_src = lxm
    }


let (val_exp_of_const : Lic.const -> Lic.val_exp) =
  fun c -> 
    let _,ve = UnifyClock.const_to_val_eff lxm true UnifyClock.empty_subst c in
    ve

let (add_when : Lic.clock -> Lic.val_exp -> Lic.val_exp) =
  fun clk ve -> 
    { ve with 
      ve_clk = List.map (fun _ -> clk) ve.ve_clk; 
      ve_core = CallByPosLic({it= WHEN clk;src=lxm},[ve]);
    }

(* [add_current ve clk out_cl] return the expression current(ve when clk)  *)
let (add_current : Lic.val_exp -> Lic.clock -> Lic.clock list -> Lic.val_exp) =
  fun ve clk out_cl -> 
    match clk with
    | On((cc,cv,_),sclk) ->
      let lxm = ve.ve_src in
        let clk_exp = val_exp_of_ident lxm cv Bool_type_eff sclk in
        { ve with
          ve_clk = out_cl;  
          ve_core = CallByPosLic({it= CURRENT(Some cc);src=lxm},[clk_exp;ve])
        }
      | _  -> assert false (* SNO *)
   


let rec (elt_type_of_array : Lic.type_ -> Lic.type_) =
  function
    | Array_type_eff(t, _) -> t
    | Abstract_type_eff(_,t) -> elt_type_of_array t
    | _  -> assert false 

let (array_var_to_val_exp : Lxm.t -> int -> var_info -> val_exp) =
  fun lxm i vi -> 
    (* vi holds x of type array and returns  x.[i] *)
    let t_elt = elt_type_of_array vi.var_type_eff in
    let op_flg = {src = lxm ; it = ARRAY_ACCES(i)} in
    { 
      ve_core = CallByPosLic(op_flg, [val_exp_of_var_info lxm vi]); 
      ve_typ  = [t_elt];
      ve_clk  = [snd vi.var_clock_eff];
      ve_src  = lxm
    }

let (node_to_val_exp : Lxm.t -> Lic.node_key -> Lic.type_ list -> Lic.clock list -> 
     val_exp list -> val_exp) =
  fun lxm nk tl cl vel -> 
    let nk = { src = lxm ; it = nk } in
    let core = CallByPosLic( { src = lxm ; it = CALL nk }, vel)  in
    {
      ve_clk = cl;
      ve_typ = tl;
      ve_core = core;
      ve_src  = lxm
    } 
let (binop_to_val_exp : Lxm.t -> Lv6Id.t -> val_exp -> val_exp -> val_exp) =
  fun lxm op ve1 ve2 ->
    let op = { it = PREDEF_CALL({src=lxm;it=("Lustre",op),[]}) ; src = lxm } in
    {
      ve_clk = ve1.ve_clk;
      ve_typ = ve1.ve_typ;
      ve_core = CallByPosLic(op, [ve1; ve2]);
      ve_src  = lxm
    }
let (binop_to_val_exp_bool : Lxm.t -> Lv6Id.t -> val_exp -> val_exp -> val_exp) =
  fun lxm op ve1 ve2 ->
    let op = { it = PREDEF_CALL({src=lxm;it=("Lustre",op),[]}) ; src = lxm } in
    {
      ve_clk = ve1.ve_clk;
      ve_typ = [Bool_type_eff];
      ve_core = CallByPosLic(op, [ve1; ve2]);
      ve_src = lxm
        
    }
let (fby_to_val_exp : Lxm.t -> val_exp -> val_exp -> val_exp) =
  fun lxm ve1 ve2 ->
    let op = { it = FBY ; src = lxm } in
    {
      ve_clk = ve1.ve_clk;
      ve_typ = ve1.ve_typ;
      ve_core = CallByPosLic(op, [ve1; ve2]);
      ve_src = lxm
    }
let (tuple_to_val_exp : Lxm.t -> val_exp list -> val_exp) =
  fun lxm vel ->
    let op = { it = TUPLE ; src = lxm } in
    {
      ve_clk = List.flatten (List.map (fun ve -> ve.ve_clk) vel);
      ve_typ = List.flatten (List.map (fun ve -> ve.ve_typ) vel);
      ve_core = CallByPosLic(op, vel);
      ve_src = lxm
    }
let (ite_to_val_exp : Lxm.t -> val_exp -> val_exp -> val_exp -> val_exp) =
  fun lxm ve1 ve2 ve3 ->
    let ite_op  = { it = PREDEF_CALL({src=lxm;it=("Lustre","if"),[]}); src = lxm } in
    {
      ve_clk = ve2.ve_clk; 
      ve_typ = ve2.ve_typ;
      ve_core = CallByPosLic(ite_op, [ve1; ve2; ve3]) ;
      ve_src = lxm
    } 

let (array_var_to_left : int -> var_info -> Lic.left) =
  fun i vi -> 
    let lp = LeftVarLic(vi,lxm) in
    let t_elt = elt_type_of_array vi.var_type_eff in
    LeftArrayLic(lp,i,t_elt)


let (create_fillred_body: local_ctx -> Lic.static_arg list ->
     Lic.node_body * var_info list) =
  fun lctx sargs ->
    (* Given 
       - a node n of type : tau * tau_1 * ... * tau_n -> tau * teta_1 * ... * teta_l
       - a integer c
       
       the fillred expression has the profile: 
       tau * tau_1^c * ... * tau_n^c  -> tau * teta_1^c * ... * teta_l^c
    *)
    let iter_node,c = match List.sort compare sargs with
      | [ConstStaticArgLic(_,Int_const_eff(c));NodeStaticArgLic(_,_node_key)]
      | [ConstStaticArgLic(_,Int_const_eff(c));TypeStaticArgLic(_);
         NodeStaticArgLic(_,_node_key)]
        -> 
        _node_key,c
      | _ -> assert false
    in
    let lxm = lctx.node.Lic.lxm in
    let iter_node = Lxm.flagit iter_node lxm in
        (*
          Hence:
          node(acc_in:tau; X1:tau_1^c ; ... ; Xn:tau_n^c) 
          returns (acc_out:tau; Y1:teta_1^c; ... ; Yl:teta_l^c) = fillred<<n,c>>;
         *)
    assert (lctx.node.Lic.inlist_eff <> []);
    assert (lctx.node.Lic.outlist_eff <> []);
    let (acc_in : var_info)      = List.hd lctx.node.Lic.inlist_eff  in
    let (y1_yl  : var_info list) = List.tl lctx.node.Lic.inlist_eff  in
    let (acc_out: var_info)      = List.hd lctx.node.Lic.outlist_eff in
    let (x1_xn  : var_info list) = List.tl lctx.node.Lic.outlist_eff in
        (*
          can be defined like this:
          node(acc_in:tau; X1:tau_1^c ; ... ; Xn:tau_n^c) 
          returns (acc_out:tau; Y1 : teta1^c; ... ; Yl: teta_l^c) =
          var
          acc_1, ..., acc_c-2 : tau;
          let 
          
          acc_1, Y1[0], ... ,Yl[0] = n(acc_in,X1[0], ... ,Xk[0]);
          acc_2, Y1[1], ... ,Yl[1] = n(acc_1, X1[1], ... ,Xk[1]);
          ... 
          acc_i+1, Y1[i], ... ,Yl[i] = n(acc_i,X1[i], ... ,Xk[i]);
          ...
          acc_out, Y1[c-1], ... ,Yl[c-1] = n(acc_c-1,X1[c-1], ... ,Xk[c-1]);
          
	       « for all i = 0, ..., c-1 » 
          acc_i+1, Y1[i], ... ,Yl[i] = n(acc_i,X1[i], ... ,Xk[i])
          tel
        *)
    let c = int_of_string c in
    let index_list = fill 0 c in        
        (* Building this list "acc_left_list" as [acc_1, ..., acc_c-2, acc_out] *)
    let type_exp,clock_exp = acc_in.var_type_eff, snd acc_in.var_clock_eff in
    let (acc_vars : var_info list) =
      let rec f i acc = if i = 0 then acc else
          f (i-1) ((new_var "acc" lctx type_exp clock_exp)::acc)
      in
      List.rev(f (c-1) [])
    in
    let (acc_left_list : left list) =
      (List.map (fun vi -> LeftVarLic(vi,lxm)) (acc_vars@[acc_out]))
    in
        (* Ditto for rigth part :  [acc_in, acc_1, ..., acc_c-1]*)
    let (acc_rigth_list : val_exp list) =
      List.map (val_exp_of_var_info lxm) (acc_in::acc_vars)
    in
    let neqs =
          (*
            So now we build those equations ;
            acc_1, Y1[0], ... ,Yl[0] = n(acc_in,X1[0], ... ,Xk[0]);
            acc_2, Y1[1], ... ,Yl[1] = n(acc_1, X1[1], ... ,Xk[1]);
            ... 
            acc_i+1, Y1[i], ... ,Yl[i] = n(acc_i,X1[i], ... ,Xk[i]);
            ...
            acc_out, Y1[c-1], ... ,Yl[c-1] = n(acc_c-1,X1[c-1], ... ,Xk[c-1]);
          *)
      list_map3
        (fun i acc_left acc_rigth ->
          let (xi_j:val_exp list) = (* X1[i], ... ,Xn[i] *)
            List.map (array_var_to_val_exp lxm i) y1_yl
          in
          let args = acc_rigth::xi_j in
          let (yi_k : left list) =  (* Y1[i], ... ,Yl[i] *)
            List.map (array_var_to_left i) x1_xn
          in
          let lhs = acc_left::yi_k in
		    let cl = 
            List.map (fun l -> snd (Lic.var_info_of_left l).var_clock_eff) lhs
          in
          let rhs = {
            ve_typ = List.map Lic.type_of_left lhs;
            ve_clk = cl;
            ve_core = 
              if AstPredef.is_a_predef_op (snd(fst iter_node.it)) then
                CallByPosLic({src=lxm;it=(Lic.PREDEF_CALL iter_node)}, args)
              else
                CallByPosLic({src=lxm;it=(CALL iter_node)}, args);
            ve_src = lxm
          }
          in
		    let eq = { src = lxm ; it = (lhs, rhs) } in
          eq 
        )
        index_list
        acc_left_list
        acc_rigth_list
    in
    { asserts_eff = []; eqs_eff = List.rev neqs }, acc_vars

let (create_map_body: local_ctx -> Lic.static_arg list -> Lic.node_body * var_info list) =
  fun lctx sargs ->
	 (* Given
	    - a node n of type: tau_1 * ... * tau_n -> teta_1 * ... * teta_l
	    - and an integer c
       
	    The profile of map<<node,c>> is:
  	    tau_1^c * ... * tau_n^c -> teta_1^c * ... * teta_l^c
       and
       
	    Y1, ... ,Yl = map<<node; c>>(X1,...,Xk)
       <=>
	    for all i = 0, ..., c-1; (Y1[i], ... ,Yl[i]) = N(X_1[i], ... ,X_k[i])
    *)
    let iter_node,c = match List.sort compare sargs with
      | [ConstStaticArgLic(_,Int_const_eff(c)) ; NodeStaticArgLic(_,node_key)]
      | [ConstStaticArgLic(_,Int_const_eff(c)) ; TypeStaticArgLic(_);
         NodeStaticArgLic(_,node_key)]
        -> 
        node_key,c
      | _ -> assert false
    in
    let iter_node = Lxm.flagit iter_node lxm in
    let (y1_yl  : var_info list) = lctx.node.Lic.inlist_eff  in
    let (x1_xn  : var_info list) = lctx.node.Lic.outlist_eff in
    let c = int_of_string c in
    let index_list = fill 0 c in        
    let neqs =
      List.map
        (fun i ->
          let (xi_j:val_exp list) = (* X1[i], ... ,Xn[i] *)
            List.map (array_var_to_val_exp lxm i) y1_yl
          in
          let (lhs : left list) =  (* Y1[i], ... ,Yl[i] *)
            List.map (array_var_to_left i) x1_xn
          in
	  let cl =
            List.map (fun l -> snd (Lic.var_info_of_left l).var_clock_eff) lhs
          in
          let p,n = fst iter_node.it in
          let rhs = {
            ve_typ = List.map Lic.type_of_left lhs;
            ve_clk = cl;
            ve_core =
              if p="Lustre" && AstPredef.is_a_predef_op n then
                CallByPosLic({src=lxm;it=(Lic.PREDEF_CALL iter_node)}, xi_j)
              else
                CallByPosLic({src=lxm;it=(CALL iter_node)}, xi_j);
            ve_src = lxm
          }
          in
	  let eq = { src = lxm ; it = (lhs, rhs) } in
          eq 
        )
        index_list
    in

    { asserts_eff = []; eqs_eff = List.rev neqs }, []

let (create_boolred_body: local_ctx -> int -> int -> int -> Lic.node_body * var_info list) =
  fun lctx i j k ->
    (* Given - 3 integers i, j, k boolred<<i,j,k>> has the profile: bool^n -> bool
       and is defined by
       node toto = boolred<<i,j,k>>(tab); 
       <=>
       node toto(tab:bool^n) returns (res:bool);
       var 
         cpt:int;
         let 
           cpt = (if tab[0] then 1 else 0) + ... + (if tab[k-1] then 1 else 0);
           res = i <= cpt && cpt <= j;
         tel
    *)
    assert(0 <= i && i <= j && j <= k && k>0);
    let lxm = lctx.node.Lic.lxm in
    let (tab_vi : var_info) = match lctx.node.Lic.inlist_eff with
      | [vi] -> vi 
      | _ -> assert false
    in
    let (res_vi : var_info) = match lctx.node.Lic.outlist_eff with
      | [vi] -> vi 
      | _ -> assert false
    in
    let (cpt_vi : var_info) = new_var "cpt" lctx Int_type_eff BaseLic in
    let cpt_left = LeftVarLic (cpt_vi,lxm) in
    let zero = val_exp_of_int lxm "0" BaseLic
    and one = val_exp_of_int lxm  "1" BaseLic in
    let index_list = fill 0 k in (* [0;1; ...;k-1]*)
    let (ite_list:Lic.val_exp list) = List.map
      (fun i -> (* returns [if A[i] then 1 else 0]_i=0,k-1 *)
        let tab_ve_i = array_var_to_val_exp lxm i tab_vi in
        ite_to_val_exp lxm tab_ve_i one zero
      )
      index_list
    in
    let cpt_rigth =
      assert(ite_list<>[]);
      List.fold_left (binop_to_val_exp lxm "plus")
                     (List.hd ite_list) (List.tl ite_list) in
    let res_left = LeftVarLic (res_vi,lxm) in
    let res_rigth = (* i <= cpt && cpt <= j; *)
      let i_eff   = val_exp_of_int lxm (string_of_int i) BaseLic in
      let j_eff   = val_exp_of_int lxm (string_of_int j) BaseLic in
      let cpt_eff = val_exp_of_var_info lxm cpt_vi in
      let i_inf_cpt = binop_to_val_exp_bool lxm "lte" i_eff cpt_eff in
      let cpt_inf_j = binop_to_val_exp_bool lxm  "lte" cpt_eff j_eff in
      binop_to_val_exp lxm  "and" i_inf_cpt cpt_inf_j
    in 
    let cpt_eq = { src = lxm ; it = ([cpt_left], cpt_rigth) } in
    let res_eq = { src = lxm ; it = ([res_left], res_rigth) } in
    { 
      asserts_eff = []; 
      eqs_eff = [cpt_eq; res_eq] 
    }, [cpt_vi]

let rec (replace_base : Lic.clock -> Lic.clock -> Lic.clock) =
  fun ck1 ck2  -> 
    match ck2 with
      | BaseLic -> ck1
      | On(x,sck)  -> On(x,replace_base sck ck2)
      | ClockVar _ -> assert false

let (create_condact_body: local_ctx -> Lic.static_arg list -> Lic.node_body * var_info list) =
  fun lctx sargs ->
    (*
      node condact_plus_0(i0:bool; i1:int; i2:int) returns (o0:int) = Lustre::condact<<toto, 0>>;

      <=>

      o0 = if i0 then current(toto(i1 when i0, i2 when i0) ) else (0 fby o0);

      Lustre::condact<<Lustre::plus, 0>>;
    *)
    let lxm = lctx.node.Lic.lxm in
    let node,c = match List.sort compare sargs with
      | [ConstStaticArgLic(_, c);TypeStaticArgLic(_);NodeStaticArgLic(_, node_key)]
      | [ConstStaticArgLic(_, c) ; NodeStaticArgLic(_, node_key)]
        -> node_key,c
      | _ -> assert false
    in
    let cond_exp, inputs = 
      match List.map (val_exp_of_var_info lxm) lctx.node.Lic.inlist_eff with
          [] -> assert false
        | x::t -> x,t
    in 
    let outputs_clk = List.map (fun var -> snd var.var_clock_eff) lctx.node.Lic.outlist_eff in
    let left = List.map (fun x -> LeftVarLic (x,lxm)) lctx.node.Lic.outlist_eff in
    let node_out_type_list = 
      List.map (fun x -> x.Lic.var_type_eff) lctx.node.Lic.outlist_eff 
    in
    let true_cc = ("Lustre","true") in
    let i0 = List.hd lctx.node.Lic.inlist_eff in
    let i0_clk = Lic.On((true_cc, i0.var_name_eff,Bool_type_eff), snd i0.var_clock_eff) in
    let inputs_when_i0 = List.map (add_when i0_clk) inputs in    
    let outputs_clk_when_i0 = (* replace baseLic by i0_clk *)
      List.map (replace_base i0_clk) outputs_clk
    in
    let then_exp =
      node_to_val_exp lxm node node_out_type_list outputs_clk_when_i0 inputs_when_i0
    in
    let then_exp = add_current then_exp i0_clk outputs_clk in
    let const_exp = val_exp_of_const c in
    let out_exp = match lctx.node.Lic.outlist_eff with 
        [o] -> val_exp_of_var_info lxm o 
      | _ -> tuple_to_val_exp lxm
        (List.map (val_exp_of_var_info lxm) lctx.node.Lic.outlist_eff)
    in
    let else_exp = fby_to_val_exp lxm const_exp out_exp in
    let rigth = ite_to_val_exp lxm cond_exp then_exp else_exp in
    let eq = { src = lxm ; it = (left, rigth) } in
    { asserts_eff = []; eqs_eff = [eq] }, []

let ios = int_of_string

let (create_merge_body: local_ctx -> Lic.static_arg list -> Lic.node_body * var_info list) =
  fun _lctx _sargs ->
    assert false (* XXX finish me! *)

let (create_meta_op_body:  local_ctx -> Lic.node_key -> Lic.node_body * var_info list) =
  fun lctx (nk,sargs) ->
    match nk with
      | "Lustre", "fill" 
      | "Lustre", "red" 
      | "Lustre", "fillred" -> create_fillred_body lctx sargs
      | "Lustre", "map"     -> create_map_body lctx sargs
      | "Lustre", "boolred" -> (
        let (i,j,k) =
          match sargs with 
            | [ConstStaticArgLic(_, Int_const_eff i);
               ConstStaticArgLic(_, Int_const_eff j);
               ConstStaticArgLic(_, Int_const_eff k)
              ] -> 
              (ios i,ios j,ios k)
            | _ -> assert false
        in
        create_boolred_body lctx i j k  
      )
      | "Lustre", "diese" -> (
        (* a diese is a particular kind of boolred:
           #(A,...,an) = boolred(0,1,n)([a1,...,an])
        *)
        let n = List.length lctx.node.Lic.inlist_eff in
        create_boolred_body lctx 0 1 n 
      )
      | "Lustre", "nor" -> (
        (* a nor is a particular kind of boolred too:
           nor(A,...,an) = boolred(0,0,n)([a1,...,an])
        *)
        let n = List.length lctx.node.Lic.inlist_eff in
        create_boolred_body lctx 0 0 n 
      )
      | "Lustre", "condact" -> create_condact_body lctx sargs
      | "Lustre", "merge"   -> create_merge_body lctx sargs
      | _,_  -> assert false


let rec (node : local_ctx -> Lic.node_exp -> bool -> Lic.node_exp) =
  fun lctx n only_boolred ->
    let sonk = Lic.string_of_node_key in
    Lv6Verbose.exe ~flag:dbg (fun () ->
      Printf.printf "#DBG: L2lInlineMetaOp %s\n" (sonk n.node_key_eff));
    match n.def_eff with
    | MetaOpLic ->
      if only_boolred && (fst n.node_key_eff) <> ("Lustre", "boolred") then n else
        let nk = n.node_key_eff in
        let nbody, nlocs = create_meta_op_body lctx nk in
        { n with 
          def_eff = BodyLic nbody;
          loclist_eff = Some nlocs;
        }
    | ExternLic 
    | AbstractLic None -> n
    | AbstractLic (Some pn) ->
      { n with def_eff = AbstractLic (Some (node lctx pn only_boolred)) }
    | BodyLic _b -> n
      
(* exported *)
let (doit :  LicPrg.t -> LicPrg.t) =
  fun inprg -> 
    let outprg = LicPrg.empty in
    (* types and constants do not change *)
    let outprg = LicPrg.fold_types  LicPrg.add_type  inprg outprg in
    let outprg = LicPrg.fold_consts LicPrg.add_const inprg outprg in
    (* transform nodes *)
    let  (do_node : Lic.node_key -> Lic.node_exp -> LicPrg.t -> LicPrg.t) = 
      fun nk ne outprg -> 
        let lctx = {
          node = ne;
          prg = inprg;
        }
        in
        let ne = node lctx ne false in
        LicPrg.add_node nk ne outprg
    in
    let outprg = LicPrg.fold_nodes do_node inprg outprg in
    outprg
(* exported *)

let (doit_boolred :  LicPrg.t -> LicPrg.t) =
  fun inprg -> 
    let outprg = LicPrg.empty in
    (* types and constants do not change *)
    let outprg = LicPrg.fold_types  LicPrg.add_type  inprg outprg in
    let outprg = LicPrg.fold_consts LicPrg.add_const inprg outprg in
    (* transform nodes *)
    let  (do_node : Lic.node_key -> Lic.node_exp -> LicPrg.t -> LicPrg.t) = 
      fun nk ne outprg -> 
        let lctx = {
          node = ne;
          prg = inprg;
        }
        in
        let ne = node lctx ne true in
        LicPrg.add_node nk ne outprg
    in
    let outprg = LicPrg.fold_nodes do_node inprg outprg in
    outprg