1331 
1331 
Utils.desome node_opt

1332 
1332 
with Utils.DeSome > raise Not_found

1333 
1333 

1334 

(* Local Variables: *)

1335 

(* compilecommand:"make C .." *)

1336 

(* End: *)


1334 
(* Pushing negations in expression. Subtitute operators whenever possible *)


1335 
let rec push_negations ?(neg=false) e =


1336 
let res =


1337 
let pn = push_negations in


1338 
let map desc = { e with expr_desc = desc } in


1339 
match e.expr_desc with


1340 
 Expr_ite (g,t,e) >


1341 
if neg then


1342 
map (Expr_ite(pn g, pn e, pn t))


1343 
else


1344 
map (Expr_ite(pn g, pn t, pn e))


1345 
 Expr_tuple t >


1346 
map (Expr_tuple (List.map (pn ~neg) t))


1347 
 Expr_arrow (e1, e2) >


1348 
map (Expr_arrow (pn ~neg e1, pn ~neg e2))


1349 
 Expr_fby (e1, e2) >


1350 
map (Expr_fby (pn ~neg e1, pn ~neg e2))


1351 
 Expr_pre e >


1352 
map (Expr_pre (pn ~neg e))


1353 
 Expr_appl (op, e', None) when op = "not" >


1354 
if neg then


1355 
push_negations ~neg:false e'


1356 
else


1357 
push_negations ~neg:true e'


1358 
 Expr_appl (op, e', None) when List.mem op (Basic_library.bool_funs @ Basic_library.rel_funs) > (


1359 
match op with


1360 
 "&&" > map (Expr_appl((if neg then "" else op), pn ~neg e', None))


1361 
 "" > map (Expr_appl((if neg then "&&" else op), pn ~neg e', None))


1362 
(* TODO xor/equi/impl *)


1363 
 "<" > map (Expr_appl((if neg then ">=" else op), pn e', None))


1364 
 ">" > map (Expr_appl((if neg then "<=" else op), pn e', None))


1365 
 "<=" > map (Expr_appl((if neg then ">" else op), pn e', None))


1366 
 ">=" > map (Expr_appl((if neg then "<" else op), pn e', None))


1367 
 "!=" > map (Expr_appl((if neg then "=" else op), pn e', None))


1368 
 "=" > map (Expr_appl((if neg then "!=" else op), pn e', None))


1369 


1370 
 _ > assert false


1371 
)


1372 
 Expr_const _


1373 
 Expr_ident _ > if neg then


1374 
mkpredef_call e.expr_loc "not" [e]


1375 
else


1376 
e


1377 
 Expr_appl (op,_,_) >


1378 
if neg then


1379 
mkpredef_call e.expr_loc "not" [e]


1380 
else


1381 
e


1382 
 _ > assert false (* no array, array access, power or merge/when *)


1383 
in


1384 
res


1385 


1386 


1387 
(* Local Variables: *)


1388 
(* compilecommand:"make C .." *)


1389 
(* End: *)
