Revision 66359a5e
Added by Pierre-Loïc Garoche about 7 years ago
src/automata.ml | ||
---|---|---|
114 | 114 |
let node_vars_of_idents node iset = |
115 | 115 |
List.fold_right (fun v res -> if ISet.mem v.var_id iset then v :: res else res) (get_node_vars node) [] |
116 | 116 |
|
117 |
let mkautomata_state used typedef loc id = |
|
117 |
let mkautomata_state nodeid used typedef loc id =
|
|
118 | 118 |
let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = loc } in |
119 | 119 |
let tydec_state id = { ty_dec_desc = Tydec_const id; ty_dec_loc = loc } in |
120 | 120 |
let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = loc } in |
... | ... | |
125 | 125 |
let actual_r = mk_new_name used (id ^ "__restart_act") in |
126 | 126 |
let actual_s = mk_new_name used (id ^ "__state_act") in |
127 | 127 |
{ |
128 |
incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false, None); |
|
129 |
incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false, None); |
|
130 |
incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false, None); |
|
131 |
incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false, None); |
|
132 |
actual_r = mkvar_decl loc (actual_r , tydec_bool, ckdec_any, false, None); |
|
133 |
actual_s = mkvar_decl loc (actual_s , tydec_state typedef.tydef_id, ckdec_any, false, None) |
|
128 |
incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false, None, Some nodeid);
|
|
129 |
incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid);
|
|
130 |
incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false, None, Some nodeid);
|
|
131 |
incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid);
|
|
132 |
actual_r = mkvar_decl loc (actual_r , tydec_bool, ckdec_any, false, None, Some nodeid);
|
|
133 |
actual_s = mkvar_decl loc (actual_s , tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid)
|
|
134 | 134 |
} |
135 | 135 |
|
136 | 136 |
let vars_of_aut_state aut_state = |
... | ... | |
225 | 225 |
|
226 | 226 |
let expand_automata nused used owner typedef node aut = |
227 | 227 |
let initial = (List.hd aut.aut_handlers).hand_state in |
228 |
let aut_state = mkautomata_state used typedef aut.aut_loc aut.aut_id in |
|
228 |
let aut_state = mkautomata_state node.node_id used typedef aut.aut_loc aut.aut_id in
|
|
229 | 229 |
let unodes = List.map (fun h -> node_of_unless nused used node aut.aut_id aut_state h) aut.aut_handlers in |
230 | 230 |
let aunodes = List.map (fun h -> node_of_assign_until nused used node aut.aut_id aut_state h) aut.aut_handlers in |
231 | 231 |
let all_outputs = List.fold_left (fun all (outputs, _, _) -> ISet.union outputs all) ISet.empty aunodes in |
Also available in: Unified diff
[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8)
typing was transformed as a functor and parametrized by basic types (int/real/bool)
it can also be applied multiple times on the same program