@@ -665,6 +665,36 @@ let bin ?comment (op : J.binop) (e0 : t) (e1 : t) : t =
665
665
let string_of_expression = ref (fun _ -> " " )
666
666
let debug = false
667
667
668
+ (* *
669
+ [push_negation e] attempts to simplify a negated expression by pushing the negation
670
+ deeper into the expression tree. Returns [Some simplified] if simplification is possible,
671
+ [None] otherwise.
672
+
673
+ Simplification rules:
674
+ - [!(not e)] -> [e]
675
+ - [!true] -> [false]
676
+ - [!false] -> [true]
677
+ - [!(a === b)] -> [a !== b]
678
+ - [!(a !== b)] -> [a === b]
679
+ - [!(a && b)] -> [!a || !b] (De Morgan's law)
680
+ - [!(a || b)] -> [!a && !b] (De Morgan's law)
681
+ *)
682
+ let rec push_negation (e : t ) : t option =
683
+ match e.expression_desc with
684
+ | Js_not e -> Some e
685
+ | Bool b -> Some (bool (not b))
686
+ | Bin (EqEqEq, a , b ) -> Some {e with expression_desc = Bin (NotEqEq , a, b)}
687
+ | Bin (NotEqEq, a , b ) -> Some {e with expression_desc = Bin (EqEqEq , a, b)}
688
+ | Bin (And, a , b ) -> (
689
+ match (push_negation a, push_negation b) with
690
+ | Some a_ , Some b_ -> Some {e with expression_desc = Bin (Or , a_, b_)}
691
+ | _ -> None )
692
+ | Bin (Or, a , b ) -> (
693
+ match (push_negation a, push_negation b) with
694
+ | Some a_ , Some b_ -> Some {e with expression_desc = Bin (And , a_, b_)}
695
+ | _ -> None )
696
+ | _ -> None
697
+
668
698
(* *
669
699
[simplify_and e1 e2] attempts to simplify the boolean AND expression [e1 && e2].
670
700
Returns [Some simplified] if simplification is possible, [None] otherwise.
@@ -802,6 +832,16 @@ let rec simplify_and (e1 : t) (e2 : t) : t option =
802
832
- [e || true] -> [true]
803
833
- [false || e] -> [e]
804
834
- [e || false] -> [e]
835
+
836
+ Algebraic transformation strategy:
837
+ When basic rules don't apply, attempts to leverage [simplify_and] by:
838
+ 1. Using the equivalence: [e1 || e2 ≡ !(!(e1) && !(e2))]
839
+ 2. Applying [push_negation] to get [!(e1)] and [!(e2)]
840
+ 3. Using [simplify_and] on these negated terms
841
+ 4. If successful, applying [push_negation] again to get the final result
842
+
843
+ This transformation allows reuse of [simplify_and]'s more extensive optimizations
844
+ in the context of OR expressions.
805
845
*)
806
846
and simplify_or (e1 : t ) (e2 : t ) : t option =
807
847
if debug then
@@ -813,7 +853,13 @@ and simplify_or (e1 : t) (e2 : t) : t option =
813
853
| _ , Bool true -> Some true_
814
854
| Bool false , _ -> Some e2
815
855
| _ , Bool false -> Some e1
816
- | _ -> None
856
+ | _ -> (
857
+ match (push_negation e1, push_negation e2) with
858
+ | Some e1_ , Some e2_ -> (
859
+ match simplify_and e1_ e2_ with
860
+ | Some e -> push_negation e
861
+ | None -> None )
862
+ | _ -> None )
817
863
818
864
let and_ ?comment (e1 : t ) (e2 : t ) : t =
819
865
match (e1.expression_desc, e2.expression_desc) with
0 commit comments