Revision 52cfee34 src/normalization.ml
| src/normalization.ml | ||
|---|---|---|
| 196 | 196 |
| Expr_uclock _ |
| 197 | 197 |
| Expr_dclock _ |
| 198 | 198 |
| Expr_phclock _ -> assert false (* Not handled yet *) |
| 199 |
|
|
| 199 |
(* Creates a conditional with a merge construct, which is more lazy *) |
|
| 200 |
(* |
|
| 201 |
let norm_conditional_as_merge alias node norm_expr offsets defvars expr = |
|
| 202 |
match expr.expr_desc with |
|
| 203 |
| Expr_ite (c, t, e) -> |
|
| 204 |
let defvars, norm_t = norm_expr (alias node offsets defvars t in |
|
| 205 |
| _ -> assert false |
|
| 206 |
*) |
|
| 200 | 207 |
and normalize_branches node offsets defvars hl = |
| 201 | 208 |
List.fold_right |
| 202 | 209 |
(fun (t, h) (defvars, norm_q) -> |
| ... | ... | |
| 308 | 315 |
match decl.top_decl_desc with |
| 309 | 316 |
| Node nd -> |
| 310 | 317 |
{decl with top_decl_desc = Node (normalize_node nd)}
|
| 311 |
| Open _ | ImportedNode _ | ImportedFun _ | Consts _ -> decl
|
|
| 318 |
| Open _ | ImportedNode _ | Consts _ -> decl |
|
| 312 | 319 |
|
| 313 | 320 |
let normalize_prog decls = |
| 314 | 321 |
List.map normalize_decl decls |
Also available in: Unified diff