Project

General

Profile

« Previous | Next » 

Revision 72a93147

Added by Pierre-Loïc Garoche almost 4 years ago

seal: stateless systems

View differences:

src/tools/seal/seal_export.ml
76 76 
let sw_to_lustre m sw_init sw_step init_out update_out =
77 77 
  let orig_nd = m.mname in
78 78 
  let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in
79 
  let vl = (* memories *)
79 
  let vl = (* vl are memories *)
80 80 
    match sw_init with
81 
    | [] -> assert false
82 
    | (gl, up)::_ -> List.map (fun (v,_) -> v) up
83 
  in
84 
  let e_init = process_sw m.mmemory (fun x -> x) sw_init in
85 
  let e_step = process_sw m.mmemory (Corelang.add_pre_expr vl) sw_step in
86 
  let e_init_out = process_sw copy_nd.node_outputs (fun x -> x) init_out in
87 
  let e_update_out = process_sw  copy_nd.node_outputs (Corelang.add_pre_expr vl) update_out in
81 
    | [] -> [] (* the system is stateless. Returning an empty list
82 
                  shall do the job *)
83
84 
    | (gl, up)::_ ->
85 
       List.map (fun (v,_) -> v) up
86 
  in
88 87 
  let loc = Location.dummy_loc in
88 
  let mem_eq =
89 
    if m.mmemory = [] then
90 
      []
91 
    else
92 
      let e_init = process_sw m.mmemory (fun x -> x) sw_init in
93 
      let e_step = process_sw m.mmemory (Corelang.add_pre_expr vl) sw_step in
94 
      [Eq
95 
         { eq_loc = loc;
96 
           eq_lhs = vl;
97 
           eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init, e_step))
98 
      }]
99 
  in
100 
  let output_eq =
101 
    let e_init_out = process_sw copy_nd.node_outputs (fun x -> x) init_out in
102 
    let e_update_out = process_sw  copy_nd.node_outputs (Corelang.add_pre_expr vl) update_out in
103 
    [
104 
      Eq
105 
        { eq_loc = loc;
106 
          eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs;
107 
          eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out))
108 
        };
109 
    ]
110 
  in
89 111 
  let new_nd =
90 112 
    { copy_nd with
91 
    node_id = copy_nd.node_id ^ "_seal";
92 
    node_locals = m.mmemory;
93 
    node_stmts = [Eq
94 
                    { eq_loc = loc;
95 
                      eq_lhs = vl;
96 
                      eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init, e_step))
97 
                    };
98 
                 Eq
99 
                    { eq_loc = loc;
100 
                      eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs;
101 
                      eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out))
102 
                    };
103 
                 ];
113 
      node_id = copy_nd.node_id ^ "_seal";
114 
      node_locals = m.mmemory;
115 
      node_stmts = mem_eq @ output_eq;
104 116 
    }
105 117 
  in
106 118 
  new_nd, orig_nd

Also available in: Unified diff