Project

General

Profile

Revision 7659bbb1

View differences:

src/corelang.ml
1331 1331
    Utils.desome node_opt
1332 1332
  with Utils.DeSome -> raise Not_found
1333 1333

  
1334
(* Local Variables: *)
1335
(* compile-command:"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
    (* compile-command:"make -C .." *)
1389
    (* End: *)
src/corelang.mli
197 197

  
198 198
val eq_has_arrows: eq -> bool
199 199

  
200
val  push_negations: ?neg:bool -> expr -> expr
200 201
(* Local Variables: *)
201 202
(* compile-command:"make -C .." *)
202 203
(* End: *)

Also available in: Unified diff